foundry_evm_symbolic/runtime/
memory.rs

1use super::*;
2
3#[derive(Clone, Debug, Default)]
4pub(crate) struct SymStack(Vec<SymWord>);
5
6impl SymStack {
7    /// Implements the `push` symbolic memory helper.
8    pub(crate) fn push(&mut self, value: SymWord) -> Result<(), SymbolicError> {
9        if self.0.len() >= EVM_STACK_LIMIT {
10            return Err(SymbolicError::StackOverflow);
11        }
12        self.0.push(value);
13        Ok(())
14    }
15
16    /// Implements the `pop` symbolic memory helper.
17    pub(crate) fn pop(&mut self) -> Result<SymWord, SymbolicError> {
18        self.0.pop().ok_or(SymbolicError::StackUnderflow)
19    }
20
21    /// Implements the `peek` symbolic memory helper.
22    pub(crate) fn peek(&self, index_from_top: usize) -> Result<&SymWord, SymbolicError> {
23        self.0
24            .get(
25                self.0
26                    .len()
27                    .checked_sub(index_from_top + 1)
28                    .ok_or(SymbolicError::StackUnderflow)?,
29            )
30            .ok_or(SymbolicError::StackUnderflow)
31    }
32
33    /// Implements the `swap` symbolic memory helper.
34    pub(crate) fn swap(&mut self, index_from_top: usize) -> Result<(), SymbolicError> {
35        let len = self.0.len();
36        let other = len.checked_sub(index_from_top + 1).ok_or(SymbolicError::StackUnderflow)?;
37        self.0.swap(len - 1, other);
38        Ok(())
39    }
40}
41
42#[derive(Clone, Debug)]
43pub(crate) enum BoundedCopySize {
44    Concrete(usize),
45    Symbolic { size: SymWord, max_size: usize },
46}
47
48#[derive(Clone, Debug, Default)]
49pub(crate) struct SymMemory {
50    pub(crate) bytes: BTreeMap<usize, SymWord>,
51    pub(crate) byte_epochs: BTreeMap<usize, u64>,
52    pub(crate) symbolic_writes: Vec<SymbolicMemoryWrite>,
53    pub(crate) epoch: u64,
54    pub(crate) size: usize,
55}
56
57#[derive(Clone, Debug)]
58pub(crate) struct SymbolicMemoryWrite {
59    pub(crate) epoch: u64,
60    pub(crate) offset: Expr,
61    pub(crate) bytes: Vec<SymWord>,
62}
63
64/// Returns the `memory_size_after_access` symbolic memory helper result.
65pub(crate) fn memory_size_after_access(offset: usize, len: usize) -> usize {
66    let Some(end) = offset.checked_add(len) else {
67        return usize::MAX & !31usize;
68    };
69    end.checked_add(31).map(|size| size & !31usize).unwrap_or(usize::MAX & !31usize)
70}
71
72/// Returns the `memory_size_after_symbolic_access` symbolic memory helper result.
73pub(crate) fn memory_size_after_symbolic_access(offset: Expr, len: U256) -> Expr {
74    let end = Expr::op(ExprOp::Add, offset, Expr::Const(len));
75    Expr::op(
76        ExprOp::And,
77        Expr::op(ExprOp::Add, end, Expr::Const(U256::from(31))),
78        Expr::Const(!U256::from(31)),
79    )
80}
81
82/// Implements the `max_u256_expr` symbolic memory helper.
83pub(crate) fn max_u256_expr(left: Expr, right: Expr) -> Expr {
84    match (&left, &right) {
85        (Expr::Const(left), Expr::Const(right)) => Expr::Const((*left).max(*right)),
86        _ if left == right => left,
87        _ => Expr::Ite(
88            Box::new(BoolExpr::cmp(BoolExprOp::Ult, left.clone(), right.clone())),
89            Box::new(right),
90            Box::new(left),
91        ),
92    }
93}
94
95impl SymMemory {
96    /// Applies the `store_word` symbolic memory helper.
97    pub(crate) fn store_word(&mut self, offset: usize, value: SymWord) {
98        self.store_bytes(offset, word_bytes(value));
99    }
100
101    /// Applies the `store_word_offset` symbolic memory helper.
102    pub(crate) fn store_word_offset(&mut self, offset: SymWord, value: SymWord) {
103        match offset {
104            SymWord::Concrete(offset) if offset <= U256::from(usize::MAX) => {
105                self.store_word(offset.to::<usize>(), value);
106            }
107            SymWord::Concrete(_) => {}
108            SymWord::Expr(offset) => self.store_symbolic_bytes(offset, word_bytes(value)),
109        }
110    }
111
112    /// Applies the `store_byte` symbolic memory helper.
113    pub(crate) fn store_byte(&mut self, offset: usize, value: SymWord) {
114        self.store_bytes(offset, vec![low_byte(value)]);
115    }
116
117    /// Applies the `store_byte_offset` symbolic memory helper.
118    pub(crate) fn store_byte_offset(&mut self, offset: SymWord, value: SymWord) {
119        match offset {
120            SymWord::Concrete(offset) if offset <= U256::from(usize::MAX) => {
121                self.store_byte(offset.to::<usize>(), value);
122            }
123            SymWord::Concrete(_) => {}
124            SymWord::Expr(offset) => self.store_symbolic_bytes(offset, vec![low_byte(value)]),
125        }
126    }
127
128    /// Applies the `store_bytes` symbolic memory helper.
129    pub(crate) fn store_bytes(&mut self, offset: usize, bytes: Vec<SymWord>) {
130        if bytes.is_empty() {
131            return;
132        }
133        self.epoch = self.epoch.saturating_add(1);
134        self.size = self.size.max(memory_size_after_access(offset, bytes.len()));
135        for (idx, byte) in bytes.into_iter().enumerate() {
136            let offset = offset + idx;
137            self.bytes.insert(offset, byte);
138            self.byte_epochs.insert(offset, self.epoch);
139        }
140    }
141
142    /// Applies the `store_symbolic_bytes` symbolic memory helper.
143    pub(crate) fn store_symbolic_bytes(&mut self, offset: Expr, bytes: Vec<SymWord>) {
144        if bytes.is_empty() {
145            return;
146        }
147        self.epoch = self.epoch.saturating_add(1);
148        self.symbolic_writes.push(SymbolicMemoryWrite { epoch: self.epoch, offset, bytes });
149    }
150
151    /// Applies the `store_bytes_offset` symbolic memory helper.
152    pub(crate) fn store_bytes_offset(&mut self, offset: SymWord, bytes: Vec<SymWord>) {
153        match offset {
154            SymWord::Concrete(offset) if offset <= U256::from(usize::MAX) => {
155                self.store_bytes(offset.to::<usize>(), bytes);
156            }
157            SymWord::Concrete(_) => {}
158            SymWord::Expr(offset) => self.store_symbolic_bytes(offset, bytes),
159        }
160    }
161
162    /// Returns the `load_word` symbolic memory helper result.
163    pub(crate) fn load_word(&self, offset: usize) -> Result<SymWord, SymbolicError> {
164        Ok(word_from_bytes((0..32).map(|idx| self.byte(offset + idx))))
165    }
166
167    /// Returns the `load_word_offset` symbolic memory helper result.
168    pub(crate) fn load_word_offset(&self, offset: SymWord) -> Result<SymWord, SymbolicError> {
169        match offset {
170            SymWord::Concrete(offset) => {
171                if offset > U256::from(usize::MAX) {
172                    return Ok(SymWord::zero());
173                }
174                self.load_word(offset.to::<usize>())
175            }
176            SymWord::Expr(offset) => {
177                Ok(word_from_bytes(self.read_bytes_offset(SymWord::Expr(offset), 32)))
178            }
179        }
180    }
181
182    /// Returns the `read_concrete` symbolic memory helper result.
183    pub(crate) fn read_concrete(
184        &self,
185        offset: usize,
186        size: usize,
187    ) -> Result<Vec<u8>, SymbolicError> {
188        let mut out = vec![0u8; size];
189        for (idx, byte) in out.iter_mut().enumerate() {
190            match self.byte(offset + idx) {
191                SymWord::Concrete(value) => *byte = value.to::<u8>(),
192                SymWord::Expr(_) => {
193                    return Err(SymbolicError::Unsupported("symbolic memory read"));
194                }
195            }
196        }
197        Ok(out)
198    }
199
200    /// Returns the `read_bytes` symbolic memory helper result.
201    pub(crate) fn read_bytes(&self, offset: usize, size: usize) -> Vec<SymWord> {
202        (0..size).map(|idx| self.byte(offset + idx)).collect()
203    }
204
205    /// Returns the `read_bytes_offset` symbolic memory helper result.
206    pub(crate) fn read_bytes_offset(&self, offset: SymWord, size: usize) -> Vec<SymWord> {
207        match offset {
208            SymWord::Concrete(offset) => {
209                if offset > U256::from(usize::MAX) {
210                    return vec![SymWord::zero(); size];
211                }
212                self.read_bytes(offset.to::<usize>(), size)
213            }
214            SymWord::Expr(offset) => {
215                (0..size).map(|idx| self.byte_dynamic_with_delta(offset.clone(), idx)).collect()
216            }
217        }
218    }
219
220    /// Returns the `read_bytes_symbolic_size` symbolic memory helper result.
221    pub(crate) fn read_bytes_symbolic_size(
222        &self,
223        offset: SymWord,
224        size: SymWord,
225        max_size: usize,
226    ) -> Vec<SymWord> {
227        let size = size.into_expr();
228        self.read_bytes_offset(offset, max_size)
229            .into_iter()
230            .enumerate()
231            .map(|(idx, source)| {
232                SymWord::Expr(Expr::Ite(
233                    Box::new(BoolExpr::cmp(
234                        BoolExprOp::Ult,
235                        Expr::Const(U256::from(idx)),
236                        size.clone(),
237                    )),
238                    Box::new(source.into_expr()),
239                    Box::new(Expr::Const(U256::ZERO)),
240                ))
241            })
242            .collect()
243    }
244
245    /// Implements the `byte` symbolic memory helper.
246    pub(crate) fn byte(&self, offset: usize) -> SymWord {
247        let (base, base_epoch) = self.base_byte(offset);
248        let mut result = base.clone().into_expr();
249        let mut has_symbolic_match = false;
250        for write in self.symbolic_writes.iter().filter(|write| write.epoch > base_epoch) {
251            for (idx, byte) in write.bytes.iter().enumerate() {
252                has_symbolic_match = true;
253                result = Expr::Ite(
254                    Box::new(BoolExpr::eq(
255                        Expr::op(ExprOp::Add, write.offset.clone(), Expr::Const(U256::from(idx))),
256                        Expr::Const(U256::from(offset)),
257                    )),
258                    Box::new(byte.clone().into_expr()),
259                    Box::new(result),
260                );
261            }
262        }
263        if has_symbolic_match { SymWord::Expr(result) } else { base }
264    }
265
266    /// Implements the `base_byte` symbolic memory helper.
267    pub(crate) fn base_byte(&self, offset: usize) -> (SymWord, u64) {
268        (
269            self.bytes.get(&offset).cloned().unwrap_or_else(SymWord::zero),
270            self.byte_epochs.get(&offset).copied().unwrap_or_default(),
271        )
272    }
273
274    /// Returns the `byte_dynamic_with_delta` symbolic memory helper result.
275    pub(crate) fn byte_dynamic_with_delta(&self, offset: Expr, delta: usize) -> SymWord {
276        let mut result = Expr::Const(U256::ZERO);
277        for candidate in (delta..self.size).rev() {
278            let (byte, base_epoch) = self.base_byte(candidate);
279            let mut candidate_result = byte.into_expr();
280            for write in self.symbolic_writes.iter().filter(|write| write.epoch > base_epoch) {
281                for (idx, byte) in write.bytes.iter().enumerate() {
282                    candidate_result = Expr::Ite(
283                        Box::new(BoolExpr::eq(
284                            Expr::op(
285                                ExprOp::Add,
286                                write.offset.clone(),
287                                Expr::Const(U256::from(idx)),
288                            ),
289                            Expr::Const(U256::from(candidate)),
290                        )),
291                        Box::new(byte.clone().into_expr()),
292                        Box::new(candidate_result),
293                    );
294                }
295            }
296            result = Expr::Ite(
297                Box::new(BoolExpr::eq(offset.clone(), Expr::Const(U256::from(candidate - delta)))),
298                Box::new(candidate_result),
299                Box::new(result),
300            );
301        }
302        SymWord::Expr(result)
303    }
304
305    /// Implements the `size_word` symbolic memory helper.
306    pub(crate) fn size_word(&self) -> SymWord {
307        let mut size = Expr::Const(U256::from(self.size));
308        for write in &self.symbolic_writes {
309            let write_size = memory_size_after_symbolic_access(
310                write.offset.clone(),
311                U256::from(write.bytes.len()),
312            );
313            size = max_u256_expr(size, write_size);
314        }
315        match size {
316            Expr::Const(value) => SymWord::Concrete(value),
317            size => SymWord::Expr(size),
318        }
319    }
320
321    #[cfg(test)]
322    /// Applies the `copy_symbolic` symbolic memory helper.
323    pub(crate) fn copy_symbolic(&mut self, dest: usize, src: Vec<SymWord>) {
324        self.store_bytes(dest, src);
325    }
326
327    /// Applies the `copy_symbolic_offset` symbolic memory helper.
328    pub(crate) fn copy_symbolic_offset(&mut self, dest: SymWord, src: Vec<SymWord>) {
329        self.store_bytes_offset(dest, src);
330    }
331
332    #[cfg(test)]
333    /// Applies the `copy_symbolic_size` symbolic memory helper.
334    pub(crate) fn copy_symbolic_size(&mut self, dest: usize, size: SymWord, src: Vec<SymWord>) {
335        self.copy_symbolic_size_offset(SymWord::Concrete(U256::from(dest)), size, src)
336            .expect("concrete symbolic-size memory copy cannot fail");
337    }
338
339    /// Applies the `copy_symbolic_size_offset` symbolic memory helper.
340    pub(crate) fn copy_symbolic_size_offset(
341        &mut self,
342        dest: SymWord,
343        size: SymWord,
344        src: Vec<SymWord>,
345    ) -> Result<(), SymbolicError> {
346        if src.is_empty() {
347            return Ok(());
348        }
349        let size = size.into_expr();
350        match dest {
351            SymWord::Concrete(dest) if dest <= U256::from(usize::MAX) => {
352                let dest = dest.to::<usize>();
353                let bytes = src
354                    .into_iter()
355                    .enumerate()
356                    .map(|(idx, source)| {
357                        self.symbolic_copy_size_byte(dest + idx, idx, &size, source)
358                    })
359                    .collect();
360                self.store_bytes(dest, bytes);
361            }
362            SymWord::Concrete(_) => {}
363            SymWord::Expr(dest) => {
364                let bytes = src
365                    .into_iter()
366                    .enumerate()
367                    .map(|(idx, source)| {
368                        let existing = self.byte_dynamic_with_delta(dest.clone(), idx);
369                        symbolic_copy_size_byte(idx, &size, source, existing)
370                    })
371                    .collect();
372                self.store_symbolic_bytes(dest, bytes);
373            }
374        }
375        Ok(())
376    }
377
378    #[cfg(test)]
379    /// Applies the `copy_calldata` symbolic memory helper.
380    pub(crate) fn copy_calldata(
381        &mut self,
382        dest: usize,
383        offset: usize,
384        size: usize,
385        calldata: &SymCalldata,
386    ) -> Result<(), SymbolicError> {
387        self.store_bytes(dest, (0..size).map(|idx| calldata.byte(offset + idx)).collect());
388        Ok(())
389    }
390
391    #[cfg(test)]
392    /// Applies the `copy_calldata_offset` symbolic memory helper.
393    pub(crate) fn copy_calldata_offset(
394        &mut self,
395        dest: usize,
396        offset: SymWord,
397        size: usize,
398        calldata: &SymCalldata,
399    ) -> Result<(), SymbolicError> {
400        self.copy_calldata_to_offset(SymWord::Concrete(U256::from(dest)), offset, size, calldata)
401    }
402
403    /// Applies the `copy_calldata_to_offset` symbolic memory helper.
404    pub(crate) fn copy_calldata_to_offset(
405        &mut self,
406        dest: SymWord,
407        offset: SymWord,
408        size: usize,
409        calldata: &SymCalldata,
410    ) -> Result<(), SymbolicError> {
411        match offset {
412            SymWord::Concrete(offset) => {
413                if offset > U256::from(usize::MAX) {
414                    self.copy_symbolic_offset(dest, vec![SymWord::zero(); size]);
415                    return Ok(());
416                }
417                self.store_bytes_offset(
418                    dest,
419                    (0..size).map(|idx| calldata.byte(offset.to::<usize>() + idx)).collect(),
420                );
421                Ok(())
422            }
423            SymWord::Expr(offset) => {
424                self.store_bytes_offset(
425                    dest,
426                    (0..size)
427                        .map(|idx| calldata.byte_dynamic_with_delta(offset.clone(), idx))
428                        .collect(),
429                );
430                Ok(())
431            }
432        }
433    }
434
435    /// Applies the `copy_calldata_symbolic_size` symbolic memory helper.
436    pub(crate) fn copy_calldata_symbolic_size(
437        &mut self,
438        dest: SymWord,
439        offset: SymWord,
440        size: SymWord,
441        max_size: usize,
442        calldata: &SymCalldata,
443    ) -> Result<(), SymbolicError> {
444        let bytes = match offset {
445            SymWord::Concrete(offset) => {
446                let offset =
447                    if offset > U256::from(usize::MAX) { None } else { Some(offset.to::<usize>()) };
448                (0..max_size)
449                    .map(|idx| {
450                        offset
451                            .map(|offset| calldata.byte(offset + idx))
452                            .unwrap_or_else(SymWord::zero)
453                    })
454                    .collect()
455            }
456            SymWord::Expr(offset) => (0..max_size)
457                .map(|idx| calldata.byte_dynamic_with_delta(offset.clone(), idx))
458                .collect(),
459        };
460        self.copy_symbolic_size_offset(dest, size, bytes)
461    }
462
463    /// Returns the `symbolic_copy_size_byte` symbolic memory helper result.
464    pub(crate) fn symbolic_copy_size_byte(
465        &self,
466        dest: usize,
467        idx: usize,
468        size: &Expr,
469        source: SymWord,
470    ) -> SymWord {
471        let existing = self.byte(dest);
472        symbolic_copy_size_byte(idx, size, source, existing)
473    }
474
475    /// Applies the `copy_return_data_to_offset` symbolic memory helper.
476    pub(crate) fn copy_return_data_to_offset(
477        &mut self,
478        dest: SymWord,
479        offset: SymWord,
480        size: usize,
481        return_data: &SymReturnData,
482    ) -> Result<(), SymbolicError> {
483        if size == 0 {
484            return Ok(());
485        }
486        if let SymWord::Concrete(offset) = &offset {
487            if *offset > U256::from(usize::MAX) {
488                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
489            }
490            if offset.to::<usize>().saturating_add(size) > return_data.len {
491                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
492            }
493        }
494        self.store_bytes_offset(dest, return_data.read_bytes_offset(offset, size));
495        Ok(())
496    }
497
498    /// Applies the `copy_return_data_symbolic_size` symbolic memory helper.
499    pub(crate) fn copy_return_data_symbolic_size(
500        &mut self,
501        dest: SymWord,
502        offset: SymWord,
503        size: SymWord,
504        max_size: usize,
505        return_data: &SymReturnData,
506    ) -> Result<(), SymbolicError> {
507        if max_size == 0 {
508            return Ok(());
509        }
510        if let SymWord::Concrete(offset) = &offset {
511            if *offset > U256::from(usize::MAX) {
512                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
513            }
514            if offset.to::<usize>().saturating_add(max_size) > return_data.len {
515                return Err(SymbolicError::Unsupported("out-of-bounds symbolic RETURNDATACOPY"));
516            }
517        }
518        let bytes = return_data.read_bytes_offset(offset, max_size);
519        self.copy_symbolic_size_offset(dest, size, bytes)
520    }
521
522    /// Applies the `copy_call_output_offset` symbolic memory helper.
523    pub(crate) fn copy_call_output_offset(
524        &mut self,
525        dest: SymWord,
526        size: &BoundedCopySize,
527        return_data: &SymReturnData,
528    ) -> Result<(), SymbolicError> {
529        match size {
530            BoundedCopySize::Concrete(size) => {
531                let size = (*size).min(return_data.len);
532                if size != 0 {
533                    if return_data.has_symbolic_len() {
534                        let bytes = (0..size)
535                            .map(|idx| self.call_output_byte(&dest, idx, None, return_data))
536                            .collect();
537                        self.store_bytes_offset(dest, bytes);
538                    } else {
539                        self.store_bytes_offset(
540                            dest,
541                            (0..size).map(|idx| return_data.byte(idx)).collect(),
542                        );
543                    }
544                }
545            }
546            BoundedCopySize::Symbolic { size, max_size } => {
547                let output_size = size.clone().into_expr();
548                let max_size = (*max_size).min(return_data.len);
549                if max_size != 0 {
550                    let bytes = (0..max_size)
551                        .map(|idx| {
552                            self.call_output_byte(&dest, idx, Some(&output_size), return_data)
553                        })
554                        .collect();
555                    self.store_bytes_offset(dest, bytes);
556                }
557            }
558        }
559        Ok(())
560    }
561
562    /// Implements the `call_output_byte` symbolic memory helper.
563    pub(crate) fn call_output_byte(
564        &self,
565        dest: &SymWord,
566        idx: usize,
567        output_size: Option<&Expr>,
568        return_data: &SymReturnData,
569    ) -> SymWord {
570        let mut guards = Vec::new();
571        if let Some(output_size) = output_size {
572            guards.push(BoolExpr::cmp(
573                BoolExprOp::Ult,
574                Expr::Const(U256::from(idx)),
575                output_size.clone(),
576            ));
577        }
578        if return_data.has_symbolic_len() {
579            guards.push(BoolExpr::cmp(
580                BoolExprOp::Ult,
581                Expr::Const(U256::from(idx)),
582                return_data.len_expr(),
583            ));
584        }
585        let guard = BoolExpr::and(guards);
586        match guard {
587            BoolExpr::Const(true) => return_data.byte(idx),
588            BoolExpr::Const(false) => self.call_output_existing_byte(dest, idx),
589            guard => SymWord::Expr(Expr::Ite(
590                Box::new(guard),
591                Box::new(return_data.byte(idx).into_expr()),
592                Box::new(self.call_output_existing_byte(dest, idx).into_expr()),
593            )),
594        }
595    }
596
597    /// Implements the `call_output_existing_byte` symbolic memory helper.
598    pub(crate) fn call_output_existing_byte(&self, dest: &SymWord, idx: usize) -> SymWord {
599        match dest {
600            SymWord::Concrete(dest) if *dest <= U256::from(usize::MAX) => {
601                self.byte(dest.to::<usize>() + idx)
602            }
603            SymWord::Concrete(_) => SymWord::zero(),
604            SymWord::Expr(dest) => self.byte_dynamic_with_delta(dest.clone(), idx),
605        }
606    }
607
608    #[cfg(test)]
609    /// Applies the `copy_memory_offset` symbolic memory helper.
610    pub(crate) fn copy_memory_offset(
611        &mut self,
612        dest: usize,
613        src: SymWord,
614        size: usize,
615    ) -> Result<(), SymbolicError> {
616        self.copy_memory_to_offset(SymWord::Concrete(U256::from(dest)), src, size)
617    }
618
619    /// Applies the `copy_memory_to_offset` symbolic memory helper.
620    pub(crate) fn copy_memory_to_offset(
621        &mut self,
622        dest: SymWord,
623        src: SymWord,
624        size: usize,
625    ) -> Result<(), SymbolicError> {
626        if size == 0 {
627            return Ok(());
628        }
629        let bytes = self.read_bytes_offset(src, size);
630        self.store_bytes_offset(dest, bytes);
631        Ok(())
632    }
633
634    /// Applies the `copy_memory_symbolic_size` symbolic memory helper.
635    pub(crate) fn copy_memory_symbolic_size(
636        &mut self,
637        dest: SymWord,
638        src: SymWord,
639        size: SymWord,
640        max_size: usize,
641    ) -> Result<(), SymbolicError> {
642        if max_size == 0 {
643            return Ok(());
644        }
645        let source = self.read_bytes_offset(src, max_size);
646        self.copy_symbolic_size_offset(dest, size, source)
647    }
648
649    /// Implements the `return_data` symbolic memory helper.
650    pub(crate) fn return_data(
651        &self,
652        offset: SymWord,
653        size: usize,
654    ) -> Result<SymReturnData, SymbolicError> {
655        Ok(SymReturnData::from_symbolic_bytes(self.read_bytes_offset(offset, size)))
656    }
657
658    /// Implements the `return_data_symbolic_size` symbolic memory helper.
659    pub(crate) fn return_data_symbolic_size(
660        &self,
661        offset: SymWord,
662        size: SymWord,
663        max_size: usize,
664    ) -> Result<SymReturnData, SymbolicError> {
665        Ok(SymReturnData::from_symbolic_bytes_with_len(
666            self.read_bytes_symbolic_size(offset, size.clone(), max_size),
667            size,
668        ))
669    }
670}
671
672/// Returns the `symbolic_copy_size_byte` symbolic memory helper result.
673pub(crate) fn symbolic_copy_size_byte(
674    idx: usize,
675    size: &Expr,
676    source: SymWord,
677    existing: SymWord,
678) -> SymWord {
679    SymWord::Expr(Expr::Ite(
680        Box::new(BoolExpr::cmp(BoolExprOp::Ult, Expr::Const(U256::from(idx)), size.clone())),
681        Box::new(source.into_expr()),
682        Box::new(existing.into_expr()),
683    ))
684}
685
686#[derive(Clone, Debug, Default, PartialEq, Eq)]
687pub(crate) struct SymCode {
688    pub(crate) bytes: Vec<SymWord>,
689}
690
691#[derive(Clone, Debug, PartialEq, Eq)]
692pub(crate) enum GuardedOpcode {
693    End,
694    Concrete(u8),
695    SymbolicSize { condition: BoolExpr, opcode: u8 },
696}
697
698impl SymCode {
699    /// Implements the `concrete` symbolic memory helper.
700    pub(crate) fn concrete(bytes: Vec<u8>) -> Self {
701        Self { bytes: bytes.into_iter().map(|byte| SymWord::Concrete(U256::from(byte))).collect() }
702    }
703
704    /// Converts values for the `from_memory_offset` symbolic memory helper.
705    pub(crate) fn from_memory_offset(memory: &SymMemory, offset: SymWord, size: usize) -> Self {
706        Self { bytes: memory.read_bytes_offset(offset, size) }
707    }
708
709    /// Converts values for the `from_memory_symbolic_size` symbolic memory helper.
710    pub(crate) fn from_memory_symbolic_size(
711        memory: &SymMemory,
712        offset: SymWord,
713        size: SymWord,
714        max_size: usize,
715    ) -> Self {
716        Self { bytes: memory.read_bytes_symbolic_size(offset, size, max_size) }
717    }
718
719    /// Implements the `len` symbolic memory helper.
720    pub(crate) const fn len(&self) -> usize {
721        self.bytes.len()
722    }
723
724    /// Returns whether `is_empty` holds.
725    pub(crate) const fn is_empty(&self) -> bool {
726        self.bytes.is_empty()
727    }
728
729    /// Implements the `opcode` symbolic memory helper.
730    pub(crate) fn opcode(&self, pc: usize) -> Result<Option<u8>, SymbolicError> {
731        self.bytes
732            .get(pc)
733            .map(|byte| match byte {
734                SymWord::Concrete(value) => Ok(value.to::<u8>()),
735                SymWord::Expr(_) => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
736            })
737            .transpose()
738    }
739
740    /// Implements the `guarded_opcode` symbolic memory helper.
741    pub(crate) fn guarded_opcode(&self, pc: usize) -> Result<GuardedOpcode, SymbolicError> {
742        match self.bytes.get(pc) {
743            None => Ok(GuardedOpcode::End),
744            Some(SymWord::Concrete(value)) => Ok(GuardedOpcode::Concrete(value.to::<u8>())),
745            Some(SymWord::Expr(Expr::Ite(condition, then_expr, else_expr))) if matches!(else_expr.as_ref(), Expr::Const(value) if value.is_zero()) => {
746                match then_expr.as_ref() {
747                    Expr::Const(value) if value.is_zero() => Ok(GuardedOpcode::Concrete(0)),
748                    Expr::Const(value) => Ok(GuardedOpcode::SymbolicSize {
749                        condition: (**condition).clone(),
750                        opcode: value.to::<u8>(),
751                    }),
752                    _ => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
753                }
754            }
755            Some(SymWord::Expr(_)) => Err(SymbolicError::Unsupported("symbolic bytecode opcode")),
756        }
757    }
758
759    /// Implements the `analysis_opcode` symbolic memory helper.
760    pub(crate) fn analysis_opcode(&self, pc: usize) -> Option<u8> {
761        self.bytes.get(pc).map(|byte| match byte {
762            SymWord::Concrete(value) => value.to::<u8>(),
763            SymWord::Expr(_) => opcode::STOP,
764        })
765    }
766
767    /// Returns the `concrete_range` symbolic memory helper result.
768    pub(crate) fn concrete_range(
769        &self,
770        offset: usize,
771        size: usize,
772        reason: &'static str,
773    ) -> Result<Vec<u8>, SymbolicError> {
774        let mut out = Vec::with_capacity(size);
775        for idx in 0..size {
776            match self.bytes.get(offset + idx) {
777                Some(SymWord::Concrete(value)) => out.push(value.to::<u8>()),
778                Some(SymWord::Expr(_)) => return Err(SymbolicError::Unsupported(reason)),
779                None => out.push(0),
780            }
781        }
782        Ok(out)
783    }
784
785    /// Returns the `read_bytes` symbolic memory helper result.
786    pub(crate) fn read_bytes(&self, offset: usize, size: usize) -> Vec<SymWord> {
787        (0..size)
788            .map(|idx| self.bytes.get(offset + idx).cloned().unwrap_or_else(SymWord::zero))
789            .collect()
790    }
791
792    /// Returns the `read_bytes_offset` symbolic memory helper result.
793    pub(crate) fn read_bytes_offset(&self, offset: SymWord, size: usize) -> Vec<SymWord> {
794        match offset {
795            SymWord::Concrete(offset) => {
796                if offset > U256::from(usize::MAX) {
797                    return vec![SymWord::zero(); size];
798                }
799                self.read_bytes(offset.to::<usize>(), size)
800            }
801            SymWord::Expr(offset) => {
802                (0..size).map(|idx| self.byte_dynamic_with_delta(offset.clone(), idx)).collect()
803            }
804        }
805    }
806
807    /// Returns the `byte_dynamic_with_delta` symbolic memory helper result.
808    pub(crate) fn byte_dynamic_with_delta(&self, offset: Expr, delta: usize) -> SymWord {
809        let mut result = Expr::Const(U256::ZERO);
810        for candidate in (delta..self.len()).rev() {
811            result = Expr::Ite(
812                Box::new(BoolExpr::eq(offset.clone(), Expr::Const(U256::from(candidate - delta)))),
813                Box::new(self.bytes[candidate].clone().into_expr()),
814                Box::new(result),
815            );
816        }
817        SymWord::Expr(result)
818    }
819
820    /// Returns the `concrete_bytes` symbolic memory helper result.
821    pub(crate) fn concrete_bytes(&self, reason: &'static str) -> Result<Vec<u8>, SymbolicError> {
822        self.concrete_range(0, self.len(), reason)
823    }
824}
825
826#[derive(Clone, Debug)]
827pub(crate) struct SymReturnData {
828    pub(crate) len: usize,
829    pub(crate) len_word: SymWord,
830    pub(crate) bytes: BTreeMap<usize, SymWord>,
831}
832
833impl Default for SymReturnData {
834    /// Implements the `default` symbolic memory helper.
835    fn default() -> Self {
836        Self { len: 0, len_word: SymWord::zero(), bytes: BTreeMap::new() }
837    }
838}
839
840impl SymReturnData {
841    /// Converts values for the `from_words` symbolic memory helper.
842    pub(crate) fn from_words(words: Vec<SymWord>) -> Self {
843        let bytes = words.into_iter().flat_map(word_bytes).collect::<Vec<_>>();
844        Self::from_symbolic_bytes(bytes)
845    }
846
847    /// Converts values for the `from_concrete_bytes` symbolic memory helper.
848    pub(crate) fn from_concrete_bytes(bytes: Vec<u8>) -> Self {
849        Self::from_symbolic_bytes(
850            bytes.into_iter().map(|byte| SymWord::Concrete(U256::from(byte))).collect(),
851        )
852    }
853
854    /// Converts values for the `from_symbolic_bytes` symbolic memory helper.
855    pub(crate) fn from_symbolic_bytes(bytes: Vec<SymWord>) -> Self {
856        let len = bytes.len();
857        Self {
858            len,
859            len_word: SymWord::Concrete(U256::from(len)),
860            bytes: bytes.into_iter().enumerate().collect(),
861        }
862    }
863
864    /// Converts values for the `from_symbolic_bytes_with_len` symbolic memory helper.
865    pub(crate) fn from_symbolic_bytes_with_len(bytes: Vec<SymWord>, len_word: SymWord) -> Self {
866        let len = bytes.len();
867        Self { len, len_word, bytes: bytes.into_iter().enumerate().collect() }
868    }
869
870    /// Implements the `len_word` symbolic memory helper.
871    pub(crate) fn len_word(&self) -> SymWord {
872        self.len_word.clone()
873    }
874
875    /// Implements the `len_expr` symbolic memory helper.
876    pub(crate) fn len_expr(&self) -> Expr {
877        self.len_word.clone().into_expr()
878    }
879
880    /// Returns whether `has_symbolic_len` holds.
881    pub(crate) const fn has_symbolic_len(&self) -> bool {
882        matches!(self.len_word, SymWord::Expr(_))
883    }
884
885    /// Implements the `byte` symbolic memory helper.
886    pub(crate) fn byte(&self, offset: usize) -> SymWord {
887        self.bytes.get(&offset).cloned().unwrap_or_else(SymWord::zero)
888    }
889
890    /// Returns the `read_bytes_offset` symbolic memory helper result.
891    pub(crate) fn read_bytes_offset(&self, offset: SymWord, size: usize) -> Vec<SymWord> {
892        match offset {
893            SymWord::Concrete(offset) => {
894                if offset > U256::from(usize::MAX) {
895                    return vec![SymWord::zero(); size];
896                }
897                let offset = offset.to::<usize>();
898                (0..size).map(|idx| self.byte(offset + idx)).collect()
899            }
900            SymWord::Expr(offset) => {
901                (0..size).map(|idx| self.byte_dynamic_with_delta(offset.clone(), idx)).collect()
902            }
903        }
904    }
905
906    /// Returns the `byte_dynamic_with_delta` symbolic memory helper result.
907    pub(crate) fn byte_dynamic_with_delta(&self, offset: Expr, delta: usize) -> SymWord {
908        let mut result = Expr::Const(U256::ZERO);
909        for candidate in (delta..self.len).rev() {
910            result = Expr::Ite(
911                Box::new(BoolExpr::eq(offset.clone(), Expr::Const(U256::from(candidate - delta)))),
912                Box::new(self.byte(candidate).into_expr()),
913                Box::new(result),
914            );
915        }
916        SymWord::Expr(result)
917    }
918
919    /// Returns the `load_word` symbolic memory helper result.
920    pub(crate) fn load_word(&self, offset: usize) -> Result<SymWord, SymbolicError> {
921        if offset.saturating_add(32) > self.len {
922            return Err(SymbolicError::Unsupported("out-of-bounds symbolic returndata word"));
923        }
924        Ok(word_from_bytes((0..32).map(|idx| self.byte(offset + idx))))
925    }
926
927    /// Returns the `read_concrete` symbolic memory helper result.
928    pub(crate) fn read_concrete(&self, reason: &'static str) -> Result<Vec<u8>, SymbolicError> {
929        let mut out = Vec::with_capacity(self.len);
930        for offset in 0..self.len {
931            match self.byte(offset) {
932                SymWord::Concrete(value) => out.push(value.to::<u8>()),
933                SymWord::Expr(_) => return Err(SymbolicError::Unsupported(reason)),
934            }
935        }
936        Ok(out)
937    }
938
939    /// Converts values for the `to_code` symbolic memory helper.
940    pub(crate) fn to_code(&self) -> Result<SymCode, SymbolicError> {
941        if self.has_symbolic_len() {
942            return Err(SymbolicError::Unsupported(
943                "CREATE with symbolic runtime size not modeled",
944            ));
945        }
946        Ok(SymCode { bytes: (0..self.len).map(|offset| self.byte(offset)).collect() })
947    }
948}
foundry_evm_symbolic/runtime/memory.rs

foundry_evm_symbolic/runtime/
memory.rs
