Limits for interpreter depth (#1890)

* Set up max depth limit for interpreter
* Add debug-level warnings if interp runs too long

Author: jaybosamiya-ms

source/rust_verify_test/tests/assert_by_compute.rs

@@ -780,3 +780,43 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] depth_tracking_infinite_recursion verus_code! {
+        use vstd::prelude::*;
+
+        spec fn infinite_recursion(n: int) -> nat
+            decreases n,
+        {
+            infinite_recursion(1)  // Infinite recursion - should trigger depth limit
+        }
+
+        proof fn test_depth_limit() {
+            assert(infinite_recursion(42) >= 0) by(compute);
+        }
+    } => Err(err) => {
+        assert_eq!(err.errors.len(), 1);
+        assert!(err.errors[0].rendered.contains("assert_by_compute exceeded maximum recursion depth"));
+    }
+}
+
+test_verify_one_file! {
+    #[test] depth_tracking_deep_but_finite verus_code! {
+        use vstd::prelude::*;
+
+        spec fn count_down(n: nat) -> nat
+            decreases n,
+        {
+            if n == 0 {
+                0
+            } else {
+                count_down((n - 1) as nat)
+            }
+        }
+
+        proof fn test_deep_recursion() {
+            // This should succeed - finite recursion within reasonable depth
+            assert(count_down(50) == 0) by(compute);
+        }
+    } => Ok(())
+}

source/vir/src/interpreter.rs

@@ -31,11 +31,22 @@ use std::iter::FromIterator;
 use std::ops::ControlFlow;
 use std::sync::Arc;
 use std::thread;
+use std::time::Instant;
 use vir_macros::ToDebugSNode;
 
 // An approximation of how many interpreter invocations we can do in 1 second (in release mode)
 const RLIMIT_MULTIPLIER: u64 = 400_000;
 
+// Depth limit multiplier: max recursion depth as a multiplier of rlimit.
+//
+// This is set to be generous enough for legitimate use cases (like complex mathematical
+// computations) while still preventing stack overflow. Stack overflow typically occurs
+// around 50,000+ recursion levels, so this gives us good protection.
+const DEPTH_LIMIT_MULTIPLIER: u64 = 500;
+
+// Time-based warning interval in seconds
+const WARNING_INTERVAL_SECS: u64 = 2;
+
 type Env = ScopeMap<UniqueIdent, Exp>;
 type TypeEnv = ScopeMap<Ident, Typ>;
 
@@ -98,7 +109,7 @@ impl<T> PtrSet<T> {
 
 /// Mutable interpreter state
 struct State {
-    /// Depth of our current recursion; used for formatting log output
+    /// Depth of our current recursion; used for formatting log output and recursion control
     depth: usize,
     /// Symbol table mapping bound variables to their values
     env: Env,
@@ -127,6 +138,10 @@ struct State {
     ptr_misses: u64,
     /// Number of calls for each function
     fun_calls: HashMap<Fun, u64>,
+
+    /// Time tracking for warnings
+    start_time: Instant,
+    last_warning_time: Instant,
 }
 
 // Define the function-call cache's API
@@ -137,6 +152,22 @@ impl State {
         }
     }
 
+    /// Check time-based warnings and emit warning if enough time has passed.  Do so only in debug mode.
+    fn check_time_warning(&mut self) {
+        if !cfg!(debug_assertions) {
+            return;
+        }
+        let now = Instant::now();
+        if now.duration_since(self.last_warning_time).as_secs() >= WARNING_INTERVAL_SECS {
+            let total_time = now.duration_since(self.start_time).as_secs();
+            eprintln!(
+                "note: assert_by_compute has been running for {} seconds (depth: {}, iterations: {})",
+                total_time, self.depth, self.iterations
+            );
+            self.last_warning_time = now;
+        }
+    }
+
     fn lookup_call(&mut self, f: &Fun, args: &Exps, memoize: bool) -> Option<Exp> {
         if self.enable_cache && memoize {
             if self.perf {
@@ -163,6 +194,8 @@ struct Ctx<'a> {
     fun_ssts: &'a HashMap<Fun, FunctionSst>,
     /// We avoid infinite loops by running for a fixed number of intervals
     max_iterations: u64,
+    /// Maximum recursion depth to prevent stack overflow
+    max_depth: usize,
     arch: ArchWordBits,
     global: &'a GlobalCtx,
 }
@@ -1057,6 +1090,11 @@ fn eval_expr_internal(ctx: &Ctx, state: &mut State, exp: &Exp) -> Result<Exp, Vi
     if state.iterations > ctx.max_iterations {
         return Err(error(&exp.span, "assert_by_compute timed out"));
     }
+    if state.depth > ctx.max_depth {
+        return Err(error(&exp.span, "assert_by_compute exceeded maximum recursion depth"));
+    }
+    state.check_time_warning();
+
     state.log(format!(
         "{}Evaluating {:}",
         "\t".repeat(state.depth),
@@ -1860,6 +1898,7 @@ fn eval_expr_launch(
     let cache = HashMap::new();
     let logging = log.is_some();
     let msgs = Vec::new();
+    let now = Instant::now();
     let mut state = State {
         depth: 0,
         env,
@@ -1877,10 +1916,14 @@ fn eval_expr_launch(
         ptr_hits: 0,
         ptr_misses: 0,
         fun_calls: HashMap::new(),
+        start_time: now,
+        last_warning_time: now,
     };
     // Don't run for too long
     let max_iterations = (rlimit as f64 * RLIMIT_MULTIPLIER as f64) as u64;
-    let ctx = Ctx { fun_ssts: &fun_ssts, max_iterations, arch, global };
+    // Calculate max recursion depth as a fraction of rlimit
+    let max_depth = (rlimit as f64 * DEPTH_LIMIT_MULTIPLIER as f64) as usize;
+    let ctx = Ctx { fun_ssts: &fun_ssts, max_iterations, max_depth, arch, global };
     let result = eval_expr_top(&ctx, &mut state, &exp)?;
     display_perf_stats(&state);
     if state.log.is_some() {