trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix audit findings: soundness, coverage reporting, docs, and review follow-ups #1

Merged
trevon merged 18 commits from fix/audit-findings into master 2026-09-25 06:48:08 +00:00
Conversation 0 Commits 18 Files changed 81 +2379 -541
81 changed files with 2379 additions and 541 deletions
Download patch file Download diff file Expand all files Collapse all files

3
AGENTS.md
View file

@ -42,7 +42,8 @@ Compatibility requirements:
- Existing `fold scan --input-type binary --binary <path>` 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:

3
BUILD.md
View file

@ -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

96
README.md
View file

@ -1,73 +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 and OpenGrep pre-push hooks; install
[OpenGrep](https://opengrep.dev/) before pushing.
## 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

11
docs/USAGE.md
View file

@ -89,6 +89,17 @@ 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`, `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
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.

29
docs/architecture/performance.md Normal file
View file

@ -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.

29
docs/positioning.md
View file

@ -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
docs/research/prior-art.md
View file

@ -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.

23
include/fold/cli/clang_shard_tu.hpp
View file

@ -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);
// `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);
// 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<std::string>& 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").
[[nodiscard]] ScanCoverage tuCoverage(const std::vector<std::string>& requested,
const std::vector<ClangShardTuOutcome>& outcomes);
} // namespace cli
} // namespace fold

1
include/fold/cli/profile.hpp
View file

@ -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;

2
include/fold/cli/scan_router.hpp
View file

@ -33,6 +33,8 @@ struct ScanRouterResult {
ScanContext context;
// RF-8: Rust fuzzable function interfaces carried through the router.
std::vector<frontend::RustInterface> rust_interfaces;
// Which requested C/C++ TUs were actually analyzed.
ScanCoverage coverage;
};
std::optional<ScanProfile> mergeScanProfilesForRouter(const std::optional<ScanProfile>& source,

3
include/fold/cli/scan_runner.hpp
View file

@ -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<SerializedSummary> func_summaries;
std::optional<ScanProfile> profile;
// Per-TU coverage of the clang source lane; untracked elsewhere.
ScanCoverage coverage;
};
struct LanguageIrSafetyDetectors {

3
include/fold/cli/source_tu_runner.hpp
View file

@ -6,6 +6,7 @@
#include <unordered_set>
#include <vector>
#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<ClangShardTuOutcome> tu_outcomes;
// Non-incremental profiling counts definitions during the existing AST
// traversal instead of launching a second fingerprinting parse.
std::unordered_set<std::string> profile_function_names;

6
include/fold/cli/subprocess_fanout.hpp
View file

@ -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<Finding> runSync(const ScanOptions& opts, const std::vector<std::string>& 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<pid_t> children_; // tracked PIDs, cleared as they exit
bool cancelled_ = false;
ScanCoverage coverage_;
};
} // namespace fold::cli

11
include/fold/cli/tu_path.hpp Normal file
View file

@ -0,0 +1,11 @@
#pragma once
#include <string>
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

4
include/fold/cli/tu_quarantine.hpp
View file

