update halmos-cheatcodes + tests + fix createInt

a16z · Oct 18, 2023 · f8025d6 · f8025d6
1 parent 084eaa4
commit f8025d6
Show file tree

Hide file tree

Showing 5 changed files with 74 additions and 2 deletions.
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
@@ -179,7 +179,7 @@ def create_int(ex, arg):
             raise HalmosException(f"bitsize larger than 256: {bits}")
 
         name = name_of(extract_string_argument(arg, 1))
-        return halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}")
+        return int256(halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}"))
 
     @staticmethod
     def create_int256(ex, arg):

diff --git a/src/halmos/utils.py b/src/halmos/utils.py
@@ -71,6 +71,15 @@ def uint256(x: BitVecRef) -> BitVecRef:
     return simplify(ZeroExt(256 - bitsize, x))
 
 
+def int256(x: BitVecRef) -> BitVecRef:
+    bitsize = x.size()
+    if bitsize > 256:
+        raise ValueError(x)
+    if bitsize == 256:
+        return x
+    return simplify(SignExt(256 - bitsize, x))
+
+
 def uint160(x: BitVecRef) -> BitVecRef:
     bitsize = x.size()
     if bitsize > 256:

diff --git a/tests/expected/all.json b/tests/expected/all.json
@@ -870,6 +870,42 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_createBytes4()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createInt()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createInt256()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_createString()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_createUint()",
                 "exitcode": 0,

diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes
diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol
@@ -13,6 +13,15 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= z && z <= type(uint8).max);
     }
 
+    function check_createInt() public {
+        int x = svm.createInt(256, 'x');
+        int y = svm.createInt(160, 'y');
+        int z = svm.createInt(8, 'z');
+        assert(type(int256).min <= x && x <= type(int256).max);
+        assert(type(int160).min <= y && y <= type(int160).max);
+        assert(type(int8).min <= z && z <= type(int8).max);
+    }
+
     function check_createBytes() public {
         bytes memory data = svm.createBytes(2, 'data');
         uint x = uint(uint8(data[0]));
@@ -21,18 +30,36 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= y && y <= type(uint8).max);
     }
 
+    function check_createString() public {
+        string memory data = svm.createString(5, 'str');
+        assert(bytes(data).length == 5);
+    }
+
     function check_createUint256() public {
         uint x = svm.createUint256('x');
         assert(0 <= x && x <= type(uint256).max);
     }
 
+    function check_createInt256() public {
+        int x = svm.createInt256('x');
+        assert(type(int256).min <= x && x <= type(int256).max);
+    }
+
     function check_createBytes32() public {
         bytes32 x = svm.createBytes32('x');
         assert(0 <= uint(x) && uint(x) <= type(uint256).max);
         uint y; assembly { y := x }
         assert(0 <= y && y <= type(uint256).max);
     }
 
+    function check_createBytes4() public {
+        bytes4 x = svm.createBytes4('x');
+        uint256 x_uint = uint256(uint32(x));
+        assert(0 <= x_uint && x_uint <= type(uint32).max);
+        uint y; assembly { y := x }
+        assert(0 <= y && y <= type(uint256).max);
+    }
+
     function check_createAddress() public {
         address x = svm.createAddress('x');
         uint y; assembly { y := x }