@@ -8,6 +8,13 @@ use super::errors::{Result, VmError};
88use super :: execution_model:: ExecutionState ;
99use super :: machine:: RegoVM ;
1010
11+ /// Debug-only sanity ceiling for `execution_stack` depth. Far above any
12+ /// legitimate nesting observed in the test suite; trips early on a runaway
13+ /// frame leak. Not a production execution limit — use `enforce_limit` /
14+ /// `MachineLimits` for those.
15+ #[ cfg( debug_assertions) ]
16+ const DEBUG_MAX_EXECUTION_STACK_DEPTH : usize = 4096 ;
17+
1118impl RegoVM {
1219 /// Reset all execution state and return objects to pools for reuse
1320pub ( super ) fn reset_execution_state ( & mut self ) {
@@ -34,6 +41,136 @@ impl RegoVM {
3441
3542 // Builtin cache entries only live for a single execution
3643 self . builtins_cache . clear ( ) ;
44+
45+ // Postcondition: every stack/cache that `reset_execution_state` touches
46+ // must be in its documented "clean" shape. This catches accidental
47+ // omissions in future edits to this function.
48+ self . debug_assert_state_is_clean ( ) ;
49+ }
50+
51+ /// Debug-only postcondition for `reset_execution_state`.
52+ ///
53+ /// Asserts the invariants every caller of `reset_execution_state` relies on
54+ /// before starting a fresh execution. The body is fully gated by
55+ /// `#[cfg(debug_assertions)]` so this is a zero-cost no-op in release.
56+ #[ inline]
57+ pub ( super ) fn debug_assert_state_is_clean ( & self ) {
58+ #[ cfg( debug_assertions) ]
59+ {
60+ // --- Stacks: every per-execution stack must be drained. ---
61+ debug_assert ! (
62+ self . execution_stack. is_empty( ) ,
63+ "reset_execution_state postcondition: execution_stack must be empty"
64+ ) ;
65+ debug_assert ! (
66+ self . loop_stack. is_empty( ) ,
67+ "reset_execution_state postcondition: loop_stack must be empty"
68+ ) ;
69+ debug_assert ! (
70+ self . comprehension_stack. is_empty( ) ,
71+ "reset_execution_state postcondition: comprehension_stack must be empty"
72+ ) ;
73+ debug_assert ! (
74+ self . call_rule_stack. is_empty( ) ,
75+ "reset_execution_state postcondition: call_rule_stack must be empty"
76+ ) ;
77+ debug_assert ! (
78+ self . register_stack. is_empty( ) ,
79+ "reset_execution_state postcondition: register_stack must be empty"
80+ ) ;
81+
82+ // --- Caches: cleared so a new program/input cannot read stale entries. ---
83+ debug_assert ! (
84+ self . builtins_cache. is_empty( ) ,
85+ "reset_execution_state postcondition: builtins_cache must be empty"
86+ ) ;
87+
88+ // --- Registers: window resized to the program's base count and zeroed. ---
89+ debug_assert_eq ! (
90+ self . registers. len( ) ,
91+ self . base_register_count,
92+ "reset_execution_state postcondition: registers must be sized to base_register_count"
93+ ) ;
94+ debug_assert ! (
95+ self . registers. iter( ) . all( |v| matches!( v, Value :: Undefined ) ) ,
96+ "reset_execution_state postcondition: all registers must be Undefined"
97+ ) ;
98+
99+ // --- Rule cache: sized to the current program and marked uncomputed. ---
100+ debug_assert_eq ! (
101+ self . rule_cache. len( ) ,
102+ self . program. rule_infos. len( ) ,
103+ "reset_execution_state postcondition: rule_cache size must match program rule_infos"
104+ ) ;
105+ debug_assert ! (
106+ self . rule_cache. iter( ) . all( |entry| !entry. 0 ) ,
107+ "reset_execution_state postcondition: rule_cache entries must be uncomputed"
108+ ) ;
109+
110+ // --- Counters and execution-state machine: zeroed and back to Ready. ---
111+ debug_assert_eq ! (
112+ self . pc, 0 ,
113+ "reset_execution_state postcondition: pc must be 0"
114+ ) ;
115+ debug_assert_eq ! (
116+ self . executed_instructions, 0 ,
117+ "reset_execution_state postcondition: executed_instructions must be 0"
118+ ) ;
119+ debug_assert ! (
120+ matches!( self . execution_state, ExecutionState :: Ready ) ,
121+ "reset_execution_state postcondition: execution_state must be Ready"
122+ ) ;
123+ }
124+ }
125+
126+ /// Per-opcode VM invariants checked from the inner dispatch loop.
127+ ///
128+ /// These hold every time control re-enters the dispatch loop with another
129+ /// instruction to execute. Fully `#[cfg(debug_assertions)]`-gated so the
130+ /// method body compiles out in release.
131+ #[ inline]
132+ pub ( super ) fn assert_vm_invariants ( & self ) {
133+ #[ cfg( debug_assertions) ]
134+ {
135+ // The dispatch loop only runs while execution is live. Once the VM
136+ // has transitioned to a terminal state (Suspended/Completed/Error)
137+ // the loop must have exited. Note `Ready` is also valid here because
138+ // some entry points (e.g. `execute_entry_point_by_index` in
139+ // RunToCompletion mode) drive `jump_to` without flipping the state.
140+ debug_assert ! (
141+ matches!(
142+ self . execution_state,
143+ ExecutionState :: Ready | ExecutionState :: Running
144+ ) ,
145+ "vm invariant: execution_state must be Ready or Running inside the dispatch loop, was {:?}" ,
146+ self . execution_state
147+ ) ;
148+
149+ // Registers must always be non-empty when the dispatch loop is
150+ // running — every instruction operates on registers.
151+ debug_assert ! (
152+ !self . registers. is_empty( ) ,
153+ "vm invariant: register window must be non-empty inside the dispatch loop"
154+ ) ;
155+
156+ // Rule cache is sized once at reset and must not change shape mid-run.
157+ debug_assert_eq ! (
158+ self . rule_cache. len( ) ,
159+ self . program. rule_infos. len( ) ,
160+ "vm invariant: rule_cache size must equal program.rule_infos size"
161+ ) ;
162+
163+ // Bound the execution stack. There is no hard MAX_FRAMES today;
164+ // this is a debug-only sanity net well above any legitimate test or
165+ // policy nesting depth in the suite, and catches runaway
166+ // frame-leaks early. Not a production limit.
167+ debug_assert ! (
168+ self . execution_stack. len( ) <= DEBUG_MAX_EXECUTION_STACK_DEPTH ,
169+ "vm invariant: execution_stack depth ({}) exceeds sanity bound ({})" ,
170+ self . execution_stack. len( ) ,
171+ DEBUG_MAX_EXECUTION_STACK_DEPTH ,
172+ ) ;
173+ }
37174 }
38175
39176 /// Return all active objects to their respective pools for reuse
0 commit comments