feat(output): SARIF 2.1.0 output format + three-valued verdict model#25
Merged
Conversation
…Type Two latent type-engine bugs that silently disabled semantic suppressions: 1. Relative-path @import resolution: Uri.fromPath turned a relative file_path (what `find | xargs zbc` produces every sweep, and the common CLI form) into file:///<rel> -> filesystem root -> imported files never loaded -> cross-file types (struct fields, aliases) silently unresolved. The analyzed file worked (in-memory source), so absolute-path single-file tests passed while sweeps ran token-only for cross-file facts. Fix: canonicalize via libc realpath(3) before fromPath (std.fs.path.resolve does not prepend CWD in this Zig dev version). 2. typeNameOfNode returns only container names, never primitives, so the float check it backed was dead. Added TypeResolver.isFloatType (InternPool simple_type f16/f32/f64/f80/f128/c_longdouble) + FileCache.isFloatType wrapper.
operandIsFloat used typeNameOfNode (container-only) to string-match 'f64', so it never matched any primitive -> the float suppression was dead. Switch to the new FileCache.isFloatType. Now `(start_y + end_y) / 2` where operands are f64 locals inferred through cross-file field arithmetic (ghostty font/face.zig aligned_y) is correctly suppressed; integer midpoints (bun md/unicode.zig usize) still fire. ghostty 134->128, mach 130->129; bun unchanged; all tests pass; known TPs preserved.
intInfo only matched InternPool .int_type, but usize/isize/c_short/c_int/... are simple_types, so it returned null for the most common integer type (usize). Every unsigned-operand query silently failed — notably the value-range oracle's `i > usize_var ⟹ i != 0` generalization (operandProvablyNonneg never confirmed usize as unsigned). Delegate to the canonical InternPool.intInfo(idx, target), gated on zigTypeTag==.int (it is unreachable on non-integers). Resolves usize/ isize via ptrBitWidth and c_* via cTypeBitSize, plus packed-struct/enum widths.
analyzeAssign/analyzeCompoundAdd only checked the RHS for the use token, so a provably-nonzero index on the WRITE side (`buf[idx - 1] = 0`) was never resolved — the index-minus-one oracle suppression silently didn't apply to assignment statements, only to reads/returns. Check the LHS first (the index is read before the store, so the current state is correct). 3 oracle tests incl. no-FN guard. Combined with the usize intInfo fix, the unsigned-`>` generalization now works on real shift/insert/swap loops: bun 777->773, ghostty 128->127, Ez 22->19; the vendored MultiArrayList `while (i > index) field_slice[i] = field_slice[i-1]` FP is gone. Unguarded writes and signed-RHS guards still fire (sound).
The oracle refined guards only in `if`-conditions, so the same-expression last-element idioms `c.len > 0 and c[c.len-1]` and `c.len == 0 or c[c.len-1]` (endsWith/startsWith) were unproven by the sound layer. Added bool_and/bool_or handling: in `A and B` the RHS sees A's THEN-facts; in `A or B` the RHS sees A's ELSE-facts. `return` now descends into its operand so the refinement applies. Generalizes beyond the token heuristic's fixed window (handles arbitrarily-nested uses in the RHS). 3 tests incl. no-FN guard. Corpus delta 0 (token hasAndGuard/hasOrGuard already cover the same-line cases), but subsumes them with a sound, position-independent fact — the project's token-proxy -> semantic-fact direction. All tests pass.
… facts
Two oracle completeness gaps that left provable last-element/index accesses
firing:
1. Use inside the loop CONDITION (`while (tmp > beg and self.text[tmp-1]==…)`)
was answered directly without descending — so the `and`'s short-circuit
refinement never applied. Now descends via analyzeNode (handles bool_and/or;
plain comparisons still fall through to answerAt). Clears md/blocks.zig
trim-loops.
2. A loop var that is nonzero before the loop and ONLY `+=`-mutated inside stays
nonzero on every iteration (unsigned `+=` can't wrap to 0 on a panic-on-
overflow build). dropLoopMutated now keeps such monotonic scalars instead of
dropping them. Clears `var p: usize = 1; while (…) { …a[p-1]…; p += 1; }`
(diff_match_patch). Sound: a `=`/`-=` reset still drops the fact (2 no-FN
unit tests; verified the genuine TP diff_match_patch:1030 still fires).
bun 773->757, Ez 19->18 (−17 FPs). All tests pass.
A comptime-known index can never underflow/OOB at RUNTIME: `CONST - 1` with CONST==0, or an out-of-range constant subscript, is a COMPILE error that never ships. Added TypeResolver.comptimeIntValue (via the now-public Analyser. resolveIntegerLiteral) + FileCache.comptimeIntValueOf; Form A suppresses when the index operand resolves to a comptime value. Covers `bytes[max_inline_len-1]` (max_inline_len a const usize=8) across the corpus. bun 757->749 (−8). Runtime indices still fire (verified); all 5 genuine TPs preserved. All tests pass.
A local `const s = base[0..N]` has `s.len == N` (start fixed at 0), the same
relation as a `.len` snapshot — record it as a {scalar:N, container:s} alias so
a nonzero N (e.g. after `if (N == 0) return`) proves s non-empty, making
`s[s.len-1]` safe. Immediate propagation when N is already nonzero at the decl.
bun 749->748 (PackageInstall.zig: `cache_path = buf2[0..cache_path_length]`
guarded by an earlier length==0 return). 2 tests incl. no-FN (unguarded N stays
unproven). TPs preserved; all tests pass.
Builds the cross-fn lever requested. `const m = callee(arg)` where an in-file single-return `callee` provably returns non-zero given a non-zero argument, and `arg` is proven non-zero, marks `m` non-zero. Pieces (reusing fn_summary.singleReturnExpr for return extraction): - ValueAlias on State: `const L = self.field` records local==path, so a guard on the simple local (`if (bit_length==0) return`) proves the field-path argument (`numMasks(self.bit_length)`) non-zero. Dropped on rebind / path-root mutation. - Cross-fn postcondition: callee's single return is non-zero given param non-zero, via exprNonzeroPostcond (positive literal, the param, unsigned add, ceil-div). - Ceil-div `(base + addend)/divisor` proven non-zero when base non-zero and addend >= divisor-1 — two ways: comptime values, OR STRUCTURAL (addend is syntactically `divisor - 1`). Structural is essential: the real idiom is `(x + (@bitSizeOf(MaskInt) - 1)) / @bitSizeOf(MaskInt)` and the engine does not evaluate @bitSizeOf, but addend==divisor-1 holds for any value. bun 748->744: bit_set.zig toggleSet/setAll/etc. `self.masks[numMasks(self.bit_length)-1]` (4 findings). Sound: unguarded arg still fires; all 5 genuine TPs preserved; 3 new oracle tests (incl. no-FN). All tests pass.
Re-evaluation (rigorous bucket triage) found slice-from-fixed-offset was ~90% FP,
NOT TP-dominated as I'd claimed — the driver is the wyhash hash-tail idiom
`rem_key = b[0..rem_len]; switch (rem_len) { K => rem_key[N..] }`: in arm K,
rem_len == K so rem_key.len == K, and rem_key[N..] is safe when K >= N. The engine
modeled no switch-arm facts at all.
Added:
- switch-arm exact-value facts: `switch (scalar) { K => … }` records scalar == K
(a ScalarVal) and scalar != 0, in that arm. analyzeSwitch in the oracle walk
(also fixes that switch bodies were previously unanalyzed entirely).
- provesMinLen(target, n): target.len >= n via a slice-length alias
(target.len == scalar) whose scalar has a known value >= n.
- Wired into slice-from-fixed-offset (`buf[off..]` safe when minlen >= off).
bun 744->677 (−67), ghostty 127->126. Sound: arm K < N still fires, no-switch
still fires (3 no-FN unit tests); genuine TPs (css_modules name[2..],
lower_decorators) preserved. All tests pass.
…ists The bug is a LOCAL ArrayList with capacity > len returning .items (excess capacity orphaned — caller frees items.len, leaks the rest; bun#23885). When recv is a POINTER parameter (`out: *std.ArrayList(T)`) the caller owns the list it passed and will deinit it, so returning .items is an intentional borrow into the caller's own allocation — no orphaned buffer. Only pointer params qualify: a by-value param could leak a post-append realloc, so it still fires. Finds the enclosing fn proto for the return and checks recv's param type is a pointer. bun 677->674. 2 tests (pointer-param suppressed; by-value still fires); local lists still fire. All tests pass.
….args The first `.next()` of a `std.process.args()` / `argsWithAllocator()` ArgIterator returns argv[0] (the program name), which is always present, so `.?` cannot panic — same guarantee the rule already uses for `split*`. Extended the first-next constructor check to ArgIterator (bare `args` gated on a `process.` receiver to avoid matching unrelated `.args` fields). Subsequent `.next().?` still fires. tigerbeetle 46->43. 2 tests (first suppressed, second fires).
Add `--format=sarif`, emitting a single SARIF 2.1.0 document so zbc
findings interoperate with GitHub code scanning, Azure DevOps, and the
usual dashboards instead of zbc's bespoke JSON.
Also adds a three-valued verdict to the finding model (Problem): a
`verdict` (unknown | confirmed | refuted, default unknown) and an
optional `witness` (a reproducing input). Static analysis emits
`unknown`; the field is a mechanism-agnostic slot any future confirmer
(corpus labelling, manual triage, a sound static refuter) can populate.
SARIF verdict mapping:
- every fired rule -> result `kind:"fail"`, `level` from severity,
region with line/col + byteOffset/byteLength, notes -> relatedLocations
- `properties.verdict` carries the verdict; `properties.witness` the
confirmed reproducing input
- a `refuted` finding also emits a `suppressions[]` entry
(`state:"accepted"`) so consumers treat it as a tool-dismissed FP
rules[] is populated with per-rule titles from the catalog, deduped
across findings. Validated as well-formed SARIF 2.1.0 (multi-result
rule dedup; notes -> relatedLocations). The verdict/witness also appear
in the existing `--format=json` output.
Known limitation: artifactLocation.uri is the path as given (relative or
absolute); GitHub code scanning wants repo-root-relative URIs, so a
uri-base normalization (`--sarif-base`) is a follow-up. Noted on #19,
which can adopt SARIF as its corpus/diff format (TP = result, FP =
suppression), making precision/recall a set-diff.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds
--format=sarif, emitting a single SARIF 2.1.0 document so zbc findings interoperate with GitHub code scanning, Azure DevOps, and the usual dashboards — instead of zbc's bespoke JSON array.Also lands a small, mechanism-agnostic three-valued verdict on the finding model that SARIF maps onto.
What changed
src/problem.zig—Problemgainsverdict: enum { unknown, confirmed, refuted }(defaultunknown) and an optional ownedwitness(a reproducing input). Static analysis always emitsunknown; the slot is for any future confirmer (corpus labelling, manual triage, a sound static refuter) to populate.src/lib.zig— re-exportsVerdict.src/main.zig—--format=sarif(printSarif), plusverdict/witnessnow also appear in the existing--format=json.SARIF mapping
resultwithkind:"fail"level(error/warning/none)region(line/col +byteOffset/byteLength)relatedLocationsverdictproperties.verdictconfirmedwitnessproperties.witnessrefutedsuppressions[]withstate:"accepted"(tool-dismissed FP)tool.driver.rules[](deduped, titles from catalog)Validation
zig build+ fullzig build testgreen.relatedLocations.Known limitation / follow-up
artifactLocation.uriis emitted as the path zbc was given (relative or absolute). GitHub code scanning expects repo-root-relative URIs, so a uri-base normalization (--sarif-base) is a follow-up.Relation to #19
Noted on #19: a labeled corpus is a set of findings tagged TP/FP, and SARIF already has the vocabulary — TP =
result(optionallyverdict:"confirmed"), FP =suppressionstate:"accepted". So the corpus, the tool run, and the regression diff can all be SARIF, and precision/recall becomes a set-diff. No bespoke schema needed. Closes nothing — this is foundation, not the full feature.