fix failed() cheatcode error (#359)

src/halmos/cheatcodes.py

@@ -208,6 +208,11 @@ def symbolic_storage(ex, arg, sevm, stack, step_id):
     account_alias = sevm.resolve_address_alias(
         ex, account, stack, step_id, branching=False
     )
+
+    if account_alias is None:
+        error_msg = f"enableSymbolicStorage() is not allowed for a nonexistent account: {hexify(account)}"
+        raise HalmosException(error_msg)
+
     ex.storage[account_alias].symbolic = True
 
 
@@ -528,6 +533,10 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
                 ex, store_account, stack, step_id, branching=False
             )
 
+            if store_account_alias is None:
+                error_msg = f"vm.store() is not allowed for a nonexistent account: {hexify(store_account)}"
+                raise HalmosException(error_msg)
+
             sevm.sstore(ex, store_account_alias, store_slot, store_value)
             return ret
 
@@ -539,6 +548,11 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
                 ex, load_account, stack, step_id, branching=False
             )
 
+            if load_account_alias is None:
+                # since load_account doesn't exist, its storage is empty.
+                # note: the storage cannot be symbolic, as the symbolic storage cheatcode fails for nonexistent addresses.
+                return ByteVec(con(0))
+
             return ByteVec(sevm.sload(ex, load_account_alias, load_slot))
 
         # vm.fee(uint256)

tests/expected/all.json

@@ -1024,6 +1024,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_failed_cheatcode()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Foundry.t.sol:FoundryTest": [
@@ -1237,6 +1246,33 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_enableSymbolicStorage_fail()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_enableSymbolicStorage_nonexistent()",
+                "exitcode": 3,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_enableSymbolicStorage_pass(uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Library.t.sol:LibraryTest": [
@@ -3141,6 +3177,15 @@
             }
         ],
         "test/Store.t.sol:StoreTest": [
+            {
+                "name": "check_load_nonexistent_account(uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_store_Array(uint256,uint256)",
                 "exitcode": 0,
@@ -3167,6 +3212,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_store_nonexistent_account()",
+                "exitcode": 3,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Struct.t.sol:StructTest": [

tests/regression/test/Foundry.t.sol

@@ -37,6 +37,11 @@ contract EarlyFailTest is Test {
         // - counterexample caused by assert(x > 0): x == 0
         assert(x > 0);
     }
+
+    function check_failed_cheatcode() public {
+        // since fail() halts immediately, failed() always returns true here
+        assertFalse(failed());
+    }
 }
 
 contract FoundryTest is Test {

tests/regression/test/HalmosCheatCode.t.sol

@@ -115,6 +115,29 @@ contract HalmosCheatCodeTest is SymTest, Test {
         // NOTE: the following reverts due to the failure of the nonzero check for extcodesize(svm)
         // Dummy(address(svm)).foo();
     }
+
+    function check_enableSymbolicStorage_pass(uint val) public {
+        address dummy = address(new Beep());
+        // initial value is zero
+        assertEq(vm.load(dummy, bytes32(0)), 0);
+
+        vm.store(dummy, bytes32(0), bytes32(val));
+        svm.enableSymbolicStorage(dummy);
+        // enableSymbolicStorage updates only uninitialized slots
+        assertEq(vm.load(dummy, bytes32(0)), bytes32(val));
+    }
+
+    function check_enableSymbolicStorage_fail() public {
+        address dummy = address(new Beep());
+        svm.enableSymbolicStorage(dummy);
+        // storage slots have been initialized with a symbolic value
+        assertEq(vm.load(dummy, bytes32(0)), 0); // fail
+    }
+
+    function check_enableSymbolicStorage_nonexistent() public {
+        // symbolic storage is not allowed for a nonexistent account
+        svm.enableSymbolicStorage(address(0xdeadbeef)); // HalmosException
+    }
 }
 
 interface Dummy {

tests/regression/test/Store.t.sol

@@ -47,4 +47,14 @@ contract StoreTest is Test {
         assert(c.a(key) == value);
         assert(uint(vm.load(address(c), bytes32(uint(keccak256(abi.encode(2))) + key))) == value);
     }
+
+    function check_store_nonexistent_account() public {
+        // vm.store() is not allowed for a nonexistent account
+        vm.store(address(0xdeadbeef), bytes32(0), bytes32(0)); // HalmosException
+    }
+
+    function check_load_nonexistent_account(uint slot) public {
+        // vm.load() from nonexistent accounts returns zero
+        assertEq(vm.load(address(0xdeadbeef), bytes32(slot)), 0);
+    }
 }