feat: replace --symbolic-storage with enableSymbolicStorage(address) cheatcode #355
Conversation
| if loc.size() not in ex.storage[addr].mapping: | ||
| ex.storage[addr].mapping[loc.size()] = cls.empty(addr, loc) |
There was a problem hiding this comment.
| if loc.size() not in ex.storage[addr].mapping: | |
| ex.storage[addr].mapping[loc.size()] = cls.empty(addr, loc) | |
| ex.storage[addr].mapping.setdefault(loc.size(), cls.empty(addr, loc)) |
...but this always evaluates cls.empty(addr, loc) so this may be more expensive?
if we want to avoid that, a defaultdict may be better
There was a problem hiding this comment.
yeah, i want to avoid setdefault in this case. but, how to use defaultdict when the default value is not a constant but a function of loc?
There was a problem hiding this comment.
If default_factory is not None, it is called without arguments to provide a default value for the given key, this value is inserted in the dictionary for the key, and returned.
well that's a problem, I thought the key was passed to the factory 🤨 oh well
There was a problem hiding this comment.
tested this out of curiosity, it seems to work the way I want:
class betterdict(dict):
def __init__(self, factory):
self.factory = factory
def __missing__(self, key):
val = self.factory(key)
self[key] = val
return valI wonder if there's some weird downside to it that would explain why defaultdict doesn't behave this way
There was a problem hiding this comment.
yeah, i will let this particular thing stay as is. this two-liner doesn't look too bad. many other parts have been improved in #356, which looks much better. this part of code is one of the most complicated/convoluted in the codebase, so i'd prefer not to use aggressive optimizations here. 😅
| class Exec: # an execution path | ||
| # network | ||
| code: dict[Address, Contract] | ||
| storage: dict[Address, dict[int, Any]] # address -> { storage slot -> value } | ||
| storage: dict[Address, StorageData] # address -> { storage slot -> value } |
There was a problem hiding this comment.
would a defaultdict work here? we wouldn't have to check if keys exist and explicitly initialize them
There was a problem hiding this comment.
yes, done in #356
| num_keys = len(keys) | ||
| size_keys = cls.bitsize(keys) | ||
| if slot not in ex.storage[addr]: | ||
| ex.storage[addr][slot] = {} | ||
| if num_keys not in ex.storage[addr][slot]: | ||
| ex.storage[addr][slot][num_keys] = {} | ||
| if size_keys not in ex.storage[addr][slot][num_keys]: | ||
| if slot not in ex.storage[addr].mapping: | ||
| ex.storage[addr].mapping[slot] = {} | ||
| if num_keys not in ex.storage[addr].mapping[slot]: | ||
| ex.storage[addr].mapping[slot][num_keys] = {} | ||
| if size_keys not in ex.storage[addr].mapping[slot][num_keys]: | ||
| if size_keys == 0: | ||
| if ex.symbolic: | ||
| if ex.storage[addr].symbolic: | ||
| label = f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00" | ||
| ex.storage[addr][slot][num_keys][size_keys] = BitVec( | ||
| ex.storage[addr].mapping[slot][num_keys][size_keys] = BitVec( | ||
| label, BitVecSort256 | ||
| ) | ||
| else: | ||
| ex.storage[addr][slot][num_keys][size_keys] = ZERO | ||
| ex.storage[addr].mapping[slot][num_keys][size_keys] = ZERO | ||
| else: | ||
| # do not use z3 const array `K(BitVecSort(size_keys), ZERO)` when not ex.symbolic | ||
| # instead use normal smt array, and generate emptyness axiom; see load() | ||
| ex.storage[addr][slot][num_keys][size_keys] = cls.empty( | ||
| ex.storage[addr].mapping[slot][num_keys][size_keys] = cls.empty( |
There was a problem hiding this comment.
take this as a soft suggestion and please double check if it is equivalent. I just applied a couple of my heuristics:
setdefaultinstead ofif x not in y: y[x] = ...- avoid repeated dict lookups, factor them out in their own variable (e.g.
storage = ex.storage[addr]) - reduce nesting with early exits when applicable (e.g.
if size_keys in slot_mapping[num_keys]: return) - move variable definitions close to their point of use
Gives the following:
@classmethod
def init(cls, ex: Exec, addr: Any, slot: int, keys: tuple) -> None:
assert_address(addr)
storage = ex.storage[addr]
storage.mapping.setdefault(slot, {})
num_keys = len(keys)
slot_mapping = storage.mapping[slot]
slot_mapping.setdefault(num_keys, {})
size_keys = cls.bitsize(keys)
if size_keys in slot_mapping[num_keys]:
return
if size_keys != 0:
# do not use z3 const array `K(BitVecSort(size_keys), ZERO)` when not ex.symbolic
# instead use normal smt array, and generate emptyness axiom; see load()
slot_mapping[num_keys][size_keys] = cls.empty(addr, slot, keys)
return
# size_keys == 0
if storage.symbolic:
label = f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00"
slot_mapping[num_keys][size_keys] = BitVec(label, BitVecSort256)
else:
slot_mapping[num_keys][size_keys] = ZEROThere was a problem hiding this comment.
taking it a couple steps further:
- factoring out
slot_mapping[num_keys] - using the return value of setdefault)
- turn if else blocks into a single expression
becomes:
@classmethod
def init(cls, ex: Exec, addr: Any, slot: int, keys: tuple) -> None:
assert_address(addr)
storage = ex.storage[addr]
slot_mapping = storage.mapping.setdefault(slot, {})
num_keys = len(keys)
slot_mapping_num_keys = slot_mapping.setdefault(num_keys, {})
size_keys = cls.bitsize(keys)
if size_keys in slot_mapping_num_keys:
return
if size_keys != 0:
# do not use z3 const array `K(BitVecSort(size_keys), ZERO)` when not ex.symbolic
# instead use normal smt array, and generate emptyness axiom; see load()
slot_mapping_num_keys[size_keys] = cls.empty(addr, slot, keys)
return
# size_keys == 0
slot_mapping_num_keys[size_keys] = (
mk_uint256(f"storage_{id_str(addr)}_{slot}_{num_keys}_{size_keys}_00")
if storage.symbolic
else ZERO
)There was a problem hiding this comment.
could be improved with a better name for slot_mapping_num_keys, but I don't have a good intuition for what it should be
| else: | ||
| if not ex.symbolic: | ||
| if not ex.storage[addr].symbolic: | ||
| # generate emptyness axiom for each array index, instead of using quantified formula; see init() | ||
| ex.path.append( | ||
| Select(cls.empty(addr, slot, keys), concat(keys)) == ZERO | ||
| ) | ||
| return ex.select( | ||
| ex.storage[addr][slot][num_keys][size_keys], concat(keys), ex.storages | ||
| ex.storage[addr].mapping[slot][num_keys][size_keys], | ||
| concat(keys), | ||
| ex.storages, | ||
| ex.storage[addr].symbolic, | ||
| ) |
There was a problem hiding this comment.
I would avoid the else block after the return and decrease nesting here
daejunpark
changed the title
daejunpark
changed the title
Co-authored-by: karmacoma <karma@coma.lol>
|
thanks for the refactoring suggestion! let me implement it in a separate pr, as this pr is already quite nontrivial. |
done in #356 |
this simplifies the code logic, and improves usability as well. note that the symbolic storage feature is not frequently used.
(to be merged after #352) todo: