feat(symbolic): allow GAS as call operand

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(())
+    }
+}

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)? {

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<usize, SymbolicError> {
+        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<bool, SymbolicError> {
+        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 {

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<bool, SymbolicError> {
+        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 {

crates/evm/symbolic/src/runtime/address.rs

@@ -109,7 +109,7 @@ pub(crate) fn expr_byte_term(expr: &Expr, index: usize) -> Option<Expr> {
 
     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)?))),

crates/evm/symbolic/src/runtime/evm.rs

@@ -167,7 +167,7 @@ pub(crate) fn expr_known_byte(expr: &Expr, index: usize) -> Option<u8> {
     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)?;

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<U256> {
     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<U256> {
     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<SymWord> {
     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<Self>, bytes: Vec<Self> },
     Hash { name: String, algorithm: &'static str, bytes: Vec<Self> },
     Not(Box<Self>),
@@ -957,6 +1007,7 @@ impl Expr {
     pub(crate) fn collect_vars(&self, vars: &mut BTreeSet<String>) {
         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()),

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<bool, SymbolicError> {
         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<BTreeMap<String, U256>, 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)),