From 5778d6a6ca5baae8f0612525eaf1dc1285bce224 Mon Sep 17 00:00:00 2001 From: Gustavo Figueiredo Date: Wed, 27 May 2026 16:30:17 +0100 Subject: [PATCH] feat(symbolic): allow gas as call operand Co-authored-by: Amp Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d --- crates/evm/symbolic/src/executor/calls.rs | 26 +- .../evm/symbolic/src/executor/cheatcodes.rs | 4 + .../evm/symbolic/src/executor/constraints.rs | 9 + crates/evm/symbolic/src/executor/opcodes.rs | 27 ++- crates/evm/symbolic/src/runtime/address.rs | 2 +- crates/evm/symbolic/src/runtime/evm.rs | 2 +- .../evm/symbolic/src/runtime/expressions.rs | 62 ++++- crates/evm/symbolic/src/runtime/solver.rs | 8 +- .../src/runtime/solver/hard_arith_fallback.rs | 13 +- .../symbolic/src/runtime/solver/normalize.rs | 8 +- crates/evm/symbolic/src/runtime/state.rs | 10 +- .../tests/cli/test_cmd/symbolic_opcodes.rs | 223 ++++++++++++++++++ 12 files changed, 376 insertions(+), 18 deletions(-) diff --git a/crates/evm/symbolic/src/executor/calls.rs b/crates/evm/symbolic/src/executor/calls.rs index 98668ae87434f..7b81c1d44ca31 100644 --- a/crates/evm/symbolic/src/executor/calls.rs +++ b/crates/evm/symbolic/src/executor/calls.rs @@ -13,7 +13,11 @@ impl SymbolicExecutor { let pre_call_state = state.clone(); let call_pc = state.pc.saturating_sub(1); let gas = state.stack.pop()?; + if gas.contains_gasleft() && !gas.is_raw_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let target = state.stack.pop()?; + ensure_word_not_gasleft(&target)?; let target_address = state.world.resolve_address(&target); let value = match (kind, target_address) { (CallKind::Call, Some(to)) if is_known_cheatcode(to) => { @@ -25,8 +29,11 @@ impl SymbolicExecutor { (CallKind::CallCode, _) => state.stack.pop()?, (CallKind::StaticCall | CallKind::DelegateCall, _) => SymWord::zero(), }; + ensure_word_not_gasleft(&value)?; let in_offset = state.stack.pop()?; + ensure_word_not_gasleft(&in_offset)?; let in_size = state.stack.pop()?; + ensure_word_not_gasleft(&in_size)?; let in_size = match state.constrained_usize(&in_size) { Some(size) => BoundedCopySize::Concrete(size), None if state.constrained_word(&in_size).is_some() => { @@ -50,7 +57,9 @@ impl SymbolicExecutor { } }; let out_offset = state.stack.pop()?; + ensure_word_not_gasleft(&out_offset)?; let out_size = state.stack.pop()?; + ensure_word_not_gasleft(&out_size)?; let out_size = match state.constrained_usize(&out_size) { Some(size) => BoundedCopySize::Concrete(size), None if state.constrained_word(&out_size).is_some() => { @@ -79,8 +88,12 @@ impl SymbolicExecutor { return Ok(StepOutcome::Revert); } + let call_input = call_input_from_memory(&state.memory, in_offset.clone(), &in_size); + if call_input.iter().any(SymWord::contains_gasleft) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } + if let Some(to) = target_address { - let call_input = call_input_from_memory(&state.memory, in_offset.clone(), &in_size); if self.branch_symbolic_function_mock_if_needed( state, worklist, @@ -660,6 +673,9 @@ impl SymbolicExecutor { BoolExpr::Const(true) => Ok((state.constraints.clone(), true)), BoolExpr::Const(false) => Ok((state.constraints.clone(), false)), condition => { + if bool_contains_gasleft(&condition) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let mut constraints = state.constraints.clone(); constraints.push(condition); let sat = self.solver.is_sat(&constraints)?; @@ -1389,3 +1405,11 @@ impl SymbolicExecutor { Ok(StepOutcome::Continue) } } + +fn ensure_word_not_gasleft(word: &SymWord) -> Result<(), SymbolicError> { + if word.contains_gasleft() { + Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")) + } else { + Ok(()) + } +} diff --git a/crates/evm/symbolic/src/executor/cheatcodes.rs b/crates/evm/symbolic/src/executor/cheatcodes.rs index 72708ee191144..4fd3e92cc4aa9 100644 --- a/crates/evm/symbolic/src/executor/cheatcodes.rs +++ b/crates/evm/symbolic/src/executor/cheatcodes.rs @@ -14,6 +14,10 @@ impl SymbolicExecutor { _ => {} } + if bool_contains_gasleft(&pass) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } + let mut fail_constraints = state.constraints.clone(); fail_constraints.push(fail); if self.solver.is_sat(&fail_constraints)? { diff --git a/crates/evm/symbolic/src/executor/constraints.rs b/crates/evm/symbolic/src/executor/constraints.rs index 87002d963970d..f815a1d2a6dce 100644 --- a/crates/evm/symbolic/src/executor/constraints.rs +++ b/crates/evm/symbolic/src/executor/constraints.rs @@ -31,6 +31,9 @@ impl SymbolicExecutor { BoolExpr::Const(true) => Ok(CheatcodeOutcome::Continue(Vec::new())), BoolExpr::Const(false) => Ok(CheatcodeOutcome::AssumeRejected), condition => { + if bool_contains_gasleft(&condition) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } state.constraints.push(condition); if self.solver.is_sat(&state.constraints)? { Ok(CheatcodeOutcome::Continue(Vec::new())) @@ -49,6 +52,9 @@ impl SymbolicExecutor { max: usize, reason: &'static str, ) -> Result { + if word.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } 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)))); @@ -82,6 +88,9 @@ impl SymbolicExecutor { word: &SymWord, min: usize, ) -> Result { + if word.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let condition = BoolExpr::cmp(BoolExprOp::Uge, word.clone().into_expr(), Expr::Const(U256::from(min))); match condition { diff --git a/crates/evm/symbolic/src/executor/opcodes.rs b/crates/evm/symbolic/src/executor/opcodes.rs index 9f8ca2840b200..536e275a53a1e 100644 --- a/crates/evm/symbolic/src/executor/opcodes.rs +++ b/crates/evm/symbolic/src/executor/opcodes.rs @@ -515,6 +515,9 @@ impl SymbolicExecutor { } Some(false) => Ok(StepOutcome::Continue), None => { + if cond.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let op_pc = state.pc.saturating_sub(1); let _branch_span = trace_span!("jumpi_branch", pc = op_pc, dest).entered(); let true_cond = cond.nonzero_bool(); @@ -551,7 +554,11 @@ impl SymbolicExecutor { state.stack.push(size)?; Ok(StepOutcome::Continue) } - opcode::GAS => Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")), + opcode::GAS => { + let gas = state.fresh_gasleft(); + state.stack.push(gas)?; + Ok(StepOutcome::Continue) + } opcode::JUMPDEST => Ok(StepOutcome::Continue), opcode::MCOPY => { let dest = state.stack.pop()?; @@ -677,7 +684,13 @@ impl SymbolicExecutor { } let topics = (op - opcode::LOG0) as usize; let offset = state.stack.pop()?; + if offset.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let size = state.stack.pop()?; + if size.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let (data_len, data) = match state.constrained_usize(&size) { Some(size) => ( SymWord::Concrete(U256::from(size)), @@ -707,7 +720,14 @@ impl SymbolicExecutor { }; let mut log_topics = Vec::with_capacity(topics); for _ in 0..topics { - log_topics.push(state.stack.pop()?); + let topic = state.stack.pop()?; + if topic.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } + log_topics.push(topic); + } + if data.iter().any(SymWord::contains_gasleft) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); } self.handle_log( state, @@ -725,6 +745,9 @@ impl SymbolicExecutor { offset: SymWord, size: SymWord, ) -> Result { + if offset.contains_gasleft() || size.contains_gasleft() { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let end = Expr::op(ExprOp::Add, offset.into_expr(), size.into_expr()); let in_bounds = BoolExpr::cmp(BoolExprOp::Ule, end, state.return_data.len_expr()); match in_bounds { diff --git a/crates/evm/symbolic/src/runtime/address.rs b/crates/evm/symbolic/src/runtime/address.rs index 60a4ba0109e92..213b9e3a443ec 100644 --- a/crates/evm/symbolic/src/runtime/address.rs +++ b/crates/evm/symbolic/src/runtime/address.rs @@ -109,7 +109,7 @@ pub(crate) fn expr_byte_term(expr: &Expr, index: usize) -> Option { match expr { Expr::Const(value) => Some(Expr::Const(U256::from(value.to_be_bytes::<32>()[index]))), - Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => { + Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => { Some(extracted_byte_expr(expr, index)) } Expr::Not(value) => Some(Expr::Not(Box::new(expr_byte_term(value, index)?))), diff --git a/crates/evm/symbolic/src/runtime/evm.rs b/crates/evm/symbolic/src/runtime/evm.rs index 4478361df8a85..e33e1eb05ec5f 100644 --- a/crates/evm/symbolic/src/runtime/evm.rs +++ b/crates/evm/symbolic/src/runtime/evm.rs @@ -167,7 +167,7 @@ pub(crate) fn expr_known_byte(expr: &Expr, index: usize) -> Option { debug_assert!(index < 32); match expr { Expr::Const(value) => Some(value.to_be_bytes::<32>()[index]), - Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, + Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, Expr::Not(value) => expr_known_byte(value, index).map(|byte| !byte), Expr::Ite(_, then_expr, else_expr) => { let then_byte = expr_known_byte(then_expr, index)?; diff --git a/crates/evm/symbolic/src/runtime/expressions.rs b/crates/evm/symbolic/src/runtime/expressions.rs index d9327d81d99bb..f4198a8ad1682 100644 --- a/crates/evm/symbolic/src/runtime/expressions.rs +++ b/crates/evm/symbolic/src/runtime/expressions.rs @@ -313,7 +313,7 @@ pub(crate) fn sym_sub(left: SymWord, right: SymWord) -> SymWord { pub(crate) fn expr_contains_keccak(expr: &Expr) -> bool { match expr { Expr::Keccak { .. } => true, - Expr::Const(_) | Expr::Var(_) | Expr::Hash { .. } => false, + Expr::Const(_) | Expr::Var(_) | Expr::GasLeft(_) | Expr::Hash { .. } => false, Expr::Not(value) => expr_contains_keccak(value), Expr::Op(_, left, right) => expr_contains_keccak(left) || expr_contains_keccak(right), Expr::Ite(cond, left, right) => { @@ -322,6 +322,26 @@ pub(crate) fn expr_contains_keccak(expr: &Expr) -> bool { } } +/// Returns whether a word expression depends on the opaque `GAS` / `gasleft()` value. +pub(crate) fn expr_contains_gasleft(expr: &Expr) -> bool { + match expr { + Expr::Const(_) => false, + Expr::Var(_) => false, + Expr::GasLeft(_) => true, + Expr::Keccak { len, bytes, .. } => { + expr_contains_gasleft(len) || bytes.iter().any(expr_contains_gasleft) + } + Expr::Hash { bytes, .. } => bytes.iter().any(expr_contains_gasleft), + Expr::Not(value) => expr_contains_gasleft(value), + Expr::Op(_, left, right) => expr_contains_gasleft(left) || expr_contains_gasleft(right), + Expr::Ite(cond, left, right) => { + bool_contains_gasleft(cond) + || expr_contains_gasleft(left) + || expr_contains_gasleft(right) + } + } +} + /// Returns the `bool_forces_expr_const_with_context` symbolic expression helper result. pub(crate) fn bool_forces_expr_const_with_context( condition: &BoolExpr, @@ -376,9 +396,12 @@ pub(crate) fn expr_nonzero_forces_const( context: &[BoolExpr], ) -> Option { match expr { - Expr::Const(_) | Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } | Expr::Not(_) => { - None - } + Expr::Const(_) + | Expr::Var(_) + | Expr::GasLeft(_) + | Expr::Keccak { .. } + | Expr::Hash { .. } + | Expr::Not(_) => None, Expr::Ite(cond, then_expr, else_expr) => { if expr_const_value(then_expr).is_some_and(|value| !value.is_zero()) && expr_const_value(else_expr).is_some_and(|value| value.is_zero()) @@ -440,7 +463,7 @@ pub(crate) fn context_forces_masked_expr(context: &[BoolExpr], target: &Expr, ma pub(crate) fn expr_const_value(expr: &Expr) -> Option { match expr { Expr::Const(value) => Some(*value), - Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, + Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, Expr::Not(value) => Some(!expr_const_value(value)?), Expr::Op(op, left, right) => { Some(eval_expr_op(*op, expr_const_value(left)?, expr_const_value(right)?)) @@ -495,6 +518,18 @@ pub(crate) fn bool_contains_keccak(expr: &BoolExpr) -> bool { } } +/// Returns whether a boolean expression depends on the opaque `GAS` / `gasleft()` value. +pub(crate) fn bool_contains_gasleft(expr: &BoolExpr) -> bool { + match expr { + BoolExpr::Const(_) => false, + BoolExpr::Not(value) => bool_contains_gasleft(value), + BoolExpr::And(values) => values.iter().any(bool_contains_gasleft), + BoolExpr::Eq(left, right) | BoolExpr::Cmp(_, left, right) => { + expr_contains_gasleft(left) || expr_contains_gasleft(right) + } + } +} + /// Returns the `word_bytes` symbolic expression helper result. pub(crate) fn word_bytes(word: SymWord) -> Vec { match word { @@ -676,6 +711,7 @@ pub(crate) fn eval_expr( Ok(match expr { Expr::Const(value) => *value, Expr::Var(var) => model.get(var).copied().unwrap_or_default(), + Expr::GasLeft(_) => return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")), Expr::Keccak { len, bytes, .. } => eval_keccak_expr(len, bytes, model)?, Expr::Hash { name, .. } => model.get(name).copied().unwrap_or_default(), Expr::Not(value) => !eval_expr(value, model)?, @@ -808,6 +844,19 @@ impl SymWord { Self::Concrete(U256::ZERO) } + /// Returns whether this word depends on the opaque `GAS` / `gasleft()` value. + pub(crate) fn contains_gasleft(&self) -> bool { + match self { + Self::Concrete(_) => false, + Self::Expr(expr) => expr_contains_gasleft(expr), + } + } + + /// Returns whether this word is exactly the opaque `GAS` / `gasleft()` value. + pub(crate) const fn is_raw_gasleft(&self) -> bool { + matches!(self, Self::Expr(Expr::GasLeft(_))) + } + /// Implements the `into_expr` symbolic expression helper. pub(crate) fn into_expr(self) -> Expr { match self { @@ -883,6 +932,7 @@ impl SymWord { pub(crate) enum Expr { Const(U256), Var(String), + GasLeft(usize), Keccak { name: String, len: Box, bytes: Vec }, Hash { name: String, algorithm: &'static str, bytes: Vec }, Not(Box), @@ -957,6 +1007,7 @@ impl Expr { pub(crate) fn collect_vars(&self, vars: &mut BTreeSet) { match self { Self::Const(_) => {} + Self::GasLeft(_) => {} Self::Var(var) => { vars.insert(var.clone()); } @@ -981,6 +1032,7 @@ impl Expr { match self { Self::Const(value) => format!("(_ bv{value} 256)"), Self::Var(var) => var.clone(), + Self::GasLeft(id) => format!("gasleft_{id}"), Self::Keccak { name, .. } | Self::Hash { name, .. } => name.clone(), Self::Not(value) => format!("(bvnot {})", value.smt()), Self::Op(op, left, right) => format!("({} {} {})", op.smt(), left.smt(), right.smt()), diff --git a/crates/evm/symbolic/src/runtime/solver.rs b/crates/evm/symbolic/src/runtime/solver.rs index 0f7241ca73380..f7114ea552bca 100644 --- a/crates/evm/symbolic/src/runtime/solver.rs +++ b/crates/evm/symbolic/src/runtime/solver.rs @@ -263,6 +263,9 @@ impl SymbolicSolver for SmtLibSubprocessSolver { /// Returns whether `is_sat` holds. fn is_sat(&mut self, constraints: &[BoolExpr]) -> Result { self.sat_queries += 1; + if constraints.iter().any(bool_contains_gasleft) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let smt_constraints = normalize_constraints_for_solver(constraints); let cache_key = constraint_cache_key(&smt_constraints); if let Some(result) = self.sat_cache.get(&cache_key) { @@ -322,6 +325,9 @@ impl SymbolicSolver for SmtLibSubprocessSolver { /// Implements the `model` solver helper. fn model(&mut self, constraints: &[BoolExpr]) -> Result, SymbolicError> { self.model_queries += 1; + if constraints.iter().any(bool_contains_gasleft) { + return Err(SymbolicError::Unsupported("GAS/gasleft() not modeled")); + } let smt_constraints = normalize_constraints_for_solver(constraints); let cache_key = constraint_cache_key(&smt_constraints); @@ -572,7 +578,7 @@ const fn cache_key_cmp(op: BoolExprOp, left: Expr, right: Expr) -> BoolExpr { /// Returns a conservative canonical word expression for cache-key equality. fn cache_key_expr(expr: Expr) -> Expr { match expr { - Expr::Const(_) | Expr::Var(_) => expr, + Expr::Const(_) | Expr::Var(_) | Expr::GasLeft(_) => expr, Expr::Keccak { name, len, bytes } => Expr::Keccak { name, len: Box::new(cache_key_expr(*len)), diff --git a/crates/evm/symbolic/src/runtime/solver/hard_arith_fallback.rs b/crates/evm/symbolic/src/runtime/solver/hard_arith_fallback.rs index 021493de3095c..b971dd559980c 100644 --- a/crates/evm/symbolic/src/runtime/solver/hard_arith_fallback.rs +++ b/crates/evm/symbolic/src/runtime/solver/hard_arith_fallback.rs @@ -15,7 +15,11 @@ pub(crate) fn bool_contains_hard_arith(expr: &BoolExpr) -> bool { /// Returns the `expr_contains_hard_arith` solver helper result. pub(crate) fn expr_contains_hard_arith(expr: &Expr) -> bool { match expr { - Expr::Const(_) | Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => false, + Expr::Const(_) + | Expr::Var(_) + | Expr::GasLeft(_) + | Expr::Keccak { .. } + | Expr::Hash { .. } => false, Expr::Not(value) => expr_contains_hard_arith(value), Expr::Op(ExprOp::Mul, left, right) => expr_contains_var(left) && expr_contains_var(right), Expr::Op(ExprOp::UDiv | ExprOp::URem | ExprOp::SDiv | ExprOp::SRem, left, right) => { @@ -39,7 +43,7 @@ pub(crate) fn expr_contains_symbolic_hash(expr: &Expr) -> bool { Expr::Keccak { len, bytes, .. } => { expr_contains_symbolic_hash(len) || bytes.iter().any(expr_contains_symbolic_hash) } - Expr::Const(_) | Expr::Var(_) => false, + Expr::Const(_) | Expr::Var(_) | Expr::GasLeft(_) => false, Expr::Not(value) => expr_contains_symbolic_hash(value), Expr::Op(_, left, right) => { expr_contains_symbolic_hash(left) || expr_contains_symbolic_hash(right) @@ -69,6 +73,7 @@ pub(crate) fn expr_contains_var(expr: &Expr) -> bool { match expr { Expr::Const(_) => false, Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => true, + Expr::GasLeft(_) => false, Expr::Not(value) => expr_contains_var(value), Expr::Op(_, left, right) => expr_contains_var(left) || expr_contains_var(right), Expr::Ite(cond, left, right) => { @@ -300,7 +305,7 @@ pub(crate) fn collect_bool_fallback_vars(expr: &BoolExpr, vars: &mut BTreeSet) { match expr { - Expr::Const(_) | Expr::Hash { .. } => {} + Expr::Const(_) | Expr::GasLeft(_) | Expr::Hash { .. } => {} Expr::Var(var) => { vars.insert(var.clone()); } @@ -411,7 +416,7 @@ pub(crate) fn collect_expr_constants(expr: &Expr, constants: &mut BTreeSet Expr::Const(value) => { constants.insert(*value); } - Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => {} + Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => {} Expr::Not(value) => collect_expr_constants(value, constants), Expr::Op(_, left, right) => { collect_expr_constants(left, constants); diff --git a/crates/evm/symbolic/src/runtime/solver/normalize.rs b/crates/evm/symbolic/src/runtime/solver/normalize.rs index d02a261795c79..437029585e8be 100644 --- a/crates/evm/symbolic/src/runtime/solver/normalize.rs +++ b/crates/evm/symbolic/src/runtime/solver/normalize.rs @@ -45,7 +45,11 @@ pub(crate) fn normalize_expr_for_solver(expr: Expr) -> Expr { } match expr { - Expr::Const(_) | Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => expr, + Expr::Const(_) + | Expr::Var(_) + | Expr::GasLeft(_) + | Expr::Keccak { .. } + | Expr::Hash { .. } => expr, Expr::Not(value) => Expr::Not(Box::new(normalize_expr_for_solver(*value))), Expr::Op(op, left, right) => { let left = normalize_expr_for_solver(*left); @@ -233,7 +237,7 @@ pub(crate) fn bool_from_word_expr(expr: &Expr) -> Option { /// Returns whether a word expression syntactically contains unsigned division. pub(crate) fn expr_contains_udiv(expr: &Expr) -> bool { match expr { - Expr::Const(_) | Expr::Var(_) => false, + Expr::Const(_) | Expr::Var(_) | Expr::GasLeft(_) => false, Expr::Keccak { len, bytes, .. } => { expr_contains_udiv(len) || bytes.iter().any(expr_contains_udiv) } diff --git a/crates/evm/symbolic/src/runtime/state.rs b/crates/evm/symbolic/src/runtime/state.rs index 6e51e57c81917..894001f37841a 100644 --- a/crates/evm/symbolic/src/runtime/state.rs +++ b/crates/evm/symbolic/src/runtime/state.rs @@ -204,7 +204,7 @@ impl PathState { let constraint_bound = self.constraint_upper_bound_usize(expr); let structural_bound = match expr { Expr::Const(value) => u256_to_usize(*value), - Expr::Var(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, + Expr::Var(_) | Expr::GasLeft(_) | Expr::Keccak { .. } | Expr::Hash { .. } => None, Expr::Not(_) => None, Expr::Ite(_, left, right) => { Some(self.expr_upper_bound_usize(left)?.max(self.expr_upper_bound_usize(right)?)) @@ -486,6 +486,13 @@ impl PathState { SymWord::Expr(Expr::Var(format!("{prefix}_{id}"))) } + /// Implements the `fresh_gasleft` symbolic state helper. + pub(crate) const fn fresh_gasleft(&mut self) -> SymWord { + let id = self.next_symbol; + self.next_symbol += 1; + SymWord::Expr(Expr::GasLeft(id)) + } + /// Implements the `fresh_bounded_uint` symbolic state helper. pub(crate) fn fresh_bounded_uint(&mut self, bits: U256) -> SymWord { let value = self.fresh_word("symbolic"); @@ -1601,6 +1608,7 @@ impl Default for SymbolicBlock { fn collect_eval_vars(expr: &Expr, vars: &mut BTreeSet) { match expr { Expr::Const(_) => {} + Expr::GasLeft(_) => {} Expr::Var(var) | Expr::Hash { name: var, .. } => { vars.insert(var.clone()); } diff --git a/crates/forge/tests/cli/test_cmd/symbolic_opcodes.rs b/crates/forge/tests/cli/test_cmd/symbolic_opcodes.rs index 1b34517e5173b..cd5b1258db7c4 100644 --- a/crates/forge/tests/cli/test_cmd/symbolic_opcodes.rs +++ b/crates/forge/tests/cli/test_cmd/symbolic_opcodes.rs @@ -266,6 +266,229 @@ incomplete symbolic execution (Stuck): unsupported symbolic execution feature: G ); }); +forgetest_init!(symbolic_gas_can_be_used_as_call_operand, |prj, cmd| { + skip_unless_z3!("symbolic_gas_can_be_used_as_call_operand"); + + prj.add_test( + "SymbolicGasCallOperand.t.sol", + r#" +contract SymbolicGasCallOperandTarget { + function ping(uint256 value) external pure returns (uint256) { + return value + 1; + } +} + +contract SymbolicGasCallOperand { + SymbolicGasCallOperandTarget target; + + function setUp() public { + target = new SymbolicGasCallOperandTarget(); + } + + function checkGasOnlyFeedsCall(uint128 raw) public view { + uint256 value = uint256(raw); + bytes4 selector = SymbolicGasCallOperandTarget.ping.selector; + address targetAddress = address(target); + bool ok; + uint256 out; + assembly { + let ptr := mload(0x40) + mstore(ptr, selector) + mstore(add(ptr, 4), value) + ok := staticcall(gas(), targetAddress, ptr, 36, ptr, 32) + out := mload(ptr) + } + + assert(ok); + assert(out == value + 1); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkGasOnlyFeedsCall"]) + .assert_success() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +[PASS] checkGasOnlyFeedsCall(uint128) +"#]], + ); + assert!(!stdout.contains("GAS/gasleft() not modeled"), "{stdout}"); +}); + +forgetest_init!(symbolic_gas_derived_call_operand_reports_unsupported, |prj, cmd| { + skip_unless_z3!("symbolic_gas_derived_call_operand_reports_unsupported"); + + prj.add_test( + "SymbolicDerivedGasCallOperand.t.sol", + r#" +contract SymbolicDerivedGasCallOperandTarget { + function ping() external pure returns (uint256) { + return 1; + } +} + +contract SymbolicDerivedGasCallOperand { + SymbolicDerivedGasCallOperandTarget target; + + function setUp() public { + target = new SymbolicDerivedGasCallOperandTarget(); + } + + function checkDerivedGasCallOperand() public view { + bytes4 selector = SymbolicDerivedGasCallOperandTarget.ping.selector; + address targetAddress = address(target); + bool ok; + assembly { + let ptr := mload(0x40) + mstore(ptr, selector) + ok := staticcall(sub(gas(), 1), targetAddress, ptr, 4, ptr, 32) + } + assert(ok); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkDerivedGasCallOperand"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + +forgetest_init!(symbolic_gas_in_call_calldata_reports_unsupported, |prj, cmd| { + skip_unless_z3!("symbolic_gas_in_call_calldata_reports_unsupported"); + + prj.add_test( + "SymbolicGasCallData.t.sol", + r#" +contract SymbolicGasCallDataTarget { + fallback() external {} +} + +contract SymbolicGasCallData { + SymbolicGasCallDataTarget target; + + function setUp() public { + target = new SymbolicGasCallDataTarget(); + } + + function checkGasInCallData() public view { + address targetAddress = address(target); + bool ok; + assembly { + let ptr := mload(0x40) + mstore(ptr, gas()) + ok := staticcall(gas(), targetAddress, ptr, 32, 0, 0) + } + assert(ok); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkGasInCallData"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + +forgetest_init!(symbolic_gas_as_call_target_reports_unsupported, |prj, cmd| { + skip_unless_z3!("symbolic_gas_as_call_target_reports_unsupported"); + + prj.add_test( + "SymbolicGasCallTarget.t.sol", + r#" +contract SymbolicGasCallTarget { + function checkGasAsCallTarget() public view { + bool ok; + assembly { + ok := staticcall(gas(), gas(), 0, 0, 0, 0) + } + assert(ok); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkGasAsCallTarget"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + +forgetest_init!(symbolic_gas_as_call_input_bounds_reports_unsupported, |prj, cmd| { + skip_unless_z3!("symbolic_gas_as_call_input_bounds_reports_unsupported"); + + prj.add_test( + "SymbolicGasCallInputBounds.t.sol", + r#" +contract SymbolicGasCallInputBoundsTarget { + fallback() external {} +} + +contract SymbolicGasCallInputBounds { + SymbolicGasCallInputBoundsTarget target; + + function setUp() public { + target = new SymbolicGasCallInputBoundsTarget(); + } + + function checkGasAsCallInputOffset() public view { + address targetAddress = address(target); + bool ok; + assembly { + ok := staticcall(gas(), targetAddress, gas(), 0, 0, 0) + } + assert(ok); + } +} +"#, + ); + + let stdout = cmd + .args(["test", "--symbolic", "--match-test", "checkGasAsCallInputOffset"]) + .assert_failure() + .get_output() + .stdout_lossy(); + + assert_relevant_lines( + &stdout, + foundry_test_utils::str![[r#" +incomplete symbolic execution (Stuck): unsupported symbolic execution feature: GAS/gasleft() not modeled +"#]], + ); +}); + // Plan-compliant target behavior for the `GAS` / `gasleft()` opcode: any // symbolic path that branches on `gasleft()` should taint the result as // Incomplete (Unsupported), because gas is not modeled symbolically and a