lex_bytecode/verify.rs
1//! Bytecode stack-depth verifier — the third `--strict` check from #347 A2.
2//!
3//! Walks every function's instruction stream, tracking the abstract stack
4//! depth through each opcode and branch. Reports a `StackError` when two
5//! paths into the same program counter carry different depths, which would
6//! mean a prior match arm leaked (or over-consumed) values and left the
7//! stack in an inconsistent state for subsequent arms.
8//!
9//! The check is lightweight: it is a single linear pass with a small
10//! worklist. No allocation beyond `Vec` is needed.
11//!
12//! # Known sound over-approximation
13//!
14//! `Return` and `Panic` terminate the function; their successors are not
15//! added to the worklist. `TailCall` is treated like `Return`. This means
16//! dead code after a `Return` / `Panic` is not checked — intentional.
17
18use crate::op::Op;
19use crate::program::Function;
20
21#[derive(Debug, Clone, PartialEq)]
22pub struct StackError {
23 pub fn_name: String,
24 pub pc: usize,
25 pub depth_a: i32,
26 pub depth_b: i32,
27}
28
29impl std::fmt::Display for StackError {
30 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
31 write!(
32 f,
33 "stack depth mismatch in `{}` at pc {}: path A leaves depth {}, path B leaves depth {}",
34 self.fn_name, self.pc, self.depth_a, self.depth_b
35 )
36 }
37}
38
39/// Verify all functions in a slice. Returns one error per inconsistent
40/// merge point found.
41pub fn verify_program(functions: &[Function]) -> Vec<StackError> {
42 let mut errors = Vec::new();
43 for func in functions {
44 verify_function(func, &mut errors);
45 }
46 errors
47}
48
49/// Verify a single function. Appends to `errors`.
50pub fn verify_function(func: &Function, errors: &mut Vec<StackError>) {
51 let n = func.code.len();
52 if n == 0 {
53 return;
54 }
55
56 // `depths[pc]` = known stack depth at that pc, or `None` if not yet visited.
57 let mut depths: Vec<Option<i32>> = vec![None; n];
58
59 // Worklist: (pc, stack_depth_on_entry_to_this_instruction)
60 let mut worklist: Vec<(usize, i32)> = vec![(0, 0)];
61
62 while let Some((pc, depth)) = worklist.pop() {
63 if pc >= n {
64 continue;
65 }
66
67 // Merge-point check.
68 if let Some(prev) = depths[pc] {
69 if prev != depth {
70 errors.push(StackError {
71 fn_name: func.name.clone(),
72 pc,
73 depth_a: prev,
74 depth_b: depth,
75 });
76 }
77 // Already processed from this depth (or recorded mismatch).
78 continue;
79 }
80 depths[pc] = Some(depth);
81
82 let op = &func.code[pc];
83 let delta = stack_delta(op);
84 let next_depth = depth + delta;
85
86 match op {
87 // Unconditional jumps: only the target is a successor.
88 Op::Jump(off) => {
89 let target = (pc as i32 + 1 + off) as usize;
90 worklist.push((target, next_depth));
91 }
92 // Conditional jumps: fall-through and jump target are both successors.
93 // Note: JumpIf / JumpIfNot pop the Bool before branching, so `delta`
94 // already accounts for that (-1). Both successors start at next_depth.
95 Op::JumpIf(off) | Op::JumpIfNot(off) => {
96 let target = (pc as i32 + 1 + off) as usize;
97 worklist.push((pc + 1, next_depth));
98 worklist.push((target, next_depth));
99 }
100 // Terminators: no successors.
101 Op::Return | Op::TailCall { .. } | Op::Panic(_) => {}
102 // All other ops: single sequential successor.
103 _ => {
104 worklist.push((pc + 1, next_depth));
105 }
106 }
107 }
108}
109
110/// Returns the net change in stack depth caused by `op`.
111///
112/// Positive = pushes more than it pops.
113/// Negative = pops more than it pushes.
114fn stack_delta(op: &Op) -> i32 {
115 match op {
116 // Stack manipulation
117 Op::PushConst(_) => 1,
118 Op::Pop => -1,
119 Op::Dup => 1,
120
121 // Locals
122 Op::LoadLocal(_) => 1,
123 Op::StoreLocal(_) => -1,
124
125 // Record / tuple / list construction
126 Op::MakeRecord { field_name_indices } => -(field_name_indices.len() as i32) + 1,
127 Op::MakeTuple(n) => -(*n as i32) + 1,
128 Op::MakeList(n) => -(*n as i32) + 1,
129 Op::MakeVariant { arity, .. } => -(*arity as i32) + 1,
130
131 // Field/element access: pop 1, push 1
132 Op::GetField(_) => 0,
133 Op::GetElem(_) => 0,
134 Op::GetListElem(_) => 0,
135 Op::GetListLen => 0,
136
137 // Variant ops: pop 1, push 1
138 Op::TestVariant(_) => 0,
139 Op::GetVariant(_) => 0,
140 Op::GetVariantArg(_)=> 0,
141
142 // Binary list ops: pop 2, push 1
143 Op::ListAppend => -1,
144 Op::GetListElemDyn => -1,
145
146 // Jumps: delta handled in the control-flow logic above; use 0 here
147 // so that next_depth = depth + 0 is the "effective post-instruction depth"
148 // before branching. The successor depths are added by the control-flow arms.
149 Op::Jump(_) | Op::JumpIf(_) | Op::JumpIfNot(_) => {
150 // JumpIf/JumpIfNot pop the Bool.
151 match op {
152 Op::JumpIf(_) | Op::JumpIfNot(_) => -1,
153 _ => 0,
154 }
155 }
156
157 // Calls: pop arity args, push 1 result
158 Op::Call { arity, .. } => -(*arity as i32) + 1,
159 Op::TailCall { arity, .. } => -(*arity as i32) + 1,
160 Op::CallClosure { arity, .. }=> -(*arity as i32 + 1) + 1, // also pops closure
161 Op::EffectCall { arity, .. } => -(*arity as i32) + 1,
162
163 // Closure construction: pop captures, push closure
164 Op::MakeClosure { capture_count, .. } => -(*capture_count as i32) + 1,
165
166 // Higher-order ops: pop list + fn, push result list
167 Op::SortByKey { .. } => -1,
168 Op::ParallelMap { .. }=> -1,
169
170 // Terminators
171 Op::Return => -1, // pop return value
172 Op::Panic(_)=> 0, // does not matter (no successor)
173
174 // Arithmetic / comparison — all binary except Neg/Not
175 Op::IntAdd | Op::IntSub | Op::IntMul | Op::IntDiv | Op::IntMod => -1,
176 Op::IntEq | Op::IntLt | Op::IntLe => -1,
177 Op::IntNeg => 0,
178
179 Op::FloatAdd | Op::FloatSub | Op::FloatMul | Op::FloatDiv => -1,
180 Op::FloatEq | Op::FloatLt | Op::FloatLe => -1,
181 Op::FloatNeg => 0,
182
183 Op::NumAdd | Op::NumSub | Op::NumMul | Op::NumDiv | Op::NumMod => -1,
184 Op::NumEq | Op::NumLt | Op::NumLe => -1,
185 Op::NumNeg => 0,
186
187 Op::BoolAnd | Op::BoolOr => -1,
188 Op::BoolNot => 0,
189
190 Op::StrConcat => -1,
191 Op::StrLen => 0,
192 Op::StrEq => -1,
193 Op::BytesLen => 0,
194 Op::BytesEq => -1,
195 }
196}
197
198#[cfg(test)]
199mod tests {
200 use super::*;
201 use crate::op::Op;
202 use crate::program::Function;
203
204 fn make_fn(name: &str, code: Vec<Op>) -> Function {
205 Function {
206 name: name.to_string(),
207 arity: 0,
208 locals_count: 4,
209 code,
210 effects: vec![],
211 body_hash: crate::program::ZERO_BODY_HASH,
212 refinements: vec![],
213 }
214 }
215
216 #[test]
217 fn clean_match_no_errors() {
218 // Simulates a two-arm match that is properly balanced:
219 // LoadLocal(0) ; push scrutinee depth=1
220 // Dup ; dup depth=2
221 // TestVariant("Ok") ; pop+push Bool depth=2
222 // JumpIfNot(+3) ; pop Bool, fall or jump depth=1
223 // Pop ; pop scrutinee depth=0
224 // PushConst(0) ; push result depth=1
225 // Jump(+2) ; to end depth=1
226 // Pop ; pop scrutinee (wildcard arm) depth=0
227 // PushConst(1) ; push result depth=1
228 // Return ; end depth=0
229 let code = vec![
230 Op::LoadLocal(0), // pc 0, depth 0→1
231 Op::Dup, // pc 1, depth 1→2
232 Op::TestVariant(0), // pc 2, depth 2→2
233 Op::JumpIfNot(3), // pc 3, depth 2→1; target=pc7
234 Op::Pop, // pc 4, depth 1→0
235 Op::PushConst(0), // pc 5, depth 0→1
236 Op::Jump(2), // pc 6, depth 1→1; target=pc9
237 Op::Pop, // pc 7, depth 1→0 (wildcard arm)
238 Op::PushConst(1), // pc 8, depth 0→1
239 Op::Return, // pc 9, depth 1→0
240 ];
241 let f = make_fn("clean", code);
242 let mut errs = Vec::new();
243 verify_function(&f, &mut errs);
244 assert!(errs.is_empty(), "expected no errors, got: {errs:?}");
245 }
246
247 #[test]
248 fn leaked_scrutinee_detected() {
249 // Two paths reach pc6 at different depths — mismatch detected.
250 // Fall path: pc2→pc3→pc6 at depth 1.
251 // Jump path: pc4→pc5→pc6 at depth 2 (extra push leaks).
252 let mismatch2 = vec![
253 Op::PushConst(0), // pc0 depth 0→1
254 Op::JumpIfNot(2), // pc1 depth 1→0; fall=pc2 depth0, jump=pc4 depth0
255 Op::PushConst(0), // pc2 depth 0→1
256 Op::Jump(2), // pc3 target=pc6, depth=1
257 Op::PushConst(0), // pc4 depth 0→1
258 Op::PushConst(0), // pc5 depth 1→2
259 Op::Return, // pc6: reached at depth=1 (from pc3) AND depth=2 (from pc5+fall)
260 ];
261 let f2 = make_fn("mismatch", mismatch2);
262 let mut errs2 = Vec::new();
263 verify_function(&f2, &mut errs2);
264 assert!(!errs2.is_empty(), "expected stack mismatch error");
265 assert_eq!(errs2[0].fn_name, "mismatch");
266 }
267}