@ -4,9 +4,9 @@
#include <string_view>
#include <unordered_set>
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`.
///

73
include/fold/detect/loop_havoc.hpp Normal file
View file

@ -0,0 +1,73 @@
#pragma once
#include <vector>
#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<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt);
void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
const std::vector<const clang::VarDecl*>& 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<const clang::VarDecl*>& vars);
// 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.
//
// 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_; }
// 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<const clang::VarDecl*>& vars) const;
private:
bool exact_ = true;
bool exited_ = false;
std::vector<const clang::VarDecl*> memory_bases_;
bool unknown_memory_write_ = false;
};
} // namespace fold::detect

4
include/fold/detect/taint_track.hpp
View file

@ -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 {

27
include/fold/detect/z3_model_support.hpp
View file

@ -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<std::string, SourceIntType>;
// 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<std::string, z3::e
}
inline std::vector<std::pair<std::string, std::string>>
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<std::string, z3::expr> symbols;
std::unordered_set<unsigned> seen;
collectLeafSymbols(expr, symbols, seen);
@ -92,6 +109,14 @@ collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSi
std::vector<std::pair<std::string, std::string>> 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;

6
include/fold/report/findings_json_report.hpp
View file

@ -4,6 +4,7 @@
#include <vector>
#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<Finding>& findings);
// With `coverage`, the envelope gains a `coverage` object (additive; the
// output_version is unchanged).
void writeFindingsJson(std::ostream& out, const std::vector<Finding>& findings,
const ScanCoverage* coverage = nullptr);
} // namespace fold

8
include/fold/report/sarif.hpp
View file

@ -4,6 +4,7 @@
#include <vector>
#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<Finding>& findings);
// Serialize a finding set that has already passed filterAndDedup.
void writeFilteredSarif(std::ostream& out, const std::vector<Finding>& 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<Finding>& findings,
const ScanCoverage* coverage = nullptr);
} // namespace fold

44
include/fold/report/scan_coverage.hpp Normal file
View file

@ -0,0 +1,44 @@
#pragma once
#include <cstddef>
#include <nlohmann/json.hpp>
#include <string>
#include <vector>
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.
// 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;
};
// 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<CoverageGap> 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

9
include/fold/symbolic/encoder.hpp
View file

@ -131,6 +131,15 @@ class SymbolicEnv {
void createHeapArray(const z3::expr& ptr, unsigned count, unsigned elem_size);
std::optional<ArrayInfo> 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<z3::expr> tryGetMember(const std::string& key) const {

22
include/fold/symbolic/encoder_callee_names.hpp
View file

@ -23,10 +23,28 @@ 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 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.
[[nodiscard]] bool isCLibraryCallee(const clang::CallExpr* ce);
} // namespace fold

9
include/fold/symbolic/encoder_type_queries.hpp
View file

@ -3,10 +3,12 @@
#include <z3++.h>
#include <cstdint>
#include <optional>
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<std::uint64_t>
typeTraitConstant(const clang::ASTContext& ctx, const clang::UnaryExprOrTypeTraitExpr* expr);
} // namespace fold::symbolic

18
include/fold/symbolic/tactics.hpp
View file

@ -32,6 +32,24 @@ 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);
/// 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. 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,
::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
/// that is just barely over budget still resolves (SAT/UNSAT) instead of losing

7
include/fold/symbolic/theory.hpp
View file

@ -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;
}

1
meson.build
View file

@ -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',

87
src/cli/clang_shard_tu.cpp
View file

@ -1,6 +1,7 @@
#include "fold/cli/clang_shard_tu.hpp"
#include <clang/AST/ASTContext.h>
#include <clang/Basic/Diagnostic.h>
#include <clang/Basic/SourceManager.h>
#include <spdlog/spdlog.h>
@ -8,33 +9,23 @@
#include <filesystem>
#include <iostream>
#include <nlohmann/json.hpp>
#include <unordered_map>
#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"
#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,7 +53,10 @@ void emitWorkerTuPayload(std::ostream& out, const ClangShardTuState& state,
state.findings->erase(state.findings->begin() + static_cast<std::ptrdiff_t>(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();
}
@ -76,17 +70,18 @@ std::string currentClangTuPath(const clang::ASTContext& ctx) {
return "<unknown>";
}
void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx,
ClangShardTuState state, ClangShardTuHooks hooks) {
ClangShardTuOutcome runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx,
ClangShardTuState state, ClangShardTuHooks hooks) {
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) {
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 +94,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 +113,50 @@ void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ct
if (opts.is_worker)
::_Exit(1);
}
return outcome;
}
void reportQuarantinedTus(const ScanOptions& opts, const std::vector<std::string>& 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<std::string>& requested,
const std::vector<ClangShardTuOutcome>& outcomes) {
std::unordered_map<std::string, std::string> gap_by_path;
for (const auto& outcome : outcomes)
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(normalizeTuPath(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

1
src/cli/detector_profile_accum.cpp
View file

@ -37,6 +37,7 @@ void applySolverStats(DetectorProfile& profile, const ::fold::SolverStats& stats
profile.z3_elapsed_ms = static_cast<std::uint64_t>(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;

5
src/cli/main.cpp
View file

@ -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<spdlog::sinks::stderr_color_sink_mt>());
if (quiet) {
spdlog::set_level(spdlog::level::warn);
}

1
src/cli/profile.cpp
View file

@ -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},

25
src/cli/scan_command.cpp
View file

@ -107,16 +107,17 @@ bool writeStreamAtomically(const std::string& output_path, Writer&& writer) {
}
int writeReport(const std::vector<fold::Finding>& 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;
}

5
src/cli/scan_router.cpp
View file

@ -34,6 +34,7 @@ struct SourceRun {
std::optional<ShardResult> shard;
std::optional<ScanProfile> profile;
std::vector<std::string> 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(),

23
src/cli/scan_runner.cpp
View file

@ -345,22 +345,13 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db,
files.reserve(files_in.size());
std::vector<std::string> skipped;
for (const auto& f : files_in) {
if (quarantined.count(normalizeQuarantinePath(f)) != 0u) {
if (quarantined.count(normalizeTuPath(f)) != 0u) {
skipped.push_back(f);
continue;
}
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<DetectorProfile> detector_profiles = detector_plan.makeDetectorProfiles();
@ -583,14 +574,16 @@ 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
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;
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)

18
src/cli/source_summary_pipeline.cpp
View file

@ -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;
}

9
src/cli/source_tu_runner.cpp
View file

@ -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;
}

33
src/cli/subprocess_fanout.cpp
View file

@ -23,6 +23,8 @@
#include <utility>
#include <vector>
#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"
@ -45,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;
@ -83,6 +69,8 @@ struct ShardOutput {
std::vector<FunctionSummary> summaries;
std::vector<Finding> findings;
std::vector<SerializedSummary> func_summaries;
// file_finished records plus the TU each dead worker was processing.
std::vector<ClangShardTuOutcome> tu_outcomes;
bool success = true;
};
@ -167,7 +155,9 @@ 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", "")});
}
} catch (const std::exception& e) {
spdlog::warn("subprocess_fanout: bad NDJSON line: {}", e.what());
@ -205,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;
@ -217,6 +207,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 +571,7 @@ std::vector<Finding> SubprocessFanout::runSync(const ScanOptions& opts,
std::vector<FunctionSummary> all_summaries;
std::vector<Finding> all_findings;
std::vector<SerializedSummary> all_func_summaries;
std::vector<ClangShardTuOutcome> all_tu_outcomes;
bool all_shards_succeeded = true;
for (auto& t : tasks) {
auto res = t.get();
@ -590,6 +583,9 @@ std::vector<Finding> 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<std::mutex> lk(mtx_);
@ -597,6 +593,7 @@ std::vector<Finding> 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

23
src/cli/tu_path.cpp Normal file
View file

@ -0,0 +1,23 @@
#include "fold/cli/tu_path.hpp"
#include <filesystem>
#include <system_error>
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

19
src/cli/tu_quarantine.cpp
View file

@ -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<std::string> loadQuarantine(const std::string& quarantine_dir) {
std::unordered_set<std::string> paths;
if (quarantine_dir.empty())
@ -61,7 +46,7 @@ std::unordered_set<std::string> 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;

114
src/detect/always_condition.cpp
View file

@ -22,6 +22,7 @@
#include <vector>
#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<Visitor> {
bool found = false;
bool VisitCallExpr(clang::CallExpr*) {
found = true;
return false;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.found;
}
std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
if (!stmt)
return {};
struct Visitor : clang::RecursiveASTVisitor<Visitor> {
std::vector<const clang::VarDecl*> vars;
std::unordered_set<const clang::VarDecl*> 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<clang::DeclRefExpr>(lhs))
add(clang::dyn_cast<clang::VarDecl>(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<clang::DeclRefExpr>(sub))
add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
return true;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.vars;
}
void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
const std::vector<const clang::VarDecl*>& extra) {
if (vars.empty()) {
vars = extra;
return;
}
std::unordered_set<const clang::VarDecl*> 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<const clang::VarDecl*>& 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,44 +282,55 @@ class AlwaysConditionWalker {
SymbolicEnv& env) {
const bool opaque_loop =
containsCallExpr(cond) || containsCallExpr(body) || containsCallExpr(inc);
std::vector<const clang::VarDecl*> assigned;
if (opaque_loop) {
assigned = collectAssignedVars(cond);
appendAssignedVars(assigned, collectAssignedVars(body));
appendAssignedVars(assigned, collectAssignedVars(inc));
}
std::vector<const clang::VarDecl*> 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<unsigned>(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) {
havocAssignedVars(env, assigned);
// 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()) {
exits.havoc(env, assigned);
env.restorePath(entry_path);
}
return true;

101
src/detect/dead_branch.cpp
View file

@ -23,6 +23,7 @@
#include <vector>
#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<Visitor> {
bool found = false;
bool VisitCallExpr(clang::CallExpr*) {
found = true;
return false;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.found;
}
std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
if (!stmt)
return {};
struct Visitor : clang::RecursiveASTVisitor<Visitor> {
std::vector<const clang::VarDecl*> vars;
std::unordered_set<const clang::VarDecl*> 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<clang::DeclRefExpr>(lhs))
add(clang::dyn_cast<clang::VarDecl>(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<clang::DeclRefExpr>(sub))
add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
return true;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.vars;
}
void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
const std::vector<const clang::VarDecl*>& extra) {
std::unordered_set<const clang::VarDecl*> 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<const clang::VarDecl*>& 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,39 +308,53 @@ 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<unsigned>(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) {
havocAssignedVars(env, assigned);
// 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()) {
exits.havoc(env, assigned);
path = entry_path;
}
return true;

3
src/detect/dead_statement.cpp
View file

@ -204,7 +204,8 @@ class DeadStatementVisitor : public clang::RecursiveASTVisitor<DeadStatementVisi
Finding f;
f.kind = FindingKind::DeadStatement;
f.confidence = Confidence::Proved;
// A CFG fact read off the AST, not a solver result.
f.confidence = Confidence::Syntactic;
f.locations.push_back(locOf(anchor, ctx_, fname));
const auto statement_anchor = stableStatementAnchor(anchor, ctx_);
f.id = stableQualityFindingId("dead-statement", stableFunctionId(fd), statement_anchor);

53
src/detect/div_by_zero.cpp
View file

@ -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"
@ -204,23 +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);
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::milliseconds>(
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<unsigned>(budget_.per_query.count()));
if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@ -250,23 +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);
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::milliseconds>(
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;
@ -609,7 +608,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;

5
src/detect/double_free.cpp
View file

@ -76,7 +76,10 @@ class DoubleFreeObserver : public SafetyObserver {
Finding f;
f.id = "double-free:" + current_function_ + ":" + dedup_key;
f.kind = FindingKind::DoubleFree;
f.confidence = Confidence::Proved;
// No solver query backs this: it is the heap model's freed flag on the
// walked path, and the path itself is never checked. Proved needs an
// exact bounded model (docs/research/soundness.md).
f.confidence = Confidence::Heuristic;
f.message = "Double-free: heap allocation freed at " + current_function_ + ":" + dedup_key +
" was already freed on this path";
Location l;

61
src/detect/int_overflow.cpp
View file

@ -419,23 +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);
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::milliseconds>(
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<unsigned>(budget_.per_query.count()));
if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@ -466,23 +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);
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::milliseconds>(
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;
@ -608,13 +606,14 @@ class IntOverflowObserver : public SafetyObserver {
return fold::mix64(seed, sourceBitWidth);
}
static std::pair<std::string, std::vector<std::pair<std::string, std::string>>>
std::pair<std::string, std::vector<std::pair<std::string, std::string>>>
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) + ")";

234
src/detect/loop_havoc.cpp Normal file
View file

@ -0,0 +1,234 @@
#include "fold/detect/loop_havoc.hpp"
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/AST/Stmt.h>
#include <clang/AST/StmtCXX.h>
#include <unordered_set>
namespace fold::detect {
bool containsCallExpr(const clang::Stmt* stmt) {
if (!stmt)
return false;
struct Visitor : clang::RecursiveASTVisitor<Visitor> {
bool found = false;
bool VisitCallExpr(clang::CallExpr*) {
found = true;
return false;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.found;
}
std::vector<const clang::VarDecl*> collectAssignedVars(const clang::Stmt* stmt) {
if (!stmt)
return {};
struct Visitor : clang::RecursiveASTVisitor<Visitor> {
std::vector<const clang::VarDecl*> vars;
std::unordered_set<const clang::VarDecl*> 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<clang::DeclRefExpr>(lhs))
add(clang::dyn_cast<clang::VarDecl>(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<clang::DeclRefExpr>(sub))
add(clang::dyn_cast<clang::VarDecl>(dre->getDecl()));
return true;
}
} visitor;
visitor.TraverseStmt(const_cast<clang::Stmt*>(stmt));
return visitor.vars;
}
void appendAssignedVars(std::vector<const clang::VarDecl*>& vars,
const std::vector<const clang::VarDecl*>& extra) {
std::unordered_set<const clang::VarDecl*> 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<const clang::VarDecl*>& 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 or continue that targets the loop being unrolled counts. A
// switch captures `break` but not `continue`.
bool escapes(const clang::Stmt* stmt, int breakable_depth, int loop_depth) {
if (!stmt)
return false;
if (clang::isa<clang::GotoStmt>(stmt) || clang::isa<clang::IndirectGotoStmt>(stmt))
return true;
if (clang::isa<clang::BreakStmt>(stmt))
return breakable_depth == 0;
// 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<clang::ContinueStmt>(stmt))
return loop_depth == 0;
const bool loop = clang::isa<clang::ForStmt>(stmt) || clang::isa<clang::WhileStmt>(stmt) ||
clang::isa<clang::DoStmt>(stmt) || clang::isa<clang::CXXForRangeStmt>(stmt);
const bool breakable = loop || clang::isa<clang::SwitchStmt>(stmt);
for (const clang::Stmt* child : stmt->children()) {
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<const clang::VarDecl*> bases;
bool unknown_target = false;
};
MemoryWrites collectMemoryWrites(const clang::Stmt* stmt) {
struct Visitor : clang::RecursiveASTVisitor<Visitor> {
MemoryWrites writes;
std::unordered_set<const clang::VarDecl*> seen;
void record(const clang::Expr* target) {
target = target->IgnoreParenImpCasts();
const clang::Expr* base = nullptr;
if (const auto* sub = clang::dyn_cast<clang::ArraySubscriptExpr>(target))
base = sub->getBase();
else if (const auto* mem = clang::dyn_cast<clang::MemberExpr>(target))
base = mem->isArrow() ? nullptr : mem->getBase();
else if (const auto* un = clang::dyn_cast<clang::UnaryOperator>(target);
un && un->getOpcode() == clang::UO_Deref) {
writes.unknown_target = true;
return;
} else if (const auto* arrow = clang::dyn_cast<clang::MemberExpr>(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<clang::ArraySubscriptExpr>(base)) {
base = sub->getBase();
continue;
}
if (const auto* mem = clang::dyn_cast<clang::MemberExpr>(base);
mem && !mem->isArrow()) {
base = mem->getBase();
continue;
}
break;
}
const auto* dre = clang::dyn_cast<clang::DeclRefExpr>(base);
const auto* vd = dre ? clang::dyn_cast<clang::VarDecl>(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<clang::Stmt*>(stmt));
return visitor.writes;
}
} // namespace
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<const clang::VarDecl*>& 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) {
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

2
src/detect/meson.build
View file

@ -6,12 +6,14 @@ 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',
'clone.cpp',
'clone_hash_cache.cpp',
'dead_branch.cpp',
'loop_havoc.cpp',
'dead_statement.cpp',
'complexity.cpp',
'equiv.cpp',

60
src/detect/null_deref.cpp
View file

@ -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"
@ -283,23 +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);
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::milliseconds>(
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<unsigned>(budget_.per_query.count()));
if (supportsParam(local_s.get_param_descrs(), "smt.threads")) {
@ -330,23 +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);
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::milliseconds>(
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;
@ -765,7 +764,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 +789,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;

87
src/detect/oob_access.cpp
View file

@ -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"
@ -210,7 +211,7 @@ class OOBObserver : public SafetyObserver {
const clang::VarDecl* base_var = nullptr) override {
SolverStats::ScopedHookTimer _t(stats_);
if (heap_access) {
checkUseAfterFree(*heap_access, path, loc);
checkUseAfterFree(*heap_access, path, loc, env);
}
if (known_len < 0) {
// T160: interprocedural buffer-bound threading (ParmVarDecl sizes).
@ -240,7 +241,7 @@ class OOBObserver : public SafetyObserver {
}
if (known_len < 0) {
if (heap_access)
checkHeapBounds(*heap_access, path, loc);
checkHeapBounds(*heap_access, path, loc, env);
return;
}
}
@ -285,6 +286,9 @@ class OOBObserver : public SafetyObserver {
static_cast<unsigned>(budget_.per_query.count()), stats_)
: symbolic::checkAdaptive(*solver_, assumptions,
static_cast<unsigned>(budget_.per_query.count()));
if (budget_.portfolio)
result =
symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
std::chrono::steady_clock::now() - t0);
if (stats_.profiling_enabled && !budget_.portfolio) {
@ -323,6 +327,9 @@ class OOBObserver : public SafetyObserver {
static_cast<unsigned>(budget_.per_query.count()), stats_)
: symbolic::checkAdaptive(local_s, assumptions,
static_cast<unsigned>(budget_.per_query.count()));
if (budget_.portfolio)
result =
symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_);
stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
std::chrono::steady_clock::now() - t0);
if (stats_.profiling_enabled && !budget_.portfolio) {
@ -351,7 +358,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);
@ -381,19 +389,22 @@ class OOBObserver : 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);
// Member writes bounds-check the region (placement_new_*: intTwo @8>4).
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);
}
}
@ -403,7 +414,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;
@ -436,22 +447,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));
}
}
@ -492,20 +510,14 @@ class OOBObserver : public SafetyObserver {
stats_)
: symbolic::checkAdaptive(*solver_, assumptions,
static_cast<unsigned>(budget_.per_query.count()));
if (budget_.portfolio)
result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
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::milliseconds>(
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 {
@ -522,20 +534,14 @@ class OOBObserver : public SafetyObserver {
s, assumptions, static_cast<unsigned>(budget_.per_query.count()), stats_)
: symbolic::checkAdaptive(s, assumptions,
static_cast<unsigned>(budget_.per_query.count()));
if (budget_.portfolio)
result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_);
stats_.elapsed += std::chrono::duration_cast<std::chrono::milliseconds>(
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::milliseconds>(
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);
}
}
@ -652,8 +658,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 + ":" +
@ -749,13 +757,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<std::pair<std::string, std::string>> 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 + ":" +
@ -835,11 +845,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 +875,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()) {

4
src/detect/static_ptr_asymmetry.cpp
View file

@ -319,7 +319,9 @@ std::vector<Finding> 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) + ":" +

73
src/detect/taint_track.cpp
View file

@ -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<TaintSource> 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<TaintSource> 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<TaintSink> 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;

29
src/detect/unreachable.cpp
View file

@ -21,6 +21,7 @@
#include <vector>
#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<const clang::VarDecl*> 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<unsigned>(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()) {
exits.havoc(env, assigned);
path = entry_path;
}
return true;
}

3
src/detect/unused_function.cpp
View file

@ -219,7 +219,8 @@ std::vector<Finding> 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() +

43
src/detect/use_after_free.cpp
View file

@ -23,6 +23,8 @@
#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"
#include "fold/symbolic/tactics.hpp"
@ -121,6 +123,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<Finding>& out) : ctx_(ctx), out_(out) {}
@ -275,14 +283,14 @@ class Analyzer {
bool isSameVarRealloc(const clang::VarDecl* lhs, const clang::Expr* rhs) const {
const auto* call = clang::dyn_cast_or_null<clang::CallExpr>(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;
}
@ -408,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<z3::context&>(heap_access.is_use_after_free.ctx());
z3::expr hazard = heap_access.is_use_after_free;
@ -444,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);
}
}
@ -466,6 +480,9 @@ class UseAfterFreeObserver : public SafetyObserver {
*solver_, assumptions,
static_cast<unsigned>(budget_.per_query.count()), stats_)
: solver_->check(assumptions);
if (budget_.portfolio)
result =
symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_);
} else {
z3::solver s(c, "QF_BV");
s.set(":timeout", static_cast<unsigned>(budget_.per_query.count()));
@ -477,6 +494,8 @@ class UseAfterFreeObserver : public SafetyObserver {
s, assumptions, static_cast<unsigned>(budget_.per_query.count()),
stats_)
: s.check(assumptions);
if (budget_.portfolio)
result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_);
}
} catch (const z3::exception&) {
++stats_.unknown;
@ -505,10 +524,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;

53
src/detect/z3_model_support.cpp Normal file
View file

@ -0,0 +1,53 @@
#include "fold/detect/z3_model_support.hpp"
#include <clang/AST/ASTContext.h>
#include <clang/AST/Decl.h>
#include <clang/AST/RecursiveASTVisitor.h>
#include <functional>
#include <set>
namespace fold::detect {
SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, const clang::ASTContext& ctx) {
SourceIntTypes types;
if (fn == nullptr)
return types;
std::set<std::string> 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<unsigned>(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<Visitor> {
std::function<void(const clang::VarDecl*)> 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<int64_t>(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

14
src/report/findings_json_report.cpp
View file

@ -7,15 +7,17 @@
namespace fold {
void writeFindingsJson(std::ostream& out, const std::vector<Finding>& findings) {
void writeFindingsJson(std::ostream& out, const std::vector<Finding>& 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

1
src/report/meson.build
View file

@ -7,6 +7,7 @@ fold_core_sources += files(
'findings_json_report.cpp',
'markdown.cpp',
'patch_writer.cpp',
'scan_coverage.cpp',
'sarif.cpp',
'triage.cpp',
)

8
src/report/sarif.cpp
View file

@ -404,7 +404,8 @@ void writeSarif(std::ostream& out, const std::vector<Finding>& findings) {
writeFilteredSarif(out, deduped);
}
void writeFilteredSarif(std::ostream& out, const std::vector<Finding>& findings) {
void writeFilteredSarif(std::ostream& out, const std::vector<Finding>& findings,
const ScanCoverage* coverage) {
const json tool = {
{"driver",
{
@ -421,7 +422,10 @@ void writeFilteredSarif(std::ostream& out, const std::vector<Finding>& 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 << ',';

47
src/report/scan_coverage.cpp Normal file
View file

@ -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

27
src/symbolic/encoder_callee_names.cpp
View file

@ -7,6 +7,8 @@
#include <clang/AST/ExprCXX.h>
#include <clang/Basic/SourceManager.h>
#include "fold/frontend/stable_identity.hpp"
namespace fold {
std::string calleeName(const clang::CallExpr* ce) {
@ -61,6 +63,31 @@ 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<clang::CXXMethodDecl>(fd))
return false;
if (fd->isExternC() || fd->isInStdNamespace())
return true;
// 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) {
return ce != nullptr && isCLibraryFunction(ce->getDirectCallee());
}
std::string qualifiedCalleeName(const clang::CallExpr* ce) {
if (ce == nullptr)
return {};

6
src/symbolic/encoder_expr.cpp
View file

@ -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<UnaryExprOrTypeTraitExpr>(e)) {
if (auto value = symbolic::typeTraitConstant(ctx, trait))
return markEncoded("UnaryExprOrTypeTraitExpr",
env.ctx().bv_val(static_cast<std::uint64_t>(*value), kBitvecWidth));
}
recordBailedNode(expr->getStmtClassName(),
std::string("expr kind ") + expr->getStmtClassName());
recordPrecision(env, EncodingPrecision::UnsupportedNode,

7
src/symbolic/encoder_expr_arms.cpp
View file

@ -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);

16
src/symbolic/encoder_type_queries.cpp
View file

@ -1,6 +1,7 @@
#include "fold/symbolic/encoder_type_queries.hpp"
#include <clang/AST/ASTContext.h>
#include <clang/AST/Expr.h>
#include <clang/AST/Type.h>
#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<std::uint64_t> 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

19
src/symbolic/summary_encoder.cpp
View file

@ -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::RecursiveASTVisitor<SummaryMetada
const auto* callee = call ? call->getDirectCallee() : 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<CallExpr>(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<z3::expr> 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<FunctionSummarized> summarizeImpl(const clang::FunctionDecl* fd,
params.push_back(p);
std::vector<ExitState> 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<symbolic::SymbolicSummary> 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<ExitState> 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;

19
src/symbolic/tactics.cpp
View file

@ -359,6 +359,25 @@ 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 recheckPortfolioVerdict(z3::solver& solver, const z3::expr_vector& assumptions,
z3::check_result portfolio, ::fold::SolverStats& stats) {
if (portfolio == z3::unknown)
return z3::unknown;
z3::check_result recheck = z3::unknown;
try {
recheck = solver.check(assumptions);
} catch (const z3::exception&) {
}
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,
unsigned timeout_ms, ::fold::SolverStats& stats) {
z3::expr query = smt_solver.ctx().bool_val(true);

5
tests/integration/meson.build
View file

@ -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,

44
tests/integration/test_cli_paths.cpp
View file

@ -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);
}
}

40
tests/integration/test_cross_tu_security.cpp
View file

@ -1,4 +1,7 @@
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/CompilationDatabase.h>
#include <clang/Tooling/Tooling.h>
#include <algorithm>
#include <catch2/catch_test_macros.hpp>
@ -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<char>(in)), std::istreambuf_iterator<char>());
auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, path.string());
if (!unit)
return {};
struct Finder : clang::RecursiveASTVisitor<Finder> {
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);

8
tests/integration/test_mcp_stdio.cpp
View file

@ -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) {

58
tests/integration/test_subprocess_fanout.cpp
View file

@ -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::normalizeTuPath(coverage.gaps[0].file) ==
fold::cli::normalizeTuPath(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");
@ -206,8 +260,8 @@ TEST_CASE("SubprocessFanout isolates sequential frontend failures and preserves
std::vector<std::string>{"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<char>(input)),
std::istreambuf_iterator<char>());

45
tests/unit/meson.build
View file

@ -186,6 +186,51 @@ 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_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_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_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_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',

27
tests/unit/test_encoder_callee_names.cpp
View file

@ -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_FALSE(fold::isCLibraryCallee(calls[4])); // global C++ function, not extern "C"
CHECK_FALSE(fold::isCLibraryCallee(calls[5])); // indirect call
CHECK_FALSE(fold::isCLibraryCallee(nullptr));
}

28
tests/unit/test_int_overflow.cpp
View file

@ -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");
}

136
tests/unit/test_library_callee_identity.cpp Normal file
View file

@ -0,0 +1,136 @@
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>
#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>
#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<clang::ASTUnit> parse(const std::string& code) {
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
}
std::size_t countKind(const std::vector<fold::Finding>& findings, fold::FindingKind kind) {
std::size_t n = 0;
for (const auto& f : findings)
if (f.kind == kind)
++n;
return n;
}
std::vector<fold::Finding> 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<fold::Finding> runUseAfterFree(const std::string& code) {
auto unit = parse(code);
REQUIRE(unit);
return fold::detectUseAfterFreeInContext(unit->getASTContext());
}
std::vector<fold::Finding> 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<int*>(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);
}
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<Obj*>(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);
}

226
tests/unit/test_loop_exit_soundness.cpp Normal file
View file

@ -0,0 +1,226 @@
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>
#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>
#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<clang::ASTUnit> parse(const std::string& code) {
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
}
std::vector<fold::Finding> 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<fold::Finding> 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<fold::Finding> 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<fold::Finding>& 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<Finder> {
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());
}
}
// 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 <cstdlib>\n"
"int pw(unsigned n) { int* buf = static_cast<int*>(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);
}

36
tests/unit/test_model_validation.cpp
View file

@ -122,3 +122,39 @@ 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);
}
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);
}

211
tests/unit/test_proved_requires_exact_model.cpp Normal file
View file

@ -0,0 +1,211 @@
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>
#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <optional>
#include <string>
#include <vector>
#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<clang::ASTUnit> parse(const std::string& code) {
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
}
std::optional<fold::Confidence> confidenceOf(const std::vector<fold::Finding>& 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<fold::Confidence> {
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<std::uint64_t> 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<Finder> {
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());
}
TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding",
"[proved-contract][oob]") {
auto oobConfidence = [](const std::string& code) -> std::optional<fold::Confidence> {
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);
}
}
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);
}

112
tests/unit/test_scan_coverage.cpp Normal file
View file

@ -0,0 +1,112 @@
#include <catch2/catch_test_macros.hpp>
#include <filesystem>
#include <nlohmann/json.hpp>
#include <sstream>
#include <string>
#include <vector>
#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<std::string> requested{tmp("ok.cpp"), tmp("broken.cpp"), tmp("missing.cpp"),
tmp("slow.cpp")};
const std::vector<fold::cli::ClangShardTuOutcome> 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"));
}
}

141
tests/unit/test_summary_key_identity.cpp Normal file
View file

@ -0,0 +1,141 @@
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>
#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>
#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<clang::ASTUnit> parse(const std::string& code) {
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
}
std::vector<const clang::FunctionDecl*> definitionsNamed(clang::ASTUnit& unit,
const std::string& name) {
struct Finder : clang::RecursiveASTVisitor<Finder> {
std::string name;
std::vector<const clang::FunctionDecl*> 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<Finder> {
std::vector<const clang::FunctionDecl*> f_decls;
std::vector<const clang::FunctionDecl*> 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);
}

3
tests/unit/test_symbolic_summary.cpp
View file

@ -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

6
tests/unit/test_tu_quarantine.cpp
View file

@ -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));
}