Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update BigRational to be compatible with .NET 2.1 #2277

Merged
merged 4 commits into from
Jun 21, 2022
Merged

Update BigRational to be compatible with .NET 2.1 #2277

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
30ce71a
Update BigRational to be compatible with .NET 2.1
atomb Jun 21, 2022
bcb8a5e
Update DafnyRuntime version to 1.2.0
atomb Jun 21, 2022
52dc26c
Avoid Double.IsSubnormal
atomb Jun 21, 2022
8255c7d
Update release notes with .NET compatibility fix
atomb Jun 21, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions RELEASE_NOTES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
12 changes: 7 additions & 5 deletions Source/DafnyRuntime/DafnyRuntime.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyRuntime/DafnyRuntime.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down