Skip to content

Commit c0598aa

Browse files
anakrishCopilot
andcommitted
rvm: add debug-mode invariant assertions
Encode VM stack/context/register lifecycle invariants as debug_assert!s. Zero cost in release; surfaces violations during debug-mode tests and CI. Invariants covered: - reset_execution_state postcondition: all stacks empty, registers resized to base and Undefined, rule_cache reset, pc/executed counters zeroed, builtins_cache cleared, execution_state Ready. - Per-opcode invariant check (assert_vm_invariants) invoked at the top of run_stackless_loop and jump_to iterations: state is Ready/Running, registers non-empty, rule_cache sized to program, execution stack bounded. - resume() precondition: execution_state is Suspended. - execute_suspendable_entry precondition: clean state (callers reset immediately before). - ComprehensionEnd dispatch: comprehension_stack non-empty. - Rule finalize / call_rule completion: call_rule_stack non-empty and popped frame's rule_index matches. - IterationState::advance: Single iterator not advanced past consumption, Array index not at usize::MAX before saturating_add. All gated by #[cfg(debug_assertions)] (directly or via debug_assert!) so release builds are unaffected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
1 parent ba7d29b commit c0598aa

5 files changed

Lines changed: 157 additions & 1 deletion

File tree

src/rvm/vm/comprehension.rs

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -528,7 +528,6 @@ impl RegoVM {
528528
Ok(false)
529529
}
530530
}
531-
532531
pub(super) fn handle_comprehension_condition_failure_suspendable(&mut self) -> Result<bool> {
533532
if let Some(mut frame) = self.execution_stack.pop() {
534533
let handled = if let &mut FrameKind::Comprehension {
@@ -606,6 +605,13 @@ impl RegoVM {
606605
}
607606

608607
fn execute_comprehension_end_run_to_completion(&mut self) -> Result<()> {
608+
// A ComprehensionEnd instruction can only be reached from inside an
609+
// active comprehension; the stack must be non-empty here.
610+
debug_assert!(
611+
!self.comprehension_stack.is_empty(),
612+
"ComprehensionEnd reached with empty comprehension_stack at pc {}",
613+
self.pc
614+
);
609615
self.comprehension_stack.pop().map_or_else(
610616
|| {
611617
Err(VmError::InvalidIteration {

src/rvm/vm/context.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,10 @@ impl IterationState {
5454
pub(super) const fn advance(&mut self) {
5555
match *self {
5656
Self::Array { ref mut index, .. } => {
57+
debug_assert!(
58+
*index < usize::MAX,
59+
"IterationState::Array index overflow on advance"
60+
);
5761
*index = index.saturating_add(1);
5862
}
5963
Self::Object {
@@ -69,6 +73,10 @@ impl IterationState {
6973
Self::Single {
7074
ref mut consumed, ..
7175
} => {
76+
debug_assert!(
77+
!*consumed,
78+
"IterationState::Single advanced after consumption"
79+
);
7280
*consumed = true;
7381
}
7482
}

src/rvm/vm/execution.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,7 @@ impl RegoVM {
117117
let target = self.convert_pc(target, "jump target")?;
118118
self.pc = target;
119119
while self.pc < program.instructions.len() {
120+
self.assert_vm_invariants();
120121
self.memory_check()?;
121122
if self.executed_instructions >= self.max_instructions {
122123
return Err(VmError::InstructionLimitExceeded {
@@ -189,6 +190,9 @@ impl RegoVM {
189190
}
190191

191192
fn execute_suspendable_entry(&mut self, entry_point_pc: usize) -> Result<Value> {
193+
// Precondition: callers (execute_entry_point_by_{index,name}) reset the
194+
// VM before invoking this method, so the VM must be in a clean state.
195+
self.debug_assert_state_is_clean();
192196
self.execution_state = ExecutionState::Running;
193197
self.reset_execution_timer_state();
194198
match self.run_stackless_from(entry_point_pc) {
@@ -201,6 +205,12 @@ impl RegoVM {
201205
}
202206

203207
pub fn resume(&mut self, resume_value: Option<Value>) -> Result<Value> {
208+
// Precondition: resume only makes sense from a Suspended state.
209+
debug_assert!(
210+
matches!(self.execution_state, ExecutionState::Suspended { .. }),
211+
"resume precondition: execution_state must be Suspended, was {:?}",
212+
self.execution_state
213+
);
204214
let (reason, mut last_result) = match self.execution_state.clone() {
205215
ExecutionState::Suspended {
206216
reason,
@@ -289,6 +299,7 @@ impl RegoVM {
289299

290300
fn run_stackless_loop(&mut self, program: &Program, last_result: &mut Value) -> Result<()> {
291301
while !self.execution_stack.is_empty() {
302+
self.assert_vm_invariants();
292303
self.memory_check()?;
293304
self.frame_pc_overridden = false;
294305
let should_finalize_rule = self.execution_stack.last().is_some_and(|frame| {

src/rvm/vm/rules.rs

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -277,6 +277,11 @@ impl RegoVM {
277277
.call_rule_stack
278278
.pop()
279279
.ok_or(VmError::CallRuleStackUnderflow { pc: self.pc })?;
280+
debug_assert_eq!(
281+
call_context.rule_index, rule_index,
282+
"call_rule_stack pop mismatch: expected rule_index {} got {}",
283+
rule_index, call_context.rule_index,
284+
);
280285
self.pc = call_context.return_pc;
281286

282287
let result_from_rule = if !rule_failed_due_to_inconsistency {
@@ -831,6 +836,13 @@ impl RegoVM {
831836

832837
self.registers = parent_registers;
833838

839+
// Finalizing a rule frame must always have a matching CallRuleContext
840+
// pushed by execute_call_rule_suspendable; underflow is a state-leak bug.
841+
debug_assert!(
842+
!self.call_rule_stack.is_empty(),
843+
"rule finalize: call_rule_stack must be non-empty at pc {}",
844+
self.pc
845+
);
834846
if self.call_rule_stack.pop().is_none() {
835847
return Err(VmError::CallRuleStackUnderflow { pc: self.pc });
836848
}

src/rvm/vm/state.rs

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,125 @@ impl RegoVM {
3434

3535
// Builtin cache entries only live for a single execution
3636
self.builtins_cache.clear();
37+
38+
// Postcondition: every stack/cache that `reset_execution_state` touches
39+
// must be in its documented "clean" shape. This catches accidental
40+
// omissions in future edits to this function.
41+
self.debug_assert_state_is_clean();
42+
}
43+
44+
/// Debug-only postcondition for `reset_execution_state`.
45+
///
46+
/// Asserts the invariants every caller of `reset_execution_state` relies on
47+
/// before starting a fresh execution. The body is fully gated by
48+
/// `#[cfg(debug_assertions)]` so this is a zero-cost no-op in release.
49+
#[inline]
50+
pub(super) fn debug_assert_state_is_clean(&self) {
51+
#[cfg(debug_assertions)]
52+
{
53+
debug_assert!(
54+
self.execution_stack.is_empty(),
55+
"reset_execution_state postcondition: execution_stack must be empty"
56+
);
57+
debug_assert!(
58+
self.loop_stack.is_empty(),
59+
"reset_execution_state postcondition: loop_stack must be empty"
60+
);
61+
debug_assert!(
62+
self.comprehension_stack.is_empty(),
63+
"reset_execution_state postcondition: comprehension_stack must be empty"
64+
);
65+
debug_assert!(
66+
self.call_rule_stack.is_empty(),
67+
"reset_execution_state postcondition: call_rule_stack must be empty"
68+
);
69+
debug_assert!(
70+
self.register_stack.is_empty(),
71+
"reset_execution_state postcondition: register_stack must be empty"
72+
);
73+
debug_assert!(
74+
self.builtins_cache.is_empty(),
75+
"reset_execution_state postcondition: builtins_cache must be empty"
76+
);
77+
debug_assert_eq!(
78+
self.registers.len(),
79+
self.base_register_count,
80+
"reset_execution_state postcondition: registers must be sized to base_register_count"
81+
);
82+
debug_assert!(
83+
self.registers.iter().all(|v| matches!(v, Value::Undefined)),
84+
"reset_execution_state postcondition: all registers must be Undefined"
85+
);
86+
debug_assert_eq!(
87+
self.rule_cache.len(),
88+
self.program.rule_infos.len(),
89+
"reset_execution_state postcondition: rule_cache size must match program rule_infos"
90+
);
91+
debug_assert!(
92+
self.rule_cache.iter().all(|entry| !entry.0),
93+
"reset_execution_state postcondition: rule_cache entries must be uncomputed"
94+
);
95+
debug_assert_eq!(
96+
self.pc, 0,
97+
"reset_execution_state postcondition: pc must be 0"
98+
);
99+
debug_assert_eq!(
100+
self.executed_instructions, 0,
101+
"reset_execution_state postcondition: executed_instructions must be 0"
102+
);
103+
debug_assert!(
104+
matches!(self.execution_state, ExecutionState::Ready),
105+
"reset_execution_state postcondition: execution_state must be Ready"
106+
);
107+
}
108+
}
109+
110+
/// Per-opcode VM invariants checked from the inner dispatch loop.
111+
///
112+
/// These hold every time control re-enters the dispatch loop with another
113+
/// instruction to execute. Fully `#[cfg(debug_assertions)]`-gated so the
114+
/// method body compiles out in release.
115+
#[inline]
116+
pub(super) fn assert_vm_invariants(&self) {
117+
#[cfg(debug_assertions)]
118+
{
119+
// The dispatch loop only runs while execution is live. Once the VM
120+
// has transitioned to a terminal state (Suspended/Completed/Error)
121+
// the loop must have exited. Note `Ready` is also valid here because
122+
// some entry points (e.g. `execute_entry_point_by_index` in
123+
// RunToCompletion mode) drive `jump_to` without flipping the state.
124+
debug_assert!(
125+
matches!(
126+
self.execution_state,
127+
ExecutionState::Ready | ExecutionState::Running
128+
),
129+
"vm invariant: execution_state must be Ready or Running inside the dispatch loop, was {:?}",
130+
self.execution_state
131+
);
132+
133+
// Registers must always be non-empty when the dispatch loop is
134+
// running — every instruction operates on registers.
135+
debug_assert!(
136+
!self.registers.is_empty(),
137+
"vm invariant: register window must be non-empty inside the dispatch loop"
138+
);
139+
140+
// Rule cache is sized once at reset and must not change shape mid-run.
141+
debug_assert_eq!(
142+
self.rule_cache.len(),
143+
self.program.rule_infos.len(),
144+
"vm invariant: rule_cache size must equal program.rule_infos size"
145+
);
146+
147+
// Bound the execution stack. There is no hard MAX_FRAMES today;
148+
// 4096 is a generous safety net well above any legitimate test or
149+
// policy nesting depth and catches runaway frame-leaks early.
150+
debug_assert!(
151+
self.execution_stack.len() <= 4096,
152+
"vm invariant: execution_stack depth ({}) exceeds sanity bound",
153+
self.execution_stack.len(),
154+
);
155+
}
37156
}
38157

39158
/// Return all active objects to their respective pools for reuse

0 commit comments

Comments
 (0)