From 76bc00f635c75596cef353b415e292038109bb94 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:00:17 -0600 Subject: [PATCH 01/18] test(fanout): build the failure worker before the recovery tests 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. --- tests/integration/meson.build | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/integration/meson.build b/tests/integration/meson.build index f0264dd..355da01 100644 --- a/tests/integration/meson.build +++ b/tests/integration/meson.build @@ -44,7 +44,10 @@ test_subprocess_fanout = executable( # fan-out can spawn it. fold_bin = meson.project_build_root() / 'src' / 'cli' / 'fold' test('subprocess_fanout', test_subprocess_fanout, - depends: [], # fold executable target lives in src/cli — referenced via path + # fold lives in src/cli and is referenced via path. The failure worker is + # build_by_default: false, so without this dependency `meson test` ran the + # recovery cases against a helper that was never built and failed them. + depends: [fanout_failure_worker], env: { 'FOLD_FIXTURES_DIR': join_paths(meson.current_source_dir(), '..', 'fixtures'), 'FOLD_WORKER_BINARY': fold_bin, -- 2.52.0 From 6adcc24e2abe0c625bae950da8528e225a3c35c9 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:08:19 -0600 Subject: [PATCH 02/18] fix(detect): never prove post-loop conditions from a bounded unroll 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. --- include/fold/detect/loop_havoc.hpp | 66 +++++++++ src/detect/always_condition.cpp | 112 ++++----------- src/detect/dead_branch.cpp | 99 ++++--------- src/detect/loop_havoc.cpp | 125 +++++++++++++++++ src/detect/meson.build | 1 + src/detect/unreachable.cpp | 29 +++- tests/unit/meson.build | 9 ++ tests/unit/test_loop_exit_soundness.cpp | 179 ++++++++++++++++++++++++ 8 files changed, 456 insertions(+), 164 deletions(-) create mode 100644 include/fold/detect/loop_havoc.hpp create mode 100644 src/detect/loop_havoc.cpp create mode 100644 tests/unit/test_loop_exit_soundness.cpp diff --git a/include/fold/detect/loop_havoc.hpp b/include/fold/detect/loop_havoc.hpp new file mode 100644 index 0000000..f102771 --- /dev/null +++ b/include/fold/detect/loop_havoc.hpp @@ -0,0 +1,66 @@ +#pragma once + +#include + +#include "fold/symbolic/encoder.hpp" + +namespace clang { +class Stmt; +class VarDecl; +} // namespace clang + +namespace fold::detect { + +// Shared by the control-flow walkers (dead-branch, always-condition, +// unreachable) that unroll loops a bounded number of times. + +[[nodiscard]] bool containsCallExpr(const clang::Stmt* stmt); + +// Variables assigned (=, op=, ++, --) anywhere in `stmt`, canonical decls, in +// first-seen order. +[[nodiscard]] std::vector collectAssignedVars(const clang::Stmt* stmt); +void appendAssignedVars(std::vector& vars, + const std::vector& extra); + +// Replace each assigned bitvector variable with a fresh unknown and drop +// access-path facts: after this, nothing about their post-loop values is known. +void havocAssignedVars(SymbolicEnv& env, const std::vector& vars); + +// A `break` or `goto` in `body` that leaves the loop (a `break` inside a nested +// loop or switch does not). Such an exit carries state the unroll never +// follows. +[[nodiscard]] bool containsLoopEscape(const clang::Stmt* body); + +// Whether a bounded unroll saw every way out of a loop. +// +// The walkers follow only the path on which the loop guard holds. The state +// they reach after the loop is exact only if no iteration could have exited +// early, the unroll stopped because the guard became infeasible (not because +// loop_unroll ran out), and the body has no escaping break/goto. Otherwise the +// caller must havoc the loop's assigned variables and restore the entry path, +// or a condition after the loop is "proved" from the loop having run exactly +// loop_unroll times. +class LoopUnrollExits { + public: + explicit LoopUnrollExits(const clang::Stmt* body); + + // The guard could not be encoded, or it was not assumed (tracked + // loop-bound assumptions are active): the exits were not modeled. + void guardNotModeled() { exact_ = false; } + + // Record one guard evaluation. Returns false when the loop certainly exits + // here (the guard cannot hold), so the unroll should stop. + bool guard(bool may_continue, bool may_exit); + + // The body walk stopped early (return/abort inside the body). + void bodyStopped() { exact_ = false; } + + // The unroll left the loop along its only exit. + [[nodiscard]] bool exact() const { return exact_ && exited_; } + + private: + bool exact_ = true; + bool exited_ = false; +}; + +} // namespace fold::detect diff --git a/src/detect/always_condition.cpp b/src/detect/always_condition.cpp index 7668cb9..65fdf1c 100644 --- a/src/detect/always_condition.cpp +++ b/src/detect/always_condition.cpp @@ -22,6 +22,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/symbolic/assumption_provenance.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" @@ -87,80 +88,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx) return loc.isValid() && sm.isMacroBodyExpansion(loc); } -bool containsCallExpr(const clang::Stmt* stmt) { - if (!stmt) - return false; - struct Visitor : clang::RecursiveASTVisitor { - bool found = false; - bool VisitCallExpr(clang::CallExpr*) { - found = true; - return false; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.found; -} - -std::vector collectAssignedVars(const clang::Stmt* stmt) { - if (!stmt) - return {}; - struct Visitor : clang::RecursiveASTVisitor { - std::vector vars; - std::unordered_set seen; - - void add(const clang::VarDecl* vd) { - if (!vd) - return; - vd = vd->getCanonicalDecl(); - if (seen.insert(vd).second) - vars.push_back(vd); - } - - bool VisitBinaryOperator(clang::BinaryOperator* op) { - if (!op || !op->isAssignmentOp()) - return true; - const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(lhs)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - - bool VisitUnaryOperator(clang::UnaryOperator* op) { - if (!op || !op->isIncrementDecrementOp()) - return true; - const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(sub)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.vars; -} - -void appendAssignedVars(std::vector& vars, - const std::vector& extra) { - if (vars.empty()) { - vars = extra; - return; - } - std::unordered_set seen(vars.begin(), vars.end()); - for (const auto* vd : extra) { - if (vd && seen.insert(vd).second) - vars.push_back(vd); - } -} - -void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { - for (const clang::VarDecl* vd : vars) { - auto current = env.tryGet(vd); - if (!current || !current->is_bv()) - continue; - env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); - } - env.clearAccessPathFacts(); - env.markLoopHavoc(); -} +using detect::appendAssignedVars; +using detect::collectAssignedVars; +using detect::containsCallExpr; +using detect::havocAssignedVars; class AlwaysConditionWalker { public: @@ -351,43 +282,54 @@ class AlwaysConditionWalker { SymbolicEnv& env) { const bool opaque_loop = containsCallExpr(cond) || containsCallExpr(body) || containsCallExpr(inc); - std::vector assigned; - if (opaque_loop) { - assigned = collectAssignedVars(cond); - appendAssignedVars(assigned, collectAssignedVars(body)); - appendAssignedVars(assigned, collectAssignedVars(inc)); - } + std::vector assigned = collectAssignedVars(cond); + appendAssignedVars(assigned, collectAssignedVars(body)); + appendAssignedVars(assigned, collectAssignedVars(inc)); const z3::expr entry_path = env.currentPath(); + detect::LoopUnrollExits exits(body); for (int iter = 0; iter < budget_.loop_unroll; ++iter) { if (cond) { const EncodingPrecisionContext precision_before = env.tag(); z3::expr guard = encodeCondition(cond, ctx_, env); - if (precisionWorsened(precision_before, env)) + if (precisionWorsened(precision_before, env)) { + exits.guardNotModeled(); break; + } if (env.trackedAssumptions().empty()) { SourcePathAssumeOptions options{ .prune_infeasible = true, .timeout_ms = static_cast(budget_.per_query.count())}; auto assumed = SourcePathState{env}.assume(guard, options); - if (!assumed.truthy.has_value()) + if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value())) break; env = std::move(assumed.truthy->env()); + } else { + exits.guardNotModeled(); } + } else { + exits.guardNotModeled(); } - if (!body) + if (!body) { + exits.bodyStopped(); break; + } { ++loop_depth_; bool ok = walk(body, env); --loop_depth_; - if (!ok) + if (!ok) { + exits.bodyStopped(); break; + } } if (inc) { (void)encodeExpr(inc, ctx_, env); } } - if (opaque_loop) { + // Unless the unroll left the loop along its only exit, the state here + // is "the loop ran some prefix of iterations": keeping it would prove + // post-loop conditions from a trip count the program need not take. + if (opaque_loop || !exits.exact()) { havocAssignedVars(env, assigned); env.restorePath(entry_path); } diff --git a/src/detect/dead_branch.cpp b/src/detect/dead_branch.cpp index e5fe046..7e6c216 100644 --- a/src/detect/dead_branch.cpp +++ b/src/detect/dead_branch.cpp @@ -23,6 +23,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/frontend/stable_identity.hpp" #include "fold/symbolic/assumption_provenance.hpp" #include "fold/symbolic/cfg_helpers.hpp" @@ -198,76 +199,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx) return loc.isValid() && sm.isMacroBodyExpansion(loc); } -bool containsCallExpr(const clang::Stmt* stmt) { - if (!stmt) - return false; - struct Visitor : clang::RecursiveASTVisitor { - bool found = false; - bool VisitCallExpr(clang::CallExpr*) { - found = true; - return false; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.found; -} - -std::vector collectAssignedVars(const clang::Stmt* stmt) { - if (!stmt) - return {}; - struct Visitor : clang::RecursiveASTVisitor { - std::vector vars; - std::unordered_set seen; - - void add(const clang::VarDecl* vd) { - if (!vd) - return; - vd = vd->getCanonicalDecl(); - if (seen.insert(vd).second) - vars.push_back(vd); - } - - bool VisitBinaryOperator(clang::BinaryOperator* op) { - if (!op || !op->isAssignmentOp()) - return true; - const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(lhs)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - - bool VisitUnaryOperator(clang::UnaryOperator* op) { - if (!op || !op->isIncrementDecrementOp()) - return true; - const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(sub)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.vars; -} - -void appendAssignedVars(std::vector& vars, - const std::vector& extra) { - std::unordered_set seen(vars.begin(), vars.end()); - for (const auto* vd : extra) { - if (vd && seen.insert(vd).second) - vars.push_back(vd); - } -} - -void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { - for (const clang::VarDecl* vd : vars) { - auto current = env.tryGet(vd); - if (!current || !current->is_bv()) - continue; - env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); - } - env.clearAccessPathFacts(); - env.markLoopHavoc(); -} +using detect::appendAssignedVars; +using detect::collectAssignedVars; +using detect::containsCallExpr; +using detect::havocAssignedVars; // Recursively walk the body, threading (env, path_predicate). At each IfStmt, // SAT-check each arm before descending. Branch state is forked so an @@ -373,38 +308,52 @@ class BodyWalker { appendAssignedVars(assigned, collectAssignedVars(body)); appendAssignedVars(assigned, collectAssignedVars(inc)); const z3::expr entry_path = path; + detect::LoopUnrollExits exits(body); for (int iter = 0; iter < budget_.loop_unroll; ++iter) { z3::expr body_path = path; if (cond) { const EncodingPrecisionContext precision_before = env.tag(); z3::expr guard = encodeCondition(cond, ctx_, env); - if (precisionWorsened(precision_before, env)) + if (precisionWorsened(precision_before, env)) { + exits.guardNotModeled(); break; + } if (env.trackedAssumptions().empty()) { SourcePathAssumeOptions options{ .prune_infeasible = true, .timeout_ms = static_cast(budget_.per_query.count())}; auto assumed = SourcePathState{env}.withPath(path).assume(guard, options); - if (!assumed.truthy.has_value()) + if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value())) break; env = std::move(assumed.truthy->env()); body_path = env.currentPath(); + } else { + exits.guardNotModeled(); } + } else { + exits.guardNotModeled(); } - if (!body) + if (!body) { + exits.bodyStopped(); break; + } { ++loop_depth_; bool ok = walk(body, env, body_path); --loop_depth_; - if (!ok) + if (!ok) { + exits.bodyStopped(); break; + } } if (inc) { (void)encodeExpr(inc, ctx_, env); } } - if (opaque_loop) { + // Unless the unroll left the loop along its only exit, the state here + // is "the loop ran some prefix of iterations": keeping it would prove + // post-loop conditions from a trip count the program need not take. + if (opaque_loop || !exits.exact()) { havocAssignedVars(env, assigned); path = entry_path; } diff --git a/src/detect/loop_havoc.cpp b/src/detect/loop_havoc.cpp new file mode 100644 index 0000000..31fa7ca --- /dev/null +++ b/src/detect/loop_havoc.cpp @@ -0,0 +1,125 @@ +#include "fold/detect/loop_havoc.hpp" + +#include +#include +#include + +#include + +namespace fold::detect { + +bool containsCallExpr(const clang::Stmt* stmt) { + if (!stmt) + return false; + struct Visitor : clang::RecursiveASTVisitor { + bool found = false; + bool VisitCallExpr(clang::CallExpr*) { + found = true; + return false; + } + } visitor; + visitor.TraverseStmt(const_cast(stmt)); + return visitor.found; +} + +std::vector collectAssignedVars(const clang::Stmt* stmt) { + if (!stmt) + return {}; + struct Visitor : clang::RecursiveASTVisitor { + std::vector vars; + std::unordered_set seen; + + void add(const clang::VarDecl* vd) { + if (!vd) + return; + vd = vd->getCanonicalDecl(); + if (seen.insert(vd).second) + vars.push_back(vd); + } + + bool VisitBinaryOperator(clang::BinaryOperator* op) { + if (!op || !op->isAssignmentOp()) + return true; + const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); + if (const auto* dre = clang::dyn_cast(lhs)) + add(clang::dyn_cast(dre->getDecl())); + return true; + } + + bool VisitUnaryOperator(clang::UnaryOperator* op) { + if (!op || !op->isIncrementDecrementOp()) + return true; + const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); + if (const auto* dre = clang::dyn_cast(sub)) + add(clang::dyn_cast(dre->getDecl())); + return true; + } + } visitor; + visitor.TraverseStmt(const_cast(stmt)); + return visitor.vars; +} + +void appendAssignedVars(std::vector& vars, + const std::vector& extra) { + std::unordered_set seen(vars.begin(), vars.end()); + for (const auto* vd : extra) { + if (vd && seen.insert(vd).second) + vars.push_back(vd); + } +} + +void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { + for (const clang::VarDecl* vd : vars) { + auto current = env.tryGet(vd); + if (!current || !current->is_bv()) + continue; + env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); + } + env.clearAccessPathFacts(); + env.markLoopHavoc(); +} + +namespace { + +// Walks a loop body tracking how many loops/switches enclose each statement, +// so only a break that targets the loop being unrolled counts. +bool escapes(const clang::Stmt* stmt, int breakable_depth) { + if (!stmt) + return false; + if (clang::isa(stmt) || clang::isa(stmt)) + return true; + if (clang::isa(stmt)) + return breakable_depth == 0; + const bool breakable = clang::isa(stmt) || clang::isa(stmt) || + clang::isa(stmt) || + clang::isa(stmt) || + clang::isa(stmt); + for (const clang::Stmt* child : stmt->children()) { + if (escapes(child, breakable_depth + (breakable ? 1 : 0))) + return true; + } + return false; +} + +} // namespace + +bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0); } + +LoopUnrollExits::LoopUnrollExits(const clang::Stmt* body) { + if (containsLoopEscape(body)) + exact_ = false; +} + +bool LoopUnrollExits::guard(bool may_continue, bool may_exit) { + if (!may_continue) { + exited_ = true; + return false; + } + // Both branches feasible: the loop may exit at this iteration, and that + // exit's state is not the one the unroll carries forward. + if (may_exit) + exact_ = false; + return true; +} + +} // namespace fold::detect diff --git a/src/detect/meson.build b/src/detect/meson.build index 5e5701a..cfcb77c 100644 --- a/src/detect/meson.build +++ b/src/detect/meson.build @@ -12,6 +12,7 @@ fold_core_sources += files( 'clone.cpp', 'clone_hash_cache.cpp', 'dead_branch.cpp', + 'loop_havoc.cpp', 'dead_statement.cpp', 'complexity.cpp', 'equiv.cpp', diff --git a/src/detect/unreachable.cpp b/src/detect/unreachable.cpp index 35d3ae4..aad306b 100644 --- a/src/detect/unreachable.cpp +++ b/src/detect/unreachable.cpp @@ -21,6 +21,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" #include "fold/symbolic/loop_bound_pin.hpp" @@ -230,32 +231,52 @@ class UnreachableBodyWalker { bool unrollLoop(const clang::Expr* cond, const clang::Stmt* body, const clang::Expr* inc, SymbolicEnv& env, z3::expr& path) { + std::vector assigned = detect::collectAssignedVars(cond); + detect::appendAssignedVars(assigned, detect::collectAssignedVars(body)); + detect::appendAssignedVars(assigned, detect::collectAssignedVars(inc)); + const z3::expr entry_path = path; + detect::LoopUnrollExits exits(body); for (int iter = 0; iter < budget_.loop_unroll; ++iter) { z3::expr body_path = path; if (cond) { const EncodingPrecisionContext precision_before = env.tag(); z3::expr guard = encodeCondition(cond, ctx_, env); - if (precisionWorsened(precision_before, env)) + if (precisionWorsened(precision_before, env)) { + exits.guardNotModeled(); break; + } if (env.trackedAssumptions().empty()) { SourcePathAssumeOptions options{ .prune_infeasible = true, .timeout_ms = static_cast(budget_.per_query.count())}; auto assumed = SourcePathState{env}.withPath(path).assume(guard, options); - if (!assumed.truthy.has_value()) + if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value())) break; env = std::move(assumed.truthy->env()); body_path = env.currentPath(); + } else { + exits.guardNotModeled(); } + } else { + exits.guardNotModeled(); } - if (!body) + if (!body) { + exits.bodyStopped(); break; - if (!walk(body, env, body_path)) + } + if (!walk(body, env, body_path)) { + exits.bodyStopped(); break; + } if (inc) { (void)encodeExpr(inc, ctx_, env); } } + // The same loop-exit soundness rule as dead-branch / always-condition. + if (!exits.exact()) { + detect::havocAssignedVars(env, assigned); + path = entry_path; + } return true; } diff --git a/tests/unit/meson.build b/tests/unit/meson.build index c50faf8..b0c5903 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -186,6 +186,15 @@ test_always_condition_freestanding = executable( ) test('always_condition_freestanding', test_always_condition_freestanding) +test_loop_exit_soundness = executable( + 'test_loop_exit_soundness', + 'test_loop_exit_soundness.cpp', + dependencies: [fold_core_dep, catch2_dep], + install: false, + build_by_default: false, +) +test('loop_exit_soundness', test_loop_exit_soundness) + test_batch_safety_observer = executable( 'test_batch_safety_observer', 'test_batch_safety_observer.cpp', diff --git a/tests/unit/test_loop_exit_soundness.cpp b/tests/unit/test_loop_exit_soundness.cpp new file mode 100644 index 0000000..c26cd49 --- /dev/null +++ b/tests/unit/test_loop_exit_soundness.cpp @@ -0,0 +1,179 @@ +#include +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/always_condition.hpp" +#include "fold/detect/dead_branch.hpp" +#include "fold/detect/loop_havoc.hpp" +#include "fold/detect/unreachable.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/modeling_options.hpp" + +// Bounded loop unrolling followed only the path on which the loop guard stays +// true. When the guard could also be false (a symbolic bound), that early exit +// was dropped, so the state after the loop was "the loop ran loop_unroll +// times" and conditions on it were reported as Proved dead / always-true or +// always-false. These cases were all Proved before the fix. + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::vector runDead(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectDeadBranchesInContext(unit->getASTContext(), b, s); +} + +std::vector runAlways(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectAlwaysConditionsInContext(unit->getASTContext(), b, s); +} + +std::vector runUnreachable(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectUnreachableCodeInContext(unit->getASTContext(), b, s); +} + +std::size_t proved(const std::vector& findings) { + std::size_t n = 0; + for (const auto& f : findings) + if (f.confidence == fold::Confidence::Proved) + ++n; + return n; +} + +// Symbolic bound: the loop may run zero times, or more than loop_unroll times. +const std::string kSymbolicLoops = + "int a0(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s == 0) return 7; return 0; }\n" + "int a1(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s > 100) return 7; return 0; }\n" + "int a2(unsigned n) { int s = 0; while (n > 0) { s += 1; n--; }" + " if (s == 0) return 7; return 0; }\n" + "int a3(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s > 5) return 1; return 0; }\n"; + +// Constant bound within the unroll budget: the unroll sees the loop's only +// exit, so the post-loop state is exact and a genuinely dead branch stays +// provable. +const std::string kExactLoop = "int e(int x) { int s = 0; for (int i = 0; i < 3; ++i) { s += 1; }" + " if (s == 7) return -1; return s + x; }\n"; + +// Constant bound, but a `break` offers a second way out whose state the +// unroll does not follow. +const std::string kBreakLoop = + "int b(int x) { int s = 0; for (int i = 0; i < 3; ++i) { if (x == i) break; s += 1; }" + " if (s == 0) return -1; return s; }\n"; + +} // namespace + +TEST_CASE("dead: a branch after a symbolic-bound loop is not proven dead", "[dead][loop]") { + CHECK(proved(runDead(kSymbolicLoops)) == 0); +} + +TEST_CASE("always-condition: a condition after a symbolic-bound loop is not proven constant", + "[always][loop]") { + CHECK(proved(runAlways(kSymbolicLoops)) == 0); +} + +TEST_CASE("unreachable: code after a symbolic-bound loop is not proven unreachable", + "[unreachable][loop]") { + CHECK(proved(runUnreachable(kSymbolicLoops)) == 0); +} + +TEST_CASE("dead: a loop the unroll exits exactly keeps its precision", "[dead][loop]") { + // Negative control for the fix: havocking every loop would silence this too. + CHECK(proved(runDead(kExactLoop)) == 1); +} + +TEST_CASE("dead: a break out of a constant loop is an exit the unroll did not follow", + "[dead][loop]") { + CHECK(proved(runDead(kBreakLoop)) == 0); +} + +namespace { + +// The body of the first loop statement in the translation unit. +const clang::Stmt* firstLoopBody(clang::ASTUnit& unit) { + struct Finder : clang::RecursiveASTVisitor { + const clang::Stmt* body = nullptr; + bool VisitForStmt(clang::ForStmt* s) { + if (!body) + body = s->getBody(); + return true; + } + bool VisitWhileStmt(clang::WhileStmt* s) { + if (!body) + body = s->getBody(); + return true; + } + } finder; + finder.TraverseDecl(unit.getASTContext().getTranslationUnitDecl()); + return finder.body; +} + +bool escapesIn(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + const auto* body = firstLoopBody(*unit); + REQUIRE(body); + return fold::detect::containsLoopEscape(body); +} + +} // namespace + +TEST_CASE("loop escape: a break out of the loop escapes; a nested one does not", "[loop_havoc]") { + CHECK(escapesIn("void f(int x){ for(int i=0;i<3;++i){ if(x) break; } }")); + CHECK(escapesIn("void f(int x){ while(x){ goto out; } out:; }")); + CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ for(;;){ break; } } }")); + CHECK_FALSE(escapesIn( + "void f(int x){ for(int i=0;i<3;++i){ switch(x){ case 1: break; default: break; } } }")); + CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ x += i; } }")); +} + +TEST_CASE("loop exits: exact only when the unroll leaves along the only exit", "[loop_havoc]") { + SECTION("guard falsified after iterations that could not exit") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(/*may_continue=*/true, /*may_exit=*/false)); + CHECK_FALSE(exits.guard(/*may_continue=*/false, /*may_exit=*/true)); + CHECK(exits.exact()); + } + SECTION("an iteration that could also exit makes the state inexact") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(true, true)); + CHECK_FALSE(exits.guard(false, true)); + CHECK_FALSE(exits.exact()); + } + SECTION("the unroll budget running out is not an exit") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(true, false)); + CHECK_FALSE(exits.exact()); + } + SECTION("an unmodeled guard or a stopped body is never exact") { + fold::detect::LoopUnrollExits unmodeled(nullptr); + unmodeled.guardNotModeled(); + CHECK_FALSE(unmodeled.guard(false, true)); + CHECK_FALSE(unmodeled.exact()); + fold::detect::LoopUnrollExits stopped(nullptr); + stopped.bodyStopped(); + CHECK_FALSE(stopped.guard(false, true)); + CHECK_FALSE(stopped.exact()); + } +} -- 2.52.0 From 67483ee6b0edb4a35a54f88781d5f3979f70f3ad Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:14:50 -0600 Subject: [PATCH 03/18] fix(model): apply libc models only to C library callees 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. --- include/fold/detect/taint_track.hpp | 4 + .../fold/symbolic/encoder_callee_names.hpp | 9 ++ src/detect/taint_track.cpp | 73 ++++++----- src/detect/use_after_free.cpp | 11 +- src/symbolic/encoder_callee_names.cpp | 12 ++ src/symbolic/encoder_expr_arms.cpp | 7 +- tests/unit/meson.build | 9 ++ tests/unit/test_encoder_callee_names.cpp | 27 ++++ tests/unit/test_library_callee_identity.cpp | 117 ++++++++++++++++++ 9 files changed, 231 insertions(+), 38 deletions(-) create mode 100644 tests/unit/test_library_callee_identity.cpp diff --git a/include/fold/detect/taint_track.hpp b/include/fold/detect/taint_track.hpp index 71dec90..79b1a89 100644 --- a/include/fold/detect/taint_track.hpp +++ b/include/fold/detect/taint_track.hpp @@ -30,6 +30,9 @@ struct TaintSource { std::string func; int param = 0; // -1 = return value std::string description = "tainted data"; + // A C library / POSIX function: matches only a callee that is one + // (isCLibraryCallee). False for method-name heuristics such as `get`. + bool c_api = true; }; struct TaintSink { @@ -37,6 +40,7 @@ struct TaintSink { int param = 0; std::string description = "dangerous sink"; unsigned domain = taint_domain::kAny; // which sanitizer domain neutralises it + bool c_api = true; // see TaintSource::c_api }; class TaintTracker : public SafetyObserver { diff --git a/include/fold/symbolic/encoder_callee_names.hpp b/include/fold/symbolic/encoder_callee_names.hpp index 53afa3f..266224a 100644 --- a/include/fold/symbolic/encoder_callee_names.hpp +++ b/include/fold/symbolic/encoder_callee_names.hpp @@ -29,4 +29,13 @@ namespace fold { [[nodiscard]] std::string qualifiedCalleeName(const clang::CallExpr* ce); +// True when `fd` can be the C library function its name suggests: not a class +// member, and declared at global scope, in namespace std, or extern "C". +// Library models (malloc/free, taint sources and sinks) must check this; the +// bare identifier alone also matches `mine::free` or `Pool::free`. +[[nodiscard]] bool isCLibraryFunction(const clang::FunctionDecl* fd); + +// isCLibraryFunction of a call's direct callee; false for indirect calls. +[[nodiscard]] bool isCLibraryCallee(const clang::CallExpr* ce); + } // namespace fold diff --git a/src/detect/taint_track.cpp b/src/detect/taint_track.cpp index 6ec5c6a..69aa3dd 100644 --- a/src/detect/taint_track.cpp +++ b/src/detect/taint_track.cpp @@ -20,45 +20,47 @@ #include "fold/detect/model_validation.hpp" #include "fold/detect/security_walker.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" namespace fold::detect { namespace { -const std::vector kSources = {{"scanf", 1, "untrusted input"}, - {"fscanf", 2, "untrusted input"}, - {"sscanf", 2, "untrusted input"}, - {"recv", 1, "network input"}, - {"recvfrom", 1, "network input"}, - {"read", 1, "file/socket input"}, - {"fread", 0, "file input"}, - {"fgets", 0, "file input"}, - {"gets", 0, "file input"}, - {"getc", -1, "file input"}, - {"getchar", -1, "stdin input"}, - {"getenv", -1, "environment variable"}, - {"socket", -1, "network handle"}, - {"accept", -1, "network handle"}, - {"curl_easy_perform", -1, "network response"}, - {"curl_easy_getinfo", 2, "network metadata"}, - {"queryParam", -1, "URL query parameter"}, - {"get_query_param", -1, "URL query parameter"}, - {"get_form_param", -1, "Form data parameter"}, - {"read_header", -1, "HTTP header"}, - {"Query", -1, "Database query result"}, - {"get", -1, "Map/Request lookup"}, - {"readString", -1, "deserialized string"}, - {"readStringVector", -1, "deserialized string list"}, - {"readStringMap", -1, "deserialized string map"}, - {"readStringArray", 2, "deserialized string array"}, - {"fromJson", -1, "JSON deserialization source"}}; +const std::vector kSources = { + {"scanf", 1, "untrusted input"}, + {"fscanf", 2, "untrusted input"}, + {"sscanf", 2, "untrusted input"}, + {"recv", 1, "network input"}, + {"recvfrom", 1, "network input"}, + {"read", 1, "file/socket input"}, + {"fread", 0, "file input"}, + {"fgets", 0, "file input"}, + {"gets", 0, "file input"}, + {"getc", -1, "file input"}, + {"getchar", -1, "stdin input"}, + {"getenv", -1, "environment variable"}, + {"socket", -1, "network handle"}, + {"accept", -1, "network handle"}, + {"curl_easy_perform", -1, "network response"}, + {"curl_easy_getinfo", 2, "network metadata"}, + {"queryParam", -1, "URL query parameter", false}, + {"get_query_param", -1, "URL query parameter", false}, + {"get_form_param", -1, "Form data parameter", false}, + {"read_header", -1, "HTTP header", false}, + {"Query", -1, "Database query result", false}, + {"get", -1, "Map/Request lookup", false}, + {"readString", -1, "deserialized string", false}, + {"readStringVector", -1, "deserialized string list", false}, + {"readStringMap", -1, "deserialized string map", false}, + {"readStringArray", 2, "deserialized string array", false}, + {"fromJson", -1, "JSON deserialization source", false}}; const std::vector kSinks = { {"sqlite3_prepare_v2", 1, "SQL injection", taint_domain::kSql}, {"sqlite3_prepare_v3", 1, "SQL injection", taint_domain::kSql}, {"PQexecParams", 1, "SQL injection", taint_domain::kSql}, - {"execute", -1, "database execution", taint_domain::kSql}, - {"query", -1, "database query", taint_domain::kSql}, + {"execute", -1, "database execution", taint_domain::kSql, false}, + {"query", -1, "database query", taint_domain::kSql, false}, {"send", -1, "network transmission", taint_domain::kNetwork}, {"write", -1, "file/socket write", taint_domain::kNetwork}, {"open", 0, "path access", taint_domain::kPath}, @@ -218,8 +220,11 @@ std::string canonicalSinkName(const std::string& callee_name) { return isExecFamilySink(callee_name) ? "exec" : callee_name; } -bool sinkMatches(const TaintSink& entry, const std::string& callee_name) { - return entry.func == callee_name; +// A libc/POSIX entry matches only the C library function itself: a method or +// namespaced function that shares the name (`Shell::system`) is not the sink. +bool sinkMatches(const TaintSink& entry, const std::string& callee_name, + const clang::CallExpr* call) { + return entry.func == callee_name && (!entry.c_api || isCLibraryCallee(call)); } } // namespace @@ -276,7 +281,7 @@ void TaintTracker::onBinaryArith(BinOp op, const z3::expr& lhs, const z3::expr& bool TaintTracker::isSourceCall(const clang::CallExpr* call, const std::string& callee_name, TaintSource& source) const { for (const auto& entry : kSources) { - if (entry.func == callee_name) { + if (entry.func == callee_name && (!entry.c_api || isCLibraryCallee(call))) { if (callee_name == "get" && call) { if (const auto* callee = call->getDirectCallee()) { if (callee->isInStdNamespace()) { @@ -300,7 +305,7 @@ bool TaintTracker::isSourceCall(const clang::CallExpr* call, const std::string& bool TaintTracker::isSinkCall(const std::string& callee_name, TaintSink& sink) const { for (const auto& entry : kSinks) { - if (sinkMatches(entry, callee_name)) { + if (entry.func == callee_name) { sink = entry; return true; } @@ -675,7 +680,7 @@ void TaintTracker::onCallExpr(const fold::ir::Call& call_ir, bool matched_sink = false; for (const auto& sink : kSinks) { - if (!sinkMatches(sink, callee_name)) + if (!sinkMatches(sink, callee_name, call)) continue; matched_sink = true; bool tainted = false; diff --git a/src/detect/use_after_free.cpp b/src/detect/use_after_free.cpp index 6ed43df..c93270a 100644 --- a/src/detect/use_after_free.cpp +++ b/src/detect/use_after_free.cpp @@ -23,6 +23,7 @@ #include "fold/detect/security_walker.hpp" #include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/heap_model.hpp" #include "fold/symbolic/safety_observer.hpp" #include "fold/symbolic/tactics.hpp" @@ -121,6 +122,12 @@ std::string calleeName(const clang::CallExpr* call) { return callee != nullptr ? callee->getNameAsString() : std::string{}; } +// The allocator functions this detector models, by resolved declaration: a +// project `mine::free` or `Pool::free` is not libc free. +std::string libraryCalleeName(const clang::CallExpr* call) { + return isCLibraryCallee(call) ? calleeName(call) : std::string{}; +} + class Analyzer { public: Analyzer(const clang::ASTContext& ctx, std::vector& out) : ctx_(ctx), out_(out) {} @@ -275,14 +282,14 @@ class Analyzer { bool isSameVarRealloc(const clang::VarDecl* lhs, const clang::Expr* rhs) const { const auto* call = clang::dyn_cast_or_null(ignore(rhs)); - if (lhs == nullptr || call == nullptr || calleeName(call) != "realloc" || + if (lhs == nullptr || call == nullptr || libraryCalleeName(call) != "realloc" || call->getNumArgs() == 0) return false; return varFromExpr(call->getArg(0)) == lhs; } bool handleFreeLikeCall(const clang::CallExpr* call, State& state) { - if (calleeName(call) == "free" && call->getNumArgs() == 1) { + if (libraryCalleeName(call) == "free" && call->getNumArgs() == 1) { poisonVar(state, varFromExpr(call->getArg(0))); return true; } diff --git a/src/symbolic/encoder_callee_names.cpp b/src/symbolic/encoder_callee_names.cpp index 0e795a0..7be3fb1 100644 --- a/src/symbolic/encoder_callee_names.cpp +++ b/src/symbolic/encoder_callee_names.cpp @@ -61,6 +61,18 @@ std::string qualifiedFunctionName(const clang::FunctionDecl* fd) { return name; } +bool isCLibraryFunction(const clang::FunctionDecl* fd) { + if (fd == nullptr || clang::isa(fd)) + return false; + if (fd->isExternC() || fd->isInStdNamespace()) + return true; + return fd->getDeclContext()->getRedeclContext()->isTranslationUnit(); +} + +bool isCLibraryCallee(const clang::CallExpr* ce) { + return ce != nullptr && isCLibraryFunction(ce->getDirectCallee()); +} + std::string qualifiedCalleeName(const clang::CallExpr* ce) { if (ce == nullptr) return {}; diff --git a/src/symbolic/encoder_expr_arms.cpp b/src/symbolic/encoder_expr_arms.cpp index d7a91fd..6d9a104 100644 --- a/src/symbolic/encoder_expr_arms.cpp +++ b/src/symbolic/encoder_expr_arms.cpp @@ -575,7 +575,10 @@ z3::expr encodeCallExprArm(const clang::CallExpr* ce, const clang::ASTContext& c } return returnCallValue(name, env.ctx().bv_val(0, kBitvecWidth), false); } - if (isMallocLikeCall(name)) { + // Heap models apply only to the C library functions, not to a project + // function or method that shares the name (`mine::free`, `Pool::free`). + const bool c_library_callee = isCLibraryCallee(ce); + if (c_library_callee && isMallocLikeCall(name)) { z3::expr size = env.ctx().bv_val(0, kBitvecWidth); bool is_stack = (name == "alloca" || name == "_alloca" || name == "__builtin_alloca"); if (name == "malloc" && ce->getNumArgs() >= 1) { @@ -606,7 +609,7 @@ z3::expr encodeCallExprArm(const clang::CallExpr* ce, const clang::ASTContext& c } return returnCallValue(name, ptr); } - if (isFreeCall(name) && ce->getNumArgs() >= 1) { + if (c_library_callee && isFreeCall(name) && ce->getNumArgs() >= 1) { z3::expr ptr = coerceToBv(env, arg_values[0]); bool known_region = env.heapModel().isTrackedPointer(ptr); bool already_freed = env.heapModel().isFreed(ptr); diff --git a/tests/unit/meson.build b/tests/unit/meson.build index b0c5903..60a65b5 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -195,6 +195,15 @@ test_loop_exit_soundness = executable( ) test('loop_exit_soundness', test_loop_exit_soundness) +test_library_callee_identity = executable( + 'test_library_callee_identity', + 'test_library_callee_identity.cpp', + dependencies: [fold_core_dep, catch2_dep], + install: false, + build_by_default: false, +) +test('library_callee_identity', test_library_callee_identity) + test_batch_safety_observer = executable( 'test_batch_safety_observer', 'test_batch_safety_observer.cpp', diff --git a/tests/unit/test_encoder_callee_names.cpp b/tests/unit/test_encoder_callee_names.cpp index 9cee950..5b0608c 100644 --- a/tests/unit/test_encoder_callee_names.cpp +++ b/tests/unit/test_encoder_callee_names.cpp @@ -153,3 +153,30 @@ TEST_CASE("qualifiedCalleeName resolves through a direct CallExpr", TEST_CASE("qualifiedCalleeName returns empty for null", "[encoder][callee_names][qualified]") { REQUIRE(fold::qualifiedCalleeName(nullptr).empty()); } + +TEST_CASE("isCLibraryCallee: only C library functions, never members or namespaced lookalikes", + "[encoder-callee-names][library]") { + auto unit = parse("extern \"C\" void free(void*);\n" + "namespace std { using ::free; }\n" + "namespace mine { void free(void*) {} }\n" + "struct Pool { void free(void*) {} };\n" + "void global_helper(void*) {}\n" + "void f(void* p, Pool& pool, void (*fp)(void*)) {\n" + " free(p);\n" + " std::free(p);\n" + " mine::free(p);\n" + " pool.free(p);\n" + " global_helper(p);\n" + " fp(p);\n" + "}\n"); + REQUIRE(unit); + const auto calls = collectCalls(*unit, "f"); + REQUIRE(calls.size() == 6); + CHECK(fold::isCLibraryCallee(calls[0])); // ::free (extern "C") + CHECK(fold::isCLibraryCallee(calls[1])); // std::free resolves to ::free + CHECK_FALSE(fold::isCLibraryCallee(calls[2])); // mine::free + CHECK_FALSE(fold::isCLibraryCallee(calls[3])); // Pool::free + CHECK(fold::isCLibraryCallee(calls[4])); // global scope: C semantics + CHECK_FALSE(fold::isCLibraryCallee(calls[5])); // indirect call + CHECK_FALSE(fold::isCLibraryCallee(nullptr)); +} diff --git a/tests/unit/test_library_callee_identity.cpp b/tests/unit/test_library_callee_identity.cpp new file mode 100644 index 0000000..1f65688 --- /dev/null +++ b/tests/unit/test_library_callee_identity.cpp @@ -0,0 +1,117 @@ +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/cross_tu_cache.hpp" +#include "fold/detect/double_free.hpp" +#include "fold/detect/taint_track.hpp" +#include "fold/detect/use_after_free.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" + +// Library models (malloc/free, taint sources and sinks) were selected by the +// callee's bare identifier, so a project function that merely shares a libc +// name was modeled as libc: `mine::free(p)` followed by `free(p)` was a Proved +// double-free. Models now require the resolved declaration to be a C library +// function (global scope, namespace std, or extern "C"; never a member). + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::size_t countKind(const std::vector& findings, fold::FindingKind kind) { + std::size_t n = 0; + for (const auto& f : findings) + if (f.kind == kind) + ++n; + return n; +} + +std::vector runDoubleFree(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectDoubleFreeInContext(unit->getASTContext(), b, s); +} + +std::vector runUseAfterFree(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + return fold::detectUseAfterFreeInContext(unit->getASTContext()); +} + +std::vector runTaint(const std::string& code) { + fold::detect::CrossTUCache::instance().clear(); + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectTaintTrackInContext(unit->getASTContext(), b, s); +} + +const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n" + "extern \"C\" void free(void*);\n"; + +} // namespace + +TEST_CASE("heap model: a namespaced function named free is not libc free", + "[library-callee][double-free]") { + const std::string code = kLibc + "namespace mine { inline void free(void*) {} }\n" + "int f() {\n" + " int* p = static_cast(malloc(sizeof(int)));\n" + " if (!p) return 0;\n" + " *p = 1;\n" + " mine::free(p);\n" + " int v = *p;\n" + " free(p);\n" + " return v;\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); + CHECK(countKind(runUseAfterFree(code), fold::FindingKind::UseAfterFree) == 0); +} + +TEST_CASE("heap model: a member function named free is not libc free", + "[library-callee][double-free]") { + const std::string code = kLibc + "struct Pool { void free(void*) {} };\n" + "void f(Pool& pool) {\n" + " void* p = malloc(8);\n" + " if (!p) return;\n" + " pool.free(p);\n" + " free(p);\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); +} + +TEST_CASE("heap model: libc free twice is still a double free", "[library-callee][double-free]") { + // Negative control: the fix must not drop the real model. + const std::string code = kLibc + "void f() {\n" + " void* p = malloc(8);\n" + " if (!p) return;\n" + " free(p);\n" + " free(p);\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 1); +} + +TEST_CASE("taint: a member function named system is not a command sink", + "[library-callee][taint]") { + const std::string code = "extern \"C\" char* getenv(const char*);\n" + "struct Shell { int system(const char*) { return 0; } };\n" + "int f(Shell& sh) { return sh.system(getenv(\"CMD\")); }\n"; + CHECK(countKind(runTaint(code), fold::FindingKind::TaintTrack) == 0); +} + +TEST_CASE("taint: libc system with tainted input is still a sink", "[library-callee][taint]") { + const std::string code = "extern \"C\" char* getenv(const char*);\n" + "extern \"C\" int system(const char*);\n" + "int f() { return system(getenv(\"CMD\")); }\n"; + CHECK(countKind(runTaint(code), fold::FindingKind::TaintTrack) == 1); +} -- 2.52.0 From 0556cc638db34d112f9afaddd6315aff761742ee Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:27:26 -0600 Subject: [PATCH 04/18] fix(report): keep Proved for exact bounded models only 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. --- .../fold/symbolic/encoder_type_queries.hpp | 9 + src/detect/dead_statement.cpp | 3 +- src/detect/double_free.cpp | 5 +- src/detect/oob_access.cpp | 45 +++-- src/detect/static_ptr_asymmetry.cpp | 4 +- src/detect/unused_function.cpp | 3 +- src/detect/use_after_free.cpp | 27 +-- src/symbolic/encoder_expr.cpp | 6 + src/symbolic/encoder_type_queries.cpp | 16 ++ tests/unit/meson.build | 9 + .../unit/test_proved_requires_exact_model.cpp | 163 ++++++++++++++++++ 11 files changed, 260 insertions(+), 30 deletions(-) create mode 100644 tests/unit/test_proved_requires_exact_model.cpp diff --git a/include/fold/symbolic/encoder_type_queries.hpp b/include/fold/symbolic/encoder_type_queries.hpp index 3f1f53c..e7de74a 100644 --- a/include/fold/symbolic/encoder_type_queries.hpp +++ b/include/fold/symbolic/encoder_type_queries.hpp @@ -3,10 +3,12 @@ #include #include +#include namespace clang { class ASTContext; class QualType; +class UnaryExprOrTypeTraitExpr; } // namespace clang namespace fold { @@ -45,4 +47,11 @@ namespace fold::symbolic { [[nodiscard]] z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx, const clang::QualType& qt); +// The exact value of `sizeof` / `alignof` (and the other type traits) when +// the compiler folds it to a constant: complete, non-dependent, non-VLA +// operands. nullopt otherwise; the encoder then treats the node as +// unsupported rather than guess a size. +[[nodiscard]] std::optional +typeTraitConstant(const clang::ASTContext& ctx, const clang::UnaryExprOrTypeTraitExpr* expr); + } // namespace fold::symbolic diff --git a/src/detect/dead_statement.cpp b/src/detect/dead_statement.cpp index c786e5e..6ae51ab 100644 --- a/src/detect/dead_statement.cpp +++ b/src/detect/dead_statement.cpp @@ -204,7 +204,8 @@ class DeadStatementVisitor : public clang::RecursiveASTVisitor4). if (heap_access->alloc_id != 0) - checkHeapBounds(*heap_access, path, loc); + checkHeapBounds(*heap_access, path, loc, env); } void onFree(const z3::expr& /*ptr*/, const ir::Expr& /*ptrExpr*/, const z3::expr& /*path*/, const ir::SourceLoc& loc, bool known_region, bool was_already_freed) override { + // No query backs this: it is the heap model's freed flag, so it cannot + // be Proved (docs/research/soundness.md). if (known_region && was_already_freed) { - emitUseAfterFree(loc, nullptr, "Double free on tracked heap region"); + emitUseAfterFree(loc, nullptr, "Double free on tracked heap region", + /*exact_model=*/false); } } @@ -436,22 +439,29 @@ class OOBObserver : public SafetyObserver { } private: + // Proved needs an exact bounded model (docs/research/soundness.md): a SAT + // result from an over-approximated encoding may be spurious. + static bool exactEncoding(const SymbolicEnv* env) { + return env != nullptr && !env->tag().isImprecise(); + } + void checkHeapBounds(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path, - const ir::SourceLoc& loc) { + const ir::SourceLoc& loc, const SymbolicEnv* env) { z3::expr end = heap_access.offset + heap_access.width; z3::expr hazard = (heap_access.ptr != heap_access.ptr.ctx().bv_val(0, 64)) && !heap_access.is_use_after_free && z3::ugt(end, heap_access.region_size); if (checkHazard(path, hazard, loc, "oob-access-heap") == z3::sat) { - emitHeap(heap_access, loc); + emitHeap(heap_access, loc, exactEncoding(env)); } } void checkUseAfterFree(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path, - const ir::SourceLoc& loc) { + const ir::SourceLoc& loc, const SymbolicEnv* env) { if (checkHazard(path, heap_access.is_use_after_free, loc, "uaf-access") == z3::sat) { emitUseAfterFree(loc, &heap_access, "Use-after-free on heap buffer from " + - describeAllocationSite(heap_access.site)); + describeAllocationSite(heap_access.site), + exactEncoding(env)); } } @@ -652,8 +662,10 @@ class OOBObserver : public SafetyObserver { Finding f; f.kind = FindingKind::OOBAccess; const auto size_value = numeralU64(size_expr); + // The copy hook carries no encoding precision, so even a constant size + // over a constant capacity is not an exact bounded model of the path. + f.confidence = Confidence::Heuristic; const bool is_const = size_value.has_value(); - f.confidence = is_const ? Confidence::Proved : Confidence::Heuristic; Location l = locationFromSloc(loc); f.locations.push_back(std::move(l)); f.id = std::string("oob-access:") + f.locations.front().file + ":" + @@ -835,11 +847,12 @@ class OOBObserver : public SafetyObserver { out_.push_back(std::move(f)); } - void emitHeap(const symbolic::HeapAccessInfo& heap_access, const ir::SourceLoc& loc) { + void emitHeap(const symbolic::HeapAccessInfo& heap_access, const ir::SourceLoc& loc, + bool exact_model) { Finding f; f.kind = FindingKind::OOBAccess; - f.confidence = - heap_access.region_size.is_numeral() ? Confidence::Proved : Confidence::Heuristic; + f.confidence = heap_access.region_size.is_numeral() && exact_model ? Confidence::Proved + : Confidence::Heuristic; Location l = locationFromSloc(loc); f.locations.push_back(std::move(l)); if (!heap_access.site.file.empty()) { @@ -864,10 +877,10 @@ class OOBObserver : public SafetyObserver { } void emitUseAfterFree(const ir::SourceLoc& loc, const symbolic::HeapAccessInfo* heap_access, - const std::string& message) { + const std::string& message, bool exact_model) { Finding f; f.kind = FindingKind::OOBAccess; - f.confidence = Confidence::Proved; + f.confidence = exact_model ? Confidence::Proved : Confidence::Heuristic; Location l = locationFromSloc(loc); f.locations.push_back(std::move(l)); if (heap_access && !heap_access->site.file.empty()) { diff --git a/src/detect/static_ptr_asymmetry.cpp b/src/detect/static_ptr_asymmetry.cpp index eaefebe..789aa2f 100644 --- a/src/detect/static_ptr_asymmetry.cpp +++ b/src/detect/static_ptr_asymmetry.cpp @@ -319,7 +319,9 @@ std::vector detectStaticPtrAsymmetryInContext(clang::ASTContext& ctx) { Finding f; f.kind = FindingKind::NullDeref; - f.confidence = Confidence::Proved; + // A cross-function discipline pattern, not a solver result: the + // unchecked function may be unreachable while the pointer is null. + f.confidence = Confidence::Heuristic; f.locations.push_back(locOf(ctx, loc, fd->getQualifiedNameAsString())); f.id = std::string("static-ptr-asymmetry:") + f.locations.front().file + ":" + std::to_string(f.locations.front().line) + ":" + diff --git a/src/detect/unused_function.cpp b/src/detect/unused_function.cpp index 940f819..b07c544 100644 --- a/src/detect/unused_function.cpp +++ b/src/detect/unused_function.cpp @@ -219,7 +219,8 @@ std::vector detectUnusedFunctionsInContext(clang::ASTContext& ctx) { Finding f; f.kind = FindingKind::UnusedFunction; - f.confidence = Confidence::Proved; + // A call-graph fact read off the AST, not a solver result. + f.confidence = Confidence::Syntactic; f.locations.push_back(locOf(fd, ctx)); f.id = stableQualityFindingId("unused-function", stableFunctionId(fd)); f.message = "Static function `" + fd->getNameAsString() + diff --git a/src/detect/use_after_free.cpp b/src/detect/use_after_free.cpp index c93270a..41d20d8 100644 --- a/src/detect/use_after_free.cpp +++ b/src/detect/use_after_free.cpp @@ -23,6 +23,7 @@ #include "fold/detect/security_walker.hpp" #include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder.hpp" #include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/heap_model.hpp" #include "fold/symbolic/safety_observer.hpp" @@ -415,33 +416,35 @@ class UseAfterFreeObserver : public SafetyObserver { const clang::VarDecl* /*var*/, const ir::SourceLoc& loc, const ::fold::symbolic::HeapAccessInfo* heap_access, const ::fold::DefUseContext* /*def_use*/, - const ::fold::SymbolicEnv* /*env*/) override { + const ::fold::SymbolicEnv* env) override { if (!heap_access) return; - checkUseAfterFree(*heap_access, path, loc); + checkUseAfterFree(*heap_access, path, loc, env); } void onArraySubscript(const z3::expr& /*idx*/, int /*known_len*/, const z3::expr& path, const ir::SourceLoc& loc, const ::fold::symbolic::HeapAccessInfo* heap_access, - const ::fold::DefUseContext* /*def_use*/, - const ::fold::SymbolicEnv* /*env*/, const clang::Expr* /*idx_expr*/, + const ::fold::DefUseContext* /*def_use*/, const ::fold::SymbolicEnv* env, + const clang::Expr* /*idx_expr*/, const clang::VarDecl* /*base_var*/) override { if (!heap_access) return; - checkUseAfterFree(*heap_access, path, loc); + checkUseAfterFree(*heap_access, path, loc, env); } void onFree(const z3::expr& /*ptr*/, const ir::Expr& /*ptrExpr*/, const z3::expr& /*path*/, const ir::SourceLoc& loc, bool known_region, bool was_already_freed) override { + // The heap model's freed flag, with no query behind it: not Proved. if (known_region && was_already_freed) { - emitUseAfterFree(loc, nullptr, "Double free on tracked heap region"); + emitUseAfterFree(loc, nullptr, "Double free on tracked heap region", + /*exact_model=*/false); } } private: void checkUseAfterFree(const symbolic::HeapAccessInfo& heap_access, const z3::expr& path, - const ir::SourceLoc& loc) { + const ir::SourceLoc& loc, const SymbolicEnv* env) { z3::context& c = const_cast(heap_access.is_use_after_free.ctx()); z3::expr hazard = heap_access.is_use_after_free; @@ -451,7 +454,11 @@ class UseAfterFreeObserver : public SafetyObserver { z3::check_result result = checkHazard(path, hazard, loc, "use-after-free"); if (result == z3::sat) { std::string alloc_desc = describeAllocationSite(heap_access.site); - emitUseAfterFree(loc, &heap_access, "Use-after-free on heap buffer from " + alloc_desc); + // Proved needs an exact bounded model: a SAT result from an + // over-approximated encoding may be spurious (soundness.md). + const bool exact = env != nullptr && !env->tag().isImprecise(); + emitUseAfterFree(loc, &heap_access, "Use-after-free on heap buffer from " + alloc_desc, + exact); } } @@ -512,10 +519,10 @@ class UseAfterFreeObserver : public SafetyObserver { } void emitUseAfterFree(const ir::SourceLoc& loc, const symbolic::HeapAccessInfo* heap_access, - const std::string& message) { + const std::string& message, bool exact_model) { Finding f; f.kind = FindingKind::UseAfterFree; - f.confidence = Confidence::Proved; + f.confidence = exact_model ? Confidence::Proved : Confidence::Heuristic; f.locations.push_back(locationFromSloc(loc)); if (heap_access && !heap_access->site.file.empty()) { Location alloc_loc; diff --git a/src/symbolic/encoder_expr.cpp b/src/symbolic/encoder_expr.cpp index 06b3b7c..ce2cb40 100644 --- a/src/symbolic/encoder_expr.cpp +++ b/src/symbolic/encoder_expr.cpp @@ -611,6 +611,12 @@ z3::expr encodeExpr(ir::Expr expr_ir, const clang::ASTContext& ctx, SymbolicEnv& // is now empty — any unmigrated AST kind falls through to the // unsupported-node bail at the function end. + if (const auto* trait = dyn_cast(e)) { + if (auto value = symbolic::typeTraitConstant(ctx, trait)) + return markEncoded("UnaryExprOrTypeTraitExpr", + env.ctx().bv_val(static_cast(*value), kBitvecWidth)); + } + recordBailedNode(expr->getStmtClassName(), std::string("expr kind ") + expr->getStmtClassName()); recordPrecision(env, EncodingPrecision::UnsupportedNode, diff --git a/src/symbolic/encoder_type_queries.cpp b/src/symbolic/encoder_type_queries.cpp index 4072115..e948745 100644 --- a/src/symbolic/encoder_type_queries.cpp +++ b/src/symbolic/encoder_type_queries.cpp @@ -1,6 +1,7 @@ #include "fold/symbolic/encoder_type_queries.hpp" #include +#include #include #include "fold/symbolic/encoder.hpp" @@ -46,4 +47,19 @@ z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx, const cla return env.ctx().bv_val(typeSizeBytes(ctx, qt), kBitvecWidth); } +std::optional typeTraitConstant(const clang::ASTContext& ctx, + const clang::UnaryExprOrTypeTraitExpr* expr) { + if (expr == nullptr || expr->isValueDependent() || expr->isTypeDependent()) + return std::nullopt; + clang::Expr::EvalResult result; + if (!expr->EvaluateAsInt(result, ctx) || !result.Val.isInt()) + return std::nullopt; + const llvm::APSInt& value = result.Val.getInt(); + if (value.isSigned() && value.isNegative()) + return std::nullopt; + if (value.getActiveBits() > 64) + return std::nullopt; + return value.getZExtValue(); +} + } // namespace fold::symbolic diff --git a/tests/unit/meson.build b/tests/unit/meson.build index 60a65b5..fbbd4c5 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -204,6 +204,15 @@ test_library_callee_identity = executable( ) test('library_callee_identity', test_library_callee_identity) +test_proved_requires_exact_model = executable( + 'test_proved_requires_exact_model', + 'test_proved_requires_exact_model.cpp', + dependencies: [fold_core_dep, catch2_dep], + install: false, + build_by_default: false, +) +test('proved_requires_exact_model', test_proved_requires_exact_model) + test_batch_safety_observer = executable( 'test_batch_safety_observer', 'test_batch_safety_observer.cpp', diff --git a/tests/unit/test_proved_requires_exact_model.cpp b/tests/unit/test_proved_requires_exact_model.cpp new file mode 100644 index 0000000..54cefc3 --- /dev/null +++ b/tests/unit/test_proved_requires_exact_model.cpp @@ -0,0 +1,163 @@ +#include +#include +#include + +#include +#include +#include +#include +#include + +#include "fold/detect/dead_statement.hpp" +#include "fold/detect/double_free.hpp" +#include "fold/detect/oob_access.hpp" +#include "fold/detect/static_ptr_asymmetry.hpp" +#include "fold/detect/unused_function.hpp" +#include "fold/detect/use_after_free.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_type_queries.hpp" + +// docs/research/soundness.md: `proved` means an exact bounded model +// established the property. These detectors assigned Proved without one: +// from a heap-model flag (double-free), a cross-function pattern +// (static-ptr-asymmetry), an AST fact (unused-function, dead-statement), or a +// SAT result whose encoding precision was never checked (stdlib OOB copy, +// use-after-free under an unknown call). + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::optional confidenceOf(const std::vector& findings, + fold::FindingKind kind) { + for (const auto& f : findings) + if (f.kind == kind) + return f.confidence; + return std::nullopt; +} + +const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n" + "extern \"C\" void free(void*);\n" + "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"; + +} // namespace + +TEST_CASE("double-free without a solver query is Heuristic", "[proved-contract][double-free]") { + auto unit = + parse(kLibc + "void f() { void* p = malloc(8); if (!p) return; free(p); free(p); }"); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto c = confidenceOf(fold::detectDoubleFreeInContext(unit->getASTContext(), b, s), + fold::FindingKind::DoubleFree); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("static-ptr-asymmetry is a pattern, not a proof", "[proved-contract][static-ptr]") { + auto unit = parse("struct S { int v; };\n" + "static S* g_state = nullptr;\n" + "int checked() { if (!g_state) return 0; return g_state->v; }\n" + "int unchecked() { return g_state->v; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectStaticPtrAsymmetryInContext(unit->getASTContext()), + fold::FindingKind::NullDeref); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("unused static function is an AST fact: Syntactic", "[proved-contract][unused]") { + auto unit = parse("static int helper(int x) { return x + 1; }\nint api(int x) { return x; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectUnusedFunctionsInContext(unit->getASTContext()), + fold::FindingKind::UnusedFunction); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Syntactic); +} + +TEST_CASE("statement after return is an AST fact: Syntactic", "[proved-contract][dead-stmt]") { + auto unit = parse("int f(int x) { return x; x += 1; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectDeadStatementsInContext(unit->getASTContext()), + fold::FindingKind::DeadStatement); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Syntactic); +} + +TEST_CASE("stdlib copy overflow without encoding precision is Heuristic", + "[proved-contract][oob]") { + auto unit = parse(kLibc + "void f(const char* src) { char buf[8]; memcpy(buf, src, 16); }"); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto c = confidenceOf(fold::detectOOBAccessInContext(unit->getASTContext(), b, s), + fold::FindingKind::OOBAccess); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("heap use-after-free keeps Proved only on an exact encoding", "[proved-contract][uaf]") { + // The SAT-backed heap use-after-free surfaces through the OOB detector + // (`uaf-access`). + auto uafConfidence = [](const std::string& code) -> std::optional { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) + if (f.id.rfind("uaf-access:", 0) == 0) + return f.confidence; + return std::nullopt; + }; + SECTION("exact: stays Proved (control)") { + const auto c = uafConfidence( + kLibc + "int f() { int* p = (int*)malloc(sizeof(int)); free(p); return p[0]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Proved); + } + SECTION("an over-approximated operation on the path: Heuristic") { + const auto c = uafConfidence(kLibc + "extern int opaque(int);\n" + "int f(int k) { int* p = (int*)malloc(sizeof(int));" + " int n = opaque(k); free(p); return p[n - n]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); + } +} + +namespace { + +// Value of the first sizeof/alignof in `code`, as the encoder would see it. +std::optional firstTypeTrait(const std::string& code, bool c_mode = false) { + auto unit = c_mode ? clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c11"}, "input.c") + : parse(code); + REQUIRE(unit); + struct Finder : clang::RecursiveASTVisitor { + const clang::UnaryExprOrTypeTraitExpr* found = nullptr; + bool VisitUnaryExprOrTypeTraitExpr(clang::UnaryExprOrTypeTraitExpr* e) { + if (!found) + found = e; + return true; + } + } finder; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + REQUIRE(finder.found); + return fold::symbolic::typeTraitConstant(unit->getASTContext(), finder.found); +} + +} // namespace + +TEST_CASE("type-trait constants are exact for complete types only", "[proved-contract][sizeof]") { + // sizeof was an unsupported node, which marked every `malloc(sizeof(T))` + // path imprecise and so could never back a Proved finding. + CHECK(firstTypeTrait("unsigned long f() { return sizeof(int); }") == 4u); + CHECK(firstTypeTrait( + "struct S { char c; double d; }; unsigned long f() { return sizeof(S); }") == 16u); + CHECK(firstTypeTrait("unsigned long f() { return alignof(double); }") == 8u); + // A VLA's size is a runtime value: not a constant. + CHECK_FALSE(firstTypeTrait("unsigned long f(int n) { char buf[n]; return sizeof(buf); }", + /*c_mode=*/true) + .has_value()); +} -- 2.52.0 From c9811b7d4191902608f324e919c5709c9715bc6f Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:37:51 -0600 Subject: [PATCH 05/18] fix(scan): report unanalyzed translation units and exit 2 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. --- AGENTS.md | 3 +- docs/USAGE.md | 10 ++ include/fold/cli/clang_shard_tu.hpp | 23 +++- include/fold/cli/scan_router.hpp | 2 + include/fold/cli/scan_runner.hpp | 3 + include/fold/cli/source_tu_runner.hpp | 3 + include/fold/cli/subprocess_fanout.hpp | 6 + include/fold/report/findings_json_report.hpp | 6 +- include/fold/report/sarif.hpp | 8 +- include/fold/report/scan_coverage.hpp | 43 +++++++ src/cli/clang_shard_tu.cpp | 79 +++++++++---- src/cli/main.cpp | 5 + src/cli/scan_command.cpp | 25 ++++- src/cli/scan_router.cpp | 5 + src/cli/scan_runner.cpp | 8 +- src/cli/source_tu_runner.cpp | 9 +- src/cli/subprocess_fanout.cpp | 12 ++ src/report/findings_json_report.cpp | 14 ++- src/report/meson.build | 1 + src/report/sarif.cpp | 8 +- src/report/scan_coverage.cpp | 47 ++++++++ tests/integration/test_cli_paths.cpp | 44 ++++++++ tests/unit/meson.build | 9 ++ tests/unit/test_scan_coverage.cpp | 112 +++++++++++++++++++ 24 files changed, 435 insertions(+), 50 deletions(-) create mode 100644 include/fold/report/scan_coverage.hpp create mode 100644 src/report/scan_coverage.cpp create mode 100644 tests/unit/test_scan_coverage.cpp diff --git a/AGENTS.md b/AGENTS.md index dc5c27b..1532447 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -42,7 +42,8 @@ Compatibility requirements: - Existing `fold scan --input-type binary --binary ` commands must keep working. - Exit codes stay stable: `0` no actionable findings, `1` actionable findings, - `2` input/config/report failure. + `2` input/config/report failure, including a scan that left any requested + translation unit unanalyzed (see `coverage` in docs/USAGE.md). - Reports must preserve per-finding backend provenance. Router implementation rules: diff --git a/docs/USAGE.md b/docs/USAGE.md index b31bc67..97ada63 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -89,6 +89,16 @@ report. Requested report/profile paths are written atomically; failures return exit `2`. Console counts and both machine formats use the same filtered and deduplicated finding set. +Both machine formats record which C/C++ translation units were analyzed: the +native JSON gains a `coverage` object (`tus_attempted`, `tus_analyzed`, and one +`gaps` entry per unanalyzed TU with a reason: `compile-errors`, +`frontend-failed`, `analysis-failed`, `timeout`, `crash`, or `worker-exit`), +and SARIF carries the same data as an `invocations` entry with +`executionSuccessful` and one `toolExecutionNotifications` entry per gap. A +scan with any gap, or one that analyzed no TU, exits `2` after writing its +report: no findings from an incomplete scan is not evidence of no bugs. +Diagnostics go to stderr, so a report written to stdout stays parseable. + `fold --version` reports the Meson semantic version plus Git revision and a `.dirty` suffix for builds configured from modified trees. SARIF, native JSON, profiles, and benchmark run artifacts retain the same provenance. diff --git a/include/fold/cli/clang_shard_tu.hpp b/include/fold/cli/clang_shard_tu.hpp index e99ff31..854a888 100644 --- a/include/fold/cli/clang_shard_tu.hpp +++ b/include/fold/cli/clang_shard_tu.hpp @@ -13,6 +13,7 @@ class ASTContext; namespace fold { struct Finding; +struct ScanCoverage; struct FunctionSummary; struct SerializedSummary; @@ -34,8 +35,26 @@ struct ClangShardTuHooks { [[nodiscard]] std::string currentClangTuPath(const clang::ASTContext& ctx); -void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, - ClangShardTuState state, ClangShardTuHooks hooks); +// Absolute, symlink-resolved form used to match TU paths across the compile +// DB, the front end, and worker records. +[[nodiscard]] std::string normalizeClangTuPath(const std::string& path); + +// `gap_reason` is empty when the TU was analyzed on a clean AST; otherwise it +// is a CoverageGap reason ("compile-errors", "analysis-failed"). +struct ClangShardTuOutcome { + std::string path; + std::string gap_reason; +}; + +// Workers report the outcome on their `file_finished` record as `gap`. +ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, + ClangShardTuState state, ClangShardTuHooks hooks); + +// Coverage of `requested` TUs given the outcomes recorded for them. A +// requested TU with no outcome never reached the detectors: the front end +// produced no AST for it ("frontend-failed"). +[[nodiscard]] ScanCoverage tuCoverage(const std::vector& requested, + const std::vector& outcomes); } // namespace cli } // namespace fold diff --git a/include/fold/cli/scan_router.hpp b/include/fold/cli/scan_router.hpp index b8f1518..37eeb0d 100644 --- a/include/fold/cli/scan_router.hpp +++ b/include/fold/cli/scan_router.hpp @@ -33,6 +33,8 @@ struct ScanRouterResult { ScanContext context; // RF-8: Rust fuzzable function interfaces carried through the router. std::vector rust_interfaces; + // Which requested C/C++ TUs were actually analyzed. + ScanCoverage coverage; }; std::optional mergeScanProfilesForRouter(const std::optional& source, diff --git a/include/fold/cli/scan_runner.hpp b/include/fold/cli/scan_runner.hpp index 5f8da42..1c5041e 100644 --- a/include/fold/cli/scan_runner.hpp +++ b/include/fold/cli/scan_runner.hpp @@ -9,6 +9,7 @@ #include "fold/frontend/rust_backend.hpp" #include "fold/ir/summary.hpp" #include "fold/report/finding.hpp" +#include "fold/report/scan_coverage.hpp" #include "fold/symbolic/serialize.hpp" namespace fold::ir { @@ -31,6 +32,8 @@ struct ShardResult { // runs detectEquivalentFunctionsCrossTU on the complete merged set. std::vector func_summaries; std::optional profile; + // Per-TU coverage of the clang source lane; untracked elsewhere. + ScanCoverage coverage; }; struct LanguageIrSafetyDetectors { diff --git a/include/fold/cli/source_tu_runner.hpp b/include/fold/cli/source_tu_runner.hpp index e5e82fc..d8ffd57 100644 --- a/include/fold/cli/source_tu_runner.hpp +++ b/include/fold/cli/source_tu_runner.hpp @@ -6,6 +6,7 @@ #include #include +#include "fold/cli/clang_shard_tu.hpp" #include "fold/cli/detector_plan.hpp" #include "fold/cli/profile.hpp" #include "fold/cli/scan_options.hpp" @@ -59,6 +60,8 @@ struct SourceTuRunState { std::size_t security_candidate_functions = 0; std::size_t security_graph_expanded_functions = 0; std::size_t source_tus_completed = 0; + // One entry per TU the front end handed over, in completion order. + std::vector tu_outcomes; // Non-incremental profiling counts definitions during the existing AST // traversal instead of launching a second fingerprinting parse. std::unordered_set profile_function_names; diff --git a/include/fold/cli/subprocess_fanout.hpp b/include/fold/cli/subprocess_fanout.hpp index 7dfc25b..aea21f7 100644 --- a/include/fold/cli/subprocess_fanout.hpp +++ b/include/fold/cli/subprocess_fanout.hpp @@ -8,6 +8,7 @@ #include "fold/cli/scan_options.hpp" #include "fold/report/finding.hpp" +#include "fold/report/scan_coverage.hpp" namespace fold::cli { @@ -35,6 +36,10 @@ class SubprocessFanout { std::vector runSync(const ScanOptions& opts, const std::vector& files, int n_workers); + // Per-TU coverage of the last runSync: TUs with compile errors, TUs the + // front end never produced an AST for, and TUs a worker died on. + [[nodiscard]] const ScanCoverage& coverage() const { return coverage_; } + // Cancel any in-flight workers. Used by MCP/LSP when the client // disconnects mid-scan. Safe to call from any thread. void cancel(); @@ -45,6 +50,7 @@ class SubprocessFanout { std::mutex mtx_; std::vector children_; // tracked PIDs, cleared as they exit bool cancelled_ = false; + ScanCoverage coverage_; }; } // namespace fold::cli diff --git a/include/fold/report/findings_json_report.hpp b/include/fold/report/findings_json_report.hpp index 0e3a060..d70a406 100644 --- a/include/fold/report/findings_json_report.hpp +++ b/include/fold/report/findings_json_report.hpp @@ -4,6 +4,7 @@ #include #include "finding.hpp" +#include "scan_coverage.hpp" namespace fold { @@ -11,6 +12,9 @@ inline constexpr int kFindingsJsonOutputVersion = 1; // Native, lossless report envelope for Fold findings. This is distinct from // SARIF and is versioned so readers can reject incompatible future shapes. -void writeFindingsJson(std::ostream& out, const std::vector& findings); +// With `coverage`, the envelope gains a `coverage` object (additive; the +// output_version is unchanged). +void writeFindingsJson(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage = nullptr); } // namespace fold diff --git a/include/fold/report/sarif.hpp b/include/fold/report/sarif.hpp index 192e67e..f81beed 100644 --- a/include/fold/report/sarif.hpp +++ b/include/fold/report/sarif.hpp @@ -4,6 +4,7 @@ #include #include "finding.hpp" +#include "scan_coverage.hpp" namespace fold { @@ -13,7 +14,10 @@ const char* sarifRuleId(FindingKind kind); // Serialize findings as SARIF 2.1.0 JSON. Single run with tool name "fold". void writeSarif(std::ostream& out, const std::vector& findings); -// Serialize a finding set that has already passed filterAndDedup. -void writeFilteredSarif(std::ostream& out, const std::vector& findings); +// Serialize a finding set that has already passed filterAndDedup. With +// `coverage`, the run carries an `invocations` entry recording which +// translation units were not analyzed. +void writeFilteredSarif(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage = nullptr); } // namespace fold diff --git a/include/fold/report/scan_coverage.hpp b/include/fold/report/scan_coverage.hpp new file mode 100644 index 0000000..770b03f --- /dev/null +++ b/include/fold/report/scan_coverage.hpp @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include +#include + +namespace fold { + +// A translation unit the scan attempted but did not fully analyze. +struct CoverageGap { + std::string file; + // compile-errors: the front end reported errors, so the AST is partial. + // frontend-failed: no AST was produced (missing file, bad command line). + // analysis-failed: the detectors threw on this TU. + // timeout / crash / worker-exit: the isolated worker died on this TU. + std::string reason; +}; + +// What part of the requested input a scan actually analyzed. A report with +// no findings is only evidence of absence when the coverage is complete. +struct ScanCoverage { + // False when the lane does not report per-TU coverage (binary, Rust, + // Swift, reachability-only); such a scan is never marked incomplete. + bool tracked = false; + std::size_t tus_attempted = 0; + std::size_t tus_analyzed = 0; + std::vector gaps; + + [[nodiscard]] bool incomplete() const { + return tracked && (!gaps.empty() || (tus_attempted > 0 && tus_analyzed == 0)); + } + + void merge(const ScanCoverage& other); +}; + +[[nodiscard]] nlohmann::json coverageToJson(const ScanCoverage& coverage); + +// SARIF 2.1.0 `invocations` entry: executionSuccessful plus one +// toolExecutionNotification per gap. +[[nodiscard]] nlohmann::json coverageToSarifInvocation(const ScanCoverage& coverage); + +} // namespace fold diff --git a/src/cli/clang_shard_tu.cpp b/src/cli/clang_shard_tu.cpp index 3ce120b..4ca6ff6 100644 --- a/src/cli/clang_shard_tu.cpp +++ b/src/cli/clang_shard_tu.cpp @@ -1,6 +1,7 @@ #include "fold/cli/clang_shard_tu.hpp" #include +#include #include #include @@ -8,33 +9,22 @@ #include #include #include +#include #include "fold/cli/scan_options.hpp" #include "fold/cli/signal_isolation.hpp" #include "fold/report/finding.hpp" #include "fold/report/finding_json.hpp" +#include "fold/report/scan_coverage.hpp" #include "fold/symbolic/serialize.hpp" namespace fold::cli { namespace { -std::string normalizeTuPath(const std::string& path) { - if (path.empty()) - return path; - std::error_code ec; - std::filesystem::path p(path); - std::filesystem::path abs = p.is_absolute() ? p : std::filesystem::absolute(p, ec); - if (ec) - return p.lexically_normal().string(); - auto canonical = std::filesystem::weakly_canonical(abs, ec); - if (!ec) - return canonical.string(); - return abs.lexically_normal().string(); -} - void emitWorkerTuPayload(std::ostream& out, const ClangShardTuState& state, std::size_t start_summaries, std::size_t start_func_summaries, - std::size_t start_findings, const std::string& tu_path) { + std::size_t start_findings, const std::string& tu_path, + const std::string& gap_reason) { for (std::size_t i = start_summaries; i < state.summaries->size(); ++i) { out << nlohmann::json{{"kind", "summary"}, {"data", fold::summaryToJson((*state.summaries)[i])}} @@ -62,12 +52,29 @@ void emitWorkerTuPayload(std::ostream& out, const ClangShardTuState& state, state.findings->erase(state.findings->begin() + static_cast(start_findings), state.findings->end()); - out << nlohmann::json{{"kind", "file_finished"}, {"data", {{"path", tu_path}}}}.dump() << '\n'; + out << nlohmann::json{{"kind", "file_finished"}, + {"data", {{"path", tu_path}, {"gap", gap_reason}}}} + .dump() + << '\n'; out.flush(); } } // namespace +std::string normalizeClangTuPath(const std::string& path) { + if (path.empty()) + return path; + std::error_code ec; + std::filesystem::path p(path); + std::filesystem::path abs = p.is_absolute() ? p : std::filesystem::absolute(p, ec); + if (ec) + return p.lexically_normal().string(); + auto canonical = std::filesystem::weakly_canonical(abs, ec); + if (!ec) + return canonical.string(); + return abs.lexically_normal().string(); +} + std::string currentClangTuPath(const clang::ASTContext& ctx) { const auto& sm = ctx.getSourceManager(); auto fid = sm.getMainFileID(); @@ -76,17 +83,18 @@ std::string currentClangTuPath(const clang::ASTContext& ctx) { return ""; } -void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, - ClangShardTuState state, ClangShardTuHooks hooks) { - const std::string tu_path = normalizeTuPath(currentClangTuPath(ctx)); +ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, + ClangShardTuState state, ClangShardTuHooks hooks) { + const std::string tu_path = normalizeClangTuPath(currentClangTuPath(ctx)); + ClangShardTuOutcome outcome{tu_path, "analysis-failed"}; if (!state.summaries || !state.func_summaries || !state.findings || !state.quarantined_this_run) { spdlog::warn("scan: skipped TU {} because shard state was not initialized", tu_path); - return; + return outcome; } if (state.quarantined_this_run->count(tu_path) != 0u) { spdlog::warn("scan: skipped TU {} already quarantined in this run", tu_path); - return; + return outcome; } const std::size_t start_summaries = state.summaries->size(); @@ -99,9 +107,15 @@ void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ct hooks.handle_translation_unit(ctx); }, opts.per_tu_timeout_seconds); + // The front end recovers from errors and still hands over an AST, + // but it is missing whatever failed to parse. + const bool compile_errors = ctx.getDiagnostics().hasErrorOccurred(); + outcome.gap_reason = compile_errors ? "compile-errors" : ""; + if (compile_errors) + spdlog::error("scan: {} has compile errors; its analysis is incomplete", tu_path); if (opts.is_worker) { emitWorkerTuPayload(std::cout, state, start_summaries, start_func_summaries, - start_findings, tu_path); + start_findings, tu_path, outcome.gap_reason); } } catch (const std::exception& e) { spdlog::warn("scan: skipped TU {} after exception: {}", tu_path, e.what()); @@ -112,6 +126,27 @@ void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ct if (opts.is_worker) ::_Exit(1); } + return outcome; +} + +ScanCoverage tuCoverage(const std::vector& requested, + const std::vector& outcomes) { + std::unordered_map gap_by_path; + for (const auto& outcome : outcomes) + gap_by_path.insert_or_assign(normalizeClangTuPath(outcome.path), outcome.gap_reason); + ScanCoverage coverage; + coverage.tracked = true; + coverage.tus_attempted = requested.size(); + for (const auto& file : requested) { + const auto it = gap_by_path.find(normalizeClangTuPath(file)); + if (it == gap_by_path.end()) + coverage.gaps.push_back({file, "frontend-failed"}); + else if (!it->second.empty()) + coverage.gaps.push_back({file, it->second}); + else + ++coverage.tus_analyzed; + } + return coverage; } } // namespace fold::cli diff --git a/src/cli/main.cpp b/src/cli/main.cpp index c5ac311..7601813 100644 --- a/src/cli/main.cpp +++ b/src/cli/main.cpp @@ -402,6 +402,11 @@ int main(int argc, char** argv) { return rc == 0 ? 0 : 2; } + // Diagnostics go to stderr so a report written to stdout stays parseable + // (docs/internal/cli-philosophy.md principle 12). + spdlog::default_logger()->sinks().clear(); + spdlog::default_logger()->sinks().push_back( + std::make_shared()); if (quiet) { spdlog::set_level(spdlog::level::warn); } diff --git a/src/cli/scan_command.cpp b/src/cli/scan_command.cpp index 20e8403..c064542 100644 --- a/src/cli/scan_command.cpp +++ b/src/cli/scan_command.cpp @@ -107,16 +107,17 @@ bool writeStreamAtomically(const std::string& output_path, Writer&& writer) { } int writeReport(const std::vector& report_findings, const std::string& output_path, - const std::string& format, bool redundancy_secondary = false) { + const std::string& format, const fold::ScanCoverage& coverage, + bool redundancy_secondary = false) { const auto serialize = [&](std::ostream& out) { if (format == "sarif") { - fold::writeFilteredSarif(out, report_findings); + fold::writeFilteredSarif(out, report_findings, &coverage); } else if (format == "json") { spdlog::warn("report format 'json' is deprecated as a SARIF alias; use 'sarif' or " "'findings-json'"); - fold::writeFilteredSarif(out, report_findings); + fold::writeFilteredSarif(out, report_findings, &coverage); } else if (format == "findings-json") { - fold::writeFindingsJson(out, report_findings); + fold::writeFindingsJson(out, report_findings, &coverage); } else if (format == "markdown" || format == "md") { fold::writeMarkdown(out, report_findings, redundancy_secondary); } else { @@ -318,8 +319,9 @@ int runScan(const ScanCommand& cli) { } const auto report_started = std::chrono::steady_clock::now(); - const int report_rc = writeReport(report_findings, cli.output_path, cli.format, - opts.freestanding.redundancy_lane_secondary); + const int report_rc = + writeReport(report_findings, cli.output_path, cli.format, router_result.coverage, + opts.freestanding.redundancy_lane_secondary); const auto report_finished = std::chrono::steady_clock::now(); if (report_rc == 2) return 2; @@ -338,6 +340,17 @@ int runScan(const ScanCommand& cli) { return 2; } + // A scan that skipped part of its input cannot vouch for the absence of + // findings there, so it is an input failure (exit 2) even when it found + // nothing. + if (router_result.coverage.incomplete()) { + const auto& coverage = router_result.coverage; + spdlog::error("scan incomplete: analyzed {} of {} translation unit(s)", + coverage.tus_analyzed, coverage.tus_attempted); + for (const auto& gap : coverage.gaps) + spdlog::error(" not analyzed ({}): {}", gap.reason, gap.file); + return 2; + } return report_rc; } diff --git a/src/cli/scan_router.cpp b/src/cli/scan_router.cpp index 1b69783..da58fb0 100644 --- a/src/cli/scan_router.cpp +++ b/src/cli/scan_router.cpp @@ -34,6 +34,7 @@ struct SourceRun { std::optional shard; std::optional profile; std::vector sources; + ScanCoverage coverage; }; struct BinaryRun { @@ -434,6 +435,7 @@ SourceRun runSource(ScanOptions opts) { fold::cli::SubprocessFanout fanout; const auto fanout_start = Clock::now(); run.findings = fanout.runSync(opts, sources, processes); + run.coverage = fanout.coverage(); fanout_ms = durationMs(fanout_start, Clock::now()); } else { spdlog::info("serial: running on {} files", sources.size()); @@ -443,6 +445,7 @@ SourceRun runSource(ScanOptions opts) { serial_ms = durationMs(serial_start, Clock::now()); run.findings = run.shard->findings; run.profile = run.shard->profile; + run.coverage = run.shard->coverage; } // Stamp the per-phase timings onto the profile so the perf-audit // doc can quote them. When --profile isn't on, run.profile is @@ -762,6 +765,7 @@ ScanRouterResult runScanRouter(ScanOptions opts) { result.source_shard = std::move(source.shard); result.profile = std::move(source.profile); result.findings = std::move(source.findings); + result.coverage = std::move(source.coverage); } else if (mode == "rust") { auto rust = runRust(opts); // Re-use the source-side context slots; findings are tagged @@ -814,6 +818,7 @@ ScanRouterResult runScanRouter(ScanOptions opts) { result.context.binary_findings = binary.findings.size(); result.source_shard = std::move(source.shard); result.binary_shard = std::move(binary.shard); + result.coverage = std::move(source.coverage); result.profile = mergeScanProfilesForRouter(source.profile, binary.profile, opts); result.findings.reserve(source.findings.size() + binary.findings.size()); result.findings.insert(result.findings.end(), diff --git a/src/cli/scan_runner.cpp b/src/cli/scan_runner.cpp index 9ea3c59..0c12af2 100644 --- a/src/cli/scan_runner.cpp +++ b/src/cli/scan_runner.cpp @@ -583,14 +583,14 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db, clone_cache.get(), graph_security_candidates.empty() ? nullptr : &graph_security_candidates}; auto factory = makeSourceTuFrontendFactory(tu_config, tu_state); - (void)tool.run(factory.get()); + (void)tool.run(factory.get()); // which TUs failed comes from tu_outcomes + out.coverage = tuCoverage(files, tu_state.tu_outcomes); } if (out.profile) { out.profile->source_tus_completed = tu_state.source_tus_completed; out.profile->source_tus_frontend_failed = - out.profile->source_tus_attempted >= out.profile->source_tus_completed - ? out.profile->source_tus_attempted - out.profile->source_tus_completed - : 0; + out.profile->source_tus_attempted - + std::min(out.profile->source_tus_attempted, out.profile->source_tus_completed); } if (detector_plan.production_reachability) diff --git a/src/cli/source_tu_runner.cpp b/src/cli/source_tu_runner.cpp index 332789f..6f8139a 100644 --- a/src/cli/source_tu_runner.cpp +++ b/src/cli/source_tu_runner.cpp @@ -222,10 +222,11 @@ class ShardFrontend final : public clang::ASTFrontendAction { handleTranslationUnitImpl(tu_ctx); }; hooks.quarantine_writer = quarantine_writer; - runClangShardTranslationUnit(opts, ctx, - ClangShardTuState{&summaries, &func_summaries, - &findings, &quarantined_this_run}, - std::move(hooks)); + state.tu_outcomes.push_back(runClangShardTranslationUnit( + opts, ctx, + ClangShardTuState{&summaries, &func_summaries, &findings, + &quarantined_this_run}, + std::move(hooks))); ++state.source_tus_completed; } diff --git a/src/cli/subprocess_fanout.cpp b/src/cli/subprocess_fanout.cpp index 17e9f43..4315c15 100644 --- a/src/cli/subprocess_fanout.cpp +++ b/src/cli/subprocess_fanout.cpp @@ -23,6 +23,7 @@ #include #include +#include "fold/cli/clang_shard_tu.hpp" #include "fold/cli/tu_quarantine.hpp" #include "fold/detect/clone.hpp" #include "fold/detect/equiv.hpp" @@ -83,6 +84,8 @@ struct ShardOutput { std::vector summaries; std::vector findings; std::vector func_summaries; + // file_finished records plus the TU each dead worker was processing. + std::vector tu_outcomes; bool success = true; }; @@ -168,6 +171,8 @@ ShardOutput runShardWithRecovery(const std::string& binary, local_func_summaries.push_back(fromJson(data)); } else if (kind == "file_finished") { finished_files.insert(normalizePath(data.value("path", ""))); + result.tu_outcomes.push_back( + {data.value("path", ""), data.value("gap", "")}); } } catch (const std::exception& e) { spdlog::warn("subprocess_fanout: bad NDJSON line: {}", e.what()); @@ -217,6 +222,8 @@ ShardOutput runShardWithRecovery(const std::string& binary, bool is_signal = WIFSIGNALED(status); const bool is_timeout = worker_read.timed_out || (is_signal && sig_or_status == SIGALRM); + result.tu_outcomes.push_back( + {failed_file, is_timeout ? "timeout" : (is_signal ? "crash" : "worker-exit")}); if (is_timeout) { spdlog::warn("worker pid {} timed out after {}s while processing TU: {}", kid.pid, opts.per_tu_timeout_seconds, failed_file); @@ -579,6 +586,7 @@ std::vector SubprocessFanout::runSync(const ScanOptions& opts, std::vector all_summaries; std::vector all_findings; std::vector all_func_summaries; + std::vector all_tu_outcomes; bool all_shards_succeeded = true; for (auto& t : tasks) { auto res = t.get(); @@ -590,6 +598,9 @@ std::vector SubprocessFanout::runSync(const ScanOptions& opts, all_func_summaries.insert(all_func_summaries.end(), std::make_move_iterator(res.func_summaries.begin()), std::make_move_iterator(res.func_summaries.end())); + all_tu_outcomes.insert(all_tu_outcomes.end(), + std::make_move_iterator(res.tu_outcomes.begin()), + std::make_move_iterator(res.tu_outcomes.end())); } { std::lock_guard lk(mtx_); @@ -597,6 +608,7 @@ std::vector SubprocessFanout::runSync(const ScanOptions& opts, } if (!all_shards_succeeded) throw std::runtime_error("source worker failed before completing its shard"); + coverage_ = tuCoverage(files, all_tu_outcomes); // Global clone clustering on the merged summary set. Multiple workers // re-#include the same headers and emit summaries for those header diff --git a/src/report/findings_json_report.cpp b/src/report/findings_json_report.cpp index a257756..d8ca43a 100644 --- a/src/report/findings_json_report.cpp +++ b/src/report/findings_json_report.cpp @@ -7,15 +7,17 @@ namespace fold { -void writeFindingsJson(std::ostream& out, const std::vector& findings) { +void writeFindingsJson(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage) { json encoded = json::array(); for (const auto& finding : findings) encoded.push_back(findingToJson(finding)); - out << json{{"output_version", kFindingsJsonOutputVersion}, - {"tool", {{"name", "fold"}, {"version", foldVersion()}}}, - {"findings", encoded}} - .dump(2) - << '\n'; + json document{{"output_version", kFindingsJsonOutputVersion}, + {"tool", {{"name", "fold"}, {"version", foldVersion()}}}, + {"findings", encoded}}; + if (coverage != nullptr) + document["coverage"] = coverageToJson(*coverage); + out << document.dump(2) << '\n'; } } // namespace fold diff --git a/src/report/meson.build b/src/report/meson.build index 0998969..e343c53 100644 --- a/src/report/meson.build +++ b/src/report/meson.build @@ -7,6 +7,7 @@ fold_core_sources += files( 'findings_json_report.cpp', 'markdown.cpp', 'patch_writer.cpp', + 'scan_coverage.cpp', 'sarif.cpp', 'triage.cpp', ) diff --git a/src/report/sarif.cpp b/src/report/sarif.cpp index db365c0..0377718 100644 --- a/src/report/sarif.cpp +++ b/src/report/sarif.cpp @@ -404,7 +404,8 @@ void writeSarif(std::ostream& out, const std::vector& findings) { writeFilteredSarif(out, deduped); } -void writeFilteredSarif(std::ostream& out, const std::vector& findings) { +void writeFilteredSarif(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage) { const json tool = { {"driver", { @@ -421,7 +422,10 @@ void writeFilteredSarif(std::ostream& out, const std::vector& findings) out << R"({"$schema":"https://json.schemastore.org/sarif-2.1.0.json",)" R"("version":"2.1.0","runs":[{"tool":)" - << tool.dump() << R"(,"results":[)"; + << tool.dump(); + if (coverage != nullptr) + out << R"(,"invocations":)" << json::array({coverageToSarifInvocation(*coverage)}).dump(); + out << R"(,"results":[)"; for (std::size_t index = 0; index < findings.size(); ++index) { if (index != 0) out << ','; diff --git a/src/report/scan_coverage.cpp b/src/report/scan_coverage.cpp new file mode 100644 index 0000000..c25a636 --- /dev/null +++ b/src/report/scan_coverage.cpp @@ -0,0 +1,47 @@ +#include "fold/report/scan_coverage.hpp" + +namespace fold { + +void ScanCoverage::merge(const ScanCoverage& other) { + if (!other.tracked) + return; + tracked = true; + tus_attempted += other.tus_attempted; + tus_analyzed += other.tus_analyzed; + gaps.insert(gaps.end(), other.gaps.begin(), other.gaps.end()); +} + +nlohmann::json coverageToJson(const ScanCoverage& coverage) { + nlohmann::json gaps = nlohmann::json::array(); + for (const auto& gap : coverage.gaps) + gaps.push_back({{"file", gap.file}, {"reason", gap.reason}}); + return {{"tracked", coverage.tracked}, + {"complete", !coverage.incomplete()}, + {"tus_attempted", coverage.tus_attempted}, + {"tus_analyzed", coverage.tus_analyzed}, + {"gaps", gaps}}; +} + +nlohmann::json coverageToSarifInvocation(const ScanCoverage& coverage) { + nlohmann::json notifications = nlohmann::json::array(); + for (const auto& gap : coverage.gaps) { + notifications.push_back( + {{"level", "error"}, + {"descriptor", {{"id", "fold/coverage/" + gap.reason}}}, + {"message", {{"text", "translation unit not analyzed (" + gap.reason + ")"}}}, + {"locations", + nlohmann::json::array( + {{{"physicalLocation", {{"artifactLocation", {{"uri", gap.file}}}}}}})}}); + } + if (coverage.tracked && coverage.tus_attempted > 0 && coverage.tus_analyzed == 0 && + coverage.gaps.empty()) { + notifications.push_back({{"level", "error"}, + {"descriptor", {{"id", "fold/coverage/none-analyzed"}}}, + {"message", {{"text", "no translation unit was analyzed"}}}}); + } + return {{"executionSuccessful", !coverage.incomplete()}, + {"toolExecutionNotifications", notifications}, + {"properties", {{"coverage", coverageToJson(coverage)}}}}; +} + +} // namespace fold diff --git a/tests/integration/test_cli_paths.cpp b/tests/integration/test_cli_paths.cpp index a4269a6..dd2577b 100644 --- a/tests/integration/test_cli_paths.cpp +++ b/tests/integration/test_cli_paths.cpp @@ -476,3 +476,47 @@ TEST_CASE("fold scan formats have truthful distinct contracts", "[cli][contract] REQUIRE(log_text.find(input_type_warning, log_text.find(input_type_warning) + 1) == std::string::npos); } + +TEST_CASE("fold scan fails when a translation unit is not analyzed", "[cli][coverage]") { + // A TU that failed to parse used to leave no trace: no findings, exit 0. + const std::string fold_bin = locateFoldBinary(); + if (fold_bin.empty()) { + WARN("could not locate fold binary; skipping CLI coverage test"); + return; + } + + TempDir dir; + const auto good = dir.path / "good.cpp"; + const auto broken = dir.path / "broken.cpp"; + writeFile(good, "int add(int a, int b) { return a + b; }\n"); + writeFile(broken, "#include \"does_not_exist.h\"\nint f(int x) { return x; }\n"); + + const auto scan = [&](const std::filesystem::path& source, const std::string& format, + const std::filesystem::path& report) { + const std::string command = "\"" + fold_bin + "\" --quiet scan --detectors div-by-zero " + + "--format " + format + " \"" + source.string() + "\" > \"" + + report.string() + "\" 2>/dev/null"; + return commandExitCode(std::system(command.c_str())); + }; + + SECTION("clean TU: complete coverage, exit 0 (control)") { + const auto report = dir.path / "good.json"; + REQUIRE(scan(good, "findings-json", report) == 0); + const auto json = nlohmann::json::parse(readFile(report)); + CHECK(json["coverage"]["complete"] == true); + CHECK(json["coverage"]["tus_analyzed"] == 1); + } + SECTION("broken TU: gap in findings JSON, exit 2") { + const auto report = dir.path / "broken.json"; + REQUIRE(scan(broken, "findings-json", report) == 2); + const auto json = nlohmann::json::parse(readFile(report)); + CHECK(json["coverage"]["complete"] == false); + CHECK(json["coverage"]["gaps"][0]["reason"] == "compile-errors"); + } + SECTION("broken TU: SARIF on stdout stays parseable and records the failure") { + const auto report = dir.path / "broken.sarif"; + REQUIRE(scan(broken, "sarif", report) == 2); + const auto sarif = nlohmann::json::parse(readFile(report)); + CHECK(sarif["runs"][0]["invocations"][0]["executionSuccessful"] == false); + } +} diff --git a/tests/unit/meson.build b/tests/unit/meson.build index fbbd4c5..86ae3f2 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -213,6 +213,15 @@ test_proved_requires_exact_model = executable( ) test('proved_requires_exact_model', test_proved_requires_exact_model) +test_scan_coverage = executable( + 'test_scan_coverage', + 'test_scan_coverage.cpp', + dependencies: [fold_core_dep, catch2_dep, json_dep], + install: false, + build_by_default: false, +) +test('scan_coverage', test_scan_coverage) + test_batch_safety_observer = executable( 'test_batch_safety_observer', 'test_batch_safety_observer.cpp', diff --git a/tests/unit/test_scan_coverage.cpp b/tests/unit/test_scan_coverage.cpp new file mode 100644 index 0000000..c66e8a3 --- /dev/null +++ b/tests/unit/test_scan_coverage.cpp @@ -0,0 +1,112 @@ +#include +#include +#include +#include +#include +#include + +#include "fold/cli/clang_shard_tu.hpp" +#include "fold/report/findings_json_report.hpp" +#include "fold/report/sarif.hpp" +#include "fold/report/scan_coverage.hpp" + +// A TU the front end could not parse used to vanish: the report had no trace +// of it and the scan exited 0, indistinguishable from a clean scan. Coverage +// now records every requested TU that was not analyzed on a clean AST. + +namespace { + +std::string tmp(const std::string& name) { + return (std::filesystem::temp_directory_path() / name).string(); +} + +} // namespace + +TEST_CASE("tuCoverage classifies every requested TU", "[coverage]") { + const std::vector requested{tmp("ok.cpp"), tmp("broken.cpp"), tmp("missing.cpp"), + tmp("slow.cpp")}; + const std::vector outcomes{ + {tmp("ok.cpp"), ""}, + {tmp("broken.cpp"), "compile-errors"}, + {tmp("slow.cpp"), "timeout"}, + }; + const auto coverage = fold::cli::tuCoverage(requested, outcomes); + CHECK(coverage.tracked); + CHECK(coverage.tus_attempted == 4); + CHECK(coverage.tus_analyzed == 1); + REQUIRE(coverage.gaps.size() == 3); + CHECK(coverage.gaps[0].file == tmp("broken.cpp")); + CHECK(coverage.gaps[0].reason == "compile-errors"); + CHECK(coverage.gaps[1].file == tmp("missing.cpp")); + CHECK(coverage.gaps[1].reason == "frontend-failed"); + CHECK(coverage.gaps[2].reason == "timeout"); + CHECK(coverage.incomplete()); +} + +TEST_CASE("tuCoverage matches paths across spellings", "[coverage]") { + // The compile DB may spell a path differently than the front end does. + const auto dir = std::filesystem::temp_directory_path(); + const std::string dotted = (dir / "sub" / ".." / "a.cpp").string(); + const auto coverage = fold::cli::tuCoverage({dotted}, {{(dir / "a.cpp").string(), ""}}); + CHECK(coverage.tus_analyzed == 1); + CHECK_FALSE(coverage.incomplete()); +} + +TEST_CASE("coverage: complete, untracked and empty scans", "[coverage]") { + SECTION("every TU analyzed is complete (control)") { + const auto coverage = fold::cli::tuCoverage({tmp("a.cpp")}, {{tmp("a.cpp"), ""}}); + CHECK_FALSE(coverage.incomplete()); + } + SECTION("an untracked lane is never incomplete") { + fold::ScanCoverage coverage; + coverage.tus_attempted = 3; + CHECK_FALSE(coverage.incomplete()); + } + SECTION("attempted TUs with none analyzed is incomplete even without gaps") { + fold::ScanCoverage coverage; + coverage.tracked = true; + coverage.tus_attempted = 2; + CHECK(coverage.incomplete()); + } + SECTION("merge sums counts and keeps gaps; an untracked side is ignored") { + auto a = fold::cli::tuCoverage({tmp("a.cpp")}, {{tmp("a.cpp"), ""}}); + const auto b = fold::cli::tuCoverage({tmp("b.cpp")}, {}); + a.merge(b); + a.merge(fold::ScanCoverage{}); + CHECK(a.tus_attempted == 2); + CHECK(a.tus_analyzed == 1); + CHECK(a.gaps.size() == 1); + } +} + +TEST_CASE("reports carry coverage", "[coverage][report]") { + const auto coverage = + fold::cli::tuCoverage({tmp("broken.cpp")}, {{tmp("broken.cpp"), "compile-errors"}}); + SECTION("SARIF: invocation is unsuccessful and names the TU") { + std::ostringstream out; + fold::writeFilteredSarif(out, {}, &coverage); + const auto sarif = nlohmann::json::parse(out.str()); + const auto& invocation = sarif["runs"][0]["invocations"][0]; + CHECK(invocation["executionSuccessful"] == false); + const auto& note = invocation["toolExecutionNotifications"][0]; + CHECK(note["level"] == "error"); + CHECK(note["locations"][0]["physicalLocation"]["artifactLocation"]["uri"] == + tmp("broken.cpp")); + CHECK(invocation["properties"]["coverage"]["tus_analyzed"] == 0); + } + SECTION("findings JSON: coverage object") { + std::ostringstream out; + fold::writeFindingsJson(out, {}, &coverage); + const auto report = nlohmann::json::parse(out.str()); + CHECK(report["coverage"]["complete"] == false); + CHECK(report["coverage"]["gaps"][0]["reason"] == "compile-errors"); + } + SECTION("no coverage argument leaves the documents unchanged") { + std::ostringstream sarif_out; + fold::writeFilteredSarif(sarif_out, {}); + CHECK_FALSE(nlohmann::json::parse(sarif_out.str())["runs"][0].contains("invocations")); + std::ostringstream json_out; + fold::writeFindingsJson(json_out, {}); + CHECK_FALSE(nlohmann::json::parse(json_out.str()).contains("coverage")); + } +} -- 2.52.0 From 46aaac427a9af76b25bff47a48fc62d9daad9493 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:49:38 -0600 Subject: [PATCH 06/18] fix(summary): key function summaries by USR, not qualified name 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). --- .../fold/symbolic/encoder_callee_names.hpp | 12 +- src/cli/source_summary_pipeline.cpp | 18 ++- src/detect/div_by_zero.cpp | 3 +- src/detect/null_deref.cpp | 10 +- src/detect/oob_access.cpp | 3 +- src/symbolic/encoder_callee_names.cpp | 10 ++ src/symbolic/summary_encoder.cpp | 19 +-- tests/integration/test_cross_tu_security.cpp | 40 ++++- tests/unit/meson.build | 9 ++ tests/unit/test_summary_key_identity.cpp | 141 ++++++++++++++++++ tests/unit/test_symbolic_summary.cpp | 3 +- 11 files changed, 240 insertions(+), 28 deletions(-) create mode 100644 tests/unit/test_summary_key_identity.cpp diff --git a/include/fold/symbolic/encoder_callee_names.hpp b/include/fold/symbolic/encoder_callee_names.hpp index 266224a..d9f8b6f 100644 --- a/include/fold/symbolic/encoder_callee_names.hpp +++ b/include/fold/symbolic/encoder_callee_names.hpp @@ -23,12 +23,20 @@ namespace fold { [[nodiscard]] std::string calleeName(const clang::CallExpr* ce); // Qualified callee name with a TU-local suffix for internal linkage -// to disambiguate `static` functions across TUs. Form used by the -// summary cache to key per-function summaries. +// to disambiguate `static` functions across TUs. Human-readable; overloads +// share it, so it must not key per-function data (see summaryStoreKey). [[nodiscard]] std::string qualifiedFunctionName(const clang::FunctionDecl* fd); [[nodiscard]] std::string qualifiedCalleeName(const clang::CallExpr* ce); +// Key for detect::SummaryStore: the declaration's USR (semanticFunctionId), +// equal across redeclarations and TUs for one external function and distinct +// for overloads. Empty for a null declaration. +[[nodiscard]] std::string summaryStoreKey(const clang::FunctionDecl* fd); + +// summaryStoreKey of a call's direct callee; empty for indirect calls. +[[nodiscard]] std::string summaryStoreKeyForCall(const clang::CallExpr* ce); + // True when `fd` can be the C library function its name suggests: not a class // member, and declared at global scope, in namespace std, or extern "C". // Library models (malloc/free, taint sources and sinks) must check this; the diff --git a/src/cli/source_summary_pipeline.cpp b/src/cli/source_summary_pipeline.cpp index bf0f020..94db868 100644 --- a/src/cli/source_summary_pipeline.cpp +++ b/src/cli/source_summary_pipeline.cpp @@ -23,6 +23,7 @@ #include "fold/frontend/comp_db.hpp" #include "fold/ir/call_graph.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/summary_encoder.hpp" namespace fold::cli { @@ -86,19 +87,22 @@ bool computeSummariesForFunctions(clang::tooling::CompilationDatabase& db, if (qualified_name.empty() || !target_names_.contains(qualified_name)) return true; + // The graph names functions by qualified name; the + // store keys them by USR so overloads stay apart. + const std::string summary_key = ::fold::summaryStoreKey(declaration); const std::uint64_t source_hash = detect::hashFunctionBody(declaration, source_manager); auto& store = detect::SummaryStore::instance(); - const auto* previous = store.lookup(qualified_name); - if (previous && store.isStale(qualified_name, source_hash)) { - store.invalidate(qualified_name); + const auto* previous = store.lookup(summary_key); + if (previous && store.isStale(summary_key, source_hash)) { + store.invalidate(summary_key); previous = nullptr; } const std::string before = previous ? previous->serialize() : std::string{}; if (!force_recompute_ && previous && - !store.isStale(qualified_name, source_hash)) { + !store.isStale(summary_key, source_hash)) { return true; } @@ -106,15 +110,15 @@ bool computeSummariesForFunctions(clang::tooling::CompilationDatabase& db, if (auto summary = ::fold::summarizeLeafFunctionSymbolically( declaration, context_)) { const std::string after = summary->serialize(); - store.store(qualified_name, *summary); - store.markComputed(qualified_name, source_hash); + store.store(summary_key, *summary); + store.markComputed(summary_key, source_hash); markChanged(after, before); } return true; } (void)::fold::ensureSymbolicSummary(declaration, context_); - if (const auto* current = store.lookup(qualified_name)) + if (const auto* current = store.lookup(summary_key)) markChanged(current->serialize(), before); return true; } diff --git a/src/detect/div_by_zero.cpp b/src/detect/div_by_zero.cpp index 769f406..8ef3b46 100644 --- a/src/detect/div_by_zero.cpp +++ b/src/detect/div_by_zero.cpp @@ -34,6 +34,7 @@ #include "fold/fuzz/param_schema.hpp" #include "fold/ir/normalize.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/expr_hash.hpp" #include "fold/symbolic/interval.hpp" #include "fold/symbolic/safety_observer.hpp" @@ -609,7 +610,7 @@ class DivByZeroObserver : public SafetyObserver { const symbolic::SymbolicSummary* summary = nullptr; { SolverStats::ScopedPhaseTimer _t(&stats_, &SolverStats::summary_lookup_ms); - summary = detect::SummaryStore::instance().lookup(callee_name); + summary = detect::SummaryStore::instance().lookup(summaryStoreKey(callee)); } if (!summary || summary->param_pre.empty()) return false; diff --git a/src/detect/null_deref.cpp b/src/detect/null_deref.cpp index 9148ea7..b75f164 100644 --- a/src/detect/null_deref.cpp +++ b/src/detect/null_deref.cpp @@ -36,6 +36,7 @@ #include "fold/ir/def_use.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/expr_hash.hpp" #include "fold/symbolic/heap_model.hpp" #include "fold/symbolic/safety_observer.hpp" @@ -765,7 +766,7 @@ class NullDerefObserver : public SafetyObserver { const symbolic::SymbolicSummary* summary = nullptr; { SolverStats::ScopedPhaseTimer _t(&stats_, &SolverStats::summary_lookup_ms); - summary = detect::SummaryStore::instance().lookup(callee_name); + summary = detect::SummaryStore::instance().lookup(summaryStoreKey(callee)); } if (!summary || summary->param_pre.empty()) return false; @@ -790,6 +791,13 @@ class NullDerefObserver : public SafetyObserver { // — skip both the solver query and the emission. if (vd && env && env->isDefinitelyNonNull(vd)) continue; + // Same contract filters as the callee-deref path below; static + // callees reach here now that summaries are keyed by USR. + if ((vd && current_debugassert_nonnull_.count(vd->getNameAsString()) > 0) || + staticCalleeParamContractProvesNonNull(callee, idx)) { + ++stats_.abstract_unsat; + continue; + } z3::check_result result = checkPreconditionViolation(*predicate, path, loc); if (result == z3::unsat || !emitted.insert(idx).second) continue; diff --git a/src/detect/oob_access.cpp b/src/detect/oob_access.cpp index ceebe1f..c8288d4 100644 --- a/src/detect/oob_access.cpp +++ b/src/detect/oob_access.cpp @@ -34,6 +34,7 @@ #include "fold/detect/z3_model_support.hpp" #include "fold/fuzz/param_schema.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/encoder_detail.hpp" #include "fold/symbolic/expr_hash.hpp" #include "fold/symbolic/heap_model.hpp" @@ -406,7 +407,7 @@ class OOBObserver : public SafetyObserver { const auto* call = call_ir.asClangCallExpr(); (void)env; const auto* callee = call ? call->getDirectCallee() : nullptr; - const std::string summary_name = qualifiedFunctionName(callee); + const std::string summary_name = summaryStoreKey(callee); const std::string callee_name = callee ? callee->getQualifiedNameAsString() : std::string{}; if (callee_name.empty()) return; diff --git a/src/symbolic/encoder_callee_names.cpp b/src/symbolic/encoder_callee_names.cpp index 7be3fb1..2a746fd 100644 --- a/src/symbolic/encoder_callee_names.cpp +++ b/src/symbolic/encoder_callee_names.cpp @@ -7,6 +7,8 @@ #include #include +#include "fold/frontend/stable_identity.hpp" + namespace fold { std::string calleeName(const clang::CallExpr* ce) { @@ -61,6 +63,14 @@ std::string qualifiedFunctionName(const clang::FunctionDecl* fd) { return name; } +std::string summaryStoreKey(const clang::FunctionDecl* fd) { + return fd == nullptr ? std::string{} : semanticFunctionId(fd); +} + +std::string summaryStoreKeyForCall(const clang::CallExpr* ce) { + return ce == nullptr ? std::string{} : summaryStoreKey(ce->getDirectCallee()); +} + bool isCLibraryFunction(const clang::FunctionDecl* fd) { if (fd == nullptr || clang::isa(fd)) return false; diff --git a/src/symbolic/summary_encoder.cpp b/src/symbolic/summary_encoder.cpp index d8c902f..841326c 100644 --- a/src/symbolic/summary_encoder.cpp +++ b/src/symbolic/summary_encoder.cpp @@ -21,6 +21,7 @@ #include "fold/detect/incremental_cache.hpp" #include "fold/detect/summary_store.hpp" #include "fold/symbolic/cfg_helpers.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/safety_observer.hpp" namespace fold { @@ -165,7 +166,7 @@ class SummaryMetadataCollector : public clang::RecursiveASTVisitorgetDirectCallee() : nullptr; if (!callee) return true; - std::string qname = qualifiedFunctionName(callee); + std::string qname = summaryStoreKey(callee); if (!qname.empty()) { callees.insert(qname); callee_decls.emplace(std::move(qname), callee); @@ -292,7 +293,7 @@ class SummaryPreconditionRecorder : public SafetyObserver { const z3::expr& path, const ir::SourceLoc& /*loc*/, const SymbolicEnv* /*env*/ = nullptr) override { const auto* call = call_ir.asClangCallExpr(); - const std::string callee_name = qualifiedCalleeName(call); + const std::string callee_name = summaryStoreKeyForCall(call); if (callee_name.empty()) return; const auto* summary = detect::SummaryStore::instance().lookup(callee_name); @@ -521,7 +522,7 @@ class SummaryWalker { return false; } if (const auto* ce = dyn_cast(stmt)) { - const std::string callee_name = qualifiedCalleeName(ce); + const std::string callee_name = summaryStoreKeyForCall(ce); if (!callee_name.empty()) { auto& store = detect::SummaryStore::instance(); const auto* summary = store.lookup(callee_name); @@ -569,7 +570,7 @@ class SummaryWalker { private: std::optional summarizeCallReturn(const clang::CallExpr* ce, const z3::expr& path) { - const std::string callee_name = qualifiedCalleeName(ce); + const std::string callee_name = summaryStoreKeyForCall(ce); if (callee_name.empty()) return std::nullopt; @@ -656,7 +657,7 @@ std::optional summarizeImpl(const clang::FunctionDecl* fd, params.push_back(p); std::vector exits; - SummaryWalker walker(ctx, env, exits, params, qualifiedFunctionName(fd)); + SummaryWalker walker(ctx, env, exits, params, summaryStoreKey(fd)); z3::expr path = env.ctx().bool_val(true); bool ok = walker.walk(fd->getBody(), path); SoundnessTag tag = env.tag(); @@ -695,7 +696,7 @@ std::optional computeSummaryForDefinition(const clang if (!def) return std::nullopt; - std::string qualified_name = qualifiedFunctionName(def); + std::string qualified_name = summaryStoreKey(def); if (qualified_name.empty()) return std::nullopt; @@ -807,7 +808,7 @@ summarizeLeafFunctionSymbolically(const clang::FunctionDecl* fd, const clang::AS SummaryPreconditionRecorder preconditions(ctx, env, raw_inputs, input_names); env.setObserver(&preconditions); std::vector exits; - SummaryWalker walker(ctx, env, exits, params, qualifiedFunctionName(fd), &preconditions); + SummaryWalker walker(ctx, env, exits, params, summaryStoreKey(fd), &preconditions); z3::expr path = env.ctx().bool_val(true); bool ok = walker.walk(fd->getBody(), path); @@ -899,7 +900,7 @@ summarizeLeafFunctionSymbolically(const clang::FunctionDecl* fd, const clang::AS SummaryMetadataCollector metadata; metadata.TraverseStmt(fd->getBody()); - const std::string caller_name = qualifiedFunctionName(fd); + const std::string caller_name = summaryStoreKey(fd); summary.reads_globals = std::move(metadata.reads_globals); summary.writes_globals = std::move(metadata.writes_globals); bool params_unchanged = can_emit_value_summary; @@ -943,7 +944,7 @@ const symbolic::SymbolicSummary* ensureSymbolicSummary(const clang::FunctionDecl if (!fd) return nullptr; - std::string qualified_name = qualifiedFunctionName(fd); + std::string qualified_name = summaryStoreKey(fd); if (qualified_name.empty()) return nullptr; diff --git a/tests/integration/test_cross_tu_security.cpp b/tests/integration/test_cross_tu_security.cpp index a2c4e82..793c284 100644 --- a/tests/integration/test_cross_tu_security.cpp +++ b/tests/integration/test_cross_tu_security.cpp @@ -1,4 +1,7 @@ +#include +#include #include +#include #include #include @@ -21,6 +24,7 @@ #include "fold/detect/summary_store.hpp" #include "fold/frontend/comp_db.hpp" #include "fold/ir/call_graph.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" namespace { @@ -37,6 +41,28 @@ struct TempDir { ~TempDir() { std::filesystem::remove_all(path); } }; +// SummaryStore key (USR-based) of the function `name` defined in `path`, +// computed from the same file the scan parsed. +std::string summaryKeyIn(const std::filesystem::path& path, const std::string& name) { + std::ifstream in(path); + const std::string code((std::istreambuf_iterator(in)), std::istreambuf_iterator()); + auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, path.string()); + if (!unit) + return {}; + struct Finder : clang::RecursiveASTVisitor { + std::string name; + const clang::FunctionDecl* found = nullptr; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (!found && fd->getNameAsString() == name) + found = fd; + return true; + } + } finder; + finder.name = name; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + return fold::summaryStoreKey(finder.found); +} + void writeFile(const std::filesystem::path& path, const std::string& content) { std::ofstream(path) << content; } @@ -478,8 +504,10 @@ TEST_CASE("symbolic summary priming reaches recursive SCC fixpoint", "[scan][sum auto result = fold::cli::runDetectorsOnShard(*db, opts, {caller.string(), callee.string()}, /*include_clone_clustering=*/false); - const auto* a_summary = fold::detect::SummaryStore::instance().lookup("a"); - const auto* b_summary = fold::detect::SummaryStore::instance().lookup("b"); + const auto* a_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(caller, "a")); + const auto* b_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(callee, "b")); REQUIRE(b_summary != nullptr); REQUIRE(a_summary != nullptr); REQUIRE(!a_summary->param_pre.empty()); @@ -520,10 +548,10 @@ TEST_CASE("symbolic summaries distinguish internal linkage functions by file", (void)fold::cli::runDetectorsOnShard(*db, opts, {unsafe.string(), safe.string()}, /*include_clone_clustering=*/false); - const auto* unsafe_summary = fold::detect::SummaryStore::instance().lookup( - std::string("require_nonzero@") + unsafe.string()); - const auto* safe_summary = fold::detect::SummaryStore::instance().lookup( - std::string("require_nonzero@") + safe.string()); + const auto* unsafe_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(unsafe, "require_nonzero")); + const auto* safe_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(safe, "require_nonzero")); REQUIRE(unsafe_summary != nullptr); REQUIRE(safe_summary != nullptr); diff --git a/tests/unit/meson.build b/tests/unit/meson.build index 86ae3f2..0fe30c2 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -222,6 +222,15 @@ test_scan_coverage = executable( ) test('scan_coverage', test_scan_coverage) +test_summary_key_identity = executable( + 'test_summary_key_identity', + 'test_summary_key_identity.cpp', + dependencies: [fold_core_dep, catch2_dep], + install: false, + build_by_default: false, +) +test('summary_key_identity', test_summary_key_identity) + test_batch_safety_observer = executable( 'test_batch_safety_observer', 'test_batch_safety_observer.cpp', diff --git a/tests/unit/test_summary_key_identity.cpp b/tests/unit/test_summary_key_identity.cpp new file mode 100644 index 0000000..5447813 --- /dev/null +++ b/tests/unit/test_summary_key_identity.cpp @@ -0,0 +1,141 @@ +#include +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/null_deref.hpp" +#include "fold/detect/summary_store.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" +#include "fold/symbolic/summary.hpp" +#include "fold/symbolic/summary_encoder.hpp" + +// Function summaries were stored under the qualified name, which overloads +// share: `take(int*, int)` (dereferences p) and `take(int*, long)` (checks p) +// both mapped to "take", so whichever was summarized first answered for both. +// A caller of the null-checking overload then inherited a nonnull +// precondition it does not have, and vice versa. Summaries are now keyed by +// the declaration's USR. + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::vector definitionsNamed(clang::ASTUnit& unit, + const std::string& name) { + struct Finder : clang::RecursiveASTVisitor { + std::string name; + std::vector found; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (fd->getNameAsString() == name && fd->isThisDeclarationADefinition()) + found.push_back(fd); + return true; + } + } finder; + finder.name = name; + finder.TraverseDecl(unit.getASTContext().getTranslationUnitDecl()); + return finder.found; +} + +bool requiresNonNull(const fold::symbolic::SymbolicSummary* summary, unsigned index) { + if (summary == nullptr) + return false; + const auto it = summary->param_pre.find(index); + if (it == summary->param_pre.end()) + return false; + for (const auto& term : it->second) + if (term.kind == "nonnull") + return true; + return false; +} + +} // namespace + +TEST_CASE("overloads get separate summaries", "[summary-key]") { + fold::detect::SummaryStore::instance().clear(); + auto unit = parse("int take(int* p, int) { return *p; }\n" + "int take(int* p, long) { return p ? *p : 0; }\n"); + REQUIRE(unit); + const auto defs = definitionsNamed(*unit, "take"); + REQUIRE(defs.size() == 2); + const auto& ctx = unit->getASTContext(); + + SECTION("dereferencing overload first") { + CHECK(requiresNonNull(fold::ensureSymbolicSummary(defs[0], ctx), 0)); + CHECK_FALSE(requiresNonNull(fold::ensureSymbolicSummary(defs[1], ctx), 0)); + } + SECTION("null-checking overload first") { + CHECK_FALSE(requiresNonNull(fold::ensureSymbolicSummary(defs[1], ctx), 0)); + CHECK(requiresNonNull(fold::ensureSymbolicSummary(defs[0], ctx), 0)); + } + fold::detect::SummaryStore::instance().clear(); +} + +TEST_CASE("summary keys: identity across redeclarations, not across names", "[summary-key]") { + auto unit = parse("int f(int* p);\n" + "int f(int* p) { return *p; }\n" + "namespace a { int g(int* p) { return *p; } }\n" + "namespace b { int g(int* p) { return p ? *p : 0; } }\n"); + REQUIRE(unit); + struct Finder : clang::RecursiveASTVisitor { + std::vector f_decls; + std::vector g_defs; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (fd->getNameAsString() == "f") + f_decls.push_back(fd); + if (fd->getNameAsString() == "g") + g_defs.push_back(fd); + return true; + } + } finder; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + REQUIRE(finder.f_decls.size() == 2); + REQUIRE(finder.g_defs.size() == 2); + CHECK(fold::summaryStoreKey(finder.f_decls[0]) == fold::summaryStoreKey(finder.f_decls[1])); + CHECK(fold::summaryStoreKey(finder.g_defs[0]) != fold::summaryStoreKey(finder.g_defs[1])); + CHECK_FALSE(fold::summaryStoreKey(finder.f_decls[0]).empty()); + CHECK(fold::summaryStoreKey(nullptr).empty()); +} + +TEST_CASE("null-deref: a cross-TU call uses its own overload's summary", + "[summary-key][null-deref]") { + // TU 1 defines both overloads and summarizes them (the dereferencing one + // last). TU 2 sees only declarations, so its call resolves through the + // store alone, and passes null to the overload that checks. + const std::string defs = "int take(int* p, long) { return p ? *p : 0; }\n" + "int take(int* p, int) { return *p; }\n"; + const std::string caller = "int take(int* p, long);\n" + "int take(int* p, int);\n" + "int caller() { int* q = nullptr; return take(q, 1L); }\n" + "int control() { int* q = nullptr; return take(q, 1); }\n"; + fold::detect::SummaryStore::instance().clear(); + auto defs_unit = parse(defs); + REQUIRE(defs_unit); + for (const auto* fd : definitionsNamed(*defs_unit, "take")) + (void)fold::ensureSymbolicSummary(fd, defs_unit->getASTContext()); + + auto caller_unit = parse(caller); + REQUIRE(caller_unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto findings = fold::detectNullDerefInContext(caller_unit->getASTContext(), b, s); + fold::detect::SummaryStore::instance().clear(); + std::size_t in_caller = 0; + std::size_t in_control = 0; + for (const auto& f : findings) { + if (!f.locations.empty() && f.locations.front().line == 3) + ++in_caller; + if (!f.locations.empty() && f.locations.front().line == 4) + ++in_control; + } + CHECK(in_caller == 0); + // Control: the dereferencing overload's precondition still applies. + CHECK(in_control == 1); +} diff --git a/tests/unit/test_symbolic_summary.cpp b/tests/unit/test_symbolic_summary.cpp index cabf182..b14b3c4 100644 --- a/tests/unit/test_symbolic_summary.cpp +++ b/tests/unit/test_symbolic_summary.cpp @@ -11,6 +11,7 @@ #include "fold/detect/null_deref.hpp" #include "fold/detect/summary_store.hpp" #include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/summary_encoder.hpp" namespace { @@ -37,7 +38,7 @@ void primeLeafSummary(clang::ASTUnit& unit, const std::string& name) { REQUIRE(fd != nullptr); auto summary = fold::summarizeLeafFunctionSymbolically(fd, ctx); REQUIRE(summary); - fold::detect::SummaryStore::instance().store(name, *summary); + fold::detect::SummaryStore::instance().store(fold::summaryStoreKey(fd), *summary); } } // namespace -- 2.52.0 From 5c352b2ee4db6c16f6472a27c59b0e85b2afca7d Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:51:07 -0600 Subject: [PATCH 07/18] fix(solver): fail closed when the portfolio re-check disagrees 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. --- include/fold/symbolic/tactics.hpp | 8 ++++++++ src/detect/div_by_zero.cpp | 2 ++ src/detect/int_overflow.cpp | 2 ++ src/detect/null_deref.cpp | 2 ++ src/symbolic/tactics.cpp | 4 ++++ tests/unit/test_model_validation.cpp | 12 ++++++++++++ 6 files changed, 30 insertions(+) diff --git a/include/fold/symbolic/tactics.hpp b/include/fold/symbolic/tactics.hpp index 11be37c..bb6a39c 100644 --- a/include/fold/symbolic/tactics.hpp +++ b/include/fold/symbolic/tactics.hpp @@ -32,6 +32,14 @@ z3::check_result checkWithAssumptionsProfiled(z3::solver& solver, z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions, unsigned timeout_ms, ::fold::SolverStats& stats); +/// Portfolio answers come from a separate solver; detectors re-check on their +/// own solver to get a model or an unsat core. The answer stands only when the +/// re-check agrees: a re-check that times out or disagrees yields unknown, so a +/// finding is never emitted from a SAT verdict the reporting solver did not +/// reproduce (and has no model for). +[[nodiscard]] z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, + z3::check_result recheck); + /// Check assumptions with an ESCALATING timeout. A query that returns UNKNOWN /// at `base_timeout_ms` is re-checked at 2x, 4x, ... up to a cap, so a query /// that is just barely over budget still resolves (SAT/UNSAT) instead of losing diff --git a/src/detect/div_by_zero.cpp b/src/detect/div_by_zero.cpp index 8ef3b46..ed832af 100644 --- a/src/detect/div_by_zero.cpp +++ b/src/detect/div_by_zero.cpp @@ -208,6 +208,7 @@ class DivByZeroObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = solver_->check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { @@ -254,6 +255,7 @@ class DivByZeroObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = local_s.check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { diff --git a/src/detect/int_overflow.cpp b/src/detect/int_overflow.cpp index 73a692e..5cbf2d6 100644 --- a/src/detect/int_overflow.cpp +++ b/src/detect/int_overflow.cpp @@ -422,6 +422,7 @@ class IntOverflowObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = solver_->check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { @@ -469,6 +470,7 @@ class IntOverflowObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = local_s.check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { diff --git a/src/detect/null_deref.cpp b/src/detect/null_deref.cpp index b75f164..959fb82 100644 --- a/src/detect/null_deref.cpp +++ b/src/detect/null_deref.cpp @@ -287,6 +287,7 @@ class NullDerefObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = solver_->check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { @@ -334,6 +335,7 @@ class NullDerefObserver : public SafetyObserver { if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { auto artifact_t0 = std::chrono::steady_clock::now(); z3::check_result artifact_result = local_s.check(assumptions); + result = symbolic::reconcilePortfolioRecheck(result, artifact_result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); if (artifact_result == z3::unsat) { diff --git a/src/symbolic/tactics.cpp b/src/symbolic/tactics.cpp index 77b3ff9..b1331f6 100644 --- a/src/symbolic/tactics.cpp +++ b/src/symbolic/tactics.cpp @@ -359,6 +359,10 @@ z3::check_result checkAdaptive(z3::solver& solver, const z3::expr_vector& assump } } +z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check_result recheck) { + return portfolio == recheck ? portfolio : z3::unknown; +} + z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions, unsigned timeout_ms, ::fold::SolverStats& stats) { z3::expr query = smt_solver.ctx().bool_val(true); diff --git a/tests/unit/test_model_validation.cpp b/tests/unit/test_model_validation.cpp index baa2461..38160bb 100644 --- a/tests/unit/test_model_validation.cpp +++ b/tests/unit/test_model_validation.cpp @@ -122,3 +122,15 @@ TEST_CASE("portfolio translation accepts Fold theory and rejects unsupported exp CHECK(fold::symbolic::checkWithPortfolio(unsupported_solver, assumptions, 100, stats) == z3::unknown); } + +TEST_CASE("portfolio verdicts stand only when the re-check agrees", "[portfolio][soundness]") { + // The re-check used to be consulted only for its model/core; a SAT + // portfolio verdict whose re-check timed out was still reported as SAT. + using fold::symbolic::reconcilePortfolioRecheck; + CHECK(reconcilePortfolioRecheck(z3::sat, z3::sat) == z3::sat); + CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unsat) == z3::unsat); + CHECK(reconcilePortfolioRecheck(z3::sat, z3::unknown) == z3::unknown); + CHECK(reconcilePortfolioRecheck(z3::unsat, z3::unknown) == z3::unknown); + CHECK(reconcilePortfolioRecheck(z3::sat, z3::unsat) == z3::unknown); + CHECK(reconcilePortfolioRecheck(z3::unsat, z3::sat) == z3::unknown); +} -- 2.52.0 From 8a32f08fd7442325649c7f8ec6e32754b2a76509 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:56:27 -0600 Subject: [PATCH 08/18] fix(int-overflow): render witnesses in the source type's width and sign 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. --- include/fold/detect/z3_model_support.hpp | 27 +++++++++++- src/detect/int_overflow.cpp | 11 ++--- src/detect/meson.build | 1 + src/detect/z3_model_support.cpp | 53 ++++++++++++++++++++++++ tests/unit/test_int_overflow.cpp | 28 +++++++++++++ 5 files changed, 114 insertions(+), 6 deletions(-) create mode 100644 src/detect/z3_model_support.cpp diff --git a/include/fold/detect/z3_model_support.hpp b/include/fold/detect/z3_model_support.hpp index b82a4ba..0e60c09 100644 --- a/include/fold/detect/z3_model_support.hpp +++ b/include/fold/detect/z3_model_support.hpp @@ -14,6 +14,22 @@ namespace fold::detect { +// Source type of an integer variable, for rendering its model value. Symbols +// are 64-bit bitvectors whose low `width` bits carry the source value. +struct SourceIntType { + unsigned width = 0; + bool is_signed = false; +}; +using SourceIntTypes = std::map; + +// Integer-typed parameters and locals of `fn`, by name. A name declared with +// two different integer types is left out rather than guessed. +[[nodiscard]] SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, + const clang::ASTContext& ctx); + +// `raw` truncated to the source width and printed with its signedness. +[[nodiscard]] std::string formatSourceIntValue(uint64_t raw, SourceIntType type); + inline std::string fallbackExprLabel(const clang::Expr* expr, const char* fallback) { if (!expr) return fallback; @@ -84,7 +100,8 @@ inline void collectLeafSymbols(const z3::expr& expr, std::map> -collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned) { +collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned, + const SourceIntTypes* types = nullptr) { std::map symbols; std::unordered_set seen; collectLeafSymbols(expr, symbols, seen); @@ -92,6 +109,14 @@ collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSi std::vector> bindings; bindings.reserve(symbols.size()); for (const auto& [name, symbol] : symbols) { + uint64_t raw = 0; + const auto type = types != nullptr ? types->find(name) : SourceIntTypes::const_iterator{}; + z3::expr value = model.eval(symbol, true); + if (types != nullptr && type != types->end() && value.is_bv() && + value.is_numeral_u64(raw)) { + bindings.emplace_back(name, formatSourceIntValue(raw, type->second)); + continue; + } bindings.emplace_back(name, formatModelValue(model, symbol, preferSigned)); } return bindings; diff --git a/src/detect/int_overflow.cpp b/src/detect/int_overflow.cpp index 5cbf2d6..2e87416 100644 --- a/src/detect/int_overflow.cpp +++ b/src/detect/int_overflow.cpp @@ -610,13 +610,14 @@ class IntOverflowObserver : public SafetyObserver { return fold::mix64(seed, sourceBitWidth); } - static std::pair>> + std::pair>> buildCounterexample(const z3::model& model, const z3::expr& lhs, const z3::expr& rhs, const clang::Expr* lhsExpr, const clang::Expr* rhsExpr, - bool isSourceSigned) { - auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned); - detect::appendUniqueBindings(bindings, - detect::collectModelBindings(model, rhs, isSourceSigned)); + bool isSourceSigned) const { + const auto types = detect::sourceIntTypesOf(current_fn_, ctx_); // source width/sign + auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned, &types); + detect::appendUniqueBindings( + bindings, detect::collectModelBindings(model, rhs, isSourceSigned, &types)); std::string text; if (!bindings.empty()) { text = " (e.g., when " + detect::joinBindings(bindings) + ")"; diff --git a/src/detect/meson.build b/src/detect/meson.build index cfcb77c..92acc0d 100644 --- a/src/detect/meson.build +++ b/src/detect/meson.build @@ -6,6 +6,7 @@ fold_core_sources += files( 'hardcoded_credential.cpp', 'format_string.cpp', 'summary_store.cpp', + 'z3_model_support.cpp', 'incremental_cache.cpp', 'function_enumeration.cpp', 'function_flow.cpp', diff --git a/src/detect/z3_model_support.cpp b/src/detect/z3_model_support.cpp new file mode 100644 index 0000000..e7e0660 --- /dev/null +++ b/src/detect/z3_model_support.cpp @@ -0,0 +1,53 @@ +#include "fold/detect/z3_model_support.hpp" + +#include +#include +#include + +#include +#include + +namespace fold::detect { + +SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, const clang::ASTContext& ctx) { + SourceIntTypes types; + if (fn == nullptr) + return types; + std::set ambiguous; + auto add = [&](const clang::VarDecl* vd) { + const clang::QualType type = vd->getType().getCanonicalType(); + if (!type->isIntegerType() || type->isDependentType() || vd->getName().empty()) + return; + const SourceIntType info{static_cast(ctx.getTypeSize(type)), + type->isSignedIntegerType()}; + const std::string name = vd->getNameAsString(); + const auto [it, inserted] = types.emplace(name, info); + if (!inserted && (it->second.width != info.width || it->second.is_signed != info.is_signed)) + ambiguous.insert(name); + }; + for (const auto* param : fn->parameters()) + add(param); + struct Visitor : clang::RecursiveASTVisitor { + std::function add; + bool VisitVarDecl(clang::VarDecl* vd) { + add(vd); + return true; + } + } visitor; + visitor.add = add; + if (fn->hasBody()) + visitor.TraverseStmt(fn->getBody()); + for (const auto& name : ambiguous) + types.erase(name); + return types; +} + +std::string formatSourceIntValue(uint64_t raw, SourceIntType type) { + if (type.width == 0 || type.width >= 64) + return type.is_signed ? std::to_string(static_cast(raw)) : std::to_string(raw); + const uint64_t truncated = raw & ((uint64_t{1} << type.width) - 1); + return type.is_signed ? formatSignedBitVector(truncated, type.width) + : std::to_string(truncated); +} + +} // namespace fold::detect diff --git a/tests/unit/test_int_overflow.cpp b/tests/unit/test_int_overflow.cpp index c0f7d88..88174a1 100644 --- a/tests/unit/test_int_overflow.cpp +++ b/tests/unit/test_int_overflow.cpp @@ -9,6 +9,7 @@ #include "fold/detect/cross_tu_cache.hpp" #include "fold/detect/int_overflow.hpp" +#include "fold/detect/z3_model_support.hpp" #include "fold/report/finding.hpp" #include "fold/symbolic/budget.hpp" @@ -669,3 +670,30 @@ TEST_CASE("int-overflow: CFString size output contract proves length-1 safe", std::fprintf(stderr, "CFSTRING-POS findings=%zu\n", findings.size()); REQUIRE(findings.empty()); } + +TEST_CASE("int-overflow: witnesses use the source type's width and signedness", + "[int_overflow][witness]") { + // Symbols are 64-bit; only the low 32 bits carry an `int`. Witnesses were + // printed from the whole bitvector, e.g. a=2147483648 or + // a=-9223372034707292160 for `int a`. + auto r = run("int sum(int a, int b) { int x = a + b; x += a; return x; }\n"); + REQUIRE_FALSE(r.findings.empty()); + for (const auto& f : r.findings) { + for (const auto& [name, value] : f.evidence.counterexample) { + const long long v = std::stoll(value); + CHECK(v >= -2147483648LL); + CHECK(v <= 2147483647LL); + } + } +} + +TEST_CASE("formatSourceIntValue truncates and signs", "[int_overflow][witness]") { + using fold::detect::formatSourceIntValue; + CHECK(formatSourceIntValue(0x80000000ULL, {32, true}) == "-2147483648"); + CHECK(formatSourceIntValue(0x8000000080000000ULL, {32, true}) == "-2147483648"); + CHECK(formatSourceIntValue(0xBFFFFFFFULL, {32, true}) == "-1073741825"); + CHECK(formatSourceIntValue(0x1FFFFFFFFULL, {32, false}) == "4294967295"); + CHECK(formatSourceIntValue(7, {32, true}) == "7"); + CHECK(formatSourceIntValue(0xFFFFFFFFFFFFFFFFULL, {64, true}) == "-1"); + CHECK(formatSourceIntValue(0xFFULL, {8, true}) == "-1"); +} -- 2.52.0 From f0fe006d6b4eb675342a4c0842eee1d3197740f8 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:57:32 -0600 Subject: [PATCH 09/18] fix(docs,tests): correct the pre-push hook claim, a dead link, MCP cleanup 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. --- README.md | 3 +-- docs/research/prior-art.md | 2 +- tests/integration/test_mcp_stdio.cpp | 8 +++++++- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index b79aeb2..1b8ea51 100644 --- a/README.md +++ b/README.md @@ -13,8 +13,7 @@ Requires system-installed LLVM/Clang 18+ and `libz3` development headers; Conan handles the rest (spdlog, CLI11, nlohmann_json, sqlite3, Catch2). **See [BUILD.md](BUILD.md) for per-platform apt/brew install lines and a Docker validation harness.** Setup also enables -the tracked lint pre-commit and OpenGrep pre-push hooks; install -[OpenGrep](https://opengrep.dev/) before pushing. +the tracked lint pre-commit hook (`.githooks/pre-commit`). ## Usage diff --git a/docs/research/prior-art.md b/docs/research/prior-art.md index 9dcbd65..2c4fc63 100644 --- a/docs/research/prior-art.md +++ b/docs/research/prior-art.md @@ -1,6 +1,6 @@ # Prior Art (condensed) -Key papers grounding fold's design. Full annotations in `prior-art-full.md`. +Key papers grounding fold's design. ## Buffer overflow - **Xu et al. (2020)** *ELAID.* doi:10.1186/s42400-020-00058-2 — interprocedural call graph + SMT on Juliet sinks. diff --git a/tests/integration/test_mcp_stdio.cpp b/tests/integration/test_mcp_stdio.cpp index 75de10e..922fd30 100644 --- a/tests/integration/test_mcp_stdio.cpp +++ b/tests/integration/test_mcp_stdio.cpp @@ -57,13 +57,19 @@ struct TempDir { std::filesystem::path path; TempDir() + // Must stay under the working directory: the MCP server rejects paths + // outside its workspace root. : path(std::filesystem::current_path() / (".fold-mcp-test-" + std::to_string(std::chrono::steady_clock::now().time_since_epoch().count()))) { std::filesystem::create_directories(path); } - ~TempDir() { std::filesystem::remove_all(path); } + // Non-throwing: a destructor that throws during unwinding terminates. + ~TempDir() { + std::error_code ec; + std::filesystem::remove_all(path, ec); + } }; void writeFile(const std::filesystem::path& path, const std::string& content) { -- 2.52.0 From c785a6aceef7cfeb403ea7f349649673dc09628d Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 20:58:26 -0600 Subject: [PATCH 10/18] docs(positioning): drop claims the code and evidence do not support 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. --- docs/positioning.md | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/docs/positioning.md b/docs/positioning.md index 847db83..2ad477e 100644 --- a/docs/positioning.md +++ b/docs/positioning.md @@ -11,20 +11,23 @@ sink with a Z3-produced witness, then optionally runs that witness through libFuzzer + ASan to promote findings from "the solver says SAT" to "we observed the crash." -Most static analyzers stop at "the solver says SAT." Most fuzzers don't -know what they're aiming at. fold links the two so the report says +Solver-backed analyzers (for example the Clang Static Analyzer's +optional Z3 refutation) use SMT to prune infeasible paths, but their +reports stop at a static verdict. Most fuzzers don't know what they're +aiming at. fold links the two so the report says which findings are confirmed observable failures, not just satisfiable path predicates. ## Confidence tiers fold reports -Findings are not all equal. fold reports four confidence tiers: +Findings are not all equal. fold reports five confidence tiers: | Tier | Source | Example | |------------------|--------------------------------------------------------------|-------------------------------------------------| | `Syntactic` | AST pattern match, no solver | "function name matches `strcpy`" | | `Heuristic` | Solver gave up or path was over-approximated | "interval analysis can't bound `len`" | -| `Proved` | Z3 returned SAT on (path ∧ hazard); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" | +| `Latent` | Proved in the callee, modulo a caller obligation not discharged | "`p` is dereferenced; no caller shown to pass null" | +| `Proved` | Z3 returned SAT on (path ∧ hazard) over an exact bounded model (no over-approximated operation on the path; see `docs/research/soundness.md`); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" | | `ConcreteWitness`| Z3 model was packaged as a seed and ASan observed the crash | "libFuzzer crashed on `seed_8f3c.bin`" | The ordering is explicit in `include/fold/report/finding.hpp::confidenceRank()` @@ -100,7 +103,7 @@ source, closed methodology, opaque false-positive rates. **fold differs by:** open source (GPL-3.0 when stable), open methodology (`docs/research/soundness.md`), and a closed loop with -libFuzzer that no commercial vendor currently ships. fold is also +libFuzzer in the same report. fold is also substantially less mature on the heuristic-refinement side — Coverity has had two decades of FP-tuning effort that fold has not. @@ -133,15 +136,16 @@ is already your CI surface. ### Bounded model checkers (CBMC, ESBMC) Unroll loops to a configurable depth, encode the bounded program -as an SMT formula, ask Z3 / MathSAT whether any sink is reachable. +as a SAT/SMT formula (CBMC's default back end is a SAT solver) and +ask whether any assertion can fail. Sound for the unrolling depth chosen; report concrete counterexamples; usable as software-verification competitors -(SV-COMP). Slow on large codebases — full-program BMC scales -poorly past a few thousand lines. +(SV-COMP). Whole-program BMC cost grows with program size and +unwinding depth. **fold differs by:** scope and product shape. CBMC verifies one -property of one bounded program; fold scans a 100k-LOC codebase -in minutes, flagging per-sink findings with per-sink witnesses, +property of one bounded program; fold runs per-sink, mostly +intraprocedural queries with a small loop unroll (5 by default), trading verification rigor for breadth. They are complementary: a fold finding worth deep verification can be re-checked under CBMC. @@ -227,8 +231,9 @@ for protocol parsers and other constrained-input APIs. ## Where fold's closed scan→fuzz loop matters -The Phase 1+2 work in M31 closed a gap that no other open-source -analyzer covers: every SAT finding is automatically packaged as a +The Phase 1+2 work in M31 closes the loop inside one tool (directed +fuzzers such as AFLGo and hybrid tools such as SAVIOR explore related +ground; see `docs/research/prior-art.md`): every SAT finding is automatically packaged as a libFuzzer seed, run under ASan, and (if a crash is observed) promoted from `Proved` to `ConcreteWitness` in the same JSON report. The user sees one Finding with `confidence: -- 2.52.0 From 2945e59bc28f76239e78131191f547567f2111e0 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:11:54 -0600 Subject: [PATCH 11/18] docs: trim the README and move the performance roadmap to docs/ 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. --- BUILD.md | 3 + README.md | 95 ++++++++++++++------------------ docs/architecture/performance.md | 29 ++++++++++ 3 files changed, 72 insertions(+), 55 deletions(-) create mode 100644 docs/architecture/performance.md diff --git a/BUILD.md b/BUILD.md index 0d66bcc..1ce15c0 100644 --- a/BUILD.md +++ b/BUILD.md @@ -8,6 +8,9 @@ # tests: meson test -C build/release ``` +`setup.sh` also enables the tracked lint pre-commit hook +(`.githooks/pre-commit`). + Linux users without root can validate against a clean container: ```sh diff --git a/README.md b/README.md index 1b8ea51..30ff28b 100644 --- a/README.md +++ b/README.md @@ -1,72 +1,57 @@ # fold -Bounded symbolic SAST for C++ — clone detection, dead-branch analysis, -and security vulnerability scanning via Clang LibTooling and Z3. +Bounded symbolic static analysis for C++: dead-branch and hazard detection +(null dereference, division by zero, integer overflow, out-of-bounds, and more), +clone and equivalence detection, and taint tracking, built on Clang LibTooling +and the Z3 solver. Rust (HIR), Swift and binary scan modes also exist; the Rust +detectors are heuristic today. -## Build +Every finding carries a confidence tier that says how it was established: + +| Tier | Meaning | +| --- | --- | +| `concrete-witness` | A fuzzer ran the solver's witness under a sanitizer and produced a correlated crash. | +| `proved` | An exact bounded model proved it: SAT for a hazard witness, or UNSAT for a negated invariant. | +| `latent` | Proved inside the function, but only reachable if a caller supplies a value the callee never guards. | +| `heuristic` | Some part of the model was over-approximated. | +| `syntactic` | An AST pattern or hash match only. | + +"Bounded" is literal: loops are unrolled to a fixed depth, and a condition that +depends on a loop's exit is never reported as proved. The contract behind each +tier is in [docs/research/soundness.md](docs/research/soundness.md). + +## Quick start ```sh -./setup.sh release -``` - -Requires system-installed LLVM/Clang 18+ and `libz3` development -headers; Conan handles the rest (spdlog, CLI11, nlohmann_json, -sqlite3, Catch2). **See [BUILD.md](BUILD.md) for per-platform -apt/brew install lines and a Docker validation harness.** Setup also enables -the tracked lint pre-commit hook (`.githooks/pre-commit`). - -## Usage - -``` +./setup.sh release # needs LLVM/Clang 18+ and libz3 headers; Conan handles the rest fold scan --compile-db compile_commands.json \ --detectors null-deref --detectors div-by-zero \ --format sarif --output findings.sarif -``` - -Detectors: `clone`, `equiv`, `class-dup`, `dead`, `null-deref`, -`div-by-zero`, `int-overflow`, `oob`, `int-truncation`, `sign-conversion`, -`taint-track`. - -Output formats: `sarif`, versioned native `findings-json`, and `markdown`. -`json` remains a deprecated compatibility alias for SARIF. Query existing Fold -reports without scanning raw source text: - -```sh fold grep "null pointer" findings.sarif --field message --ignore-case ``` -See `docs/USAGE.md` for the full CLI and MCP/LSP reference, and -`docs/compatibility.md` for deprecated-name migrations and removal criteria. +Per-platform install lines and a Docker validation harness are in +[BUILD.md](BUILD.md). -## Research docs +Output formats are `sarif`, versioned `findings-json`, and `markdown`. Both +machine formats record which translation units were analysed. A scan exits `0` +with no findings, `1` with any unsuppressed finding, and `2` when a report could +not be written or any translation unit was not analysed (compile errors, +frontend failure, crash, timeout): no findings from an incomplete scan is not +evidence of no bugs. -`docs/research/` — architecture, benchmarks, prior art, frontier roadmap, -soundness proofs, and audit artifacts. +## Documentation -## Performance architecture - -Optimization is measurement-first and gate-guarded. Every candidate -change runs through the manifest-driven evaluation harness -(`tests/benchmarks/projects/*.json`), which enforces finding-fingerprint -stability, gold precision/recall (`bench/gold/`), reviewed dispositions, and -wall/RSS regression baselines. A full ledger of measured wins and closed -hypotheses lives in -[`docs/research/optimization-loop-2026-07-30.md`](docs/research/optimization-loop-2026-07-30.md). - -The one structural work on the roadmap is **single-pass graph building**. -Today a source scan parses each translation unit twice — once to build the -project call graph, once to run detectors — because the detector pass consumes -the graph (cross-TU candidate expansion and summary priming). The planned -change collapses these into one parse per TU that produces graph contributions -and runs the intra-TU detectors in the same pass, retaining only light per-TU -edge/signature records, and runs the cross-TU-dependent closure after every TU. -This is deliberately chosen over precompiled-header/module caching to -**preserve portability**: it introduces no clang-version-locked serialized -artifacts, no SDK/toolchain-locked module cache, and no `-std`/`-I`/`-D` -flag-matching bug surface — every machine that consumes a -`compile_commands.json` today keeps working unchanged. Correctness parity for -the deferred closure is policed by the existing finding-fingerprint and gold -gates. +- [Usage](docs/USAGE.md): the full CLI (scan modes, scopes, confirmation, + fuzzing), every detector with its CWE and method, MCP/LSP, and project + evaluation. +- [MCP tools](docs/mcp-tools.md) and [compatibility](docs/compatibility.md) + (deprecated names and removal criteria). +- [Positioning](docs/positioning.md) and [prior art](docs/research/prior-art.md): + how fold relates to other analyzers. +- [Performance](docs/architecture/performance.md): the evaluation gates and the + single-pass graph-building plan. +- [Architecture](docs/architecture/) and [research](docs/research/) notes. ## License diff --git a/docs/architecture/performance.md b/docs/architecture/performance.md new file mode 100644 index 0000000..48e0544 --- /dev/null +++ b/docs/architecture/performance.md @@ -0,0 +1,29 @@ +# Performance + +Optimization is measurement-first and gate-guarded. Every candidate change runs +through the manifest-driven evaluation harness +(`tests/benchmarks/projects/*.json`), which enforces finding-fingerprint +stability, reviewed dispositions, wall-time and RSS regression baselines, and a +gold set (`bench/gold/`). The gold set was derived from fold's own reviewed +output and is matched by detector kind and file, so it catches drift; it is not +an independent precision or recall measure. A ledger of measured wins and +closed hypotheses is in +[the optimization loop](../research/optimization-loop-2026-07-30.md). + +## Single-pass graph building + +The one structural item on the roadmap is single-pass graph building. A source +scan currently parses each translation unit twice: once to build the project +call graph, and once to run detectors, because the detector pass consumes the +graph (cross-TU candidate expansion and summary priming). The planned change +collapses these into one parse per TU that produces graph contributions and runs +the intra-TU detectors in the same pass, keeping only light per-TU edge and +signature records, then runs the cross-TU-dependent closure after every TU. See +[the design](../research/single-pass-graph-design.md). + +This is chosen over precompiled-header or module caching to preserve +portability: it introduces no Clang-version-locked serialized artifacts, no +SDK- or toolchain-locked module cache, and no `-std`/`-I`/`-D` flag-matching +bug surface, so every machine that consumes a `compile_commands.json` today +keeps working. Correctness parity for the deferred closure is policed by the +existing finding-fingerprint and gold gates. -- 2.52.0 From 9e37fd0387f944cc8c3110f05601d6626a30a4fa Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:26:27 -0600 Subject: [PATCH 12/18] fix(detect): model continue exits and memory stores in truncated loops 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. --- include/fold/detect/loop_havoc.hpp | 13 ++- include/fold/symbolic/encoder.hpp | 9 ++ src/detect/always_condition.cpp | 2 +- src/detect/dead_branch.cpp | 2 +- src/detect/loop_havoc.cpp | 125 ++++++++++++++++++++++-- src/detect/unreachable.cpp | 2 +- tests/unit/test_loop_exit_soundness.cpp | 47 +++++++++ 7 files changed, 186 insertions(+), 14 deletions(-) diff --git a/include/fold/detect/loop_havoc.hpp b/include/fold/detect/loop_havoc.hpp index f102771..484f73c 100644 --- a/include/fold/detect/loop_havoc.hpp +++ b/include/fold/detect/loop_havoc.hpp @@ -26,9 +26,9 @@ void appendAssignedVars(std::vector& vars, // access-path facts: after this, nothing about their post-loop values is known. void havocAssignedVars(SymbolicEnv& env, const std::vector& vars); -// A `break` or `goto` in `body` that leaves the loop (a `break` inside a nested -// loop or switch does not). Such an exit carries state the unroll never -// follows. +// A `break`, `continue` or `goto` in `body` that leaves the loop's iteration +// (a `break` inside a nested loop or switch, or a `continue` inside a nested +// loop, does not). Such an exit carries state the unroll never follows. [[nodiscard]] bool containsLoopEscape(const clang::Stmt* body); // Whether a bounded unroll saw every way out of a loop. @@ -58,9 +58,16 @@ class LoopUnrollExits { // The unroll left the loop along its only exit. [[nodiscard]] bool exact() const { return exact_ && exited_; } + // Havoc the loop's post-state: assigned variables become unknown, and when + // the body stores through an array element, member or pointer, the env is + // marked over-approximated because that state is not havocked. + void havoc(SymbolicEnv& env, const std::vector& vars) const; + private: bool exact_ = true; bool exited_ = false; + std::vector memory_bases_; + bool unknown_memory_write_ = false; }; } // namespace fold::detect diff --git a/include/fold/symbolic/encoder.hpp b/include/fold/symbolic/encoder.hpp index 4151fd4..067b05a 100644 --- a/include/fold/symbolic/encoder.hpp +++ b/include/fold/symbolic/encoder.hpp @@ -131,6 +131,15 @@ class SymbolicEnv { void createHeapArray(const z3::expr& ptr, unsigned count, unsigned elem_size); std::optional getHeapArray(const z3::expr& ptr) const; void updateHeapArray(const z3::expr& ptr, const z3::expr& new_array); + // Replace every tracked heap array with a fresh array of the same sort: a + // store through an unknown pointer may have written any of them. + void havocHeapArrays() { + static unsigned counter = 0; + for (auto& [_, info] : heap_arrays_) { + const std::string name = "heap_array_havoc_" + std::to_string(counter++); + info.array = ctx_->constant(name.c_str(), info.array.get_sort()); + } + } void removeHeapArray(const z3::expr& ptr); std::optional tryGetMember(const std::string& key) const { diff --git a/src/detect/always_condition.cpp b/src/detect/always_condition.cpp index 65fdf1c..0aa55b9 100644 --- a/src/detect/always_condition.cpp +++ b/src/detect/always_condition.cpp @@ -330,7 +330,7 @@ class AlwaysConditionWalker { // is "the loop ran some prefix of iterations": keeping it would prove // post-loop conditions from a trip count the program need not take. if (opaque_loop || !exits.exact()) { - havocAssignedVars(env, assigned); + exits.havoc(env, assigned); env.restorePath(entry_path); } return true; diff --git a/src/detect/dead_branch.cpp b/src/detect/dead_branch.cpp index 7e6c216..605fd49 100644 --- a/src/detect/dead_branch.cpp +++ b/src/detect/dead_branch.cpp @@ -354,7 +354,7 @@ class BodyWalker { // is "the loop ran some prefix of iterations": keeping it would prove // post-loop conditions from a trip count the program need not take. if (opaque_loop || !exits.exact()) { - havocAssignedVars(env, assigned); + exits.havoc(env, assigned); path = entry_path; } return true; diff --git a/src/detect/loop_havoc.cpp b/src/detect/loop_havoc.cpp index 31fa7ca..ae8ec77 100644 --- a/src/detect/loop_havoc.cpp +++ b/src/detect/loop_havoc.cpp @@ -82,32 +82,141 @@ void havocAssignedVars(SymbolicEnv& env, const std::vector(stmt) || clang::isa(stmt)) return true; if (clang::isa(stmt)) return breakable_depth == 0; - const bool breakable = clang::isa(stmt) || clang::isa(stmt) || - clang::isa(stmt) || - clang::isa(stmt) || - clang::isa(stmt); + // The walkers drop an arm that ends in `continue` (it always leaves the + // iteration), so the iterations that took it are never modeled. + if (clang::isa(stmt)) + return loop_depth == 0; + const bool loop = clang::isa(stmt) || clang::isa(stmt) || + clang::isa(stmt) || clang::isa(stmt); + const bool breakable = loop || clang::isa(stmt); for (const clang::Stmt* child : stmt->children()) { - if (escapes(child, breakable_depth + (breakable ? 1 : 0))) + if (escapes(child, breakable_depth + (breakable ? 1 : 0), loop_depth + (loop ? 1 : 0))) return true; } return false; } +// Stores that do not go through a plain variable: an array element, a member, +// or a dereferenced pointer. Havocking assigned variables does not reach that +// state. When the store's base is a named variable (`buf[i] = ...`, +// `s.f = ...`), that variable is reported so its whole value can be havocked; +// a store through an unknown pointer is only flagged. +struct MemoryWrites { + std::vector bases; + bool unknown_target = false; +}; + +MemoryWrites collectMemoryWrites(const clang::Stmt* stmt) { + struct Visitor : clang::RecursiveASTVisitor { + MemoryWrites writes; + std::unordered_set seen; + + void record(const clang::Expr* target) { + target = target->IgnoreParenImpCasts(); + const clang::Expr* base = nullptr; + if (const auto* sub = clang::dyn_cast(target)) + base = sub->getBase(); + else if (const auto* mem = clang::dyn_cast(target)) + base = mem->isArrow() ? nullptr : mem->getBase(); + else if (const auto* un = clang::dyn_cast(target); + un && un->getOpcode() == clang::UO_Deref) { + writes.unknown_target = true; + return; + } else if (const auto* arrow = clang::dyn_cast(target); + arrow && arrow->isArrow()) { + writes.unknown_target = true; + return; + } else { + return; + } + if (!base) { + writes.unknown_target = true; + return; + } + // Walk nested subscripts/members (`m[i][j]`, `a.b.c`) to the variable. + for (;;) { + base = base->IgnoreParenImpCasts(); + if (const auto* sub = clang::dyn_cast(base)) { + base = sub->getBase(); + continue; + } + if (const auto* mem = clang::dyn_cast(base); + mem && !mem->isArrow()) { + base = mem->getBase(); + continue; + } + break; + } + const auto* dre = clang::dyn_cast(base); + const auto* vd = dre ? clang::dyn_cast(dre->getDecl()) : nullptr; + // Subscripting a pointer variable writes through it, not into it. + if (!vd || vd->getType()->isPointerType()) { + writes.unknown_target = true; + return; + } + vd = vd->getCanonicalDecl(); + if (seen.insert(vd).second) + writes.bases.push_back(vd); + } + bool VisitBinaryOperator(clang::BinaryOperator* op) { + if (op && op->isAssignmentOp()) + record(op->getLHS()); + return true; + } + bool VisitUnaryOperator(clang::UnaryOperator* op) { + if (op && op->isIncrementDecrementOp()) + record(op->getSubExpr()); + return true; + } + } visitor; + if (stmt) + visitor.TraverseStmt(const_cast(stmt)); + return visitor.writes; +} + } // namespace -bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0); } +bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0, 0); } LoopUnrollExits::LoopUnrollExits(const clang::Stmt* body) { if (containsLoopEscape(body)) exact_ = false; + auto writes = collectMemoryWrites(body); + memory_bases_ = std::move(writes.bases); + unknown_memory_write_ = writes.unknown_target; +} + +void LoopUnrollExits::havoc(SymbolicEnv& env, + const std::vector& vars) const { + havocAssignedVars(env, vars); + // Array element and member stores from the truncated unroll would survive + // the scalar havoc: replace each written aggregate with a fresh value of + // its sort. + static unsigned counter = 0; + auto fresh = [&](const z3::sort& sort) { + const std::string name = "loop_memory_havoc_" + std::to_string(counter++); + return env.ctx().constant(name.c_str(), sort); + }; + for (const clang::VarDecl* vd : memory_bases_) { + if (auto array = env.getArray(vd)) + env.updateArray(vd, fresh(array->array.get_sort())); + else if (auto current = env.tryGet(vd)) + env.replace(vd, fresh(current->get_sort())); + } + // A store through a pointer may have written any tracked heap array. + if (unknown_memory_write_) { + env.havocHeapArrays(); + env.markOverApproximated("loop-truncated-memory-write"); + } } bool LoopUnrollExits::guard(bool may_continue, bool may_exit) { diff --git a/src/detect/unreachable.cpp b/src/detect/unreachable.cpp index aad306b..5e3f428 100644 --- a/src/detect/unreachable.cpp +++ b/src/detect/unreachable.cpp @@ -274,7 +274,7 @@ class UnreachableBodyWalker { } // The same loop-exit soundness rule as dead-branch / always-condition. if (!exits.exact()) { - detect::havocAssignedVars(env, assigned); + exits.havoc(env, assigned); path = entry_path; } return true; diff --git a/tests/unit/test_loop_exit_soundness.cpp b/tests/unit/test_loop_exit_soundness.cpp index c26cd49..744a80c 100644 --- a/tests/unit/test_loop_exit_soundness.cpp +++ b/tests/unit/test_loop_exit_soundness.cpp @@ -177,3 +177,50 @@ TEST_CASE("loop exits: exact only when the unroll leaves along the only exit", " CHECK_FALSE(stopped.exact()); } } + +// Review finding: a `continue` arm is dropped by the walkers (the arm always +// exits the iteration), so iterations that took it are not modeled even when +// the guard sequence is exact. `x == 2` holds only when y == 0. +const std::string kContinueLoop = + "int c(int y) { int x = 0; for (int i = 0; i < 2; i++) { if (y) continue; x++; }" + " if (x == 2) return 1; return 0; }\n"; + +TEST_CASE("a loop with continue is not treated as an exact unroll", "[loop][continue]") { + CHECK(proved(runAlways(kContinueLoop)) == 0); + CHECK(proved(runDead(kContinueLoop)) == 0); + CHECK(proved(runUnreachable(kContinueLoop)) == 0); +} + +// Review finding: a truncated unroll havocs scalar variables but kept array +// element writes from the partial unroll. With n == 0, buf[0] is never set. +const std::string kArrayWriteLoop = "int w(unsigned n) { int buf[4] = {0, 0, 0, 0};" + " for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;" + " if (buf[0] == 1) return 1; return 0; }\n"; + +// The same through a pointer: the store may have reached any heap array. +const std::string kPointerWriteLoop = + "#include \n" + "int pw(unsigned n) { int* buf = static_cast(std::calloc(4, sizeof(int)));" + " if (!buf) return 0;" + " for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;" + " int r = buf[0] == 1 ? 1 : 0; std::free(buf); return r; }\n"; + +TEST_CASE("array writes in a truncated loop do not survive into proofs", "[loop][memory]") { + CHECK(proved(runAlways(kArrayWriteLoop)) == 0); + CHECK(proved(runDead(kArrayWriteLoop)) == 0); + CHECK(proved(runUnreachable(kArrayWriteLoop)) == 0); + CHECK(proved(runAlways(kPointerWriteLoop)) == 0); + CHECK(proved(runDead(kPointerWriteLoop)) == 0); +} + +// Review finding: unreachable omitted the opaque-loop rule. A call can change +// the loop variable through a pointer, which assigned-variable collection +// does not see. +const std::string kOpaqueCallLoop = "void advance(int* p);\n" + "int u() { int i = 0; while (i < 3) { advance(&i); i++; }" + " if (i != 3) { int k = i * 2; return k; } return 0; }\n"; + +TEST_CASE("unreachable havocs loops that contain calls", "[unreachable][loop][opaque]") { + CHECK(proved(runUnreachable(kOpaqueCallLoop)) == 0); + CHECK(proved(runDead(kOpaqueCallLoop)) == 0); +} -- 2.52.0 From 964769cdf8be4317d60359bfba2e0675c7d0dba9 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:29:22 -0600 Subject: [PATCH 13/18] fix(oob): require an exact encoding before a constant-index OOB is Proved 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). --- src/detect/oob_access.cpp | 9 ++++--- .../unit/test_proved_requires_exact_model.cpp | 26 +++++++++++++++++++ 2 files changed, 32 insertions(+), 3 deletions(-) diff --git a/src/detect/oob_access.cpp b/src/detect/oob_access.cpp index c8288d4..4ae28a9 100644 --- a/src/detect/oob_access.cpp +++ b/src/detect/oob_access.cpp @@ -352,7 +352,8 @@ class OOBObserver : public SafetyObserver { if (result == z3::sat) { ++stats_.sat; auto bindings = detect::collectModelBindings(m, idx64, false); - emit(idx64, known_len, loc, idx_expr, base_var, std::move(bindings)); + emit(idx64, known_len, loc, exactEncoding(env), idx_expr, base_var, + std::move(bindings)); // M31 R3-oob: fuzz witness with captured model populated. const std::string id = std::string("oob-access:") + loc.file + ":" + std::to_string(loc.line) + ":" + std::to_string(loc.column); @@ -762,13 +763,15 @@ class OOBObserver : public SafetyObserver { out_.push_back(std::move(f)); } - void emit(const z3::expr& idx, int known_len, const ir::SourceLoc& loc, + void emit(const z3::expr& idx, int known_len, const ir::SourceLoc& loc, bool exact_model, const clang::Expr* idx_expr = nullptr, const clang::VarDecl* base_var = nullptr, std::vector> model_bindings = {}) { Finding f; f.kind = FindingKind::OOBAccess; + // A constant index proves the access out of bounds only when the path + // that reaches it was encoded exactly (docs/research/soundness.md). const bool is_const = idx.is_numeral(); - f.confidence = is_const ? Confidence::Proved : Confidence::Heuristic; + f.confidence = is_const && exact_model ? Confidence::Proved : Confidence::Heuristic; Location l = locationFromSloc(loc); f.locations.push_back(std::move(l)); f.id = std::string("oob-access:") + f.locations.front().file + ":" + diff --git a/tests/unit/test_proved_requires_exact_model.cpp b/tests/unit/test_proved_requires_exact_model.cpp index 54cefc3..326ae52 100644 --- a/tests/unit/test_proved_requires_exact_model.cpp +++ b/tests/unit/test_proved_requires_exact_model.cpp @@ -161,3 +161,29 @@ TEST_CASE("type-trait constants are exact for complete types only", "[proved-con /*c_mode=*/true) .has_value()); } + +TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding", + "[proved-contract][oob]") { + auto oobConfidence = [](const std::string& code) -> std::optional { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) + if (f.id.rfind("oob-access:", 0) == 0) + return f.confidence; + return std::nullopt; + }; + SECTION("exact: stays Proved (control)") { + const auto c = oobConfidence("int f() { int a[4] = {0}; return a[4]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Proved); + } + SECTION("an over-approximated operation on the path: Heuristic") { + const auto c = oobConfidence("extern int opaque(int);\n" + "int f(int k) { int a[4] = {0}; int n = opaque(k);" + " if (n > 2) return a[4]; return 0; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); + } +} -- 2.52.0 From 29a292c6d57adfd80c8e3a32e4604d90d25c08f2 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:32:16 -0600 Subject: [PATCH 14/18] fix(oob,uaf): re-check portfolio verdicts on the reporting solver 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). --- include/fold/symbolic/tactics.hpp | 7 +++++ src/detect/oob_access.cpp | 28 +++++++------------ src/detect/use_after_free.cpp | 4 +++ src/symbolic/tactics.cpp | 11 ++++++++ .../unit/test_proved_requires_exact_model.cpp | 22 +++++++++++++++ 5 files changed, 54 insertions(+), 18 deletions(-) diff --git a/include/fold/symbolic/tactics.hpp b/include/fold/symbolic/tactics.hpp index bb6a39c..52944b1 100644 --- a/include/fold/symbolic/tactics.hpp +++ b/include/fold/symbolic/tactics.hpp @@ -40,6 +40,13 @@ z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vecto [[nodiscard]] z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check_result recheck); +/// Re-checks a decided portfolio verdict on `solver`, the reporting solver, so +/// it holds the model or unsat core, and reconciles the two answers. Unknown +/// stays unknown without a re-check. +[[nodiscard]] z3::check_result recheckPortfolioVerdict(z3::solver& solver, + const z3::expr_vector& assumptions, + z3::check_result portfolio); + /// Check assumptions with an ESCALATING timeout. A query that returns UNKNOWN /// at `base_timeout_ms` is re-checked at 2x, 4x, ... up to a cap, so a query /// that is just barely over budget still resolves (SAT/UNSAT) instead of losing diff --git a/src/detect/oob_access.cpp b/src/detect/oob_access.cpp index 4ae28a9..3a7344a 100644 --- a/src/detect/oob_access.cpp +++ b/src/detect/oob_access.cpp @@ -286,6 +286,8 @@ class OOBObserver : public SafetyObserver { static_cast(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(*solver_, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -324,6 +326,8 @@ class OOBObserver : public SafetyObserver { static_cast(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(local_s, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(local_s, assumptions, result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -504,20 +508,14 @@ class OOBObserver : public SafetyObserver { stats_) : symbolic::checkAdaptive(*solver_, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { stats_.accumulate(solver_->statistics(), result); } - if (budget_.portfolio && result == z3::unsat) { - auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = solver_->check(assumptions); - stats_.elapsed += std::chrono::duration_cast( - std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard, detector_name); - } - } else if (result == z3::unsat) { + if (result == z3::unsat) { rememberUnsatCore(*solver_, path, hazard, detector_name); } } else { @@ -534,20 +532,14 @@ class OOBObserver : public SafetyObserver { s, assumptions, static_cast(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(s, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(s, assumptions, result); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { stats_.accumulate(s.statistics(), result); } - if (budget_.portfolio && result == z3::unsat) { - auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = s.check(assumptions); - stats_.elapsed += std::chrono::duration_cast( - std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(s, path, unsafe, detector_name); - } - } else if (result == z3::unsat) { + if (result == z3::unsat) { rememberUnsatCore(s, path, unsafe, detector_name); } } diff --git a/src/detect/use_after_free.cpp b/src/detect/use_after_free.cpp index 41d20d8..73686a1 100644 --- a/src/detect/use_after_free.cpp +++ b/src/detect/use_after_free.cpp @@ -480,6 +480,8 @@ class UseAfterFreeObserver : public SafetyObserver { *solver_, assumptions, static_cast(budget_.per_query.count()), stats_) : solver_->check(assumptions); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); } else { z3::solver s(c, "QF_BV"); s.set(":timeout", static_cast(budget_.per_query.count())); @@ -491,6 +493,8 @@ class UseAfterFreeObserver : public SafetyObserver { s, assumptions, static_cast(budget_.per_query.count()), stats_) : s.check(assumptions); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(s, assumptions, result); } } catch (const z3::exception&) { ++stats_.unknown; diff --git a/src/symbolic/tactics.cpp b/src/symbolic/tactics.cpp index b1331f6..941e731 100644 --- a/src/symbolic/tactics.cpp +++ b/src/symbolic/tactics.cpp @@ -363,6 +363,17 @@ z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check return portfolio == recheck ? portfolio : z3::unknown; } +z3::check_result recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions, + z3::check_result portfolio) { + if (portfolio == z3::unknown) + return z3::unknown; + try { + return reconcilePortfolioRecheck(portfolio, solver.check(assumptions)); + } catch (const z3::exception&) { + return z3::unknown; + } +} + z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions, unsigned timeout_ms, ::fold::SolverStats& stats) { z3::expr query = smt_solver.ctx().bool_val(true); diff --git a/tests/unit/test_proved_requires_exact_model.cpp b/tests/unit/test_proved_requires_exact_model.cpp index 326ae52..f6c4989 100644 --- a/tests/unit/test_proved_requires_exact_model.cpp +++ b/tests/unit/test_proved_requires_exact_model.cpp @@ -187,3 +187,25 @@ TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding", CHECK(*c == fold::Confidence::Heuristic); } } + +TEST_CASE("portfolio OOB verdicts are re-checked on the reporting solver", + "[proved-contract][oob][portfolio]") { + // The portfolio answers on its own solvers; the model used to be read from + // the reporting solver without re-checking it, so the counterexample did + // not satisfy the path (i=0 under `i > 5`). + auto unit = parse("int f(int i) { int a[4] = {0}; if (i > 5) return a[i]; return 0; }"); + REQUIRE(unit); + fold::SolverBudget b; + b.portfolio = true; + fold::SolverStats s; + bool found = false; + for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) { + if (f.id.rfind("oob-access:", 0) != 0) + continue; + found = true; + REQUIRE(f.evidence.counterexample.size() == 1); + CHECK(f.evidence.counterexample[0].first == "i"); + CHECK(std::stoll(f.evidence.counterexample[0].second) > 5); + } + CHECK(found); +} -- 2.52.0 From 00082448f439b4a5e182dab02374b46625ba8bd4 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:34:16 -0600 Subject: [PATCH 15/18] fix(encoder): a global C++ lookalike is not a C library function 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. --- .../fold/symbolic/encoder_callee_names.hpp | 7 ++++--- src/symbolic/encoder_callee_names.cpp | 7 ++++++- tests/unit/test_encoder_callee_names.cpp | 2 +- tests/unit/test_library_callee_identity.cpp | 19 +++++++++++++++++++ 4 files changed, 30 insertions(+), 5 deletions(-) diff --git a/include/fold/symbolic/encoder_callee_names.hpp b/include/fold/symbolic/encoder_callee_names.hpp index d9f8b6f..912a3f1 100644 --- a/include/fold/symbolic/encoder_callee_names.hpp +++ b/include/fold/symbolic/encoder_callee_names.hpp @@ -38,9 +38,10 @@ namespace fold { [[nodiscard]] std::string summaryStoreKeyForCall(const clang::CallExpr* ce); // True when `fd` can be the C library function its name suggests: not a class -// member, and declared at global scope, in namespace std, or extern "C". -// Library models (malloc/free, taint sources and sinks) must check this; the -// bare identifier alone also matches `mine::free` or `Pool::free`. +// member, and extern "C", in namespace std, or declared at global scope in a +// system header. Library models (malloc/free, taint sources and sinks) must +// check this; the bare identifier alone also matches `mine::free`, +// `Pool::free` or a project's global `free(Obj*)` overload. [[nodiscard]] bool isCLibraryFunction(const clang::FunctionDecl* fd); // isCLibraryFunction of a call's direct callee; false for indirect calls. diff --git a/src/symbolic/encoder_callee_names.cpp b/src/symbolic/encoder_callee_names.cpp index 2a746fd..faede4f 100644 --- a/src/symbolic/encoder_callee_names.cpp +++ b/src/symbolic/encoder_callee_names.cpp @@ -76,7 +76,12 @@ bool isCLibraryFunction(const clang::FunctionDecl* fd) { return false; if (fd->isExternC() || fd->isInStdNamespace()) return true; - return fd->getDeclContext()->getRedeclContext()->isTranslationUnit(); + // A global C++ function is a library function only when a system header + // declares it; a project overload that shares a libc name is not. + if (!fd->getDeclContext()->getRedeclContext()->isTranslationUnit()) + return false; + const auto& sm = fd->getASTContext().getSourceManager(); + return sm.isInSystemHeader(fd->getCanonicalDecl()->getLocation()); } bool isCLibraryCallee(const clang::CallExpr* ce) { diff --git a/tests/unit/test_encoder_callee_names.cpp b/tests/unit/test_encoder_callee_names.cpp index 5b0608c..25c4b8b 100644 --- a/tests/unit/test_encoder_callee_names.cpp +++ b/tests/unit/test_encoder_callee_names.cpp @@ -176,7 +176,7 @@ TEST_CASE("isCLibraryCallee: only C library functions, never members or namespac CHECK(fold::isCLibraryCallee(calls[1])); // std::free resolves to ::free CHECK_FALSE(fold::isCLibraryCallee(calls[2])); // mine::free CHECK_FALSE(fold::isCLibraryCallee(calls[3])); // Pool::free - CHECK(fold::isCLibraryCallee(calls[4])); // global scope: C semantics + CHECK_FALSE(fold::isCLibraryCallee(calls[4])); // global C++ function, not extern "C" CHECK_FALSE(fold::isCLibraryCallee(calls[5])); // indirect call CHECK_FALSE(fold::isCLibraryCallee(nullptr)); } diff --git a/tests/unit/test_library_callee_identity.cpp b/tests/unit/test_library_callee_identity.cpp index 1f65688..d2890e3 100644 --- a/tests/unit/test_library_callee_identity.cpp +++ b/tests/unit/test_library_callee_identity.cpp @@ -115,3 +115,22 @@ TEST_CASE("taint: libc system with tainted input is still a sink", "[library-cal "int f() { return system(getenv(\"CMD\")); }\n"; CHECK(countKind(runTaint(code), fold::FindingKind::TaintTrack) == 1); } + +TEST_CASE("heap model: a global C++ function named free is not libc free", + "[library-callee][double-free][global]") { + // A global-scope C++ overload (no extern "C", not in a system header) is a + // project function that shares libc's name, not the library function. + const std::string code = kLibc + "struct Obj { int v; };\n" + "void free(Obj*) {}\n" + "int f() {\n" + " Obj* o = static_cast(malloc(sizeof(Obj)));\n" + " if (!o) return 0;\n" + " o->v = 1;\n" + " free(o);\n" + " int v = o->v;\n" + " free(o);\n" + " return v;\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); + CHECK(countKind(runUseAfterFree(code), fold::FindingKind::UseAfterFree) == 0); +} -- 2.52.0 From b8c997c732e3fdfadb225039ff87d94502e0c547 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:37:21 -0600 Subject: [PATCH 16/18] fix(scan): report quarantined TUs as coverage gaps 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. --- docs/USAGE.md | 3 +- include/fold/cli/clang_shard_tu.hpp | 4 ++ include/fold/report/scan_coverage.hpp | 1 + src/cli/clang_shard_tu.cpp | 23 +++++++++ src/cli/scan_runner.cpp | 15 ++---- tests/integration/test_subprocess_fanout.cpp | 54 ++++++++++++++++++++ 6 files changed, 88 insertions(+), 12 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 97ada63..8f6f67d 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -92,7 +92,8 @@ deduplicated finding set. Both machine formats record which C/C++ translation units were analyzed: the native JSON gains a `coverage` object (`tus_attempted`, `tus_analyzed`, and one `gaps` entry per unanalyzed TU with a reason: `compile-errors`, -`frontend-failed`, `analysis-failed`, `timeout`, `crash`, or `worker-exit`), +`frontend-failed`, `analysis-failed`, `timeout`, `crash`, `worker-exit`, or +`quarantined` for a TU a prior run's quarantine skipped), and SARIF carries the same data as an `invocations` entry with `executionSuccessful` and one `toolExecutionNotifications` entry per gap. A scan with any gap, or one that analyzed no TU, exits `2` after writing its diff --git a/include/fold/cli/clang_shard_tu.hpp b/include/fold/cli/clang_shard_tu.hpp index 854a888..89bc4a5 100644 --- a/include/fold/cli/clang_shard_tu.hpp +++ b/include/fold/cli/clang_shard_tu.hpp @@ -50,6 +50,10 @@ struct ClangShardTuOutcome { ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, ClangShardTuState state, ClangShardTuHooks hooks); +// Log TUs skipped because a prior run quarantined them; a worker also emits a +// `quarantined` file_finished record for each so its parent counts the gap. +void reportQuarantinedTus(const ScanOptions& opts, const std::vector& skipped); + // Coverage of `requested` TUs given the outcomes recorded for them. A // requested TU with no outcome never reached the detectors: the front end // produced no AST for it ("frontend-failed"). diff --git a/include/fold/report/scan_coverage.hpp b/include/fold/report/scan_coverage.hpp index 770b03f..58c468c 100644 --- a/include/fold/report/scan_coverage.hpp +++ b/include/fold/report/scan_coverage.hpp @@ -13,6 +13,7 @@ struct CoverageGap { // compile-errors: the front end reported errors, so the AST is partial. // frontend-failed: no AST was produced (missing file, bad command line). // analysis-failed: the detectors threw on this TU. + // quarantined: a prior run quarantined this TU, so it was skipped. // timeout / crash / worker-exit: the isolated worker died on this TU. std::string reason; }; diff --git a/src/cli/clang_shard_tu.cpp b/src/cli/clang_shard_tu.cpp index 4ca6ff6..11c2ff1 100644 --- a/src/cli/clang_shard_tu.cpp +++ b/src/cli/clang_shard_tu.cpp @@ -129,6 +129,29 @@ ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang: return outcome; } +void reportQuarantinedTus(const ScanOptions& opts, const std::vector& skipped) { + if (skipped.empty()) + return; + spdlog::info("quarantine: skipping {} TU(s) from prior run in {}", skipped.size(), + opts.quarantine_dir); + for (std::size_t i = 0; i < skipped.size() && i < 8; ++i) + spdlog::info(" skipped: {}", skipped[i]); + if (skipped.size() > 8) + spdlog::info(" ... (+{} more)", skipped.size() - 8); + // A quarantined TU was not analysed, so it is a coverage gap. A worker + // tells its parent, which otherwise sees no file_finished record and + // calls the TU frontend-failed. + if (!opts.is_worker) + return; + for (const auto& file : skipped) { + std::cout << nlohmann::json{{"kind", "file_finished"}, + {"data", {{"path", file}, {"gap", "quarantined"}}}} + .dump() + << '\n'; + } + std::cout.flush(); +} + ScanCoverage tuCoverage(const std::vector& requested, const std::vector& outcomes) { std::unordered_map gap_by_path; diff --git a/src/cli/scan_runner.cpp b/src/cli/scan_runner.cpp index 0c12af2..2895f1c 100644 --- a/src/cli/scan_runner.cpp +++ b/src/cli/scan_runner.cpp @@ -351,16 +351,7 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db, } files.push_back(f); } - if (!skipped.empty()) { - spdlog::info("quarantine: skipping {} TU(s) from prior run in {}", skipped.size(), - opts.quarantine_dir); - for (std::size_t i = 0; i < skipped.size() && i < 8; ++i) { - spdlog::info(" skipped: {}", skipped[i]); - } - if (skipped.size() > 8) { - spdlog::info(" ... (+{} more)", skipped.size() - 8); - } - } + reportQuarantinedTus(opts, skipped); const SourceDetectorPlan detector_plan = makeSourceDetectorPlan(opts.detectors); std::vector detector_profiles = detector_plan.makeDetectorProfiles(); @@ -584,7 +575,9 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db, graph_security_candidates.empty() ? nullptr : &graph_security_candidates}; auto factory = makeSourceTuFrontendFactory(tu_config, tu_state); (void)tool.run(factory.get()); // which TUs failed comes from tu_outcomes - out.coverage = tuCoverage(files, tu_state.tu_outcomes); + for (const auto& f : skipped) + tu_state.tu_outcomes.push_back({f, "quarantined"}); + out.coverage = tuCoverage(files_in, tu_state.tu_outcomes); } if (out.profile) { out.profile->source_tus_completed = tu_state.source_tus_completed; diff --git a/tests/integration/test_subprocess_fanout.cpp b/tests/integration/test_subprocess_fanout.cpp index b941e83..53327fe 100644 --- a/tests/integration/test_subprocess_fanout.cpp +++ b/tests/integration/test_subprocess_fanout.cpp @@ -172,6 +172,60 @@ TEST_CASE("SubprocessFanout single worker == serial path", "[fanout][unit]") { REQUIRE(parallel.size() == serial.findings.size()); } +TEST_CASE("quarantined TUs are coverage gaps in serial and fan-out scans", + "[fanout][quarantine][coverage]") { + // A TU skipped because a prior run quarantined it was not analysed. The + // serial path dropped it from the attempted set (a complete scan with it + // missing); the fan-out path reported it as frontend-failed. + auto fixtures = locateFixtures(); + writeCompileDb(fixtures); + std::string err; + auto db = fold::loadCompilationDatabase(fixtures, err); + REQUIRE(db); + auto files = db->getAllFiles(); + REQUIRE(files.size() == 3); + + const auto unique = std::to_string(std::chrono::steady_clock::now().time_since_epoch().count()); + const auto quarantine = + std::filesystem::temp_directory_path() / ("fold-quarantine-coverage-" + unique); + fold::cli::appendQuarantine(quarantine.string(), files[0], SIGSEGV); + + fold::cli::ScanOptions opts; + opts.compile_db = fixtures; + opts.detectors = {"clone"}; + opts.min_body_stmts = 1; + opts.quarantine_dir = quarantine.string(); + + auto quarantinedGap = [&](const fold::ScanCoverage& coverage) { + CHECK(coverage.tus_attempted == 3); + CHECK(coverage.tus_analyzed == 2); + REQUIRE(coverage.gaps.size() == 1); + CHECK(fold::cli::normalizeQuarantinePath(coverage.gaps[0].file) == + fold::cli::normalizeQuarantinePath(files[0])); + CHECK(coverage.gaps[0].reason == "quarantined"); + }; + + SECTION("serial") { + auto serial = fold::cli::runDetectorsOnShard(*db, opts, files, + /*include_clone_clustering=*/true); + quarantinedGap(serial.coverage); + } + SECTION("fan-out") { + std::string fold_bin = locateFoldBinary(); + if (fold_bin.empty()) { + WARN("could not locate fold binary; skipping fan-out coverage"); + return; + } + ScopedWorkerBinary worker(fold_bin); + fold::cli::SubprocessFanout fanout; + (void)fanout.runSync(opts, files, /*n_workers=*/2); + quarantinedGap(fanout.coverage()); + } + + std::error_code error; + std::filesystem::remove_all(quarantine, error); +} + TEST_CASE("SubprocessFanout isolates sequential frontend failures and preserves findings", "[fanout][recovery]") { const char* helper = std::getenv("FOLD_TEST_FANOUT_FAILURE_WORKER"); -- 2.52.0 From ed48d4460518973a63d5bceee7598ca02048ee9c Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:43:15 -0600 Subject: [PATCH 17/18] fix(solver): never memoize a core from a portfolio disagreement 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. --- include/fold/cli/profile.hpp | 1 + include/fold/symbolic/tactics.hpp | 7 ++-- include/fold/symbolic/theory.hpp | 7 ++++ src/cli/detector_profile_accum.cpp | 1 + src/cli/profile.cpp | 1 + src/detect/div_by_zero.cpp | 52 +++++++++++++--------------- src/detect/int_overflow.cpp | 52 +++++++++++++--------------- src/detect/null_deref.cpp | 52 +++++++++++++--------------- src/detect/oob_access.cpp | 10 +++--- src/detect/use_after_free.cpp | 5 +-- src/symbolic/tactics.cpp | 10 ++++-- tests/unit/test_model_validation.cpp | 24 +++++++++++++ 12 files changed, 127 insertions(+), 95 deletions(-) diff --git a/include/fold/cli/profile.hpp b/include/fold/cli/profile.hpp index baa605f..e97baf7 100644 --- a/include/fold/cli/profile.hpp +++ b/include/fold/cli/profile.hpp @@ -47,6 +47,7 @@ struct DetectorProfile { std::uint64_t z3_elapsed_ms = 0; std::uint64_t abstract_sat = 0; std::uint64_t abstract_unsat = 0; + std::uint64_t portfolio_disagreements = 0; std::uint64_t z3_decisions = 0; std::uint64_t z3_conflicts = 0; std::uint64_t findings_emitted = 0; diff --git a/include/fold/symbolic/tactics.hpp b/include/fold/symbolic/tactics.hpp index 52944b1..f298ac4 100644 --- a/include/fold/symbolic/tactics.hpp +++ b/include/fold/symbolic/tactics.hpp @@ -42,10 +42,13 @@ z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vecto /// Re-checks a decided portfolio verdict on `solver`, the reporting solver, so /// it holds the model or unsat core, and reconciles the two answers. Unknown -/// stays unknown without a re-check. +/// stays unknown without a re-check. A verdict the re-check does not reproduce +/// counts in `stats.portfolio_disagreements`; callers must then neither read a +/// model nor memoize an unsat core from `solver`. [[nodiscard]] z3::check_result recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions, - z3::check_result portfolio); + z3::check_result portfolio, + ::fold::SolverStats& stats); /// Check assumptions with an ESCALATING timeout. A query that returns UNKNOWN /// at `base_timeout_ms` is re-checked at 2x, 4x, ... up to a cap, so a query diff --git a/include/fold/symbolic/theory.hpp b/include/fold/symbolic/theory.hpp index d796dd0..dea5014 100644 --- a/include/fold/symbolic/theory.hpp +++ b/include/fold/symbolic/theory.hpp @@ -130,6 +130,9 @@ struct SolverStats { std::uint64_t timeouts = 0; std::uint64_t abstract_sat = 0; std::uint64_t abstract_unsat = 0; + // Portfolio verdicts the reporting solver did not reproduce (it timed out + // or answered the other way); each became unknown. + std::uint64_t portfolio_disagreements = 0; std::uint64_t bailed_functions = 0; std::uint64_t states_merged = 0; std::uint64_t states_kept_separate = 0; @@ -254,6 +257,7 @@ struct SolverStats { timeouts += other.timeouts; abstract_sat += other.abstract_sat; abstract_unsat += other.abstract_unsat; + portfolio_disagreements += other.portfolio_disagreements; bailed_functions += other.bailed_functions; states_merged += other.states_merged; states_kept_separate += other.states_kept_separate; @@ -360,6 +364,9 @@ struct SolverStats { if (abstract_sat != 0 || abstract_unsat != 0) { os << " abstract_sat=" << abstract_sat << " abstract_unsat=" << abstract_unsat; } + if (portfolio_disagreements != 0) { + os << " portfolio_disagreements=" << portfolio_disagreements; + } if (bailed_functions != 0) { os << " bailed_functions=" << bailed_functions; } diff --git a/src/cli/detector_profile_accum.cpp b/src/cli/detector_profile_accum.cpp index 9b0b93b..0206dc7 100644 --- a/src/cli/detector_profile_accum.cpp +++ b/src/cli/detector_profile_accum.cpp @@ -37,6 +37,7 @@ void applySolverStats(DetectorProfile& profile, const ::fold::SolverStats& stats profile.z3_elapsed_ms = static_cast(stats.elapsed.count()); profile.abstract_sat = stats.abstract_sat; profile.abstract_unsat = stats.abstract_unsat; + profile.portfolio_disagreements = stats.portfolio_disagreements; profile.z3_decisions = stats.decisions; profile.z3_conflicts = stats.conflicts; profile.states_merged = stats.states_merged; diff --git a/src/cli/profile.cpp b/src/cli/profile.cpp index 2038faf..9e1a7cd 100644 --- a/src/cli/profile.cpp +++ b/src/cli/profile.cpp @@ -53,6 +53,7 @@ std::string ScanProfile::to_json() const { {"z3_elapsed_ms", detector.z3_elapsed_ms}, {"abstract_sat", detector.abstract_sat}, {"abstract_unsat", detector.abstract_unsat}, + {"portfolio_disagreements", detector.portfolio_disagreements}, {"z3_decisions", detector.z3_decisions}, {"z3_conflicts", detector.z3_conflicts}, {"findings_emitted", detector.findings_emitted}, diff --git a/src/detect/div_by_zero.cpp b/src/detect/div_by_zero.cpp index ed832af..5667d36 100644 --- a/src/detect/div_by_zero.cpp +++ b/src/detect/div_by_zero.cpp @@ -205,24 +205,22 @@ class DivByZeroObserver : public SafetyObserver { result == z3::sat ? "SAT (flagged)" : result == z3::unsat ? "UNSAT (guarded)" : "TIMEOUT"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = solver_->check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("div-by-zero", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, hazard); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, hazard); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -252,24 +250,22 @@ class DivByZeroObserver : public SafetyObserver { result == z3::sat ? "SAT (flagged)" : result == z3::unsat ? "UNSAT (guarded)" : "TIMEOUT"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = local_s.check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("div-by-zero", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(local_s, path, hazard); - } - if (artifact_result == z3::sat) { - m = local_s.get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(local_s, path, hazard); - if (result == z3::sat) - m = local_s.get_model(); } + // Only a reconciled verdict leaves `local_s` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(local_s, path, hazard); + if (result == z3::sat) + m = local_s.get_model(); } symbolic::ExprCache::instance().store(canonical_hash, result); CachedDivResult cached_result; diff --git a/src/detect/int_overflow.cpp b/src/detect/int_overflow.cpp index 2e87416..2d40fe1 100644 --- a/src/detect/int_overflow.cpp +++ b/src/detect/int_overflow.cpp @@ -419,24 +419,22 @@ class IntOverflowObserver : public SafetyObserver { : result == z3::unsat ? "UNSAT (guarded)" : unknown_reason.empty() ? "UNKNOWN" : "UNKNOWN (" + unknown_reason + ")"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = solver_->check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("int-overflow", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, unsafe); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, unsafe); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, unsafe); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -467,24 +465,22 @@ class IntOverflowObserver : public SafetyObserver { : result == z3::unsat ? "UNSAT (guarded)" : unknown_reason.empty() ? "UNKNOWN" : "UNKNOWN (" + unknown_reason + ")"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = local_s.check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("int-overflow", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(local_s, path, unsafe); - } - if (artifact_result == z3::sat) { - m = local_s.get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(local_s, path, unsafe); - if (result == z3::sat) - m = local_s.get_model(); } + // Only a reconciled verdict leaves `local_s` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(local_s, path, unsafe); + if (result == z3::sat) + m = local_s.get_model(); } symbolic::ExprCache::instance().store(canonical_hash, result); CachedOverflowResult cached_result; diff --git a/src/detect/null_deref.cpp b/src/detect/null_deref.cpp index 959fb82..3468e5a 100644 --- a/src/detect/null_deref.cpp +++ b/src/detect/null_deref.cpp @@ -284,24 +284,22 @@ class NullDerefObserver : public SafetyObserver { result == z3::sat ? "SAT (flagged)" : result == z3::unsat ? "UNSAT (guarded)" : "TIMEOUT"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = solver_->check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("null-deref", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, hazard); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, hazard); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -332,24 +330,22 @@ class NullDerefObserver : public SafetyObserver { result == z3::sat ? "SAT (flagged)" : result == z3::unsat ? "UNSAT (guarded)" : "TIMEOUT"); - if (budget_.portfolio && (result == z3::sat || result == z3::unsat)) { + if (budget_.portfolio) { auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = local_s.check(assumptions); - result = symbolic::reconcilePortfolioRecheck(result, artifact_result); + const auto disagreements = stats_.portfolio_disagreements; + result = + symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_); + if (stats_.portfolio_disagreements != disagreements) + traceQuery("null-deref", loc, result, + "UNKNOWN (portfolio re-check disagreed)"); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(local_s, path, hazard); - } - if (artifact_result == z3::sat) { - m = local_s.get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(local_s, path, hazard); - if (result == z3::sat) - m = local_s.get_model(); } + // Only a reconciled verdict leaves `local_s` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(local_s, path, hazard); + if (result == z3::sat) + m = local_s.get_model(); } symbolic::ExprCache::instance().store(canonical_hash, result); CachedNullResult cached_result; diff --git a/src/detect/oob_access.cpp b/src/detect/oob_access.cpp index 3a7344a..79fb441 100644 --- a/src/detect/oob_access.cpp +++ b/src/detect/oob_access.cpp @@ -287,7 +287,8 @@ class OOBObserver : public SafetyObserver { : symbolic::checkAdaptive(*solver_, assumptions, static_cast(budget_.per_query.count())); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -327,7 +328,8 @@ class OOBObserver : public SafetyObserver { : symbolic::checkAdaptive(local_s, assumptions, static_cast(budget_.per_query.count())); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(local_s, assumptions, result); + result = + symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -509,7 +511,7 @@ class OOBObserver : public SafetyObserver { : symbolic::checkAdaptive(*solver_, assumptions, static_cast(budget_.per_query.count())); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); + result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -533,7 +535,7 @@ class OOBObserver : public SafetyObserver { : symbolic::checkAdaptive(s, assumptions, static_cast(budget_.per_query.count())); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(s, assumptions, result); + result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { diff --git a/src/detect/use_after_free.cpp b/src/detect/use_after_free.cpp index 73686a1..3d8bc38 100644 --- a/src/detect/use_after_free.cpp +++ b/src/detect/use_after_free.cpp @@ -481,7 +481,8 @@ class UseAfterFreeObserver : public SafetyObserver { static_cast(budget_.per_query.count()), stats_) : solver_->check(assumptions); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result); + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); } else { z3::solver s(c, "QF_BV"); s.set(":timeout", static_cast(budget_.per_query.count())); @@ -494,7 +495,7 @@ class UseAfterFreeObserver : public SafetyObserver { stats_) : s.check(assumptions); if (budget_.portfolio) - result = symbolic::recheckPortfolioVerdict(s, assumptions, result); + result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_); } } catch (const z3::exception&) { ++stats_.unknown; diff --git a/src/symbolic/tactics.cpp b/src/symbolic/tactics.cpp index 941e731..d05d3d3 100644 --- a/src/symbolic/tactics.cpp +++ b/src/symbolic/tactics.cpp @@ -364,14 +364,18 @@ z3::check_result reconcilePortfolioRecheck(z3::check_result portfolio, z3::check } z3::check_result recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions, - z3::check_result portfolio) { + z3::check_result portfolio, ::fold::SolverStats& stats) { if (portfolio == z3::unknown) return z3::unknown; + z3::check_result recheck = z3::unknown; try { - return reconcilePortfolioRecheck(portfolio, solver.check(assumptions)); + recheck = solver.check(assumptions); } catch (const z3::exception&) { - return z3::unknown; } + const z3::check_result reconciled = reconcilePortfolioRecheck(portfolio, recheck); + if (reconciled == z3::unknown) + ++stats.portfolio_disagreements; + return reconciled; } z3::check_result checkWithPortfolio(z3::solver& smt_solver, const z3::expr_vector& assumptions, diff --git a/tests/unit/test_model_validation.cpp b/tests/unit/test_model_validation.cpp index 38160bb..1428499 100644 --- a/tests/unit/test_model_validation.cpp +++ b/tests/unit/test_model_validation.cpp @@ -134,3 +134,27 @@ TEST_CASE("portfolio verdicts stand only when the re-check agrees", "[portfolio] CHECK(reconcilePortfolioRecheck(z3::sat, z3::unsat) == z3::unknown); CHECK(reconcilePortfolioRecheck(z3::unsat, z3::sat) == z3::unknown); } + +TEST_CASE("portfolio re-check on the reporting solver records disagreements", + "[portfolio][soundness]") { + // A disagreement used to be silent, and the detectors memoized the + // re-check's unsat core even when the verdict became unknown. + z3::context ctx; + z3::solver solver(ctx, "QF_BV"); + const z3::expr value = ctx.bv_const("value", 64); + solver.add(value == ctx.bv_val(7, 64)); + z3::expr_vector assumptions(ctx); + using fold::symbolic::recheckPortfolioVerdict; + + fold::SolverStats stats; + CHECK(recheckPortfolioVerdict(solver, assumptions, z3::sat, stats) == z3::sat); + CHECK(stats.portfolio_disagreements == 0); + CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unknown, stats) == z3::unknown); + CHECK(stats.portfolio_disagreements == 0); + CHECK(recheckPortfolioVerdict(solver, assumptions, z3::unsat, stats) == z3::unknown); + CHECK(stats.portfolio_disagreements == 1); + + fold::SolverStats merged; + merged.merge(stats); + CHECK(merged.portfolio_disagreements == 1); +} -- 2.52.0 From fcf474e4f0c6e857f17b1d0879be131987fb0385 Mon Sep 17 00:00:00 2001 From: trvon Date: Thu, 24 Sep 2026 21:46:12 -0600 Subject: [PATCH 18/18] refactor(cli): one TU path normalizer for coverage, fan-out and quarantine 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. --- include/fold/cli/clang_shard_tu.hpp | 4 ---- include/fold/cli/tu_path.hpp | 11 ++++++++++ include/fold/cli/tu_quarantine.hpp | 4 ++-- meson.build | 1 + src/cli/clang_shard_tu.cpp | 21 ++++-------------- src/cli/scan_runner.cpp | 2 +- src/cli/subprocess_fanout.cpp | 21 +++--------------- src/cli/tu_path.cpp | 23 ++++++++++++++++++++ src/cli/tu_quarantine.cpp | 19 ++-------------- tests/integration/test_subprocess_fanout.cpp | 8 +++---- tests/unit/test_tu_quarantine.cpp | 6 ++--- 11 files changed, 54 insertions(+), 66 deletions(-) create mode 100644 include/fold/cli/tu_path.hpp create mode 100644 src/cli/tu_path.cpp diff --git a/include/fold/cli/clang_shard_tu.hpp b/include/fold/cli/clang_shard_tu.hpp index 89bc4a5..14d8889 100644 --- a/include/fold/cli/clang_shard_tu.hpp +++ b/include/fold/cli/clang_shard_tu.hpp @@ -35,10 +35,6 @@ struct ClangShardTuHooks { [[nodiscard]] std::string currentClangTuPath(const clang::ASTContext& ctx); -// Absolute, symlink-resolved form used to match TU paths across the compile -// DB, the front end, and worker records. -[[nodiscard]] std::string normalizeClangTuPath(const std::string& path); - // `gap_reason` is empty when the TU was analyzed on a clean AST; otherwise it // is a CoverageGap reason ("compile-errors", "analysis-failed"). struct ClangShardTuOutcome { diff --git a/include/fold/cli/tu_path.hpp b/include/fold/cli/tu_path.hpp new file mode 100644 index 0000000..12f2ae1 --- /dev/null +++ b/include/fold/cli/tu_path.hpp @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace fold::cli { + +// Absolute, symlink-resolved form used to match TU paths across the compile +// DB, the front end, worker records and the quarantine file. +[[nodiscard]] std::string normalizeTuPath(const std::string& path); + +} // namespace fold::cli diff --git a/include/fold/cli/tu_quarantine.hpp b/include/fold/cli/tu_quarantine.hpp index 906ac36..9cb2dba 100644 --- a/include/fold/cli/tu_quarantine.hpp +++ b/include/fold/cli/tu_quarantine.hpp @@ -4,9 +4,9 @@ #include #include -namespace fold::cli { +#include "fold/cli/tu_path.hpp" -[[nodiscard]] std::string normalizeQuarantinePath(const std::string& path); +namespace fold::cli { /// Read quarantine.txt from `quarantine_dir`. /// diff --git a/meson.build b/meson.build index 6699b26..6001ff5 100644 --- a/meson.build +++ b/meson.build @@ -294,6 +294,7 @@ fold_core_sources += files( 'src/cli/source_summary_pipeline.cpp', 'src/cli/source_tu_runner.cpp', 'src/cli/tu_quarantine.cpp', + 'src/cli/tu_path.cpp', 'src/cli/detector_plan.cpp', 'src/cli/detector_profile_accum.cpp', 'src/cli/finding_evidence.cpp', diff --git a/src/cli/clang_shard_tu.cpp b/src/cli/clang_shard_tu.cpp index 11c2ff1..7186f92 100644 --- a/src/cli/clang_shard_tu.cpp +++ b/src/cli/clang_shard_tu.cpp @@ -13,6 +13,7 @@ #include "fold/cli/scan_options.hpp" #include "fold/cli/signal_isolation.hpp" +#include "fold/cli/tu_path.hpp" #include "fold/report/finding.hpp" #include "fold/report/finding_json.hpp" #include "fold/report/scan_coverage.hpp" @@ -61,20 +62,6 @@ void emitWorkerTuPayload(std::ostream& out, const ClangShardTuState& state, } // namespace -std::string normalizeClangTuPath(const std::string& path) { - if (path.empty()) - return path; - std::error_code ec; - std::filesystem::path p(path); - std::filesystem::path abs = p.is_absolute() ? p : std::filesystem::absolute(p, ec); - if (ec) - return p.lexically_normal().string(); - auto canonical = std::filesystem::weakly_canonical(abs, ec); - if (!ec) - return canonical.string(); - return abs.lexically_normal().string(); -} - std::string currentClangTuPath(const clang::ASTContext& ctx) { const auto& sm = ctx.getSourceManager(); auto fid = sm.getMainFileID(); @@ -85,7 +72,7 @@ std::string currentClangTuPath(const clang::ASTContext& ctx) { ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, ClangShardTuState state, ClangShardTuHooks hooks) { - const std::string tu_path = normalizeClangTuPath(currentClangTuPath(ctx)); + const std::string tu_path = normalizeTuPath(currentClangTuPath(ctx)); ClangShardTuOutcome outcome{tu_path, "analysis-failed"}; if (!state.summaries || !state.func_summaries || !state.findings || !state.quarantined_this_run) { @@ -156,12 +143,12 @@ ScanCoverage tuCoverage(const std::vector& requested, const std::vector& outcomes) { std::unordered_map gap_by_path; for (const auto& outcome : outcomes) - gap_by_path.insert_or_assign(normalizeClangTuPath(outcome.path), outcome.gap_reason); + gap_by_path.insert_or_assign(normalizeTuPath(outcome.path), outcome.gap_reason); ScanCoverage coverage; coverage.tracked = true; coverage.tus_attempted = requested.size(); for (const auto& file : requested) { - const auto it = gap_by_path.find(normalizeClangTuPath(file)); + const auto it = gap_by_path.find(normalizeTuPath(file)); if (it == gap_by_path.end()) coverage.gaps.push_back({file, "frontend-failed"}); else if (!it->second.empty()) diff --git a/src/cli/scan_runner.cpp b/src/cli/scan_runner.cpp index 2895f1c..ba052c5 100644 --- a/src/cli/scan_runner.cpp +++ b/src/cli/scan_runner.cpp @@ -345,7 +345,7 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db, files.reserve(files_in.size()); std::vector skipped; for (const auto& f : files_in) { - if (quarantined.count(normalizeQuarantinePath(f)) != 0u) { + if (quarantined.count(normalizeTuPath(f)) != 0u) { skipped.push_back(f); continue; } diff --git a/src/cli/subprocess_fanout.cpp b/src/cli/subprocess_fanout.cpp index 4315c15..33b405b 100644 --- a/src/cli/subprocess_fanout.cpp +++ b/src/cli/subprocess_fanout.cpp @@ -24,6 +24,7 @@ #include #include "fold/cli/clang_shard_tu.hpp" +#include "fold/cli/tu_path.hpp" #include "fold/cli/tu_quarantine.hpp" #include "fold/detect/clone.hpp" #include "fold/detect/equiv.hpp" @@ -46,22 +47,6 @@ namespace { using json = nlohmann::json; -std::string normalizePath(const std::string& path) { - if (path.empty()) - return path; - std::error_code ec; - std::filesystem::path p(path); - std::filesystem::path abs = p.is_absolute() ? p : std::filesystem::absolute(p, ec); - if (ec) { - return p.lexically_normal().string(); - } - auto canonical = std::filesystem::weakly_canonical(abs, ec); - if (!ec) { - return canonical.string(); - } - return abs.lexically_normal().string(); -} - struct ChildProc { pid_t pid = -1; int stdin_fd = -1; @@ -170,7 +155,7 @@ ShardOutput runShardWithRecovery(const std::string& binary, } else if (kind == "func_summary") { local_func_summaries.push_back(fromJson(data)); } else if (kind == "file_finished") { - finished_files.insert(normalizePath(data.value("path", ""))); + finished_files.insert(normalizeTuPath(data.value("path", ""))); result.tu_outcomes.push_back( {data.value("path", ""), data.value("gap", "")}); } @@ -210,7 +195,7 @@ ShardOutput runShardWithRecovery(const std::string& binary, std::string failed_file; std::size_t failed_index = shard_files.size(); for (std::size_t i = 0; i < shard_files.size(); ++i) { - if (finished_files.count(normalizePath(shard_files[i])) == 0) { + if (finished_files.count(normalizeTuPath(shard_files[i])) == 0) { failed_file = shard_files[i]; failed_index = i; break; diff --git a/src/cli/tu_path.cpp b/src/cli/tu_path.cpp new file mode 100644 index 0000000..1692ccf --- /dev/null +++ b/src/cli/tu_path.cpp @@ -0,0 +1,23 @@ +#include "fold/cli/tu_path.hpp" + +#include +#include + +namespace fold::cli { + +std::string normalizeTuPath(const std::string& path) { + if (path.empty()) + return path; + std::error_code error; + std::filesystem::path input(path); + std::filesystem::path absolute = + input.is_absolute() ? input : std::filesystem::absolute(input, error); + if (error) + return input.lexically_normal().string(); + auto canonical = std::filesystem::weakly_canonical(absolute, error); + if (!error) + return canonical.string(); + return absolute.lexically_normal().string(); +} + +} // namespace fold::cli diff --git a/src/cli/tu_quarantine.cpp b/src/cli/tu_quarantine.cpp index 828f722..05bb8db 100644 --- a/src/cli/tu_quarantine.cpp +++ b/src/cli/tu_quarantine.cpp @@ -21,21 +21,6 @@ bool hasSignalSuffix(const std::string& line, std::size_t colon) { } // namespace -std::string normalizeQuarantinePath(const std::string& path) { - if (path.empty()) - return path; - std::error_code error; - std::filesystem::path input(path); - std::filesystem::path absolute = - input.is_absolute() ? input : std::filesystem::absolute(input, error); - if (error) - return input.lexically_normal().string(); - auto canonical = std::filesystem::weakly_canonical(absolute, error); - if (!error) - return canonical.string(); - return absolute.lexically_normal().string(); -} - std::unordered_set loadQuarantine(const std::string& quarantine_dir) { std::unordered_set paths; if (quarantine_dir.empty()) @@ -61,7 +46,7 @@ std::unordered_set loadQuarantine(const std::string& quarantine_dir const auto colon = line.rfind(':'); std::string path = hasSignalSuffix(line, colon) ? line.substr(0, colon) : line; if (!path.empty()) - paths.insert(normalizeQuarantinePath(path)); + paths.insert(normalizeTuPath(path)); } return paths; } @@ -70,7 +55,7 @@ void appendQuarantineFailure(const std::string& quarantine_dir, const std::strin std::string_view cause, int code) { if (quarantine_dir.empty() || tu_path.empty()) return; - const std::string normalized = normalizeQuarantinePath(tu_path); + const std::string normalized = normalizeTuPath(tu_path); if (loadQuarantine(quarantine_dir).contains(normalized)) return; diff --git a/tests/integration/test_subprocess_fanout.cpp b/tests/integration/test_subprocess_fanout.cpp index 53327fe..88c172f 100644 --- a/tests/integration/test_subprocess_fanout.cpp +++ b/tests/integration/test_subprocess_fanout.cpp @@ -200,8 +200,8 @@ TEST_CASE("quarantined TUs are coverage gaps in serial and fan-out scans", CHECK(coverage.tus_attempted == 3); CHECK(coverage.tus_analyzed == 2); REQUIRE(coverage.gaps.size() == 1); - CHECK(fold::cli::normalizeQuarantinePath(coverage.gaps[0].file) == - fold::cli::normalizeQuarantinePath(files[0])); + CHECK(fold::cli::normalizeTuPath(coverage.gaps[0].file) == + fold::cli::normalizeTuPath(files[0])); CHECK(coverage.gaps[0].reason == "quarantined"); }; @@ -260,8 +260,8 @@ TEST_CASE("SubprocessFanout isolates sequential frontend failures and preserves std::vector{"fanout-test:after.cpp", "fanout-test:before.cpp"}); const auto quarantined = fold::cli::loadQuarantine(quarantine.string()); - REQUIRE(quarantined.contains(fold::cli::normalizeQuarantinePath(files[1]))); - REQUIRE(quarantined.contains(fold::cli::normalizeQuarantinePath(files[2]))); + REQUIRE(quarantined.contains(fold::cli::normalizeTuPath(files[1]))); + REQUIRE(quarantined.contains(fold::cli::normalizeTuPath(files[2]))); std::ifstream input(quarantine / "quarantine.txt"); const std::string records((std::istreambuf_iterator(input)), std::istreambuf_iterator()); diff --git a/tests/unit/test_tu_quarantine.cpp b/tests/unit/test_tu_quarantine.cpp index e345e0c..893cdb8 100644 --- a/tests/unit/test_tu_quarantine.cpp +++ b/tests/unit/test_tu_quarantine.cpp @@ -36,7 +36,7 @@ TEST_CASE("TU quarantine loads signal suffixes and ignores comments", "[cli][qua const auto paths = fold::cli::loadQuarantine(temp.path().string()); REQUIRE(paths.size() == 1); - CHECK(paths.contains(fold::cli::normalizeQuarantinePath(source.string()))); + CHECK(paths.contains(fold::cli::normalizeTuPath(source.string()))); } TEST_CASE("TU quarantine append is normalized and idempotent", "[cli][quarantine]") { @@ -51,11 +51,11 @@ TEST_CASE("TU quarantine append is normalized and idempotent", "[cli][quarantine const auto paths = fold::cli::loadQuarantine(temp.path().string()); REQUIRE(paths.size() == 1); - CHECK(paths.contains(fold::cli::normalizeQuarantinePath(source.string()))); + CHECK(paths.contains(fold::cli::normalizeTuPath(source.string()))); std::ifstream input(temp.path() / "quarantine.txt"); std::string line; REQUIRE(std::getline(input, line)); - CHECK(line == fold::cli::normalizeQuarantinePath(source.string()) + "\tsignal:6"); + CHECK(line == fold::cli::normalizeTuPath(source.string()) + "\tsignal:6"); CHECK_FALSE(std::getline(input, line)); } -- 2.52.0