fix(symbolic): find writes beyond materialized_size in dynamic memory reads

.changelog/fix-symbolic-memory-dynamic-read-false-negative.md

@@ -0,0 +1,6 @@
+---
+forge: patch
+foundry-evm-symbolic: patch
+---
+
+Fixed a false negative in symbolic execution's dynamic-offset memory reads: a write recorded past the tracked materialized region (including one dispatched as symbolic despite its offset being constant-evaluable) could silently read back as zero instead of its stored value, which could hide a genuine violation behind an apparent "Safe" result.

crates/evm/symbolic/src/runtime/memory.rs

@@ -233,25 +233,15 @@ impl SymMemory {
         } else {
             let size = Self::size_after_access_word(cx, offset.clone(), 32);
             self.expand_to(cx, size);
-            self.load_word_dynamic(cx, &offset)
+            // Delegate to `read_bytes_offset`'s dynamic-offset path rather than
+            // maintaining a separate implementation here: it already assembles a
+            // dynamic read out of `byte_dynamic_with_delta`, which is the single
+            // place responsible for staying sound with respect to writes whose
+            // own offset is genuinely symbolic (see that function's doc comment).
+            Ok(self.read_bytes_offset(cx, offset, 32).word_at(cx, 0))
         }
     }
 
-    fn load_word_dynamic(
-        &self,
-        cx: &mut SymCx,
-        offset: &SymExpr,
-    ) -> Result<SymExpr, SymbolicError> {
-        let mut result = SymExpr::zero(cx);
-        for candidate in (0..self.materialized_size).rev() {
-            let candidate_expr = SymExpr::constant(cx, U256::from(candidate));
-            let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
-            let word = self.load_word(cx, candidate)?;
-            result = SymExpr::ite(cx, condition, word, result);
-        }
-        Ok(result)
-    }
-
     pub(crate) fn read_concrete(
         &self,
         cx: &mut SymCx,
@@ -439,18 +429,80 @@ impl SymMemory {
         result
     }
 
+    /// Resolves the byte at logical position `offset + delta` for a
+    /// dynamic (non-constant) `offset`.
+    ///
+    /// `store_symbolic_bytes` records writes without extending
+    /// `materialized_size`, including writes whose offsets are
+    /// constant-evaluable but not literal constants. Therefore,
+    /// `materialized_size` does not automatically bound every recorded
+    /// write; a write recorded via `store_symbolic_bytes` can land at a
+    /// position the candidate enumeration below never reaches, and would
+    /// silently read back as zero instead of its stored value.
+    ///
+    /// When every recorded write's full extent is provably within
+    /// `materialized_size`, that bound is a correct bound and the
+    /// enumeration below (unchanged from before) is sound. Only when at
+    /// least one write falls outside that guarantee do we fall back to
+    /// folding every write directly
+    /// against the (symbolic) read target, mirroring `byte()`'s own
+    /// technique -- which already handles a symbolic write offset soundly,
+    /// just for a *concrete* read target -- generalized to a symbolic one.
+    /// This full fold is deliberately not combined with the bounded
+    /// enumeration: doing so would require re-deriving cross-write
+    /// insertion-order priority by hand, and get it wrong for two writes
+    /// that could alias at solve time.
+    ///
+    /// The bound check below is deliberately `write.concrete_offset()`
+    /// (`offset.eval()`, full evaluation) *combined with* a checked
+    /// `offset + len <= materialized_size` extent check -- not
+    /// `concrete_offset().is_some()` alone. `materialized_size` is only
+    /// ever bumped by `store_bytes` (reached when the store dispatch's
+    /// `offset.as_const()` succeeds) and, separately, by
+    /// `store_symbolic_sized_bytes` when its own `offset.eval()` succeeds.
+    /// A write can land in `store_symbolic_bytes` (no bump, ever) because
+    /// `as_const()` -- a shallow single-node check -- failed on an offset
+    /// expression that `eval()` -- full recursive evaluation -- can still
+    /// resolve to a constant. `concrete_offset()` uses `eval()`, so such a
+    /// write reports as "concrete" here even though `materialized_size`
+    /// was never extended to cover it. Requiring the full extent to fit
+    /// inside the current bound (not just the offset to be evaluable)
+    /// catches exactly that mismatch and routes it to the safe fold-every-
+    /// write fallback instead of silently reading back zero.
     pub(crate) fn byte_dynamic_with_delta(
         &self,
         cx: &mut SymCx,
         offset: &SymExpr,
         delta: usize,
     ) -> SymExpr {
+        let materialized_size = self.materialized_size;
+        let all_writes_bounded = self.symbolic_writes.iter().all(|write| {
+            write
+                .concrete_offset()
+                .and_then(|write_offset| write_offset.checked_add(write.bytes.len()))
+                .is_some_and(|end| end <= materialized_size)
+        });
+
+        if all_writes_bounded {
+            let mut result = SymExpr::zero(cx);
+            for candidate in (delta..self.materialized_size).rev() {
+                let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta));
+                let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
+                let byte = self.byte(cx, candidate);
+                result = SymExpr::ite(cx, condition, byte, result);
+            }
+            return result;
+        }
+
+        let target = SymExpr::add_const(cx, offset.clone(), U256::from(delta));
         let mut result = SymExpr::zero(cx);
