foundry_evm_symbolic/executor/
calls.rs

1use super::*;
2
3impl SymbolicExecutor {
4    /// Implements the `call` symbolic executor helper.
5    pub(super) fn call(
6        &mut self,
7        executor: &Executor<impl FoundryEvmNetwork>,
8        state: &mut PathState,
9        worklist: &mut VecDeque<PathState>,
10        completed_paths: &mut usize,
11        kind: CallKind,
12    ) -> Result<StepOutcome, SymbolicError> {
13        let pre_call_state = state.clone();
14        let call_pc = state.pc.saturating_sub(1);
15        let gas = state.stack.pop()?;
16        if gas.contains_gasleft() && !gas.is_raw_gasleft() {
17            return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
18        }
19        let target = state.stack.pop()?;
20        ensure_word_not_gasleft(&target)?;
21        let target_address = state.world.resolve_address(&target);
22        let value = match (kind, target_address) {
23            (CallKind::Call, Some(to)) if is_known_cheatcode(to) => {
24                let value = state.stack.pop()?;
25                let value = state.expect_constrained_word(value, "symbolic CALL value")?;
26                SymWord::Concrete(value)
27            }
28            (CallKind::Call, _) => state.stack.pop()?,
29            (CallKind::CallCode, _) => state.stack.pop()?,
30            (CallKind::StaticCall | CallKind::DelegateCall, _) => SymWord::zero(),
31        };
32        ensure_word_not_gasleft(&value)?;
33        let in_offset = state.stack.pop()?;
34        ensure_word_not_gasleft(&in_offset)?;
35        let in_size = state.stack.pop()?;
36        ensure_word_not_gasleft(&in_size)?;
37        let in_size = match state.constrained_usize(&in_size) {
38            Some(size) => BoundedCopySize::Concrete(size),
39            None if state.constrained_word(&in_size).is_some() => {
40                return Ok(StepOutcome::Revert);
41            }
42            None => {
43                let max_limit = self.config.max_calldata_bytes as usize;
44                let max_size = state
45                    .upper_bound_usize(&in_size)
46                    .filter(|size| *size <= max_limit)
47                    .map(Ok)
48                    .unwrap_or_else(|| {
49                        self.solver_upper_bound_usize(
50                            state,
51                            &in_size,
52                            max_limit,
53                            "symbolic CALL input size",
54                        )
55                    })?;
56                BoundedCopySize::Symbolic { size: in_size, max_size }
57            }
58        };
59        let out_offset = state.stack.pop()?;
60        ensure_word_not_gasleft(&out_offset)?;
61        let out_size = state.stack.pop()?;
62        ensure_word_not_gasleft(&out_size)?;
63        let out_size = match state.constrained_usize(&out_size) {
64            Some(size) => BoundedCopySize::Concrete(size),
65            None if state.constrained_word(&out_size).is_some() => {
66                return Ok(StepOutcome::Revert);
67            }
68            None => {
69                let max_limit = self.config.max_calldata_bytes as usize;
70                let max_size = state
71                    .upper_bound_usize(&out_size)
72                    .filter(|size| *size <= max_limit)
73                    .map(Ok)
74                    .unwrap_or_else(|| {
75                        self.solver_upper_bound_usize(
76                            state,
77                            &out_size,
78                            max_limit,
79                            "symbolic CALL output size",
80                        )
81                    })?;
82                BoundedCopySize::Symbolic { size: out_size, max_size }
83            }
84        };
85
86        if state.is_static && !state.constrained_word(&value).is_some_and(|value| value.is_zero()) {
87            state.return_data = SymReturnData::default();
88            return Ok(StepOutcome::Revert);
89        }
90
91        let call_input = call_input_from_memory(&state.memory, in_offset.clone(), &in_size);
92        if call_input.iter().any(SymWord::contains_gasleft) {
93            return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
94        }
95
96        if let Some(to) = target_address {
97            if self.branch_symbolic_function_mock_if_needed(
98                state,
99                worklist,
100                &pre_call_state,
101                call_pc,
102                to,
103                &call_input,
104            )? {
105                return Ok(StepOutcome::Forked);
106            }
107            let code_address = self.function_mock_target(state, to, &call_input)?.unwrap_or(to);
108            if self.branch_symbolic_call_value_if_needed(
109                state,
110                worklist,
111                &pre_call_state,
112                call_pc,
113                to,
114                code_address,
115                &value,
116                &gas,
117                &call_input,
118            )? {
119                return Ok(StepOutcome::Forked);
120            }
121            let concrete_value = state.constrained_word(&value);
122            if self.branch_symbolic_call_match_if_needed(
123                state,
124                worklist,
125                &pre_call_state,
126                call_pc,
127                to,
128                code_address,
129                concrete_value,
130                &gas,
131                &call_input,
132            )? {
133                return Ok(StepOutcome::Forked);
134            }
135            return self.call_concrete_target(
136                executor,
137                state,
138                worklist,
139                completed_paths,
140                kind,
141                to,
142                Some(target),
143                value,
144                gas,
145                in_offset,
146                in_size,
147                out_offset,
148                out_size,
149            );
150        }
151
152        self.call_symbolic_target(
153            executor,
154            state,
155            worklist,
156            completed_paths,
157            kind,
158            target,
159            value,
160            gas,
161            in_offset,
162            in_size,
163            out_offset,
164            out_size,
165        )
166    }
167
168    #[expect(clippy::too_many_arguments)]
169    /// Implements the `branch_symbolic_call_value_if_needed` symbolic executor helper.
170    pub(super) fn branch_symbolic_call_value_if_needed(
171        &mut self,
172        state: &mut PathState,
173        worklist: &mut VecDeque<PathState>,
174        pre_call_state: &PathState,
175        call_pc: usize,
176        to: Address,
177        code_address: Address,
178        value: &SymWord,
179        gas: &SymWord,
180        call_input: &[SymWord],
181    ) -> Result<bool, SymbolicError> {
182        if state.constrained_word(value).is_some() {
183            return Ok(false);
184        }
185
186        let mut candidates = BTreeSet::new();
187        for expected in &state.expected_calls {
188            let Some(expected_value) = expected.value else { continue };
189            if self
190                .expected_call_match_constraints(
191                    state,
192                    expected,
193                    to,
194                    Some(expected_value),
195                    gas,
196                    call_input,
197                )?
198                .is_some()
199            {
200                candidates.insert(expected_value);
201            }
202        }
203        for mock in &state.call_mocks {
204            let Some(mock_value) = mock.value else { continue };
205            if self
206                .call_mock_match_constraints(
207                    state,
208                    mock,
209                    code_address,
210                    Some(mock_value),
211                    call_input,
212                )?
213                .is_some()
214            {
215                candidates.insert(mock_value);
216            }
217        }
218
219        for candidate in candidates {
220            let eq = BoolExpr::eq(value.clone().into_expr(), Expr::Const(candidate));
221            let (eq_constraints, eq_sat) = self.constraints_with_condition(state, eq.clone())?;
222            let (neq_constraints, neq_sat) = self.constraints_with_condition(state, eq.not())?;
223
224            match (eq_sat, neq_sat) {
225                (true, true) => {
226                    let mut eq_state = pre_call_state.clone();
227                    eq_state.pc = call_pc;
228                    eq_state.constraints = eq_constraints;
229                    worklist.push_back(eq_state);
230
231                    let mut neq_state = pre_call_state.clone();
232                    neq_state.pc = call_pc;
233                    neq_state.constraints = neq_constraints;
234                    worklist.push_back(neq_state);
235                    return Ok(true);
236                }
237                (true, false) => {
238                    state.constraints = eq_constraints;
239                    return Ok(false);
240                }
241                (false, true) => {
242                    state.constraints = neq_constraints;
243                }
244                (false, false) => return Ok(false),
245            }
246        }
247
248        Ok(false)
249    }
250
251    /// Implements the `branch_symbolic_function_mock_if_needed` symbolic executor helper.
252    pub(super) fn branch_symbolic_function_mock_if_needed(
253        &mut self,
254        state: &mut PathState,
255        worklist: &mut VecDeque<PathState>,
256        pre_call_state: &PathState,
257        call_pc: usize,
258        callee: Address,
259        calldata: &[SymWord],
260    ) -> Result<bool, SymbolicError> {
261        let function_mocks = state.function_mocks.clone();
262        for mock in function_mocks.iter().rev().cloned() {
263            if mock.data.len() != calldata.len() {
264                continue;
265            }
266            let Some(condition) = function_mock_match_condition(
267                &mock,
268                callee,
269                calldata,
270                "symbolic vm.mockFunction calldata",
271            )?
272            else {
273                continue;
274            };
275            if self.branch_symbolic_match_condition_if_needed(
276                state,
277                worklist,
278                pre_call_state,
279                call_pc,
280                condition,
281            )? {
282                return Ok(true);
283            }
284        }
285
286        for mock in function_mocks.iter().rev().cloned() {
287            if mock.data.len() != 4 {
288                continue;
289            }
290            let Some(condition) = function_mock_match_condition(
291                &mock,
292                callee,
293                calldata,
294                "symbolic vm.mockFunction selector",
295            )?
296            else {
297                continue;
298            };
299            if self.branch_symbolic_match_condition_if_needed(
300                state,
301                worklist,
302                pre_call_state,
303                call_pc,
304                condition,
305            )? {
306                return Ok(true);
307            }
308        }
309
310        Ok(false)
311    }
312
313    /// Applies the `observe_expected_call` symbolic executor helper.
314    pub(super) fn observe_expected_call(
315        &mut self,
316        state: &mut PathState,
317        callee: Address,
318        value: Option<U256>,
319        gas: &SymWord,
320        calldata: &[SymWord],
321    ) -> Result<bool, SymbolicError> {
322        if state.expected_calls.is_empty() {
323            return Ok(true);
324        }
325        for idx in 0..state.expected_calls.len() {
326            let expected = state.expected_calls[idx].clone();
327            if let Some(constraints) = self
328                .expected_call_match_constraints(state, &expected, callee, value, gas, calldata)?
329            {
330                state.constraints = constraints;
331                return Ok(state.expected_calls[idx].observe());
332            }
333        }
334        Ok(true)
335    }
336
337    #[expect(clippy::too_many_arguments)]
338    /// Implements the `branch_symbolic_call_match_if_needed` symbolic executor helper.
339    pub(super) fn branch_symbolic_call_match_if_needed(
340        &mut self,
341        state: &mut PathState,
342        worklist: &mut VecDeque<PathState>,
343        pre_call_state: &PathState,
344        call_pc: usize,
345        callee: Address,
346        code_address: Address,
347        value: Option<U256>,
348        gas: &SymWord,
349        calldata: &[SymWord],
350    ) -> Result<bool, SymbolicError> {
351        let expected_calls = state.expected_calls.clone();
352        for expected in expected_calls {
353            let Some(condition) =
354                self.expected_call_match_condition(&expected, callee, value, gas, calldata)?
355            else {
356                continue;
357            };
358            if self.branch_symbolic_match_condition_if_needed(
359                state,
360                worklist,
361                pre_call_state,
362                call_pc,
363                condition,
364            )? {
365                return Ok(true);
366            }
367        }
368
369        let mut mocks = state.call_mocks.iter().cloned().enumerate().collect::<Vec<_>>();
370        mocks.sort_by_key(|(idx, mock)| {
371            (std::cmp::Reverse(mock.data.len()), std::cmp::Reverse(mock.value.is_some()), *idx)
372        });
373
374        for (_, mock) in mocks {
375            let Some(condition) =
376                self.call_mock_match_condition(&mock, code_address, value, calldata)?
377            else {
378                continue;
379            };
380            if self.branch_symbolic_match_condition_if_needed(
381                state,
382                worklist,
383                pre_call_state,
384                call_pc,
385                condition,
386            )? {
387                return Ok(true);
388            }
389        }
390
391        Ok(false)
392    }
393
394    /// Implements the `take_call_mock` symbolic executor helper.
395    pub(super) fn take_call_mock(
396        &mut self,
397        state: &mut PathState,
398        callee: Address,
399        value: Option<U256>,
400        calldata: &[SymWord],
401    ) -> Result<Option<CallMockOutcome>, SymbolicError> {
402        if state.call_mocks.is_empty() {
403            return Ok(None);
404        }
405        let mut best = None;
406        for idx in 0..state.call_mocks.len() {
407            let mock = state.call_mocks[idx].clone();
408            let Some(constraints) =
409                self.call_mock_match_constraints(state, &mock, callee, value, calldata)?
410            else {
411                continue;
412            };
413            let specificity = (mock.data.len(), mock.value.is_some());
414            if best.as_ref().is_none_or(
415                |(_, best_specificity, _): &(usize, (usize, bool), Vec<BoolExpr>)| {
416                    specificity > *best_specificity
417                },
418            ) {
419                best = Some((idx, specificity, constraints));
420            }
421        }
422        let Some((idx, _, constraints)) = best else {
423            return Ok(None);
424        };
425        state.constraints = constraints;
426        Ok(Some(state.call_mocks[idx].next_outcome()))
427    }
428
429    /// Implements the `branch_symbolic_match_condition_if_needed` symbolic executor helper.
430    pub(super) fn branch_symbolic_match_condition_if_needed(
431        &mut self,
432        state: &mut PathState,
433        worklist: &mut VecDeque<PathState>,
434        pre_call_state: &PathState,
435        call_pc: usize,
436        condition: BoolExpr,
437    ) -> Result<bool, SymbolicError> {
438        let (match_constraints, match_sat) =
439            self.constraints_with_condition(state, condition.clone())?;
440        let (mismatch_constraints, mismatch_sat) =
441            self.constraints_with_condition(state, condition.not())?;
442
443        match (match_sat, mismatch_sat) {
444            (true, true) => {
445                let mut match_state = pre_call_state.clone();
446                match_state.pc = call_pc;
447                match_state.constraints = match_constraints;
448                worklist.push_back(match_state);
449
450                let mut mismatch_state = pre_call_state.clone();
451                mismatch_state.pc = call_pc;
452                mismatch_state.constraints = mismatch_constraints;
453                worklist.push_back(mismatch_state);
454                Ok(true)
455            }
456            (true, false) => {
457                state.constraints = match_constraints;
458                Ok(false)
459            }
460            (false, true) => {
461                state.constraints = mismatch_constraints;
462                Ok(false)
463            }
464            (false, false) => Ok(false),
465        }
466    }
467
468    /// Implements the `function_mock_target` symbolic executor helper.
469    pub(super) fn function_mock_target(
470        &mut self,
471        state: &mut PathState,
472        callee: Address,
473        calldata: &[SymWord],
474    ) -> Result<Option<Address>, SymbolicError> {
475        for mock in state.function_mocks.iter().rev().cloned() {
476            if mock.data.len() != calldata.len() {
477                continue;
478            }
479            let Some(condition) = function_mock_match_condition(
480                &mock,
481                callee,
482                calldata,
483                "symbolic vm.mockFunction calldata",
484            )?
485            else {
486                continue;
487            };
488            if let Some(constraints) = self.constraints_for_condition(state, condition)? {
489                state.constraints = constraints;
490                return Ok(Some(mock.target));
491            }
492        }
493        for mock in state.function_mocks.iter().rev().cloned() {
494            if mock.data.len() != 4 {
495                continue;
496            }
497            let Some(condition) = function_mock_match_condition(
498                &mock,
499                callee,
500                calldata,
501                "symbolic vm.mockFunction selector",
502            )?
503            else {
504                continue;
505            };
506            if let Some(constraints) = self.constraints_for_condition(state, condition)? {
507                state.constraints = constraints;
508                return Ok(Some(mock.target));
509            }
510        }
511        Ok(None)
512    }
513
514    /// Implements the `expected_call_match_constraints` symbolic executor helper.
515    pub(super) fn expected_call_match_constraints(
516        &mut self,
517        state: &PathState,
518        expected: &ExpectedCall,
519        callee: Address,
520        value: Option<U256>,
521        gas: &SymWord,
522        calldata: &[SymWord],
523    ) -> Result<Option<Vec<BoolExpr>>, SymbolicError> {
524        let Some(condition) =
525            self.expected_call_match_condition(expected, callee, value, gas, calldata)?
526        else {
527            return Ok(None);
528        };
529        self.constraints_for_condition(state, condition)
530    }
531
532    /// Implements the `call_mock_match_constraints` symbolic executor helper.
533    pub(super) fn call_mock_match_constraints(
534        &mut self,
535        state: &PathState,
536        mock: &CallMock,
537        callee: Address,
538        value: Option<U256>,
539        calldata: &[SymWord],
540    ) -> Result<Option<Vec<BoolExpr>>, SymbolicError> {
541        let Some(condition) = self.call_mock_match_condition(mock, callee, value, calldata)? else {
542            return Ok(None);
543        };
544        self.constraints_for_condition(state, condition)
545    }
546
547    /// Implements the `expected_call_match_condition` symbolic executor helper.
548    pub(super) fn expected_call_match_condition(
549        &self,
550        expected: &ExpectedCall,
551        callee: Address,
552        value: Option<U256>,
553        gas: &SymWord,
554        calldata: &[SymWord],
555    ) -> Result<Option<BoolExpr>, SymbolicError> {
556        if !expected.static_parts_match(value, gas)? {
557            return Ok(None);
558        }
559        let Some(data_condition) =
560            calldata_prefix_condition(calldata, &expected.data, "symbolic expected call calldata")?
561        else {
562            return Ok(None);
563        };
564        Ok(Some(BoolExpr::and(vec![
565            address_match_condition(&expected.callee, callee),
566            data_condition,
567        ])))
568    }
569
570    /// Implements the `call_mock_match_condition` symbolic executor helper.
571    pub(super) fn call_mock_match_condition(
572        &self,
573        mock: &CallMock,
574        callee: Address,
575        value: Option<U256>,
576        calldata: &[SymWord],
577    ) -> Result<Option<BoolExpr>, SymbolicError> {
578        if !mock.static_parts_match(value) {
579            return Ok(None);
580        }
581        let Some(data_condition) =
582            calldata_prefix_condition(calldata, &mock.data, "symbolic mocked call calldata")?
583        else {
584            return Ok(None);
585        };
586        Ok(Some(BoolExpr::and(vec![address_match_condition(&mock.callee, callee), data_condition])))
587    }
588
589    /// Returns whether `expected_revert_matches` holds.
590    pub(super) fn expected_revert_matches(
591        &mut self,
592        state: &mut PathState,
593        expected: &ExpectedRevert,
594        reverter: Address,
595        return_data: &SymReturnData,
596    ) -> Result<bool, SymbolicError> {
597        let Some(condition) = expected_revert_match_condition(expected, reverter, return_data)
598        else {
599            return Ok(false);
600        };
601
602        let (match_constraints, match_sat) =
603            self.constraints_with_condition(state, condition.clone())?;
604        if !match_sat {
605            return Ok(false);
606        }
607
608        let (mismatch_constraints, mismatch_sat) =
609            self.constraints_with_condition(state, condition.not())?;
610        if mismatch_sat {
611            state.constraints = mismatch_constraints;
612            return Ok(false);
613        }
614
615        state.constraints = match_constraints;
616        Ok(true)
617    }
618
619    /// Implements the `assume_no_revert_rejects` symbolic executor helper.
620    pub(super) fn assume_no_revert_rejects(
621        &mut self,
622        state: &mut PathState,
623        assumption: &AssumeNoRevert,
624        reverter: Address,
625        return_data: &SymReturnData,
626    ) -> Result<bool, SymbolicError> {
627        let AssumeNoRevert::Filtered(filters) = assumption else {
628            return Ok(true);
629        };
630
631        let conditions = filters
632            .iter()
633            .filter_map(|filter| expected_revert_match_condition(filter, reverter, return_data))
634            .collect::<Vec<_>>();
635        if conditions.is_empty() {
636            return Ok(false);
637        }
638
639        let condition = BoolExpr::or(conditions);
640        let (_match_constraints, match_sat) =
641            self.constraints_with_condition(state, condition.clone())?;
642        if !match_sat {
643            return Ok(false);
644        }
645
646        let (mismatch_constraints, mismatch_sat) =
647            self.constraints_with_condition(state, condition.not())?;
648        if mismatch_sat {
649            state.constraints = mismatch_constraints;
650            return Ok(false);
651        }
652
653        Ok(true)
654    }
655
656    /// Implements the `constraints_for_condition` symbolic executor helper.
657    pub(super) fn constraints_for_condition(
658        &mut self,
659        state: &PathState,
660        condition: BoolExpr,
661    ) -> Result<Option<Vec<BoolExpr>>, SymbolicError> {
662        let (constraints, sat) = self.constraints_with_condition(state, condition)?;
663        Ok(sat.then_some(constraints))
664    }
665
666    /// Implements the `constraints_with_condition` symbolic executor helper.
667    pub(super) fn constraints_with_condition(
668        &mut self,
669        state: &PathState,
670        condition: BoolExpr,
671    ) -> Result<(Vec<BoolExpr>, bool), SymbolicError> {
672        match condition {
673            BoolExpr::Const(true) => Ok((state.constraints.clone(), true)),
674            BoolExpr::Const(false) => Ok((state.constraints.clone(), false)),
675            condition => {
676                if bool_contains_gasleft(&condition) {
677                    return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
678                }
679                let mut constraints = state.constraints.clone();
680                constraints.push(condition);
681                let sat = self.solver.is_sat(&constraints)?;
682                Ok((constraints, sat))
683            }
684        }
685    }
686
687    /// Implements the `take_loop_jump` symbolic executor helper.
688    pub(super) fn take_loop_jump(
689        &self,
690        state: &mut PathState,
691        source_pc: usize,
692        dest: usize,
693    ) -> bool {
694        let Some(bound) = self.config.loop_bound else {
695            return true;
696        };
697        if dest >= source_pc {
698            return true;
699        }
700        let count = state.loop_jumps.entry(dest).or_default();
701        if *count >= bound {
702            return false;
703        }
704        *count += 1;
705        true
706    }
707
708    /// Runs the `handle_log` symbolic executor helper.
709    pub(super) fn handle_log(
710        &mut self,
711        state: &mut PathState,
712        log: SymbolicLog,
713    ) -> Result<StepOutcome, SymbolicError> {
714        let Some(mut expected) = state.expected_emit.take() else {
715            state.record_log(log);
716            return Ok(StepOutcome::Continue);
717        };
718
719        if let Some(template) = expected.template.clone() {
720            if !self.expected_emit_matches(state, &expected, &template, &log)? {
721                state.expected_emit = Some(expected);
722                state.record_log(log);
723                return Ok(StepOutcome::Failure);
724            }
725            expected.consume_one();
726            if !expected.is_satisfied() {
727                state.expected_emit = Some(expected);
728            }
729        } else {
730            expected.template = Some(log.clone());
731            state.expected_emit = Some(expected);
732        }
733
734        state.record_log(log);
735        Ok(StepOutcome::Continue)
736    }
737
738    /// Returns whether `expected_emit_matches` holds.
739    pub(super) fn expected_emit_matches(
740        &mut self,
741        state: &mut PathState,
742        expected: &ExpectedEmit,
743        template: &SymbolicLog,
744        actual: &SymbolicLog,
745    ) -> Result<bool, SymbolicError> {
746        let mut conditions = Vec::new();
747        if let Some(expected_emitter) = &expected.emitter {
748            conditions.push(address_match_condition(expected_emitter, actual.emitter));
749        }
750        for idx in 0..expected.checks.topics.len() {
751            if !expected.checks.topics[idx] {
752                continue;
753            }
754            match (template.topics.get(idx), actual.topics.get(idx)) {
755                (Some(left), Some(right)) => {
756                    conditions
757                        .push(BoolExpr::eq(left.clone().into_expr(), right.clone().into_expr()));
758                }
759                (None, None) => {}
760                _ => return Ok(false),
761            }
762        }
763
764        if expected.checks.data {
765            conditions.push(BoolExpr::eq(
766                template.data_len.clone().into_expr(),
767                actual.data_len.clone().into_expr(),
768            ));
769            if template.data.len() != actual.data.len() {
770                return Ok(false);
771            }
772            conditions.extend(
773                template
774                    .data
775                    .iter()
776                    .cloned()
777                    .zip(actual.data.iter().cloned())
778                    .map(|(left, right)| BoolExpr::eq(left.into_expr(), right.into_expr())),
779            );
780        }
781
782        let condition = BoolExpr::and(conditions);
783        let (match_constraints, match_sat) =
784            self.constraints_with_condition(state, condition.clone())?;
785        if !match_sat {
786            return Ok(false);
787        }
788
789        let (mismatch_constraints, mismatch_sat) =
790            self.constraints_with_condition(state, condition.not())?;
791        if mismatch_sat {
792            state.constraints = mismatch_constraints;
793            return Ok(false);
794        }
795
796        state.constraints = match_constraints;
797        Ok(true)
798    }
799
800    #[expect(clippy::too_many_arguments)]
801    /// Implements the `call_concrete_target` symbolic executor helper.
802    pub(super) fn call_concrete_target<FEN: FoundryEvmNetwork>(
803        &mut self,
804        executor: &Executor<FEN>,
805        state: &mut PathState,
806        worklist: &mut VecDeque<PathState>,
807        completed_paths: &mut usize,
808        kind: CallKind,
809        to: Address,
810        target_word: Option<SymWord>,
811        value: SymWord,
812        gas: SymWord,
813        in_offset: SymWord,
814        in_size: BoundedCopySize,
815        out_offset: SymWord,
816        out_size: BoundedCopySize,
817    ) -> Result<StepOutcome, SymbolicError> {
818        if is_known_cheatcode(to) {
819            if !state.constrained_word(&value).is_some_and(|value| value.is_zero()) {
820                return Err(SymbolicError::Unsupported("value-bearing cheatcode CALL"));
821            }
822            let (in_size_word, in_size, has_symbolic_in_size) = bounded_copy_size_parts(&in_size);
823            if in_size < 4 {
824                return Err(SymbolicError::Unsupported("short cheatcode CALL"));
825            }
826            let in_offset = in_offset.into_usize("symbolic cheatcode CALL input offset")?;
827            if !self.assume_word_at_least(state, &in_size_word, 4)? {
828                return Ok(StepOutcome::AssumeRejected);
829            }
830
831            let selector = state
832                .memory
833                .read_concrete(in_offset, 4)?
834                .try_into()
835                .map_err(|_| SymbolicError::Unsupported("symbolic cheatcode selector"))?;
836            if has_symbolic_in_size {
837                let min_size = if to == CHEATCODE_ADDRESS {
838                    foundry_cheatcode_min_input_size(selector)
839                } else if to == SYMBOLIC_VM_COMPAT_ADDRESS {
840                    symbolic_vm_cheatcode_min_input_size(selector)
841                } else {
842                    None
843                }
844                .ok_or(SymbolicError::Unsupported("symbolic cheatcode CALL input size"))?;
845                if min_size > in_size {
846                    return Err(SymbolicError::Unsupported("symbolic cheatcode CALL input size"));
847                }
848                if !self.assume_word_at_least(state, &in_size_word, min_size)? {
849                    return Ok(StepOutcome::AssumeRejected);
850                }
851            }
852
853            if to == CHEATCODE_ADDRESS
854                && let Some(outcome) = self.branch_accesses_cheatcode_if_needed(
855                    state,
856                    worklist,
857                    selector,
858                    in_offset,
859                    out_offset.clone(),
860                    &out_size,
861                )?
862            {
863                return Ok(outcome);
864            }
865
866            let return_data = if to == CHEATCODE_ADDRESS {
867                match self
868                    .handle_foundry_cheatcode(executor, state, selector, in_offset, in_size)?
869                {
870                    CheatcodeOutcome::Continue(ret) => SymReturnData::from_words(ret),
871                    CheatcodeOutcome::ContinueData(ret) => ret,
872                    CheatcodeOutcome::AssumeRejected => return Ok(StepOutcome::AssumeRejected),
873                    CheatcodeOutcome::Failure => return Ok(StepOutcome::Failure),
874                }
875            } else if to == SYMBOLIC_VM_COMPAT_ADDRESS {
876                self.handle_symbolic_vm_cheatcode(state, selector, in_offset)?
877            } else {
878                return Err(SymbolicError::Unsupported("symbolic cheatcode address"));
879            };
880
881            state.return_data = return_data;
882            let return_data = state.return_data.clone();
883            state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
884            state.stack.push(SymWord::Concrete(U256::from(1)))?;
885            return Ok(StepOutcome::Continue);
886        }
887
888        if is_console(to) {
889            state.return_data = SymReturnData::default();
890            let return_data = state.return_data.clone();
891            state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
892            state.stack.push(SymWord::Concrete(U256::from(1)))?;
893            return Ok(StepOutcome::Continue);
894        }
895
896        let call_input = call_input_from_memory(&state.memory, in_offset.clone(), &in_size);
897        if !state.expected_calls.is_empty() {
898            let concrete_value = state.constrained_word(&value);
899            if !self.observe_expected_call(state, to, concrete_value, &gas, &call_input)? {
900                return Ok(StepOutcome::Failure);
901            }
902        }
903        let code_address = self.function_mock_target(state, to, &call_input)?.unwrap_or(to);
904        if !state.call_mocks.is_empty() {
905            let concrete_value = state.constrained_word(&value);
906            if let Some(mock) =
907                self.take_call_mock(state, code_address, concrete_value, &call_input)?
908            {
909                if !matches!(kind, CallKind::DelegateCall) {
910                    let _ = state.prank_for_next_call();
911                }
912                state.return_data = mock.return_data;
913                let return_data = state.return_data.clone();
914                state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
915                state.stack.push(SymWord::Concrete(U256::from(!mock.reverts)))?;
916                return Ok(StepOutcome::Continue);
917            }
918        }
919
920        if matches!(kind, CallKind::Call)
921            && !self.prepare_value_transfer(
922                executor,
923                state,
924                worklist,
925                value.clone(),
926                out_offset.clone(),
927                &out_size,
928            )?
929        {
930            return Ok(StepOutcome::Continue);
931        }
932
933        if is_supported_precompile(code_address) {
934            let input_len = bounded_copy_size_word(&in_size);
935            let input = call_input_from_memory(&state.memory, in_offset, &in_size);
936            match execute_symbolic_precompile(code_address, input, input_len)? {
937                Some(return_data) => {
938                    state.return_data = return_data;
939                    if matches!(kind, CallKind::Call) {
940                        state.world.transfer(executor, state.address, to, value);
941                    }
942                    let return_data = state.return_data.clone();
943                    state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
944                    state.stack.push(SymWord::Concrete(U256::from(1)))?;
945                }
946                None => {
947                    state.return_data = SymReturnData::default();
948                    let return_data = state.return_data.clone();
949                    state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
950                    state.stack.push(SymWord::zero())?;
951                }
952            }
953            return Ok(StepOutcome::Continue);
954        }
955
956        let child_code = state.world.extcode(executor, code_address)?;
957        if child_code.is_empty() {
958            if matches!(kind, CallKind::Call) {
959                state.world.transfer(executor, state.address, to, value);
960            }
961            state.return_data = SymReturnData::default();
962            let return_data = state.return_data.clone();
963            state.memory.copy_call_output_offset(out_offset, &out_size, &return_data)?;
964            state.stack.push(SymWord::Concrete(U256::from(1)))?;
965            return Ok(StepOutcome::Continue);
966        }
967
968        let calldata = calldata_from_call_input(call_input, &in_size);
969        let callee_address_word = state
970            .world
971            .symbolic_word_for_address(to)
972            .or_else(|| {
973                target_word
974                    .as_ref()
975                    .filter(|word| state.world.resolve_address(word) == Some(to))
976                    .cloned()
977            })
978            .unwrap_or_else(|| SymWord::Concrete(address_word(to)));
979        if matches!(kind, CallKind::DelegateCall)
980            && (state.prank.next_caller.is_some()
981                || state.prank.next_origin.is_some()
982                || state.prank.persistent_caller.is_some()
983                || state.prank.persistent_origin.is_some())
984        {
985            return Err(SymbolicError::Unsupported("symbolic prank delegatecall"));
986        }
987        let (pranked_caller, pranked_caller_word, pranked_origin) = state.prank_for_next_call();
988        let frame = match kind {
989            CallKind::Call => {
990                let mut frame = CallFrame::new(
991                    to,
992                    code_address,
993                    to,
994                    pranked_caller,
995                    value.clone(),
996                    state.is_static,
997                    calldata,
998                );
999                frame.address_word = callee_address_word;
1000                frame.caller_word = pranked_caller_word;
1001                frame
1002            }
1003            CallKind::StaticCall => {
1004                let mut frame = CallFrame::new(
1005                    to,
1006                    code_address,
1007                    to,
1008                    pranked_caller,
1009                    SymWord::zero(),
1010                    true,
1011                    calldata,
1012                );
1013                frame.address_word = callee_address_word;
1014                frame.caller_word = pranked_caller_word;
1015                frame
1016            }
1017            CallKind::DelegateCall => {
1018                let mut frame = CallFrame::new(
1019                    state.address,
1020                    code_address,
1021                    state.storage_address,
1022                    state.caller,
1023                    state.callvalue.clone(),
1024                    state.is_static,
1025                    calldata,
1026                );
1027                frame.address_word = state.address_word.clone();
1028                frame.caller_word = state.caller_word.clone();
1029                frame
1030            }
1031            CallKind::CallCode => {
1032                let mut frame = CallFrame::new(
1033                    state.address,
1034                    code_address,
1035                    state.storage_address,
1036                    pranked_caller,
1037                    value.clone(),
1038                    state.is_static,
1039                    calldata,
1040                );
1041                frame.address_word = state.address_word.clone();
1042                frame.caller_word = pranked_caller_word;
1043                frame
1044            }
1045        };
1046
1047        let original_world = state.world.clone();
1048        let mut child = state.child(frame);
1049        if let Some((origin, origin_word)) = pranked_origin {
1050            child.origin = origin;
1051            child.origin_word = origin_word;
1052        }
1053        if matches!(kind, CallKind::Call) {
1054            child.world.transfer(executor, state.address, to, value);
1055        }
1056        child.expected_revert = None;
1057        child.assume_no_revert_next_call = None;
1058        let outcomes = self.execute_external_call(executor, child, &child_code, completed_paths)?;
1059        let Some((first, rest)) = outcomes.split_first() else {
1060            return Ok(StepOutcome::AssumeRejected);
1061        };
1062
1063        let mut parents = VecDeque::with_capacity(outcomes.len());
1064        for outcome in std::iter::once(first).chain(rest.iter()) {
1065            let mut parent = state.clone();
1066            parent.constraints = outcome.state.constraints.clone();
1067            parent.next_symbol = outcome.state.next_symbol;
1068
1069            if let Some(assumption) = parent.assume_no_revert_next_call.take()
1070                && matches!(outcome.status, TopLevelCallStatus::Revert)
1071                && self.assume_no_revert_rejects(
1072                    &mut parent,
1073                    &assumption,
1074                    to,
1075                    &outcome.return_data,
1076                )?
1077            {
1078                continue;
1079            }
1080
1081            if let Some(mut expected) = parent.expected_revert.clone() {
1082                match outcome.status {
1083                    TopLevelCallStatus::Success => {
1084                        *state = parent;
1085                        return Ok(StepOutcome::Failure);
1086                    }
1087                    TopLevelCallStatus::Revert | TopLevelCallStatus::Failure => {
1088                        if !self.expected_revert_matches(
1089                            &mut parent,
1090                            &expected,
1091                            to,
1092                            &outcome.return_data,
1093                        )? {
1094                            *state = parent;
1095                            return Ok(StepOutcome::Failure);
1096                        }
1097                        if expected.consume_one() {
1098                            parent.expected_revert = None;
1099                        } else {
1100                            parent.expected_revert = Some(expected);
1101                        }
1102                        parent.access_record = outcome.state.access_record.clone();
1103                        parent.expected_calls = outcome.state.expected_calls.clone();
1104                        parent.expected_creates = outcome.state.expected_creates.clone();
1105                        parent.call_mocks = outcome.state.call_mocks.clone();
1106                        parent.function_mocks = outcome.state.function_mocks.clone();
1107                        parent.world = original_world.clone();
1108                        parent.return_data = SymReturnData::default();
1109                        let return_data = parent.return_data.clone();
1110                        parent.memory.copy_call_output_offset(
1111                            out_offset.clone(),
1112                            &out_size,
1113                            &return_data,
1114                        )?;
1115                        parent.stack.push(SymWord::Concrete(U256::from(1)))?;
1116                        parents.push_back(parent);
1117                        continue;
1118                    }
1119                }
1120            }
1121
1122            parent.world = if matches!(outcome.status, TopLevelCallStatus::Success) {
1123                outcome.state.world.clone()
1124            } else {
1125                original_world.clone()
1126            };
1127            match outcome.status {
1128                TopLevelCallStatus::Success => {
1129                    parent.block = outcome.state.block.clone();
1130                    parent.recorded_logs = outcome.state.recorded_logs.clone();
1131                    parent.access_record = outcome.state.access_record.clone();
1132                    parent.expected_emit = outcome.state.expected_emit.clone();
1133                    parent.expected_calls = outcome.state.expected_calls.clone();
1134                    parent.expected_creates = outcome.state.expected_creates.clone();
1135                    parent.call_mocks = outcome.state.call_mocks.clone();
1136                    parent.function_mocks = outcome.state.function_mocks.clone();
1137                }
1138                TopLevelCallStatus::Failure => {
1139                    *state = parent;
1140                    return Ok(StepOutcome::Failure);
1141                }
1142                TopLevelCallStatus::Revert => {}
1143            }
1144            parent.return_data = outcome.return_data.clone();
1145            let return_data = parent.return_data.clone();
1146            parent.memory.copy_call_output_offset(out_offset.clone(), &out_size, &return_data)?;
1147            parent.stack.push(SymWord::Concrete(U256::from(matches!(
1148                outcome.status,
1149                TopLevelCallStatus::Success
1150            ))))?;
1151            parents.push_back(parent);
1152        }
1153
1154        let Some(first) = pop_batch(&mut parents, self.config.exploration_order) else {
1155            return Ok(StepOutcome::AssumeRejected);
1156        };
1157        *state = first;
1158        spill_batch(parents, worklist, self.config.exploration_order);
1159        Ok(StepOutcome::Continue)
1160    }
1161
1162    /// Implements the `prepare_value_transfer` symbolic executor helper.
1163    pub(super) fn prepare_value_transfer<FEN: FoundryEvmNetwork>(
1164        &mut self,
1165        executor: &Executor<FEN>,
1166        state: &mut PathState,
1167        worklist: &mut VecDeque<PathState>,
1168        value: SymWord,
1169        out_offset: SymWord,
1170        out_size: &BoundedCopySize,
1171    ) -> Result<bool, SymbolicError> {
1172        if state.constrained_word(&value).is_some_and(|value| value.is_zero()) {
1173            return Ok(true);
1174        }
1175
1176        let balance = state.world.balance_word_for_address(executor, state.address);
1177        let can_pay = BoolExpr::cmp(BoolExprOp::Uge, balance.into_expr(), value.into_expr());
1178        match can_pay {
1179            BoolExpr::Const(true) => Ok(true),
1180            BoolExpr::Const(false) => {
1181                state.return_data = SymReturnData::default();
1182                let return_data = state.return_data.clone();
1183                state.memory.copy_call_output_offset(out_offset, out_size, &return_data)?;
1184                state.stack.push(SymWord::zero())?;
1185                Ok(false)
1186            }
1187            can_pay => {
1188                let mut success_constraints = state.constraints.clone();
1189                success_constraints.push(can_pay.clone());
1190                let success_sat = self.solver.is_sat(&success_constraints)?;
1191
1192                let mut failure_constraints = state.constraints.clone();
1193                failure_constraints.push(can_pay.not());
1194                let failure_sat = self.solver.is_sat(&failure_constraints)?;
1195
1196                match (success_sat, failure_sat) {
1197                    (true, true) => {
1198                        let mut failure = state.clone();
1199                        failure.constraints = failure_constraints;
1200                        failure.return_data = SymReturnData::default();
1201                        let return_data = failure.return_data.clone();
1202                        failure.memory.copy_call_output_offset(
1203                            out_offset,
1204                            out_size,
1205                            &return_data,
1206                        )?;
1207                        failure.stack.push(SymWord::zero())?;
1208                        worklist.push_back(failure);
1209
1210                        state.constraints = success_constraints;
1211                        Ok(true)
1212                    }
1213                    (true, false) => {
1214                        state.constraints = success_constraints;
1215                        Ok(true)
1216                    }
1217                    (false, true) => {
1218                        state.constraints = failure_constraints;
1219                        state.return_data = SymReturnData::default();
1220                        let return_data = state.return_data.clone();
1221                        state.memory.copy_call_output_offset(out_offset, out_size, &return_data)?;
1222                        state.stack.push(SymWord::zero())?;
1223                        Ok(false)
1224                    }
1225                    (false, false) => Ok(false),
1226                }
1227            }
1228        }
1229    }
1230
1231    /// Implements the `prepare_create_value_transfer` symbolic executor helper.
1232    pub(super) fn prepare_create_value_transfer<FEN: FoundryEvmNetwork>(
1233        &mut self,
1234        executor: &Executor<FEN>,
1235        state: &mut PathState,
1236        worklist: &mut VecDeque<PathState>,
1237        value: SymWord,
1238    ) -> Result<bool, SymbolicError> {
1239        if state.constrained_word(&value).is_some_and(|value| value.is_zero()) {
1240            return Ok(true);
1241        }
1242
1243        let balance = state.world.balance_word_for_address(executor, state.address);
1244        let can_pay = BoolExpr::cmp(BoolExprOp::Uge, balance.into_expr(), value.into_expr());
1245        match can_pay {
1246            BoolExpr::Const(true) => Ok(true),
1247            BoolExpr::Const(false) => {
1248                state.return_data = SymReturnData::default();
1249                state.stack.push(SymWord::zero())?;
1250                Ok(false)
1251            }
1252            can_pay => {
1253                let mut success_constraints = state.constraints.clone();
1254                success_constraints.push(can_pay.clone());
1255                let success_sat = self.solver.is_sat(&success_constraints)?;
1256
1257                let mut failure_constraints = state.constraints.clone();
1258                failure_constraints.push(can_pay.not());
1259                let failure_sat = self.solver.is_sat(&failure_constraints)?;
1260
1261                match (success_sat, failure_sat) {
1262                    (true, true) => {
1263                        let mut failure = state.clone();
1264                        failure.constraints = failure_constraints;
1265                        failure.return_data = SymReturnData::default();
1266                        failure.stack.push(SymWord::zero())?;
1267                        worklist.push_back(failure);
1268
1269                        state.constraints = success_constraints;
1270                        Ok(true)
1271                    }
1272                    (true, false) => {
1273                        state.constraints = success_constraints;
1274                        Ok(true)
1275                    }
1276                    (false, true) => {
1277                        state.constraints = failure_constraints;
1278                        state.return_data = SymReturnData::default();
1279                        state.stack.push(SymWord::zero())?;
1280                        Ok(false)
1281                    }
1282                    (false, false) => Ok(false),
1283                }
1284            }
1285        }
1286    }
1287
1288    #[expect(clippy::too_many_arguments)]
1289    /// Implements the `call_symbolic_target` symbolic executor helper.
1290    pub(super) fn call_symbolic_target<FEN: FoundryEvmNetwork>(
1291        &mut self,
1292        executor: &Executor<FEN>,
1293        state: &mut PathState,
1294        worklist: &mut VecDeque<PathState>,
1295        completed_paths: &mut usize,
1296        kind: CallKind,
1297        target: SymWord,
1298        value: SymWord,
1299        gas: SymWord,
1300        in_offset: SymWord,
1301        in_size: BoundedCopySize,
1302        out_offset: SymWord,
1303        out_size: BoundedCopySize,
1304    ) -> Result<StepOutcome, SymbolicError> {
1305        let target = target.into_expr();
1306        let mut candidates = state.world.symbolic_call_targets(executor)?;
1307        candidates.extend((1..=10).map(precompile_address));
1308        candidates.sort();
1309        candidates.dedup();
1310        if candidates.is_empty() {
1311            return Err(SymbolicError::Unsupported(
1312                "symbolic CALL target has no known contract candidates",
1313            ));
1314        }
1315
1316        let candidate_constraints = candidates
1317            .iter()
1318            .map(|address| BoolExpr::eq(target.clone(), Expr::Const(address_word(*address))))
1319            .collect::<Vec<_>>();
1320        let mut outside_constraints = state.constraints.clone();
1321        outside_constraints.extend(candidate_constraints.iter().cloned().map(BoolExpr::not));
1322        let outside_sat = self.solver.is_sat(&outside_constraints)?;
1323
1324        if !self.config.symbolic_call_targets && outside_sat {
1325            return Err(SymbolicError::Unsupported("symbolic CALL target"));
1326        }
1327
1328        let mut parents = VecDeque::new();
1329        if outside_sat {
1330            let mut branch = state.clone();
1331            branch.constraints = outside_constraints;
1332
1333            if matches!(kind, CallKind::Call) {
1334                if self.prepare_value_transfer(
1335                    executor,
1336                    &mut branch,
1337                    &mut parents,
1338                    value.clone(),
1339                    out_offset.clone(),
1340                    &out_size,
1341                )? {
1342                    let symbolic_target = SymWord::Expr(target);
1343                    let to = branch.world.symbolic_address_slot(symbolic_target);
1344                    branch.world.transfer(executor, branch.address, to, value.clone());
1345                    branch.return_data = SymReturnData::default();
1346                    let return_data = branch.return_data.clone();
1347                    branch.memory.copy_call_output_offset(
1348                        out_offset.clone(),
1349                        &out_size,
1350                        &return_data,
1351                    )?;
1352                    branch.stack.push(SymWord::Concrete(U256::from(1)))?;
1353                    parents.push_back(branch);
1354                }
1355            } else {
1356                branch.return_data = SymReturnData::default();
1357                let return_data = branch.return_data.clone();
1358                branch.memory.copy_call_output_offset(
1359                    out_offset.clone(),
1360                    &out_size,
1361                    &return_data,
1362                )?;
1363                branch.stack.push(SymWord::Concrete(U256::from(1)))?;
1364                parents.push_back(branch);
1365            }
1366        }
1367
1368        for (to, constraint) in candidates.into_iter().zip(candidate_constraints) {
1369            let mut branch = state.clone();
1370            branch.constraints.push(constraint);
1371            if !self.solver.is_sat(&branch.constraints)? {
1372                continue;
1373            }
1374
1375            let mut branch_worklist = VecDeque::new();
1376            match self.call_concrete_target(
1377                executor,
1378                &mut branch,
1379                &mut branch_worklist,
1380                completed_paths,
1381                kind,
1382                to,
1383                None,
1384                value.clone(),
1385                gas.clone(),
1386                in_offset.clone(),
1387                in_size.clone(),
1388                out_offset.clone(),
1389                out_size.clone(),
1390            )? {
1391                StepOutcome::Continue => {
1392                    parents.push_back(branch);
1393                    spill_batch(branch_worklist, &mut parents, self.config.exploration_order);
1394                }
1395                StepOutcome::AssumeRejected => {}
1396                outcome => return Ok(outcome),
1397            }
1398        }
1399
1400        let Some(first) = pop_batch(&mut parents, self.config.exploration_order) else {
1401            return Ok(StepOutcome::AssumeRejected);
1402        };
1403        *state = first;
1404        spill_batch(parents, worklist, self.config.exploration_order);
1405        Ok(StepOutcome::Continue)
1406    }
1407}
1408
1409fn ensure_word_not_gasleft(word: &SymWord) -> Result<(), SymbolicError> {
1410    if word.contains_gasleft() {
1411        Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"))
1412    } else {
1413        Ok(())
1414    }
1415}
foundry_evm_symbolic/executor/calls.rs

foundry_evm_symbolic/executor/
calls.rs
