Repository navigation
Conversation
With the optimizer on, solc folds the slot of a mapping entry at a constant key into a PUSH32, and the engine counted that constant as a fixed slot that a write through a symbolic key never reaches, so `m[o] = 5; assert(m[K] == 0)` passed. Before a run, hash the mapping roots of each deployed contract's storage layout (requested as extra output for `--symbolic`) with the source literals and the contract's PUSH immediates, one nested level deep, and record the results as concrete preimages. Constants that no candidate produces, such as ERC-1967 and ERC-7201 roots, stay fixed slots.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
Please address the inline finding.
| for &key in keys.iter().filter(|&&key| key_fits(key_ty, key)) { | ||
| let hash = record_mapping_preimage(cx, key, slot); | ||
| register_mapping_slots(cx, layout, hash, value_id, keys, levels - 1); |
There was a problem hiding this comment.
Please avoid eagerly materializing every candidate-key pair for nested mappings. For mapping(uint256 => mapping(uint256 => uint256)), this iterates all keys again for each outer key and retains N² preimages on every symbolic run, even if the property never accesses the mapping. In a local dev build of this head, a pure assert(x == x) test with that unused mapping and 2,000 unused integer constants took 7.74s and 3.06 GB peak RSS; with 400 constants it took 0.28s and 213 MB. Discovery also has no deadline/cancellation check, so larger projects can exhaust memory or overrun frontier-search budgets. Please avoid retaining the full Cartesian product and honor the deadline while scanning.
The nested level of a folded mapping slot is a product over the candidate keys, and registering it eagerly retained N² preimages on every run, even when the property never touched the mapping. Register the first level eagerly and search the nested level only for a large constant slot the run loads or stores, once per slot, recording only the match. Both scans stop at the run deadline.
A probe of the same constant slot in another contract could suppress nested mapping preimage discovery. Cache only completed searches for a contract-slot pair. The integration test fails without this fix and finds a replayed counterexample with it.
Why
With the optimizer on, solc folds
keccak256(abi.encode(K, slot))for a constant key into a PUSH32. Underforge test --symbolicthat constant counts as a fixed slot that never aliases a write through a symbolic key, som[o] = 5; assert(m[K] == 0)passes althougho == Kbreaks it. Found by symdiff (Tempo, OPT-01); thecheck_/test_twins disagree before and agree after.Change
New
runtime/folded_slots.rs: before a run, for every cached account whose code matches a known artifact with a storage layout, hash each mapping root (also inside structs, one nested level) with every candidate key of a fitting type and record the preimage inconcrete_keccak_preimages. Candidate keys are the contract's PUSH immediates plus source literals from the fuzz literals dictionary, so constants solc folded away still count.ExecutorView::with_projectwires the known contracts and literals at the four runner call sites;forge testaddsstorageLayouttoextra_outputwhen symbolic mode is on. Cases folded intosymbolic_keccak_known_preimage_bases_do_not_alias.Downstream
Base
mablr/evm2-migration. Adds afoundry-compilersdependency to the symbolic crate for the layout types and requestsstorageLayoutoutput in symbolic runs. A registered preimage is a real one, so this adds no unsoundness; ERC-1967 and ERC-7201 constant slots stay fixed slots. Limits: a key that appears in neither the literals nor the bytecode, and a root reached only through assembly (keccak("ns.slot")), are still missed. Cost is keys times roots keccaks per deployed contract per run, not measured on a large project.