Skip to content

Commit

Permalink
refactor: common prefix for uninterpreted function names
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Jun 24, 2024
1 parent b881bc4 commit 84b222e
Showing 2 changed files with 18 additions and 18 deletions.
34 changes: 17 additions & 17 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
@@ -44,21 +44,21 @@

# symbolic states
# calldataload(index)
f_calldataload = Function("calldataload", BitVecSort256, BitVecSort256)
f_calldataload = Function("f_calldataload", BitVecSort256, BitVecSort256)
# calldatasize()
f_calldatasize = Function("calldatasize", BitVecSort256)
f_calldatasize = Function("f_calldatasize", BitVecSort256)
# extcodesize(target address)
f_extcodesize = Function("extcodesize", BitVecSort160, BitVecSort256)
f_extcodesize = Function("f_extcodesize", BitVecSort160, BitVecSort256)
# extcodehash(target address)
f_extcodehash = Function("extcodehash", BitVecSort160, BitVecSort256)
f_extcodehash = Function("f_extcodehash", BitVecSort160, BitVecSort256)
# blockhash(block number)
f_blockhash = Function("blockhash", BitVecSort256, BitVecSort256)
f_blockhash = Function("f_blockhash", BitVecSort256, BitVecSort256)
# gas(cnt)
f_gas = Function("gas", BitVecSort256, BitVecSort256)
f_gas = Function("f_gas", BitVecSort256, BitVecSort256)
# gasprice()
f_gasprice = Function("gasprice", BitVecSort256)
f_gasprice = Function("f_gasprice", BitVecSort256)
# origin()
f_origin = Function("origin", BitVecSort160)
f_origin = Function("f_origin", BitVecSort160)

# uninterpreted arithmetic
f_div = Function("evm_bvudiv", BitVecSort256, BitVecSort256, BitVecSort256)
@@ -811,7 +811,7 @@ def sha3_data(self, data: Bytes) -> Word:
if isinstance(data, bytes):
data = bytes_to_bv_value(data)

f_sha3 = Function(f"sha3_{size * 8}", BitVecSorts[size * 8], BitVecSort256)
f_sha3 = Function(f"f_sha3_{size * 8}", BitVecSorts[size * 8], BitVecSort256)
sha3_expr = f_sha3(data)
else:
sha3_expr = BitVec("sha3_0", BitVecSort256)
@@ -1004,17 +1004,17 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
def decode(cls, loc: Any) -> Any:
loc = normalize(loc)
# m[k] : hash(k.m)
if loc.decl().name() == "sha3_512":
if loc.decl().name() == "f_sha3_512":
args = loc.arg(0)
offset = simplify(Extract(511, 256, args))
base = simplify(Extract(255, 0, args))
return cls.decode(base) + (offset, con(0))
# a[i] : hash(a) + i
elif loc.decl().name() == "sha3_256":
elif loc.decl().name() == "f_sha3_256":
base = loc.arg(0)
return cls.decode(base) + (con(0),)
# m[k] : hash(k.m) where |k| != 256-bit
elif loc.decl().name().startswith("sha3_"):
elif loc.decl().name().startswith("f_sha3_"):
sha3_input = normalize(loc.arg(0))
if sha3_input.decl().name() == "concat" and sha3_input.num_args() == 2:
offset = simplify(sha3_input.arg(0))
@@ -1105,12 +1105,12 @@ def store(cls, ex: Exec, addr: Any, loc: Any, val: Any) -> None:
@classmethod
def decode(cls, loc: Any) -> Any:
loc = normalize(loc)
if loc.decl().name() == "sha3_512": # hash(hi,lo), recursively
if loc.decl().name() == "f_sha3_512": # hash(hi,lo), recursively
args = loc.arg(0)
hi = cls.decode(simplify(Extract(511, 256, args)))
lo = cls.decode(simplify(Extract(255, 0, args)))
return cls.simple_hash(Concat(hi, lo))
elif loc.decl().name().startswith("sha3_"):
elif loc.decl().name().startswith("f_sha3_"):
sha3_input = normalize(loc.arg(0))
if sha3_input.decl().name() == "concat":
decoded_sha3_input_args = [
@@ -1639,7 +1639,7 @@ def call_unknown() -> None:

if arg_size > 0:
f_call = Function(
"call_" + str(arg_size * 8),
"f_call_" + str(arg_size * 8),
BitVecSort256, # cnt
BitVecSort256, # gas
BitVecSort160, # to
@@ -1654,7 +1654,7 @@ def call_unknown() -> None:
exit_code = f_call(con(call_id), gas, to, fund, arg_bv)
else:
f_call = Function(
"call_" + str(arg_size * 8),
"f_call_" + str(arg_size * 8),
BitVecSort256, # cnt
BitVecSort256, # gas
BitVecSort160, # to
@@ -1674,7 +1674,7 @@ def call_unknown() -> None:
ret = ByteVec()
if actual_ret_size > 0:
f_ret = Function(
"ret_" + str(actual_ret_size * 8),
"f_ret_" + str(actual_ret_size * 8),
BitVecSort256,
BitVecSorts[actual_ret_size * 8],
)
2 changes: 1 addition & 1 deletion src/halmos/utils.py
Original file line number Diff line number Diff line change
@@ -61,7 +61,7 @@ def __getitem__(self, size: int) -> BitVecSort:

# ecrecover(digest, v, r, s)
f_ecrecover = Function(
"ecrecover", BitVecSort256, BitVecSort8, BitVecSort256, BitVecSort256, BitVecSort160
"f_ecrecover", BitVecSort256, BitVecSort8, BitVecSort256, BitVecSort256, BitVecSort160
)


0 comments on commit 84b222e

Please sign in to comment.