Update BigRational to be compatible with .NET 2.1 (#2277)

* Avoid Double.IsSubnormal and BitConverter.DoubleToUInt64Bits * Update DafnyRuntime version to 1.2.0 * Update release notes Fixes #2276
dafny-lang · Jun 21, 2022 · 7a72c5f · 7a72c5f
1 parent c85bbd1
commit 7a72c5f
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 6 deletions.
diff --git 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)

diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -1583,23 +1583,25 @@ 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;
       const ulong signMask = 0x8000000000000000;
       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;
       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);

diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj
@@ -6,7 +6,7 @@
       <GeneratePackageOnBuild>true</GeneratePackageOnBuild>
       <GenerateAssemblyInfo>false</GenerateAssemblyInfo>
       <DefineConstants>TRACE;ISDAFNYRUNTIMELIB</DefineConstants>
-      <PackageVersion>1.1.0</PackageVersion>
+      <PackageVersion>1.2.0</PackageVersion>
       <TargetFramework>net6.0</TargetFramework>
       <OutputPath>..\..\Binaries\</OutputPath>
       <LangVersion>7.3</LangVersion>