lab/sx
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

ERR/E1.8: path-sensitive value-slot liveness check

Browse Source 
A `v, err := failable()` destructure now binds the value slot(s) "live
only where `err` is proven absent". Reading `v` where the compiler cannot
prove `err == null` is a compile error.

New diagnostic-only Pass 1e (`checkErrorFlow` in ir/lower.zig): a
structured, path-sensitive walk over each main-file function body. A
proven-null set is threaded across branches and joined by intersection
at each `if`'s merge. Proof shapes recognized:

  - `if !err { … v … }`           (proven inside the guard)
  - `if err { return/raise } … v` (proven on the fall-through)
  - `if err { … } else { … v … }` (proven in the else branch)
  - `!err and <reads v>`          (short-circuit refinement)

Error-set tag compares (`if err == error.X`) prove nothing about
absence — they narrow the tag only. Nested lambdas are analyzed as their
own boundaries. Library modules are trusted (skipped).

Migrated the canon value-failable examples (1011/1012/1018/1044) to read
their value slots under `if !err` guards — output unchanged. New
regressions: 1046 (every proof shape compiles + runs, exit 210) and 1047
(unproven reads rejected, exit 1).

Gates: zig build, zig build test, run_examples.sh -> 338 passed, 0 failed.
This commit is contained in:
agra
2026-06-01 23:14:24 +03:00
parent 5491acbcbb
commit 296c809d85
13 changed files with 475 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

355
src/ir/lower.zig
View File

