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        let symbol = self.cx.intern(name);
448        self.cx.mark_replayable_input(symbol);
449        SymExpr::get_var(self.cx, symbol)
450    }
451
452    pub(super) fn fresh_byte(
453        &mut self,
454        state: &mut SymbolicAbiState,
455        name: &str,
456        printable: bool,
457    ) -> SymExpr {
458        let word = self.fresh_word(name);
459        state.constraints.push(SymBoolExpr::cmp_word_const(
460            self.cx,
461            SymCmpOp::Ult,
462            &word,
463            U256::from(256),
464        ));
465        if printable {
466            state.constraints.push(SymBoolExpr::cmp_word_const(
467                self.cx,
468                SymCmpOp::Uge,
469                &word,
470                U256::from(0x20),
471            ));
472            state.constraints.push(SymBoolExpr::cmp_word_const(
473                self.cx,
474                SymCmpOp::Ule,
475                &word,
476                U256::from(0x7e),
477            ));
478        }
479        word
480    }
481
482    pub(super) fn next_dynamic_length(
483        &self,
484        state: &mut SymbolicAbiState,
485        name: &str,
486        aliases: &[String],
487        kind: DynamicKind,
488    ) -> Result<usize, SymbolicError> {
489        Ok(first_dynamic_length(
490            &self.next_dynamic_length_options(state, name, aliases, kind)?,
491            "symbolic dynamic length",
492        )? as usize)
493    }
494
495    pub(super) fn next_dynamic_length_options(
496        &self,
497        state: &mut SymbolicAbiState,
498        name: &str,
499        aliases: &[String],
500        kind: DynamicKind,
501    ) -> Result<Vec<u32>, SymbolicError> {
502        let named_lengths = std::iter::once(name)
503            .chain(aliases.iter().map(String::as_str))
504            .find_map(|name| self.config.dynamic_lengths.get(name));
505
506        let lengths = if let Some(lengths) = named_lengths {
507            lengths.clone()
508        } else if let Some(lengths) = kind.default_lengths(self.config) {
509            lengths.to_vec()
510        } else if let Some(len) =
511            self.config.array_lengths.get(state.positional_dynamic_index).copied()
512        {
513            state.positional_dynamic_index += 1;
514            vec![len]
515        } else {
516            vec![self.config.default_dynamic_length]
517        };
518
519        if lengths.is_empty() {
520            return Err(SymbolicError::UnsupportedAbi(
521                "symbolic dynamic length set must not be empty".to_string(),
522            ));
523        }
524        for len in &lengths {
525            if *len > self.config.max_dynamic_length {
526                return Err(SymbolicError::UnsupportedAbi(format!(
527                    "symbolic {} length {len} exceeds max_dynamic_length {}",
528                    kind.name(),
529                    self.config.max_dynamic_length
530                )));
531            }
532        }
533        Ok(lengths)
534    }
535
536    pub(super) fn constrain_uint(
537        &mut self,
538        state: &mut SymbolicAbiState,
539        word: &SymExpr,
540        bits: usize,
541    ) {
542        if bits < 256 {
543            state.constraints.push(SymBoolExpr::cmp_word_const(
544                self.cx,
545                SymCmpOp::Ult,
546                word,
547                U256::from(1) << bits,
548            ));
549        }
550    }
551
552    pub(super) fn constrain_int(
553        &mut self,
554        state: &mut SymbolicAbiState,
555        word: &SymExpr,
556        bits: usize,
557    ) {
558        if bits < 256 {
559            let byte_index = U256::from(bits / 8 - 1);
560            let signextended = signextend_word(self.cx, byte_index, word.clone());
561            state.constraints.push(SymBoolExpr::eq(self.cx, word.clone(), signextended));
562        }
563    }
564
565    pub(super) fn encode_sequence<'v>(
566        &mut self,
567        values: impl IntoIterator<Item = &'v SymbolicAbiValue>,
568    ) -> SymBytes {
569        encode_sequence(self.cx, values)
570    }
571}
572
573/// Validates that positional ABI length config can be consumed by at least one expanded variant.
574fn validate_positional_dynamic_lengths(
575    config: &SymbolicConfig,
576    max_positional_dynamic_index: usize,
577) -> Result<(), SymbolicError> {
578    if config.array_lengths.len() > max_positional_dynamic_index {
579        return Err(SymbolicError::UnsupportedAbi(format!(
580            "symbolic.array_lengths has {} entries but ABI used at most {} positional dynamic leaves",
581            config.array_lengths.len(),
582            max_positional_dynamic_index
583        )));
584    }
585    Ok(())
586}
587
588/// Returns the maximum number of calldata variants allowed during ABI expansion.
589fn calldata_variant_limit(config: &SymbolicConfig) -> usize {
590    config.path_width().max(1) as usize
591}
592
593/// Adds one expansion variant while enforcing the configured symbolic path-width budget.
594fn push_variant<T>(variants: &mut Vec<T>, variant: T, limit: usize) -> Result<(), SymbolicError> {
595    if variants.len() >= limit {
596        return Err(SymbolicError::CalldataVariantLimit(limit));
597    }
598    variants.push(variant);
599    Ok(())
600}
601
602#[derive(Clone, Copy)]
603pub(super) enum DynamicKind {
604    Array,
605    Bytes,
606    String,
607}
608
609impl DynamicKind {
610    pub(super) const fn name(self) -> &'static str {
611        match self {
612            Self::Array => "array",
613            Self::Bytes => "bytes",
614            Self::String => "string",
615        }
616    }
617
618    pub(super) fn default_lengths(self, config: &SymbolicConfig) -> Option<&[u32]> {
619        match self {
620            Self::Array if !config.default_array_lengths.is_empty() => {
621                Some(&config.default_array_lengths)
622            }
623            Self::Bytes | Self::String if !config.default_bytes_lengths.is_empty() => {
624                Some(&config.default_bytes_lengths)
625            }
626            _ => None,
627        }
628    }
629}
630
631pub(super) fn first_dynamic_length(lengths: &[u32], field: &str) -> Result<u32, SymbolicError> {
632    lengths
633        .first()
634        .copied()
635        .ok_or_else(|| SymbolicError::UnsupportedAbi(format!("{field} must not be empty")))
636}
637
638pub(super) fn child_aliases(aliases: &[String], idx: usize) -> Vec<String> {
639    aliases.iter().map(|alias| format!("{alias}_{idx}")).collect()
640}
641
642#[derive(Clone, Debug)]
643pub(super) enum SymbolicAbiValue {
644    Bool { word: SymExpr },
645    Uint { bits: usize, word: SymExpr },
646    Int { bits: usize, word: SymExpr },
647    FixedBytes { bytes: SymBytes, size: usize },
648    Address { word: SymExpr },
649    Bytes { len: SymExpr, bytes: SymBytes },
650    String { bytes: SymBytes },
651    Array { elements: Vec<Self> },
652    FixedArray { elements: Vec<Self> },
653    Tuple { elements: Vec<Self> },
654}
655
656impl SymbolicAbiValue {
657    /// Returns whether `is_dynamic` holds.
658    pub(super) fn is_dynamic(&self) -> bool {
659        match self {
660            Self::Bool { .. }
661            | Self::Uint { .. }
662            | Self::Int { .. }
663            | Self::FixedBytes { .. }
664            | Self::Address { .. } => false,
665            Self::Bytes { .. } | Self::String { .. } | Self::Array { .. } => true,
666            Self::FixedArray { elements } | Self::Tuple { elements } => {
667                elements.iter().any(Self::is_dynamic)
668            }
669        }
670    }
671
672    pub(super) fn head_size(&self) -> usize {
673        if self.is_dynamic() {
674            32
675        } else {
676            match self {
677                Self::Bool { .. }
678                | Self::Uint { .. }
679                | Self::Int { .. }
680                | Self::FixedBytes { .. }
681                | Self::Address { .. } => 32,
682                Self::FixedArray { elements } | Self::Tuple { elements } => {
683                    elements.iter().map(Self::head_size).sum()
684                }
685                Self::Bytes { .. } | Self::String { .. } | Self::Array { .. } => 32,
686            }
687        }
688    }
689
690    pub(super) fn model_value(
691        &self,
692        cx: &mut SymCx,
693        model: &(impl SymbolicModelLookup + ?Sized),
694    ) -> Result<DynSolValue, SymbolicError> {
695        Ok(match self {
696            Self::Bool { word } => DynSolValue::Bool(!word.eval_model(model)?.is_zero()),
697            Self::Uint { bits, word } => {
698                DynSolValue::Uint(mask_bits(word.eval_model(model)?, *bits), *bits)
699            }
700            Self::Int { bits, word } => {
701                DynSolValue::Int(I256::from_raw(word.eval_model(model)?), *bits)
702            }
703            Self::FixedBytes { bytes, size } => {
704                let mut word = [0u8; 32];
705                for (idx, out) in word.iter_mut().enumerate().take(bytes.len()) {
706                    *out = bytes.byte(cx, idx).eval_model(model)?.to::<u8>();
707                }
708                DynSolValue::FixedBytes(B256::from(word), *size)
709            }
710            Self::Address { word } => {
711                DynSolValue::Address(word_to_address(word.eval_model(model)?))
712            }
713            Self::Bytes { len, bytes } => {
714                let len = len.eval_model(model)?;
715                let len = usize::try_from(len)
716                    .ok()
717                    .filter(|len| *len <= bytes.len())
718                    .ok_or_else(|| SymbolicError::Solver("invalid symbolic bytes length".into()))?;
719                let mut bytes = bytes.eval_model(cx, model)?;
720                bytes.truncate(len);
721                DynSolValue::Bytes(bytes)
722            }
723            Self::String { bytes } => {
724                let bytes = bytes.eval_model(cx, model)?;
725                let value = String::from_utf8(bytes).map_err(|err| {
726                    SymbolicError::Solver(format!("invalid symbolic string model: {err}"))
727                })?;
728                DynSolValue::String(value)
729            }
730            Self::Array { elements } => DynSolValue::Array(
731                elements
732                    .iter()
733                    .map(|value| value.model_value(cx, model))
734                    .collect::<Result<Vec<_>, _>>()?,
735            ),
736            Self::FixedArray { elements } => DynSolValue::FixedArray(
737                elements
738                    .iter()
739                    .map(|value| value.model_value(cx, model))
740                    .collect::<Result<Vec<_>, _>>()?,
741            ),
742            Self::Tuple { elements } => DynSolValue::Tuple(
743                elements
744                    .iter()
745                    .map(|value| value.model_value(cx, model))
746                    .collect::<Result<Vec<_>, _>>()?,
747            ),
748        })
749    }
750
751    pub(super) fn seed_model_value(
752        &self,
753        cx: &mut SymCx,
754        model: &mut SymbolicModel,
755        value: &DynSolValue,
756    ) -> bool {
757        match (self, value) {
758            (Self::Bool { word }, DynSolValue::Bool(value)) => {
759                word.assign_model_value(model, U256::from(*value as u8))
760            }
761            (Self::Uint { bits, word }, DynSolValue::Uint(value, value_bits))
762                if bits == value_bits =>
763            {
764                word.assign_model_value(model, *value)
765            }
766            (Self::Int { bits, word }, DynSolValue::Int(value, value_bits))
767                if bits == value_bits =>
768            {
769                word.assign_model_value(model, value.into_raw())
770            }
771            (Self::FixedBytes { bytes, size }, DynSolValue::FixedBytes(value, value_size))
772                if size == value_size =>
773            {
774                seed_model_bytes(cx, model, bytes, &value.as_slice()[..*size])
775            }
776            (Self::Address { word }, DynSolValue::Address(value)) => {
777                word.assign_model_value(model, address_word(*value))
778            }
779            (Self::Bytes { len, bytes }, DynSolValue::Bytes(value)) => {
780                len.assign_model_value(model, U256::from(value.len()))
781                    && seed_model_bytes(cx, model, bytes, value)
782            }
783            (Self::String { bytes }, DynSolValue::String(value)) => {
784                seed_model_bytes(cx, model, bytes, value.as_bytes())
785            }
786            (Self::Array { elements }, DynSolValue::Array(values))
787            | (Self::FixedArray { elements }, DynSolValue::FixedArray(values))
788            | (Self::Tuple { elements }, DynSolValue::Tuple(values)) => {
789                seed_model_elements(cx, model, elements, values)
790            }
791            (Self::Tuple { elements }, DynSolValue::CustomStruct { tuple, .. }) => {
792                seed_model_elements(cx, model, elements, tuple)
793            }
794            _ => false,
795        }
796    }
797}
798
799fn seed_model_elements(
800    cx: &mut SymCx,
801    model: &mut SymbolicModel,
802    elements: &[SymbolicAbiValue],
803    values: &[DynSolValue],
804) -> bool {
805    elements.len() == values.len()
806        && elements
807            .iter()
808            .zip(values)
809            .all(|(element, value)| element.seed_model_value(cx, model, value))
810}
811
812fn seed_model_bytes(
813    cx: &mut SymCx,
814    model: &mut SymbolicModel,
815    bytes: &SymBytes,
816    value: &[u8],
817) -> bool {
818    bytes.len() == value.len()
819        && value
820            .iter()
821            .enumerate()
822            .all(|(idx, byte)| bytes.byte(cx, idx).assign_model_value(model, U256::from(*byte)))
823}
824
825pub(super) fn encode_sequence<'a>(
826    cx: &mut SymCx,
827    values: impl IntoIterator<Item = &'a SymbolicAbiValue>,
828) -> SymBytes {
829    let values = values.into_iter().collect::<Vec<_>>();
830    let head_size = values.iter().map(|value| value.head_size()).sum::<usize>();
831    let mut head = Vec::with_capacity(values.len());
832    let mut tail = Vec::new();
833    let mut tail_len = 0usize;
834
835    for value in values {
836        if value.is_dynamic() {
837            let offset = SymExpr::constant(cx, U256::from(head_size + tail_len));
838            head.push(offset.into_bytes(cx));
839            let body = encode_dynamic_body(cx, value);
840            tail_len += body.len();
841            tail.push(body);
842        } else {
843            head.push(encode_static(cx, value));
844        }
845    }
846
847    SymBytes::concat(cx, head.into_iter().chain(tail))
848}
849
850fn encode_static(cx: &mut SymCx, value: &SymbolicAbiValue) -> SymBytes {
851    match value {
852        SymbolicAbiValue::Bool { word }
853        | SymbolicAbiValue::Uint { word, .. }
854        | SymbolicAbiValue::Int { word, .. }
855        | SymbolicAbiValue::Address { word } => word.clone().into_bytes(cx),
856        SymbolicAbiValue::FixedBytes { bytes, .. } => {
857            let padding = SymBytes::concrete(cx, vec![0; 32usize.saturating_sub(bytes.len())]);
858            SymBytes::concat(cx, [bytes.clone(), padding])
859        }
860        SymbolicAbiValue::FixedArray { elements } | SymbolicAbiValue::Tuple { elements } => {
861            encode_sequence(cx, elements.iter())
862        }
863        SymbolicAbiValue::Bytes { .. }
864        | SymbolicAbiValue::String { .. }
865        | SymbolicAbiValue::Array { .. } => unreachable!("dynamic ABI value encoded as static"),
866    }
867}
868
869fn encode_dynamic_body(cx: &mut SymCx, value: &SymbolicAbiValue) -> SymBytes {
870    match value {
871        SymbolicAbiValue::Bytes { len, bytes } => {
872            encode_packed_bytes_with_len(cx, len.clone(), bytes)
873        }
874        SymbolicAbiValue::String { bytes } => {
875            let len = SymExpr::constant(cx, U256::from(bytes.len()));
876            encode_packed_bytes_with_len(cx, len, bytes)
877        }
878        SymbolicAbiValue::Array { elements } => {
879            let len = SymExpr::constant(cx, U256::from(elements.len()));
880            let len = len.into_bytes(cx);
881            let elements = encode_sequence(cx, elements.iter());
882            SymBytes::concat(cx, [len, elements])
883        }
884        SymbolicAbiValue::FixedArray { elements } | SymbolicAbiValue::Tuple { elements } => {
885            encode_sequence(cx, elements.iter())
886        }
887        SymbolicAbiValue::Bool { .. }
888        | SymbolicAbiValue::Uint { .. }
889        | SymbolicAbiValue::Int { .. }
890        | SymbolicAbiValue::FixedBytes { .. }
891        | SymbolicAbiValue::Address { .. } => unreachable!("static ABI value encoded as dynamic"),
892    }
893}
894
895pub(super) fn encode_packed_bytes_with_len(
896    cx: &mut SymCx,
897    len: SymExpr,
898    bytes: &SymBytes,
899) -> SymBytes {
900    let padded_len = bytes.len().next_multiple_of(32);
901    let len = len.into_bytes(cx);
902    let padding = SymBytes::concrete(cx, vec![0; padded_len - bytes.len()]);
903    SymBytes::concat(cx, [len, bytes.clone(), padding])
904}
foundry_evm_symbolic/abi.rs

foundry_evm_symbolic/
abi.rs
