fix: Type conversions from unsigned Java types (dafny-lang#4384)

Fixes dafny-lang#4152.
keyboardDrummer · Sep 15, 2023 · d8cd09f · d8cd09f
1 parent 09e1ad2
commit d8cd09f
Show file tree

Hide file tree

Showing 6 changed files with 52 additions and 63 deletions.
diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs
@@ -4011,9 +4011,12 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
         if (toType.IsNumericBased(Type.NumericPersuasion.Real)) {
           // (int or bv or char) -> real
           Contract.Assert(AsNativeType(toType) == null);
+          var fromNative = AsNativeType(fromType);
           wr.Write($"new {DafnyBigRationalClass}(");
-          if (AsNativeType(fromType) != null) {
-            wr.Write("java.math.BigInteger.valueOf");
+          if (fromNative != null) {
+            wr.Write(fromNative.LowerBound >= 0
+              ? $"{DafnyHelpersClass}.unsignedToBigInteger"
+              : "java.math.BigInteger.valueOf");
             TrParenExpr(arg, wr, inLetExprBody, wStmts);
             wr.Write(", java.math.BigInteger.ONE)");
           } else if (fromType.IsCharType) {
@@ -4053,19 +4056,10 @@ protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody,
             }
           } else if (fromNative != null && toNative == null) {
             // native (int or bv) -> big-integer (int or bv)
-            if (fromNative.Sel == NativeType.Selection.ULong) {
-              // Can't just use .longValue() because that may return a negative
-              wr.Write($"{DafnyHelpersClass}.unsignedLongToBigInteger");
-              TrParenExpr(arg, wr, inLetExprBody, wStmts);
-            } else {
-              wr.Write("java.math.BigInteger.valueOf(");
-              if (fromNative.LowerBound >= 0) {
-                TrParenExpr($"{GetBoxedNativeTypeName(fromNative)}.toUnsignedLong", arg, wr, inLetExprBody, wStmts);
-              } else {
-                TrParenExpr(arg, wr, inLetExprBody, wStmts);
-              }
-              wr.Write(")");
-            }
+            wr.Write(fromNative.LowerBound >= 0
+              ? $"{DafnyHelpersClass}.unsignedToBigInteger"
+              : "java.math.BigInteger.valueOf");
+            TrParenExpr(arg, wr, inLetExprBody, wStmts);
           } else if (fromNative != null && NativeTypeSize(toNative) == NativeTypeSize(fromNative)) {
             // native (int or bv) -> native (int or bv)
             // Cast between signed and unsigned, which have the same Java type

diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java
@@ -262,7 +262,7 @@ public T select(long i) {
     }
 
     public T selectUnsigned(long i) {
-        return select(Helpers.unsignedLongToBigInteger(i));
+        return select(Helpers.unsignedToBigInteger(i));
     }
 
     public T select(BigInteger i) {
@@ -326,7 +326,7 @@ public DafnySequence<T> drop(long lo) {
     }
 
     public DafnySequence<T> dropUnsigned(long lo) {
-        return drop(Helpers.unsignedLongToBigInteger(lo));
+        return drop(Helpers.unsignedToBigInteger(lo));
     }
 
     public DafnySequence<T> drop(BigInteger lo) {
@@ -357,7 +357,7 @@ public DafnySequence<T> take(long hi) {
     }
 
     public DafnySequence<T> takeUnsigned(long hi) {
-        return take(Helpers.unsignedLongToBigInteger(hi));
+        return take(Helpers.unsignedToBigInteger(hi));
     }
 
     public DafnySequence<T> take(BigInteger hi) {

diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
@@ -248,14 +248,32 @@ public static int unsignedToInt(long x) {
         return (int)x;
     }
 
-    private final static BigInteger ULONG_LIMIT = new BigInteger("18446744073709551616");  // 0x1_0000_0000_0000_0000
-
-    public static BigInteger unsignedLongToBigInteger(long l) {
-        if (0 <= l) {
-            return BigInteger.valueOf(l);
-        } else {
-            return BigInteger.valueOf(l).add(ULONG_LIMIT);
+    private final static BigInteger BYTE_LIMIT =   new BigInteger("256");                   // 0x1_00
+    private final static BigInteger USHORT_LIMIT = new BigInteger("65536");                 // 0x1_0000
+    private final static BigInteger UINT_LIMIT =   new BigInteger("4294967296");            // 0x1_0000_0000
+    private final static BigInteger ULONG_LIMIT =  new BigInteger("18446744073709551616");  // 0x1_0000_0000_0000_0000
+
+    private static BigInteger unsignedToBigInteger_h(BigInteger i, BigInteger LIMIT) {
+        if (i.signum() == -1) {
+            i = i.add(LIMIT);
         }
+        return i;
+    }
+
+    public static BigInteger unsignedToBigInteger(byte b){
+        return unsignedToBigInteger_h(BigInteger.valueOf(b), BYTE_LIMIT);
+    }
+
+    public static BigInteger unsignedToBigInteger(short s){
+        return unsignedToBigInteger_h(BigInteger.valueOf(s), USHORT_LIMIT);
+    }
+
+    public static BigInteger unsignedToBigInteger(int i){
+        return unsignedToBigInteger_h(BigInteger.valueOf(i), UINT_LIMIT);
+    }
+
+    public static BigInteger unsignedToBigInteger(long l){
+        return unsignedToBigInteger_h(BigInteger.valueOf(l), ULONG_LIMIT);
     }
 
     public static byte divideUnsignedByte(byte a, byte b) {

diff --git a/Test/dafny0/TypeConversionsCompile.dfy.java.expect b/Test/dafny0/TypeConversionsCompile.dfy.java.expect
diff --git a/Test/git-issues/git-issue-4152.dfy b/Test/git-issues/git-issue-4152.dfy
@@ -0,0 +1,12 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+method Main() {
+  var a: bv8 := 0xFF;
+  var b: bv16 := 0xFFFF;
+  var c: bv32 := 0xFFFF_FFFF;
+  var d: bv64 := 0xFFFF_FFFF_FFFF_FFFF;
+  var e: bv128 := 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF;
+  print a as real, " ", b as real, " ", c as real, " ", d as real , " ", e as real, "\n";
+  print a as nat, " ", b as nat, " ", c as nat, " ", d as nat, " ", e as nat, "\n";
+  print a as ORDINAL, " ", b as ORDINAL, " ", c as ORDINAL, " ", d as ORDINAL, " ", e as ORDINAL, "\n";
+}
diff --git a/Test/git-issues/git-issue-4152.dfy.expect b/Test/git-issues/git-issue-4152.dfy.expect
@@ -0,0 +1,3 @@
+255.0 65535.0 4294967295.0 18446744073709551615.0 340282366920938463463374607431768211455.0
+255 65535 4294967295 18446744073709551615 340282366920938463463374607431768211455
+255 65535 4294967295 18446744073709551615 340282366920938463463374607431768211455