Skip to content

Commit

Permalink
update trace
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Feb 19, 2025
1 parent 4dd1340 commit 76d980b
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 4 deletions.
6 changes: 4 additions & 2 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -350,13 +350,15 @@ class StorageWrite:
address: Address
slot: Word
value: Word
transient: bool


@dataclass(frozen=True)
class StorageRead:
address: Address
slot: Word
value: Word
transient: bool


@dataclass(frozen=True)
Expand Down Expand Up @@ -2072,15 +2074,15 @@ def mk_storagedata(self) -> StorageData:
def sload(self, ex: Exec, addr: Any, loc: Word, transient: bool = False) -> Word:
storage = ex.storage if not transient else ex.transient_storage
val = self.storage_model.load(ex, storage, addr, loc)
ex.context.trace.append(StorageRead(addr, loc, val))
ex.context.trace.append(StorageRead(addr, loc, val, transient))
return val

def sstore(
self, ex: Exec, addr: Any, loc: Any, val: Any, transient: bool = False
) -> None:
storage = ex.storage if not transient else ex.transient_storage

ex.context.trace.append(StorageWrite(addr, loc, val))
ex.context.trace.append(StorageWrite(addr, loc, val, transient))

if ex.message().is_static:
raise WriteInStaticContext(ex.context_str())
Expand Down
6 changes: 4 additions & 2 deletions src/halmos/traces.py
Original file line number Diff line number Diff line change
Expand Up @@ -114,12 +114,14 @@ def rendered_slot(slot: Address) -> str:

def rendered_sstore(update: StorageWrite) -> str:
slot_str = rendered_slot(update.slot)
return f"{cyan('SSTORE')} @{slot_str}{hexify(update.value)}"
opcode = cyan("SSTORE" if not update.transient else "TSTORE")
return f"{opcode} @{slot_str}{hexify(update.value)}"


def rendered_sload(read: StorageRead) -> str:
slot_str = rendered_slot(read.slot)
return f"{cyan('SLOAD')} @{slot_str}{hexify(read.value)}"
opcode = cyan("SLOAD" if not read.transient else "TLOAD")
return f"{opcode} @{slot_str}{hexify(read.value)}"


def rendered_trace(context: CallContext) -> str:
Expand Down

0 comments on commit 76d980b

Please sign in to comment.