foundry_evm_symbolic/executor/
create.rs

1use super::*;
2
3impl SymbolicExecutor {
4    pub(super) fn create<FEN: FoundryEvmNetwork>(
5        &mut self,
6        executor: &Executor<FEN>,
7        state: &mut PathState,
8        worklist: &mut VecDeque<PathState>,
9        completed_paths: &mut usize,
10        kind: CreateKind,
11    ) -> Result<StepOutcome, SymbolicError> {
12        if state.is_static {
13            state.return_data = SymReturnData::empty(&mut self.cx);
14            return Ok(StepOutcome::Revert);
15        }
16
17        let value = state.stack.pop()?;
18        let offset = state.stack.pop()?;
19        let size = state.stack.pop()?;
20        let size = match state.constrained_usize_checked(&mut self.cx, &size) {
21            Some(Ok(size)) => BoundedCopySize::Concrete(size),
22            Some(Err(_)) => {
23                state.return_data = SymReturnData::empty(&mut self.cx);
24                state.stack.push(SymExpr::zero(&mut self.cx))?;
25                return Ok(StepOutcome::Continue);
26            }
27            None => {
28                let max_limit = self.config.max_calldata_bytes as usize;
29                let max_size = state
30                    .upper_bound_usize(&mut self.cx, &size)
31                    .filter(|size| *size <= max_limit)
32                    .map(Ok)
33                    .unwrap_or_else(|| {
34                        self.solver_upper_bound_usize(
35                            state,
36                            &size,
37                            max_limit,
38                            "symbolic CREATE initcode size",
39                        )
40                    })?;
41                BoundedCopySize::Symbolic { size, max_size }
42            }
43        };
44        let salt =
45            if matches!(kind, CreateKind::Create2) { Some(state.stack.pop()?) } else { None };
46
47        let initcode = match &size {
48            BoundedCopySize::Concrete(size) => {
49                if let Some(offset) = state.constrained_usize(&mut self.cx, &offset) {
50                    let bytes = state.memory.read_bytes(&mut self.cx, offset, *size);
51                    SymCode::from_bytes(&mut self.cx, bytes)
52                } else {
53                    SymCode::from_memory_offset(&mut self.cx, &state.memory, offset, *size)
54                }
55            }
56            BoundedCopySize::Symbolic { size, max_size } => SymCode::from_memory_symbolic_size(
57                &mut self.cx,
58                &state.memory,
59                offset,
60                size.clone(),
61                *max_size,
62            ),
63        };
64        let (created_word, created) = match kind {
65            CreateKind::Create => {
66                let nonce = state.world.nonce(executor, state.address)?;
67                let address = state.address.create(nonce);
68                (SymExpr::constant(&mut self.cx, address_word(address)), address)
69            }
70            CreateKind::Create2 => create2_address_word(
71                &mut self.cx,
72                state,
73                state.address,
74                salt.expect("CREATE2 salt exists"),
75                &initcode,
76            )?,
77        };
78
79        if !self.prepare_create_value_transfer(executor, state, worklist, value.clone())? {
80            return Ok(StepOutcome::Continue);
81        }
82
83        let mut failure_world = state.world.clone();
84        failure_world.increment_nonce(executor, state.address)?;
85
86        if failure_world.has_code_or_nonce(&mut self.cx, executor, created)? {
87            state.world = failure_world;
88            state.return_data = SymReturnData::empty(&mut self.cx);
89            state.stack.push(SymExpr::zero(&mut self.cx))?;
90            return Ok(StepOutcome::Continue);
91        }
92
93        let calldata = SymBytes::empty(&mut self.cx);
94        let calldata = SymCalldata::from_bytes(&mut self.cx, calldata);
95        let mut frame = CallFrame::new(
96            &mut self.cx,
97            created,
98            created,
99            created,
100            state.address,
101            value.clone(),
102            false,
103            calldata,
104        );
105        frame.address_word = created_word.clone();
106        frame.caller_word = state.address_word.clone();
107        let mut child = state.child(frame);
108        let pending_expected_creates = std::mem::take(&mut child.expected_creates);
109        child.world = failure_world.clone();
110        child.world.mark_current_transaction_created(created);
111        child.world.set_nonce(created, 1);
112        child.world.transfer(&mut self.cx, executor, state.address, created, value);
113        child.expected_revert = None;
114        child.assume_no_revert_next_call = None;
115
116        let outcomes = self.execute_external_call(executor, child, &initcode, completed_paths)?;
117        let Some((first, rest)) = outcomes.split_first() else {
118            return Ok(StepOutcome::AssumeRejected);
119        };
120
121        let mut parents = VecDeque::with_capacity(outcomes.len());
122        for outcome in std::iter::once(first).chain(rest.iter()) {
123            let mut parent = state.clone();
124            parent.constraints = outcome.state.constraints.clone();
125            parent.next_symbol = outcome.state.next_symbol;
126            parent.inherit_branch_target_progress(&outcome.state);
127            parent.storage_load_hooks = outcome.state.storage_load_hooks.clone();
128            parent.storage_store_hooks = outcome.state.storage_store_hooks.clone();
129            parent.mapping_storage_store_hooks = outcome.state.mapping_storage_store_hooks.clone();
130            parent.inherit_mapping_hook_provenance(&outcome.state);
131            parent.return_data = SymReturnData::empty(&mut self.cx);
132
133            if let Some(assumption) = parent.assume_no_revert_next_call.take()
134                && matches!(outcome.status, TopLevelCallStatus::Revert)
135                && self.assume_no_revert_rejects(
136                    &mut parent,
137                    &assumption,
138                    created,
139                    &outcome.return_data,
140                )?
141            {
142                continue;
143            }
144
145            if let Some(mut expected) = parent.expected_revert.clone() {
146                match outcome.status {
147                    TopLevelCallStatus::Success => {
148                        *state = parent;
149                        return Ok(StepOutcome::Failure);
150                    }
151                    TopLevelCallStatus::Revert | TopLevelCallStatus::Failure => {
152                        if !self.expected_revert_matches(
153                            &mut parent,
154                            &expected,
155                            created,
156                            &outcome.return_data,
157                        )? {
158                            *state = parent;
159                            return Ok(StepOutcome::Failure);
160                        }
161                        if expected.consume_one() {
162                            parent.expected_revert = None;
163                        } else {
164                            parent.expected_revert = Some(expected);
165                        }
166                        parent.access_record = outcome.state.access_record.clone();
167                        parent.expected_calls = outcome.state.expected_calls.clone();
168                        parent.expected_creates = pending_expected_creates.clone();
169                        parent.call_mocks = outcome.state.call_mocks.clone();
170                        parent.function_mocks = outcome.state.function_mocks.clone();
171                        parent.world = failure_world.clone();
172                        parent.stack.push(created_word.clone())?;
173                        parents.push_back(parent);
174                        continue;
175                    }
176                }
177            }
178
179            match outcome.status {
180                TopLevelCallStatus::Success => {
181                    parent.world = outcome.state.world.clone();
182                    parent.block = outcome.state.block.clone();
183                    parent.recorded_logs = outcome.state.recorded_logs.clone();
184                    parent.access_record = outcome.state.access_record.clone();
185                    parent.expected_emit = outcome.state.expected_emit.clone();
186                    parent.expected_calls = outcome.state.expected_calls.clone();
187                    parent.expected_creates = pending_expected_creates.clone();
188                    parent.call_mocks = outcome.state.call_mocks.clone();
189                    parent.function_mocks = outcome.state.function_mocks.clone();
190                    self.observe_expected_create(
191                        &mut parent,
192                        state.address,
193                        kind,
194                        &outcome.return_data,
195                    )?;
196                    if !parent.world.is_destroyed(created) {
197                        parent
198                            .world
199                            .install_code(created, outcome.return_data.to_code(&mut self.cx)?);
200                        parent.world.set_nonce(created, 1);
201                    }
202                    parent.stack.push(created_word.clone())?;
203                }
204                TopLevelCallStatus::Revert => {
205                    parent.world = failure_world.clone();
206                    parent.stack.push(SymExpr::zero(&mut self.cx))?;
207                }
208                TopLevelCallStatus::Failure => {
209                    *state = parent;
210                    return Ok(StepOutcome::Failure);
211                }
212            }
213
214            parents.push_back(parent);
215        }
216
217        let Some(first) = self.pop_next_path(&mut parents) else {
218            return Ok(StepOutcome::AssumeRejected);
219        };
220        *state = first;
221        worklist.extend(parents);
222        Ok(StepOutcome::Continue)
223    }
224
225    pub(super) fn execute_external_call<FEN: FoundryEvmNetwork>(
226        &mut self,
227        executor: &Executor<FEN>,
228        initial: PathState,
229        code: &SymCode,
230        completed_paths: &mut usize,
231    ) -> Result<Vec<ExternalCallOutcome>, SymbolicError> {
232        let mut worklist = VecDeque::from([initial]);
233        let mut outcomes = Vec::new();
234        let path_limit = self.config.path_width() as usize;
235        let depth_limit = self.config.execution_depth() as usize;
236
237        while let Some(mut state) = self.pop_next_feasible_path(&mut worklist)? {
238            if *completed_paths >= path_limit {
239                return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
240            }
241            if std::mem::take(&mut state.pending_storage_hook_revert) {
242                *completed_paths += 1;
243                outcomes.push(ExternalCallOutcome {
244                    status: TopLevelCallStatus::Revert,
245                    return_data: state.return_data.clone(),
246                    state,
247                });
248                continue;
249            }
250
251            loop {
252                self.check_timeout()?;
253                if state.depth >= depth_limit {
254                    return Err(SymbolicError::Unsupported("symbolic depth limit exceeded"));
255                }
256                state.depth += 1;
257
258                let op = match code.guarded_opcode(&mut self.cx, state.pc)? {
259                    GuardedOpcode::End => {
260                        *completed_paths += 1;
261                        outcomes.push(ExternalCallOutcome {
262                            status: if state.storage_hook_active || state.expectations_satisfied() {
263                                TopLevelCallStatus::Success
264                            } else {
265                                TopLevelCallStatus::Failure
266                            },
267                            return_data: state.return_data.clone(),
268                            state,
269                        });
270                        break;
271                    }
272                    GuardedOpcode::Concrete(op) => op,
273                    GuardedOpcode::SymbolicSize { condition, opcode } => {
274                        let mut in_bounds_constraints = state.constraints.clone();
275                        in_bounds_constraints.push(condition.clone());
276                        let in_bounds_sat =
277                            self.solver.is_sat(&mut self.cx, &in_bounds_constraints)?;
278
279                        let mut out_of_bounds_constraints = state.constraints.clone();
280                        out_of_bounds_constraints.push(condition.not(&mut self.cx));
281                        if self.solver.is_sat(&mut self.cx, &out_of_bounds_constraints)? {
282                            let mut halted = state.clone();
283                            halted.constraints = out_of_bounds_constraints;
284                            *completed_paths += 1;
285                            outcomes.push(ExternalCallOutcome {
286                                status: if halted.storage_hook_active
287                                    || halted.expectations_satisfied()
288                                {
289                                    TopLevelCallStatus::Success
290                                } else {
291                                    TopLevelCallStatus::Failure
292                                },
293                                return_data: halted.return_data.clone(),
294                                state: halted,
295                            });
296                        }
297
298                        if in_bounds_sat {
299                            state.constraints = in_bounds_constraints;
300                            opcode
301                        } else {
302                            break;
303                        }
304                    }
305                };
306
307                match self.step(
308                    executor,
309                    code,
310                    code.jump_table(),
311                    &mut state,
312                    &mut worklist,
313                    completed_paths,
314                    op,
315                )? {
316                    StepOutcome::Continue => {}
317                    StepOutcome::Halt => {
318                        *completed_paths += 1;
319                        outcomes.push(ExternalCallOutcome {
320                            status: if state.storage_hook_active || state.expectations_satisfied() {
321                                TopLevelCallStatus::Success
322                            } else {
323                                TopLevelCallStatus::Failure
324                            },
325                            return_data: state.return_data.clone(),
326                            state,
327                        });
328                        break;
329                    }
330                    StepOutcome::Revert => {
331                        *completed_paths += 1;
332                        outcomes.push(ExternalCallOutcome {
333                            status: TopLevelCallStatus::Revert,
334                            return_data: state.return_data.clone(),
335                            state,
336                        });
337                        break;
338                    }
339                    StepOutcome::Failure => {
340                        *completed_paths += 1;
341                        outcomes.push(ExternalCallOutcome {
342                            status: TopLevelCallStatus::Failure,
343                            return_data: state.return_data.clone(),
344                            state,
345                        });
346                        break;
347                    }
348                    StepOutcome::AssumeRejected | StepOutcome::Forked => break,
349                }
350            }
351        }
352
353        Ok(outcomes)
354    }
355}
foundry_evm_symbolic/executor/create.rs

foundry_evm_symbolic/executor/
create.rs
