From 32b81edb41edda432d2d86b5fe43b3a0f02283cd Mon Sep 17 00:00:00 2001
From: karmacoma <karma@coma.lol>
Date: Tue, 23 Jul 2024 16:19:47 -0700
Subject: [PATCH] fix bad abi encoding in createBytes4 (#329)

---
 src/halmos/cheatcodes.py                    |  2 +-
 tests/expected/all.json                     | 11 ++++++-
 tests/regression/test/HalmosCheatCode.t.sol | 36 ++++++++++++++++++---
 3 files changed, 43 insertions(+), 6 deletions(-)

diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
index 97f8f770..9d08c84f 100644
--- a/src/halmos/cheatcodes.py
+++ b/src/halmos/cheatcodes.py
@@ -188,7 +188,7 @@ def create_string(ex, arg):
 
 def create_bytes4(ex, arg):
     name = name_of(extract_string_argument(arg, 0))
-    return uint256(create_generic(ex, 32, name, "bytes4"))
+    return Concat(create_generic(ex, 32, name, "bytes4"), con(0, size_bits=224))
 
 
 def create_bytes32(ex, arg):
diff --git a/tests/expected/all.json b/tests/expected/all.json
index 571c73e2..577e488e 100644
--- a/tests/expected/all.json
+++ b/tests/expected/all.json
@@ -931,7 +931,7 @@
                 "num_bounded_loops": null
             },
             {
-                "name": "check_createBytes4()",
+                "name": "check_createBytes4_basic()",
                 "exitcode": 0,
                 "num_models": 0,
                 "models": null,
@@ -939,6 +939,15 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_createBytes4_finds_selector()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_createInt()",
                 "exitcode": 0,
diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol
index ee928f81..c0c6e10c 100644
--- a/tests/regression/test/HalmosCheatCode.t.sol
+++ b/tests/regression/test/HalmosCheatCode.t.sol
@@ -1,9 +1,16 @@
 // SPDX-License-Identifier: AGPL-3.0
 pragma solidity >=0.8.0 <0.9.0;
 
+import "forge-std/Test.sol";
 import {SymTest} from "halmos-cheatcodes/SymTest.sol";
 
-contract HalmosCheatCodeTest is SymTest {
+contract Beep {
+    function boop() public pure returns (uint256) {
+        return 42;
+    }
+}
+
+contract HalmosCheatCodeTest is SymTest, Test {
     function check_createUint() public {
         uint x = svm.createUint(256, 'x');
         uint y = svm.createUint(160, 'y');
@@ -52,14 +59,35 @@ contract HalmosCheatCodeTest is SymTest {
         assert(0 <= y && y <= type(uint256).max);
     }
 
-    function check_createBytes4() public {
+    function check_createBytes4_basic() public {
         bytes4 x = svm.createBytes4('x');
+
+        uint256 r;
+        assembly {
+            r := returndatasize()
+        }
+        assert(r == 32);
+
         uint256 x_uint = uint256(uint32(x));
-        assert(0 <= x_uint && x_uint <= type(uint32).max);
+        assertLe(x_uint, type(uint32).max);
         uint y; assembly { y := x }
-        assert(0 <= y && y <= type(uint256).max);
+        assertLe(y, type(uint256).max);
     }
 
+    /// @dev we expect a counterexample
+    ///      (meaning that createBytes4 is able to find the selector for boop())
+    function check_createBytes4_finds_selector() public {
+        Beep beep = new Beep();
+
+        bytes4 selector = svm.createBytes4("selector");
+        (bool succ, bytes memory ret) = address(beep).call(abi.encode(selector));
+        vm.assume(succ);
+        uint256 val = abi.decode(ret, (uint256));
+
+        assertNotEq(val, 42);
+    }
+
+
     function check_createAddress() public {
         address x = svm.createAddress('x');
         uint y; assembly { y := x }