-        for candidate in (delta..self.materialized_size).rev() {
-            let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta));
-            let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
-            let byte = self.byte(cx, candidate);
-            result = SymExpr::ite(cx, condition, byte, result);
+        for write in &self.symbolic_writes {
+            for idx in 0..write.bytes.len() {
+                let write_offset = SymExpr::add_const(cx, write.offset.clone(), U256::from(idx));
+                let condition = SymBoolExpr::eq(cx, write_offset, target.clone());
+                let byte = write.bytes.byte(cx, idx);
+                result = SymExpr::ite(cx, condition, byte, result);
+            }
         }
         result
     }

crates/evm/symbolic/src/tests.rs

@@ -1173,6 +1173,256 @@ fn memory_symbolic_write_after_concrete_overwrite_still_applies() {
     assert_eq!(loaded.eval_model(&later_symbolic_wins).unwrap(), U256::from(0xbb));
 }
 
+#[test]
+fn memory_dynamic_read_finds_symbolic_write_with_no_concrete_write_at_all() {
+    // Regression for a false negative: a store at a genuinely symbolic offset
+    // never extends `materialized_size` (there is no concrete candidate to
+    // extend it to), so a dynamic read used to enumerate zero candidates and
+    // silently return zero instead of the write's actual value.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let write_offset = SymExpr::var(&mut cx, "write_offset");
+    let byte = SymExpr::var(&mut cx, "byte");
+    memory.store_byte_offset(&mut cx, write_offset, byte);
+
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0);
+
+    let model = symbolic_model(
+        &mut cx,
+        [
+            ("write_offset".to_string(), U256::from(500)),
+            ("read_offset".to_string(), U256::from(500)),
+            ("byte".to_string(), U256::from(0xcd)),
+        ],
+    );
+    assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xcd));
+}
+
+#[test]
+fn memory_dynamic_read_finds_symbolic_write_beyond_concretely_materialized_region() {
+    // Same defect, shaped like the realistic trigger: some concrete writes
+    // establish a modest `materialized_size` (e.g. a Solidity free-memory
+    // pointer write), then a *symbolic*-offset write lands well past that
+    // region with no further concrete write. A dynamic read at the symbolic
+    // write's own location must still find it.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let concrete = SymExpr::constant(&mut cx, U256::from(0xaa));
+    memory.store_byte(&mut cx, 0x20, concrete); // establishes a small materialized_size
+
+    let write_offset = SymExpr::var(&mut cx, "write_offset");
+    let byte = SymExpr::var(&mut cx, "byte");
+    memory.store_byte_offset(&mut cx, write_offset, byte); // symbolic offset, well past 0x20
+
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0);
+
+    let model = symbolic_model(
+        &mut cx,
+        [
+            ("write_offset".to_string(), U256::from(0x200)),
+            ("read_offset".to_string(), U256::from(0x200)),
+            ("byte".to_string(), U256::from(0xef)),
+        ],
+    );
+    assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xef));
+}
+
+#[test]
+fn memory_load_word_offset_dynamic_finds_symbolic_write_beyond_materialized_region() {
+    // Same defect via `load_word_offset` (MLOAD's entry point), which used to
+    // have its own separate, independently-buggy `load_word_dynamic` bounded
+    // the same way. Now delegates through the fixed read path.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let concrete = SymExpr::constant(&mut cx, U256::from(0xaa));
+    memory.store_byte(&mut cx, 0x20, concrete);
+
+    let write_offset = SymExpr::var(&mut cx, "write_offset");
+    let word = SymExpr::var(&mut cx, "word");
+    memory.store_word_offset(&mut cx, write_offset, word);
+
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap();
+
+    let model = symbolic_model(
+        &mut cx,
+        [
+            ("write_offset".to_string(), U256::from(0x200)),
+            ("read_offset".to_string(), U256::from(0x200)),
+            ("word".to_string(), U256::from(0x1234)),
+        ],
+    );
+    assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0x1234));
+}
+
+#[test]
+fn memory_dynamic_read_finds_write_at_const_evaluable_but_undispatched_concrete_offset() {
+    // Regression for the store-dispatch / `concrete_offset()` mismatch: store
+    // dispatch (`store_byte_offset` et al.) gates on `offset.as_const()` -- a
+    // shallow "is this literally a `Const` node" check -- to decide whether a
+    // write bumps `materialized_size`. `SymbolicMemoryWrite::concrete_offset`
+    // gates on the strictly broader `offset.eval()` (full recursive
+    // evaluation). `Keccak(1) & 0xff` evaluates to a concrete, small value via
+    // `eval()` without ever folding to a literal `Const` at construction time
+    // (the mask-folding rules in `and_const` have no case for a bare
+    // `Keccak` operand), so `as_const()` reports `None`, the write is
+    // dispatched through `store_symbolic_bytes` -- which never bumps
+    // `materialized_size` -- while `concrete_offset()` still reports it as
+    // concrete. A naive `concrete_offset().is_some()` fast-path predicate
+    // would wrongly trust `materialized_size` here and silently return zero.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let (write_offset, concrete_write_offset) = undispatched_concrete_offset(&mut cx, 1);
+
+    let write_byte = SymExpr::constant(&mut cx, U256::from(0xef));
+    memory.store_byte_offset(&mut cx, write_offset, write_byte);
+
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0);
+
+    let model = symbolic_model(&mut cx, [("read_offset".to_string(), concrete_write_offset)]);
+    assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xef));
+}
+
+#[test]
+fn memory_load_word_offset_dynamic_finds_write_at_const_evaluable_but_undispatched_concrete_offset()
+{
+    // Same defect as above, exercised through `load_word_offset` (MLOAD's
+    // entry point) with a materialized region already established by an
+    // ordinary concrete store, matching the realistic trigger: some earlier
+    // concrete writes give a modest `materialized_size`, then a write whose
+    // offset only *looks* symbolic to the store dispatch (but is actually
+    // const-evaluable) lands past that region.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let filler = SymExpr::constant(&mut cx, U256::from(0xaa));
+    memory.store_byte(&mut cx, 31, filler); // establishes materialized_size = 32
+
+    let (write_offset, concrete_write_offset) = undispatched_concrete_offset(&mut cx, 2);
+
+    let write_byte = SymExpr::constant(&mut cx, U256::from(0xef));
+    memory.store_byte_offset(&mut cx, write_offset, write_byte);
+
+    // Read a full word starting exactly at the write's own (now-known)
+    // concrete position, so the write's byte lands at the word's most
+    // significant (first) position.
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap();
+
+    let model = symbolic_model(&mut cx, [("read_offset".to_string(), concrete_write_offset)]);
+    let mut expected_bytes = [0u8; 32];
+    expected_bytes[0] = 0xef;
+    let expected = U256::from_be_bytes(expected_bytes);
+    assert_eq!(loaded.eval_model(&model).unwrap(), expected);
+}
+
+/// Builds an offset expression that is const-evaluable (via `Keccak(..) &
+/// 0xff`) but not `as_const()`-able, so store dispatch never bumps
+/// `materialized_size` for a write using it, while `concrete_offset()`
+/// still resolves it to a concrete value. Returns the offset expression and
+/// its resolved concrete value (in `0..=0xff`, unpredictable but
+/// deterministic per `seed`).
+fn undispatched_concrete_offset(cx: &mut SymCx, seed: u64) -> (SymExpr, U256) {
+    let preimage = SymExpr::constant(cx, U256::from(seed));
+    let len = SymExpr::constant(cx, U256::from(1));
+    let name = stable_symbol(cx, "test-keccak-offset", &seed.to_be_bytes());
+    let keccak = SymExpr::keccak_symbol(cx, name, len, vec![preimage]);
+    let mask = SymExpr::constant(cx, U256::from(0xff));
+    let offset = SymExpr::binop(cx, SymBinOp::And, keccak, mask);
+    assert!(offset.as_const().is_none(), "must not fold to a literal Const at construction");
+    let value = offset.eval().expect("Keccak(const) & 0xff is fully evaluable with no free vars");
+    (offset, value)
+}
+
+#[test]
+fn memory_dynamic_read_finds_write_straddling_the_materialized_boundary() {
+    // Coverage gap named by review: the fast-path predicate must reject a
+    // write whose const-evaluable-but-undispatched offset starts INSIDE the
+    // current `materialized_size` bound but whose full extent (offset +
+    // length) ends past it. A predicate that only checked the offset itself
+    // (not the write's full extent) would wrongly accept this write into
+    // the bounded fast path, which stops enumerating at `materialized_size`
+    // and would miss the write's tail bytes.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let (write_offset, offset_value) = undispatched_concrete_offset(&mut cx, 3);
+    let offset_usize = usize::try_from(offset_value).unwrap();
+
+    // A concrete filler two bytes past the write's own start pins
+    // `materialized_size` to `offset + 2`: inside the write's real 32-byte
+    // extent (`store_word_offset` always writes a full EVM word), so it
+    // starts inside the bound and ends well past it.
+    let filler = SymExpr::constant(&mut cx, U256::from(0xaa));
+    memory.store_byte(&mut cx, offset_usize + 1, filler);
+
+    let write_word = SymExpr::var(&mut cx, "write_word");
+    memory.store_word_offset(&mut cx, write_offset, write_word);
+
+    // Read word-local index 3 (a marker byte placed there via the model) --
+    // inside the write's real extent but well past `materialized_size`, so
+    // a predicate that ignored the write's full extent would have wrongly
+    // trusted the bounded fast path and returned zero here.
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.byte_dynamic_with_delta(&mut cx, &read_offset, 0);
+
+    let mut write_word_bytes = [0u8; 32];
+    write_word_bytes[3] = 0xab;
+    let model = symbolic_model(
+        &mut cx,
+        [
+            ("read_offset".to_string(), offset_value + U256::from(3)),
+            ("write_word".to_string(), U256::from_be_bytes(write_word_bytes)),
+        ],
+    );
+    assert_eq!(loaded.eval_model(&model).unwrap(), U256::from(0xab));
+}
+
+#[test]
+fn memory_load_word_offset_dynamic_word_read_includes_pseudo_concrete_write_past_materialized_size()
+{
+    // The exact regression named by review, relative to the deleted
+    // `load_word_dynamic`: a const-evaluable (but undispatched-as-concrete)
+    // write lands well past `materialized_size`, and a dynamic WORD read
+    // starts 24 bytes before it -- so the write falls at word-local index
+    // 24, not at the read's own start. Byte-by-byte enumeration over a
+    // wrongly-accepted bounded fast path would exclude it entirely.
+    let mut cx = SymCx::new();
+    let mut memory = SymMemory::default();
+
+    let filler = SymExpr::constant(&mut cx, U256::from(0xaa));
+    memory.store_byte(&mut cx, 31, filler); // establishes materialized_size = 32
+
+    // `| 0x80` guarantees the resolved offset is >= 128, so `offset - 24`
+    // below never underflows.
+    let (keccak_masked, _) = undispatched_concrete_offset(&mut cx, 4);
+    let high_bit = SymExpr::constant(&mut cx, U256::from(0x80));
+    let write_offset = SymExpr::binop(&mut cx, SymBinOp::Or, keccak_masked, high_bit);
+    assert!(write_offset.as_const().is_none(), "must not fold to a literal Const at construction");
+    let offset_value = write_offset.eval().expect("offset is fully evaluable with no free vars");
+    assert!(offset_value >= U256::from(0x80));
+
+    let write_byte = SymExpr::constant(&mut cx, U256::from(0xef));
+    memory.store_byte_offset(&mut cx, write_offset, write_byte);
+
+    let read_offset = SymExpr::var(&mut cx, "read_offset");
+    let loaded = memory.load_word_offset(&mut cx, read_offset).unwrap();
+
+    let model =
+        symbolic_model(&mut cx, [("read_offset".to_string(), offset_value - U256::from(24))]);
+    let mut expected_bytes = [0u8; 32];
+    expected_bytes[24] = 0xef;
+    let expected = U256::from_be_bytes(expected_bytes);
+    assert_eq!(loaded.eval_model(&model).unwrap(), expected);
+}
+
 #[test]
 fn memory_store_byte_accepts_symbolic_offsets() {
     let mut cx = SymCx::new();