foundry_evm_symbolic/executor/mod.rs
1use super::{abi::*, runtime::*, *};
2
3mod calls;
4mod cheatcodes;
5mod constraints;
6mod create;
7mod invariant;
8mod opcodes;
9mod run;
10
11impl SymbolicExecutor {
12 pub(super) fn pop_next_path(&self, paths: &mut VecDeque<PathState>) -> Option<PathState> {
13 match self.config.exploration_order {
14 SymbolicExplorationOrder::Bfs => paths.pop_front(),
15 SymbolicExplorationOrder::Dfs => paths.pop_back(),
16 }
17 }
18
19 pub(super) fn pop_next_feasible_path(
20 &mut self,
21 paths: &mut VecDeque<PathState>,
22 ) -> Result<Option<PathState>, SymbolicError> {
23 while let Some(mut state) = self.pop_next_path(paths) {
24 if state.take_deferred_feasibility_check()
25 && !self.branch_is_sat_or_defer(&state.constraints)?
26 {
27 continue;
28 }
29 return Ok(Some(state));
30 }
31 Ok(None)
32 }
33}