fix: Use the right comparison operators for JS bitvectors and Go ordi…

…nals (#2716) Closes #2672 and #2769.
dafny-lang · Sep 20, 2022 · 968595c · 968595c
1 parent a969ac0
commit 968595c
Show file tree

Hide file tree

Showing 5 changed files with 184 additions and 11 deletions.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -4,6 +4,7 @@
 - feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
+- fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)
 - fix: Retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
 - fix: Correctly substitute variables introduced by a binding guard (https://github.com/dafny-lang/dafny/pull/2745)
 

diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs
@@ -2905,7 +2905,7 @@ private bool IsDirectlyComparable(Type t) {
     }
 
     private bool IsOrderedByCmp(Type t) {
-      return t.IsIntegerType || t.IsRealType || (t.IsBitVectorType && t.AsBitVectorType.NativeType == null) || (t.AsNewtype is NewtypeDecl nt && nt.NativeType == null);
+      return t.IsIntegerType || t.IsRealType || t.IsBigOrdinalType || (t.IsBitVectorType && t.AsBitVectorType.NativeType == null) || (t.AsNewtype is NewtypeDecl nt && nt.NativeType == null);
     }
 
     private bool IsComparedByEquals(Type t) {

diff --git a/Source/DafnyCore/Compilers/Compiler-js.cs b/Source/DafnyCore/Compilers/Compiler-js.cs
@@ -1923,6 +1923,18 @@ bool IsDirectlyComparable(Type t) {
       return t.IsBoolType || t.IsCharType || AsNativeType(t) != null || t.IsRefType;
     }
 
+    bool IsRepresentedAsBigNumber(Type t) {
+      if (AsNativeType(t) != null) {
+        return false;
+      } else if (t.AsBitVectorType is { } bvt) {
+        return bvt.NativeType == null;
+      } else {
+        return t.IsNumericBased(Type.NumericPersuasion.Int)
+          || t.IsBitVectorType
+          || t.IsBigOrdinalType;
+      }
+    }
+
     protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
       Expression e0, Expression e1, IToken tok, Type resultType,
       out string opString,
@@ -2017,38 +2029,46 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
           }
 
         case BinaryExpr.ResolvedOpcode.Lt:
-          if (e0.Type.IsNumericBased() && AsNativeType(e0.Type) == null) {
+          if (AsNativeType(e0.Type) != null) {
+            opString = "<";
+          } else if (IsRepresentedAsBigNumber(e0.Type) || e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
             callString = "isLessThan";
           } else {
-            opString = "<";
+            Contract.Assert(false); throw new cce.UnreachableException();
           }
           break;
         case BinaryExpr.ResolvedOpcode.Le:
-          if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && AsNativeType(e0.Type) == null) {
+          if (AsNativeType(e0.Type) != null) {
+            opString = "<=";
+          } else if (IsRepresentedAsBigNumber(e0.Type)) {
             callString = "isLessThanOrEqualTo";
-          } else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && AsNativeType(e0.Type) == null) {
+          } else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
             callString = "isAtMost";
           } else {
-            opString = "<=";
+            Contract.Assert(false); throw new cce.UnreachableException();
           }
           break;
         case BinaryExpr.ResolvedOpcode.Ge:
-          if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && AsNativeType(e0.Type) == null) {
+          if (AsNativeType(e0.Type) != null) {
+            opString = ">=";
+          } else if (IsRepresentedAsBigNumber(e0.Type)) {
             callString = "isLessThanOrEqualTo";
             reverseArguments = true;
-          } else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && AsNativeType(e0.Type) == null) {
+          } else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
             callString = "isAtMost";
             reverseArguments = true;
           } else {
-            opString = ">=";
+            Contract.Assert(false); throw new cce.UnreachableException();
           }
           break;
         case BinaryExpr.ResolvedOpcode.Gt:
