foundry_evm_symbolic/runtime/
memory.rs

1use super::*;
2use foundry_evm::revm::interpreter::STACK_LIMIT;
3
4#[derive(Clone, Debug, Default)]
5pub(crate) struct SymStack(Vec<SymExpr>);
6
7impl SymStack {
8    pub(crate) fn push(&mut self, value: SymExpr) -> Result<(), SymbolicError> {
9        if self.0.len() >= STACK_LIMIT {
10            return Err(SymbolicError::StackOverflow);
11        }
12        self.0.push(value);
13        Ok(())
14    }
15
16    pub(crate) fn pop(&mut self) -> Result<SymExpr, SymbolicError> {
17        self.0.pop().ok_or(SymbolicError::StackUnderflow)
18    }
19
20    pub(crate) fn peek(&self, index_from_top: usize) -> Result<&SymExpr, SymbolicError> {
21        self.0
22            .get(
23                self.0
24                    .len()
25                    .checked_sub(index_from_top + 1)
26                    .ok_or(SymbolicError::StackUnderflow)?,
27            )
28            .ok_or(SymbolicError::StackUnderflow)
29    }
30
31    pub(crate) fn swap(&mut self, index_from_top: usize) -> Result<(), SymbolicError> {
32        let len = self.0.len();
33        let other = len.checked_sub(index_from_top + 1).ok_or(SymbolicError::StackUnderflow)?;
34        self.0.swap(len - 1, other);
35        Ok(())
36    }
37}
38
39#[derive(Clone, Debug)]
40pub(crate) enum BoundedCopySize {
41    Concrete(usize),
42    Symbolic { size: SymExpr, max_size: usize },
43}
44
45#[derive(Clone, Debug, Default)]
46pub(crate) struct SymMemory {
47    symbolic_writes: Vec<SymbolicMemoryWrite>,
48    materialized_size: usize,
49    logical_size: Option<SymExpr>,
50}
51
52#[derive(Clone, Debug)]
53struct SymbolicMemoryWrite {
54    offset: SymExpr,
55    bytes: SymBytes,
56    /// Proven lower bound for the start of a guarded, non-wrapping write.
57    minimum_offset: usize,
58}
59
60impl SymbolicMemoryWrite {
61    fn concrete_offset(&self) -> Option<usize> {
62        self.offset.eval().and_then(|offset| usize::try_from(offset).ok())
63    }
64
65    fn concrete_byte_index(&self, offset: usize) -> Option<usize> {
66        let write_offset = self.concrete_offset()?;
67        let idx = offset.checked_sub(write_offset)?;
68        (idx < self.bytes.len()).then_some(idx)
69    }
70
71    fn concrete_byte(&self, cx: &mut SymCx, offset: usize) -> Option<SymExpr> {
72        self.concrete_byte_index(offset).map(|idx| self.bytes.byte(cx, idx))
73    }
74}
75
76impl SymMemory {
77    fn saturating_add_word(cx: &mut SymCx, left: SymExpr, right: SymExpr) -> SymExpr {
78        let sum = SymExpr::binop(cx, SymBinOp::Add, left.clone(), right);
79        let overflow = SymBoolExpr::cmp_word_expr(cx, SymCmpOp::Ult, &sum, left);
80        let max = SymExpr::constant(cx, U256::MAX);
81        SymExpr::ite(cx, overflow, max, sum)
82    }
83
84    pub(crate) fn size_after_access_word(cx: &mut SymCx, offset: SymExpr, len: usize) -> SymExpr {
85        let size = SymExpr::constant(cx, U256::from(len));
86        Self::size_after_range_word(cx, offset, size)
87    }
88
89    fn size_after_range_word(cx: &mut SymCx, offset: SymExpr, size: SymExpr) -> SymExpr {
90        let end = Self::saturating_add_word(cx, offset, size.clone());
91        let round = SymExpr::constant(cx, U256::from(31));
92        let rounded = Self::saturating_add_word(cx, end, round);
93        let mask = SymExpr::constant(cx, !U256::from(31));
94        let rounded = SymExpr::binop(cx, SymBinOp::And, rounded, mask);
95        let is_empty = SymBoolExpr::eq_word_const(cx, &size, U256::ZERO);
96        let zero = SymExpr::zero(cx);
97        SymExpr::ite(cx, is_empty, zero, rounded)
98    }
99
100    fn size_after_access(offset: usize, len: usize) -> usize {
101        let Some(end) = offset.checked_add(len) else {
102            return usize::MAX & !31usize;
103        };
104        end.checked_add(31).map(|size| size & !31usize).unwrap_or(usize::MAX & !31usize)
105    }
106
107    fn max_size_word(cx: &mut SymCx, left: SymExpr, right: SymExpr) -> SymExpr {
108        if let (Some(left_value), Some(right_value)) = (left.as_const(), right.as_const()) {
109            return SymExpr::constant(cx, left_value.max(right_value));
110        }
111        if left == right {
112            left
113        } else {
114            let condition = SymBoolExpr::cmp_word_expr(cx, SymCmpOp::Ult, &left, right.clone());
115            SymExpr::ite(cx, condition, right, left)
116        }
117    }
118
119    fn expand_to(&mut self, cx: &mut SymCx, size: SymExpr) {
120        self.logical_size = Some(match self.logical_size.take() {
121            Some(current) => Self::max_size_word(cx, current, size),
122            None => size,
123        });
124    }
125
126    pub(crate) fn store_word(&mut self, cx: &mut SymCx, offset: usize, value: SymExpr) {
127        let bytes = value.into_bytes(cx);
128        self.store_bytes(cx, offset, bytes);
129    }
130
131    pub(crate) fn store_word_offset(
132        &mut self,
133        cx: &mut SymCx,
134        offset: SymExpr,
135        value: SymExpr,
136        minimum_offset: usize,
137    ) {
138        if let Some(offset) = offset.as_const() {
139            if let Ok(offset) = usize::try_from(offset) {
140                self.store_word(cx, offset, value);
141            }
142        } else {
143            let bytes = value.into_bytes(cx);
144            self.store_symbolic_bytes(cx, offset, bytes, minimum_offset);
145        }
146    }
147
148    pub(crate) fn store_byte(&mut self, cx: &mut SymCx, offset: usize, value: SymExpr) {
149        let byte = value.low_byte(cx);
150        let bytes = SymBytes::exprs(cx, vec![byte]);
151        self.store_bytes(cx, offset, bytes);
152    }
153
154    pub(crate) fn store_byte_offset(
155        &mut self,
156        cx: &mut SymCx,
157        offset: SymExpr,
158        value: SymExpr,
159        minimum_offset: usize,
160    ) {
161        if let Some(offset) = offset.as_const() {
162            if let Ok(offset) = usize::try_from(offset) {
163                self.store_byte(cx, offset, value);
164            }
165        } else {
166            let byte = value.low_byte(cx);
167            let bytes = SymBytes::exprs(cx, vec![byte]);
168            self.store_symbolic_bytes(cx, offset, bytes, minimum_offset);
169        }
170    }
171
172    pub(crate) fn store_bytes(&mut self, cx: &mut SymCx, offset: usize, bytes: SymBytes) {
173        if bytes.is_empty() {
174            return;
175        }
176        let size = Self::size_after_access(offset, bytes.len());
177        self.materialized_size = self.materialized_size.max(size);
178        let size = SymExpr::constant(cx, U256::from(size));
179        self.expand_to(cx, size);
180        let minimum_offset = offset;
181        let offset = SymExpr::constant(cx, U256::from(offset));
182        self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes, minimum_offset });
183    }
184
185    fn store_symbolic_bytes(
186        &mut self,
187        cx: &mut SymCx,
188        offset: SymExpr,
189        bytes: SymBytes,
190        minimum_offset: usize,
191    ) {
192        if bytes.is_empty() {
193            return;
194        }
195        let size = Self::size_after_access_word(cx, offset.clone(), bytes.len());
196        self.expand_to(cx, size);
197        self.symbolic_writes.push(SymbolicMemoryWrite { offset, bytes, minimum_offset });
198    }
199
200    fn store_symbolic_sized_bytes(
201        &mut self,
202        cx: &mut SymCx,
203        offset: SymExpr,
204        bytes: SymBytes,
205        access_size: SymExpr,
206    ) {
207        if !bytes.is_empty()
208            && let Some(offset) = offset.eval().and_then(|offset| usize::try_from(offset).ok())
209        {
210            let size = Self::size_after_access(offset, bytes.len());
211            self.materialized_size = self.materialized_size.max(size);
212        }
213        if !bytes.is_empty() {
214            self.symbolic_writes.push(SymbolicMemoryWrite {
215                offset: offset.clone(),
216                bytes,
217                minimum_offset: 0,
218            });
219        }
220        let size = Self::size_after_range_word(cx, offset, access_size);
221        self.expand_to(cx, size);
222    }
223
224    pub(crate) fn store_bytes_offset(&mut self, cx: &mut SymCx, offset: SymExpr, bytes: SymBytes) {
225        if let Some(offset) = offset.as_const() {
226            if let Ok(offset) = usize::try_from(offset) {
227                self.store_bytes(cx, offset, bytes);
228            }
229        } else {
230            self.store_symbolic_bytes(cx, offset, bytes, 0);
231        }
232    }
233
234    pub(crate) fn load_word(
235        &self,
236        cx: &mut SymCx,
237        offset: usize,
238    ) -> Result<SymExpr, SymbolicError> {
239        let offset = SymExpr::constant(cx, U256::from(offset));
240        Ok(self.read_bytes_offset(cx, offset, 32).word_at(cx, 0))
241    }
242
243    pub(crate) fn load_word_offset(
244        &mut self,
245        cx: &mut SymCx,
246        offset: SymExpr,
247    ) -> Result<SymExpr, SymbolicError> {
248        if let Some(offset) = offset.as_const() {
249            let Ok(offset) = usize::try_from(offset) else { return Ok(SymExpr::zero(cx)) };
250            let size = Self::size_after_access(offset, 32);
251            let size = SymExpr::constant(cx, U256::from(size));
252            self.expand_to(cx, size);
253            self.load_word(cx, offset)
254        } else {
255            let size = Self::size_after_access_word(cx, offset.clone(), 32);
256            self.expand_to(cx, size);
257            // Share the byte-read path so symbolic writes are included.
258            Ok(self.read_bytes_offset(cx, offset, 32).word_at(cx, 0))
259        }
260    }
261
262    pub(crate) fn read_concrete(
263        &self,
264        cx: &mut SymCx,
265        offset: usize,
266        size: usize,
267    ) -> Result<Vec<u8>, SymbolicError> {
268        if let Some(bytes) = self.read_stored_bytes(cx, offset, size) {
269            return bytes.concrete_bytes(cx, "symbolic memory read");
270        }
271
272        let mut out = vec![0u8; size];
273        for (idx, byte) in out.iter_mut().enumerate() {
274            if let Some(value) = self.byte(cx, offset + idx).as_const() {
275                *byte = value.to::<u8>();
276            } else {
277                return Err(SymbolicError::Unsupported("symbolic memory read"));
278            }
279        }
280        Ok(out)
281    }
282
283    pub(crate) fn read_byte_exprs(
284        &self,
285        cx: &mut SymCx,
286        offset: usize,
287        size: usize,
288    ) -> Vec<SymExpr> {
289        self.read_bytes(cx, offset, size).materialize(cx)
290    }
291
292    pub(crate) fn read_byte_exprs_offset(
293        &self,
294        cx: &mut SymCx,
295        offset: SymExpr,
296        size: usize,
297    ) -> Vec<SymExpr> {
298        self.read_bytes_offset(cx, offset, size).materialize(cx)
299    }
300
301    pub(crate) fn read_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> SymBytes {
302        let offset = SymExpr::constant(cx, U256::from(offset));
303        self.read_bytes_offset(cx, offset, size)
304    }
305
306    pub(crate) fn read_bytes_offset(
307        &self,
308        cx: &mut SymCx,
309        offset: SymExpr,
310        size: usize,
311    ) -> SymBytes {
312        self.read_bytes_offset_with_bounds(cx, offset, size, 0, None)
313    }
314
315    pub(crate) fn read_bytes_offset_with_bounds(
316        &self,
317        cx: &mut SymCx,
318        offset: SymExpr,
319        size: usize,
320        minimum_offset: usize,
321        maximum_offset: Option<usize>,
322    ) -> SymBytes {
323        if let Some(offset) = offset.as_const() {
324            let Ok(offset) = usize::try_from(offset) else {
325                return SymBytes::concrete(cx, vec![0; size]);
326            };
327            if let Some(bytes) = self.read_stored_bytes(cx, offset, size) {
328                return bytes;
329            }
330            let bytes = (0..size).map(|idx| self.byte(cx, offset + idx)).collect();
331            SymBytes::exprs(cx, bytes)
332        } else {
333            let bytes = (0..size)
334                .map(|idx| {
335                    self.byte_dynamic_with_delta_and_bounds(
336                        cx,
337                        &offset,
338                        idx,
339                        minimum_offset,
340                        maximum_offset,
341                    )
342                })
343                .collect();
344            SymBytes::exprs(cx, bytes)
345        }
346    }
347
348    pub(crate) fn load_word_offset_with_bounds(
349        &self,
350        cx: &mut SymCx,
351        base: &SymExpr,
352        relative_offset: usize,
353        minimum_base: usize,
354        maximum_base: Option<usize>,
355    ) -> SymExpr {
356        let offset = SymExpr::add_const(cx, base.clone(), U256::from(relative_offset));
357        let maximum_offset = maximum_base.and_then(|offset| offset.checked_add(relative_offset));
358        let minimum_offset = if relative_offset == 0 || maximum_offset.is_some() {
359            minimum_base.checked_add(relative_offset).unwrap_or_default()
360        } else {
361            0
362        };
363        self.read_bytes_offset_with_bounds(cx, offset, 32, minimum_offset, maximum_offset)
364            .word_at(cx, 0)
365    }
366
367    fn read_stored_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> Option<SymBytes> {
368        if size == 0 {
369            return Some(SymBytes::empty(cx));
370        }
371        let end = offset.checked_add(size)?;
372
373        let mut unresolved = vec![(offset, end)];
374        let mut pieces = Vec::new();
375
376        for write in self.symbolic_writes.iter().rev() {
377            if unresolved.is_empty() {
378                break;
379            }
380
381            let write_offset = write.concrete_offset()?;
382            let write_end = write_offset.checked_add(write.bytes.len())?;
383
384            if write_end <= offset || end <= write_offset {
385                continue;
386            }
387
388            let mut next_unresolved = Vec::new();
389            for (start, end) in unresolved {
390                let overlap_start = start.max(write_offset);
391                let overlap_end = end.min(write_end);
392
393                if overlap_start >= overlap_end {
394                    next_unresolved.push((start, end));
395                    continue;
396                }
397
398                if start < overlap_start {
399                    next_unresolved.push((start, overlap_start));
400                }
401
402                pieces.push((
403                    overlap_start - offset,
404                    write.bytes.slice_concrete(
405                        cx,
406                        overlap_start - write_offset,
407                        overlap_end - overlap_start,
408                    ),
409                ));
410
411                if overlap_end < end {
412                    next_unresolved.push((overlap_end, end));
413                }
414            }
415            unresolved = next_unresolved;
416        }
417
418        pieces.extend(
419            unresolved
420                .into_iter()
421                .map(|(start, end)| (start - offset, SymBytes::concrete(cx, vec![0; end - start]))),
422        );
423        pieces.sort_by_key(|(offset, _)| *offset);
424
425        Some(SymBytes::concat(cx, pieces.into_iter().map(|(_, bytes)| bytes)))
426    }
427
428    pub(crate) fn read_byte_exprs_symbolic_size(
429        &self,
430        cx: &mut SymCx,
431        offset: SymExpr,
432        size: SymExpr,
433        max_size: usize,
434    ) -> Vec<SymExpr> {
435        self.read_bytes_symbolic_size(cx, offset, size, max_size).materialize(cx)
436    }
437
438    pub(crate) fn read_bytes_symbolic_size(
439        &self,
440        cx: &mut SymCx,
441        offset: SymExpr,
442        size: SymExpr,
443        max_size: usize,
444    ) -> SymBytes {
445        if let Some(size) = size.eval() {
446            let size = usize::try_from(size).map_or(max_size, |size| size.min(max_size));
447            let bytes = self.read_bytes_offset(cx, offset, size);
448            let padding = SymBytes::concrete(cx, vec![0; max_size - size]);
449            return SymBytes::concat(cx, [bytes, padding]);
450        }
451
452        let bytes = self.read_bytes_offset(cx, offset, max_size);
453        SymBytes::sized(cx, bytes, size, max_size)
454    }
455
456    pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
457        let mut writes = self.symbolic_writes.as_slice();
458        let mut result = if let Some(base_idx) =
459            writes.iter().rposition(|write| write.concrete_byte_index(offset).is_some())
460        {
461            let write = &writes[base_idx];
462            let byte = write.concrete_byte(cx, offset).expect("concrete byte index is present");
463            writes = &writes[base_idx + 1..];
464            byte
465        } else {
466            SymExpr::zero(cx)
467        };
468
469        for write in writes {
470            if let Some(byte) = write.concrete_byte(cx, offset) {
471                result = byte;
472                continue;
473            }
474            if write.concrete_offset().is_some() {
475                continue;
476            }
477            if write.minimum_offset > offset {
478                continue;
479            }
480            for idx in 0..write.bytes.len() {
481                let write_offset = SymExpr::add_const(cx, write.offset.clone(), U256::from(idx));
482                let offset = SymExpr::constant(cx, U256::from(offset));
483                let condition = SymBoolExpr::eq(cx, write_offset, offset);
484                let byte = write.bytes.byte(cx, idx);
485                result = SymExpr::ite(cx, condition, byte, result);
486            }
487        }
488        result
489    }
490
491    /// Reads the byte at `offset + delta`.
492    ///
493    /// Symbolic stores need not extend `materialized_size`, even when their offsets
494    /// are const-evaluable. Enumerate that region only if it contains every write;
495    /// otherwise fold all writes in insertion order so later writes win.
496    pub(crate) fn byte_dynamic_with_delta(
497        &self,
498        cx: &mut SymCx,
499        offset: &SymExpr,
500        delta: usize,
501    ) -> SymExpr {
502        self.byte_dynamic_with_delta_and_bounds(cx, offset, delta, 0, None)
503    }
504
505    fn byte_dynamic_with_delta_and_bounds(
506        &self,
507        cx: &mut SymCx,
508        offset: &SymExpr,
509        delta: usize,
510        minimum_offset: usize,
511        maximum_offset: Option<usize>,
512    ) -> SymExpr {
513        let materialized_size = self.materialized_size;
514        let all_writes_bounded = self.symbolic_writes.iter().all(|write| {
515            write
516                .concrete_offset()
517                .and_then(|write_offset| write_offset.checked_add(write.bytes.len()))
518                .is_some_and(|end| end <= materialized_size)
519        });
520        let maximum_target = maximum_offset.and_then(|offset| offset.checked_add(delta));
521        let target_non_wrapping = delta == 0 || maximum_target.is_some();
522
523        if all_writes_bounded && target_non_wrapping {
524            let mut result = SymExpr::zero(cx);
525            for candidate in (delta..self.materialized_size).rev() {
526                let candidate_expr = SymExpr::constant(cx, U256::from(candidate - delta));
527                let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
528                let byte = self.byte(cx, candidate);
529                result = SymExpr::ite(cx, condition, byte, result);
530            }
531            return result;
532        }
533
534        let target = SymExpr::add_const(cx, offset.clone(), U256::from(delta));
535        let minimum_target = if target_non_wrapping {
536            minimum_offset.checked_add(delta).unwrap_or_default()
537        } else {
538            0
539        };
540        let gas_dependent_offset = offset.contains_gasleft();
541        let mut result = SymExpr::zero(cx);
542        for write in &self.symbolic_writes {
543            if write
544                .concrete_offset()
545                .and_then(|offset| offset.checked_add(write.bytes.len()))
546                .is_some_and(|end| end <= minimum_target)
547                || maximum_target.is_some_and(|target| write.minimum_offset > target)
548            {
549                continue;
550            }
551            if !gas_dependent_offset
552                && !write.offset.contains_gasleft()
553                && let Some(index) = target.constant_difference(&write.offset)
554            {
555                if let Ok(index) = usize::try_from(index)
556                    && index < write.bytes.len()
557                {
558                    result = write.bytes.byte(cx, index);
559                }
560                continue;
561            }
562            for idx in 0..write.bytes.len() {
563                let write_offset = SymExpr::add_const(cx, write.offset.clone(), U256::from(idx));
564                let condition = SymBoolExpr::eq(cx, write_offset, target.clone());
565                let byte = write.bytes.byte(cx, idx);
566                result = SymExpr::ite(cx, condition, byte, result);
567            }
568        }
569        result
570    }
571
572    pub(crate) fn size_word(&self, cx: &mut SymCx) -> SymExpr {
573        self.logical_size.clone().unwrap_or_else(|| SymExpr::zero(cx))
574    }
575
576    pub(crate) fn size_after_range_expansion_word(
577        &self,
578        cx: &mut SymCx,
579        offset: SymExpr,
580        size: SymExpr,
581    ) -> SymExpr {
582        let current = self.size_word(cx);
583        let expanded = Self::size_after_range_word(cx, offset, size);
584        Self::max_size_word(cx, current, expanded)
585    }
586
587    pub(crate) fn expand_range(&mut self, cx: &mut SymCx, offset: SymExpr, size: SymExpr) {
588        if let (Some(offset), Some(size)) = (offset.as_const(), size.as_const())
589            && let (Ok(offset), Ok(size)) = (usize::try_from(offset), usize::try_from(size))
590        {
591            if size != 0 {
592                let size = Self::size_after_access(offset, size);
593                let size = SymExpr::constant(cx, U256::from(size));
594                self.expand_to(cx, size);
595            }
596            return;
597        }
598        let size = Self::size_after_range_word(cx, offset, size);
599        self.expand_to(cx, size);
600    }
601
602    pub(crate) fn copy_bytes_size_offset(
603        &mut self,
604        cx: &mut SymCx,
605        dest: SymExpr,
606        size: SymExpr,
607        src: SymBytes,
608    ) -> Result<(), SymbolicError> {
609        if src.is_empty() {
610            return Ok(());
611        }
612        if let Some(size) = size.eval() {
613            let size = usize::try_from(size).map_or(src.len(), |size| size.min(src.len()));
614            if size != 0 {
615                let src = src.slice_concrete(cx, 0, size);
616                self.store_bytes_offset(cx, dest, src);
617            }
618            return Ok(());
619        }
620
621        if let Some(dest) = dest.as_const() {
622            if let Ok(dest) = usize::try_from(dest) {
623                let bytes = (0..src.len())
624                    .map(|idx| {
625                        let source = src.byte(cx, idx);
626                        self.copy_size_byte_at(cx, dest + idx, idx, &size, source)
627                    })
628                    .collect::<Vec<_>>();
629                let bytes = SymBytes::exprs(cx, bytes);
630                let dest = SymExpr::constant(cx, U256::from(dest));
631                self.store_symbolic_sized_bytes(cx, dest, bytes, size);
632            }
633        } else {
634            let bytes = (0..src.len())
635                .map(|idx| {
636                    let existing = self.byte_dynamic_with_delta(cx, &dest, idx);
637                    let source = src.byte(cx, idx);
638                    Self::copy_size_byte(cx, idx, &size, source, existing)
639                })
640                .collect();
641            let bytes = SymBytes::exprs(cx, bytes);
642            self.store_symbolic_sized_bytes(cx, dest, bytes, size);
643        }
644        Ok(())
645    }
646
647    pub(crate) fn copy_calldata_to_offset(
648        &mut self,
649        cx: &mut SymCx,
650        dest: SymExpr,
651        offset: SymExpr,
652        size: usize,
653        calldata: &SymCalldata,
654    ) {
655        let bytes = if offset.as_const().is_some_and(|offset| usize::try_from(offset).is_err()) {
656            SymBytes::concrete(cx, vec![0; size])
657        } else {
658            calldata.read_bytes_offset(cx, offset, size)
659        };
660        self.store_bytes_offset(cx, dest, bytes);
661    }
662
663    pub(crate) fn copy_calldata_symbolic_size(
664        &mut self,
665        cx: &mut SymCx,
666        dest: SymExpr,
667        offset: SymExpr,
668        size: SymExpr,
669        max_size: usize,
670        calldata: &SymCalldata,
671    ) -> Result<(), SymbolicError> {
672        let bytes = calldata.read_bytes_offset(cx, offset, max_size);
673        self.copy_bytes_size_offset(cx, dest, size, bytes)
674    }
675
676    fn copy_size_byte_at(
677        &self,
678        cx: &mut SymCx,
679        dest: usize,
680        idx: usize,
681        size: &SymExpr,
682        source: SymExpr,
683    ) -> SymExpr {
684        let existing = self.byte(cx, dest);
685        Self::copy_size_byte(cx, idx, size, source, existing)
686    }
687
688    fn copy_size_byte(
689        cx: &mut SymCx,
690        idx: usize,
691        size: &SymExpr,
692        source: SymExpr,
693        existing: SymExpr,
694    ) -> SymExpr {
695        let idx = SymExpr::constant(cx, U256::from(idx));
696        let condition = SymBoolExpr::cmp(cx, SymCmpOp::Ult, idx, size.clone());
697        SymExpr::ite(cx, condition, source, existing)
698    }
699
700    pub(crate) fn copy_return_data_to_offset(
701        &mut self,
702        cx: &mut SymCx,
703        dest: SymExpr,
704        offset: SymExpr,
705        size: usize,
706        return_data: &SymReturnData,
707    ) -> Result<(), SymbolicError> {
708        if size == 0 {
709            return Ok(());
710        }
711        if let Some(offset) = offset.as_const() {
712            let Ok(offset) = usize::try_from(offset) else {
713                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
714            };
715            if offset.saturating_add(size) > return_data.len() {
716                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
717            }
718        }
719        let bytes = return_data.read_bytes_offset(cx, offset, size);
720        self.store_bytes_offset(cx, dest, bytes);
721        Ok(())
722    }
723
724    pub(crate) fn copy_return_data_symbolic_size(
725        &mut self,
726        cx: &mut SymCx,
727        dest: SymExpr,
728        offset: SymExpr,
729        size: SymExpr,
730        max_size: usize,
731        return_data: &SymReturnData,
732    ) -> Result<(), SymbolicError> {
733        if max_size == 0 {
734            return Ok(());
735        }
736        if let Some(offset) = offset.as_const() {
737            let Ok(offset) = usize::try_from(offset) else {
738                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
739            };
740            if offset.saturating_add(max_size) > return_data.len() {
741                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
742            }
743        }
744        let bytes = return_data.read_bytes_offset(cx, offset, max_size);
745        self.copy_bytes_size_offset(cx, dest, size, bytes)
746    }
747
748    pub(crate) fn copy_call_output_offset(
749        &mut self,
750        cx: &mut SymCx,
751        dest: SymExpr,
752        size: &BoundedCopySize,
753        return_data: &SymReturnData,
754    ) -> Result<(), SymbolicError> {
755        match size {
756            BoundedCopySize::Concrete(size) => {
757                if *size != 0 {
758                    let copy_size = (*size).min(return_data.len());
759                    let bytes = if return_data.len_word.as_const().is_none() {
760                        let bytes = (0..copy_size)
761                            .map(|idx| self.call_output_byte(cx, &dest, idx, None, return_data))
762                            .collect::<Vec<_>>();
763                        SymBytes::exprs(cx, bytes)
764                    } else {
765                        let offset = SymExpr::zero(cx);
766                        return_data.read_bytes_offset(cx, offset, copy_size)
767                    };
768                    let size = SymExpr::constant(cx, U256::from(*size));
769                    self.store_symbolic_sized_bytes(cx, dest, bytes, size);
770                }
771            }
772            BoundedCopySize::Symbolic { size, max_size } => {
773                let output_size = size.clone();
774                if *max_size != 0 {
775                    let copy_size = (*max_size).min(return_data.len());
776                    let bytes = (0..copy_size)
777                        .map(|idx| {
778                            self.call_output_byte(cx, &dest, idx, Some(&output_size), return_data)
779                        })
780                        .collect::<Vec<_>>();
781                    let bytes = SymBytes::exprs(cx, bytes);
782                    self.store_symbolic_sized_bytes(cx, dest, bytes, output_size);
783                }
784            }
785        }
786        Ok(())
787    }
788
789    pub(crate) fn call_output_byte(
790        &self,
791        cx: &mut SymCx,
792        dest: &SymExpr,
793        idx: usize,
794        output_size: Option<&SymExpr>,
795        return_data: &SymReturnData,
796    ) -> SymExpr {
797        let mut guards = Vec::new();
798        if let Some(output_size) = output_size {
799            let idx_expr = SymExpr::constant(cx, U256::from(idx));
800            guards.push(SymBoolExpr::cmp(cx, SymCmpOp::Ult, idx_expr, output_size.clone()));
801        }
802        if return_data.len_word.as_const().is_none() {
803            let idx_expr = SymExpr::constant(cx, U256::from(idx));
804            guards.push(SymBoolExpr::cmp(
805                cx,
806                SymCmpOp::Ult,
807                idx_expr,
808                return_data.len_word.clone(),
809            ));
810        }
811        let guard = SymBoolExpr::and(cx, guards);
812        match guard.as_const() {
813            Some(true) => return_data.byte(cx, idx),
814            Some(false) => self.call_output_existing_byte(cx, dest, idx),
815            None => {
816                let byte = return_data.byte(cx, idx);
817                let existing = self.call_output_existing_byte(cx, dest, idx);
818                SymExpr::ite(cx, guard, byte, existing)
819            }
820        }
821    }
822
823    pub(crate) fn call_output_existing_byte(
824        &self,
825        cx: &mut SymCx,
826        dest: &SymExpr,
827        idx: usize,
828    ) -> SymExpr {
829        if let Some(dest) = dest.as_const() {
830            match usize::try_from(dest) {
831                Ok(dest) => self.byte(cx, dest + idx),
832                Err(_) => SymExpr::zero(cx),
833            }
834        } else {
835            self.byte_dynamic_with_delta(cx, dest, idx)
836        }
837    }
838
839    pub(crate) fn copy_memory_to_offset(
840        &mut self,
841        cx: &mut SymCx,
842        dest: SymExpr,
843        src: SymExpr,
844        size: usize,
845    ) -> Result<(), SymbolicError> {
846        if size == 0 {
847            return Ok(());
848        }
849        let bytes = self.read_bytes_offset(cx, src, size);
850        self.store_bytes_offset(cx, dest, bytes);
851        Ok(())
852    }
853
854    pub(crate) fn copy_memory_symbolic_size(
855        &mut self,
856        cx: &mut SymCx,
857        dest: SymExpr,
858        src: SymExpr,
859        size: SymExpr,
860        max_size: usize,
861    ) -> Result<(), SymbolicError> {
862        if max_size == 0 {
863            return Ok(());
864        }
865        let source = self.read_bytes_offset(cx, src, max_size);
866        self.copy_bytes_size_offset(cx, dest, size, source)
867    }
868
869    pub(crate) fn return_data(
870        &self,
871        cx: &mut SymCx,
872        offset: SymExpr,
873        size: usize,
874    ) -> Result<SymReturnData, SymbolicError> {
875        let bytes = self.read_bytes_offset(cx, offset, size);
876        Ok(SymReturnData::from_bytes(cx, bytes))
877    }
878
879    pub(crate) fn return_data_symbolic_size(
880        &self,
881        cx: &mut SymCx,
882        offset: SymExpr,
883        size: SymExpr,
884        max_size: usize,
885    ) -> Result<SymReturnData, SymbolicError> {
886        Ok(SymReturnData {
887            bytes: self.read_bytes_symbolic_size(cx, offset, size.clone(), max_size),
888            len_word: size,
889        })
890    }
891}
892
893#[derive(Clone, Debug, PartialEq, Eq)]
894pub(crate) struct SymCode {
895    bytes: SymBytes,
896    jump_table: JumpTable,
897}
898
899#[derive(Clone, Debug, PartialEq, Eq)]
900pub(crate) enum GuardedOpcode {
901    End,
902    Concrete(u8),
903    SymbolicSize { condition: SymBoolExpr, opcode: u8 },
904}
905
906impl SymCode {
907    pub(crate) fn empty(cx: &mut SymCx) -> Self {
908        Self { bytes: SymBytes::empty(cx), jump_table: JumpTable::default() }
909    }
910
911    pub(crate) fn from_byte_exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
912        let bytes = SymBytes::exprs(cx, bytes);
913        Self::from_bytes(cx, bytes)
914    }
915
916    pub(crate) fn from_bytes(cx: &mut SymCx, bytes: SymBytes) -> Self {
917        let analysis = if let Some(bytes) = bytes.as_concrete_slice() {
918            bytes.to_vec()
919        } else {
920            (0..bytes.len())
921                .map(|idx| {
922                    bytes.byte(cx, idx).as_const().map_or(opcode::STOP, |value| value.to::<u8>())
923                })
924                .collect::<Vec<_>>()
925        };
926        let analyzed = Bytecode::new_legacy(Bytes::from(analysis));
927        let jump_table = analyzed.legacy_jump_table().cloned().unwrap_or_default();
928        Self { bytes, jump_table }
929    }
930
931    pub(crate) fn concrete(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
932        Self::from_bytecode(cx, &Bytecode::new_legacy(Bytes::from(bytes)))
933    }
934
935    pub(crate) fn from_bytecode(cx: &mut SymCx, bytecode: &Bytecode) -> Self {
936        let bytes = SymBytes::concrete(cx, bytecode.original_byte_slice().to_vec());
937        let jump_table = bytecode.legacy_jump_table().cloned().unwrap_or_default();
938        Self { bytes, jump_table }
939    }
940
941    pub(crate) fn from_memory_offset(
942        cx: &mut SymCx,
943        memory: &SymMemory,
944        offset: SymExpr,
945        size: usize,
946    ) -> Self {
947        let bytes = memory.read_bytes_offset(cx, offset, size);
948        Self::from_bytes(cx, bytes)
949    }
950
951    pub(crate) fn from_memory_symbolic_size(
952        cx: &mut SymCx,
953        memory: &SymMemory,
954        offset: SymExpr,
955        size: SymExpr,
956        max_size: usize,
957    ) -> Self {
958        let bytes = memory.read_bytes_symbolic_size(cx, offset, size, max_size);
959        Self::from_bytes(cx, bytes)
960    }
961
962    pub(crate) fn len(&self) -> usize {
963        self.bytes.len()
964    }
965
966    pub(crate) fn is_empty(&self) -> bool {
967        self.bytes.is_empty()
968    }
969
970    pub(crate) const fn jump_table(&self) -> &JumpTable {
971        &self.jump_table
972    }
973
974    pub(crate) fn opcode(&self, cx: &mut SymCx, pc: usize) -> Result<Option<u8>, SymbolicError> {
975        if pc >= self.len() {
976            return Ok(None);
977        }
978        match self.bytes.byte(cx, pc).as_const() {
979            Some(value) => Ok(Some(value.to::<u8>())),
980            None => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
981        }
982    }
983
984    pub(crate) fn guarded_opcode(
985        &self,
986        cx: &mut SymCx,
987        pc: usize,
988    ) -> Result<GuardedOpcode, SymbolicError> {
989        if pc >= self.len() {
990            return Ok(GuardedOpcode::End);
991        }
992        let byte = self.bytes.byte(cx, pc);
993        match byte.as_const() {
994            Some(value) => Ok(GuardedOpcode::Concrete(value.to::<u8>())),
995            None => {
996                if let SymExprKind::Ite(condition, then_expr, else_expr) = byte.kind()
997                    && else_expr.as_const().is_some_and(|value| value.is_zero())
998                {
999                    match then_expr.as_const() {
1000                        Some(value) if value.is_zero() => Ok(GuardedOpcode::Concrete(0)),
1001                        Some(value) => Ok(GuardedOpcode::SymbolicSize {
1002                            condition: condition.clone(),
1003                            opcode: value.to::<u8>(),
1004                        }),
1005                        None => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
1006                    }
1007                } else {
1008                    Err(SymbolicError::Unsupported("symbolic bytecode opcode"))
1009                }
1010            }
1011        }
1012    }
1013
1014    pub(crate) fn concrete_range(
1015        &self,
1016        cx: &mut SymCx,
1017        offset: usize,
1018        size: usize,
1019        reason: &'static str,
1020    ) -> Result<Vec<u8>, SymbolicError> {
1021        if let Some(bytes) = self.bytes.as_concrete_slice() {
1022            let mut out = Vec::with_capacity(size);
1023            let end = offset.saturating_add(size).min(bytes.len());
1024            if offset < end {
1025                out.extend_from_slice(&bytes[offset..end]);
1026            }
1027            out.resize(size, 0);
1028            return Ok(out);
1029        }
1030
1031        let mut out = Vec::with_capacity(size);
1032        for idx in 0..size {
1033            if offset + idx >= self.len() {
1034                out.push(0);
1035                continue;
1036            }
1037            match self.bytes.byte(cx, offset + idx).as_const() {
1038                Some(value) => out.push(value.to::<u8>()),
1039                None => return Err(SymbolicError::Unsupported(reason)),
1040            }
1041        }
1042        Ok(out)
1043    }
1044
1045    pub(crate) fn read_byte_exprs(
1046        &self,
1047        cx: &mut SymCx,
1048        offset: usize,
1049        size: usize,
1050    ) -> Vec<SymExpr> {
1051        self.read_bytes(cx, offset, size).materialize(cx)
1052    }
1053
1054    pub(crate) fn read_byte_exprs_offset(
1055        &self,
1056        cx: &mut SymCx,
1057        offset: SymExpr,
1058        size: usize,
1059    ) -> Vec<SymExpr> {
1060        self.read_bytes_offset(cx, offset, size).materialize(cx)
1061    }
1062
1063    pub(crate) fn read_bytes(&self, cx: &mut SymCx, offset: usize, size: usize) -> SymBytes {
1064        self.bytes.slice_concrete(cx, offset, size)
1065    }
1066
1067    pub(crate) fn read_bytes_offset(
1068        &self,
1069        cx: &mut SymCx,
1070        offset: SymExpr,
1071        size: usize,
1072    ) -> SymBytes {
1073        self.bytes.read_offset(cx, offset, size)
1074    }
1075
1076    pub(crate) fn push_data_word(&self, cx: &mut SymCx, offset: usize, len: usize) -> SymExpr {
1077        self.bytes.right_aligned_word(cx, offset, len)
1078    }
1079
1080    pub(crate) fn concrete_bytes(
1081        &self,
1082        cx: &mut SymCx,
1083        reason: &'static str,
1084    ) -> Result<Vec<u8>, SymbolicError> {
1085        self.concrete_range(cx, 0, self.len(), reason)
1086    }
1087}
1088
1089#[derive(Clone, Debug)]
1090pub(crate) struct SymReturnData {
1091    pub(crate) len_word: SymExpr,
1092    pub(crate) bytes: SymBytes,
1093}
1094
1095impl SymReturnData {
1096    pub(crate) fn empty(cx: &mut SymCx) -> Self {
1097        Self { len_word: SymExpr::zero(cx), bytes: SymBytes::empty(cx) }
1098    }
1099
1100    pub(crate) fn from_words(cx: &mut SymCx, words: Vec<SymExpr>) -> Self {
1101        let bytes = words.into_iter().map(|word| word.into_bytes(cx)).collect::<Vec<_>>();
1102        let bytes = SymBytes::concat(cx, bytes);
1103        Self::from_bytes(cx, bytes)
1104    }
1105
1106    pub(crate) fn from_concrete_bytes(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
1107        let bytes = SymBytes::concrete(cx, bytes);
1108        Self::from_bytes(cx, bytes)
1109    }
1110
1111    pub(crate) fn from_byte_exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
1112        let bytes = SymBytes::exprs(cx, bytes);
1113        Self::from_bytes(cx, bytes)
1114    }
1115
1116    pub(crate) fn from_bytes(cx: &mut SymCx, bytes: SymBytes) -> Self {
1117        let len = bytes.len();
1118        Self { len_word: SymExpr::constant(cx, U256::from(len)), bytes }
1119    }
1120
1121    pub(crate) fn len(&self) -> usize {
1122        self.bytes.len()
1123    }
1124
1125    pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
1126        self.bytes.byte(cx, offset)
1127    }
1128
1129    pub(crate) fn read_bytes_offset(
1130        &self,
1131        cx: &mut SymCx,
1132        offset: SymExpr,
1133        size: usize,
1134    ) -> SymBytes {
1135        self.bytes.read_offset(cx, offset, size)
1136    }
1137
1138    pub(crate) fn read_concrete(
1139        &self,
1140        cx: &mut SymCx,
1141        reason: &'static str,
1142    ) -> Result<Vec<u8>, SymbolicError> {
1143        self.bytes.concrete_bytes(cx, reason)
1144    }
1145
1146    pub(crate) fn to_code(&self, cx: &mut SymCx) -> Result<SymCode, SymbolicError> {
1147        if self.len_word.as_const().is_none() {
1148            return Err(SymbolicError::Unsupported(
1149                "CREATE with symbolic runtime size not modeled",
1150            ));
1151        }
1152        Ok(SymCode::from_bytes(cx, self.bytes.clone()))
1153    }
1154}
foundry_evm_symbolic/runtime/memory.rs

foundry_evm_symbolic/runtime/
memory.rs
