1use super::*;
2
3enum MappingStorageProvenance {
4 None,
5 Exact(SymbolicMappingProvenance),
6 Fork { equality: Vec<SymBoolExpr>, inequality: Vec<SymBoolExpr> },
7}
8
9impl SymbolicExecutor {
10 fn classify_mapping_match(
11 &mut self,
12 state: &PathState,
13 matches: SymBoolExpr,
14 provenance: SymbolicMappingProvenance,
15 ) -> Result<Option<MappingStorageProvenance>, SymbolicError> {
16 let does_not_match = matches.clone().not(&mut self.cx);
17 let (inequality, inequality_is_sat) =
18 self.constraints_with_condition(state, does_not_match)?;
19 if !inequality_is_sat {
20 return Ok(Some(MappingStorageProvenance::Exact(provenance)));
21 }
22 let (equality, equality_is_sat) = self.constraints_with_condition(state, matches)?;
23 Ok(equality_is_sat.then_some(MappingStorageProvenance::Fork { equality, inequality }))
24 }
25
26 fn observed_mapping_chain(
27 &mut self,
28 state: &PathState,
29 hash: &SymExpr,
30 ) -> Option<(SymExpr, Vec<SymExpr>)> {
31 let account = state.storage_address;
32 let mut current = hash.clone();
33 let mut keys = Vec::new();
34 let mut visited = Vec::new();
35 loop {
36 if visited.contains(¤t) {
37 return None;
38 }
39 visited.push(current.clone());
40 let Some(bytes) =
41 state.mapping_hook_keccak_preimages.get(&(account, current.clone())).cloned()
42 else {
43 keys.reverse();
44 return Some((current, keys));
45 };
46 if bytes.len() != 64 {
47 return None;
48 }
49 keys.push(SymExpr::from_bytes(&mut self.cx, bytes[..32].iter().cloned()));
50 current = SymExpr::from_bytes(&mut self.cx, bytes[32..64].iter().cloned());
51 }
52 }
53
54 fn mapping_storage_provenance(
55 &mut self,
56 state: &PathState,
57 key: &SymExpr,
58 ) -> Result<MappingStorageProvenance, SymbolicError> {
59 let account = state.storage_address;
60 let observed = |hash: &SymExpr| {
61 state.mapping_hook_keccak_preimages.get(&(account, hash.clone())).cloned()
62 };
63 if let Some(provenance) =
64 key.storage_mapping_provenance_observed_with(&mut self.cx, observed)
65 {
66 return Ok(MappingStorageProvenance::Exact(provenance));
67 }
68 let mut hashes = state
69 .mapping_hook_keccak_preimages
70 .keys()
71 .filter(|(address, _)| *address == account)
72 .map(|(_, hash)| hash.clone())
73 .collect::<Vec<_>>();
74 let contains_observed_hash =
75 hashes.iter().any(|hash| key.visit_bool(|candidate| candidate == hash));
76 let key_is_const = key.as_const().is_some();
77 let key_contains_keccak = key.contains_keccak();
78 let key_is_storage_mapping_key = key.storage_mapping_key(&mut self.cx).is_some();
79 let roots = state
80 .mapping_storage_store_hooks
81 .keys()
82 .filter(|(address, _)| *address == account)
83 .map(|(_, root)| *root)
84 .collect::<Vec<_>>();
85 hashes.sort_by_key(|hash| hash != key);
86 for hash in hashes {
87 if contains_observed_hash && !key.visit_bool(|candidate| candidate == &hash) {
88 continue;
89 }
90 let use_legacy_match = contains_observed_hash || !key_contains_keccak;
91 if use_legacy_match
92 && let Some(provenance) =
93 hash.storage_mapping_provenance_observed_with(&mut self.cx, |candidate| {
94 state
95 .mapping_hook_keccak_preimages
96 .get(&(account, candidate.clone()))
97 .cloned()
98 })
99 {
100 if !state.mapping_storage_store_hooks.contains_key(&(account, provenance.root_slot))
101 {
102 continue;
103 }
104 let equality = SymBoolExpr::eq(&mut self.cx, key.clone(), hash.clone());
105 if key_is_const {
106 let inequality = equality.not(&mut self.cx);
107 let (_, inequality_is_sat) =
108 self.constraints_with_condition(state, inequality)?;
109 if !inequality_is_sat {
110 return Ok(MappingStorageProvenance::Exact(provenance));
111 }
112 continue;
113 }
114 if let Some(provenance) =
115 self.classify_mapping_match(state, equality, provenance)?
116 {
117 return Ok(provenance);
118 }
119 continue;
120 }
121 if (key_is_const || key_contains_keccak) && !key_is_storage_mapping_key {
122 continue;
123 }
124 let Some((root, keys)) = self.observed_mapping_chain(state, &hash) else {
125 continue;
126 };
127 for &root_slot in &roots {
128 let slot_matches = if key_is_const || key.visit_bool(|candidate| candidate == &hash)
129 {
130 SymBoolExpr::eq(&mut self.cx, key.clone(), hash.clone())
131 } else {
132 key.storage_key_eq(&mut self.cx, &hash)
133 };
134 let matches = if let Some(constrained_root) =
135 state.constrained_word(&mut self.cx, &root)
136 {
137 if constrained_root != root_slot {
138 continue;
139 }
140 slot_matches
141 } else {
142 let root_slot_expr = SymExpr::constant(&mut self.cx, root_slot);
143 let root_matches = SymBoolExpr::eq(&mut self.cx, root.clone(), root_slot_expr);
144 SymBoolExpr::and(&mut self.cx, vec![slot_matches, root_matches])
145 };
146 let provenance = SymbolicMappingProvenance { root_slot, keys: keys.clone() };
147 if let Some(provenance) = self.classify_mapping_match(state, matches, provenance)? {
148 return Ok(provenance);
149 }
150 }
151 }
152 Ok(MappingStorageProvenance::None)
153 }
154
155 fn storage_hook_calldata(
156 &mut self,
157 selector: [u8; 4],
158 words: impl IntoIterator<Item = SymExpr>,
159 ) -> SymCalldata {
160 let selector = SymBytes::concrete(&mut self.cx, selector.to_vec());
161 let words = words.into_iter().map(|word| word.into_bytes(&mut self.cx)).collect::<Vec<_>>();
162 let bytes = SymBytes::concat(&mut self.cx, std::iter::once(selector).chain(words));
163 SymCalldata::from_bytes(&mut self.cx, bytes)
164 }
165
166 fn mapping_storage_hook_calldata(
167 &mut self,
168 selector: [u8; 4],
169 [account, computed_slot, root_slot, old_value, new_value]: [SymExpr; 5],
170 keys: Vec<SymExpr>,
171 ) -> SymCalldata {
172 let selector = SymBytes::concrete(&mut self.cx, selector.to_vec());
173 let keys_offset = SymExpr::constant(&mut self.cx, U256::from(6 * 32));
174 let mut words = vec![account, computed_slot, root_slot, keys_offset, old_value, new_value];
175 words.push(SymExpr::constant(&mut self.cx, U256::from(keys.len())));
176 words.extend(keys);
177 let words = words.into_iter().map(|word| word.into_bytes(&mut self.cx)).collect::<Vec<_>>();
178 let bytes = SymBytes::concat(&mut self.cx, std::iter::once(selector).chain(words));
179 SymCalldata::from_bytes(&mut self.cx, bytes)
180 }
181
182 fn invoke_storage_hook<FEN: FoundryEvmNetwork>(
183 &mut self,
184 executor: &Executor<FEN>,
185 state: &mut PathState,
186 worklist: &mut VecDeque<PathState>,
187 completed_paths: &mut usize,
188 hook: SymbolicStorageHook,
189 calldata: SymCalldata,
190 ) -> Result<StepOutcome, SymbolicError> {
191 let code = state.world.extcode(&mut self.cx, executor, hook.callback_target)?;
192 if code.is_empty() {
193 return Ok(StepOutcome::Continue);
194 }
195
196 let callvalue = SymExpr::zero(&mut self.cx);
197 let frame = CallFrame::new(
198 &mut self.cx,
199 hook.callback_target,
200 hook.callback_target,
201 hook.callback_target,
202 CHEATCODE_ADDRESS,
203 callvalue,
204 false,
205 calldata,
206 );
207 let child = state.storage_hook_child(frame);
208 let outcomes = self.execute_external_call(executor, child, &code, completed_paths)?;
209 if outcomes.is_empty() {
210 return Ok(StepOutcome::AssumeRejected);
211 }
212
213 let mut parents = VecDeque::with_capacity(outcomes.len());
214 for outcome in outcomes {
215 let mut parent = state.clone();
216 parent.constraints = outcome.state.constraints.clone();
217 parent.next_symbol = outcome.state.next_symbol;
218 parent.storage_load_hooks = outcome.state.storage_load_hooks.clone();
219 parent.storage_store_hooks = outcome.state.storage_store_hooks.clone();
220 parent.mapping_storage_store_hooks = outcome.state.mapping_storage_store_hooks.clone();
221 parent.inherit_mapping_hook_provenance(&outcome.state);
222 parent.storage_hook_active = false;
223
224 match outcome.status {
225 TopLevelCallStatus::Success => {
226 parent.world = outcome.state.world.clone();
227 parent.block = outcome.state.block.clone();
228 }
229 TopLevelCallStatus::Revert | TopLevelCallStatus::Failure => {
230 parent.return_data = outcome.return_data.clone();
231 parent.pending_storage_hook_revert = true;
232 }
233 }
234 parents.push_back(parent);
235 }
236
237 let Some(first) = self.pop_next_path(&mut parents) else {
238 return Ok(StepOutcome::AssumeRejected);
239 };
240 *state = first;
241 worklist.extend(parents);
242 Ok(if std::mem::take(&mut state.pending_storage_hook_revert) {
243 StepOutcome::Revert
244 } else {
245 StepOutcome::Continue
246 })
247 }
248
249 fn push_comparison_result(
250 &mut self,
251 state: &mut PathState,
252 op_pc: usize,
253 opcode: u8,
254 condition: SymBoolExpr,
255 ) -> Result<StepOutcome, SymbolicError> {
256 if !self.apply_branch_target_constraint(state, op_pc, opcode, &condition)? {
257 return Ok(StepOutcome::AssumeRejected);
258 }
259 let value = SymExpr::bool_word(&mut self.cx, condition);
260 state.stack.push(value)?;
261 Ok(StepOutcome::Continue)
262 }
263
264 fn apply_branch_target_constraint(
265 &mut self,
266 state: &mut PathState,
267 op_pc: usize,
268 opcode: u8,
269 condition: &SymBoolExpr,
270 ) -> Result<bool, SymbolicError> {
271 let Some(target) = state.branch_target() else {
272 return Ok(true);
273 };
274 if state.satisfies_branch_target() {
275 return Ok(true);
276 }
277 if !target.matches(state.address, op_pc, opcode) {
278 return Ok(true);
279 }
280
281 let desired =
282 if target.result() { condition.clone().not(&mut self.cx) } else { condition.clone() };
283 let mut constraints = state.constraints.clone();
284 constraints.push(desired);
285 if !self.branch_is_sat_or_defer(&constraints)? {
286 return Ok(false);
287 }
288 state.constraints = constraints;
289 state.mark_branch_target_reached();
290 Ok(true)
291 }
292
293 #[expect(clippy::too_many_arguments)]
294 pub(super) fn step<FEN: FoundryEvmNetwork>(
295 &mut self,
296 executor: &Executor<FEN>,
297 code: &SymCode,
298 jumpdests: &JumpTable,
299 state: &mut PathState,
300 worklist: &mut VecDeque<PathState>,
301 completed_paths: &mut usize,
302 op: u8,
303 ) -> Result<StepOutcome, SymbolicError> {
304 state.pc += 1;
305
306 match op {
307 opcode::PUSH0 => {
308 state.stack.push(SymExpr::zero(&mut self.cx))?;
309 }
310 opcode::PUSH1..=opcode::PUSH32 => {
311 let n = (op - opcode::PUSH1 + 1) as usize;
312 let end = state.pc.saturating_add(n);
313 if end > code.len() {
314 return Err(SymbolicError::InvalidBytecode("truncated PUSH data"));
315 }
316 let value = code.push_data_word(&mut self.cx, state.pc, n);
317 state.pc = end;
318 state.stack.push(value)?;
319 }
320 opcode::DUP1..=opcode::DUP16 => {
321 let n = (op - opcode::DUP1 + 1) as usize;
322 let value = state.stack.peek(n - 1)?.clone();
323 state.stack.push(value)?;
324 }
325 opcode::SWAP1..=opcode::SWAP16 => {
326 let n = (op - opcode::SWAP1 + 1) as usize;
327 state.stack.swap(n)?;
328 }
329 opcode::STOP => return Ok(StepOutcome::Halt),
330 opcode::ADD => {
331 state.bin_word(&mut self.cx, SymBinOp::Add)?;
332 }
333 opcode::SUB => {
334 state.bin_word(&mut self.cx, SymBinOp::Sub)?;
335 }
336 opcode::MUL => {
337 state.bin_word(&mut self.cx, SymBinOp::Mul)?;
338 }
339 opcode::EXP => {
340 state.exp_word(&mut self.cx)?;
341 }
342 opcode::DIV => {
343 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::UDiv)?;
344 }
345 opcode::SDIV => {
346 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::SDiv)?;
347 }
348 opcode::MOD => {
349 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::URem)?;
350 }
351 opcode::SMOD => {
352 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::SRem)?;
353 }
354 opcode::ADDMOD => {
355 let a = state.stack.pop()?;
356 let b = state.stack.pop()?;
357 let n = state.stack.pop()?;
358 state.stack.push(SymExpr::ternop(&mut self.cx, SymTernOp::AddMod, a, b, n))?;
359 }
360 opcode::MULMOD => {
361 let a = state.stack.pop()?;
362 let b = state.stack.pop()?;
363 let n = state.stack.pop()?;
364 state.stack.push(SymExpr::ternop(&mut self.cx, SymTernOp::MulMod, a, b, n))?;
365 }
366 opcode::LT => {
367 let op_pc = state.pc - 1;
368 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Ult)?;
369 return self.push_comparison_result(state, op_pc, op, condition);
370 }
371 opcode::GT => {
372 let op_pc = state.pc - 1;
373 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Ugt)?;
374 return self.push_comparison_result(state, op_pc, op, condition);
375 }
376 opcode::SLT => {
377 let op_pc = state.pc - 1;
378 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Slt)?;
379 return self.push_comparison_result(state, op_pc, op, condition);
380 }
381 opcode::SGT => {
382 let op_pc = state.pc - 1;
383 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Sgt)?;
384 return self.push_comparison_result(state, op_pc, op, condition);
385 }
386 opcode::EQ => {
387 let op_pc = state.pc - 1;
388 let a = state.stack.pop()?;
389 let b = state.stack.pop()?;
390 let condition = SymBoolExpr::eq(&mut self.cx, b, a);
391 return self.push_comparison_result(state, op_pc, op, condition);
392 }
393 opcode::ISZERO => {
394 let op_pc = state.pc - 1;
395 let value = state.stack.pop()?;
396 let value = value.into_zero_bool(&mut self.cx);
397 return self.push_comparison_result(state, op_pc, op, value);
398 }
399 opcode::AND => {
400 state.bin_word(&mut self.cx, SymBinOp::And)?;
401 }
402 opcode::OR => {
403 state.bin_word(&mut self.cx, SymBinOp::Or)?;
404 }
405 opcode::XOR => {
406 state.bin_word(&mut self.cx, SymBinOp::Xor)?;
407 }
408 opcode::NOT => {
409 let value = state.stack.pop()?;
410 state.stack.push(SymExpr::not(&mut self.cx, value))?;
411 }
412 opcode::SIGNEXTEND => {
413 let byte_index = state.stack.pop()?;
414 let value = state.stack.pop()?;
415 state.stack.push(signextend_word_dynamic(&mut self.cx, byte_index, value))?;
416 }
417 opcode::BYTE => {
418 let index = state.stack.pop()?;
419 let word = state.stack.pop()?;
420 state.stack.push(byte_word_dynamic(&mut self.cx, index, word))?;
421 }
422 opcode::SHL => {
423 state.shift_word(&mut self.cx, ShiftKind::Shl)?;
424 }
425 opcode::SHR => {
426 state.shift_word(&mut self.cx, ShiftKind::Shr)?;
427 }
428 opcode::SAR => {
429 state.shift_word(&mut self.cx, ShiftKind::Sar)?;
430 }
431 opcode::KECCAK256 => {
432 let offset = state.stack.pop()?;
433 let size = state.stack.pop()?;
434 match state.constrained_usize_checked(&mut self.cx, &size) {
435 Some(Ok(size)) => {
436 let bytes = state.memory.read_byte_exprs_offset(&mut self.cx, offset, size);
437 let hash = keccak_word(&mut self.cx, bytes.clone());
438 let has_mapping_hook = state
439 .mapping_storage_store_hooks
440 .keys()
441 .any(|(address, _)| *address == state.storage_address);
442 if has_mapping_hook && !state.storage_hook_active && size == 64 {
443 state
444 .mapping_hook_keccak_preimages
445 .entry((state.storage_address, hash.clone()))
446 .or_insert_with(|| bytes.into());
447 }
448 state.stack.push(hash)?;
449 }
450 Some(Err(_)) => {
451 return Ok(StepOutcome::Revert);
452 }
453 None => {
454 let has_mapping_hook = state
455 .mapping_storage_store_hooks
456 .keys()
457 .any(|(address, _)| *address == state.storage_address);
458 if has_mapping_hook && !state.storage_hook_active {
459 let mapping_size = SymExpr::constant(&mut self.cx, U256::from(64));
460 let mapping_size_feasible =
461 SymBoolExpr::eq(&mut self.cx, size.clone(), mapping_size);
462 let (_, mapping_size_feasible) =
463 self.constraints_with_condition(state, mapping_size_feasible)?;
464 if mapping_size_feasible {
465 self.defer_incomplete(
466 "symbolic KECCAK256 size may conceal mapping provenance",
467 );
468 }
469 }
470 let max_limit = self.config.max_calldata_bytes as usize;
471 let max_size = state
472 .upper_bound_usize(&mut self.cx, &size)
473 .filter(|size| *size <= max_limit)
474 .map(Ok)
475 .unwrap_or_else(|| {
476 self.solver_upper_bound_usize(
477 state,
478 &size,
479 max_limit,
480 "symbolic SHA3 size",
481 )
482 })?;
483 let bytes = state.memory.read_byte_exprs_symbolic_size(
484 &mut self.cx,
485 offset,
486 size.clone(),
487 max_size,
488 );
489 state.stack.push(keccak_word_with_len(&mut self.cx, bytes, size))?;
490 }
491 }
492 }
493 opcode::ADDRESS => {
494 let address = state.address_word.clone();
495 state.stack.push(address)?;
496 }
497 opcode::CALLER => {
498 let caller = state.caller_word.clone();
499 state.stack.push(caller)?;
500 }
501 opcode::ORIGIN => {
502 let origin = state.origin_word.clone();
503 state.stack.push(origin)?;
504 }
505 opcode::CALLVALUE => {
506 let callvalue = state.callvalue.clone();
507 state.stack.push(callvalue)?;
508 }
509 opcode::BLOCKHASH => {
510 let number = state.stack.pop()?;
511 let hash = state.block.block_hash_word(&mut self.cx, executor, number)?;
512 state.stack.push(hash)?;
513 }
514 opcode::BALANCE => {
515 let target = state.stack.pop()?;
516 let balance = state.balance_word(&mut self.cx, executor, target)?;
517 state.stack.push(balance)?;
518 }
519 opcode::SELFBALANCE => {
520 let balance = state.balance(&mut self.cx, executor, state.address);
521 state.stack.push(balance)?;
522 }
523 opcode::EXTCODESIZE => {
524 let target = state.stack.pop()?;
525 let size = state.extcode_size_word(&mut self.cx, executor, target)?;
526 state.stack.push(size)?;
527 }
528 opcode::EXTCODEHASH => {
529 let target = state.stack.pop()?;
530 let hash = state.extcode_hash_word(&mut self.cx, executor, target)?;
531 state.stack.push(hash)?;
532 }
533 opcode::EXTCODECOPY => {
534 let target = state.stack.pop()?;
535 let dest = state.stack.pop()?;
536 let offset = state.stack.pop()?;
537 let size = state.stack.pop()?;
538 match state.constrained_usize_checked(&mut self.cx, &size) {
539 Some(Ok(size)) => {
540 let bytes = state.extcode_bytes_word(
541 &mut self.cx,
542 executor,
543 target,
544 offset,
545 size,
546 )?;
547 state.memory.copy_bytes_offset(&mut self.cx, dest, bytes);
548 }
549 Some(Err(_)) => {
550 return Ok(StepOutcome::Revert);
551 }
552 None => {
553 let max_limit = self.config.max_calldata_bytes as usize;
554 let max_size = state
555 .upper_bound_usize(&mut self.cx, &size)
556 .filter(|size| *size <= max_limit)
557 .map(Ok)
558 .unwrap_or_else(|| {
559 self.solver_upper_bound_usize(
560 state,
561 &size,
562 max_limit,
563 "symbolic EXTCODECOPY size",
564 )
565 })?;
566 if max_size != 0 {
567 let bytes = state.extcode_bytes_word(
568 &mut self.cx,
569 executor,
570 target,
571 offset,
572 max_size,
573 )?;
574 state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
575 }
576 }
577 }
578 }
579 opcode::CALLDATALOAD => {
580 let offset = state.stack.pop()?;
581 let value = state.calldata.load_word(&mut self.cx, offset)?;
582 state.stack.push(value)?;
583 }
584 opcode::CALLDATASIZE => {
585 let size = state.calldata.size_word();
586 state.stack.push(size)?;
587 }
588 opcode::CALLDATACOPY => {
589 let dest = state.stack.pop()?;
590 let offset = state.stack.pop()?;
591 let size = state.stack.pop()?;
592 match state.constrained_usize_checked(&mut self.cx, &size) {
593 Some(Ok(size)) => {
594 if size != 0 {
595 state.copy_calldata_to_offset(&mut self.cx, dest, offset, size)?;
596 }
597 }
598 Some(Err(_)) => {
599 return Ok(StepOutcome::Revert);
600 }
601 None => {
602 let max_limit = self.config.max_calldata_bytes as usize;
603 let max_size = state
604 .upper_bound_usize(&mut self.cx, &size)
605 .filter(|size| *size <= max_limit)
606 .map(Ok)
607 .unwrap_or_else(|| {
608 self.solver_upper_bound_usize(
609 state,
610 &size,
611 max_limit,
612 "symbolic CALLDATACOPY size",
613 )
614 })?;
615 if max_size != 0 {
616 state.copy_calldata_symbolic_size(
617 &mut self.cx,
618 dest,
619 offset,
620 size,
621 max_size,
622 )?;
623 }
624 }
625 }
626 }
627 opcode::CODESIZE => {
628 let value = SymExpr::constant(&mut self.cx, U256::from(code.len()));
629 state.stack.push(value)?;
630 }
631 opcode::CODECOPY => {
632 let dest = state.stack.pop()?;
633 let offset = state.stack.pop()?;
634 let size = state.stack.pop()?;
635 match state.constrained_usize_checked(&mut self.cx, &size) {
636 Some(Ok(size)) => {
637 let bytes = code.read_bytes_offset(&mut self.cx, offset, size);
638 state.memory.copy_bytes_offset(&mut self.cx, dest, bytes);
639 }
640 Some(Err(_)) => {
641 return Ok(StepOutcome::Revert);
642 }
643 None => {
644 let max_limit = self.config.max_calldata_bytes as usize;
645 let max_size = state
646 .upper_bound_usize(&mut self.cx, &size)
647 .filter(|size| *size <= max_limit)
648 .map(Ok)
649 .unwrap_or_else(|| {
650 self.solver_upper_bound_usize(
651 state,
652 &size,
653 max_limit,
654 "symbolic CODECOPY size",
655 )
656 })?;
657 if max_size != 0 {
658 let bytes = code.read_bytes_offset(&mut self.cx, offset, max_size);
659 state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
660 }
661 }
662 }
663 }
664 opcode::RETURNDATASIZE => {
665 let size = state.return_data.len_word();
666 state.stack.push(size)?;
667 }
668 opcode::RETURNDATACOPY => {
669 let dest = state.stack.pop()?;
670 let offset = state.stack.pop()?;
671 let size = state.stack.pop()?;
672 match state.constrained_usize_checked(&mut self.cx, &size) {
673 Some(Ok(size)) => {
674 let size_word = SymExpr::constant(&mut self.cx, U256::from(size));
675 if !self.assume_returndata_copy_in_bounds(
676 state,
677 offset.clone(),
678 size_word,
679 )? {
680 return Ok(StepOutcome::Revert);
681 }
682 state.copy_return_data_to_offset(&mut self.cx, dest, offset, size)?;
683 }
684 Some(Err(_)) => {
685 return Ok(StepOutcome::Revert);
686 }
687 None => {
688 let available = state
689 .constrained_usize(&mut self.cx, &offset)
690 .map(|offset| state.return_data.len().saturating_sub(offset))
691 .unwrap_or(state.return_data.len());
692 let max_limit = available.min(self.config.max_calldata_bytes as usize);
693 let max_size = state
694 .upper_bound_usize(&mut self.cx, &size)
695 .filter(|size| *size <= max_limit)
696 .map(Ok)
697 .unwrap_or_else(|| {
698 self.solver_upper_bound_usize(
699 state,
700 &size,
701 max_limit,
702 "symbolic RETURNDATACOPY size",
703 )
704 })?;
705 if max_size != 0 {
706 if !self.assume_returndata_copy_in_bounds(
707 state,
708 offset.clone(),
709 size.clone(),
710 )? {
711 return Ok(StepOutcome::Revert);
712 }
713 state.copy_return_data_symbolic_size(
714 &mut self.cx,
715 dest,
716 offset,
717 size,
718 max_size,
719 )?;
720 }
721 }
722 }
723 }
724 opcode::POP => {
725 state.stack.pop()?;
726 }
727 opcode::MLOAD => {
728 let offset = state.stack.pop()?;
729 let value = state.memory.load_word_offset(&mut self.cx, offset)?;
730 state.stack.push(value)?;
731 }
732 opcode::MSTORE => {
733 let offset = state.stack.pop()?;
734 let value = state.stack.pop()?;
735 state.memory.store_word_offset(&mut self.cx, offset, value);
736 }
737 opcode::MSTORE8 => {
738 let offset = state.stack.pop()?;
739 let value = state.stack.pop()?;
740 state.memory.store_byte_offset(&mut self.cx, offset, value);
741 }
742 opcode::SLOAD => {
743 let key = state.stack.pop()?;
744 state.record_sload(state.storage_address, key.clone());
745 let concrete_key = state.constrained_word(&mut self.cx, &key);
746 let value = state.world.sload(
747 &mut self.cx,
748 executor,
749 state.storage_address,
750 key.clone(),
751 concrete_key,
752 )?;
753 state.stack.push(value.clone())?;
754 if !state.storage_hook_active
755 && let Some(hook) =
756 state.storage_load_hooks.get(&state.storage_address).copied()
757 {
758 let account =
759 SymExpr::constant(&mut self.cx, address_word(state.storage_address));
760 let calldata =
761 self.storage_hook_calldata(hook.callback_selector, [account, key, value]);
762 return self.invoke_storage_hook(
763 executor,
764 state,
765 worklist,
766 completed_paths,
767 hook,
768 calldata,
769 );
770 }
771 }
772 opcode::SSTORE => {
773 if state.is_static {
774 state.return_data = SymReturnData::empty(&mut self.cx);
775 return Ok(StepOutcome::Revert);
776 }
777 let key = state.stack.peek(0)?.clone();
778 state.stack.peek(1)?;
779 let hook = (!state.storage_hook_active)
780 .then(|| state.storage_store_hooks.get(&state.storage_address).copied())
781 .flatten();
782 let mapping = if state.storage_hook_active {
783 MappingStorageProvenance::None
784 } else {
785 self.mapping_storage_provenance(state, &key)?
786 };
787 let mapping = match mapping {
788 MappingStorageProvenance::None => None,
789 MappingStorageProvenance::Exact(provenance) => state
790 .mapping_storage_store_hooks
791 .get(&(state.storage_address, provenance.root_slot))
792 .copied()
793 .map(|hook| (hook, provenance)),
794 MappingStorageProvenance::Fork { equality, inequality } => {
795 let store_pc = state.pc - 1;
796 let mut equality_state = state.clone();
797 equality_state.pc = store_pc;
798 equality_state.constraints = equality;
799 let mut inequality_state = state.clone();
800 inequality_state.pc = store_pc;
801 inequality_state.constraints = inequality;
802 worklist.push_back(equality_state);
803 worklist.push_back(inequality_state);
804 return Ok(StepOutcome::Forked);
805 }
806 };
807 state.stack.pop()?;
808 let value = state.stack.pop()?;
809 state.record_sstore(state.storage_address, key.clone());
810 let old_value = if hook.is_some() || mapping.is_some() {
811 let concrete_key = state.constrained_word(&mut self.cx, &key);
812 Some(state.world.sload(
813 &mut self.cx,
814 executor,
815 state.storage_address,
816 key.clone(),
817 concrete_key,
818 )?)
819 } else {
820 None
821 };
822 state.world.sstore(state.storage_address, key.clone(), value.clone());
823 if let Some(hook) = hook {
824 let account =
825 SymExpr::constant(&mut self.cx, address_word(state.storage_address));
826 let calldata = self.storage_hook_calldata(
827 hook.callback_selector,
828 [
829 account,
830 key,
831 old_value.expect("old value loaded for storage hook"),
832 value,
833 ],
834 );
835 return self.invoke_storage_hook(
836 executor,
837 state,
838 worklist,
839 completed_paths,
840 hook,
841 calldata,
842 );
843 } else if let Some((hook, provenance)) = mapping {
844 let account =
845 SymExpr::constant(&mut self.cx, address_word(state.storage_address));
846 let root = SymExpr::constant(&mut self.cx, provenance.root_slot);
847 let calldata = self.mapping_storage_hook_calldata(
848 hook.callback_selector,
849 [
850 account,
851 key,
852 root,
853 old_value.expect("old value loaded for mapping storage hook"),
854 value,
855 ],
856 provenance.keys,
857 );
858 return self.invoke_storage_hook(
859 executor,
860 state,
861 worklist,
862 completed_paths,
863 hook,
864 calldata,
865 );
866 }
867 }
868 opcode::TLOAD => {
869 let key = state.stack.pop()?;
870 let value = state.world.tload(&mut self.cx, state.storage_address, key);
871 state.stack.push(value)?;
872 }
873 opcode::TSTORE => {
874 if state.is_static {
875 state.return_data = SymReturnData::empty(&mut self.cx);
876 return Ok(StepOutcome::Revert);
877 }
878 let key = state.stack.pop()?;
879 let value = state.stack.pop()?;
880 state.world.tstore(state.storage_address, key, value);
881 }
882 opcode::JUMP => {
883 let dest = state.stack.pop()?;
884 let dest = state.expect_constrained_usize(
885 &mut self.cx,
886 dest,
887 "symbolic JUMP destination",
888 )?;
889 ensure_jumpdest(dest, jumpdests)?;
890 if !self.take_loop_jump(state, state.pc, dest) {
891 return Ok(StepOutcome::AssumeRejected);
892 }
893 state.pc = dest;
894 }
895 opcode::JUMPI => {
896 let dest = state.stack.pop()?;
897 let dest = state.expect_constrained_usize(
898 &mut self.cx,
899 dest,
900 "symbolic JUMPI destination",
901 )?;
902 ensure_jumpdest(dest, jumpdests)?;
903 let cond = state.stack.pop()?;
904 match cond.truth() {
905 Some(true) => {
906 if !self.take_loop_jump(state, state.pc, dest) {
907 return Ok(StepOutcome::AssumeRejected);
908 }
909 state.pc = dest;
910 }
911 Some(false) => {}
912 None => {
913 let op_pc = state.pc.saturating_sub(1);
914 let _branch_span = trace_span!("jumpi_branch", pc = op_pc, dest).entered();
915 let true_cond = cond.nonzero_bool(&mut self.cx);
916 let false_cond = true_cond.clone().not(&mut self.cx);
917 let fallthrough = state.pc;
918 let (true_seed_models, false_seed_models) =
919 state.split_corpus_seed_models(&true_cond);
920 let mut true_state = state.clone();
921 true_state.constraints.push(true_cond);
922 true_state.set_corpus_seed_models(true_seed_models);
923 true_state.pc = dest;
924 let mut false_state = state.clone();
925 false_state.constraints.push(false_cond);
926 false_state.set_corpus_seed_models(false_seed_models);
927 false_state.pc = fallthrough;
928
929 let true_pending = self.take_loop_jump(&mut true_state, fallthrough, dest);
930 if true_pending {
931 true_state.defer_feasibility_check();
932 }
933 false_state.defer_feasibility_check();
934 trace!(true_pending, false_pending = true, "JUMPI symbolic branch");
935 if true_pending {
936 let true_seed_count = true_state.corpus_seed_model_count();
937 let false_seed_count = false_state.corpus_seed_model_count();
938 match (
939 false_seed_count.cmp(&true_seed_count),
940 self.config.exploration_order,
941 ) {
942 (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Bfs)
943 | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Dfs) => {
944 worklist.push_back(false_state);
945 worklist.push_back(true_state);
946 }
947 (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Dfs)
948 | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Bfs)
949 | (std::cmp::Ordering::Equal, _) => {
950 worklist.push_back(true_state);
951 worklist.push_back(false_state);
952 }
953 }
954 } else {
955 worklist.push_back(false_state);
956 }
957 return Ok(StepOutcome::Forked);
958 }
959 }
960 }
961 opcode::PC => {
962 let pc = state.pc - 1;
963 let pc = SymExpr::constant(&mut self.cx, U256::from(pc));
964 state.stack.push(pc)?;
965 }
966 opcode::MSIZE => {
967 let size = state.memory.size_word(&mut self.cx);
968 state.stack.push(size)?;
969 }
970 opcode::GAS => {
971 let gas = state.fresh_gasleft(&mut self.cx);
972 state.stack.push(gas)?;
973 }
974 opcode::JUMPDEST => {}
975 opcode::MCOPY => {
976 let dest = state.stack.pop()?;
977 let src = state.stack.pop()?;
978 let size = state.stack.pop()?;
979 match state.constrained_usize_checked(&mut self.cx, &size) {
980 Some(Ok(size)) => {
981 state.memory.copy_memory_to_offset(&mut self.cx, dest, src, size)?;
982 }
983 Some(Err(_)) => {
984 return Ok(StepOutcome::Revert);
985 }
986 None => {
987 let max_limit = self.config.max_calldata_bytes as usize;
988 let max_size = state
989 .upper_bound_usize(&mut self.cx, &size)
990 .filter(|size| *size <= max_limit)
991 .map(Ok)
992 .unwrap_or_else(|| {
993 self.solver_upper_bound_usize(
994 state,
995 &size,
996 max_limit,
997 "symbolic MCOPY size",
998 )
999 })?;
1000 if max_size != 0 {
1001 state.memory.copy_memory_symbolic_size(
1002 &mut self.cx,
1003 dest,
1004 src,
1005 size,
1006 max_size,
1007 )?;
1008 }
1009 }
1010 }
1011 }
1012 opcode::RETURN => return self.return_or_revert(state, false),
1013 opcode::REVERT => return self.return_or_revert(state, true),
1014 opcode::INVALID => return Ok(StepOutcome::Failure),
1015 opcode::CALL => {
1016 return self.call(executor, state, worklist, completed_paths, CallKind::Call);
1017 }
1018 opcode::CALLCODE => {
1019 return self.call(executor, state, worklist, completed_paths, CallKind::CallCode);
1020 }
1021 opcode::DELEGATECALL => {
1022 return self.call(
1023 executor,
1024 state,
1025 worklist,
1026 completed_paths,
1027 CallKind::DelegateCall,
1028 );
1029 }
1030 opcode::STATICCALL => {
1031 return self.call(executor, state, worklist, completed_paths, CallKind::StaticCall);
1032 }
1033 opcode::CREATE => {
1034 return self.create(executor, state, worklist, completed_paths, CreateKind::Create);
1035 }
1036 opcode::CREATE2 => {
1037 return self.create(
1038 executor,
1039 state,
1040 worklist,
1041 completed_paths,
1042 CreateKind::Create2,
1043 );
1044 }
1045 opcode::SELFDESTRUCT => {
1046 if state.is_static {
1047 state.return_data = SymReturnData::empty(&mut self.cx);
1048 return Ok(StepOutcome::Revert);
1049 }
1050 let spec_id: SpecId = executor.spec_id().into();
1051 let (beneficiary_word, beneficiary) =
1052 state.pop_address_word_or_symbolic_slot(&mut self.cx)?;
1053 if spec_id < SpecId::CANCUN
1054 || state.world.was_created_in_current_transaction(state.address)
1055 {
1056 state.world.selfdestruct_legacy(
1057 &mut self.cx,
1058 executor,
1059 state.address,
1060 beneficiary,
1061 )?;
1062 } else {
1063 if state.constrained_word(&mut self.cx, &beneficiary_word).is_none() {
1064 return Err(SymbolicError::Unsupported(
1065 "symbolic SELFDESTRUCT beneficiary",
1066 ));
1067 }
1068 state.world.selfdestruct_cancun_existing(
1069 &mut self.cx,
1070 executor,
1071 state.address,
1072 beneficiary,
1073 );
1074 }
1075 state.return_data = SymReturnData::empty(&mut self.cx);
1076 return Ok(StepOutcome::Halt);
1077 }
1078 opcode::CHAINID => {
1079 let value = state.block.chain_id.clone();
1080 state.stack.push(value)?;
1081 }
1082 opcode::BASEFEE => {
1083 let value = state.block.basefee.clone();
1084 state.stack.push(value)?;
1085 }
1086 opcode::GASPRICE => {
1087 let gas_price = state.gas_price.clone();
1088 state.stack.push(gas_price)?;
1089 }
1090 opcode::BLOBHASH => {
1091 let index = state.stack.pop()?;
1092 let index = state.expect_constrained_usize(
1093 &mut self.cx,
1094 index,
1095 "symbolic BLOBHASH index",
1096 )?;
1097 let hash = state.block.blob_hash(index);
1098 let hash = SymExpr::constant(&mut self.cx, U256::from_be_slice(hash.as_slice()));
1099 state.stack.push(hash)?;
1100 }
1101 opcode::COINBASE => {
1102 let coinbase = state.block.coinbase;
1103 let coinbase = SymExpr::constant(&mut self.cx, address_word(coinbase));
1104 state.stack.push(coinbase)?;
1105 }
1106 opcode::TIMESTAMP => {
1107 let value = state.block.timestamp.clone();
1108 state.stack.push(value)?;
1109 }
1110 opcode::NUMBER => {
1111 let value = state.block.number.clone();
1112 state.stack.push(value)?;
1113 }
1114 opcode::DIFFICULTY => {
1115 let value = state.block.difficulty.clone();
1116 state.stack.push(value)?;
1117 }
1118 opcode::GASLIMIT => {
1119 let value = state.block.gaslimit.clone();
1120 state.stack.push(value)?;
1121 }
1122 opcode::BLOBBASEFEE => {
1123 let value = state.block.blob_basefee.clone();
1124 state.stack.push(value)?;
1125 }
1126 opcode::LOG0 | opcode::LOG1 | opcode::LOG2 | opcode::LOG3 | opcode::LOG4 => {
1127 if state.is_static {
1128 state.return_data = SymReturnData::empty(&mut self.cx);
1129 return Ok(StepOutcome::Revert);
1130 }
1131 let topics = (op - opcode::LOG0) as usize;
1132 let offset = state.stack.pop()?;
1133 if offset.contains_gasleft() {
1134 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1135 }
1136 let size = state.stack.pop()?;
1137 if size.contains_gasleft() {
1138 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1139 }
1140 let (data_len, data) = match state.constrained_usize_checked(&mut self.cx, &size) {
1141 Some(Ok(size)) => (
1142 SymExpr::constant(&mut self.cx, U256::from(size)),
1143 state.memory.read_bytes_offset(&mut self.cx, offset, size),
1144 ),
1145 Some(Err(_)) => {
1146 return Ok(StepOutcome::Revert);
1147 }
1148 None => {
1149 let max_limit = self.config.max_calldata_bytes as usize;
1150 let max_size = state
1151 .upper_bound_usize(&mut self.cx, &size)
1152 .filter(|size| *size <= max_limit)
1153 .map(Ok)
1154 .unwrap_or_else(|| {
1155 self.solver_upper_bound_usize(
1156 state,
1157 &size,
1158 max_limit,
1159 "symbolic LOG size",
1160 )
1161 })?;
1162 let data = state.memory.read_bytes_symbolic_size(
1163 &mut self.cx,
1164 offset,
1165 size.clone(),
1166 max_size,
1167 );
1168 (size, data)
1169 }
1170 };
1171 let mut log_topics = Vec::with_capacity(topics);
1172 for _ in 0..topics {
1173 let topic = state.stack.pop()?;
1174 if topic.contains_gasleft() {
1175 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1176 }
1177 log_topics.push(topic);
1178 }
1179 return self.handle_log(
1180 state,
1181 SymbolicLog::new(log_topics, data_len, data, state.address),
1182 );
1183 }
1184 _ => return Err(SymbolicError::UnsupportedOpcode(op)),
1185 };
1186
1187 Ok(StepOutcome::Continue)
1188 }
1189
1190 pub(super) fn assume_returndata_copy_in_bounds(
1191 &mut self,
1192 state: &mut PathState,
1193 offset: SymExpr,
1194 size: SymExpr,
1195 ) -> Result<bool, SymbolicError> {
1196 if offset.contains_gasleft() || size.contains_gasleft() {
1197 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
1198 }
1199 let end = SymExpr::binop(&mut self.cx, SymBinOp::Add, offset, size);
1200 let in_bounds =
1201 SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, end, state.return_data.len_expr());
1202 match in_bounds.as_const() {
1203 Some(value) => Ok(value),
1204 None => {
1205 let mut constraints = state.constraints.clone();
1206 constraints.push(in_bounds);
1207 if self.solver.is_sat(&mut self.cx, &constraints)? {
1208 state.constraints = constraints;
1209 Ok(true)
1210 } else {
1211 Ok(false)
1212 }
1213 }
1214 }
1215 }
1216
1217 pub(super) fn return_or_revert(
1218 &mut self,
1219 state: &mut PathState,
1220 is_revert: bool,
1221 ) -> Result<StepOutcome, SymbolicError> {
1222 let offset = state.stack.pop()?;
1223 let size = state.stack.pop()?;
1224 match state.constrained_usize_checked(&mut self.cx, &size) {
1225 Some(Ok(size)) => {
1226 state.return_data = state.memory.return_data(&mut self.cx, offset.clone(), size)?;
1227 if is_revert {
1228 Ok(self.classify_revert(state, offset, size))
1229 } else {
1230 Ok(StepOutcome::Halt)
1231 }
1232 }
1233 Some(Err(_)) => Ok(StepOutcome::Revert),
1234 None => {
1235 let max_limit = self.config.max_calldata_bytes as usize;
1236 let max_size = state
1237 .upper_bound_usize(&mut self.cx, &size)
1238 .filter(|size| *size <= max_limit)
1239 .map(Ok)
1240 .unwrap_or_else(|| {
1241 self.solver_upper_bound_usize(
1242 state,
1243 &size,
1244 max_limit,
1245 if is_revert { "symbolic REVERT size" } else { "symbolic RETURN size" },
1246 )
1247 })?;
1248 state.return_data =
1249 state.memory.return_data_symbolic_size(&mut self.cx, offset, size, max_size)?;
1250 Ok(if is_revert { StepOutcome::Revert } else { StepOutcome::Halt })
1251 }
1252 }
1253 }
1254
1255 pub(super) fn classify_revert(
1256 &mut self,
1257 state: &PathState,
1258 offset: SymExpr,
1259 size: usize,
1260 ) -> StepOutcome {
1261 if state.call_depth == 0
1262 && let Some(offset) = offset.as_const()
1263 && let Ok(offset) = usize::try_from(offset)
1264 && let Ok(data) = state.memory.read_concrete(&mut self.cx, offset, size)
1265 && is_assertion_revert(&data)
1266 {
1267 StepOutcome::Failure
1268 } else {
1269 StepOutcome::Revert
1270 }
1271 }
1272}
1273
1274#[cfg(test)]
1275mod tests {
1276 use super::*;
1277
1278 fn empty_state(executor: &mut SymbolicExecutor) -> PathState {
1279 let calldata =
1280 SymbolicCalldata::selector_only(&mut executor.cx, &Function::parse("empty()").unwrap())
1281 .unwrap();
1282 PathState::new(&mut executor.cx, Address::ZERO, Address::ZERO, U256::ZERO, calldata, false)
1283 }
1284
1285 #[test]
1286 fn branch_target_constraint_is_one_shot_after_target_reached() {
1287 let mut executor = SymbolicExecutor::new(SymbolicConfig::default());
1288 let mut state = empty_state(&mut executor);
1289 state.set_branch_target(Some(SymbolicBranchTarget::new(
1290 Address::ZERO,
1291 0,
1292 opcode::EQ,
1293 false,
1294 )));
1295 state.mark_branch_target_reached();
1296
1297 let condition = SymBoolExpr::constant(&mut executor.cx, false);
1298 let accepted =
1299 executor.apply_branch_target_constraint(&mut state, 0, opcode::EQ, &condition).unwrap();
1300
1301 assert!(accepted);
1302 assert!(state.constraints.is_empty());
1303 assert!(state.satisfies_branch_target());
1304 }
1305}