Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: implement DELEGATECALL and CALLCODE #159

Merged
merged 4 commits into from
Aug 5, 2023
Merged

feat: implement DELEGATECALL and CALLCODE #159

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
5a2fc5e
feat: implement DELEGATECALL and CALLCODE
daejunpark Aug 4, 2023
23eb302
Merge remote-tracking branch 'origin/main' into feat/delegatecall
daejunpark Aug 4, 2023
a48a4fd
add comments in test
daejunpark Aug 4, 2023
1d6ffe1
fix lint
daejunpark Aug 4, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 8 additions & 3 deletions src/halmos/__main__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
)
Expand Down Expand Up @@ -237,20 +238,21 @@ 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(),
calldata=[],
callvalue=con(0),
caller=mk_caller(args),
this=this,
pgm=creation_bytecode,
symbolic=False,
solver=solver,
)
Expand All @@ -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
Expand Down Expand Up @@ -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={},
Expand Down
46 changes: 32 additions & 14 deletions src/halmos/sevm.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"]
Expand All @@ -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(
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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()
Expand All @@ -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)
)
Expand All @@ -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={},
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -1784,6 +1792,7 @@ def create(
caller=caller,
this=new_addr,
#
pgm=create_code,
pc=0,
st=State(),
jumpis={},
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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"):
Expand Down Expand Up @@ -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),
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -2383,6 +2399,7 @@ def mk_exec(
caller,
this,
#
pgm,
# pc,
# st,
# jumpis,
Expand Down Expand Up @@ -2414,6 +2431,7 @@ def mk_exec(
caller=caller,
this=this,
#
pgm=pgm,
pc=0,
st=State(),
jumpis={},
Expand Down
56 changes: 54 additions & 2 deletions tests/expected/all.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()",
Expand Down Expand Up @@ -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)",
Expand Down Expand Up @@ -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,
Expand Down
Loading