Merge branch 'main' into chore/ruff

src/halmos/__main__.py

@@ -407,60 +407,6 @@ def render_trace(context: CallContext, file=sys.stdout) -> None:
         print(file=file)
 
 
-def run_bytecode(hexcode: str, args: HalmosConfig) -> list[Exec]:
-    solver = mk_solver(args)
-    this = mk_this()
-    message = Message(
-        target=this,
-        caller=mk_caller(args),
-        origin=mk_addr("tx_origin"),
-        value=mk_callvalue(),
-        data=ByteVec(),
-        call_scheme=EVM.CALL,
-    )
-
-    contract = Contract.from_hexcode(hexcode)
-    sevm = SEVM(args)
-    ex = sevm.mk_exec(
-        code={this: contract},
-        storage={this: {}},
-        balance=mk_balance(),
-        block=mk_block(),
-        context=CallContext(message=message),
-        pgm=contract,
-        symbolic=args.symbolic_storage,
-        path=Path(solver),
-    )
-    exs = sevm.run(ex)
-    result_exs = []
-
-    for idx, ex in enumerate(exs):
-        result_exs.append(ex)
-        opcode = ex.current_opcode()
-        error_output = ex.context.output.error
-        returndata = ex.context.output.data
-
-        if error_output:
-            warn_code(
-                INTERNAL_ERROR,
-                f"{mnemonic(opcode)} failed, error={error_output}, returndata={returndata}",
-            )
-        else:
-            print(f"Final opcode: {mnemonic(opcode)})")
-            print(f"Return data: {returndata}")
-            dump_dirname = f"/tmp/halmos-{uuid.uuid4().hex}"
-            model_with_context = gen_model_from_sexpr(
-                GenModelArgs(args, idx, ex.path.to_smt2(args), {}, dump_dirname)
-            )
-            print(f"Input example: {model_with_context.model}")
-
-        if args.print_states:
-            print(f"# {idx+1}")
-            print(ex)
-
-    return result_exs
-
-
 def deploy_test(
     creation_hexcode: str,
     deployed_hexcode: str,
@@ -618,14 +564,11 @@ def setup(
             raise HalmosException(f"No successful path found in {setup_sig}")
 
         if len(setup_exs) > 1:
-            info(
-                f"Warning: multiple paths were found in {setup_sig}; "
-                "an arbitrary path has been selected for the following tests."
-            )
-
             if args.debug:
                 print("\n".join(map(str, setup_exs)))
 
+            raise HalmosException(f"Multiple paths were found in {setup_sig}")
+
         setup_ex = setup_exs[0]
 
         if args.print_setup_states:
@@ -639,12 +582,6 @@ def setup(
             if args.debug:
                 print("\n".join(jumpid_str(x) for x in sevm.logs.bounded_loops))
 
-    if args.reset_bytecode:
-        for assign in [x.split("=") for x in args.reset_bytecode.split(",")]:
-            addr = con_addr(int(assign[0].strip(), 0))
-            new_hexcode = assign[1].strip()
-            setup_ex.set_code(addr, Contract.from_hexcode(new_hexcode))
-
     if args.statistics:
         print(setup_timer.report())
 
@@ -1565,11 +1502,6 @@ def _main(_args=None) -> MainResult:
         print(f"halmos {metadata.version('halmos')}")
         return MainResult(0)
 
-    # quick bytecode execution mode
-    if args.bytecode is not None:
-        run_bytecode(args.bytecode, args)
-        return MainResult(0)
-
     #
     # compile
     #

src/halmos/config.py

@@ -342,20 +342,6 @@ class Config:
 
     ### Experimental options
 
-    bytecode: str = arg(
-        help="execute the given bytecode",
-        global_default=None,
-        metavar="HEX_STRING",
-        group=experimental,
-    )
-
-    reset_bytecode: str = arg(
-        help="reset the bytecode of given addresses after setUp()",
-        global_default=None,
-        metavar="ADDR1=CODE1,ADDR2=CODE2,...",
-        group=experimental,
-    )
-
     test_parallel: bool = arg(
         help="run tests in parallel", global_default=False, group=experimental
     )

tests/expected/all.json

@@ -1600,17 +1600,6 @@
                 "num_bounded_loops": null
             }
         ],
-        "test/Reset.t.sol:ResetTest": [
-            {
-                "name": "check_foo()",
-                "exitcode": 0,
-                "num_models": 0,
-                "models": null,
-                "num_paths": null,
-                "time": null,
-                "num_bounded_loops": null
-            }
-        ],
         "test/Revert.t.sol:CTest": [
             {
                 "name": "check_Revert1(uint256)",

tests/regression/test/Context.t.sol

@@ -191,7 +191,10 @@ contract ContextTest is Test {
     }
 
     function check_call0_normal(uint mode0) public payable {
-        require(mode0 < 9);
+        // vm.assume(mode0 < 9);
+        // NOTE: explicitly branch over mode0, as an infeasible path with mode0 >= 9 may not be eliminated due to an extremely inefficient solver environment (e.g, github workflow)
+        mode0 = split_mode_up_to_9(mode0);
+
         _check_call0(mode0);
     }
 
@@ -221,7 +224,10 @@ contract ContextTest is Test {
     }
 
     function check_call1_normal(uint mode1, uint mode0) public payable {
-        require(mode0 < 9);
+        // vm.assume(mode0 < 9);
+        // NOTE: explicitly branch over mode0, as an infeasible path with mode0 >= 9 may not be eliminated due to an extremely inefficient solver environment (e.g, github workflow)
+        mode0 = split_mode_up_to_9(mode0);
+
         _check_call1(mode1, mode0);
     }
 
@@ -273,6 +279,19 @@ contract ContextTest is Test {
         else if (mode == 10) assert(!success && retdata.length ==  0);
     }
 
+    function split_mode_up_to_9(uint mode) internal returns (uint) {
+             if (mode == 0) return 0;
+        else if (mode == 1) return 1;
+        else if (mode == 2) return 2;
+        else if (mode == 3) return 3;
+        else if (mode == 4) return 4;
+        else if (mode == 5) return 5;
+        else if (mode == 6) return 6;
+        else if (mode == 7) return 7;
+        else if (mode == 8) return 8;
+        else                return 0;
+    }
+
     function returndatasize() internal pure returns (uint size) {
         assembly {
             size := returndatasize()

tests/regression/test/SetupSymbolic.t.sol

@@ -3,7 +3,7 @@ pragma solidity >=0.8.0 <0.9.0;
 
 contract SetupSymbolicTest {
     function setUpSymbolic(uint x) public pure {
-        if (x > 0) return; // generate multiple setup output states
+        if (x > 0) revert(); // generate multiple setup output states, but only a single success output state
     }
 
     function check_True() public pure {

tests/test_cli.py

@@ -5,7 +5,7 @@
 
 from halmos.utils import EVM, hexify
 from halmos.sevm import con, Contract, Instruction
-from halmos.__main__ import str_abi, run_bytecode, FunctionInfo
+from halmos.__main__ import str_abi, FunctionInfo
 
 from test_fixtures import args
 
@@ -104,17 +104,6 @@ def test_decode_mixed_bytecode():
     assert contract.valid_jump_destinations() == set()
 
 
-def test_run_bytecode(args):
-    args = args.with_overrides(
-        source="test_run_bytecode", symbolic_jump=True, print_steps=True
-    )
-
-    hexcode = "34381856FDFDFDFDFDFD5B00"
-    exs = run_bytecode(hexcode, args)
-    assert len(exs) == 1
-    assert exs[0].current_opcode() == EVM.STOP
-
-
 def test_instruction():
     assert str(Instruction(con(0))) == "STOP"
     assert str(Instruction(con(1))) == "ADD"