foundry_evm_symbolic/executor/
create.rs1use 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.return_data = SymReturnData::empty(&mut self.cx);
128
129 if let Some(assumption) = parent.assume_no_revert_next_call.take()
130 && matches!(outcome.status, TopLevelCallStatus::Revert)
131 && self.assume_no_revert_rejects(
132 &mut parent,
133 &assumption,
134 created,
135 &outcome.return_data,
136 )?
137 {
138 continue;
139 }
140
141 if let Some(mut expected) = parent.expected_revert.clone() {
142 match outcome.status {
143 TopLevelCallStatus::Success => {
144 *state = parent;
145 return Ok(StepOutcome::Failure);
146 }
147 TopLevelCallStatus::Revert | TopLevelCallStatus::Failure => {
148 if !self.expected_revert_matches(
149 &mut parent,
150 &expected,
151 created,
152 &outcome.return_data,
153 )? {
154 *state = parent;
155 return Ok(StepOutcome::Failure);
156 }
157 if expected.consume_one() {
158 parent.expected_revert = None;
159 } else {
160 parent.expected_revert = Some(expected);
161 }
162 parent.access_record = outcome.state.access_record.clone();
163 parent.expected_calls = outcome.state.expected_calls.clone();
164 parent.expected_creates = pending_expected_creates.clone();
165 parent.call_mocks = outcome.state.call_mocks.clone();
166 parent.function_mocks = outcome.state.function_mocks.clone();
167 parent.world = failure_world.clone();
168 parent.stack.push(created_word.clone())?;
169 parents.push_back(parent);
170 continue;
171 }
172 }
173 }
174
175 match outcome.status {
176 TopLevelCallStatus::Success => {
177 parent.world = outcome.state.world.clone();
178 parent.block = outcome.state.block.clone();
179 parent.recorded_logs = outcome.state.recorded_logs.clone();
180 parent.access_record = outcome.state.access_record.clone();
181 parent.expected_emit = outcome.state.expected_emit.clone();
182 parent.expected_calls = outcome.state.expected_calls.clone();
183 parent.expected_creates = pending_expected_creates.clone();
184 parent.call_mocks = outcome.state.call_mocks.clone();
185 parent.function_mocks = outcome.state.function_mocks.clone();
186 self.observe_expected_create(
187 &mut parent,
188 state.address,
189 kind,
190 &outcome.return_data,
191 )?;
192 if !parent.world.is_destroyed(created) {
193 parent
194 .world
195 .install_code(created, outcome.return_data.to_code(&mut self.cx)?);
196 parent.world.set_nonce(created, 1);
197 }
198 parent.stack.push(created_word.clone())?;
199 }
200 TopLevelCallStatus::Revert => {
201 parent.world = failure_world.clone();
202 parent.stack.push(SymExpr::zero(&mut self.cx))?;
203 }
204 TopLevelCallStatus::Failure => {
205 *state = parent;
206 return Ok(StepOutcome::Failure);
207 }
208 }
209
210 parents.push_back(parent);
211 }
212
213 let Some(first) = self.pop_next_path(&mut parents) else {
214 return Ok(StepOutcome::AssumeRejected);
215 };
216 *state = first;
217 worklist.extend(parents);
218 Ok(StepOutcome::Continue)
219 }
220
221 pub(super) fn execute_external_call<FEN: FoundryEvmNetwork>(
222 &mut self,
223 executor: &Executor<FEN>,
224 initial: PathState,
225 code: &SymCode,
226 completed_paths: &mut usize,
227 ) -> Result<Vec<ExternalCallOutcome>, SymbolicError> {
228 let mut worklist = VecDeque::from([initial]);
229 let mut outcomes = Vec::new();
230 let path_limit = self.config.path_width() as usize;
231 let depth_limit = self.config.execution_depth() as usize;
232
233 while let Some(mut state) = self.pop_next_feasible_path(&mut worklist)? {
234 if *completed_paths >= path_limit {
235 return Err(SymbolicError::Unsupported("symbolic path limit exceeded"));
236 }
237
238 loop {
239 self.check_timeout()?;
240 if state.depth >= depth_limit {
241 return Err(SymbolicError::Unsupported("symbolic depth limit exceeded"));
242 }
243 state.depth += 1;
244
245 let op = match code.guarded_opcode(&mut self.cx, state.pc)? {
246 GuardedOpcode::End => {
247 *completed_paths += 1;
248 outcomes.push(ExternalCallOutcome {
249 status: if state.expectations_satisfied() {
250 TopLevelCallStatus::Success
251 } else {
252 TopLevelCallStatus::Failure
253 },
254 return_data: state.return_data.clone(),
255 state,
256 });
257 break;
258 }
259 GuardedOpcode::Concrete(op) => op,
260 GuardedOpcode::SymbolicSize { condition, opcode } => {
261 let mut in_bounds_constraints = state.constraints.clone();
262 in_bounds_constraints.push(condition.clone());
263 let in_bounds_sat =
264 self.solver.is_sat(&mut self.cx, &in_bounds_constraints)?;
265
266 let mut out_of_bounds_constraints = state.constraints.clone();
267 out_of_bounds_constraints.push(condition.not(&mut self.cx));
268 if self.solver.is_sat(&mut self.cx, &out_of_bounds_constraints)? {
269 let mut halted = state.clone();
270 halted.constraints = out_of_bounds_constraints;
271 *completed_paths += 1;
272 outcomes.push(ExternalCallOutcome {
273 status: if halted.expectations_satisfied() {
274 TopLevelCallStatus::Success
275 } else {
276 TopLevelCallStatus::Failure
277 },
278 return_data: halted.return_data.clone(),
279 state: halted,
280 });
281 }
282
283 if in_bounds_sat {
284 state.constraints = in_bounds_constraints;
285 opcode
286 } else {
287 break;
288 }
289 }
290 };
291
292 match self.step(
293 executor,
294 code,
295 code.jump_table(),
296 &mut state,
297 &mut worklist,
298 completed_paths,
299 op,
300 )? {
301 StepOutcome::Continue => {}
302 StepOutcome::Halt => {
303 *completed_paths += 1;
304 outcomes.push(ExternalCallOutcome {
305 status: if state.expectations_satisfied() {
306 TopLevelCallStatus::Success
307 } else {
308 TopLevelCallStatus::Failure
309 },
310 return_data: state.return_data.clone(),
311 state,
312 });
313 break;
314 }
315 StepOutcome::Revert => {
316 *completed_paths += 1;
317 outcomes.push(ExternalCallOutcome {
318 status: TopLevelCallStatus::Revert,
319 return_data: state.return_data.clone(),
320 state,
321 });
322 break;
323 }
324 StepOutcome::Failure => {
325 *completed_paths += 1;
326 outcomes.push(ExternalCallOutcome {
327 status: TopLevelCallStatus::Failure,
328 return_data: state.return_data.clone(),
329 state,
330 });
331 break;
332 }
333 StepOutcome::AssumeRejected | StepOutcome::Forked => break,
334 }
335 }
336 }
337
338 Ok(outcomes)
339 }
340}