Skip to content

Commit ca7c6e3

Browse files
daejunparkdaejunpark
committed
fix: move special handling of PUSH into Exec.push()
1 parent 6e7d9e7 commit ca7c6e3

File tree

1 file changed

+70
-67
lines changed

1 file changed

+70
-67
lines changed

‎src/halmos/sevm.py‎

Lines changed: 70 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -488,7 +488,7 @@ def str_memory(self) -> str:
488488
+ "\n"
489489
)
490490

491-
def push(self, v: Word) -> None:
491+
def _push(self, v: Word) -> None:
492492
if isinstance(v, int):
493493
# TODO: support native types on the stack
494494
# if not (0 <= v < 2**256):
@@ -1041,6 +1041,19 @@ def context_str(self) -> str:
10411041
opcode = self.current_opcode()
10421042
return f"addr={hexify(self.this())} pc={self.pc} insn={mnemonic(opcode)}"
10431043

1044+
def push(self, val) -> None:
1045+
val = unbox_int(val)
1046+
1047+
if isinstance(val, int):
1048+
if val in sha3_inv:
1049+
# restore precomputed hashes
1050+
val = self.sha3_data(con(sha3_inv[val]))
1051+
# TODO: support more commonly used concrete keccak values
1052+
elif val == EMPTY_KECCAK:
1053+
val = self.sha3_data(b"")
1054+
1055+
self.st._push(val)
1056+
10441057
def halt(
10451058
self,
10461059
data: ByteVec | None,
@@ -1258,7 +1271,7 @@ def sha3(self) -> None:
12581271
size: int = self.int_of(self.st.pop(), "symbolic SHA3 data size")
12591272
data = self.st.mslice(loc, size).unwrap() if size else b""
12601273
sha3_image = self.sha3_data(data)
1261-
self.st.push(sha3_image)
1274+
self.push(sha3_image)
12621275

12631276
def sha3_hash(self, data: Bytes) -> bytes | None:
12641277
"""return concrete bytes if the hash can be evaluated, otherwise None"""
@@ -2233,7 +2246,7 @@ def callback(new_ex: Exec, stack, step_id):
22332246

22342247
# set status code on the stack
22352248
subcall_success = subcall.output.error is None
2236-
new_ex.st.push(1 if subcall_success else 0)
2249+
new_ex.push(1 if subcall_success else 0)
22372250

22382251
if not subcall_success:
22392252
# revert network states
@@ -2386,7 +2399,7 @@ def call_unknown() -> None:
23862399
f"call_exit_code_{uid()}_{ex.new_call_id():>02}", BitVecSort256
23872400
)
23882401
ex.path.append(exit_code_var == exit_code)
2389-
ex.st.push(exit_code if is_bv_value(exit_code) else exit_code_var)
2402+
ex.push(exit_code if is_bv_value(exit_code) else exit_code_var)
23902403

