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