Proper object equals

src/nagini_translation/resources/bool.sil

@@ -56,17 +56,17 @@ function int___eq__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), int())
     requires issubtype(typeof(other), int())
-{
-    int___unbox__(self) == int___unbox__(other)
-}
+    ensures result == int___unbox__(self) == int___unbox__(other)
+    ensures result == object___eq__(self, other)
+
 
 function bool___eq__(self: Ref, other: Ref): Bool
     decreases _
     requires issubtype(typeof(self), bool())
     requires issubtype(typeof(other), bool())
-{
-    bool___unbox__(self) == bool___unbox__(other)
-}
+    ensures result == bool___unbox__(self) == bool___unbox__(other)
+    ensures result == object___eq__(self, other)
+
 
 function int___ge__(self: Int, other: Int): Bool
     decreases _
@@ -135,10 +135,25 @@ function int___int__(self: Ref): Ref
     requires issubtype(typeof(self), int())
     ensures result == self
 
-function object___eq__(self: Ref, other: Ref): Bool
-    decreases _
-    ensures self == other ==> result
-    ensures ((self == null) != (other == null)) ==> !result
+domain __ObjectEquality {
+    function object___eq__(Ref, Ref): Bool
+
+    axiom {
+        forall o1: Ref, o2: Ref, o3: Ref ::
+            { object___eq__(o1, o2), object___eq__(o2, o3) }
+            { object___eq__(o1, o2), object___eq__(o1, o3) }
+            { object___eq__(o2, o3), object___eq__(o1, o3) }
+            object___eq__(o1, o2) && object___eq__(o2, o3) ==> object___eq__(o1, o3)
+    }
+
+    axiom {
+        forall o1: Ref, o2: Ref :: { object___eq__(o1, o2) }
+            (object___eq__(o1, o2) == object___eq__(o2, o1)) &&
+            (o1 == o2 ==> object___eq__(o1, o2)) &&
+            (((o1 == null) != (o2 == null)) ==> !object___eq__(o1, o2))
+    }
+
+}
 
 function Place___eq__(self: Ref, other: Ref): Bool
     decreases _

src/nagini_translation/resources/bytes.sil

@@ -33,6 +33,7 @@ function bytes___eq__(self: Ref, other: Ref): Bool
     requires issubtype(typeof(self), bytes())
     ensures (bytes___val__(self) == bytes___val__(other)) == result
     ensures result ==> (issubtype(typeof(other), bytes()) && bytes___len__(self) == bytes___len__(other))
+    ensures result == object___eq__(self, other)
 
 function bytes___sil_seq__(self: Ref) : Seq[Ref]
     decreases _

src/nagini_translation/resources/preamble.index

@@ -559,7 +559,7 @@
         "__eq__": {
             "args": ["tuple", "object"],
             "type": "__prim__bool",
-            "requires": ["__len__", "__getitem__"]
+            "requires": ["__len__", "__getitem__", "object___eq__"]
         },
         "__sil_seq__": {
             "args": ["tuple"],

src/nagini_translation/resources/pset.sil

@@ -52,6 +52,7 @@ function PSet___eq__(self: Ref, other: Ref): Bool
     requires PSet_arg(typeof(self), 0) == PSet_arg(typeof(other), 0)
     ensures result == (PSet___unbox__(self) == PSet___unbox__(other))
     ensures result ==> self == other
+    ensures result == object___eq__(self, other)
 
 
 
@@ -103,3 +104,4 @@ function PMultiset___eq__(self: Ref, other: Ref): Bool
     requires PMultiset_arg(typeof(self), 0) == PMultiset_arg(typeof(other), 0)
     ensures result == (PMultiset___unbox__(self) == PMultiset___unbox__(other))
     ensures result ==> self == other // extensionality
+    ensures result == object___eq__(self, other)

src/nagini_translation/resources/range.sil

@@ -63,6 +63,7 @@ function range___eq__(self: Ref, other: Ref): Bool
   requires issubtype(typeof(self), range_0())
   ensures (range___val__(self) == range___val__(other)) == result
   ensures result ==> (issubtype(typeof(other), range_0()) && range___len__(self) == range___len__(other))
+  ensures result == object___eq__(self, other)
 
 
 function range___contains__(self: Ref, item: Ref): Bool

src/nagini_translation/resources/seq.sil

@@ -64,6 +64,7 @@ function PSeq___eq__(self: Ref, other: Ref): Bool
     requires PSeq_arg(typeof(self), 0) == PSeq_arg(typeof(other), 0)
     ensures result == (PSeq___sil_seq__(self) == PSeq___sil_seq__(other))
     ensures result ==> self == other // extensionality
+    ensures result == object___eq__(self, other)
 
 
 domain __MSHelper[T$] {

src/nagini_translation/resources/str.sil

@@ -29,6 +29,7 @@ function str___eq__(self: Ref, other: Ref): Bool
     requires issubtype(typeof(self), str())
     ensures (str___val__(self) == str___val__(other)) == result
     ensures result ==> (str___len__(self) == str___len__(other))
+    ensures result == object___eq__(self, other)
 
 function str___add__(self: Ref, other: Ref): Ref
     decreases _

src/nagini_translation/resources/tuple.sil

@@ -119,7 +119,9 @@ function tuple___contains__(self: Ref, item: Ref): Bool
 
 function tuple___eq__(self: Ref, other: Ref): Bool
     decreases _
-    ensures (tuple___len__(self) == tuple___len__(other) &&
-             (forall i: Int :: {tuple___getitem__(self, i), tuple___getitem__(other, i)} i >= 0 && i < tuple___len__(self)
-                                ==> tuple___getitem__(self, i) == tuple___getitem__(other, i)))
-             ==> result
+    ensures result <==>
+            (tuple___len__(self) == tuple___len__(other) &&
+             (forall i: Int :: { tuple___getitem__(self, i) }
+                               { tuple___getitem__(other, i)}
+                               i >= 0 && i < tuple___len__(self)
+                                ==> object___eq__(tuple___getitem__(self, i), tuple___getitem__(other, i))))

src/nagini_translation/translators/common.py

@@ -20,6 +20,7 @@
     MAIN_METHOD_NAME,
     MAY_SET_PRED,
     NAME_DOMAIN,
+    OBJECT_TYPE,
     PRIMITIVE_BOOL_TYPE,
     PRIMITIVE_INT_TYPE,
     RANGE_TYPE,
@@ -710,6 +711,12 @@ def get_function_call(self, receiver: PythonType,
             # expression
             return chain_cond_exp(guarded_functions, self.viper, position,
                                   self.no_info(ctx), ctx)
+        elif func_name == '__eq__' and receiver.python_class.name == OBJECT_TYPE:
+            assert len(args) == 2
+            arg1 = self.to_ref(args[0], ctx)
+            arg2 = self.to_ref(args[1], ctx)
+            return self.viper.DomainFuncApp('object___eq__', [arg1, arg2], self.viper.Bool, position,
+                                            self.no_info(ctx), '__ObjectEquality')
         else:
             if receiver.python_class.name == FLOAT_TYPE:
                 if ctx.float_encoding is None: