refactor(symbolic): split executor into modules

crates/evm/symbolic/src/executor/constraints.rs

@@ -0,0 +1,227 @@
+use super::*;
+
+impl SymbolicExecutor {
+    /// Runs the `handle_assume` symbolic executor helper.
+    pub(super) fn handle_assume(
+        &mut self,
+        state: &mut PathState,
+        condition_offset: usize,
+    ) -> Result<CheatcodeOutcome, SymbolicError> {
+        let cond = state.memory.load_word(condition_offset)?;
+        self.assume_condition(state, cond.nonzero_bool())
+    }
+
+    /// Runs the `handle_skip` symbolic executor helper.
+    pub(super) fn handle_skip(
+        &mut self,
+        state: &mut PathState,
+        condition_offset: usize,
+    ) -> Result<CheatcodeOutcome, SymbolicError> {
+        let cond = state.memory.load_word(condition_offset)?;
+        self.assume_condition(state, cond.nonzero_bool().not())
+    }
+
+    /// Implements the `assume_condition` symbolic executor helper.
+    pub(super) fn assume_condition(
+        &mut self,
+        state: &mut PathState,
+        condition: BoolExpr,
+    ) -> Result<CheatcodeOutcome, SymbolicError> {
+        match condition {
+            BoolExpr::Const(true) => Ok(CheatcodeOutcome::Continue(Vec::new())),
+            BoolExpr::Const(false) => Ok(CheatcodeOutcome::AssumeRejected),
+            condition => {
+                state.constraints.push(condition);
+                if self.solver.is_sat(&state.constraints)? {
+                    Ok(CheatcodeOutcome::Continue(Vec::new()))
+                } else {
+                    Ok(CheatcodeOutcome::AssumeRejected)
+                }
+            }
+        }
+    }
+
+    /// Implements the `solver_upper_bound_usize` symbolic executor helper.
+    pub(super) fn solver_upper_bound_usize(
+        &mut self,
+        state: &PathState,
+        word: &SymWord,
+        max: usize,
+        reason: &'static str,
+    ) -> Result<usize, SymbolicError> {
+        let expr = word.clone().into_expr();
+        let mut above_max = state.constraints.clone();
+        above_max.push(BoolExpr::cmp(BoolExprOp::Ugt, expr.clone(), Expr::Const(U256::from(max))));
+        if self.solver.is_sat(&above_max)? {
+            return Err(SymbolicError::Unsupported(reason));
+        }
+
+        let mut low = 0usize;
+        let mut high = max;
+        while low < high {
+            let mid = low + (high - low) / 2;
+            let mut above_mid = state.constraints.clone();
+            above_mid.push(BoolExpr::cmp(
+                BoolExprOp::Ugt,
+                expr.clone(),
+                Expr::Const(U256::from(mid)),
+            ));
+            if self.solver.is_sat(&above_mid)? {
+                low = mid + 1;
+            } else {
+                high = mid;
+            }
+        }
+        Ok(low)
+    }
+
+    /// Implements the `assume_word_at_least` symbolic executor helper.
+    pub(super) fn assume_word_at_least(
+        &mut self,
+        state: &mut PathState,
+        word: &SymWord,
+        min: usize,
+    ) -> Result<bool, SymbolicError> {
+        let condition =
+            BoolExpr::cmp(BoolExprOp::Uge, word.clone().into_expr(), Expr::Const(U256::from(min)));
+        match condition {
+            BoolExpr::Const(value) => Ok(value),
+            condition => {
+                let mut constraints = state.constraints.clone();
+                constraints.push(condition);
+                if self.solver.is_sat(&constraints)? {
+                    state.constraints = constraints;
+                    Ok(true)
+                } else {
+                    Ok(false)
+                }
+            }
+        }
+    }
+
+    /// Rejects symbolic integer bit widths outside the EVM word size.
+    pub(super) fn validate_symbolic_integer_bits(
+        bits: U256,
+        context: &'static str,
+    ) -> Result<(), SymbolicError> {
+        if bits <= U256::from(256) { Ok(()) } else { Err(SymbolicError::Unsupported(context)) }
+    }
+
+    /// Runs the `handle_bound_uint` symbolic executor helper.
+    pub(super) fn handle_bound_uint(
+        &mut self,
+        state: &mut PathState,
+        args_offset: usize,
+    ) -> Result<CheatcodeOutcome, SymbolicError> {
+        let value = read_abi_word_arg(&state.memory, args_offset, 0)?;
+        let min = read_abi_word_arg(&state.memory, args_offset, 1)?;
+        let max = read_abi_word_arg(&state.memory, args_offset, 2)?;
+
+        if let (SymWord::Concrete(value), SymWord::Concrete(min), SymWord::Concrete(max)) =
+            (&value, &min, &max)
+        {
+            if min >= max || value < min || value > max {
+                return Ok(CheatcodeOutcome::Failure);
+            }
+            let bounded = if value == min { *max } else { *min };
+            return Ok(CheatcodeOutcome::Continue(vec![SymWord::Concrete(bounded)]));
+        }
+
+        if let (SymWord::Concrete(min), SymWord::Concrete(max)) = (&min, &max)
+            && min >= max
+        {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+        let (SymWord::Concrete(min_value), SymWord::Concrete(max_value)) = (&min, &max) else {
+            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
+        };
+
+        let value_expr = value.into_expr();
+        let in_range = BoolExpr::and(vec![
+            BoolExpr::cmp(BoolExprOp::Uge, value_expr.clone(), Expr::Const(*min_value)),
+            BoolExpr::cmp(BoolExprOp::Ule, value_expr.clone(), Expr::Const(*max_value)),
+        ]);
+        let (_in_range_constraints, in_range_sat) =
+            self.constraints_with_condition(state, in_range.clone())?;
+        if !in_range_sat {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+        let (_out_of_range_constraints, out_of_range_sat) =
+            self.constraints_with_condition(state, in_range.not())?;
+        if out_of_range_sat {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+
+        let bounded = state.fresh_word("vmBoundUint");
+        state.constraints.push(BoolExpr::cmp(
+            BoolExprOp::Uge,
+            bounded.clone().into_expr(),
+            Expr::Const(*min_value),
+        ));
+        state.constraints.push(BoolExpr::cmp(
+            BoolExprOp::Ule,
+            bounded.clone().into_expr(),
+            Expr::Const(*max_value),
+        ));
+        state.constraints.push(BoolExpr::eq(bounded.clone().into_expr(), value_expr).not());
+        Ok(CheatcodeOutcome::Continue(vec![bounded]))
+    }
+
+    /// Runs the `handle_bound_int` symbolic executor helper.
+    pub(super) fn handle_bound_int(
+        &mut self,
+        state: &mut PathState,
+        args_offset: usize,
+    ) -> Result<CheatcodeOutcome, SymbolicError> {
+        let value = read_abi_word_arg(&state.memory, args_offset, 0)?;
+        let min = read_abi_word_arg(&state.memory, args_offset, 1)?;
+        let max = read_abi_word_arg(&state.memory, args_offset, 2)?;
+
+        if let (SymWord::Concrete(value), SymWord::Concrete(min), SymWord::Concrete(max)) =
+            (&value, &min, &max)
+        {
+            if !slt(*min, *max) || slt(*value, *min) || slt(*max, *value) {
+                return Ok(CheatcodeOutcome::Failure);
+            }
+            let bounded = if value == min { *max } else { *min };
+            return Ok(CheatcodeOutcome::Continue(vec![SymWord::Concrete(bounded)]));
+        }
+
+        if let (SymWord::Concrete(min), SymWord::Concrete(max)) = (&min, &max)
+            && !slt(*min, *max)
+        {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+        let (SymWord::Concrete(min_value), SymWord::Concrete(max_value)) = (&min, &max) else {
+            return Err(SymbolicError::Unsupported("symbolic vm.bound range"));
+        };
+
+        let value_expr = value.into_expr();
+        let in_range = BoolExpr::and(vec![
+            BoolExpr::cmp(BoolExprOp::Slt, value_expr.clone(), Expr::Const(*min_value)).not(),
+            BoolExpr::cmp(BoolExprOp::Sgt, value_expr.clone(), Expr::Const(*max_value)).not(),
+        ]);
+        let (_in_range_constraints, in_range_sat) =
+            self.constraints_with_condition(state, in_range.clone())?;
+        if !in_range_sat {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+        let (_out_of_range_constraints, out_of_range_sat) =
+            self.constraints_with_condition(state, in_range.not())?;
+        if out_of_range_sat {
+            return Ok(CheatcodeOutcome::Failure);
+        }
+
+        let bounded = state.fresh_word("vmBoundInt");
+        state.constraints.push(
+            BoolExpr::cmp(BoolExprOp::Slt, bounded.clone().into_expr(), Expr::Const(*min_value))
+                .not(),
+        );
+        state.constraints.push(
+            BoolExpr::cmp(BoolExprOp::Sgt, bounded.clone().into_expr(), Expr::Const(*max_value))
+                .not(),
+        );
+        state.constraints.push(BoolExpr::eq(bounded.clone().into_expr(), value_expr).not());
+        Ok(CheatcodeOutcome::Continue(vec![bounded]))
+    }
+}