Problem: normalizeClangTuPath, normalizeQuarantinePath and fan-out's
normalizePath were three copies of the same absolute + weakly_canonical
routine. Coverage, worker records and the quarantine file must agree on a
TU's spelling, and three copies can drift apart.
Fix: move the routine to fold/cli/tu_path.hpp as normalizeTuPath and use it
at every site. No behaviour change.
Test: existing test_scan_coverage (path spellings), test_tu_quarantine and
test_subprocess_fanout, updated to the new name. Full suite: 140/140.
Problem: null-deref, div-by-zero and int-overflow re-check a portfolio
verdict on the reporting solver and reconcile the two, but then memoized the
re-check's unsat core (and read its model) from the raw re-check result. A
portfolio SAT that the re-check called UNSAT became unknown, yet its core was
still reused as the assumptions for later queries on the same path. The
disagreement itself was silent: no stat, and the trace showed the portfolio's
verdict.
Fix: all six sites use symbolic::recheckPortfolioVerdict and act only on the
reconciled verdict, so an unknown leaves no core or model behind. The helper
counts SolverStats::portfolio_disagreements (merged, printed, and exported in
the detector profile), and the sites trace
"UNKNOWN (portfolio re-check disagreed)".
Test: test_model_validation "[portfolio]" checks the helper's agreement,
unknown and disagreement cases and the merged counter. Full suite: 140/140.
Problem: a TU skipped because a prior run quarantined it was not analysed,
but coverage did not say so. The serial path dropped it from the attempted
set, so a scan whose only TU was quarantined was complete and exited 0; the
fan-out path saw no file_finished record and called it frontend-failed.
Fix: the shard runner counts every requested TU and records skipped ones
with gap reason `quarantined`; a worker emits a file_finished record with
that reason so the parent classifies it the same way. USAGE lists the reason.
Test: test_subprocess_fanout "[quarantine]" covers serial (was 2 attempted,
no gap) and fan-out (was frontend-failed). CLI probe: serial and fan-out
both exit 2 with a `quarantined` gap.
Problem: isCLibraryFunction accepted any global-scope non-member function,
so a project's `void free(Obj*)` overload was modeled as libc free: calling
it twice was a double free, and reading after it a use-after-free.
Fix: a global function counts only when it is extern "C", in namespace std,
or declared in a system header. extern "C" also covers C translation units,
where external functions have C language linkage.
Test: test_library_callee_identity "[global]" (DoubleFree and UseAfterFree
now 0; were 1 each); test_encoder_callee_names flips the global C++ helper
to not-a-library-callee. Full suite: 140/140.
Problem: with --portfolio the OOB and UAF detectors took the portfolio's
SAT/UNSAT answer as final. The portfolio solves on its own contexts, so the
reporting solver was never checked: OOB read its counterexample from an
unchecked solver (i=0 under `i > 5`), and a SAT the reporting solver would
not reproduce was still emitted. Other detectors already fail closed through
reconcilePortfolioRecheck.
Fix: add symbolic::recheckPortfolioVerdict, which re-checks a decided verdict
on the reporting solver and reconciles the two (disagreement or timeout ->
unknown), and apply it at the four OOB and two UAF portfolio sites. The
now-redundant UNSAT-only artifact re-checks in OOB checkHazard are removed.
Test: test_proved_requires_exact_model "[portfolio]" requires the portfolio
counterexample to satisfy the path (was i=0, now i=6).
Problem: OOBObserver::emit marked every constant-index array OOB as Proved,
even when the path reaching the access was over-approximated (an opaque call
or a truncated loop). The heap and UAF paths already gated on exactEncoding.
Fix: pass exactEncoding(env) into emit and require it alongside a numeral
index before assigning Proved; otherwise the finding is Heuristic.
Test: test_proved_requires_exact_model "[oob]" adds an exact control (stays
Proved) and an opaque-call path (now Heuristic; was Proved).
Two gaps in the loop-exit soundness rule from 6adcc24, both found in
review and reproduced as Proved always-conditions:
- `continue` was not an escape. The walkers drop an arm that ends in
`continue` (it always leaves the iteration), so iterations that took it
were never modeled, yet the unroll still counted as exact and the
loop's variables were not havocked:
for (i = 0; i < 2; i++) { if (y) continue; x++; } if (x == 2)
was "always true" although y != 0 gives x == 0. containsLoopEscape now
treats a continue that targets the loop as an escape (a switch
captures break but not continue; a nested loop captures both).
- Havocking a truncated loop reset scalar variables only. Array element
and member stores from the partial unroll survived:
for (i = 0; i < n && i < 4; i++) buf[i] = 1; if (buf[0] == 1)
was "always true" although n == 0 leaves buf[0] == 0. The unroll now
records the base variables of array/member stores and replaces their
arrays/values with fresh ones of the same sort; a store through a
pointer havocs every tracked heap array (SymbolicEnv::havocHeapArrays)
and marks the env over-approximated. The three walkers share this via
LoopUnrollExits::havoc.
Tests (test_loop_exit_soundness): continue, local-array and heap-pointer
stores are no longer Proved by dead-branch, always-condition or
unreachable; the exact constant-bound loop stays Proved (negative
control). A pointer-mutating call inside the loop (review #9) did not
reproduce for unreachable; its case is kept as a regression guard.
The README listed 11 of fold's 17 detectors, never explained the
confidence tiers every finding carries, did not mention the new exit
code 2 / coverage reporting, and spent half its length on a
performance roadmap.
It now says what fold is, defines the five tiers (from
include/fold/report/finding.hpp, including concrete-witness and
latent), what "bounded" means after the loop-exit fix, a quick start,
output formats and exit codes (0 none, 1 any unsuppressed finding, 2
unwritable report or any unanalysed translation unit), and links. The
detector list defers to the complete table in docs/USAGE.md.
The performance section moves to docs/architecture/performance.md, with
one correction: the gold set was derived from fold's own reviewed output
and is matched by detector kind and file, so it catches drift rather
than measuring precision/recall independently. The lint pre-commit hook
note moves to BUILD.md.
Problem: docs/positioning.md claimed four confidence tiers (there are
five, including Latent) and defined Proved as any Z3 SAT, which
contradicts soundness.md's exact-model requirement. It claimed "fold
scans a 100k-LOC codebase in minutes" with no committed benchmark (the
audit measured 2 files in 5.9 s at 407 MB RSS). It described CBMC as
asking Z3/MathSAT (its default back end is SAT) and as scaling poorly
past a few thousand lines, without support. It claimed a scan-to-fuzz
loop "no other open-source analyzer covers" and "no commercial vendor
ships" (directed and hybrid fuzzers such as AFLGo and SAVIOR cover
related ground, and prior-art.md cites that line of work). It said most
analyzers "stop at SAT", ignoring the Clang Static Analyzer's Z3
refutation.
Fix: five tiers with Latent defined; Proved requires an exact bounded
model; the CBMC comparison describes the method and fold's real scope
(per-sink, mostly intraprocedural, unroll 5) instead of speed; the
uniqueness claims now describe the loop without exclusivity; CSA's Z3
refutation is acknowledged. The README is left for a separate docs pass.
Problem: the README said setup enables "tracked ... OpenGrep pre-push
hooks", but only .githooks/pre-commit is tracked, so fresh clones get no
pre-push hook. docs/research/prior-art.md pointed to prior-art-full.md,
which has never been in the repository. test_mcp_stdio's TempDir
destructor called the throwing remove_all overload; a failure during
unwinding terminates the test binary and leaves .fold-mcp-test-*
directories behind.
Fix: the README names only the tracked pre-commit hook. The pre-push
hook is not committed: it runs `opengrep --config auto`, which needs the
network. The dead reference is removed. TempDir uses the error_code
remove_all overload. It stays under the working directory, because the
MCP server rejects paths outside its workspace root (moving it to
temp_directory_path broke three MCP tests).
Test: mcp_stdio passes.
Problem: symbols are 64-bit bitvectors whose low bits carry the source
value, but int-overflow witnesses printed the whole bitvector. For a
32-bit `int a` the report showed a=2147483648 or a=-9223372034707292160,
which are not values of `a` and would make bad fuzz seeds
(tests/fixtures/clones/exact.cpp).
Fix: detect::sourceIntTypesOf() maps the function's integer parameters
and locals to their width and signedness (a name declared with two types
is left out). collectModelBindings() takes that map and prints each bound
symbol truncated to its source width with its signedness
(formatSourceIntValue). int-overflow passes the map for the current
function; other detectors are unchanged.
Test: test_int_overflow "[witness]": every binding for an `int` overflow
lies in int range, and formatSourceIntValue covers sign/width cases.
exact.cpp before: a=2147483648, a=3221225471. After: a=-2147483648,
a=-1073741825, the int values that actually overflow.
Problem: with --portfolio, null-deref, div-by-zero and int-overflow take
the verdict from a separate portfolio solver, then re-check on their own
solver only to obtain a model or unsat core. The re-check's result was
never compared: if it timed out (unknown) or disagreed, the portfolio's
SAT still produced a finding, with no model from the reporting solver.
Fix: symbolic::reconcilePortfolioRecheck() keeps the verdict only when
the re-check reproduces it and otherwise returns unknown. It is applied
at all six re-check sites.
Test: test_model_validation "portfolio verdicts stand only when the
re-check agrees" covers agreement, re-check unknown, and disagreement in
both directions. null_deref, int_overflow, div_by_zero and
source_structure pass.
Problem: SummaryStore keyed summaries by getQualifiedNameAsString (plus
"@file" for internal linkage), which overloads share. When a TU calls a
function whose body lives in another TU, the lookup returns whichever
overload was summarized last. Example: `take(int*, int)` dereferences p,
`take(int*, long)` checks it, and a call `take(q, 1L)` with a null q was
reported as a null-deref because it inherited the other overload's nonnull
precondition. Lookups also used a different spelling (no "@file") than
stores for static functions, so their summaries were never found at call
sites.
Fix: summaryStoreKey()/summaryStoreKeyForCall() return the declaration's
USR (semanticFunctionId: USR, TU-qualified for internal linkage). Every
clang-side store, lookup, dependency edge and staleness check uses it:
summary_encoder, null-deref, div-by-zero, OOB and the summary priming
pipeline, which still selects targets by the call graph's qualified names.
Rust summaries keep their own keys. Now that static callees' summaries
are found, null-deref's summary-precondition path applies the same
DEBUGASSERT and static-parameter-contract filters as its callee-deref
path.
Test: tests/unit/test_summary_key_identity.cpp covers per-overload
summaries, key identity across redeclarations and distinct keys across
namespaces, and the cross-TU overload call. That call reported a false
null-deref before the fix; a control call to the dereferencing overload
still reports one. Tests that hand-built the old keys
(test_symbolic_summary, test_cross_tu_security) now derive them from the
declaration. Full suite: 140/140 (rust_frontend's 500 ms timeout test
flaked once at load average 22 and passed on four reruns).
Problem: a TU the front end could not parse left no trace. ClangTool::run's
status was discarded, TUs with compile errors were analyzed on a partial
AST and counted as done, and the isolated-worker path dropped TUs that
never produced an AST. A scan of only broken files printed no findings and
exited 0, the same as a clean scan. Separately, the scan logger wrote to
stdout, so any warning corrupted a SARIF/JSON report written to stdout.
Fix: every TU now yields an outcome (clean, compile-errors,
analysis-failed); workers carry it on their file_finished record, and the
fan-out parent adds timeout/crash/worker-exit for the TU a worker died on.
tuCoverage() turns the requested file list plus outcomes into a
ScanCoverage (requested TUs with no outcome are frontend-failed). SARIF
gets a run `invocations` entry (executionSuccessful, one
toolExecutionNotification per gap); findings JSON gets an additive
`coverage` object. A scan with any gap, or with nothing analyzed, exits 2
after writing its report. CLI diagnostics now go to stderr, as
docs/internal/cli-philosophy.md principle 12 requires. USAGE.md and
AGENTS.md document the coverage fields and the exit code.
Test: tests/unit/test_scan_coverage.cpp (classification, path spelling,
complete/untracked controls, merge, both writers, and unchanged output
without coverage); test_cli_paths "[coverage]" covers a clean TU (exit 0,
complete) and a TU with a missing include (exit 2, gap in JSON, SARIF on
stdout parseable with executionSuccessful=false). Before: both probe files
exited 0 with no coverage information. Full suite: 139/139.
Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.
Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.
Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.
malloc/free heap modeling (encoder), use-after-free's free/realloc, and
the taint source/sink tables selected a model by the callee's bare
identifier. A project function that merely shares a libc name was
modeled as libc:
namespace mine { void free(void*); }
mine::free(p); ... std::free(p); // double-free "proved", plus
// oob "double free" and a UAF
and `Pool::free(p)` behaved the same way, as did a member function
named `system` as a command-execution sink.
isCLibraryFunction / isCLibraryCallee (encoder_callee_names) accept a
direct callee that is not a class member and is declared at global
scope, in namespace std, or extern "C". The encoder's malloc-family and
free models, use-after-free's free/realloc, and every libc/POSIX taint
entry now require it. Entries that are deliberately method-name
heuristics (get, Query, execute, query, fromJson, readString*, the
request-parameter getters) are marked c_api = false and keep matching
by name as before.
Tests: test_library_callee_identity (namespaced and member `free` are
not double-free/UAF; member `system` is not a sink; libc free twice and
libc system(getenv()) still are), and isCLibraryCallee cases in
test_encoder_callee_names (::free, std::free, mine::free, Pool::free,
a global helper, an indirect call). Full suite 137/137.
The dead-branch, always-condition and unreachable walkers unroll loops
loop_unroll times, following only the path on which the guard holds.
When the guard could also be false (any symbolic bound), that early
exit was dropped, and the loop's assigned variables were havocked only
for loops containing calls. The state after the loop was therefore
"the loop ran exactly loop_unroll times", and conditions on it were
reported as Proved:
int s = 0; for (unsigned i = 0; i < n; ++i) s += 1;
if (s == 0) ... // "dead" proved/exact, "always false" proved
The same held for `s > 100`, while loops, and a `break` out of a
constant loop. On the audit probes this was 7 Proved findings, all
false.
LoopUnrollExits now records whether the unroll saw every way out of
the loop: no iteration could exit early (the guard's false branch was
infeasible), the unroll stopped because the guard became infeasible
rather than because loop_unroll ran out, and the body has no break or
goto that escapes. When any of that fails, the walker havocs the loop's
assigned variables and restores the entry path, as it already did for
opaque loops. A loop the unroll exits exactly (constant bound within
budget) keeps its precise state, so a genuinely dead branch after it
is still Proved.
Loop-bound provenance (--suppress-loop-bound-always-conditions) stays
off by default: it existed to downgrade proofs that leaned on the
unroll bound, and an inexact loop exit now havocs instead of producing
such a proof in the first place.
The duplicated helpers (containsCallExpr, collectAssignedVars,
appendAssignedVars, havocAssignedVars) move from dead_branch.cpp and
always_condition.cpp into detect/loop_havoc so all three walkers share
them; dead_branch.cpp drops under the 800-line soft cap.
Tests: test_loop_exit_soundness covers the symbolic-bound cases for all
three detectors (4 Proved each for dead and always-condition before),
the break escape, the exact-loop negative control, and the extracted
helpers (containsLoopEscape, LoopUnrollExits). Full suite 136/136.
fold:subprocess_fanout reads FOLD_TEST_FANOUT_FAILURE_WORKER, but the
worker target is build_by_default: false and the test declared
`depends: []`, so a plain `meson test -C build/release` ran the two
recovery cases against a binary that was never built and failed both
(`REQUIRE(std::filesystem::exists(helper))`). The test now depends on
the worker, and the suite is green from a fresh build.