@@ -361,6 +361,12 @@ pub const Lowering = struct {
// top-level sets; before body lowering so `try slot(x)` widening sees
// the full per-shape union.
self.convergeClosureShapeSets();
// Pass 1e: error-flow checks (ERR E1.8 value-slot liveness + E1.7
// cleanup-body absorption) over the main file's functions. Runs after
// the error-set convergence passes (so failable callees resolve) and
// before body lowering — purely a diagnostic pass; `core.zig` halts on
// any error before codegen.
self.checkErrorFlow(decls);
// Pass 2: lower main (and comptime side-effects)
self.lowerMainAndComptime(decls);
// Pass 3: lower deferred functions (any_to_string etc.) now that all types are registered
@@ -440,6 +446,355 @@ pub const Lowering = struct {
}
}
// ── ERR E1.7 / E1.8 — error-flow analysis ───────────────────────────────
//
// One structured, path-sensitive walk over each MAIN-file function body
// (imported modules are trusted) drives two checks:
//
// • E1.8 (value-slot liveness): a `v, err := failable()` destructure binds
// `v` "live only where `err` is proven absent". A read of `v` is legal
// iff `err` is proven null on the current path — established by
// `if !err { … }` (proven inside) or `if err { return/raise }` (proven on
// the fall-through). Error-set `==`/tag-compares do NOT prove absence.
//
// • E1.7 (cleanup absorption): a bare failable call in a `defer`/`onfail`
// body (with no `catch` / `or value`) is rejected — its error has nowhere
// to propagate (the block is already exiting). See `checkCleanupBody`.
/// Per-function registration state for the flow walk. `bindings` maps each
/// failable value-slot variable to its partner error variable; `err_vars`
/// is the set of those error variables (so conditions over them refine the
/// proven-null set). Both are monotonic — entries are added as destructures
/// are encountered, never removed (out-of-scope names simply stop being read).
const FlowCtx = struct {
bindings: std.StringHashMap([]const u8),
err_vars: std.StringHashMap(void),
};
/// The proven-null set: error-variable names known to be absent on the
/// current path. Threaded by value-clone across branches; the join after an
/// `if` is the intersection of the reachable branches' sets.
const ProvenSet = std.ArrayList([]const u8);
fn provenHas(set: ProvenSet, name: []const u8) bool {
for (set.items) |n| if (std.mem.eql(u8, n, name)) return true;
return false;
}
fn provenAdd(self: *Lowering, set: *ProvenSet, name: []const u8) void {
if (!provenHas(set.*, name)) set.append(self.alloc, name) catch {};
}
fn provenClone(self: *Lowering, set: ProvenSet) ProvenSet {
var out = ProvenSet.empty;
out.appendSlice(self.alloc, set.items) catch {};
return out;
}
fn provenIntersect(self: *Lowering, a: ProvenSet, b: ProvenSet) ProvenSet {
var out = ProvenSet.empty;
for (a.items) |n| if (provenHas(b, n)) (out.append(self.alloc, n) catch {});
return out;
}
/// Pass 1e: run the error-flow checks over every function defined in the
/// main file. Library modules are assumed well-formed (and may use patterns
/// this conservative check would over-reject), so they are skipped.
fn checkErrorFlow(self: *Lowering, decls: []const *const Node) void {
if (self.diagnostics == null) return;
for (decls) |decl| {
if (self.main_file) |mf| {
if (decl.source_file) |sf| {
if (!std.mem.eql(u8, sf, mf)) continue;
}
}
switch (decl.data) {
.fn_decl => |fd| self.analyzeFnBody(fd.body),
.const_decl => |cd| {
if (cd.value.data == .fn_decl) self.analyzeFnBody(cd.value.data.fn_decl.body);
},
else => {},
}
}
}
/// Analyze one function (or lambda) body as its own boundary — a fresh
/// binding context and an empty proven set.
fn analyzeFnBody(self: *Lowering, body: *const Node) void {
var ctx = FlowCtx{
.bindings = std.StringHashMap([]const u8).init(self.alloc),
.err_vars = std.StringHashMap(void).init(self.alloc),
};
var proven = ProvenSet.empty;
_ = self.flowWalk(body, &ctx, &proven);
}
/// Walk a block or single statement. Returns whether control always
/// diverges (every path ends in return/raise/break/continue) — used by the
/// caller to mark code after a branch unreachable.
fn flowWalk(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: *ProvenSet) bool {
switch (node.data) {
.block => |b| {
for (b.stmts) |s| if (self.flowStmt(s, ctx, proven)) return true;
return false;
},
else => return self.flowStmt(node, ctx, proven),
}
}
fn flowStmt(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: *ProvenSet) bool {
switch (node.data) {
.destructure_decl => |dd| {
self.flowExpr(dd.value, ctx, proven.*);
self.registerFailableDestructure(&dd, ctx);
return false;
},
.var_decl => |vd| {
if (vd.value) |v| self.flowExpr(v, ctx, proven.*);
return false;
},
.const_decl => |cd| {
self.flowExpr(cd.value, ctx, proven.*);
return false;
},
.assignment => |a| {
self.flowExpr(a.value, ctx, proven.*);
self.flowExpr(a.target, ctx, proven.*);
return false;
},
.multi_assign => |ma| {
for (ma.values) |v| self.flowExpr(v, ctx, proven.*);
return false;
},
.return_stmt => |r| {
if (r.value) |v| self.flowExpr(v, ctx, proven.*);
return true;
},
.raise_stmt => |rs| {
self.flowExpr(rs.tag, ctx, proven.*);
return true;
},
.break_expr, .continue_expr => return true,
.if_expr => |ie| return self.flowIf(&ie, ctx, proven),
.while_expr => |we| {
self.flowExpr(we.condition, ctx, proven.*);
var loop_proven = self.provenClone(proven.*);
_ = self.flowWalk(we.body, ctx, &loop_proven);
return false;
},
.for_expr => |fe| {
self.flowExpr(fe.iterable, ctx, proven.*);
if (fe.range_end) |re| self.flowExpr(re, ctx, proven.*);
var loop_proven = self.provenClone(proven.*);
_ = self.flowWalk(fe.body, ctx, &loop_proven);
return false;
},
.match_expr => |me| return self.flowMatch(&me, ctx, proven),
.push_stmt => |ps| {
self.flowExpr(ps.context_expr, ctx, proven.*);
var inner = self.provenClone(proven.*);
_ = self.flowWalk(ps.body, ctx, &inner);
return false;
},
.defer_stmt => |ds| {
self.checkCleanupBody(ds.expr, "defer");
self.flowExpr(ds.expr, ctx, proven.*);
return false;
},
.onfail_stmt => |os| {
self.checkCleanupBody(os.body, "onfail");
self.flowExpr(os.body, ctx, proven.*);
return false;
},
else => {
self.flowExpr(node, ctx, proven.*);
return false;
},
}
}
/// Path-sensitive `if`: refine the proven set on each branch, recurse, and
/// join the reachable fall-through states by intersection.
fn flowIf(self: *Lowering, ie: *const ast.IfExpr, ctx: *FlowCtx, proven: *ProvenSet) bool {
self.flowExpr(ie.condition, ctx, proven.*);
var then_proven = self.provenClone(proven.*);
var else_proven = self.provenClone(proven.*);
self.applyRefinement(ie.condition, true, ctx, &then_proven);
self.applyRefinement(ie.condition, false, ctx, &else_proven);
const then_div = self.flowWalk(ie.then_branch, ctx, &then_proven);
var else_div = false;
if (ie.else_branch) |eb| else_div = self.flowWalk(eb, ctx, &else_proven);
// Reachable fall-through contributors: a branch that doesn't diverge,
// plus the implicit (empty) else when there is no `else`.
var contributors = std.ArrayList(ProvenSet).empty;
if (!then_div) contributors.append(self.alloc, then_proven) catch {};
if (ie.else_branch != null) {
if (!else_div) contributors.append(self.alloc, else_proven) catch {};
} else {
contributors.append(self.alloc, else_proven) catch {};
}
if (contributors.items.len == 0) return true; // both branches diverge
var result = self.provenClone(contributors.items[0]);
for (contributors.items[1..]) |c| result = self.provenIntersect(result, c);
proven.* = result;
return false;
}
/// Refine the proven-null set for a branch taken when `cond` is `want_true`.
/// A bare error-variable is truthy when it HOLDS an error, so its falsy edge
/// proves absence; `!`, `&&`, `||` compose. Tag/equality compares prove
/// nothing (error-set `==` compares tags, not presence).
fn applyRefinement(self: *Lowering, cond: *const Node, want_true: bool, ctx: *FlowCtx, set: *ProvenSet) void {
switch (cond.data) {
.identifier => |id| {
if (ctx.err_vars.contains(id.name) and !want_true) self.provenAdd(set, id.name);
},
.unary_op => |uop| {
if (uop.op == .not) self.applyRefinement(uop.operand, !want_true, ctx, set);
},
.binary_op => |bop| {
if (bop.op == .and_op and want_true) {
self.applyRefinement(bop.lhs, true, ctx, set);
self.applyRefinement(bop.rhs, true, ctx, set);
} else if (bop.op == .or_op and !want_true) {
self.applyRefinement(bop.lhs, false, ctx, set);
self.applyRefinement(bop.rhs, false, ctx, set);
}
},
else => {},
}
}
fn flowMatch(self: *Lowering, me: *const ast.MatchExpr, ctx: *FlowCtx, proven: *ProvenSet) bool {
self.flowExpr(me.subject, ctx, proven.*);
for (me.arms) |arm| {
var arm_proven = self.provenClone(proven.*);
_ = self.flowWalk(arm.body, ctx, &arm_proven);
}
return false;
}
/// Check an expression for reads of a still-tainted value-slot variable and
/// recurse into nested lambdas as their own boundaries. `proven` is by value
/// — sub-expressions never publish proven-null facts back to the statement.
fn flowExpr(self: *Lowering, node: *const Node, ctx: *FlowCtx, proven: ProvenSet) void {
switch (node.data) {
.identifier => |id| {
if (ctx.bindings.get(id.name)) |err_var| {
if (!provenHas(proven, err_var)) {
if (self.diagnostics) |d| d.addFmt(.err, node.span, "value `{s}` from a failable can be used only where its error `{s}` is proven absent — guard the use with `if !{s} {{ … }}`, or return early with `if {s} {{ return; }}` before reading `{s}`", .{ id.name, err_var, err_var, err_var, id.name });
}
}
},
.lambda => |lam| self.analyzeFnBody(lam.body),
.binary_op => |b| {
self.flowExpr(b.lhs, ctx, proven);
// Short-circuit: the rhs of `&&` runs only when the lhs is true
// (and `||`'s rhs only when the lhs is false), so refine the
// proven-null set accordingly before checking it. This is what
// makes `if !err && use(v)` legal.
if (b.op == .and_op or b.op == .or_op) {
var rp = self.provenClone(proven);
self.applyRefinement(b.lhs, b.op == .and_op, ctx, &rp);
self.flowExpr(b.rhs, ctx, rp);
} else {
self.flowExpr(b.rhs, ctx, proven);
}
},
.chained_comparison => |cc| {
for (cc.operands) |op| self.flowExpr(op, ctx, proven);
},
.unary_op => |u| self.flowExpr(u.operand, ctx, proven),
.call => |c| {
self.flowExpr(c.callee, ctx, proven);
for (c.args) |a| self.flowExpr(a, ctx, proven);
},
.field_access => |fa| self.flowExpr(fa.object, ctx, proven),
.index_expr => |ix| {
self.flowExpr(ix.object, ctx, proven);
self.flowExpr(ix.index, ctx, proven);
},
.slice_expr => |se| {
self.flowExpr(se.object, ctx, proven);
if (se.start) |s| self.flowExpr(s, ctx, proven);
if (se.end) |e| self.flowExpr(e, ctx, proven);
},
.try_expr => |te| self.flowExpr(te.operand, ctx, proven),
.catch_expr => |ce| {
self.flowExpr(ce.operand, ctx, proven);
self.flowExpr(ce.body, ctx, proven);
},
.force_unwrap => |fu| self.flowExpr(fu.operand, ctx, proven),
.null_coalesce => |nc| {
self.flowExpr(nc.lhs, ctx, proven);
self.flowExpr(nc.rhs, ctx, proven);
},
.deref_expr => |de| self.flowExpr(de.operand, ctx, proven),
.comptime_expr => |ce| self.flowExpr(ce.expr, ctx, proven),
.insert_expr => |ie| self.flowExpr(ie.expr, ctx, proven),
.spread_expr => |se| self.flowExpr(se.operand, ctx, proven),
.struct_literal => |sl| {
for (sl.field_inits) |fi| self.flowExpr(fi.value, ctx, proven);
},
.array_literal => |al| {
for (al.elements) |el| self.flowExpr(el, ctx, proven);
},
.tuple_literal => |tl| {
for (tl.elements) |el| self.flowExpr(el.value, ctx, proven);
},
.if_expr => |ie| {
var tmp = self.provenClone(proven);
_ = self.flowIf(&ie, ctx, &tmp);
},
.match_expr => |me| {
var tmp = self.provenClone(proven);
_ = self.flowMatch(&me, ctx, &tmp);
},
.block => |b| {
var tmp = self.provenClone(proven);
for (b.stmts) |s| if (self.flowStmt(s, ctx, &tmp)) break;
},
else => {},
}
}
/// Register a `v…, err := failable()` destructure. Only a complete bare
/// destructure (every slot bound, error slot a real name) creates taint —
/// an omitted or `_`-bound error slot is already rejected by the discard
/// check in `lowerDestructureDecl`, so it produces no proof obligation here.
fn registerFailableDestructure(self: *Lowering, dd: *const ast.DestructureDecl, ctx: *FlowCtx) void {
const ty = self.inferExprType(dd.value);
if (self.errorChannelOf(ty) == null) return;
if (ty.isBuiltin()) return;
const ti = self.module.types.get(ty);
if (ti != .tuple) return;
const fields = ti.tuple.fields;
if (dd.names.len != fields.len) return;
const err_name = dd.names[fields.len - 1];
if (std.mem.eql(u8, err_name, "_")) return;
ctx.err_vars.put(err_name, {}) catch {};
var i: usize = 0;
while (i + 1 < dd.names.len) : (i += 1) {
const vn = dd.names[i];
if (std.mem.eql(u8, vn, "_")) continue;
ctx.bindings.put(vn, err_name) catch {};
}
}
/// E1.7: a `defer`/`onfail` body runs while the block is already exiting, so
/// a bare failable call has nowhere to send its error. Reject any failable
/// expression-statement that isn't absorbed locally by `catch` / `or value`
/// / a destructure binding. (Parser already bans `try`/`raise`/`return`/
/// `break`/`continue` here.) Stub until slice B.
fn checkCleanupBody(self: *Lowering, body: *const Node, kind: []const u8) void {
_ = self;
_ = body;
_ = kind;
}
/// On Android, the OS loads the .so via a Java-side Activity declared
/// with `#jni_main #jni_class("...")`. The Java class drives the
/// lifecycle (onCreate / onPause / etc.) and sx provides the native