From 7a72c5fa507310187355fc7e6e0abac8625b28f6 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Tue, 21 Jun 2022 13:12:37 -0700
Subject: [PATCH] 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
---
 RELEASE_NOTES.md                        |  2 ++
 Source/DafnyRuntime/DafnyRuntime.cs     | 12 +++++++-----
 Source/DafnyRuntime/DafnyRuntime.csproj |  2 +-
 3 files changed, 10 insertions(+), 6 deletions(-)

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)
diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
index 5857e49be36..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;
@@ -1594,12 +1590,18 @@ 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;
       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
index 834fd428901..2760b21308a 100755
--- 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>