From 30ce71aa237683845cfa4c9b82de502173c67c66 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 21 Jun 2022 11:40:49 -0700 Subject: [PATCH 1/4] Update BigRational to be compatible with .NET 2.1 --- Source/DafnyRuntime/DafnyRuntime.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index 5857e49be36..adf50ef1fed 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -1594,7 +1594,7 @@ public BigRational(double n) { const ulong exptMask = 0x7FF0000000000000; const ulong mantMask = 0x000FFFFFFFFFFFFF; const int mantBits = 52; - ulong bits = BitConverter.DoubleToUInt64Bits(n); + ulong bits = BitConverter.ToUInt64(BitConverter.GetBytes(n), 0); // Generic conversion bool isNeg = (bits & signMask) != 0; From bcb8a5e16aca52d0e48bab8e8219c4f21be948f3 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 21 Jun 2022 11:42:07 -0700 Subject: [PATCH 2/4] Update DafnyRuntime version to 1.2.0 --- Source/DafnyRuntime/DafnyRuntime.csproj | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 834fd428901..2760b21308a 100755 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -6,7 +6,7 @@ true false TRACE;ISDAFNYRUNTIMELIB - 1.1.0 + 1.2.0 net6.0 ..\..\Binaries\ 7.3 From 52dc26c956f76c7327e25795e3a3b4b80c7ccafa Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 21 Jun 2022 12:04:05 -0700 Subject: [PATCH 3/4] Avoid Double.IsSubnormal --- Source/DafnyRuntime/DafnyRuntime.cs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index adf50ef1fed..9a0a6f96851 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -1583,10 +1583,6 @@ public BigRational(double n) { throw new ArgumentException( "Can't convert +/- infinity to a rational."); } - if (Double.IsSubnormal(n)) { - throw new ArgumentException( - "Can't convert a subnormal value to a rational (yet)."); - } // Double-specific values const int exptBias = 1023; @@ -1600,6 +1596,12 @@ public BigRational(double n) { bool isNeg = (bits & signMask) != 0; int expt = ((int)((bits & exptMask) >> mantBits)) - exptBias; var mant = (bits & mantMask); + + if (expt == -exptBias && mant != 0) { + throw new ArgumentException( + "Can't convert a subnormal value to a rational (yet)."); + } + var one = BigInteger.One; var negFactor = isNeg ? BigInteger.Negate(one) : one; var two = new BigInteger(2); From 8255c7d7b2cc39f41ee0953990819f4cd1f93c91 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 21 Jun 2022 12:14:50 -0700 Subject: [PATCH 4/4] Update release notes with .NET compatibility fix --- RELEASE_NOTES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 742c55ee15a..74033bc5234 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,7 @@ # Upcoming +- fix: The Dafny runtime library for C# is now compatible with .NET Standard 2.1, as it was before 3.7.0. Its version has been updated to 1.2.0 to reflect this. + # 3.7.0 - feat: The Dafny CLI, Dafny as a library, and the C# runtime are now available on NuGet. You can install the CLI with `dotnet tool install --global Dafny`. The library is available as `DafnyPipeline` and the runtime is available as `DafnyRuntime`. (https://github.com/dafny-lang/dafny/pull/2051)