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