-          if (e0.Type.IsNumericBased() && AsNativeType(e0.Type) == null) {
+          if (AsNativeType(e0.Type) != null) {
+            opString = ">";
+          } else if (IsRepresentedAsBigNumber(e0.Type) || e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
             callString = "isLessThan";
             reverseArguments = true;
           } else {
-            opString = ">";
+            Contract.Assert(false); throw new cce.UnreachableException();
           }
           break;
         case BinaryExpr.ResolvedOpcode.LeftShift:

diff --git a/Test/git-issues/git-issue-2672.dfy b/Test/git-issues/git-issue-2672.dfy
@@ -0,0 +1,100 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
+// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+newtype sreal = r: real | r > -4 as real
+newtype sint = r: int | r > -4 as int
+newtype ssreal = r: sreal | r > -3 as sreal
+newtype ssint = r: sint | r > -3 as sint
+
+method Print(b: bool, end: string)
+  // Print boolean `b` as `true` or `false`, then print `end`.  This is needed
+  // by C++ due to BUG(https://github.com/dafny-lang/dafny/issues/2773).
+{
+  if b {
+    print "true";
+  } else {
+    print "false";
+  }
+  print end;
+}
+
+method Main() {
+  Print(24 as real <= 1507 as real, " ");
+  Print(24 as sreal <= 1507 as sreal, " ");
+  Print(24 as ssreal <= 1507 as ssreal, " ");
+  Print(24 as int <= 1507 as int, " ");
+  Print(24 as sint <= 1507 as sint, " ");
+  Print(24 as ssint <= 1507 as ssint, " ");
+  Print(24 as bv16 <= 1507 as bv16, " ");
+  Print(24 as bv232 <= 1507 as bv232, " ");
+  Print(24 as char <= 1507 as char, " ");
+  Print(24 as ORDINAL <= 1507 as ORDINAL, "\n");
+
+  Print(24 as real == 1507 as real, " ");
+  Print(24 as sreal == 1507 as sreal, " ");
+  Print(24 as ssreal == 1507 as ssreal, " ");
+  Print(24 as int == 1507 as int, " ");
+  Print(24 as sint == 1507 as sint, " ");
+  Print(24 as ssint == 1507 as ssint, " ");
+  Print(24 as bv16 == 1507 as bv16, " ");
+  Print(24 as bv232 == 1507 as bv232, " ");
+  Print(24 as char == 1507 as char, " ");
+  Print(24 as ORDINAL == 1507 as ORDINAL, "\n");
+
+  Print(24 as real >= 1507 as real, " ");
+  Print(24 as sreal >= 1507 as sreal, " ");
+  Print(24 as ssreal >= 1507 as ssreal, " ");
+  Print(24 as int >= 1507 as int, " ");
+  Print(24 as sint >= 1507 as sint, " ");
+  Print(24 as ssint >= 1507 as ssint, " ");
+  Print(24 as bv16 >= 1507 as bv16, " ");
+  Print(24 as bv232 >= 1507 as bv232, " ");
+  Print(24 as char >= 1507 as char, " ");
+  Print(24 as ORDINAL >= 1507 as ORDINAL, "\n");
+
+  Print(24 as real < 1507 as real, " ");
+  Print(24 as sreal < 1507 as sreal, " ");
+  Print(24 as ssreal < 1507 as ssreal, " ");
+  Print(24 as int < 1507 as int, " ");
+  Print(24 as sint < 1507 as sint, " ");
+  Print(24 as ssint < 1507 as ssint, " ");
+  Print(24 as bv16 < 1507 as bv16, " ");
+  Print(24 as bv232 < 1507 as bv232, " ");
+  Print(24 as char < 1507 as char, " ");
+  Print(24 as ORDINAL < 1507 as ORDINAL, "\n");
+
+  Print(24 as real != 1507 as real, " ");
+  Print(24 as sreal != 1507 as sreal, " ");
+  Print(24 as ssreal != 1507 as ssreal, " ");
+  Print(24 as int != 1507 as int, " ");
+  Print(24 as sint != 1507 as sint, " ");
+  Print(24 as ssint != 1507 as ssint, " ");
+  Print(24 as bv16 != 1507 as bv16, " ");
+  Print(24 as bv232 != 1507 as bv232, " ");
+  Print(24 as char != 1507 as char, " ");
+  Print(24 as ORDINAL != 1507 as ORDINAL, "\n");
+
+  Print(24 as real > 1507 as real, " ");
+  Print(24 as sreal > 1507 as sreal, " ");
+  Print(24 as ssreal > 1507 as ssreal, " ");
+  Print(24 as int > 1507 as int, " ");
+  Print(24 as sint > 1507 as sint, " ");
+  Print(24 as ssint > 1507 as ssint, " ");
+  Print(24 as bv16 > 1507 as bv16, " ");
+  Print(24 as bv232 > 1507 as bv232, " ");
+  Print(24 as char > 1507 as char, " ");
+  Print(24 as ORDINAL > 1507 as ORDINAL, "\n");
+
+  Print(0 as bv0 <= 0 as bv0, " ");
+  Print(0 as bv0 == 0 as bv0, " ");
+  Print(0 as bv0 >= 0 as bv0, "\n");
+
+  Print(0 as bv0 < 0 as bv0, " ");
+  Print(0 as bv0 != 0 as bv0, " ");
+  Print(0 as bv0 > 0 as bv0, "\n");
+}
diff --git a/Test/git-issues/git-issue-2672.dfy.expect b/Test/git-issues/git-issue-2672.dfy.expect
@@ -0,0 +1,52 @@
+
+Dafny program verifier finished with 5 verified, 0 errors
+
+Dafny program verifier did not attempt verification
+true true true true true true true true true true
+false false false false false false false false false false
+false false false false false false false false false false
+true true true true true true true true true true
+true true true true true true true true true true
+false false false false false false false false false false
+true true true
+false false false
+
+Dafny program verifier did not attempt verification
+true true true true true true true true true true
+false false false false false false false false false false
+false false false false false false false false false false
+true true true true true true true true true true
+true true true true true true true true true true
+false false false false false false false false false false
+true true true
+false false false
+
+Dafny program verifier did not attempt verification
+true true true true true true true true true true
+false false false false false false false false false false
+false false false false false false false false false false
+true true true true true true true true true true
+true true true true true true true true true true
+false false false false false false false false false false
+true true true
+false false false
+
+Dafny program verifier did not attempt verification
+true true true true true true true true true true
+false false false false false false false false false false
+false false false false false false false false false false
+true true true true true true true true true true
+true true true true true true true true true true
+false false false false false false false false false false
+true true true
+false false false
+
+Dafny program verifier did not attempt verification
+true true true true true true true true true true
+false false false false false false false false false false
+false false false false false false false false false false
+true true true true true true true true true true
+true true true true true true true true true true
+false false false false false false false false false false
+true true true
+false false false