Skip to content

Commit

Permalink
move code
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Feb 19, 2025
1 parent ca7c6e3 commit 5593859
Showing 1 changed file with 13 additions and 13 deletions.
26 changes: 13 additions & 13 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -1041,19 +1041,6 @@ def context_str(self) -> str:
opcode = self.current_opcode()
return f"addr={hexify(self.this())} pc={self.pc} insn={mnemonic(opcode)}"

def push(self, val) -> None:
val = unbox_int(val)

if isinstance(val, int):
if val in sha3_inv:
# restore precomputed hashes
val = self.sha3_data(con(sha3_inv[val]))
# TODO: support more commonly used concrete keccak values
elif val == EMPTY_KECCAK:
val = self.sha3_data(b"")

self.st._push(val)

def halt(
self,
data: ByteVec | None,
Expand Down Expand Up @@ -1450,6 +1437,19 @@ def ret(self) -> ByteVec:
def int_of(self, x: Any, err: str = None) -> int:
return int_of(x, err, self.path.concretization.substitution)

def push(self, val) -> None:
val = unbox_int(val)

if isinstance(val, int):
if val in sha3_inv:
# restore precomputed hashes
val = self.sha3_data(con(sha3_inv[val]))
# TODO: support more commonly used concrete keccak values
elif val == EMPTY_KECCAK:
val = self.sha3_data(b"")

self.st._push(val)


class Storage:
pass
Expand Down

0 comments on commit 5593859

Please sign in to comment.