Bugs in HEVM Equivalence

tests/hevm/fail/aliasing/aliasing.act

@@ -0,0 +1,64 @@
+constructor of A
+interface constructor(uint z)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint x := z
+
+
+behaviour x of A
+interface x()
+
+iff
+    CALLVALUE == 0
+
+returns pre(x)
+
+behaviour set_x of A
+interface set_x(uint z)
+
+iff
+    CALLVALUE == 0
+
+storage
+    x => z
+
+
+constructor of B
+interface constructor(address x)
+
+pointers
+    x |-> A
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := x
+
+
+behaviour upd of B
+interface upd()
+
+iff
+    CALLVALUE == 0
+
+storage
+    a.x => 42
+
+
+constructor of C
+interface constructor(address x)
+
+pointers
+    x |-> A
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := create A(42)
+    B b1 := create B(x)
+    B b2 := create B(x)

tests/hevm/fail/aliasing/aliasing.sol

@@ -0,0 +1,38 @@
+pragma solidity >=0.8.0;
+
+contract A {
+    uint public x;
+
+    constructor (uint z)  {
+        x = z;
+    }
+
+    function set_x(uint z) public{
+        x = z;
+    }
+}
+
+contract B {
+    A a;
+
+    constructor(address x) {
+        a = A(x);
+    }
+
+    function upd() public {
+        a.set_x(42);
+    }
+
+}
+
+contract C {
+    A a;
+    B b1;
+    B b2;
+
+    constructor(address x) {
+        a = new A(11);
+        b1 = new B(x);
+        b2 = new B(x);
+    }
+}

tests/hevm/fail/shape/shape.act

@@ -68,13 +68,3 @@ iff
 creates
    A a := y.a
    B b := y 
-
-behaviour change of C
-interface change()
-
-iff
-
-  CALLVALUE == 0
-
-storage
-  a => create A(42)

tests/hevm/fail/shape/shape.sol

@@ -4,11 +4,11 @@ contract A {
     uint public x;
 
     constructor (uint z)  {
-	x = z;
+        x = z;
     }
 
     function set_x(uint z) public{
-	x = z;
+        x = z;
     }
 }
 
@@ -17,8 +17,8 @@ contract B {
     A public a;
 
     constructor (uint z)  {
-	y = z;
-	a = new A(0);
+        y = z;
+        a = new A(0);
     }    
 }
 
@@ -27,11 +27,11 @@ contract C {
     B b;
 
     constructor (address y)  {
-	a = B(y).a();
-	b = B(y);
+        a = B(y).a();
+        b = B(y);
     }
 
     function change() public {
-	a = new A(42);
+        a = new A(42);
     }
 }

tests/hevm/pass/multi6/multi6.act

@@ -0,0 +1,63 @@
+constructor of A
+interface constructor(uint z)
+
+iff
+    CALLVALUE == 0
+
+creates
+    uint x := z
+
+
+behaviour x of A
+interface x()
+
+iff
+    CALLVALUE == 0
+
+returns pre(x)
+
+behaviour set_x of A
+interface set_x(uint z)
+
+iff
+    CALLVALUE == 0
+
+storage
+    x => z
+
+
+constructor of B
+interface constructor(address x)
+
+pointers
+    x |-> A
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := x
+
+
+behaviour upd of B
+interface upd()
+
+iff
+    CALLVALUE == 0
+
+storage
+    a.x => 42
+
+
+constructor of C
+interface constructor(address x)
+
+pointers
+    x |-> A
+
+iff
+    CALLVALUE == 0
+
+creates
+    A a := create A(11)
+    B b := create B(x)

tests/hevm/pass/multi6/multi6.sol

@@ -0,0 +1,36 @@
+pragma solidity >=0.8.0;
+
+contract A {
+    uint public x;
+
+    constructor (uint z)  {
+        x = z;
+    }
+
+    function set_x(uint z) public{
+        x = z;
+    }
+}
+
+contract B {
+    A a;
+
+    constructor(address x) {
+        a = A(x);
+    }
+
+    function upd() public {
+        a.set_x(42);
+    }
+
+}
+
+contract C {
+    A a;
+    B b;
+
+    constructor(address x) {
+        a = new A(11);
+        b = new B(x);
+    }
+}