diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 59fa49cc..a2a05617 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -210,6 +210,7 @@ def run_bytecode(hexcode: str, args: Namespace) -> List[Exec]: callvalue=callvalue, caller=caller, this=this, + pgm=contract, symbolic=args.symbolic_storage, solver=solver, ) @@ -237,13 +238,13 @@ def deploy_test( args: Namespace, ) -> Exec: # test contract creation bytecode - contract = Contract.from_hexcode(hexcode) + creation_bytecode = Contract.from_hexcode(hexcode) solver = mk_solver(args) this = mk_this() ex = sevm.mk_exec( - code={this: contract}, + code={this: Contract(b"")}, storage={this: {}}, balance=mk_balance(), block=mk_block(), @@ -251,6 +252,7 @@ def deploy_test( callvalue=con(0), caller=mk_caller(args), this=this, + pgm=creation_bytecode, symbolic=False, solver=solver, ) @@ -268,7 +270,9 @@ def deploy_test( raise ValueError(f"constructor: failed: {ex.current_opcode()}: {ex.error}") # deployed bytecode - ex.code[this] = Contract(ex.output) + deployed_bytecode = Contract(ex.output) + ex.code[this] = deployed_bytecode + ex.pgm = deployed_bytecode # reset vm state ex.pc = 0 @@ -436,6 +440,7 @@ def run( caller=setup_ex.caller, this=setup_ex.this, # + pgm=setup_ex.code[setup_ex.this], pc=0, st=State(), jumpis={}, diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index de8c728d..9b101ad7 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -613,6 +613,7 @@ class Exec: # an execution path caller: Address # msg.sender this: Address # current account address # vm state + pgm: Contract pc: int st: State # stack and memory jumpis: Dict[str, Dict[bool, int]] # for loop detection @@ -644,6 +645,7 @@ def __init__(self, **kwargs) -> None: self.caller = kwargs["caller"] self.this = kwargs["this"] # + self.pgm = kwargs["pgm"] self.pc = kwargs["pc"] self.st = kwargs["st"] self.jumpis = kwargs["jumpis"] @@ -667,10 +669,10 @@ def __init__(self, **kwargs) -> None: assert_address(self.this) def current_opcode(self) -> UnionType[int, BitVecRef]: - return unbox_int(self.code[self.this][self.pc]) + return unbox_int(self.pgm[self.pc]) def current_instruction(self) -> Instruction: - return self.code[self.this].decode_instruction(self.pc) + return self.pgm.decode_instruction(self.pc) def str_cnts(self) -> str: return "".join( @@ -735,7 +737,7 @@ def __str__(self) -> str: ) def next_pc(self) -> None: - self.pc = self.code[self.this].next_pc(self.pc) + self.pc = self.pgm.next_pc(self.pc) def check(self, cond: Any) -> Any: self.solver.push() @@ -980,7 +982,7 @@ def is_jumpdest(self, x: Word) -> bool: if pc < 0: raise ValueError(pc) - opcode = unbox_int(self.code[self.this][pc]) + opcode = unbox_int(self.pgm[pc]) return opcode == EVM.JUMPDEST def jumpi_id(self) -> str: @@ -1261,7 +1263,7 @@ def call( to = uint160(ex.st.pop()) - if op == EVM.STATICCALL: + if op == EVM.STATICCALL or op == EVM.DELEGATECALL: fund = con(0) else: fund = ex.st.pop() @@ -1284,7 +1286,8 @@ def call( orig_balance = deepcopy(ex.balance) orig_log = deepcopy(ex.log) - if not (is_bv_value(fund) and fund.as_long() == 0): + if op == EVM.CALL and not (is_bv_value(fund) and fund.as_long() == 0): + # no balance update for CALLCODE which transfers to itself ex.balance_update( caller, self.arith(ex, EVM.SUB, ex.balance_of(caller), fund) ) @@ -1307,10 +1310,11 @@ def call_known() -> None: block=ex.block, # calldata=calldata, - callvalue=fund, - caller=caller, - this=to, + callvalue=fund if op != EVM.DELEGATECALL else ex.callvalue, + caller=caller if op != EVM.DELEGATECALL else ex.caller, + this=to if op in [EVM.CALL, EVM.STATICCALL] else ex.this, # + pgm=ex.code[to], pc=0, st=State(), jumpis={}, @@ -1345,6 +1349,7 @@ def call_known() -> None: new_ex.this = ex.this # restore vm state + new_ex.pgm = ex.pgm new_ex.pc = ex.pc new_ex.st = deepcopy(ex.st) new_ex.jumpis = deepcopy(ex.jumpis) @@ -1749,11 +1754,14 @@ def create( # new account address new_addr = ex.new_address() + if new_addr in ex.code: + raise ValueError(f"existing address: {new_addr}") + for addr in ex.code: ex.solver.add(new_addr != addr) # ensure new address is fresh # setup new account - ex.code[new_addr] = create_code # existing code must be empty + ex.code[new_addr] = Contract(b"") # existing code must be empty ex.storage[new_addr] = {} # existing storage may not be empty and reset here # lookup prank @@ -1784,6 +1792,7 @@ def create( caller=caller, this=new_addr, # + pgm=create_code, pc=0, st=State(), jumpis={}, @@ -1825,6 +1834,7 @@ def create( new_ex.this = ex.this # restore vm state + new_ex.pgm = ex.pgm new_ex.pc = ex.pc new_ex.st = deepcopy(ex.st) new_ex.jumpis = deepcopy(ex.jumpis) @@ -1923,7 +1933,7 @@ def jump(self, ex: Exec, stack: List[Tuple[Exec, int]], step_id: int) -> None: # otherwise, create a new execution for feasible targets elif self.options["sym_jump"]: - for target in ex.code[ex.this].valid_jump_destinations(): + for target in ex.pgm.valid_jump_destinations(): target_reachable = simplify(dst == target) if ex.check(target_reachable) != unsat: # jump if self.options.get("debug"): @@ -1952,6 +1962,7 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec: caller=ex.caller, this=ex.this, # + pgm=ex.pgm, pc=target, st=deepcopy(ex.st), jumpis=deepcopy(ex.jumpis), @@ -2174,7 +2185,7 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: elif opcode == EVM.EXTCODEHASH: ex.st.push(f_extcodehash(ex.st.pop())) elif opcode == EVM.CODESIZE: - ex.st.push(con(len(ex.code[ex.this]))) + ex.st.push(con(len(ex.pgm))) elif opcode == EVM.GAS: ex.st.push(f_gas(con(ex.new_gas_id()))) elif opcode == EVM.GASPRICE: @@ -2206,7 +2217,12 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: elif opcode == EVM.SELFBALANCE: ex.st.push(ex.balance_of(ex.this)) - elif opcode == EVM.CALL or opcode == EVM.STATICCALL: + elif opcode in [ + EVM.CALL, + EVM.CALLCODE, + EVM.DELEGATECALL, + EVM.STATICCALL, + ]: self.call(ex, opcode, stack, step_id, out, bounded_loops) continue @@ -2288,7 +2304,7 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: size: int = int_of(ex.st.pop(), "symbolic CODECOPY size") wextend(ex.st.memory, loc, size) - codeslice = ex.code[ex.this][offset : offset + size] + codeslice = ex.pgm[offset : offset + size] ex.st.memory[loc : loc + size] = iter_bytes(codeslice) elif opcode == EVM.BYTE: @@ -2383,6 +2399,7 @@ def mk_exec( caller, this, # + pgm, # pc, # st, # jumpis, @@ -2414,6 +2431,7 @@ def mk_exec( caller=caller, this=this, # + pgm=pgm, pc=0, st=State(), jumpis={}, diff --git a/tests/expected/all.json b/tests/expected/all.json index 967842d2..0986b58f 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -125,6 +125,40 @@ "num_bounded_loops": null } ], + "test/Call.t.sol:CallTest": [ + { + "name": "check_call(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_callcode(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_delegatecall(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_staticcall(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Console.t.sol:ConsoleTest": [ { "name": "check_log()", @@ -155,6 +189,24 @@ "num_bounded_loops": null } ], + "test/Constructor.t.sol:ConstructorTest": [ + { + "name": "check_constructor()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_setCodesize()", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Counter.t.sol:CounterTest": [ { "name": "check_div_1(uint256,uint256)", @@ -772,8 +824,8 @@ ], "test/Proxy.t.sol:ProxyTest": [ { - "name": "check_foo(uint256)", - "exitcode": 1, + "name": "check_foo(uint256,uint256,address)", + "exitcode": 0, "num_models": 0, "num_paths": null, "time": null, diff --git a/tests/test/Call.t.sol b/tests/test/Call.t.sol new file mode 100644 index 00000000..40a72c2e --- /dev/null +++ b/tests/test/Call.t.sol @@ -0,0 +1,146 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +contract C { + uint public num; + function foo(uint x) public payable returns (address, uint, address) { + if (x > 0) num = x; + return (msg.sender, msg.value, address(this)); + } +} + +contract D { + uint public num; + C public c; + + constructor () { + c = new C(); + } + + function call_foo(uint x) public payable returns (bool success, bytes memory retdata) { + (success, retdata) = address(c).call{ value: msg.value }(abi.encodeWithSelector(c.foo.selector, x)); + } + + function staticcall_foo(uint x) public payable returns (bool success, bytes memory retdata) { + (success, retdata) = address(c).staticcall(abi.encodeWithSelector(c.foo.selector, x)); + } + + function delegatecall_foo(uint x) public payable returns (bool success, bytes memory retdata) { + (success, retdata) = address(c).delegatecall(abi.encodeWithSelector(c.foo.selector, x)); + } + + function callcode_foo(uint x) public payable returns (bool success, bytes memory retdata) { + address msg_sender; + uint msg_value; + address target; + + bytes4 sig = c.foo.selector; + + assembly { + let m := mload(0x40) + mstore(m, sig) + mstore(add(m, 0x04), x) + success := callcode(gas(), sload(c.slot), callvalue(), m, 0x24, m, 0x60) + msg_sender := mload(m) + msg_value := mload(add(m, 0x20)) + target := mload(add(m, 0x40)) + } + + retdata = abi.encode(msg_sender, msg_value, target); + } +} + +contract CallTest is Test { + D d; + + function setUp() public { + d = new D(); + } + + function check_call(uint x, uint fund) public payable { + vm.deal(address(this), fund); + vm.deal(address(d), 0); + vm.deal(address(d.c()), 0); + + (bool success, bytes memory retdata) = d.call_foo{ value: fund }(x); + vm.assume(success); + (address msg_sender, uint msg_value, address target) = abi.decode(retdata, (address, uint, address)); + + assert(msg_sender == address(d)); + assert(msg_value == fund); + assert(target == address(d.c())); + + assert(d.num() == 0); + assert(d.c().num() == x); + + assert(address(this).balance == 0); + assert(address(d).balance == 0); + assert(address(d.c()).balance == fund); + } + + function check_staticcall(uint x, uint fund) public payable { + vm.deal(address(this), fund); + vm.deal(address(d), 0); + vm.deal(address(d.c()), 0); + + (bool success, bytes memory retdata) = d.staticcall_foo{ value: fund }(x); + vm.assume(success); + (address msg_sender, uint msg_value, address target) = abi.decode(retdata, (address, uint, address)); + + assert(msg_sender == address(d)); + assert(msg_value == 0); // no fund transfer for staticcall + assert(target == address(d.c())); + + assert(d.num() == 0); + assert(d.c().num() == x); + + assert(address(this).balance == 0); + assert(address(d).balance == fund); + assert(address(d.c()).balance == 0); + } + + function check_delegatecall(uint x, uint fund) public payable { + vm.deal(address(this), fund); + vm.deal(address(d), 0); + vm.deal(address(d.c()), 0); + + (bool success, bytes memory retdata) = d.delegatecall_foo{ value: fund }(x); + vm.assume(success); + (address msg_sender, uint msg_value, address target) = abi.decode(retdata, (address, uint, address)); + + // delegatecall is executed in the caller's context + assert(msg_sender == address(this)); + assert(msg_value == fund); + assert(target == address(d)); + + assert(d.num() == x); // delegatecall updates the caller's state + assert(d.c().num() == 0); + + assert(address(this).balance == 0); + assert(address(d).balance == fund); // no fund transfer for delegatecall + assert(address(d.c()).balance == 0); + } + + function check_callcode(uint x, uint fund) public payable { + vm.deal(address(this), fund); + vm.deal(address(d), 0); + vm.deal(address(d.c()), 0); + + (bool success, bytes memory retdata) = d.callcode_foo{ value: fund }(x); + vm.assume(success); + (address msg_sender, uint msg_value, address target) = abi.decode(retdata, (address, uint, address)); + + assert(msg_sender == address(d)); + assert(msg_value == fund); + assert(target == address(d)); // callcode calls to itself + + assert(d.num() == x); // callcode updates the caller's state + assert(d.c().num() == 0); + + assert(address(this).balance == 0); + assert(address(d).balance == fund); // fund is transfered to itself + assert(address(d.c()).balance == 0); + } +} diff --git a/tests/test/Constructor.t.sol b/tests/test/Constructor.t.sol new file mode 100644 index 00000000..0bf9069a --- /dev/null +++ b/tests/test/Constructor.t.sol @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +contract C { + uint public codesize_; + uint public extcodesize_; + + constructor () { + setCodesize(); + } + + function setCodesize() public { + assembly { + sstore(codesize_.slot, codesize()) + sstore(extcodesize_.slot, extcodesize(address())) + } + } +} + +contract ConstructorTest { + C c; + + function setUp() public { + c = new C(); + } + + function check_constructor() public { + assert(c.codesize_() > 0); // contract creation bytecode size + assert(c.extcodesize_() == 0); // code is not yet deposited in the network state during constructor() + } + + function check_setCodesize() public { + uint creation_codesize = c.codesize_(); + + c.setCodesize(); + + assert(c.codesize_() > 0); // deployed bytecode size + assert(c.extcodesize_() > 0); // deployed bytecode size + assert(c.codesize_() == c.extcodesize_()); + + assert(c.codesize_() < creation_codesize); // deployed bytecode is smaller than creation bytecode + } +} diff --git a/tests/test/Proxy.t.sol b/tests/test/Proxy.t.sol index 3e3fbc87..c89dfc5a 100644 --- a/tests/test/Proxy.t.sol +++ b/tests/test/Proxy.t.sol @@ -6,8 +6,9 @@ import {ERC1967Proxy} from "openzeppelin-contracts/contracts/proxy/ERC1967/ERC19 contract C { uint public num; - function foo(uint x) public { + function foo(uint x) public payable returns (address, uint, address) { num = x; + return (msg.sender, msg.value, address(this)); } } @@ -20,9 +21,15 @@ contract ProxyTest is Test { c = C(address(new ERC1967Proxy(address(cImpl), ""))); } - function check_foo(uint x) public { - c.foo(x); - assert(c.num() == x); // currently unsupported // TODO: support DELEGATECALL + function check_foo(uint x, uint fund, address caller) public { + vm.deal(caller, fund); + vm.prank(caller); + (address msg_sender, uint msg_value, address target) = c.foo{ value: fund }(x); + assert(msg_sender == caller); + assert(msg_value == fund); + assert(target == address(c)); + + assert(c.num() == x); assert(cImpl.num() == 0); } } diff --git a/tests/test/TestConstructor.t.sol b/tests/test/TestConstructor.t.sol index e1a1c0be..4641a597 100644 --- a/tests/test/TestConstructor.t.sol +++ b/tests/test/TestConstructor.t.sol @@ -6,10 +6,17 @@ contract TestConstructorTest { uint constant const = 2; uint immutable flag; uint value; + uint codesize_; + uint extcodesize_; constructor () { flag = 3; value = 4; + + assembly { + sstore(codesize_.slot, codesize()) + sstore(extcodesize_.slot, extcodesize(address())) + } } function check_value() public view { @@ -17,5 +24,8 @@ contract TestConstructorTest { assert(const == 2); assert(flag == 3); assert(value == 4); + + assert(codesize_ > 0); + assert(extcodesize_ == 0); } } diff --git a/tests/test_sevm.py b/tests/test_sevm.py index f85d44a6..9f267bf6 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -51,8 +51,9 @@ def storage(): def mk_ex(hexcode, sevm, solver, storage, caller, this): + bytecode = Contract(hexcode) return sevm.mk_exec( - code={this: Contract(hexcode)}, + code={this: bytecode}, storage={this: storage}, balance=balance, block=mk_block(), @@ -60,6 +61,7 @@ def mk_ex(hexcode, sevm, solver, storage, caller, this): callvalue=callvalue, caller=caller, this=this, + pgm=bytecode, symbolic=True, solver=solver, )