foundry_evm_symbolic/executor/
invariant.rs

1use super::*;
2
3impl SymbolicExecutor {
4    #[expect(clippy::too_many_arguments)]
5    /// Computes the `execute_invariant_check` symbolic executor helper result.
6    pub(super) fn execute_invariant_check<FEN: FoundryEvmNetwork>(
7        &mut self,
8        executor: &Executor<FEN>,
9        state: PathState,
10        invariant_address: Address,
11        sender: Address,
12        invariant: &Function,
13        after_invariant: Option<&Function>,
14        completed_paths: &mut usize,
15    ) -> Result<Vec<InvariantCheckOutcome>, SymbolicError> {
16        let calldata = SymbolicCalldata::selector_only(invariant)?;
17        let outcomes = self.execute_sequence_call(
18            executor,
19            state,
20            invariant_address,
21            sender,
22            invariant,
23            calldata.call_data(),
24            calldata.constraints,
25            completed_paths,
26        )?;
27
28        let mut checked = Vec::new();
29        for mut outcome in outcomes {
30            if !matches!(outcome.status, TopLevelCallStatus::Success) {
31                outcome.status = TopLevelCallStatus::Failure;
32                checked.push(InvariantCheckOutcome { failed: true, state: outcome.state });
33                continue;
34            }
35
36            if self.invariant_return_failed(invariant, &outcome.return_data, &mut outcome.state)? {
37                checked.push(InvariantCheckOutcome { failed: true, state: outcome.state });
38                continue;
39            }
40
41            let Some(after_invariant) = after_invariant else {
42                checked.push(InvariantCheckOutcome { failed: false, state: outcome.state });
43                continue;
44            };
45
46            let after_calldata = SymbolicCalldata::selector_only(after_invariant)?;
47            for after_outcome in self.execute_sequence_call(
48                executor,
49                outcome.state.clone(),
50                invariant_address,
51                sender,
52                after_invariant,
53                after_calldata.call_data(),
54                after_calldata.constraints.clone(),
55                completed_paths,
56            )? {
57                checked.push(InvariantCheckOutcome {
58                    failed: !matches!(after_outcome.status, TopLevelCallStatus::Success),
59                    state: after_outcome.state,
60                });
61            }
62        }
63        Ok(checked)
64    }
65
66    /// Implements the `invariant_return_failed` symbolic executor helper.
67    pub(super) fn invariant_return_failed(
68        &mut self,
69        invariant: &Function,
70        return_data: &SymReturnData,
71        state: &mut PathState,
72    ) -> Result<bool, SymbolicError> {
73        if invariant.outputs.is_empty() {
74            return Ok(false);
75        }
76        if invariant.outputs.len() != 1 || invariant.outputs[0].selector_type().as_ref() != "bool" {
77            return Ok(false);
78        }
79        if return_data.len < 32 {
80            return Ok(true);
81        }
82
83        let pass = return_data.load_word(0)?.nonzero_bool();
84        let fail = pass.clone().not();
85        match fail {
86            BoolExpr::Const(true) => Ok(true),
87            BoolExpr::Const(false) => Ok(false),
88            fail => {
89                let mut constraints = state.constraints.clone();
90                constraints.push(fail);
91                if self.solver.is_sat(&constraints)? {
92                    state.constraints = constraints;
93                    Ok(true)
94                } else {
95                    state.constraints.push(pass);
96                    Ok(false)
97                }
98            }
99        }
100    }
101
102    #[expect(clippy::too_many_arguments)]
103    /// Computes the `execute_sequence_call` symbolic executor helper result.
104    pub(super) fn execute_sequence_call<FEN: FoundryEvmNetwork>(
105        &mut self,
106        executor: &Executor<FEN>,
107        mut state: PathState,
108        target: Address,
109        sender: Address,
110        _function: &Function,
111        calldata: SymCalldata,
112        constraints: Vec<BoolExpr>,
113        completed_paths: &mut usize,
114    ) -> Result<Vec<TopLevelCallOutcome>, SymbolicError> {
115        state.world.clear_transient_storage();
116        let code = state.world.extcode(executor, target)?;
117        let jumpdests = analyze_jumpdests(&code);
118        state.call_depth = 0;
119        state.origin = sender;
120        state.origin_word = SymWord::Concrete(address_word(sender));
121        state.frame =
122            CallFrame::new(target, target, target, sender, SymWord::zero(), false, calldata);
123        state.constraints.extend(constraints);
124
125        let mut worklist = VecDeque::from([state]);
126        let mut outcomes = Vec::new();
127        let path_limit = self.config.path_width() as usize;
128        let depth_limit = self.config.execution_depth() as usize;
129
130        while let Some(mut state) = pop_worklist(&mut worklist, self.config.exploration_order) {
131            if *completed_paths >= path_limit {
132                return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
133            }
134            let _path_span =
135                trace_span!("symbolic_path", completed_paths, worklist_size = worklist.len())
136                    .entered();
137            trace!(completed_paths, worklist_size = worklist.len(), "exploring symbolic path");
138
139            loop {
140                if state.depth >= depth_limit {
141                    return Err(SymbolicError::Unsupported("symbolic depth limit exceeded"));
142                }
143                state.depth += 1;
144
145                let Some(op) = code.opcode(state.pc)? else {
146                    *completed_paths += 1;
147                    outcomes.push(TopLevelCallOutcome {
148                        status: if state.expectations_satisfied() {
149                            TopLevelCallStatus::Success
150                        } else {
151                            TopLevelCallStatus::Failure
152                        },
153                        return_data: state.return_data.clone(),
154                        state,
155                    });
156                    break;
157                };
158
159                let _step_span = trace_span!("symbolic_step", pc = state.pc - 1, op).entered();
160                match self.step(
161                    executor,
162                    &code,
163                    &jumpdests,
164                    &mut state,
165                    &mut worklist,
166                    completed_paths,
167                    op,
168                )? {
169                    StepOutcome::Continue => {}
170                    StepOutcome::Halt => {
171                        *completed_paths += 1;
172                        outcomes.push(TopLevelCallOutcome {
173                            status: if state.expectations_satisfied() {
174                                TopLevelCallStatus::Success
175                            } else {
176                                TopLevelCallStatus::Failure
177                            },
178                            return_data: state.return_data.clone(),
179                            state,
180                        });
181                        break;
182                    }
183                    StepOutcome::Revert => {
184                        *completed_paths += 1;
185                        outcomes.push(TopLevelCallOutcome {
186                            status: TopLevelCallStatus::Revert,
187                            return_data: state.return_data.clone(),
188                            state,
189                        });
190                        break;
191                    }
192                    StepOutcome::Failure => {
193                        *completed_paths += 1;
194                        outcomes.push(TopLevelCallOutcome {
195                            status: TopLevelCallStatus::Failure,
196                            return_data: state.return_data.clone(),
197                            state,
198                        });
199                        break;
200                    }
201                    StepOutcome::AssumeRejected | StepOutcome::Forked => break,
202                }
203            }
204        }
205
206        Ok(outcomes)
207    }
208
209    /// Runs the `materialize_sequence` symbolic executor helper.
210    pub(super) fn materialize_sequence(
211        &mut self,
212        steps: &[SequenceStepTemplate],
213        state: &PathState,
214    ) -> Result<Vec<SymbolicInvariantStep>, SymbolicError> {
215        let model = self.solver.model(&state.constraints)?;
216        steps
217            .iter()
218            .map(|step| {
219                let args = step.calldata.model_to_args(&model)?;
220                let calldata = Bytes::from(step.function.abi_encode_input(&args)?);
221                Ok(SymbolicInvariantStep {
222                    sender: step.sender,
223                    address: step.address,
224                    contract_name: step.contract_name.clone(),
225                    function_name: step.function.name.clone(),
226                    signature: step.function.signature(),
227                    args,
228                    calldata,
229                })
230            })
231            .collect()
232    }
233}
foundry_evm_symbolic/executor/invariant.rs

foundry_evm_symbolic/executor/
invariant.rs
