foundry_evm_symbolic/
abi.rs

1use super::{runtime::*, *};
2
3#[derive(Clone, Debug)]
4pub(super) struct SymbolicCalldata {
5    bytes: SymBytes,
6    inputs: Vec<SymbolicInput>,
7    constraints: Vec<SymBoolExpr>,
8}
9
10impl SymbolicCalldata {
11    pub(super) fn variants(
12        function: &Function,
13        config: &SymbolicConfig,
14        cx: &mut SymCx,
15    ) -> Result<Vec<Self>, SymbolicError> {
16        Self::variants_with_prefix(function, config, cx, "calldata")
17    }
18
19    pub(super) fn selector_only(
20        cx: &mut SymCx,
21        function: &Function,
22    ) -> Result<Self, SymbolicError> {
23        if !function.inputs.is_empty() {
24            return Err(SymbolicError::UnsupportedAbi(format!(
25                "symbolic invariant `{}` must take no parameters",
26                function.name
27            )));
28        }
29        Ok(Self {
30            bytes: SymBytes::concrete(cx, function.selector().to_vec()),
31            inputs: Vec::new(),
32            constraints: Vec::new(),
33        })
34    }
35
36    pub(super) fn variants_with_prefix(
37        function: &Function,
38        config: &SymbolicConfig,
39        cx: &mut SymCx,
40        prefix: &str,
41    ) -> Result<Vec<Self>, SymbolicError> {
42        let variant_limit = calldata_variant_limit(config);
43        let mut builder = SymbolicAbiBuilder::new(config, cx);
44        let mut variants = vec![(SymbolicAbiState::default(), Vec::new())];
45        for (idx, input) in function.inputs.iter().enumerate() {
46            let ty = input.selector_type();
47            let mut next_variants = Vec::new();
48            for (state, inputs) in variants {
49                for (state, input) in SymbolicInput::variants(
50                    &mut builder,
51                    state,
52                    prefix,
53                    idx,
54                    Some(input.name.as_str()),
55                    ty.as_ref(),
56                )? {
57                    let mut inputs = inputs.clone();
58                    inputs.push(input);
59                    push_variant(&mut next_variants, (state, inputs), variant_limit)?;
60                }
61            }
62            variants = next_variants;
63        }
64
65        validate_positional_dynamic_lengths(
66            config,
67            variants.iter().map(|(state, _)| state.positional_dynamic_index).max().unwrap_or(0),
68        )?;
69
70        let mut out = Vec::with_capacity(variants.len());
71        for (state, inputs) in variants {
72            let selector = SymBytes::concrete(builder.cx, function.selector().to_vec());
73            let encoded = builder.encode_sequence(inputs.iter().map(|input| &input.value));
74            let bytes = SymBytes::concat(builder.cx, [selector, encoded]);
75            if bytes.len() > config.max_calldata_bytes as usize {
76                return Err(SymbolicError::Unsupported(
77                    "symbolic calldata size exceeds configured max",
78                ));
79            }
80
81            out.push(Self { bytes, inputs, constraints: state.constraints });
82        }
83        Ok(out)
84    }
85
86    pub(super) fn call_data(&self, cx: &mut SymCx) -> SymCalldata {
87        SymCalldata::from_bytes(cx, self.bytes.clone())
88    }
89
90    /// Returns symbolic calldata constraints.
91    pub(super) fn constraints(&self) -> &[SymBoolExpr] {
92        &self.constraints
93    }
94
95    /// Consumes this symbolic calldata into its constraints.
96    pub(super) fn into_constraints(self) -> Vec<SymBoolExpr> {
97        self.constraints
98    }
99
100    pub(super) fn model_to_args(
101        &self,
102        cx: &mut SymCx,
103        model: &(impl SymbolicModelLookup + ?Sized),
104    ) -> Result<Vec<DynSolValue>, SymbolicError> {
105        self.inputs.iter().map(|input| input.value.model_value(cx, model)).collect()
106    }
107
108    pub(super) fn seed_model(
109        &self,
110        cx: &mut SymCx,
111        seed: &SymbolicConcreteInput,
112    ) -> Option<SymbolicModel> {
113        if seed.args.len() != self.inputs.len() {
114            return None;
115        }
116
117        let mut model = SymbolicModel::default();
118        for (input, arg) in self.inputs.iter().zip(&seed.args) {
119            if !input.value.seed_model_value(cx, &mut model, arg) {
120                return None;
121            }
122        }
123
124        for constraint in &self.constraints {
125            if constraint.eval_model_if_complete(&model).ok().flatten() != Some(true) {
126                return None;
127            }
128        }
129
130        let calldata = self.bytes.eval_model(cx, &model).ok()?;
131        (calldata.as_slice() == seed.calldata.as_ref()).then_some(model)
132    }
133}
134
135#[derive(Clone, Debug)]
136pub(super) struct SymbolicInput {
137    value: SymbolicAbiValue,
138}
139
140impl SymbolicInput {
141    pub(super) fn variants<'a, 'cx>(
142        builder: &mut SymbolicAbiBuilder<'a, 'cx>,
143        state: SymbolicAbiState,
144        prefix: &str,
145        idx: usize,
146        abi_name: Option<&str>,
147        ty: &str,
148    ) -> Result<Vec<(SymbolicAbiState, Self)>, SymbolicError> {
149        let ty =
150            DynSolType::parse(ty).map_err(|_| SymbolicError::UnsupportedAbi(ty.to_string()))?;
151        let name = format!("{prefix}_{idx}");
152        let aliases =
153            abi_name.filter(|name| !name.is_empty()).map(str::to_string).into_iter().collect();
154        builder.value_variants(state, name, aliases, &ty).map(|variants| {
155            variants.into_iter().map(|(state, value)| (state, Self { value })).collect()
156        })
157    }
158}
159
160#[derive(Clone, Debug, Default)]
161pub(super) struct SymbolicAbiState {
162    constraints: Vec<SymBoolExpr>,
163    positional_dynamic_index: usize,
164}
165
166#[derive(Debug)]
167pub(super) struct SymbolicAbiBuilder<'a, 'cx> {
168    config: &'a SymbolicConfig,
169    cx: &'cx mut SymCx,
170}
171
172impl<'a, 'cx> SymbolicAbiBuilder<'a, 'cx> {
173    /// Constructs a new instance.
174    pub(super) const fn new(config: &'a SymbolicConfig, cx: &'cx mut SymCx) -> Self {
175        Self { config, cx }
176    }
177
178    pub(super) fn value(
179        &mut self,
180        state: &mut SymbolicAbiState,
181        name: String,
182        aliases: Vec<String>,
183        ty: &DynSolType,
184    ) -> Result<SymbolicAbiValue, SymbolicError> {
185        Ok(match ty {
186            DynSolType::Bool => {
187                let word = self.fresh_word(&name);
188                state.constraints.push(SymBoolExpr::cmp_word_const(
189                    self.cx,
190                    SymCmpOp::Ult,
191                    &word,
192                    U256::from(2),
193                ));
194                SymbolicAbiValue::Bool { word }
195            }
196            DynSolType::Uint(bits) => {
197                let word = self.fresh_word(&name);
198                self.constrain_uint(state, &word, *bits);
199                SymbolicAbiValue::Uint { bits: *bits, word }
200            }
201            DynSolType::Int(bits) => {
202                let word = self.fresh_word(&name);
203                self.constrain_int(state, &word, *bits);
204                SymbolicAbiValue::Int { bits: *bits, word }
205            }
206            DynSolType::FixedBytes(size) => {
207                let bytes = (0..*size)
208                    .map(|idx| self.fresh_byte(state, &format!("{name}_{idx}"), false))
209                    .collect();
210                SymbolicAbiValue::FixedBytes { bytes: SymBytes::exprs(self.cx, bytes), size: *size }
211            }
212            DynSolType::Address => {
213                let word = self.fresh_word(&name);
214                self.constrain_uint(state, &word, 160);
215                SymbolicAbiValue::Address { word }
216            }
217            DynSolType::Function => {
218                return Err(SymbolicError::UnsupportedAbi("function".to_string()));
219            }
220            DynSolType::Bytes => {
221                let len = self.next_dynamic_length(state, &name, &aliases, DynamicKind::Bytes)?;
222                let bytes = (0..len)
223                    .map(|idx| self.fresh_byte(state, &format!("{name}_{idx}"), false))
224                    .collect();
225                SymbolicAbiValue::Bytes {
226                    len: SymExpr::constant(self.cx, U256::from(len)),
227                    bytes: SymBytes::exprs(self.cx, bytes),
228                }
229            }
230            DynSolType::String => {
231                let len = self.next_dynamic_length(state, &name, &aliases, DynamicKind::String)?;
232                let bytes = (0..len)
233                    .map(|idx| self.fresh_byte(state, &format!("{name}_{idx}"), true))
234                    .collect();
235                SymbolicAbiValue::String { bytes: SymBytes::exprs(self.cx, bytes) }
236            }
237            DynSolType::Array(inner) => {
238                let len = self.next_dynamic_length(state, &name, &aliases, DynamicKind::Array)?;
239                SymbolicAbiValue::Array {
240                    elements: (0..len)
241                        .map(|idx| {
242                            self.value(
243                                state,
244                                format!("{name}_{idx}"),
245                                child_aliases(&aliases, idx),
246                                inner,
247                            )
248                        })
249                        .collect::<Result<Vec<_>, _>>()?,
250                }
251            }
252            DynSolType::FixedArray(inner, len) => SymbolicAbiValue::FixedArray {
253                elements: (0..*len)
254                    .map(|idx| {
255                        self.value(
256                            state,
257                            format!("{name}_{idx}"),
258                            child_aliases(&aliases, idx),
259                            inner,
260                        )
261                    })
262                    .collect::<Result<Vec<_>, _>>()?,
263            },
264            DynSolType::Tuple(types) => SymbolicAbiValue::Tuple {
265                elements: types
266                    .iter()
267                    .enumerate()
268                    .map(|(idx, ty)| {
269                        self.value(state, format!("{name}_{idx}"), child_aliases(&aliases, idx), ty)
270                    })
271                    .collect::<Result<Vec<_>, _>>()?,
272            },
273            DynSolType::CustomStruct { tuple, .. } => SymbolicAbiValue::Tuple {
274                elements: tuple
275                    .iter()
276                    .enumerate()
277                    .map(|(idx, ty)| {
278                        self.value(state, format!("{name}_{idx}"), child_aliases(&aliases, idx), ty)
279                    })
280                    .collect::<Result<Vec<_>, _>>()?,
281            },
282        })
283    }
284
285    pub(super) fn value_variants(
286        &mut self,
287        state: SymbolicAbiState,
288        name: String,
289        aliases: Vec<String>,
290        ty: &DynSolType,
291    ) -> Result<Vec<(SymbolicAbiState, SymbolicAbiValue)>, SymbolicError> {
292        Ok(match ty {
293            DynSolType::Bytes => {
294                let mut state = state;
295                let lengths = self.next_dynamic_length_options(
296                    &mut state,
297                    &name,
298                    &aliases,
299                    DynamicKind::Bytes,
300                )?;
301                let limit = calldata_variant_limit(self.config);
302                let mut variants = Vec::new();
303                for len in lengths {
304                    let mut state = state.clone();
305                    let bytes = (0..len as usize)
306                        .map(|idx| self.fresh_byte(&mut state, &format!("{name}_{idx}"), false))
307                        .collect();
308                    let value = SymbolicAbiValue::Bytes {
309                        len: SymExpr::constant(self.cx, U256::from(len)),
310                        bytes: SymBytes::exprs(self.cx, bytes),
311                    };
312                    push_variant(&mut variants, (state, value), limit)?;
313                }
314                variants
315            }
316            DynSolType::String => {
317                let mut state = state;
318                let lengths = self.next_dynamic_length_options(
319                    &mut state,
320                    &name,
321                    &aliases,
322                    DynamicKind::String,
323                )?;
324                let limit = calldata_variant_limit(self.config);
325                let mut variants = Vec::new();
326                for len in lengths {
327                    let mut state = state.clone();
328                    let bytes = (0..len as usize)
329                        .map(|idx| self.fresh_byte(&mut state, &format!("{name}_{idx}"), true))
330                        .collect();
331                    let value = SymbolicAbiValue::String { bytes: SymBytes::exprs(self.cx, bytes) };
332                    push_variant(&mut variants, (state, value), limit)?;
333                }
334                variants
335            }
336            DynSolType::Array(inner) => {
337                let mut state = state;
338                let lengths = self.next_dynamic_length_options(
339                    &mut state,
340                    &name,
341                    &aliases,
342                    DynamicKind::Array,
343                )?;
344                let limit = calldata_variant_limit(self.config);
345                let mut variants = Vec::new();
346                for len in lengths {
347                    for (state, elements) in self.array_elements_variants(
348                        state.clone(),
349                        &name,
350                        &aliases,
351                        inner,
352                        len as usize,
353                    )? {
354                        push_variant(
355                            &mut variants,
356                            (state, SymbolicAbiValue::Array { elements }),
357                            limit,
358                        )?;
359                    }
360                }
361                variants
362            }
363            DynSolType::FixedArray(inner, len) => self
364                .array_elements_variants(state, &name, &aliases, inner, *len)
365                .map(|variants| {
366                    variants
367                        .into_iter()
368                        .map(|(state, elements)| (state, SymbolicAbiValue::FixedArray { elements }))
369                        .collect()
370                })?,
371            DynSolType::Tuple(types) => self
372                .tuple_elements_variants(state, &name, &aliases, types)?
373                .into_iter()
374                .map(|(state, elements)| (state, SymbolicAbiValue::Tuple { elements }))
375                .collect(),
376            DynSolType::CustomStruct { tuple, .. } => self
377                .tuple_elements_variants(state, &name, &aliases, tuple)?
378                .into_iter()
379                .map(|(state, elements)| (state, SymbolicAbiValue::Tuple { elements }))
380                .collect(),
381            _ => {
382                let mut state = state;
383                let value = self.value(&mut state, name, aliases, ty)?;
384                vec![(state, value)]
385            }
386        })
387    }
388
389    pub(super) fn array_elements_variants(
390        &mut self,
391        state: SymbolicAbiState,
392        name: &str,
393        aliases: &[String],
394        inner: &DynSolType,
395        len: usize,
396    ) -> Result<Vec<(SymbolicAbiState, Vec<SymbolicAbiValue>)>, SymbolicError> {
397        let limit = calldata_variant_limit(self.config);
398        let mut variants = vec![(state, Vec::with_capacity(len))];
399        for idx in 0..len {
400            let mut next_variants = Vec::new();
401            for (state, elements) in variants {
402                for (state, value) in self.value_variants(
403                    state,
404                    format!("{name}_{idx}"),
405                    child_aliases(aliases, idx),
406                    inner,
407                )? {
408                    let mut elements = elements.clone();
409                    elements.push(value);
410                    push_variant(&mut next_variants, (state, elements), limit)?;
411                }
412            }
413            variants = next_variants;
414        }
415        Ok(variants)
416    }
417
418    pub(super) fn tuple_elements_variants(
419        &mut self,
420        state: SymbolicAbiState,
421        name: &str,
422        aliases: &[String],
423        types: &[DynSolType],
424    ) -> Result<Vec<(SymbolicAbiState, Vec<SymbolicAbiValue>)>, SymbolicError> {
425        let limit = calldata_variant_limit(self.config);
426        let mut variants = vec![(state, Vec::with_capacity(types.len()))];
427        for (idx, ty) in types.iter().enumerate() {
428            let mut next_variants = Vec::new();
429            for (state, elements) in variants {
430                for (state, value) in self.value_variants(
431                    state,
432                    format!("{name}_{idx}"),
433                    child_aliases(aliases, idx),
434                    ty,
435                )? {
436                    let mut elements = elements.clone();
437                    elements.push(value);
438                    push_variant(&mut next_variants, (state, elements), limit)?;
439                }
440            }
441            variants = next_variants;
442        }
443        Ok(variants)
444    }
445
446    pub(super) fn fresh_word(&mut self, name: &str) -> SymExpr {
447        SymExpr::var(self.cx, name)
448    }
449
450    pub(super) fn fresh_byte(
451        &mut self,
452        state: &mut SymbolicAbiState,
453        name: &str,
454        printable: bool,
455    ) -> SymExpr {
456        let word = self.fresh_word(name);
457        state.constraints.push(SymBoolExpr::cmp_word_const(
458            self.cx,
459            SymCmpOp::Ult,
460            &word,
461            U256::from(256),
462        ));
463        if printable {
464            state.constraints.push(SymBoolExpr::cmp_word_const(
465                self.cx,
466                SymCmpOp::Uge,
467                &word,
468                U256::from(0x20),
469            ));
470            state.constraints.push(SymBoolExpr::cmp_word_const(
471                self.cx,
472                SymCmpOp::Ule,
473                &word,
474                U256::from(0x7e),
475            ));
476        }
477        word
478    }
479
480    pub(super) fn next_dynamic_length(
481        &self,
482        state: &mut SymbolicAbiState,
483        name: &str,
484        aliases: &[String],
485        kind: DynamicKind,
486    ) -> Result<usize, SymbolicError> {
487        Ok(first_dynamic_length(
488            &self.next_dynamic_length_options(state, name, aliases, kind)?,
489            "symbolic dynamic length",
490        )? as usize)
491    }
492
493    pub(super) fn next_dynamic_length_options(
494        &self,
495        state: &mut SymbolicAbiState,
496        name: &str,
497        aliases: &[String],
498        kind: DynamicKind,
499    ) -> Result<Vec<u32>, SymbolicError> {
500        let named_lengths = std::iter::once(name)
501            .chain(aliases.iter().map(String::as_str))
502            .find_map(|name| self.config.dynamic_lengths.get(name));
503
504        let lengths = if let Some(lengths) = named_lengths {
505            lengths.clone()
506        } else if let Some(lengths) = kind.default_lengths(self.config) {
507            lengths.to_vec()
508        } else if let Some(len) =
509            self.config.array_lengths.get(state.positional_dynamic_index).copied()
510        {
511            state.positional_dynamic_index += 1;
512            vec![len]
513        } else {
514            vec![self.config.default_dynamic_length]
515        };
516
517        if lengths.is_empty() {
518            return Err(SymbolicError::UnsupportedAbi(
519                "symbolic dynamic length set must not be empty".to_string(),
520            ));
521        }
522        for len in &lengths {
523            if *len > self.config.max_dynamic_length {
524                return Err(SymbolicError::UnsupportedAbi(format!(
525                    "symbolic {} length {len} exceeds max_dynamic_length {}",
526                    kind.name(),
527                    self.config.max_dynamic_length
528                )));
529            }
530        }
531        Ok(lengths)
532    }
533
534    pub(super) fn constrain_uint(
535        &mut self,
536        state: &mut SymbolicAbiState,
537        word: &SymExpr,
538        bits: usize,
539    ) {
540        if bits < 256 {
541            state.constraints.push(SymBoolExpr::cmp_word_const(
542                self.cx,
543                SymCmpOp::Ult,
544                word,
545                U256::from(1) << bits,
546            ));
547        }
548    }
549
550    pub(super) fn constrain_int(
551        &mut self,
552        state: &mut SymbolicAbiState,
553        word: &SymExpr,
554        bits: usize,
555    ) {
556        if bits < 256 {
557            let byte_index = U256::from(bits / 8 - 1);
558            let signextended = signextend_word(self.cx, byte_index, word.clone());
559            state.constraints.push(SymBoolExpr::eq(self.cx, word.clone(), signextended));
560        }
561    }
562
563    pub(super) fn encode_sequence<'v>(
564        &mut self,
565        values: impl IntoIterator<Item = &'v SymbolicAbiValue>,
566    ) -> SymBytes {
567        encode_sequence(self.cx, values)
568    }
569}
570
571/// Validates that positional ABI length config can be consumed by at least one expanded variant.
572fn validate_positional_dynamic_lengths(
573    config: &SymbolicConfig,
574    max_positional_dynamic_index: usize,
575) -> Result<(), SymbolicError> {
576    if config.array_lengths.len() > max_positional_dynamic_index {
577        return Err(SymbolicError::UnsupportedAbi(format!(
578            "symbolic.array_lengths has {} entries but ABI used at most {} positional dynamic leaves",
579            config.array_lengths.len(),
580            max_positional_dynamic_index
581        )));
582    }
583    Ok(())
584}
585
586/// Returns the maximum number of calldata variants allowed during ABI expansion.
587fn calldata_variant_limit(config: &SymbolicConfig) -> usize {
588    config.path_width().max(1) as usize
589}
590
591/// Adds one expansion variant while enforcing the configured symbolic path-width budget.
592fn push_variant<T>(variants: &mut Vec<T>, variant: T, limit: usize) -> Result<(), SymbolicError> {
593    if variants.len() >= limit {
594        return Err(SymbolicError::CalldataVariantLimit(limit));
595    }
596    variants.push(variant);
597    Ok(())
598}
599
600#[derive(Clone, Copy)]
601pub(super) enum DynamicKind {
602    Array,
603    Bytes,
604    String,
605}
606
607impl DynamicKind {
608    pub(super) const fn name(self) -> &'static str {
609        match self {
610            Self::Array => "array",
611            Self::Bytes => "bytes",
612            Self::String => "string",
613        }
614    }
615
616    pub(super) fn default_lengths(self, config: &SymbolicConfig) -> Option<&[u32]> {
617        match self {
618            Self::Array if !config.default_array_lengths.is_empty() => {
619                Some(&config.default_array_lengths)
620            }
621            Self::Bytes | Self::String if !config.default_bytes_lengths.is_empty() => {
622                Some(&config.default_bytes_lengths)
623            }
624            _ => None,
625        }
626    }
627}
628
629pub(super) fn first_dynamic_length(lengths: &[u32], field: &str) -> Result<u32, SymbolicError> {
630    lengths
631        .first()
632        .copied()
633        .ok_or_else(|| SymbolicError::UnsupportedAbi(format!("{field} must not be empty")))
634}
635
636pub(super) fn child_aliases(aliases: &[String], idx: usize) -> Vec<String> {
637    aliases.iter().map(|alias| format!("{alias}_{idx}")).collect()
638}
639
640#[derive(Clone, Debug)]
641pub(super) enum SymbolicAbiValue {
642    Bool { word: SymExpr },
643    Uint { bits: usize, word: SymExpr },
644    Int { bits: usize, word: SymExpr },
645    FixedBytes { bytes: SymBytes, size: usize },
646    Address { word: SymExpr },
647    Bytes { len: SymExpr, bytes: SymBytes },
648    String { bytes: SymBytes },
649    Array { elements: Vec<Self> },
650    FixedArray { elements: Vec<Self> },
651    Tuple { elements: Vec<Self> },
652}
653
654impl SymbolicAbiValue {
655    /// Returns whether `is_dynamic` holds.
656    pub(super) fn is_dynamic(&self) -> bool {
657        match self {
658            Self::Bool { .. }
659            | Self::Uint { .. }
660            | Self::Int { .. }
661            | Self::FixedBytes { .. }
662            | Self::Address { .. } => false,
663            Self::Bytes { .. } | Self::String { .. } | Self::Array { .. } => true,
664            Self::FixedArray { elements } | Self::Tuple { elements } => {
665                elements.iter().any(Self::is_dynamic)
666            }
667        }
668    }
669
670    pub(super) fn head_size(&self) -> usize {
671        if self.is_dynamic() {
672            32
673        } else {
674            match self {
675                Self::Bool { .. }
676                | Self::Uint { .. }
677                | Self::Int { .. }
678                | Self::FixedBytes { .. }
679                | Self::Address { .. } => 32,
680                Self::FixedArray { elements } | Self::Tuple { elements } => {
681                    elements.iter().map(Self::head_size).sum()
682                }
683                Self::Bytes { .. } | Self::String { .. } | Self::Array { .. } => 32,
684            }
685        }
686    }
687
688    pub(super) fn model_value(
689        &self,
690        cx: &mut SymCx,
691        model: &(impl SymbolicModelLookup + ?Sized),
692    ) -> Result<DynSolValue, SymbolicError> {
693        Ok(match self {
694            Self::Bool { word } => DynSolValue::Bool(!word.eval_model(model)?.is_zero()),
695            Self::Uint { bits, word } => {
696                DynSolValue::Uint(mask_bits(word.eval_model(model)?, *bits), *bits)
697            }
698            Self::Int { bits, word } => {
699                DynSolValue::Int(I256::from_raw(word.eval_model(model)?), *bits)
700            }
701            Self::FixedBytes { bytes, size } => {
702                let mut word = [0u8; 32];
703                for (idx, out) in word.iter_mut().enumerate().take(bytes.len()) {
704                    *out = bytes.byte(cx, idx).eval_model(model)?.to::<u8>();
705                }
706                DynSolValue::FixedBytes(B256::from(word), *size)
707            }
708            Self::Address { word } => {
709                DynSolValue::Address(word_to_address(word.eval_model(model)?))
710            }
711            Self::Bytes { len, bytes } => {
712                let len = len.eval_model(model)?;
713                let len = usize::try_from(len)
714                    .ok()
715                    .filter(|len| *len <= bytes.len())
716                    .ok_or_else(|| SymbolicError::Solver("invalid symbolic bytes length".into()))?;
717                let mut bytes = bytes.eval_model(cx, model)?;
718                bytes.truncate(len);
719                DynSolValue::Bytes(bytes)
720            }
721            Self::String { bytes } => {
722                let bytes = bytes.eval_model(cx, model)?;
723                let value = String::from_utf8(bytes).map_err(|err| {
724                    SymbolicError::Solver(format!("invalid symbolic string model: {err}"))
725                })?;
726                DynSolValue::String(value)
727            }
728            Self::Array { elements } => DynSolValue::Array(
729                elements
730                    .iter()
731                    .map(|value| value.model_value(cx, model))
732                    .collect::<Result<Vec<_>, _>>()?,
733            ),
734            Self::FixedArray { elements } => DynSolValue::FixedArray(
735                elements
736                    .iter()
737                    .map(|value| value.model_value(cx, model))
738                    .collect::<Result<Vec<_>, _>>()?,
739            ),
740            Self::Tuple { elements } => DynSolValue::Tuple(
741                elements
742                    .iter()
743                    .map(|value| value.model_value(cx, model))
744                    .collect::<Result<Vec<_>, _>>()?,
745            ),
746        })
747    }
748
749    pub(super) fn seed_model_value(
750        &self,
751        cx: &mut SymCx,
752        model: &mut SymbolicModel,
753        value: &DynSolValue,
754    ) -> bool {
755        match (self, value) {
756            (Self::Bool { word }, DynSolValue::Bool(value)) => {
757                word.assign_model_value(model, U256::from(*value as u8))
758            }
759            (Self::Uint { bits, word }, DynSolValue::Uint(value, value_bits))
760                if bits == value_bits =>
761            {
762                word.assign_model_value(model, *value)
763            }
764            (Self::Int { bits, word }, DynSolValue::Int(value, value_bits))
765                if bits == value_bits =>
766            {
767                word.assign_model_value(model, value.into_raw())
768            }
769            (Self::FixedBytes { bytes, size }, DynSolValue::FixedBytes(value, value_size))
770                if size == value_size =>
771            {
772                seed_model_bytes(cx, model, bytes, &value.as_slice()[..*size])
773            }
774            (Self::Address { word }, DynSolValue::Address(value)) => {
775                word.assign_model_value(model, address_word(*value))
776            }
777            (Self::Bytes { len, bytes }, DynSolValue::Bytes(value)) => {
778                len.assign_model_value(model, U256::from(value.len()))
779                    && seed_model_bytes(cx, model, bytes, value)
780            }
781            (Self::String { bytes }, DynSolValue::String(value)) => {
782                seed_model_bytes(cx, model, bytes, value.as_bytes())
783            }
784            (Self::Array { elements }, DynSolValue::Array(values))
785            | (Self::FixedArray { elements }, DynSolValue::FixedArray(values))
786            | (Self::Tuple { elements }, DynSolValue::Tuple(values)) => {
787                seed_model_elements(cx, model, elements, values)
788            }
789            (Self::Tuple { elements }, DynSolValue::CustomStruct { tuple, .. }) => {
790                seed_model_elements(cx, model, elements, tuple)
791            }
792            _ => false,
793        }
794    }
795}
796
797fn seed_model_elements(
798    cx: &mut SymCx,
799    model: &mut SymbolicModel,
800    elements: &[SymbolicAbiValue],
801    values: &[DynSolValue],
802) -> bool {
803    elements.len() == values.len()
804        && elements
805            .iter()
806            .zip(values)
807            .all(|(element, value)| element.seed_model_value(cx, model, value))
808}
809
810fn seed_model_bytes(
811    cx: &mut SymCx,
812    model: &mut SymbolicModel,
813    bytes: &SymBytes,
814    value: &[u8],
815) -> bool {
816    bytes.len() == value.len()
817        && value
818            .iter()
819            .enumerate()
820            .all(|(idx, byte)| bytes.byte(cx, idx).assign_model_value(model, U256::from(*byte)))
821}
822
823pub(super) fn encode_sequence<'a>(
824    cx: &mut SymCx,
825    values: impl IntoIterator<Item = &'a SymbolicAbiValue>,
826) -> SymBytes {
827    let values = values.into_iter().collect::<Vec<_>>();
828    let head_size = values.iter().map(|value| value.head_size()).sum::<usize>();
829    let mut head = Vec::with_capacity(values.len());
830    let mut tail = Vec::new();
831    let mut tail_len = 0usize;
832
833    for value in values {
834        if value.is_dynamic() {
835            let offset = SymExpr::constant(cx, U256::from(head_size + tail_len));
836            head.push(offset.into_bytes(cx));
837            let body = encode_dynamic_body(cx, value);
838            tail_len += body.len();
839            tail.push(body);
840        } else {
841            head.push(encode_static(cx, value));
842        }
843    }
844
845    SymBytes::concat(cx, head.into_iter().chain(tail))
846}
847
848fn encode_static(cx: &mut SymCx, value: &SymbolicAbiValue) -> SymBytes {
849    match value {
850        SymbolicAbiValue::Bool { word }
851        | SymbolicAbiValue::Uint { word, .. }
852        | SymbolicAbiValue::Int { word, .. }
853        | SymbolicAbiValue::Address { word } => word.clone().into_bytes(cx),
854        SymbolicAbiValue::FixedBytes { bytes, .. } => {
855            let padding = SymBytes::concrete(cx, vec![0; 32usize.saturating_sub(bytes.len())]);
856            SymBytes::concat(cx, [bytes.clone(), padding])
857        }
858        SymbolicAbiValue::FixedArray { elements } | SymbolicAbiValue::Tuple { elements } => {
859            encode_sequence(cx, elements.iter())
860        }
861        SymbolicAbiValue::Bytes { .. }
862        | SymbolicAbiValue::String { .. }
863        | SymbolicAbiValue::Array { .. } => unreachable!("dynamic ABI value encoded as static"),
864    }
865}
866
867fn encode_dynamic_body(cx: &mut SymCx, value: &SymbolicAbiValue) -> SymBytes {
868    match value {
869        SymbolicAbiValue::Bytes { len, bytes } => {
870            encode_packed_bytes_with_len(cx, len.clone(), bytes)
871        }
872        SymbolicAbiValue::String { bytes } => {
873            let len = SymExpr::constant(cx, U256::from(bytes.len()));
874            encode_packed_bytes_with_len(cx, len, bytes)
875        }
876        SymbolicAbiValue::Array { elements } => {
877            let len = SymExpr::constant(cx, U256::from(elements.len()));
878            let len = len.into_bytes(cx);
879            let elements = encode_sequence(cx, elements.iter());
880            SymBytes::concat(cx, [len, elements])
881        }
882        SymbolicAbiValue::FixedArray { elements } | SymbolicAbiValue::Tuple { elements } => {
883            encode_sequence(cx, elements.iter())
884        }
885        SymbolicAbiValue::Bool { .. }
886        | SymbolicAbiValue::Uint { .. }
887        | SymbolicAbiValue::Int { .. }
888        | SymbolicAbiValue::FixedBytes { .. }
889        | SymbolicAbiValue::Address { .. } => unreachable!("static ABI value encoded as dynamic"),
890    }
891}
892
893pub(super) fn encode_packed_bytes_with_len(
894    cx: &mut SymCx,
895    len: SymExpr,
896    bytes: &SymBytes,
897) -> SymBytes {
898    let padded_len = bytes.len().next_multiple_of(32);
899    let len = len.into_bytes(cx);
900    let padding = SymBytes::concrete(cx, vec![0; padded_len - bytes.len()]);
901    SymBytes::concat(cx, [len, bytes.clone(), padding])
902}
foundry_evm_symbolic/abi.rs

foundry_evm_symbolic/
abi.rs
