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_count, .. } => -(*field_count 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 // Superinstructions (#461). The fused op contributes its
197 // net delta (+1, same shape as a bare LoadLocal). The two
198 // inert primitive ops the peephole leaves at pc+1 / pc+2
199 // are walked as if live: their deltas (+1 PushConst, -1
200 // IntAdd) cancel, so the depth at pc+3 matches what the
201 // unfused sequence would have produced.
202 Op::LoadLocalAddIntConst { .. } => 1,
203 }
204}
205
206#[cfg(test)]
207mod tests {
208 use super::*;
209 use crate::op::Op;
210 use crate::program::Function;
211
212 fn make_fn(name: &str, code: Vec<Op>) -> Function {
213 Function {
214 name: name.to_string(),
215 arity: 0,
216 locals_count: 4,
217 code,
218 effects: vec![],
219 body_hash: crate::program::ZERO_BODY_HASH,
220 refinements: vec![],
221 }
222 }
223
224 #[test]
225 fn clean_match_no_errors() {
226 // Simulates a two-arm match that is properly balanced:
227 // LoadLocal(0) ; push scrutinee depth=1
228 // Dup ; dup depth=2
229 // TestVariant("Ok") ; pop+push Bool depth=2
230 // JumpIfNot(+3) ; pop Bool, fall or jump depth=1
231 // Pop ; pop scrutinee depth=0
232 // PushConst(0) ; push result depth=1
233 // Jump(+2) ; to end depth=1
234 // Pop ; pop scrutinee (wildcard arm) depth=0
235 // PushConst(1) ; push result depth=1
236 // Return ; end depth=0
237 let code = vec![
238 Op::LoadLocal(0), // pc 0, depth 0→1
239 Op::Dup, // pc 1, depth 1→2
240 Op::TestVariant(0), // pc 2, depth 2→2
241 Op::JumpIfNot(3), // pc 3, depth 2→1; target=pc7
242 Op::Pop, // pc 4, depth 1→0
243 Op::PushConst(0), // pc 5, depth 0→1
244 Op::Jump(2), // pc 6, depth 1→1; target=pc9
245 Op::Pop, // pc 7, depth 1→0 (wildcard arm)
246 Op::PushConst(1), // pc 8, depth 0→1
247 Op::Return, // pc 9, depth 1→0
248 ];
249 let f = make_fn("clean", code);
250 let mut errs = Vec::new();
251 verify_function(&f, &mut errs);
252 assert!(errs.is_empty(), "expected no errors, got: {errs:?}");
253 }
254
255 #[test]
256 fn leaked_scrutinee_detected() {
257 // Two paths reach pc6 at different depths — mismatch detected.
258 // Fall path: pc2→pc3→pc6 at depth 1.
259 // Jump path: pc4→pc5→pc6 at depth 2 (extra push leaks).
260 let mismatch2 = vec![
261 Op::PushConst(0), // pc0 depth 0→1
262 Op::JumpIfNot(2), // pc1 depth 1→0; fall=pc2 depth0, jump=pc4 depth0
263 Op::PushConst(0), // pc2 depth 0→1
264 Op::Jump(2), // pc3 target=pc6, depth=1
265 Op::PushConst(0), // pc4 depth 0→1
266 Op::PushConst(0), // pc5 depth 1→2
267 Op::Return, // pc6: reached at depth=1 (from pc3) AND depth=2 (from pc5+fall)
268 ];
269 let f2 = make_fn("mismatch", mismatch2);
270 let mut errs2 = Vec::new();
271 verify_function(&f2, &mut errs2);
272 assert!(!errs2.is_empty(), "expected stack mismatch error");
273 assert_eq!(errs2[0].fn_name, "mismatch");
274 }
275}