1use super::*;
2
3impl SymbolicExecutor {
4 fn push_comparison_result(
5 &mut self,
6 state: &mut PathState,
7 op_pc: usize,
8 opcode: u8,
9 condition: SymBoolExpr,
10 ) -> Result<StepOutcome, SymbolicError> {
11 if !self.apply_branch_target_constraint(state, op_pc, opcode, &condition)? {
12 return Ok(StepOutcome::AssumeRejected);
13 }
14 let value = SymExpr::bool_word(&mut self.cx, condition);
15 state.stack.push(value)?;
16 Ok(StepOutcome::Continue)
17 }
18
19 fn apply_branch_target_constraint(
20 &mut self,
21 state: &mut PathState,
22 op_pc: usize,
23 opcode: u8,
24 condition: &SymBoolExpr,
25 ) -> Result<bool, SymbolicError> {
26 let Some(target) = state.branch_target() else {
27 return Ok(true);
28 };
29 if state.satisfies_branch_target() {
30 return Ok(true);
31 }
32 if !target.matches(state.address, op_pc, opcode) {
33 return Ok(true);
34 }
35
36 let desired =
37 if target.result() { condition.clone().not(&mut self.cx) } else { condition.clone() };
38 let mut constraints = state.constraints.clone();
39 constraints.push(desired);
40 if !self.branch_is_sat_or_defer(&constraints)? {
41 return Ok(false);
42 }
43 state.constraints = constraints;
44 state.mark_branch_target_reached();
45 Ok(true)
46 }
47
48 #[expect(clippy::too_many_arguments)]
49 pub(super) fn step<FEN: FoundryEvmNetwork>(
50 &mut self,
51 executor: &Executor<FEN>,
52 code: &SymCode,
53 jumpdests: &JumpTable,
54 state: &mut PathState,
55 worklist: &mut VecDeque<PathState>,
56 completed_paths: &mut usize,
57 op: u8,
58 ) -> Result<StepOutcome, SymbolicError> {
59 state.pc += 1;
60
61 match op {
62 opcode::PUSH0 => {
63 state.stack.push(SymExpr::zero(&mut self.cx))?;
64 }
65 opcode::PUSH1..=opcode::PUSH32 => {
66 let n = (op - opcode::PUSH1 + 1) as usize;
67 let end = state.pc.saturating_add(n);
68 if end > code.len() {
69 return Err(SymbolicError::InvalidBytecode("truncated PUSH data"));
70 }
71 let value = code.push_data_word(&mut self.cx, state.pc, n);
72 state.pc = end;
73 state.stack.push(value)?;
74 }
75 opcode::DUP1..=opcode::DUP16 => {
76 let n = (op - opcode::DUP1 + 1) as usize;
77 let value = state.stack.peek(n - 1)?.clone();
78 state.stack.push(value)?;
79 }
80 opcode::SWAP1..=opcode::SWAP16 => {
81 let n = (op - opcode::SWAP1 + 1) as usize;
82 state.stack.swap(n)?;
83 }
84 opcode::STOP => return Ok(StepOutcome::Halt),
85 opcode::ADD => {
86 state.bin_word(&mut self.cx, SymBinOp::Add)?;
87 }
88 opcode::SUB => {
89 state.bin_word(&mut self.cx, SymBinOp::Sub)?;
90 }
91 opcode::MUL => {
92 state.bin_word(&mut self.cx, SymBinOp::Mul)?;
93 }
94 opcode::EXP => {
95 state.exp_word(&mut self.cx)?;
96 }
97 opcode::DIV => {
98 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::UDiv)?;
99 }
100 opcode::SDIV => {
101 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::SDiv)?;
102 }
103 opcode::MOD => {
104 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::URem)?;
105 }
106 opcode::SMOD => {
107 state.bin_word_div_zero_guard(&mut self.cx, SymBinOp::SRem)?;
108 }
109 opcode::ADDMOD => {
110 let a = state.stack.pop()?;
111 let b = state.stack.pop()?;
112 let n = state.stack.pop()?;
113 state.stack.push(SymExpr::ternop(&mut self.cx, SymTernOp::AddMod, a, b, n))?;
114 }
115 opcode::MULMOD => {
116 let a = state.stack.pop()?;
117 let b = state.stack.pop()?;
118 let n = state.stack.pop()?;
119 state.stack.push(SymExpr::ternop(&mut self.cx, SymTernOp::MulMod, a, b, n))?;
120 }
121 opcode::LT => {
122 let op_pc = state.pc - 1;
123 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Ult)?;
124 return self.push_comparison_result(state, op_pc, op, condition);
125 }
126 opcode::GT => {
127 let op_pc = state.pc - 1;
128 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Ugt)?;
129 return self.push_comparison_result(state, op_pc, op, condition);
130 }
131 opcode::SLT => {
132 let op_pc = state.pc - 1;
133 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Slt)?;
134 return self.push_comparison_result(state, op_pc, op, condition);
135 }
136 opcode::SGT => {
137 let op_pc = state.pc - 1;
138 let condition = state.cmp_word_condition(&mut self.cx, SymCmpOp::Sgt)?;
139 return self.push_comparison_result(state, op_pc, op, condition);
140 }
141 opcode::EQ => {
142 let op_pc = state.pc - 1;
143 let a = state.stack.pop()?;
144 let b = state.stack.pop()?;
145 let condition = SymBoolExpr::eq(&mut self.cx, b, a);
146 return self.push_comparison_result(state, op_pc, op, condition);
147 }
148 opcode::ISZERO => {
149 let op_pc = state.pc - 1;
150 let value = state.stack.pop()?;
151 let value = value.into_zero_bool(&mut self.cx);
152 return self.push_comparison_result(state, op_pc, op, value);
153 }
154 opcode::AND => {
155 state.bin_word(&mut self.cx, SymBinOp::And)?;
156 }
157 opcode::OR => {
158 state.bin_word(&mut self.cx, SymBinOp::Or)?;
159 }
160 opcode::XOR => {
161 state.bin_word(&mut self.cx, SymBinOp::Xor)?;
162 }
163 opcode::NOT => {
164 let value = state.stack.pop()?;
165 state.stack.push(SymExpr::not(&mut self.cx, value))?;
166 }
167 opcode::SIGNEXTEND => {
168 let byte_index = state.stack.pop()?;
169 let value = state.stack.pop()?;
170 state.stack.push(signextend_word_dynamic(&mut self.cx, byte_index, value))?;
171 }
172 opcode::BYTE => {
173 let index = state.stack.pop()?;
174 let word = state.stack.pop()?;
175 state.stack.push(byte_word_dynamic(&mut self.cx, index, word))?;
176 }
177 opcode::SHL => {
178 state.shift_word(&mut self.cx, ShiftKind::Shl)?;
179 }
180 opcode::SHR => {
181 state.shift_word(&mut self.cx, ShiftKind::Shr)?;
182 }
183 opcode::SAR => {
184 state.shift_word(&mut self.cx, ShiftKind::Sar)?;
185 }
186 opcode::KECCAK256 => {
187 let offset = state.stack.pop()?;
188 let size = state.stack.pop()?;
189 match state.constrained_usize_checked(&mut self.cx, &size) {
190 Some(Ok(size)) => {
191 let bytes = state.memory.read_byte_exprs_offset(&mut self.cx, offset, size);
192 state.stack.push(keccak_word(&mut self.cx, bytes))?;
193 }
194 Some(Err(_)) => {
195 return Ok(StepOutcome::Revert);
196 }
197 None => {
198 let max_limit = self.config.max_calldata_bytes as usize;
199 let max_size = state
200 .upper_bound_usize(&mut self.cx, &size)
201 .filter(|size| *size <= max_limit)
202 .map(Ok)
203 .unwrap_or_else(|| {
204 self.solver_upper_bound_usize(
205 state,
206 &size,
207 max_limit,
208 "symbolic SHA3 size",
209 )
210 })?;
211 let bytes = state.memory.read_byte_exprs_symbolic_size(
212 &mut self.cx,
213 offset,
214 size.clone(),
215 max_size,
216 );
217 state.stack.push(keccak_word_with_len(&mut self.cx, bytes, size))?;
218 }
219 }
220 }
221 opcode::ADDRESS => {
222 let address = state.address_word.clone();
223 state.stack.push(address)?;
224 }
225 opcode::CALLER => {
226 let caller = state.caller_word.clone();
227 state.stack.push(caller)?;
228 }
229 opcode::ORIGIN => {
230 let origin = state.origin_word.clone();
231 state.stack.push(origin)?;
232 }
233 opcode::CALLVALUE => {
234 let callvalue = state.callvalue.clone();
235 state.stack.push(callvalue)?;
236 }
237 opcode::BLOCKHASH => {
238 let number = state.stack.pop()?;
239 let hash = state.block.block_hash_word(&mut self.cx, executor, number)?;
240 state.stack.push(hash)?;
241 }
242 opcode::BALANCE => {
243 let target = state.stack.pop()?;
244 let balance = state.balance_word(&mut self.cx, executor, target)?;
245 state.stack.push(balance)?;
246 }
247 opcode::SELFBALANCE => {
248 let balance = state.balance(&mut self.cx, executor, state.address);
249 state.stack.push(balance)?;
250 }
251 opcode::EXTCODESIZE => {
252 let target = state.stack.pop()?;
253 let size = state.extcode_size_word(&mut self.cx, executor, target)?;
254 state.stack.push(size)?;
255 }
256 opcode::EXTCODEHASH => {
257 let target = state.stack.pop()?;
258 let hash = state.extcode_hash_word(&mut self.cx, executor, target)?;
259 state.stack.push(hash)?;
260 }
261 opcode::EXTCODECOPY => {
262 let target = state.stack.pop()?;
263 let dest = state.stack.pop()?;
264 let offset = state.stack.pop()?;
265 let size = state.stack.pop()?;
266 match state.constrained_usize_checked(&mut self.cx, &size) {
267 Some(Ok(size)) => {
268 let bytes = state.extcode_bytes_word(
269 &mut self.cx,
270 executor,
271 target,
272 offset,
273 size,
274 )?;
275 state.memory.copy_bytes_offset(&mut self.cx, dest, bytes);
276 }
277 Some(Err(_)) => {
278 return Ok(StepOutcome::Revert);
279 }
280 None => {
281 let max_limit = self.config.max_calldata_bytes as usize;
282 let max_size = state
283 .upper_bound_usize(&mut self.cx, &size)
284 .filter(|size| *size <= max_limit)
285 .map(Ok)
286 .unwrap_or_else(|| {
287 self.solver_upper_bound_usize(
288 state,
289 &size,
290 max_limit,
291 "symbolic EXTCODECOPY size",
292 )
293 })?;
294 if max_size != 0 {
295 let bytes = state.extcode_bytes_word(
296 &mut self.cx,
297 executor,
298 target,
299 offset,
300 max_size,
301 )?;
302 state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
303 }
304 }
305 }
306 }
307 opcode::CALLDATALOAD => {
308 let offset = state.stack.pop()?;
309 let value = state.calldata.load_word(&mut self.cx, offset)?;
310 state.stack.push(value)?;
311 }
312 opcode::CALLDATASIZE => {
313 let size = state.calldata.size_word();
314 state.stack.push(size)?;
315 }
316 opcode::CALLDATACOPY => {
317 let dest = state.stack.pop()?;
318 let offset = state.stack.pop()?;
319 let size = state.stack.pop()?;
320 match state.constrained_usize_checked(&mut self.cx, &size) {
321 Some(Ok(size)) => {
322 if size != 0 {
323 state.copy_calldata_to_offset(&mut self.cx, dest, offset, size)?;
324 }
325 }
326 Some(Err(_)) => {
327 return Ok(StepOutcome::Revert);
328 }
329 None => {
330 let max_limit = self.config.max_calldata_bytes as usize;
331 let max_size = state
332 .upper_bound_usize(&mut self.cx, &size)
333 .filter(|size| *size <= max_limit)
334 .map(Ok)
335 .unwrap_or_else(|| {
336 self.solver_upper_bound_usize(
337 state,
338 &size,
339 max_limit,
340 "symbolic CALLDATACOPY size",
341 )
342 })?;
343 if max_size != 0 {
344 state.copy_calldata_symbolic_size(
345 &mut self.cx,
346 dest,
347 offset,
348 size,
349 max_size,
350 )?;
351 }
352 }
353 }
354 }
355 opcode::CODESIZE => {
356 let value = SymExpr::constant(&mut self.cx, U256::from(code.len()));
357 state.stack.push(value)?;
358 }
359 opcode::CODECOPY => {
360 let dest = state.stack.pop()?;
361 let offset = state.stack.pop()?;
362 let size = state.stack.pop()?;
363 match state.constrained_usize_checked(&mut self.cx, &size) {
364 Some(Ok(size)) => {
365 let bytes = code.read_bytes_offset(&mut self.cx, offset, size);
366 state.memory.copy_bytes_offset(&mut self.cx, dest, bytes);
367 }
368 Some(Err(_)) => {
369 return Ok(StepOutcome::Revert);
370 }
371 None => {
372 let max_limit = self.config.max_calldata_bytes as usize;
373 let max_size = state
374 .upper_bound_usize(&mut self.cx, &size)
375 .filter(|size| *size <= max_limit)
376 .map(Ok)
377 .unwrap_or_else(|| {
378 self.solver_upper_bound_usize(
379 state,
380 &size,
381 max_limit,
382 "symbolic CODECOPY size",
383 )
384 })?;
385 if max_size != 0 {
386 let bytes = code.read_bytes_offset(&mut self.cx, offset, max_size);
387 state.memory.copy_bytes_size_offset(&mut self.cx, dest, size, bytes)?;
388 }
389 }
390 }
391 }
392 opcode::RETURNDATASIZE => {
393 let size = state.return_data.len_word();
394 state.stack.push(size)?;
395 }
396 opcode::RETURNDATACOPY => {
397 let dest = state.stack.pop()?;
398 let offset = state.stack.pop()?;
399 let size = state.stack.pop()?;
400 match state.constrained_usize_checked(&mut self.cx, &size) {
401 Some(Ok(size)) => {
402 let size_word = SymExpr::constant(&mut self.cx, U256::from(size));
403 if !self.assume_returndata_copy_in_bounds(
404 state,
405 offset.clone(),
406 size_word,
407 )? {
408 return Ok(StepOutcome::Revert);
409 }
410 state.copy_return_data_to_offset(&mut self.cx, dest, offset, size)?;
411 }
412 Some(Err(_)) => {
413 return Ok(StepOutcome::Revert);
414 }
415 None => {
416 let available = state
417 .constrained_usize(&mut self.cx, &offset)
418 .map(|offset| state.return_data.len().saturating_sub(offset))
419 .unwrap_or(state.return_data.len());
420 let max_limit = available.min(self.config.max_calldata_bytes as usize);
421 let max_size = state
422 .upper_bound_usize(&mut self.cx, &size)
423 .filter(|size| *size <= max_limit)
424 .map(Ok)
425 .unwrap_or_else(|| {
426 self.solver_upper_bound_usize(
427 state,
428 &size,
429 max_limit,
430 "symbolic RETURNDATACOPY size",
431 )
432 })?;
433 if max_size != 0 {
434 if !self.assume_returndata_copy_in_bounds(
435 state,
436 offset.clone(),
437 size.clone(),
438 )? {
439 return Ok(StepOutcome::Revert);
440 }
441 state.copy_return_data_symbolic_size(
442 &mut self.cx,
443 dest,
444 offset,
445 size,
446 max_size,
447 )?;
448 }
449 }
450 }
451 }
452 opcode::POP => {
453 state.stack.pop()?;
454 }
455 opcode::MLOAD => {
456 let offset = state.stack.pop()?;
457 let value = state.memory.load_word_offset(&mut self.cx, offset)?;
458 state.stack.push(value)?;
459 }
460 opcode::MSTORE => {
461 let offset = state.stack.pop()?;
462 let value = state.stack.pop()?;
463 state.memory.store_word_offset(&mut self.cx, offset, value);
464 }
465 opcode::MSTORE8 => {
466 let offset = state.stack.pop()?;
467 let value = state.stack.pop()?;
468 state.memory.store_byte_offset(&mut self.cx, offset, value);
469 }
470 opcode::SLOAD => {
471 let key = state.stack.pop()?;
472 state.record_sload(state.storage_address, key.clone());
473 let concrete_key = state.constrained_word(&mut self.cx, &key);
474 let value = state.world.sload(
475 &mut self.cx,
476 executor,
477 state.storage_address,
478 key,
479 concrete_key,
480 )?;
481 state.stack.push(value)?;
482 }
483 opcode::SSTORE => {
484 if state.is_static {
485 state.return_data = SymReturnData::empty(&mut self.cx);
486 return Ok(StepOutcome::Revert);
487 }
488 let key = state.stack.pop()?;
489 let value = state.stack.pop()?;
490 state.record_sstore(state.storage_address, key.clone());
491 state.world.sstore(state.storage_address, key, value);
492 }
493 opcode::TLOAD => {
494 let key = state.stack.pop()?;
495 let value = state.world.tload(&mut self.cx, state.storage_address, key);
496 state.stack.push(value)?;
497 }
498 opcode::TSTORE => {
499 if state.is_static {
500 state.return_data = SymReturnData::empty(&mut self.cx);
501 return Ok(StepOutcome::Revert);
502 }
503 let key = state.stack.pop()?;
504 let value = state.stack.pop()?;
505 state.world.tstore(state.storage_address, key, value);
506 }
507 opcode::JUMP => {
508 let dest = state.stack.pop()?;
509 let dest = state.expect_constrained_usize(
510 &mut self.cx,
511 dest,
512 "symbolic JUMP destination",
513 )?;
514 ensure_jumpdest(dest, jumpdests)?;
515 if !self.take_loop_jump(state, state.pc, dest) {
516 return Ok(StepOutcome::AssumeRejected);
517 }
518 state.pc = dest;
519 }
520 opcode::JUMPI => {
521 let dest = state.stack.pop()?;
522 let dest = state.expect_constrained_usize(
523 &mut self.cx,
524 dest,
525 "symbolic JUMPI destination",
526 )?;
527 ensure_jumpdest(dest, jumpdests)?;
528 let cond = state.stack.pop()?;
529 match cond.truth() {
530 Some(true) => {
531 if !self.take_loop_jump(state, state.pc, dest) {
532 return Ok(StepOutcome::AssumeRejected);
533 }
534 state.pc = dest;
535 }
536 Some(false) => {}
537 None => {
538 let op_pc = state.pc.saturating_sub(1);
539 let _branch_span = trace_span!("jumpi_branch", pc = op_pc, dest).entered();
540 let true_cond = cond.nonzero_bool(&mut self.cx);
541 let false_cond = true_cond.clone().not(&mut self.cx);
542 let fallthrough = state.pc;
543 let (true_seed_models, false_seed_models) =
544 state.split_corpus_seed_models(&true_cond);
545 let mut true_state = state.clone();
546 true_state.constraints.push(true_cond);
547 true_state.set_corpus_seed_models(true_seed_models);
548 true_state.pc = dest;
549 let mut false_state = state.clone();
550 false_state.constraints.push(false_cond);
551 false_state.set_corpus_seed_models(false_seed_models);
552 false_state.pc = fallthrough;
553
554 let true_pending = self.take_loop_jump(&mut true_state, fallthrough, dest);
555 if true_pending {
556 true_state.defer_feasibility_check();
557 }
558 false_state.defer_feasibility_check();
559 trace!(true_pending, false_pending = true, "JUMPI symbolic branch");
560 if true_pending {
561 let true_seed_count = true_state.corpus_seed_model_count();
562 let false_seed_count = false_state.corpus_seed_model_count();
563 match (
564 false_seed_count.cmp(&true_seed_count),
565 self.config.exploration_order,
566 ) {
567 (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Bfs)
568 | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Dfs) => {
569 worklist.push_back(false_state);
570 worklist.push_back(true_state);
571 }
572 (std::cmp::Ordering::Greater, SymbolicExplorationOrder::Dfs)
573 | (std::cmp::Ordering::Less, SymbolicExplorationOrder::Bfs)
574 | (std::cmp::Ordering::Equal, _) => {
575 worklist.push_back(true_state);
576 worklist.push_back(false_state);
577 }
578 }
579 } else {
580 worklist.push_back(false_state);
581 }
582 return Ok(StepOutcome::Forked);
583 }
584 }
585 }
586 opcode::PC => {
587 let pc = state.pc - 1;
588 let pc = SymExpr::constant(&mut self.cx, U256::from(pc));
589 state.stack.push(pc)?;
590 }
591 opcode::MSIZE => {
592 let size = state.memory.size_word(&mut self.cx);
593 state.stack.push(size)?;
594 }
595 opcode::GAS => {
596 let gas = state.fresh_gasleft(&mut self.cx);
597 state.stack.push(gas)?;
598 }
599 opcode::JUMPDEST => {}
600 opcode::MCOPY => {
601 let dest = state.stack.pop()?;
602 let src = state.stack.pop()?;
603 let size = state.stack.pop()?;
604 match state.constrained_usize_checked(&mut self.cx, &size) {
605 Some(Ok(size)) => {
606 state.memory.copy_memory_to_offset(&mut self.cx, dest, src, size)?;
607 }
608 Some(Err(_)) => {
609 return Ok(StepOutcome::Revert);
610 }
611 None => {
612 let max_limit = self.config.max_calldata_bytes as usize;
613 let max_size = state
614 .upper_bound_usize(&mut self.cx, &size)
615 .filter(|size| *size <= max_limit)
616 .map(Ok)
617 .unwrap_or_else(|| {
618 self.solver_upper_bound_usize(
619 state,
620 &size,
621 max_limit,
622 "symbolic MCOPY size",
623 )
624 })?;
625 if max_size != 0 {
626 state.memory.copy_memory_symbolic_size(
627 &mut self.cx,
628 dest,
629 src,
630 size,
631 max_size,
632 )?;
633 }
634 }
635 }
636 }
637 opcode::RETURN => return self.return_or_revert(state, false),
638 opcode::REVERT => return self.return_or_revert(state, true),
639 opcode::INVALID => return Ok(StepOutcome::Failure),
640 opcode::CALL => {
641 return self.call(executor, state, worklist, completed_paths, CallKind::Call);
642 }
643 opcode::CALLCODE => {
644 return self.call(executor, state, worklist, completed_paths, CallKind::CallCode);
645 }
646 opcode::DELEGATECALL => {
647 return self.call(
648 executor,
649 state,
650 worklist,
651 completed_paths,
652 CallKind::DelegateCall,
653 );
654 }
655 opcode::STATICCALL => {
656 return self.call(executor, state, worklist, completed_paths, CallKind::StaticCall);
657 }
658 opcode::CREATE => {
659 return self.create(executor, state, worklist, completed_paths, CreateKind::Create);
660 }
661 opcode::CREATE2 => {
662 return self.create(
663 executor,
664 state,
665 worklist,
666 completed_paths,
667 CreateKind::Create2,
668 );
669 }
670 opcode::SELFDESTRUCT => {
671 if state.is_static {
672 state.return_data = SymReturnData::empty(&mut self.cx);
673 return Ok(StepOutcome::Revert);
674 }
675 let spec_id: SpecId = executor.spec_id().into();
676 let (beneficiary_word, beneficiary) =
677 state.pop_address_word_or_symbolic_slot(&mut self.cx)?;
678 if spec_id < SpecId::CANCUN
679 || state.world.was_created_in_current_transaction(state.address)
680 {
681 state.world.selfdestruct_legacy(
682 &mut self.cx,
683 executor,
684 state.address,
685 beneficiary,
686 )?;
687 } else {
688 if state.constrained_word(&mut self.cx, &beneficiary_word).is_none() {
689 return Err(SymbolicError::Unsupported(
690 "symbolic SELFDESTRUCT beneficiary",
691 ));
692 }
693 state.world.selfdestruct_cancun_existing(
694 &mut self.cx,
695 executor,
696 state.address,
697 beneficiary,
698 );
699 }
700 state.return_data = SymReturnData::empty(&mut self.cx);
701 return Ok(StepOutcome::Halt);
702 }
703 opcode::CHAINID => {
704 let value = state.block.chain_id.clone();
705 state.stack.push(value)?;
706 }
707 opcode::BASEFEE => {
708 let value = state.block.basefee.clone();
709 state.stack.push(value)?;
710 }
711 opcode::GASPRICE => {
712 let gas_price = state.gas_price.clone();
713 state.stack.push(gas_price)?;
714 }
715 opcode::BLOBHASH => {
716 let index = state.stack.pop()?;
717 let index = state.expect_constrained_usize(
718 &mut self.cx,
719 index,
720 "symbolic BLOBHASH index",
721 )?;
722 let hash = state.block.blob_hash(index);
723 let hash = SymExpr::constant(&mut self.cx, U256::from_be_slice(hash.as_slice()));
724 state.stack.push(hash)?;
725 }
726 opcode::COINBASE => {
727 let coinbase = state.block.coinbase;
728 let coinbase = SymExpr::constant(&mut self.cx, address_word(coinbase));
729 state.stack.push(coinbase)?;
730 }
731 opcode::TIMESTAMP => {
732 let value = state.block.timestamp.clone();
733 state.stack.push(value)?;
734 }
735 opcode::NUMBER => {
736 let value = state.block.number.clone();
737 state.stack.push(value)?;
738 }
739 opcode::DIFFICULTY => {
740 let value = state.block.difficulty.clone();
741 state.stack.push(value)?;
742 }
743 opcode::GASLIMIT => {
744 let value = state.block.gaslimit.clone();
745 state.stack.push(value)?;
746 }
747 opcode::BLOBBASEFEE => {
748 let value = state.block.blob_basefee.clone();
749 state.stack.push(value)?;
750 }
751 opcode::LOG0 | opcode::LOG1 | opcode::LOG2 | opcode::LOG3 | opcode::LOG4 => {
752 if state.is_static {
753 state.return_data = SymReturnData::empty(&mut self.cx);
754 return Ok(StepOutcome::Revert);
755 }
756 let topics = (op - opcode::LOG0) as usize;
757 let offset = state.stack.pop()?;
758 if offset.contains_gasleft() {
759 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
760 }
761 let size = state.stack.pop()?;
762 if size.contains_gasleft() {
763 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
764 }
765 let (data_len, data) = match state.constrained_usize_checked(&mut self.cx, &size) {
766 Some(Ok(size)) => (
767 SymExpr::constant(&mut self.cx, U256::from(size)),
768 state.memory.read_bytes_offset(&mut self.cx, offset, size),
769 ),
770 Some(Err(_)) => {
771 return Ok(StepOutcome::Revert);
772 }
773 None => {
774 let max_limit = self.config.max_calldata_bytes as usize;
775 let max_size = state
776 .upper_bound_usize(&mut self.cx, &size)
777 .filter(|size| *size <= max_limit)
778 .map(Ok)
779 .unwrap_or_else(|| {
780 self.solver_upper_bound_usize(
781 state,
782 &size,
783 max_limit,
784 "symbolic LOG size",
785 )
786 })?;
787 let data = state.memory.read_bytes_symbolic_size(
788 &mut self.cx,
789 offset,
790 size.clone(),
791 max_size,
792 );
793 (size, data)
794 }
795 };
796 let mut log_topics = Vec::with_capacity(topics);
797 for _ in 0..topics {
798 let topic = state.stack.pop()?;
799 if topic.contains_gasleft() {
800 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
801 }
802 log_topics.push(topic);
803 }
804 return self.handle_log(
805 state,
806 SymbolicLog::new(log_topics, data_len, data, state.address),
807 );
808 }
809 _ => return Err(SymbolicError::UnsupportedOpcode(op)),
810 };
811
812 Ok(StepOutcome::Continue)
813 }
814
815 pub(super) fn assume_returndata_copy_in_bounds(
816 &mut self,
817 state: &mut PathState,
818 offset: SymExpr,
819 size: SymExpr,
820 ) -> Result<bool, SymbolicError> {
821 if offset.contains_gasleft() || size.contains_gasleft() {
822 return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled"));
823 }
824 let end = SymExpr::binop(&mut self.cx, SymBinOp::Add, offset, size);
825 let in_bounds =
826 SymBoolExpr::cmp(&mut self.cx, SymCmpOp::Ule, end, state.return_data.len_expr());
827 match in_bounds.as_const() {
828 Some(value) => Ok(value),
829 None => {
830 let mut constraints = state.constraints.clone();
831 constraints.push(in_bounds);
832 if self.solver.is_sat(&mut self.cx, &constraints)? {
833 state.constraints = constraints;
834 Ok(true)
835 } else {
836 Ok(false)
837 }
838 }
839 }
840 }
841
842 pub(super) fn return_or_revert(
843 &mut self,
844 state: &mut PathState,
845 is_revert: bool,
846 ) -> Result<StepOutcome, SymbolicError> {
847 let offset = state.stack.pop()?;
848 let size = state.stack.pop()?;
849 match state.constrained_usize_checked(&mut self.cx, &size) {
850 Some(Ok(size)) => {
851 state.return_data = state.memory.return_data(&mut self.cx, offset.clone(), size)?;
852 if is_revert {
853 Ok(self.classify_revert(state, offset, size))
854 } else {
855 Ok(StepOutcome::Halt)
856 }
857 }
858 Some(Err(_)) => Ok(StepOutcome::Revert),
859 None => {
860 let max_limit = self.config.max_calldata_bytes as usize;
861 let max_size = state
862 .upper_bound_usize(&mut self.cx, &size)
863 .filter(|size| *size <= max_limit)
864 .map(Ok)
865 .unwrap_or_else(|| {
866 self.solver_upper_bound_usize(
867 state,
868 &size,
869 max_limit,
870 if is_revert { "symbolic REVERT size" } else { "symbolic RETURN size" },
871 )
872 })?;
873 state.return_data =
874 state.memory.return_data_symbolic_size(&mut self.cx, offset, size, max_size)?;
875 Ok(if is_revert { StepOutcome::Revert } else { StepOutcome::Halt })
876 }
877 }
878 }
879
880 pub(super) fn classify_revert(
881 &mut self,
882 state: &PathState,
883 offset: SymExpr,
884 size: usize,
885 ) -> StepOutcome {
886 if state.call_depth == 0
887 && let Some(offset) = offset.as_const()
888 && let Ok(offset) = usize::try_from(offset)
889 && let Ok(data) = state.memory.read_concrete(&mut self.cx, offset, size)
890 && is_assertion_revert(&data)
891 {
892 StepOutcome::Failure
893 } else {
894 StepOutcome::Revert
895 }
896 }
897}
898
899#[cfg(test)]
900mod tests {
901 use super::*;
902
903 fn empty_state(executor: &mut SymbolicExecutor) -> PathState {
904 let calldata =
905 SymbolicCalldata::selector_only(&mut executor.cx, &Function::parse("empty()").unwrap())
906 .unwrap();
907 PathState::new(&mut executor.cx, Address::ZERO, Address::ZERO, U256::ZERO, calldata, false)
908 }
909
910 #[test]
911 fn branch_target_constraint_is_one_shot_after_target_reached() {
912 let mut executor = SymbolicExecutor::new(SymbolicConfig::default());
913 let mut state = empty_state(&mut executor);
914 state.set_branch_target(Some(SymbolicBranchTarget::new(
915 Address::ZERO,
916 0,
917 opcode::EQ,
918 false,
919 )));
920 state.mark_branch_target_reached();
921
922 let condition = SymBoolExpr::constant(&mut executor.cx, false);
923 let accepted =
924 executor.apply_branch_target_constraint(&mut state, 0, opcode::EQ, &condition).unwrap();
925
926 assert!(accepted);
927 assert!(state.constraints.is_empty());
928 assert!(state.satisfies_branch_target());
929 }
930}