From f8025d6d629a730591c40c3f47775bd5fa15be95 Mon Sep 17 00:00:00 2001
From: karmacoma <karma@coma.lol>
Date: Wed, 18 Oct 2023 15:40:48 -0700
Subject: [PATCH] update halmos-cheatcodes + tests + fix createInt

---
 src/halmos/cheatcodes.py                    |  2 +-
 src/halmos/utils.py                         |  9 ++++++
 tests/expected/all.json                     | 36 +++++++++++++++++++++
 tests/lib/halmos-cheatcodes                 |  2 +-
 tests/regression/test/HalmosCheatCode.t.sol | 27 ++++++++++++++++
 5 files changed, 74 insertions(+), 2 deletions(-)

diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
index 528a378d..5cd5f024 100644
--- 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
index 58b1101b..c6832010 100644
--- 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
index 2b8b95a8..e1d99045 100644
--- 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
index c9e5f804..c0d86550 160000
--- a/tests/lib/halmos-cheatcodes
+++ b/tests/lib/halmos-cheatcodes
@@ -1 +1 @@
-Subproject commit c9e5f80441b9d8aeb2e724db07a1322e59aaeb82
+Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5
diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol
index 1207ae48..ee928f81 100644
--- 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,11 +30,21 @@ 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);
@@ -33,6 +52,14 @@ contract HalmosCheatCodeTest is SymTest {
         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 }