23912404
# transfer msg.value
23922405
send_callvalue(exit_code_var != ZERO)
@@ -2500,7 +2513,7 @@ def create(
25002513

25012514
if new_addr in ex.code:
25022515
# address conflicts don't revert, they push 0 on the stack and continue
2503-
ex.st.push(0)
2516+
ex.push(0)
25042517
ex.advance_pc()
25052518

25062519
# add a virtual subcontext to the trace for debugging purposes
@@ -2561,11 +2574,11 @@ def callback(new_ex: Exec, stack, step_id):
25612574
new_ex.set_code(new_addr, new_code)
25622575

25632576
# push new address to stack
2564-
new_ex.st.push(uint256(new_addr))
2577+
new_ex.push(uint256(new_addr))
25652578

25662579
else:
25672580
# creation failed
2568-
new_ex.st.push(0)
2581+
new_ex.push(0)
25692582

25702583
# revert network states
25712584
new_ex.code = orig_code.copy()
@@ -2756,12 +2769,12 @@ def calldataload(
27562769

27572770
for candidate in ex.path.concretization.candidates[loaded]:
27582771
new_ex = self.create_branch(ex, loaded == candidate, ex.pc)
2759-
new_ex.st.push(candidate)
2772+
new_ex.push(candidate)
27602773
new_ex.advance_pc()
27612774
stack.push(new_ex, step_id)
27622775
return
27632776

2764-
ex.st.push(loaded)
2777+
ex.push(loaded)
27652778
ex.advance_pc()
27662779
stack.push(ex, step_id)
27672780

@@ -2886,102 +2899,102 @@ def finalize(ex: Exec):
28862899
pass
28872900

28882901
elif EVM.ADD <= opcode <= EVM.SMOD: # ADD MUL SUB DIV SDIV MOD SMOD
2889-
ex.st.push(self.arith(ex, opcode, ex.st.pop(), ex.st.pop()))
2902+
ex.push(self.arith(ex, opcode, ex.st.pop(), ex.st.pop()))
28902903

28912904
elif EVM.ADDMOD <= opcode <= EVM.MULMOD: # ADDMOD MULMOD
2892-
ex.st.push(
2905+
ex.push(
28932906
self.arith2(ex, opcode, ex.st.pop(), ex.st.pop(), ex.st.pop())
28942907
)
28952908

28962909
elif opcode == EVM.EXP:
2897-
ex.st.push(self.arith(ex, opcode, ex.st.pop(), ex.st.pop()))
2910+
ex.push(self.arith(ex, opcode, ex.st.pop(), ex.st.pop()))
28982911

28992912
elif opcode == EVM.LT:
29002913
w1 = ex.st.popi()
29012914
w2 = ex.st.popi()
2902-
ex.st.push(ULT(w1, w2)) # bvult
2915+
ex.push(ULT(w1, w2)) # bvult
29032916

29042917
elif opcode == EVM.GT:
29052918
w1 = ex.st.popi()
29062919
w2 = ex.st.popi()
2907-
ex.st.push(UGT(w1, w2)) # bvugt
2920+
ex.push(UGT(w1, w2)) # bvugt
29082921

29092922
elif opcode == EVM.SLT:
29102923
w1 = ex.st.popi()
29112924
w2 = ex.st.popi()
2912-
ex.st.push(w1 < w2) # bvslt
2925+
ex.push(w1 < w2) # bvslt
29132926

29142927
elif opcode == EVM.SGT:
29152928
w1 = ex.st.popi()
29162929
w2 = ex.st.popi()
2917-
ex.st.push(w1 > w2) # bvsgt
2930+
ex.push(w1 > w2) # bvsgt
29182931

29192932
elif opcode == EVM.EQ:
29202933
w1 = ex.st.pop()
29212934
w2 = ex.st.pop()
29222935

29232936
if eq(w1.sort(), w2.sort()):
2924-
ex.st.push(w1 == w2)
2937+
ex.push(w1 == w2)
29252938
else:
29262939
if is_bool(w1):
29272940
if not is_bv(w2):
29282941
raise ValueError(w2)
2929-
ex.st.push(If(w1, ONE, ZERO) == w2)
2942+
ex.push(If(w1, ONE, ZERO) == w2)
29302943
else:
29312944
if not is_bv(w1):
29322945
raise ValueError(w1)
29332946
if not is_bool(w2):
29342947
raise ValueError(w2)
2935-
ex.st.push(w1 == If(w2, ONE, ZERO))
2948+
ex.push(w1 == If(w2, ONE, ZERO))
29362949

29372950
elif opcode == EVM.ISZERO:
2938-
ex.st.push(is_zero(ex.st.pop()))
2951+
ex.push(is_zero(ex.st.pop()))
29392952

29402953
elif opcode in [EVM.AND, EVM.OR, EVM.XOR]:
2941-
ex.st.push(bitwise(opcode, ex.st.pop(), ex.st.pop()))
2954+
ex.push(bitwise(opcode, ex.st.pop(), ex.st.pop()))
29422955

29432956
elif opcode == EVM.NOT:
2944-
ex.st.push(~ex.st.popi()) # bvnot
2957+
ex.push(~ex.st.popi()) # bvnot
29452958

29462959
elif opcode == EVM.SHL:
29472960
w1 = ex.st.popi()
29482961
w2 = ex.st.popi()
2949-
ex.st.push(w2 << w1) # bvshl
2962+
ex.push(w2 << w1) # bvshl
29502963

29512964
elif opcode == EVM.SAR:
29522965
w1 = ex.st.popi()
29532966
w2 = ex.st.popi()
2954-
ex.st.push(w2 >> w1) # bvashr
2967+
ex.push(w2 >> w1) # bvashr
29552968

29562969
elif opcode == EVM.SHR:
29572970
w1 = ex.st.popi()
29582971
w2 = ex.st.popi()
2959-
ex.st.push(LShR(w2, w1)) # bvlshr
2972+
ex.push(LShR(w2, w1)) # bvlshr
29602973

29612974
elif opcode == EVM.SIGNEXTEND:
29622975
w = ex.int_of(ex.st.popi(), "symbolic SIGNEXTEND size")
29632976
if w <= 30: # if w == 31, result is SignExt(0, value) == value
29642977
bl = (w + 1) * 8
2965-
ex.st.push(SignExt(256 - bl, Extract(bl - 1, 0, ex.st.popi())))
2978+
ex.push(SignExt(256 - bl, Extract(bl - 1, 0, ex.st.popi())))
29662979

29672980
elif opcode == EVM.CALLDATALOAD:
29682981
self.calldataload(ex, stack, step_id)
29692982
continue
29702983

29712984
elif opcode == EVM.CALLDATASIZE:
2972-
ex.st.push(len(ex.calldata()))
2985+
ex.push(len(ex.calldata()))
29732986

29742987
elif opcode == EVM.CALLVALUE:
2975-
ex.st.push(ex.callvalue())
2988+
ex.push(ex.callvalue())
29762989

29772990
elif opcode == EVM.CALLER:
2978-
ex.st.push(uint256(ex.caller()))
2991+
ex.push(uint256(ex.caller()))
29792992

29802993
elif opcode == EVM.ORIGIN:
2981-
ex.st.push(uint256(ex.origin()))
2994+
ex.push(uint256(ex.origin()))
29822995

29832996
elif opcode == EVM.ADDRESS:
2984-
ex.st.push(uint256(ex.this()))
2997+
ex.push(uint256(ex.this()))
29852998

29862999
elif opcode == EVM.EXTCODESIZE:
29873000
account = uint160(ex.st.peek())
@@ -3003,7 +3016,7 @@ def finalize(ex: Exec):
30033016
else 0
30043017
)
30053018

3006-
ex.st.push(codesize)
3019+
ex.push(codesize)
30073020

30083021
elif opcode == EVM.EXTCODECOPY:
30093022
account: Address = uint160(ex.st.peek())
@@ -3050,49 +3063,49 @@ def finalize(ex: Exec):
30503063
else:
30513064
codehash = 0 # vs EMPTY_KECCAK, see EIP-1052
30523065

3053-
ex.st.push(codehash)
3066+
ex.push(codehash)
30543067

30553068
elif opcode == EVM.CODESIZE:
3056-
ex.st.push(len(ex.pgm))
3069+
ex.push(len(ex.pgm))
30573070

30583071
elif opcode == EVM.GAS:
3059-
ex.st.push(f_gas(con(ex.new_gas_id())))
3072+
ex.push(f_gas(con(ex.new_gas_id())))
30603073

30613074
elif opcode == EVM.GASPRICE:
3062-
ex.st.push(f_gasprice())
3075+
ex.push(f_gasprice())
30633076

30643077
elif opcode == EVM.BASEFEE:
3065-
ex.st.push(ex.block.basefee)
3078+
ex.push(ex.block.basefee)
30663079

30673080
elif opcode == EVM.CHAINID:
3068-
ex.st.push(ex.block.chainid)
3081+
ex.push(ex.block.chainid)
30693082

30703083
elif opcode == EVM.COINBASE:
3071-
ex.st.push(uint256(ex.block.coinbase))
3084+
ex.push(uint256(ex.block.coinbase))
30723085

30733086
elif opcode == EVM.DIFFICULTY:
3074-
ex.st.push(ex.block.difficulty)
3087+
ex.push(ex.block.difficulty)
30753088

30763089
elif opcode == EVM.GASLIMIT:
3077-
ex.st.push(ex.block.gaslimit)
3090+
ex.push(ex.block.gaslimit)
30783091

30793092
elif opcode == EVM.NUMBER:
3080-
ex.st.push(ex.block.number)
3093+
ex.push(ex.block.number)
30813094

30823095
elif opcode == EVM.TIMESTAMP:
3083-
ex.st.push(ex.block.timestamp)
3096+
ex.push(ex.block.timestamp)
30843097

30853098
elif opcode == EVM.PC:
3086-
ex.st.push(ex.pc)
3099+
ex.push(ex.pc)
30873100

30883101
elif opcode == EVM.BLOCKHASH:
3089-
ex.st.push(f_blockhash(ex.st.pop()))
3102+
ex.push(f_blockhash(ex.st.pop()))
30903103

30913104
elif opcode == EVM.BALANCE:
3092-
ex.st.push(ex.balance_of(uint160(ex.st.pop())))
3105+
ex.push(ex.balance_of(uint160(ex.st.pop())))
30933106

30943107
elif opcode == EVM.SELFBALANCE:
3095-
ex.st.push(ex.balance_of(ex.this()))
3108+
ex.push(ex.balance_of(ex.this()))
30963109

30973110
elif opcode in [
30983111
EVM.CALL,
@@ -3118,7 +3131,7 @@ def finalize(ex: Exec):
31183131

31193132
elif opcode == EVM.MLOAD:
31203133
loc: int = ex.mloc(check_size=True)
3121-
ex.st.push(ex.st.memory.get_word(loc))
3134+
ex.push(ex.st.memory.get_word(loc))
31223135

31233136
elif opcode == EVM.MSTORE:
31243137
loc: int = ex.mloc(check_size=True)
@@ -3134,19 +3147,19 @@ def finalize(ex: Exec):
31343147
size: int = len(ex.st.memory)
31353148
# round up to the next multiple of 32
31363149
size = ((size + 31) // 32) * 32
3137-
ex.st.push(size)
3150+
ex.push(size)
31383151

31393152
elif opcode == EVM.SLOAD:
31403153
slot: Word = ex.st.pop()
3141-
ex.st.push(self.sload(ex, ex.this(), slot))
3154+
ex.push(self.sload(ex, ex.this(), slot))
31423155

31433156
elif opcode == EVM.SSTORE:
31443157
slot: Word = ex.st.pop()
31453158
value: Word = ex.st.pop()
31463159
self.sstore(ex, ex.this(), slot, value)
31473160

31483161
elif opcode == EVM.RETURNDATASIZE:
3149-
ex.st.push(ex.returndatasize())
3162+
ex.push(ex.returndatasize())
31503163

31513164
elif opcode == EVM.RETURNDATACOPY:
31523165
loc: int = ex.mloc(check_size=False)
@@ -3197,9 +3210,9 @@ def finalize(ex: Exec):
31973210
if idx < 0:
31983211
raise ValueError(idx)
31993212
if idx >= 32:
3200-
ex.st.push(0)
3213+
ex.push(0)
32013214
else:
3202-
ex.st.push(
3215+
ex.push(
32033216
ZeroExt(
32043217
248, Extract((31 - idx) * 8 + 7, (31 - idx) * 8, w)
32053218
)
@@ -3209,7 +3222,7 @@ def finalize(ex: Exec):
32093222
f"Warning: the use of symbolic BYTE indexing may potentially "
32103223
f"impact the performance of symbolic reasoning: BYTE {idx} {w}"
32113224
)
3212-
ex.st.push(self.sym_byte_of(idx, w))
3225+
ex.push(self.sym_byte_of(idx, w))
32133226

32143227
elif EVM.LOG0 <= opcode <= EVM.LOG4:
32153228
if ex.message().is_static:
@@ -3223,24 +3236,14 @@ def finalize(ex: Exec):
32233236
ex.emit_log(EventLog(ex.this(), topics, data))
32243237

32253238
elif opcode == EVM.PUSH0:
3226-
ex.st.push(0)
3239+
ex.push(0)
32273240

32283241
elif EVM.PUSH1 <= opcode <= EVM.PUSH32:
32293242
val = unbox_int(insn.operand)
32303243
if isinstance(val, int):
3231-
if opcode == EVM.PUSH32:
3232-
if val in sha3_inv:
3233-
# restore precomputed hashes
3234-
ex.st.push(ex.sha3_data(con(sha3_inv[val])))
3235-
# TODO: support more commonly used concrete keccak values
3236-
elif val == EMPTY_KECCAK:
3237-
ex.st.push(ex.sha3_data(b""))
3238-
else:
3239-
ex.st.push(val)
3240-
else:
3241-
ex.st.push(val)
3244+
ex.push(val)
32423245
else:
3243-
ex.st.push(uint256(val) if opcode < EVM.PUSH32 else val)
3246+
ex.push(uint256(val) if opcode < EVM.PUSH32 else val)
32443247

32453248
elif EVM.DUP1 <= opcode <= EVM.DUP16:
32463249
ex.st.dup(opcode - EVM.DUP1 + 1)

0 commit comments

Comments
 (0)