foundry_evm_symbolic/runtime/
bytes.rs

1use super::{expr::hashcons::HashConsed, *};
2
3#[derive(Clone, PartialEq, Eq, Hash)]
4pub(crate) struct SymBytes {
5    pub(in crate::runtime) kind: HashConsed<SymBytesKind>,
6}
7
8impl fmt::Debug for SymBytes {
9    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
10        self.kind().fmt(f)
11    }
12}
13
14#[derive(Debug, PartialEq, Eq, Hash)]
15pub(in crate::runtime) enum SymBytesKind {
16    Concrete(Vec<u8>),
17    Exprs(Vec<SymExpr>),
18    Word(SymExpr),
19    Concat(Vec<SymBytes>),
20    Slice { bytes: SymBytes, offset: SymExpr, len: usize },
21    Sized { bytes: SymBytes, size: SymExpr, max_size: usize },
22}
23
24impl SymBytes {
25    fn from_kind(cx: &mut SymCx, kind: SymBytesKind) -> Self {
26        cx.mk_bytes_kind(kind)
27    }
28
29    fn kind(&self) -> &SymBytesKind {
30        self.kind.value()
31    }
32
33    pub(crate) fn empty(cx: &mut SymCx) -> Self {
34        Self::from_kind(cx, SymBytesKind::Concrete(Vec::new()))
35    }
36
37    pub(crate) fn concrete(cx: &mut SymCx, bytes: Vec<u8>) -> Self {
38        Self::from_kind(cx, SymBytesKind::Concrete(bytes))
39    }
40
41    pub(crate) fn as_concrete_slice(&self) -> Option<&[u8]> {
42        match self.kind() {
43            SymBytesKind::Concrete(bytes) => Some(bytes),
44            _ => None,
45        }
46    }
47
48    pub(crate) fn exprs(cx: &mut SymCx, bytes: Vec<SymExpr>) -> Self {
49        if let Ok(concrete) = concrete_expr_bytes(&bytes, "symbolic bytes") {
50            Self::concrete(cx, concrete)
51        } else {
52            Self::from_kind(cx, SymBytesKind::Exprs(bytes))
53        }
54    }
55
56    pub(crate) fn word(cx: &mut SymCx, word: SymExpr) -> Self {
57        if let Some(word) = word.as_const() {
58            Self::concrete(cx, word.to_be_bytes::<32>().to_vec())
59        } else {
60            Self::from_kind(cx, SymBytesKind::Word(word))
61        }
62    }
63
64    pub(crate) fn concat(cx: &mut SymCx, bytes: impl IntoIterator<Item = Self>) -> Self {
65        let mut out = Vec::new();
66        for bytes in bytes {
67            match bytes.kind() {
68                SymBytesKind::Concrete(values) if values.is_empty() => {}
69                SymBytesKind::Concat(values) => out.extend(values.iter().cloned()),
70                _ => out.push(bytes),
71            }
72        }
73        match out.len() {
74            0 => Self::empty(cx),
75            1 => out.pop().expect("single item exists"),
76            _ => Self::from_kind(cx, SymBytesKind::Concat(out)),
77        }
78    }
79
80    pub(crate) fn slice(cx: &mut SymCx, bytes: Self, offset: SymExpr, len: usize) -> Self {
81        if len == 0 {
82            return Self::empty(cx);
83        }
84        if let Some(offset) = offset.eval() {
85            let Ok(offset) = usize::try_from(offset) else {
86                return Self::concrete(cx, vec![0; len]);
87            };
88            return bytes.slice_concrete(cx, offset, len);
89        }
90        Self::slice_node(cx, bytes, offset, len)
91    }
92
93    fn slice_node(cx: &mut SymCx, bytes: Self, offset: SymExpr, len: usize) -> Self {
94        Self::from_kind(cx, SymBytesKind::Slice { bytes, offset, len })
95    }
96
97    pub(crate) fn sized(cx: &mut SymCx, bytes: Self, size: SymExpr, max_size: usize) -> Self {
98        if max_size == 0 {
99            return Self::empty(cx);
100        }
101        if let Some(size) = size.eval() {
102            let size = usize::try_from(size).map_or(max_size, |size| size.min(max_size));
103            let bytes = bytes.slice_concrete(cx, 0, size);
104            let padding = Self::concrete(cx, vec![0; max_size - size]);
105            return Self::concat(cx, [bytes, padding]);
106        }
107        Self::from_kind(cx, SymBytesKind::Sized { bytes, size, max_size })
108    }
109
110    pub(crate) fn len(&self) -> usize {
111        match self.kind() {
112            SymBytesKind::Concrete(bytes) => bytes.len(),
113            SymBytesKind::Exprs(bytes) => bytes.len(),
114            SymBytesKind::Word(_) => 32,
115            SymBytesKind::Concat(values) => {
116                values.iter().fold(0usize, |len, bytes| len.saturating_add(bytes.len()))
117            }
118            SymBytesKind::Slice { len, .. } => *len,
119            SymBytesKind::Sized { max_size, .. } => *max_size,
120        }
121    }
122
123    pub(crate) fn is_empty(&self) -> bool {
124        self.len() == 0
125    }
126
127    pub(crate) fn byte(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
128        match self.kind() {
129            SymBytesKind::Concrete(bytes) => bytes
130                .get(offset)
131                .copied()
132                .map(|byte| SymExpr::constant(cx, U256::from(byte)))
133                .unwrap_or_else(|| SymExpr::zero(cx)),
134            SymBytesKind::Exprs(bytes) => {
135                bytes.get(offset).cloned().unwrap_or_else(|| SymExpr::zero(cx))
136            }
137            SymBytesKind::Word(word) => {
138                if offset >= 32 {
139                    SymExpr::zero(cx)
140                } else if let Some(byte) = word.known_byte(offset) {
141                    SymExpr::constant(cx, U256::from(byte))
142                } else {
143                    word.extracted_byte(cx, offset)
144                }
145            }
146            SymBytesKind::Concat(values) => {
147                let mut offset = offset;
148                for bytes in values {
149                    if offset < bytes.len() {
150                        return bytes.byte(cx, offset);
151                    }
152                    offset = offset.saturating_sub(bytes.len());
153                }
154                SymExpr::zero(cx)
155            }
156            SymBytesKind::Slice { bytes, offset: base_offset, len } => {
157                if offset >= *len {
158                    SymExpr::zero(cx)
159                } else if let Some(base_offset) = base_offset.eval() {
160                    let Ok(base_offset) = usize::try_from(base_offset) else {
161                        return SymExpr::zero(cx);
162                    };
163                    let Some(offset) = base_offset.checked_add(offset) else {
164                        return SymExpr::zero(cx);
165                    };
166                    bytes.byte(cx, offset)
167                } else {
168                    bytes.byte_dynamic_with_delta(cx, base_offset, offset)
169                }
170            }
171            SymBytesKind::Sized { bytes, size, max_size } => {
172                if offset >= *max_size {
173                    return SymExpr::zero(cx);
174                }
175                let source = bytes.byte(cx, offset);
176                let offset = SymExpr::constant(cx, U256::from(offset));
177                let condition = SymBoolExpr::cmp(cx, SymCmpOp::Ult, offset, size.clone());
178                let zero = SymExpr::zero(cx);
179                SymExpr::ite(cx, condition, source, zero)
180            }
181        }
182    }
183
184    pub(crate) fn byte_dynamic_with_delta(
185        &self,
186        cx: &mut SymCx,
187        offset: &SymExpr,
188        delta: usize,
189    ) -> SymExpr {
190        let mut result = SymExpr::zero(cx);
191        for candidate in (delta..self.len()).rev() {
192            let candidate_offset = candidate - delta;
193            let candidate_expr = SymExpr::constant(cx, U256::from(candidate_offset));
194            let condition = SymBoolExpr::eq(cx, offset.clone(), candidate_expr);
195            let byte = self.byte(cx, candidate);
196            result = SymExpr::ite(cx, condition, byte, result);
197        }
198        result
199    }
200
201    pub(crate) fn slice_concrete(&self, cx: &mut SymCx, offset: usize, len: usize) -> Self {
202        if len == 0 {
203            return Self::empty(cx);
204        }
205        if offset == 0 && len == self.len() {
206            return self.clone();
207        }
208        match self.kind() {
209            SymBytesKind::Concrete(bytes) => {
210                let out = if offset.checked_add(len).is_some_and(|end| end <= bytes.len()) {
211                    bytes[offset..offset + len].to_vec()
212                } else {
213                    (0..len)
214                        .map(|idx| bytes.get(offset + idx).copied().unwrap_or_default())
215                        .collect()
216                };
217                Self::concrete(cx, out)
218            }
219            SymBytesKind::Exprs(bytes) => {
220                let bytes = (0..len)
221                    .map(|idx| {
222                        bytes.get(offset + idx).cloned().unwrap_or_else(|| SymExpr::zero(cx))
223                    })
224                    .collect();
225                Self::exprs(cx, bytes)
226            }
227            SymBytesKind::Word(word) if offset == 0 && len == 32 => Self::word(cx, word.clone()),
228            SymBytesKind::Word(_) | SymBytesKind::Sized { .. } => {
229                let offset = SymExpr::constant(cx, U256::from(offset));
230                Self::slice_node(cx, self.clone(), offset, len)
231            }
232            SymBytesKind::Slice { bytes, offset: base_offset, .. } => {
233                if let Some(base_offset) = base_offset.eval()
234                    && let Ok(base_offset) = usize::try_from(base_offset)
235                    && let Some(offset) = base_offset.checked_add(offset)
236                {
237                    bytes.slice_concrete(cx, offset, len)
238                } else {
239                    let offset = SymExpr::constant(cx, U256::from(offset));
240                    Self::slice_node(cx, self.clone(), offset, len)
241                }
242            }
243            SymBytesKind::Concat(values) => {
244                let mut offset = offset;
245                let mut len = len;
246                let mut out = Vec::new();
247                for bytes in values {
248                    if len == 0 {
249                        break;
250                    }
251
252                    let bytes_len = bytes.len();
253                    if offset >= bytes_len {
254                        offset -= bytes_len;
255                        continue;
256                    }
257
258                    let take = (bytes_len - offset).min(len);
259                    if offset == 0 && take == bytes_len {
260                        out.push(bytes.clone());
261                    } else {
262                        out.push(bytes.slice_concrete(cx, offset, take));
263                    }
264                    len -= take;
265                    offset = 0;
266                }
267
268                if len != 0 {
269                    out.push(Self::concrete(cx, vec![0; len]));
270                }
271                Self::concat(cx, out)
272            }
273        }
274    }
275
276    pub(crate) fn read_offset(&self, cx: &mut SymCx, offset: SymExpr, len: usize) -> Self {
277        Self::slice(cx, self.clone(), offset, len)
278    }
279
280    pub(crate) fn word_at(&self, cx: &mut SymCx, offset: usize) -> SymExpr {
281        if let Some(word) = self.word_fragment_at(cx, offset, 32, 0) {
282            return word;
283        }
284
285        match self.kind() {
286            SymBytesKind::Concrete(bytes) => {
287                let mut word = [0u8; 32];
288                if offset < bytes.len() {
289                    let take = (bytes.len() - offset).min(32);
290                    word[..take].copy_from_slice(&bytes[offset..offset + take]);
291                }
292                SymExpr::constant(cx, U256::from_be_bytes(word))
293            }
294            SymBytesKind::Exprs(bytes) => {
295                let bytes = (0..32)
296                    .map(|idx| {
297                        bytes.get(offset + idx).cloned().unwrap_or_else(|| SymExpr::zero(cx))
298                    })
299                    .collect::<Vec<_>>();
300                SymExpr::from_bytes(cx, bytes)
301            }
302            SymBytesKind::Word(word) if offset == 0 => word.clone(),
303            SymBytesKind::Word(_) if offset >= 32 => SymExpr::zero(cx),
304            SymBytesKind::Slice { bytes, offset: base_offset, len } => {
305                if offset.checked_add(32).is_some_and(|end| end <= *len)
306                    && let Some(base_offset) = base_offset.eval()
307                    && let Ok(base_offset) = usize::try_from(base_offset)
308                    && let Some(base_offset) = base_offset.checked_add(offset)
309                {
310                    return bytes.word_at(cx, base_offset);
311                }
312                let bytes = (0..32).map(|idx| self.byte(cx, offset + idx)).collect::<Vec<_>>();
313                SymExpr::from_bytes(cx, bytes)
314            }
315            _ => {
316                let bytes = (0..32).map(|idx| self.byte(cx, offset + idx)).collect::<Vec<_>>();
317                SymExpr::from_bytes(cx, bytes)
318            }
319        }
320    }
321
322    pub(crate) fn right_aligned_word(&self, cx: &mut SymCx, offset: usize, len: usize) -> SymExpr {
323        debug_assert!(len <= 32);
324        let len = len.min(32);
325        if let Some(word) = self.word_fragment_at(cx, offset, len, 32 - len) {
326            return word;
327        }
328
329        let mut bytes = Vec::with_capacity(32);
330        for _ in 0..32 - len {
331            bytes.push(SymExpr::zero(cx));
332        }
333        bytes.extend((0..len).map(|idx| self.byte(cx, offset + idx)));
334        SymExpr::from_bytes(cx, bytes)
335    }
336
337    fn word_fragment_at(
338        &self,
339        cx: &mut SymCx,
340        offset: usize,
341        len: usize,
342        out_offset: usize,
343    ) -> Option<SymExpr> {
344        debug_assert!(len <= 32);
345        debug_assert!(out_offset <= 32);
346        debug_assert!(out_offset + len <= 32);
347
348        if len == 0 {
349            return Some(SymExpr::zero(cx));
350        }
351
352        match self.kind() {
353            SymBytesKind::Concrete(bytes) => {
354                let mut word = [0u8; 32];
355                if offset < bytes.len() {
356                    let take = (bytes.len() - offset).min(len);
357                    word[out_offset..out_offset + take]
358                        .copy_from_slice(&bytes[offset..offset + take]);
359                }
360                Some(SymExpr::constant(cx, U256::from_be_bytes(word)))
361            }
362            SymBytesKind::Word(word) => {
363                Self::word_expr_fragment(cx, word.clone(), offset, len, out_offset)
364            }
365            SymBytesKind::Slice { bytes, offset: base_offset, len: slice_len } => {
366                let available = slice_len.saturating_sub(offset).min(len);
367                if available == 0 {
368                    return Some(SymExpr::zero(cx));
369                }
370                let base_offset =
371                    base_offset.eval().and_then(|offset| usize::try_from(offset).ok())?;
372                bytes.word_fragment_at(cx, base_offset.checked_add(offset)?, available, out_offset)
373            }
374            SymBytesKind::Concat(values) => {
375                let mut offset = offset;
376                let mut out_offset = out_offset;
377                let mut remaining = len;
378                let mut out = SymExpr::zero(cx);
379
380                for bytes in values {
381                    if remaining == 0 {
382                        break;
383                    }
384
385                    let bytes_len = bytes.len();
386                    if offset >= bytes_len {
387                        offset -= bytes_len;
388                        continue;
389                    }
390
391                    let take = (bytes_len - offset).min(remaining);
392                    let fragment = bytes.word_fragment_at(cx, offset, take, out_offset)?;
393                    out = SymExpr::binop(cx, SymBinOp::Or, out, fragment);
394                    out_offset += take;
395                    remaining -= take;
396                    offset = 0;
397                }
398
399                Some(out)
400            }
401            SymBytesKind::Exprs(_) | SymBytesKind::Sized { .. } => None,
402        }
403    }
404
405    fn word_expr_fragment(
406        cx: &mut SymCx,
407        word: SymExpr,
408        offset: usize,
409        len: usize,
410        out_offset: usize,
411    ) -> Option<SymExpr> {
412        let len = 32usize.checked_sub(offset)?.min(len);
413        if len == 0 {
414            return Some(SymExpr::zero(cx));
415        }
416        if offset == 0 && len == 32 && out_offset == 0 {
417            return Some(word);
418        }
419
420        let src_trailing_bits = (32 - (offset + len)) * 8;
421        let dst_trailing_bits = (32 - (out_offset + len)) * 8;
422        let mask = mask_bits(U256::MAX, len * 8);
423
424        let src_trailing_bits = SymExpr::constant(cx, U256::from(src_trailing_bits));
425        let expr = SymExpr::binop(cx, SymBinOp::Shr, word, src_trailing_bits);
426        let mask = SymExpr::constant(cx, mask);
427        let expr = SymExpr::binop(cx, SymBinOp::And, expr, mask);
428        let dst_trailing_bits = SymExpr::constant(cx, U256::from(dst_trailing_bits));
429        Some(SymExpr::binop(cx, SymBinOp::Shl, expr, dst_trailing_bits))
430    }
431
432    /// Returns `true` if the observable bytes depend on an unresolved `GAS` / `gasleft()` value.
433    ///
434    /// Only the represented byte range is inspected: bytes of a backing value that a slice or a
435    /// `max_size` bound excludes are never reachable and do not taint the result. A gas-dependent
436    /// slice offset or dynamic size always taints, because the byte layout itself would then
437    /// depend on gas.
438    pub(crate) fn contains_gasleft(&self, cx: &mut SymCx) -> bool {
439        if self.shape_depends_on_gasleft() {
440            return true;
441        }
442        // Fast structural pre-check: without a gas-dependent backing value nothing can be tainted.
443        if !self.backing_contains_gasleft() {
444            return false;
445        }
446        (0..self.len()).any(|offset| self.byte(cx, offset).contains_gasleft())
447    }
448
449    /// Returns `true` if a slice offset or dynamic size anywhere in the tree mentions `gasleft()`.
450    fn shape_depends_on_gasleft(&self) -> bool {
451        match self.kind() {
452            SymBytesKind::Concrete(_) | SymBytesKind::Exprs(_) | SymBytesKind::Word(_) => false,
453            SymBytesKind::Concat(parts) => parts.iter().any(Self::shape_depends_on_gasleft),
454            SymBytesKind::Slice { bytes, offset, .. } => {
455                offset.contains_gasleft() || bytes.shape_depends_on_gasleft()
456            }
457            SymBytesKind::Sized { bytes, size, .. } => {
458                size.contains_gasleft() || bytes.shape_depends_on_gasleft()
459            }
460        }
461    }
462
463    /// Returns `true` if any backing value, observable or not, mentions `gasleft()`.
464    fn backing_contains_gasleft(&self) -> bool {
465        match self.kind() {
466            SymBytesKind::Concrete(_) => false,
467            SymBytesKind::Exprs(bytes) => bytes.iter().any(SymExpr::contains_gasleft),
468            SymBytesKind::Word(word) => word.contains_gasleft(),
469            SymBytesKind::Concat(parts) => parts.iter().any(Self::backing_contains_gasleft),
470            SymBytesKind::Slice { bytes, .. } | SymBytesKind::Sized { bytes, .. } => {
471                bytes.backing_contains_gasleft()
472            }
473        }
474    }
475
476    pub(crate) fn materialize(&self, cx: &mut SymCx) -> Vec<SymExpr> {
477        (0..self.len()).map(|idx| self.byte(cx, idx)).collect()
478    }
479
480    pub(crate) fn same_bytes(&self, cx: &mut SymCx, other: &Self) -> bool {
481        self.len() == other.len()
482            && (0..self.len()).all(|idx| self.byte(cx, idx) == other.byte(cx, idx))
483    }
484
485    pub(crate) fn prefix_condition(&self, cx: &mut SymCx, prefix: &Self) -> Option<SymBoolExpr> {
486        if prefix.len() > self.len() {
487            return None;
488        }
489        let mut conditions = Vec::new();
490        for idx in 0..prefix.len() {
491            let actual = self.byte(cx, idx);
492            let expected = prefix.byte(cx, idx);
493            if actual == expected {
494                continue;
495            }
496            match (actual.as_const(), expected.as_const()) {
497                (Some(actual), Some(expected)) if actual.to::<u8>() == expected.to::<u8>() => {}
498                (Some(_), Some(_)) => return None,
499                _ => conditions.push(SymBoolExpr::eq(cx, actual, expected)),
500            }
501        }
502        Some(SymBoolExpr::and(cx, conditions))
503    }
504
505    pub(crate) fn eval_model<M: SymbolicModelLookup + ?Sized>(
506        &self,
507        cx: &mut SymCx,
508        model: &M,
509    ) -> Result<Vec<u8>, SymbolicError> {
510        match self.kind() {
511            SymBytesKind::Concrete(bytes) => Ok(bytes.clone()),
512            _ => (0..self.len())
513                .map(|idx| Ok(self.byte(cx, idx).eval_model(model)?.to::<u8>()))
514                .collect(),
515        }
516    }
517
518    pub(crate) fn concrete_bytes(
519        &self,
520        cx: &mut SymCx,
521        reason: &'static str,
522    ) -> Result<Vec<u8>, SymbolicError> {
523        let mut out = Vec::with_capacity(self.len());
524        self.append_concrete_range(cx, 0, self.len(), &mut out, reason)?;
525        Ok(out)
526    }
527
528    fn append_concrete_range(
529        &self,
530        cx: &mut SymCx,
531        mut offset: usize,
532        mut len: usize,
533        out: &mut Vec<u8>,
534        reason: &'static str,
535    ) -> Result<(), SymbolicError> {
536        if len == 0 {
537            return Ok(());
538        }
539
540        match self.kind() {
541            SymBytesKind::Concrete(bytes) => {
542                if offset >= bytes.len() {
543                    out.resize(out.len() + len, 0);
544                    return Ok(());
545                }
546
547                let take = (bytes.len() - offset).min(len);
548                out.extend_from_slice(&bytes[offset..offset + take]);
549                if len > take {
550                    out.resize(out.len() + len - take, 0);
551                }
552            }
553            SymBytesKind::Exprs(bytes) => {
554                for idx in 0..len {
555                    let Some(byte) = offset.checked_add(idx).and_then(|idx| bytes.get(idx)) else {
556                        out.push(0);
557                        continue;
558                    };
559                    let Some(byte) = byte.as_const() else {
560                        return Err(SymbolicError::Unsupported(reason));
561                    };
562                    out.push(byte.to::<u8>());
563                }
564            }
565            SymBytesKind::Concat(values) => {
566                for bytes in values {
567                    if len == 0 {
568                        break;
569                    }
570
571                    let bytes_len = bytes.len();
572                    if offset >= bytes_len {
573                        offset -= bytes_len;
574                        continue;
575                    }
576
577                    let take = (bytes_len - offset).min(len);
578                    bytes.append_concrete_range(cx, offset, take, out, reason)?;
579                    len -= take;
580                    offset = 0;
581                }
582
583                if len != 0 {
584                    out.resize(out.len() + len, 0);
585                }
586            }
587            SymBytesKind::Slice { bytes, offset: base_offset, len: slice_len } => {
588                if offset >= *slice_len {
589                    out.resize(out.len() + len, 0);
590                    return Ok(());
591                }
592
593                let take = (*slice_len - offset).min(len);
594                if let Some(base_offset) = base_offset.eval()
595                    && let Ok(base_offset) = usize::try_from(base_offset)
596                    && let Some(offset) = base_offset.checked_add(offset)
597                {
598                    bytes.append_concrete_range(cx, offset, take, out, reason)?;
599                    if len > take {
600                        out.resize(out.len() + len - take, 0);
601                    }
602                } else {
603                    let bytes = self.slice_concrete(cx, offset, len).materialize(cx);
604                    out.extend(concrete_expr_bytes(&bytes, reason)?);
605                }
606            }
607            _ => {
608                let bytes = self.slice_concrete(cx, offset, len).materialize(cx);
609                out.extend(concrete_expr_bytes(&bytes, reason)?);
610            }
611        }
612        Ok(())
613    }
614}
615
616#[cfg(test)]
617mod tests {
618    use super::*;
619
620    #[test]
621    fn bytes_contains_gasleft_inspects_only_observable_range() {
622        let mut cx = SymCx::new();
623        let gas = SymExpr::gas_left(&mut cx, 0);
624        let mask = SymExpr::constant(&mut cx, U256::from(0xff));
625        let low_byte_gas = SymExpr::binop(&mut cx, SymBinOp::And, gas.clone(), mask);
626        let word = SymBytes::word(&mut cx, low_byte_gas);
627        assert!(word.contains_gasleft(&mut cx));
628
629        // The 31 high bytes are provably zero, so slicing them out is gas independent.
630        let high_bytes = word.slice_concrete(&mut cx, 0, 31);
631        assert!(!high_bytes.contains_gasleft(&mut cx));
632        let low_byte = word.slice_concrete(&mut cx, 31, 1);
633        assert!(low_byte.contains_gasleft(&mut cx));
634
635        // A gas-dependent slice offset taints even gas-independent source bytes.
636        let source = SymBytes::concrete(&mut cx, vec![1, 2, 3, 4]);
637        let gas_slice = SymBytes::slice(&mut cx, source, gas.clone(), 2);
638        assert!(gas_slice.contains_gasleft(&mut cx));
639
640        // Bytes beyond `max_size` can never reach the consumer.
641        let zeros = SymBytes::concrete(&mut cx, vec![0; 32]);
642        let gas_word = SymBytes::word(&mut cx, gas.clone());
643        let source = SymBytes::concat(&mut cx, [zeros, gas_word]);
644        let size = SymExpr::var(&mut cx, "size");
645        let sized = SymBytes::sized(&mut cx, source.clone(), size, 32);
646        assert!(!sized.contains_gasleft(&mut cx));
647        // A gas-dependent size taints even when every observable byte is zero.
648        let sized = SymBytes::sized(&mut cx, source.clone(), gas, 32);
649        assert!(sized.contains_gasleft(&mut cx));
650        let size = SymExpr::var(&mut cx, "size");
651        let sized = SymBytes::sized(&mut cx, source, size, 64);
652        assert!(sized.contains_gasleft(&mut cx));
653    }
654}
foundry_evm_symbolic/runtime/bytes.rs

foundry_evm_symbolic/runtime/
bytes.rs
