Dafny: liberalized equality to work when the types could possibly be the same

(i.e. a != b is allowed when a: array<int> and b: array<T>)

5 files changed, 97 insertions, 6 deletions

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 6cf215d6..e013367b 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -2877,8 +2877,10 @@ namespace Microsoft.Dafny {
 

           case BinaryExpr.Opcode.Eq:

           case BinaryExpr.Opcode.Neq:

-            if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

-              Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);

+            if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) {

+              if (!UnifyTypes(e.E0.Type, e.E1.Type)) {

+                Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type);

+              }

             }

             expr.Type = Type.Bool;

             break;

@@ -3270,6 +3272,35 @@ namespace Microsoft.Dafny {
       }

     }

 

+    private bool CouldPossiblyBeSameType(Type A, Type B) {

+      if (A.IsTypeParameter || B.IsTypeParameter) {

+        return true;

+      }

+      if (A.IsArrayType && B.IsArrayType) {

+        Type a = UserDefinedType.ArrayElementType(A);

+        Type b = UserDefinedType.ArrayElementType(B);

+        return CouldPossiblyBeSameType(a, b);

+      }

+      if (A is UserDefinedType && B is UserDefinedType) {

+        UserDefinedType a = (UserDefinedType)A;

+        UserDefinedType b = (UserDefinedType)B;

+        if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass == b.ResolvedClass) {

+          if (a.TypeArgs.Count != b.TypeArgs.Count) {

+            return false; // this probably doesn't happen if the classes are the same.

+          }

+          for (int i = 0; i < a.TypeArgs.Count; i++) {

+            if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i]))

+              return false;

+          }

+          // all parameters could be the same

+          return true;

+        }

+        // either we don't know what class it is yet, or the classes mismatch

+        return false;

+      }

+      return false;

+    }

+

     /// <summary>

     /// Generate an error for every non-ghost feature used in "expr".

     /// Requires "expr" to have been successfully resolved.

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index be41fbf8..8866491e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1574,6 +1574,11 @@ Execution trace:
 

 Dafny program verifier finished with 30 verified, 2 errors

 

+-------------------- LiberalEquality.dfy --------------------

+LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)

+LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)

+2 resolution/type errors detected in LiberalEquality.dfy

+

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy
new file mode 100644
index 00000000..3dc52c80
--- /dev/null
+++ b/Test/dafny0/LiberalEquality.dfy
@@ -0,0 +1,55 @@
+

+class Array<T>

+{

+   var Length: nat;

+}

+

+class Test<T> {

+  var a: Array<int>;

+  var b: Array<T>;

+  predicate valid()

+      reads this, a, b;

+  {

+      a != null && b != null && a != b && a.Length == b.Length

+  }

+}

+

+method m1<T, U>(t: T, u: U)

+   requires t != u;

+{

+   

+}

+

+method m2<T>(t: array<T>, a: array<int>)

+   requires t != null && a != null && t != a && t.Length == a.Length;

+{

+

+}

+

+

+class Weird<T, U, V>

+{

+

+}

+

+

+method m3<T, V>(a: Weird<T, int, V>, b: Weird<T, bool, V>)

+   requires a == b; // Bad: second parameter can't be both bool and int.

+{

+

+}

+

+

+method m4<T, U, V>(a: Weird<T, U, V>, b: Weird<T, bool, V>)

+  requires a == b;

+{

+

+}

+

+

+// Just to make sure nothing went wrong.

+method m5(a: array<int>, b: array<bool>)

+   requires a == b; // Bad: never equal

+{

+

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index e4c134f6..0da7fe3e 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -22,7 +22,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
             LoopModifies.dfy Refinement.dfy RefinementErrors.dfy

             ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy

             CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy

-            Predicates.dfy Skeletons.dfy Maps.dfy) do (

+            Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index e56a8317..3e5a95ef 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -11,10 +11,10 @@ class LazyInitArray<T> {
     reads this, a, b, c;

   {

     a != null && b != null && c != null &&

-    a.Length == |Contents| + 1 &&  // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'

+    a.Length == |Contents| &&

     b.Length == |Contents| &&

     c.Length == |Contents| &&

-    b != c &&

+    b != c && a != b && a != c &&

     0 <= n && n <= c.Length &&

     (forall i :: 0 <= i && i < |Contents| ==>

        Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&

@@ -41,7 +41,7 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    a := new T[N+1];

+    a := new T[N];

     b := new int[N];

     c := new int[N];

     n := 0;