diff --git a/AGENTS.md b/AGENTS.md index dc5c27b..1532447 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -42,7 +42,8 @@ Compatibility requirements: - Existing `fold scan --input-type binary --binary ` commands must keep working. - Exit codes stay stable: `0` no actionable findings, `1` actionable findings, - `2` input/config/report failure. + `2` input/config/report failure, including a scan that left any requested + translation unit unanalyzed (see `coverage` in docs/USAGE.md). - Reports must preserve per-finding backend provenance. Router implementation rules: diff --git a/BUILD.md b/BUILD.md index 0d66bcc..1ce15c0 100644 --- a/BUILD.md +++ b/BUILD.md @@ -8,6 +8,9 @@ # tests: meson test -C build/release ``` +`setup.sh` also enables the tracked lint pre-commit hook +(`.githooks/pre-commit`). + Linux users without root can validate against a clean container: ```sh diff --git a/README.md b/README.md index b79aeb2..30ff28b 100644 --- a/README.md +++ b/README.md @@ -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 diff --git a/docs/USAGE.md b/docs/USAGE.md index b31bc67..8f6f67d 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -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. diff --git a/docs/architecture/performance.md b/docs/architecture/performance.md new file mode 100644 index 0000000..48e0544 --- /dev/null +++ b/docs/architecture/performance.md @@ -0,0 +1,29 @@ +# Performance + +Optimization is measurement-first and gate-guarded. Every candidate change runs +through the manifest-driven evaluation harness +(`tests/benchmarks/projects/*.json`), which enforces finding-fingerprint +stability, reviewed dispositions, wall-time and RSS regression baselines, and a +gold set (`bench/gold/`). The gold set was derived from fold's own reviewed +output and is matched by detector kind and file, so it catches drift; it is not +an independent precision or recall measure. A ledger of measured wins and +closed hypotheses is in +[the optimization loop](../research/optimization-loop-2026-07-30.md). + +## Single-pass graph building + +The one structural item on the roadmap is single-pass graph building. A source +scan currently parses each translation unit twice: once to build the project +call graph, and once to run detectors, because the detector pass consumes the +graph (cross-TU candidate expansion and summary priming). The planned change +collapses these into one parse per TU that produces graph contributions and runs +the intra-TU detectors in the same pass, keeping only light per-TU edge and +signature records, then runs the cross-TU-dependent closure after every TU. See +[the design](../research/single-pass-graph-design.md). + +This is chosen over precompiled-header or module caching to preserve +portability: it introduces no Clang-version-locked serialized artifacts, no +SDK- or toolchain-locked module cache, and no `-std`/`-I`/`-D` flag-matching +bug surface, so every machine that consumes a `compile_commands.json` today +keeps working. Correctness parity for the deferred closure is policed by the +existing finding-fingerprint and gold gates. diff --git a/docs/positioning.md b/docs/positioning.md index 847db83..2ad477e 100644 --- a/docs/positioning.md +++ b/docs/positioning.md @@ -11,20 +11,23 @@ sink with a Z3-produced witness, then optionally runs that witness through libFuzzer + ASan to promote findings from "the solver says SAT" to "we observed the crash." -Most static analyzers stop at "the solver says SAT." Most fuzzers don't -know what they're aiming at. fold links the two so the report says +Solver-backed analyzers (for example the Clang Static Analyzer's +optional Z3 refutation) use SMT to prune infeasible paths, but their +reports stop at a static verdict. Most fuzzers don't know what they're +aiming at. fold links the two so the report says which findings are confirmed observable failures, not just satisfiable path predicates. ## Confidence tiers fold reports -Findings are not all equal. fold reports four confidence tiers: +Findings are not all equal. fold reports five confidence tiers: | Tier | Source | Example | |------------------|--------------------------------------------------------------|-------------------------------------------------| | `Syntactic` | AST pattern match, no solver | "function name matches `strcpy`" | | `Heuristic` | Solver gave up or path was over-approximated | "interval analysis can't bound `len`" | -| `Proved` | Z3 returned SAT on (path ∧ hazard); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" | +| `Latent` | Proved in the callee, modulo a caller obligation not discharged | "`p` is dereferenced; no caller shown to pass null" | +| `Proved` | Z3 returned SAT on (path ∧ hazard) over an exact bounded model (no over-approximated operation on the path; see `docs/research/soundness.md`); model is the witness | "Z3 finds `idx=42, len=10` violating bounds" | | `ConcreteWitness`| Z3 model was packaged as a seed and ASan observed the crash | "libFuzzer crashed on `seed_8f3c.bin`" | The ordering is explicit in `include/fold/report/finding.hpp::confidenceRank()` @@ -100,7 +103,7 @@ source, closed methodology, opaque false-positive rates. **fold differs by:** open source (GPL-3.0 when stable), open methodology (`docs/research/soundness.md`), and a closed loop with -libFuzzer that no commercial vendor currently ships. fold is also +libFuzzer in the same report. fold is also substantially less mature on the heuristic-refinement side — Coverity has had two decades of FP-tuning effort that fold has not. @@ -133,15 +136,16 @@ is already your CI surface. ### Bounded model checkers (CBMC, ESBMC) Unroll loops to a configurable depth, encode the bounded program -as an SMT formula, ask Z3 / MathSAT whether any sink is reachable. +as a SAT/SMT formula (CBMC's default back end is a SAT solver) and +ask whether any assertion can fail. Sound for the unrolling depth chosen; report concrete counterexamples; usable as software-verification competitors -(SV-COMP). Slow on large codebases — full-program BMC scales -poorly past a few thousand lines. +(SV-COMP). Whole-program BMC cost grows with program size and +unwinding depth. **fold differs by:** scope and product shape. CBMC verifies one -property of one bounded program; fold scans a 100k-LOC codebase -in minutes, flagging per-sink findings with per-sink witnesses, +property of one bounded program; fold runs per-sink, mostly +intraprocedural queries with a small loop unroll (5 by default), trading verification rigor for breadth. They are complementary: a fold finding worth deep verification can be re-checked under CBMC. @@ -227,8 +231,9 @@ for protocol parsers and other constrained-input APIs. ## Where fold's closed scan→fuzz loop matters -The Phase 1+2 work in M31 closed a gap that no other open-source -analyzer covers: every SAT finding is automatically packaged as a +The Phase 1+2 work in M31 closes the loop inside one tool (directed +fuzzers such as AFLGo and hybrid tools such as SAVIOR explore related +ground; see `docs/research/prior-art.md`): every SAT finding is automatically packaged as a libFuzzer seed, run under ASan, and (if a crash is observed) promoted from `Proved` to `ConcreteWitness` in the same JSON report. The user sees one Finding with `confidence: diff --git a/docs/research/prior-art.md b/docs/research/prior-art.md index 9dcbd65..2c4fc63 100644 --- a/docs/research/prior-art.md +++ b/docs/research/prior-art.md @@ -1,6 +1,6 @@ # Prior Art (condensed) -Key papers grounding fold's design. Full annotations in `prior-art-full.md`. +Key papers grounding fold's design. ## Buffer overflow - **Xu et al. (2020)** *ELAID.* doi:10.1186/s42400-020-00058-2 — interprocedural call graph + SMT on Juliet sinks. diff --git a/include/fold/cli/clang_shard_tu.hpp b/include/fold/cli/clang_shard_tu.hpp index e99ff31..14d8889 100644 --- a/include/fold/cli/clang_shard_tu.hpp +++ b/include/fold/cli/clang_shard_tu.hpp @@ -13,6 +13,7 @@ class ASTContext; namespace fold { struct Finding; +struct ScanCoverage; struct FunctionSummary; struct SerializedSummary; @@ -34,8 +35,26 @@ struct ClangShardTuHooks { [[nodiscard]] std::string currentClangTuPath(const clang::ASTContext& ctx); -void runClangShardTranslationUnit(const ScanOptions& opts, clang::ASTContext& ctx, - ClangShardTuState state, ClangShardTuHooks hooks); +// `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& 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& requested, + const std::vector& outcomes); } // namespace cli } // namespace fold diff --git a/include/fold/cli/profile.hpp b/include/fold/cli/profile.hpp index baa605f..e97baf7 100644 --- a/include/fold/cli/profile.hpp +++ b/include/fold/cli/profile.hpp @@ -47,6 +47,7 @@ struct DetectorProfile { std::uint64_t z3_elapsed_ms = 0; std::uint64_t abstract_sat = 0; std::uint64_t abstract_unsat = 0; + std::uint64_t portfolio_disagreements = 0; std::uint64_t z3_decisions = 0; std::uint64_t z3_conflicts = 0; std::uint64_t findings_emitted = 0; diff --git a/include/fold/cli/scan_router.hpp b/include/fold/cli/scan_router.hpp index b8f1518..37eeb0d 100644 --- a/include/fold/cli/scan_router.hpp +++ b/include/fold/cli/scan_router.hpp @@ -33,6 +33,8 @@ struct ScanRouterResult { ScanContext context; // RF-8: Rust fuzzable function interfaces carried through the router. std::vector rust_interfaces; + // Which requested C/C++ TUs were actually analyzed. + ScanCoverage coverage; }; std::optional mergeScanProfilesForRouter(const std::optional& source, diff --git a/include/fold/cli/scan_runner.hpp b/include/fold/cli/scan_runner.hpp index 5f8da42..1c5041e 100644 --- a/include/fold/cli/scan_runner.hpp +++ b/include/fold/cli/scan_runner.hpp @@ -9,6 +9,7 @@ #include "fold/frontend/rust_backend.hpp" #include "fold/ir/summary.hpp" #include "fold/report/finding.hpp" +#include "fold/report/scan_coverage.hpp" #include "fold/symbolic/serialize.hpp" namespace fold::ir { @@ -31,6 +32,8 @@ struct ShardResult { // runs detectEquivalentFunctionsCrossTU on the complete merged set. std::vector func_summaries; std::optional profile; + // Per-TU coverage of the clang source lane; untracked elsewhere. + ScanCoverage coverage; }; struct LanguageIrSafetyDetectors { diff --git a/include/fold/cli/source_tu_runner.hpp b/include/fold/cli/source_tu_runner.hpp index e5e82fc..d8ffd57 100644 --- a/include/fold/cli/source_tu_runner.hpp +++ b/include/fold/cli/source_tu_runner.hpp @@ -6,6 +6,7 @@ #include #include +#include "fold/cli/clang_shard_tu.hpp" #include "fold/cli/detector_plan.hpp" #include "fold/cli/profile.hpp" #include "fold/cli/scan_options.hpp" @@ -59,6 +60,8 @@ struct SourceTuRunState { std::size_t security_candidate_functions = 0; std::size_t security_graph_expanded_functions = 0; std::size_t source_tus_completed = 0; + // One entry per TU the front end handed over, in completion order. + std::vector tu_outcomes; // Non-incremental profiling counts definitions during the existing AST // traversal instead of launching a second fingerprinting parse. std::unordered_set profile_function_names; diff --git a/include/fold/cli/subprocess_fanout.hpp b/include/fold/cli/subprocess_fanout.hpp index 7dfc25b..aea21f7 100644 --- a/include/fold/cli/subprocess_fanout.hpp +++ b/include/fold/cli/subprocess_fanout.hpp @@ -8,6 +8,7 @@ #include "fold/cli/scan_options.hpp" #include "fold/report/finding.hpp" +#include "fold/report/scan_coverage.hpp" namespace fold::cli { @@ -35,6 +36,10 @@ class SubprocessFanout { std::vector runSync(const ScanOptions& opts, const std::vector& files, int n_workers); + // Per-TU coverage of the last runSync: TUs with compile errors, TUs the + // front end never produced an AST for, and TUs a worker died on. + [[nodiscard]] const ScanCoverage& coverage() const { return coverage_; } + // Cancel any in-flight workers. Used by MCP/LSP when the client // disconnects mid-scan. Safe to call from any thread. void cancel(); @@ -45,6 +50,7 @@ class SubprocessFanout { std::mutex mtx_; std::vector children_; // tracked PIDs, cleared as they exit bool cancelled_ = false; + ScanCoverage coverage_; }; } // namespace fold::cli diff --git a/include/fold/cli/tu_path.hpp b/include/fold/cli/tu_path.hpp new file mode 100644 index 0000000..12f2ae1 --- /dev/null +++ b/include/fold/cli/tu_path.hpp @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace fold::cli { + +// Absolute, symlink-resolved form used to match TU paths across the compile +// DB, the front end, worker records and the quarantine file. +[[nodiscard]] std::string normalizeTuPath(const std::string& path); + +} // namespace fold::cli diff --git a/include/fold/cli/tu_quarantine.hpp b/include/fold/cli/tu_quarantine.hpp index 906ac36..9cb2dba 100644 --- a/include/fold/cli/tu_quarantine.hpp +++ b/include/fold/cli/tu_quarantine.hpp @@ -4,9 +4,9 @@ #include #include -namespace fold::cli { +#include "fold/cli/tu_path.hpp" -[[nodiscard]] std::string normalizeQuarantinePath(const std::string& path); +namespace fold::cli { /// Read quarantine.txt from `quarantine_dir`. /// diff --git a/include/fold/detect/loop_havoc.hpp b/include/fold/detect/loop_havoc.hpp new file mode 100644 index 0000000..484f73c --- /dev/null +++ b/include/fold/detect/loop_havoc.hpp @@ -0,0 +1,73 @@ +#pragma once + +#include + +#include "fold/symbolic/encoder.hpp" + +namespace clang { +class Stmt; +class VarDecl; +} // namespace clang + +namespace fold::detect { + +// Shared by the control-flow walkers (dead-branch, always-condition, +// unreachable) that unroll loops a bounded number of times. + +[[nodiscard]] bool containsCallExpr(const clang::Stmt* stmt); + +// Variables assigned (=, op=, ++, --) anywhere in `stmt`, canonical decls, in +// first-seen order. +[[nodiscard]] std::vector collectAssignedVars(const clang::Stmt* stmt); +void appendAssignedVars(std::vector& vars, + const std::vector& extra); + +// Replace each assigned bitvector variable with a fresh unknown and drop +// access-path facts: after this, nothing about their post-loop values is known. +void havocAssignedVars(SymbolicEnv& env, const std::vector& vars); + +// A `break`, `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& vars) const; + + private: + bool exact_ = true; + bool exited_ = false; + std::vector memory_bases_; + bool unknown_memory_write_ = false; +}; + +} // namespace fold::detect diff --git a/include/fold/detect/taint_track.hpp b/include/fold/detect/taint_track.hpp index 71dec90..79b1a89 100644 --- a/include/fold/detect/taint_track.hpp +++ b/include/fold/detect/taint_track.hpp @@ -30,6 +30,9 @@ struct TaintSource { std::string func; int param = 0; // -1 = return value std::string description = "tainted data"; + // A C library / POSIX function: matches only a callee that is one + // (isCLibraryCallee). False for method-name heuristics such as `get`. + bool c_api = true; }; struct TaintSink { @@ -37,6 +40,7 @@ struct TaintSink { int param = 0; std::string description = "dangerous sink"; unsigned domain = taint_domain::kAny; // which sanitizer domain neutralises it + bool c_api = true; // see TaintSource::c_api }; class TaintTracker : public SafetyObserver { diff --git a/include/fold/detect/z3_model_support.hpp b/include/fold/detect/z3_model_support.hpp index b82a4ba..0e60c09 100644 --- a/include/fold/detect/z3_model_support.hpp +++ b/include/fold/detect/z3_model_support.hpp @@ -14,6 +14,22 @@ namespace fold::detect { +// Source type of an integer variable, for rendering its model value. Symbols +// are 64-bit bitvectors whose low `width` bits carry the source value. +struct SourceIntType { + unsigned width = 0; + bool is_signed = false; +}; +using SourceIntTypes = std::map; + +// Integer-typed parameters and locals of `fn`, by name. A name declared with +// two different integer types is left out rather than guessed. +[[nodiscard]] SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, + const clang::ASTContext& ctx); + +// `raw` truncated to the source width and printed with its signedness. +[[nodiscard]] std::string formatSourceIntValue(uint64_t raw, SourceIntType type); + inline std::string fallbackExprLabel(const clang::Expr* expr, const char* fallback) { if (!expr) return fallback; @@ -84,7 +100,8 @@ inline void collectLeafSymbols(const z3::expr& expr, std::map> -collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned) { +collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSigned, + const SourceIntTypes* types = nullptr) { std::map symbols; std::unordered_set seen; collectLeafSymbols(expr, symbols, seen); @@ -92,6 +109,14 @@ collectModelBindings(const z3::model& model, const z3::expr& expr, bool preferSi std::vector> bindings; bindings.reserve(symbols.size()); for (const auto& [name, symbol] : symbols) { + uint64_t raw = 0; + const auto type = types != nullptr ? types->find(name) : SourceIntTypes::const_iterator{}; + z3::expr value = model.eval(symbol, true); + if (types != nullptr && type != types->end() && value.is_bv() && + value.is_numeral_u64(raw)) { + bindings.emplace_back(name, formatSourceIntValue(raw, type->second)); + continue; + } bindings.emplace_back(name, formatModelValue(model, symbol, preferSigned)); } return bindings; diff --git a/include/fold/report/findings_json_report.hpp b/include/fold/report/findings_json_report.hpp index 0e3a060..d70a406 100644 --- a/include/fold/report/findings_json_report.hpp +++ b/include/fold/report/findings_json_report.hpp @@ -4,6 +4,7 @@ #include #include "finding.hpp" +#include "scan_coverage.hpp" namespace fold { @@ -11,6 +12,9 @@ inline constexpr int kFindingsJsonOutputVersion = 1; // Native, lossless report envelope for Fold findings. This is distinct from // SARIF and is versioned so readers can reject incompatible future shapes. -void writeFindingsJson(std::ostream& out, const std::vector& findings); +// With `coverage`, the envelope gains a `coverage` object (additive; the +// output_version is unchanged). +void writeFindingsJson(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage = nullptr); } // namespace fold diff --git a/include/fold/report/sarif.hpp b/include/fold/report/sarif.hpp index 192e67e..f81beed 100644 --- a/include/fold/report/sarif.hpp +++ b/include/fold/report/sarif.hpp @@ -4,6 +4,7 @@ #include #include "finding.hpp" +#include "scan_coverage.hpp" namespace fold { @@ -13,7 +14,10 @@ const char* sarifRuleId(FindingKind kind); // Serialize findings as SARIF 2.1.0 JSON. Single run with tool name "fold". void writeSarif(std::ostream& out, const std::vector& findings); -// Serialize a finding set that has already passed filterAndDedup. -void writeFilteredSarif(std::ostream& out, const std::vector& findings); +// Serialize a finding set that has already passed filterAndDedup. With +// `coverage`, the run carries an `invocations` entry recording which +// translation units were not analyzed. +void writeFilteredSarif(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage = nullptr); } // namespace fold diff --git a/include/fold/report/scan_coverage.hpp b/include/fold/report/scan_coverage.hpp new file mode 100644 index 0000000..58c468c --- /dev/null +++ b/include/fold/report/scan_coverage.hpp @@ -0,0 +1,44 @@ +#pragma once + +#include +#include +#include +#include + +namespace fold { + +// A translation unit the scan attempted but did not fully analyze. +struct CoverageGap { + std::string file; + // compile-errors: the front end reported errors, so the AST is partial. + // frontend-failed: no AST was produced (missing file, bad command line). + // analysis-failed: the detectors threw on this TU. + // 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 gaps; + + [[nodiscard]] bool incomplete() const { + return tracked && (!gaps.empty() || (tus_attempted > 0 && tus_analyzed == 0)); + } + + void merge(const ScanCoverage& other); +}; + +[[nodiscard]] nlohmann::json coverageToJson(const ScanCoverage& coverage); + +// SARIF 2.1.0 `invocations` entry: executionSuccessful plus one +// toolExecutionNotification per gap. +[[nodiscard]] nlohmann::json coverageToSarifInvocation(const ScanCoverage& coverage); + +} // namespace fold diff --git a/include/fold/symbolic/encoder.hpp b/include/fold/symbolic/encoder.hpp index 4151fd4..067b05a 100644 --- a/include/fold/symbolic/encoder.hpp +++ b/include/fold/symbolic/encoder.hpp @@ -131,6 +131,15 @@ class SymbolicEnv { void createHeapArray(const z3::expr& ptr, unsigned count, unsigned elem_size); std::optional getHeapArray(const z3::expr& ptr) const; void updateHeapArray(const z3::expr& ptr, const z3::expr& new_array); + // Replace every tracked heap array with a fresh array of the same sort: a + // store through an unknown pointer may have written any of them. + void havocHeapArrays() { + static unsigned counter = 0; + for (auto& [_, info] : heap_arrays_) { + const std::string name = "heap_array_havoc_" + std::to_string(counter++); + info.array = ctx_->constant(name.c_str(), info.array.get_sort()); + } + } void removeHeapArray(const z3::expr& ptr); std::optional tryGetMember(const std::string& key) const { diff --git a/include/fold/symbolic/encoder_callee_names.hpp b/include/fold/symbolic/encoder_callee_names.hpp index 53afa3f..912a3f1 100644 --- a/include/fold/symbolic/encoder_callee_names.hpp +++ b/include/fold/symbolic/encoder_callee_names.hpp @@ -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 diff --git a/include/fold/symbolic/encoder_type_queries.hpp b/include/fold/symbolic/encoder_type_queries.hpp index 3f1f53c..e7de74a 100644 --- a/include/fold/symbolic/encoder_type_queries.hpp +++ b/include/fold/symbolic/encoder_type_queries.hpp @@ -3,10 +3,12 @@ #include #include +#include namespace clang { class ASTContext; class QualType; +class UnaryExprOrTypeTraitExpr; } // namespace clang namespace fold { @@ -45,4 +47,11 @@ namespace fold::symbolic { [[nodiscard]] z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx, const clang::QualType& qt); +// The exact value of `sizeof` / `alignof` (and the other type traits) when +// the compiler folds it to a constant: complete, non-dependent, non-VLA +// operands. nullopt otherwise; the encoder then treats the node as +// unsupported rather than guess a size. +[[nodiscard]] std::optional +typeTraitConstant(const clang::ASTContext& ctx, const clang::UnaryExprOrTypeTraitExpr* expr); + } // namespace fold::symbolic diff --git a/include/fold/symbolic/tactics.hpp b/include/fold/symbolic/tactics.hpp index 11be37c..f298ac4 100644 --- a/include/fold/symbolic/tactics.hpp +++ b/include/fold/symbolic/tactics.hpp @@ -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 diff --git a/include/fold/symbolic/theory.hpp b/include/fold/symbolic/theory.hpp index d796dd0..dea5014 100644 --- a/include/fold/symbolic/theory.hpp +++ b/include/fold/symbolic/theory.hpp @@ -130,6 +130,9 @@ struct SolverStats { std::uint64_t timeouts = 0; std::uint64_t abstract_sat = 0; std::uint64_t abstract_unsat = 0; + // Portfolio verdicts the reporting solver did not reproduce (it timed out + // or answered the other way); each became unknown. + std::uint64_t portfolio_disagreements = 0; std::uint64_t bailed_functions = 0; std::uint64_t states_merged = 0; std::uint64_t states_kept_separate = 0; @@ -254,6 +257,7 @@ struct SolverStats { timeouts += other.timeouts; abstract_sat += other.abstract_sat; abstract_unsat += other.abstract_unsat; + portfolio_disagreements += other.portfolio_disagreements; bailed_functions += other.bailed_functions; states_merged += other.states_merged; states_kept_separate += other.states_kept_separate; @@ -360,6 +364,9 @@ struct SolverStats { if (abstract_sat != 0 || abstract_unsat != 0) { os << " abstract_sat=" << abstract_sat << " abstract_unsat=" << abstract_unsat; } + if (portfolio_disagreements != 0) { + os << " portfolio_disagreements=" << portfolio_disagreements; + } if (bailed_functions != 0) { os << " bailed_functions=" << bailed_functions; } diff --git a/meson.build b/meson.build index 6699b26..6001ff5 100644 --- a/meson.build +++ b/meson.build @@ -294,6 +294,7 @@ fold_core_sources += files( 'src/cli/source_summary_pipeline.cpp', 'src/cli/source_tu_runner.cpp', 'src/cli/tu_quarantine.cpp', + 'src/cli/tu_path.cpp', 'src/cli/detector_plan.cpp', 'src/cli/detector_profile_accum.cpp', 'src/cli/finding_evidence.cpp', diff --git a/src/cli/clang_shard_tu.cpp b/src/cli/clang_shard_tu.cpp index 3ce120b..7186f92 100644 --- a/src/cli/clang_shard_tu.cpp +++ b/src/cli/clang_shard_tu.cpp @@ -1,6 +1,7 @@ #include "fold/cli/clang_shard_tu.hpp" #include +#include #include #include @@ -8,33 +9,23 @@ #include #include #include +#include #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(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 ""; } -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& skipped) { + if (skipped.empty()) + return; + spdlog::info("quarantine: skipping {} TU(s) from prior run in {}", skipped.size(), + opts.quarantine_dir); + for (std::size_t i = 0; i < skipped.size() && i < 8; ++i) + spdlog::info(" skipped: {}", skipped[i]); + if (skipped.size() > 8) + spdlog::info(" ... (+{} more)", skipped.size() - 8); + // A quarantined TU was not analysed, so it is a coverage gap. A worker + // tells its parent, which otherwise sees no file_finished record and + // calls the TU frontend-failed. + if (!opts.is_worker) + return; + for (const auto& file : skipped) { + std::cout << nlohmann::json{{"kind", "file_finished"}, + {"data", {{"path", file}, {"gap", "quarantined"}}}} + .dump() + << '\n'; + } + std::cout.flush(); +} + +ScanCoverage tuCoverage(const std::vector& requested, + const std::vector& outcomes) { + std::unordered_map gap_by_path; + 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 diff --git a/src/cli/detector_profile_accum.cpp b/src/cli/detector_profile_accum.cpp index 9b0b93b..0206dc7 100644 --- a/src/cli/detector_profile_accum.cpp +++ b/src/cli/detector_profile_accum.cpp @@ -37,6 +37,7 @@ void applySolverStats(DetectorProfile& profile, const ::fold::SolverStats& stats profile.z3_elapsed_ms = static_cast(stats.elapsed.count()); profile.abstract_sat = stats.abstract_sat; profile.abstract_unsat = stats.abstract_unsat; + profile.portfolio_disagreements = stats.portfolio_disagreements; profile.z3_decisions = stats.decisions; profile.z3_conflicts = stats.conflicts; profile.states_merged = stats.states_merged; diff --git a/src/cli/main.cpp b/src/cli/main.cpp index c5ac311..7601813 100644 --- a/src/cli/main.cpp +++ b/src/cli/main.cpp @@ -402,6 +402,11 @@ int main(int argc, char** argv) { return rc == 0 ? 0 : 2; } + // Diagnostics go to stderr so a report written to stdout stays parseable + // (docs/internal/cli-philosophy.md principle 12). + spdlog::default_logger()->sinks().clear(); + spdlog::default_logger()->sinks().push_back( + std::make_shared()); if (quiet) { spdlog::set_level(spdlog::level::warn); } diff --git a/src/cli/profile.cpp b/src/cli/profile.cpp index 2038faf..9e1a7cd 100644 --- a/src/cli/profile.cpp +++ b/src/cli/profile.cpp @@ -53,6 +53,7 @@ std::string ScanProfile::to_json() const { {"z3_elapsed_ms", detector.z3_elapsed_ms}, {"abstract_sat", detector.abstract_sat}, {"abstract_unsat", detector.abstract_unsat}, + {"portfolio_disagreements", detector.portfolio_disagreements}, {"z3_decisions", detector.z3_decisions}, {"z3_conflicts", detector.z3_conflicts}, {"findings_emitted", detector.findings_emitted}, diff --git a/src/cli/scan_command.cpp b/src/cli/scan_command.cpp index 20e8403..c064542 100644 --- a/src/cli/scan_command.cpp +++ b/src/cli/scan_command.cpp @@ -107,16 +107,17 @@ bool writeStreamAtomically(const std::string& output_path, Writer&& writer) { } int writeReport(const std::vector& report_findings, const std::string& output_path, - const std::string& format, bool redundancy_secondary = false) { + const std::string& format, const fold::ScanCoverage& coverage, + bool redundancy_secondary = false) { const auto serialize = [&](std::ostream& out) { if (format == "sarif") { - fold::writeFilteredSarif(out, report_findings); + fold::writeFilteredSarif(out, report_findings, &coverage); } else if (format == "json") { spdlog::warn("report format 'json' is deprecated as a SARIF alias; use 'sarif' or " "'findings-json'"); - fold::writeFilteredSarif(out, report_findings); + fold::writeFilteredSarif(out, report_findings, &coverage); } else if (format == "findings-json") { - fold::writeFindingsJson(out, report_findings); + fold::writeFindingsJson(out, report_findings, &coverage); } else if (format == "markdown" || format == "md") { fold::writeMarkdown(out, report_findings, redundancy_secondary); } else { @@ -318,8 +319,9 @@ int runScan(const ScanCommand& cli) { } const auto report_started = std::chrono::steady_clock::now(); - const int report_rc = writeReport(report_findings, cli.output_path, cli.format, - opts.freestanding.redundancy_lane_secondary); + const int report_rc = + writeReport(report_findings, cli.output_path, cli.format, router_result.coverage, + opts.freestanding.redundancy_lane_secondary); const auto report_finished = std::chrono::steady_clock::now(); if (report_rc == 2) return 2; @@ -338,6 +340,17 @@ int runScan(const ScanCommand& cli) { return 2; } + // A scan that skipped part of its input cannot vouch for the absence of + // findings there, so it is an input failure (exit 2) even when it found + // nothing. + if (router_result.coverage.incomplete()) { + const auto& coverage = router_result.coverage; + spdlog::error("scan incomplete: analyzed {} of {} translation unit(s)", + coverage.tus_analyzed, coverage.tus_attempted); + for (const auto& gap : coverage.gaps) + spdlog::error(" not analyzed ({}): {}", gap.reason, gap.file); + return 2; + } return report_rc; } diff --git a/src/cli/scan_router.cpp b/src/cli/scan_router.cpp index 1b69783..da58fb0 100644 --- a/src/cli/scan_router.cpp +++ b/src/cli/scan_router.cpp @@ -34,6 +34,7 @@ struct SourceRun { std::optional shard; std::optional profile; std::vector sources; + ScanCoverage coverage; }; struct BinaryRun { @@ -434,6 +435,7 @@ SourceRun runSource(ScanOptions opts) { fold::cli::SubprocessFanout fanout; const auto fanout_start = Clock::now(); run.findings = fanout.runSync(opts, sources, processes); + run.coverage = fanout.coverage(); fanout_ms = durationMs(fanout_start, Clock::now()); } else { spdlog::info("serial: running on {} files", sources.size()); @@ -443,6 +445,7 @@ SourceRun runSource(ScanOptions opts) { serial_ms = durationMs(serial_start, Clock::now()); run.findings = run.shard->findings; run.profile = run.shard->profile; + run.coverage = run.shard->coverage; } // Stamp the per-phase timings onto the profile so the perf-audit // doc can quote them. When --profile isn't on, run.profile is @@ -762,6 +765,7 @@ ScanRouterResult runScanRouter(ScanOptions opts) { result.source_shard = std::move(source.shard); result.profile = std::move(source.profile); result.findings = std::move(source.findings); + result.coverage = std::move(source.coverage); } else if (mode == "rust") { auto rust = runRust(opts); // Re-use the source-side context slots; findings are tagged @@ -814,6 +818,7 @@ ScanRouterResult runScanRouter(ScanOptions opts) { result.context.binary_findings = binary.findings.size(); result.source_shard = std::move(source.shard); result.binary_shard = std::move(binary.shard); + result.coverage = std::move(source.coverage); result.profile = mergeScanProfilesForRouter(source.profile, binary.profile, opts); result.findings.reserve(source.findings.size() + binary.findings.size()); result.findings.insert(result.findings.end(), diff --git a/src/cli/scan_runner.cpp b/src/cli/scan_runner.cpp index 9ea3c59..ba052c5 100644 --- a/src/cli/scan_runner.cpp +++ b/src/cli/scan_runner.cpp @@ -345,22 +345,13 @@ ShardResult runClangDetectorsOnShard(clang::tooling::CompilationDatabase& db, files.reserve(files_in.size()); std::vector skipped; for (const auto& f : files_in) { - if (quarantined.count(normalizeQuarantinePath(f)) != 0u) { + if (quarantined.count(normalizeTuPath(f)) != 0u) { skipped.push_back(f); continue; } files.push_back(f); } - if (!skipped.empty()) { - spdlog::info("quarantine: skipping {} TU(s) from prior run in {}", skipped.size(), - opts.quarantine_dir); - for (std::size_t i = 0; i < skipped.size() && i < 8; ++i) { - spdlog::info(" skipped: {}", skipped[i]); - } - if (skipped.size() > 8) { - spdlog::info(" ... (+{} more)", skipped.size() - 8); - } - } + reportQuarantinedTus(opts, skipped); const SourceDetectorPlan detector_plan = makeSourceDetectorPlan(opts.detectors); std::vector detector_profiles = detector_plan.makeDetectorProfiles(); @@ -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) diff --git a/src/cli/source_summary_pipeline.cpp b/src/cli/source_summary_pipeline.cpp index bf0f020..94db868 100644 --- a/src/cli/source_summary_pipeline.cpp +++ b/src/cli/source_summary_pipeline.cpp @@ -23,6 +23,7 @@ #include "fold/frontend/comp_db.hpp" #include "fold/ir/call_graph.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/summary_encoder.hpp" namespace fold::cli { @@ -86,19 +87,22 @@ bool computeSummariesForFunctions(clang::tooling::CompilationDatabase& db, if (qualified_name.empty() || !target_names_.contains(qualified_name)) return true; + // The graph names functions by qualified name; the + // store keys them by USR so overloads stay apart. + const std::string summary_key = ::fold::summaryStoreKey(declaration); const std::uint64_t source_hash = detect::hashFunctionBody(declaration, source_manager); auto& store = detect::SummaryStore::instance(); - const auto* previous = store.lookup(qualified_name); - if (previous && store.isStale(qualified_name, source_hash)) { - store.invalidate(qualified_name); + const auto* previous = store.lookup(summary_key); + if (previous && store.isStale(summary_key, source_hash)) { + store.invalidate(summary_key); previous = nullptr; } const std::string before = previous ? previous->serialize() : std::string{}; if (!force_recompute_ && previous && - !store.isStale(qualified_name, source_hash)) { + !store.isStale(summary_key, source_hash)) { return true; } @@ -106,15 +110,15 @@ bool computeSummariesForFunctions(clang::tooling::CompilationDatabase& db, if (auto summary = ::fold::summarizeLeafFunctionSymbolically( declaration, context_)) { const std::string after = summary->serialize(); - store.store(qualified_name, *summary); - store.markComputed(qualified_name, source_hash); + store.store(summary_key, *summary); + store.markComputed(summary_key, source_hash); markChanged(after, before); } return true; } (void)::fold::ensureSymbolicSummary(declaration, context_); - if (const auto* current = store.lookup(qualified_name)) + if (const auto* current = store.lookup(summary_key)) markChanged(current->serialize(), before); return true; } diff --git a/src/cli/source_tu_runner.cpp b/src/cli/source_tu_runner.cpp index 332789f..6f8139a 100644 --- a/src/cli/source_tu_runner.cpp +++ b/src/cli/source_tu_runner.cpp @@ -222,10 +222,11 @@ class ShardFrontend final : public clang::ASTFrontendAction { handleTranslationUnitImpl(tu_ctx); }; hooks.quarantine_writer = quarantine_writer; - runClangShardTranslationUnit(opts, ctx, - ClangShardTuState{&summaries, &func_summaries, - &findings, &quarantined_this_run}, - std::move(hooks)); + state.tu_outcomes.push_back(runClangShardTranslationUnit( + opts, ctx, + ClangShardTuState{&summaries, &func_summaries, &findings, + &quarantined_this_run}, + std::move(hooks))); ++state.source_tus_completed; } diff --git a/src/cli/subprocess_fanout.cpp b/src/cli/subprocess_fanout.cpp index 17e9f43..33b405b 100644 --- a/src/cli/subprocess_fanout.cpp +++ b/src/cli/subprocess_fanout.cpp @@ -23,6 +23,8 @@ #include #include +#include "fold/cli/clang_shard_tu.hpp" +#include "fold/cli/tu_path.hpp" #include "fold/cli/tu_quarantine.hpp" #include "fold/detect/clone.hpp" #include "fold/detect/equiv.hpp" @@ -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 summaries; std::vector findings; std::vector func_summaries; + // file_finished records plus the TU each dead worker was processing. + std::vector tu_outcomes; bool success = true; }; @@ -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 SubprocessFanout::runSync(const ScanOptions& opts, std::vector all_summaries; std::vector all_findings; std::vector all_func_summaries; + std::vector all_tu_outcomes; bool all_shards_succeeded = true; for (auto& t : tasks) { auto res = t.get(); @@ -590,6 +583,9 @@ std::vector SubprocessFanout::runSync(const ScanOptions& opts, all_func_summaries.insert(all_func_summaries.end(), std::make_move_iterator(res.func_summaries.begin()), std::make_move_iterator(res.func_summaries.end())); + all_tu_outcomes.insert(all_tu_outcomes.end(), + std::make_move_iterator(res.tu_outcomes.begin()), + std::make_move_iterator(res.tu_outcomes.end())); } { std::lock_guard lk(mtx_); @@ -597,6 +593,7 @@ std::vector SubprocessFanout::runSync(const ScanOptions& opts, } if (!all_shards_succeeded) throw std::runtime_error("source worker failed before completing its shard"); + coverage_ = tuCoverage(files, all_tu_outcomes); // Global clone clustering on the merged summary set. Multiple workers // re-#include the same headers and emit summaries for those header diff --git a/src/cli/tu_path.cpp b/src/cli/tu_path.cpp new file mode 100644 index 0000000..1692ccf --- /dev/null +++ b/src/cli/tu_path.cpp @@ -0,0 +1,23 @@ +#include "fold/cli/tu_path.hpp" + +#include +#include + +namespace fold::cli { + +std::string normalizeTuPath(const std::string& path) { + if (path.empty()) + return path; + std::error_code error; + std::filesystem::path input(path); + std::filesystem::path absolute = + input.is_absolute() ? input : std::filesystem::absolute(input, error); + if (error) + return input.lexically_normal().string(); + auto canonical = std::filesystem::weakly_canonical(absolute, error); + if (!error) + return canonical.string(); + return absolute.lexically_normal().string(); +} + +} // namespace fold::cli diff --git a/src/cli/tu_quarantine.cpp b/src/cli/tu_quarantine.cpp index 828f722..05bb8db 100644 --- a/src/cli/tu_quarantine.cpp +++ b/src/cli/tu_quarantine.cpp @@ -21,21 +21,6 @@ bool hasSignalSuffix(const std::string& line, std::size_t colon) { } // namespace -std::string normalizeQuarantinePath(const std::string& path) { - if (path.empty()) - return path; - std::error_code error; - std::filesystem::path input(path); - std::filesystem::path absolute = - input.is_absolute() ? input : std::filesystem::absolute(input, error); - if (error) - return input.lexically_normal().string(); - auto canonical = std::filesystem::weakly_canonical(absolute, error); - if (!error) - return canonical.string(); - return absolute.lexically_normal().string(); -} - std::unordered_set loadQuarantine(const std::string& quarantine_dir) { std::unordered_set paths; if (quarantine_dir.empty()) @@ -61,7 +46,7 @@ std::unordered_set loadQuarantine(const std::string& quarantine_dir const auto colon = line.rfind(':'); std::string path = hasSignalSuffix(line, colon) ? line.substr(0, colon) : line; if (!path.empty()) - paths.insert(normalizeQuarantinePath(path)); + paths.insert(normalizeTuPath(path)); } return paths; } @@ -70,7 +55,7 @@ void appendQuarantineFailure(const std::string& quarantine_dir, const std::strin std::string_view cause, int code) { if (quarantine_dir.empty() || tu_path.empty()) return; - const std::string normalized = normalizeQuarantinePath(tu_path); + const std::string normalized = normalizeTuPath(tu_path); if (loadQuarantine(quarantine_dir).contains(normalized)) return; diff --git a/src/detect/always_condition.cpp b/src/detect/always_condition.cpp index 7668cb9..0aa55b9 100644 --- a/src/detect/always_condition.cpp +++ b/src/detect/always_condition.cpp @@ -22,6 +22,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/symbolic/assumption_provenance.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" @@ -87,80 +88,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx) return loc.isValid() && sm.isMacroBodyExpansion(loc); } -bool containsCallExpr(const clang::Stmt* stmt) { - if (!stmt) - return false; - struct Visitor : clang::RecursiveASTVisitor { - bool found = false; - bool VisitCallExpr(clang::CallExpr*) { - found = true; - return false; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.found; -} - -std::vector collectAssignedVars(const clang::Stmt* stmt) { - if (!stmt) - return {}; - struct Visitor : clang::RecursiveASTVisitor { - std::vector vars; - std::unordered_set seen; - - void add(const clang::VarDecl* vd) { - if (!vd) - return; - vd = vd->getCanonicalDecl(); - if (seen.insert(vd).second) - vars.push_back(vd); - } - - bool VisitBinaryOperator(clang::BinaryOperator* op) { - if (!op || !op->isAssignmentOp()) - return true; - const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(lhs)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - - bool VisitUnaryOperator(clang::UnaryOperator* op) { - if (!op || !op->isIncrementDecrementOp()) - return true; - const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(sub)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.vars; -} - -void appendAssignedVars(std::vector& vars, - const std::vector& extra) { - if (vars.empty()) { - vars = extra; - return; - } - std::unordered_set seen(vars.begin(), vars.end()); - for (const auto* vd : extra) { - if (vd && seen.insert(vd).second) - vars.push_back(vd); - } -} - -void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { - for (const clang::VarDecl* vd : vars) { - auto current = env.tryGet(vd); - if (!current || !current->is_bv()) - continue; - env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); - } - env.clearAccessPathFacts(); - env.markLoopHavoc(); -} +using detect::appendAssignedVars; +using detect::collectAssignedVars; +using detect::containsCallExpr; +using detect::havocAssignedVars; class AlwaysConditionWalker { public: @@ -351,44 +282,55 @@ class AlwaysConditionWalker { SymbolicEnv& env) { const bool opaque_loop = containsCallExpr(cond) || containsCallExpr(body) || containsCallExpr(inc); - std::vector assigned; - if (opaque_loop) { - assigned = collectAssignedVars(cond); - appendAssignedVars(assigned, collectAssignedVars(body)); - appendAssignedVars(assigned, collectAssignedVars(inc)); - } + std::vector assigned = collectAssignedVars(cond); + appendAssignedVars(assigned, collectAssignedVars(body)); + appendAssignedVars(assigned, collectAssignedVars(inc)); const z3::expr entry_path = env.currentPath(); + detect::LoopUnrollExits exits(body); for (int iter = 0; iter < budget_.loop_unroll; ++iter) { if (cond) { const EncodingPrecisionContext precision_before = env.tag(); z3::expr guard = encodeCondition(cond, ctx_, env); - if (precisionWorsened(precision_before, env)) + if (precisionWorsened(precision_before, env)) { + exits.guardNotModeled(); break; + } if (env.trackedAssumptions().empty()) { SourcePathAssumeOptions options{ .prune_infeasible = true, .timeout_ms = static_cast(budget_.per_query.count())}; auto assumed = SourcePathState{env}.assume(guard, options); - if (!assumed.truthy.has_value()) + if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value())) break; env = std::move(assumed.truthy->env()); + } else { + exits.guardNotModeled(); } + } else { + exits.guardNotModeled(); } - if (!body) + if (!body) { + exits.bodyStopped(); break; + } { ++loop_depth_; bool ok = walk(body, env); --loop_depth_; - if (!ok) + if (!ok) { + exits.bodyStopped(); break; + } } if (inc) { (void)encodeExpr(inc, ctx_, env); } } - if (opaque_loop) { - 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; diff --git a/src/detect/dead_branch.cpp b/src/detect/dead_branch.cpp index e5fe046..605fd49 100644 --- a/src/detect/dead_branch.cpp +++ b/src/detect/dead_branch.cpp @@ -23,6 +23,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/frontend/stable_identity.hpp" #include "fold/symbolic/assumption_provenance.hpp" #include "fold/symbolic/cfg_helpers.hpp" @@ -198,76 +199,10 @@ bool isMacroBodyStatement(const clang::Stmt* stmt, const clang::ASTContext& ctx) return loc.isValid() && sm.isMacroBodyExpansion(loc); } -bool containsCallExpr(const clang::Stmt* stmt) { - if (!stmt) - return false; - struct Visitor : clang::RecursiveASTVisitor { - bool found = false; - bool VisitCallExpr(clang::CallExpr*) { - found = true; - return false; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.found; -} - -std::vector collectAssignedVars(const clang::Stmt* stmt) { - if (!stmt) - return {}; - struct Visitor : clang::RecursiveASTVisitor { - std::vector vars; - std::unordered_set seen; - - void add(const clang::VarDecl* vd) { - if (!vd) - return; - vd = vd->getCanonicalDecl(); - if (seen.insert(vd).second) - vars.push_back(vd); - } - - bool VisitBinaryOperator(clang::BinaryOperator* op) { - if (!op || !op->isAssignmentOp()) - return true; - const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(lhs)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - - bool VisitUnaryOperator(clang::UnaryOperator* op) { - if (!op || !op->isIncrementDecrementOp()) - return true; - const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); - if (const auto* dre = clang::dyn_cast(sub)) - add(clang::dyn_cast(dre->getDecl())); - return true; - } - } visitor; - visitor.TraverseStmt(const_cast(stmt)); - return visitor.vars; -} - -void appendAssignedVars(std::vector& vars, - const std::vector& extra) { - std::unordered_set seen(vars.begin(), vars.end()); - for (const auto* vd : extra) { - if (vd && seen.insert(vd).second) - vars.push_back(vd); - } -} - -void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { - for (const clang::VarDecl* vd : vars) { - auto current = env.tryGet(vd); - if (!current || !current->is_bv()) - continue; - env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); - } - env.clearAccessPathFacts(); - env.markLoopHavoc(); -} +using detect::appendAssignedVars; +using detect::collectAssignedVars; +using detect::containsCallExpr; +using detect::havocAssignedVars; // Recursively walk the body, threading (env, path_predicate). At each IfStmt, // SAT-check each arm before descending. Branch state is forked so an @@ -373,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(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; diff --git a/src/detect/dead_statement.cpp b/src/detect/dead_statement.cpp index c786e5e..6ae51ab 100644 --- a/src/detect/dead_statement.cpp +++ b/src/detect/dead_statement.cpp @@ -204,7 +204,8 @@ class DeadStatementVisitor : public clang::RecursiveASTVisitorcheck(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::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, hazard); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, hazard); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -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::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; diff --git a/src/detect/double_free.cpp b/src/detect/double_free.cpp index a4e3ce5..645c541 100644 --- a/src/detect/double_free.cpp +++ b/src/detect/double_free.cpp @@ -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; diff --git a/src/detect/int_overflow.cpp b/src/detect/int_overflow.cpp index 73a692e..2d40fe1 100644 --- a/src/detect/int_overflow.cpp +++ b/src/detect/int_overflow.cpp @@ -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::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, unsafe); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, unsafe); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, unsafe); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -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::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::pair>> buildCounterexample(const z3::model& model, const z3::expr& lhs, const z3::expr& rhs, const clang::Expr* lhsExpr, const clang::Expr* rhsExpr, - bool isSourceSigned) { - auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned); - detect::appendUniqueBindings(bindings, - detect::collectModelBindings(model, rhs, isSourceSigned)); + bool isSourceSigned) const { + const auto types = detect::sourceIntTypesOf(current_fn_, ctx_); // source width/sign + auto bindings = detect::collectModelBindings(model, lhs, isSourceSigned, &types); + detect::appendUniqueBindings( + bindings, detect::collectModelBindings(model, rhs, isSourceSigned, &types)); std::string text; if (!bindings.empty()) { text = " (e.g., when " + detect::joinBindings(bindings) + ")"; diff --git a/src/detect/loop_havoc.cpp b/src/detect/loop_havoc.cpp new file mode 100644 index 0000000..ae8ec77 --- /dev/null +++ b/src/detect/loop_havoc.cpp @@ -0,0 +1,234 @@ +#include "fold/detect/loop_havoc.hpp" + +#include +#include +#include + +#include + +namespace fold::detect { + +bool containsCallExpr(const clang::Stmt* stmt) { + if (!stmt) + return false; + struct Visitor : clang::RecursiveASTVisitor { + bool found = false; + bool VisitCallExpr(clang::CallExpr*) { + found = true; + return false; + } + } visitor; + visitor.TraverseStmt(const_cast(stmt)); + return visitor.found; +} + +std::vector collectAssignedVars(const clang::Stmt* stmt) { + if (!stmt) + return {}; + struct Visitor : clang::RecursiveASTVisitor { + std::vector vars; + std::unordered_set seen; + + void add(const clang::VarDecl* vd) { + if (!vd) + return; + vd = vd->getCanonicalDecl(); + if (seen.insert(vd).second) + vars.push_back(vd); + } + + bool VisitBinaryOperator(clang::BinaryOperator* op) { + if (!op || !op->isAssignmentOp()) + return true; + const auto* lhs = op->getLHS()->IgnoreParenImpCasts(); + if (const auto* dre = clang::dyn_cast(lhs)) + add(clang::dyn_cast(dre->getDecl())); + return true; + } + + bool VisitUnaryOperator(clang::UnaryOperator* op) { + if (!op || !op->isIncrementDecrementOp()) + return true; + const auto* sub = op->getSubExpr()->IgnoreParenImpCasts(); + if (const auto* dre = clang::dyn_cast(sub)) + add(clang::dyn_cast(dre->getDecl())); + return true; + } + } visitor; + visitor.TraverseStmt(const_cast(stmt)); + return visitor.vars; +} + +void appendAssignedVars(std::vector& vars, + const std::vector& extra) { + std::unordered_set seen(vars.begin(), vars.end()); + for (const auto* vd : extra) { + if (vd && seen.insert(vd).second) + vars.push_back(vd); + } +} + +void havocAssignedVars(SymbolicEnv& env, const std::vector& vars) { + for (const clang::VarDecl* vd : vars) { + auto current = env.tryGet(vd); + if (!current || !current->is_bv()) + continue; + env.replace(vd, env.freshUnknown(current->get_sort().bv_size())); + } + env.clearAccessPathFacts(); + env.markLoopHavoc(); +} + +namespace { + +// Walks a loop body tracking how many loops/switches enclose each statement, +// so only a break 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(stmt) || clang::isa(stmt)) + return true; + if (clang::isa(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(stmt)) + return loop_depth == 0; + const bool loop = clang::isa(stmt) || clang::isa(stmt) || + clang::isa(stmt) || clang::isa(stmt); + const bool breakable = loop || clang::isa(stmt); + for (const clang::Stmt* child : stmt->children()) { + if (escapes(child, breakable_depth + (breakable ? 1 : 0), loop_depth + (loop ? 1 : 0))) + return true; + } + return false; +} + +// Stores that do not go through a plain variable: an array element, a member, +// or a dereferenced pointer. Havocking assigned variables does not reach that +// state. When the store's base is a named variable (`buf[i] = ...`, +// `s.f = ...`), that variable is reported so its whole value can be havocked; +// a store through an unknown pointer is only flagged. +struct MemoryWrites { + std::vector bases; + bool unknown_target = false; +}; + +MemoryWrites collectMemoryWrites(const clang::Stmt* stmt) { + struct Visitor : clang::RecursiveASTVisitor { + MemoryWrites writes; + std::unordered_set seen; + + void record(const clang::Expr* target) { + target = target->IgnoreParenImpCasts(); + const clang::Expr* base = nullptr; + if (const auto* sub = clang::dyn_cast(target)) + base = sub->getBase(); + else if (const auto* mem = clang::dyn_cast(target)) + base = mem->isArrow() ? nullptr : mem->getBase(); + else if (const auto* un = clang::dyn_cast(target); + un && un->getOpcode() == clang::UO_Deref) { + writes.unknown_target = true; + return; + } else if (const auto* arrow = clang::dyn_cast(target); + arrow && arrow->isArrow()) { + writes.unknown_target = true; + return; + } else { + return; + } + if (!base) { + writes.unknown_target = true; + return; + } + // Walk nested subscripts/members (`m[i][j]`, `a.b.c`) to the variable. + for (;;) { + base = base->IgnoreParenImpCasts(); + if (const auto* sub = clang::dyn_cast(base)) { + base = sub->getBase(); + continue; + } + if (const auto* mem = clang::dyn_cast(base); + mem && !mem->isArrow()) { + base = mem->getBase(); + continue; + } + break; + } + const auto* dre = clang::dyn_cast(base); + const auto* vd = dre ? clang::dyn_cast(dre->getDecl()) : nullptr; + // Subscripting a pointer variable writes through it, not into it. + if (!vd || vd->getType()->isPointerType()) { + writes.unknown_target = true; + return; + } + vd = vd->getCanonicalDecl(); + if (seen.insert(vd).second) + writes.bases.push_back(vd); + } + bool VisitBinaryOperator(clang::BinaryOperator* op) { + if (op && op->isAssignmentOp()) + record(op->getLHS()); + return true; + } + bool VisitUnaryOperator(clang::UnaryOperator* op) { + if (op && op->isIncrementDecrementOp()) + record(op->getSubExpr()); + return true; + } + } visitor; + if (stmt) + visitor.TraverseStmt(const_cast(stmt)); + return visitor.writes; +} + +} // namespace + +bool containsLoopEscape(const clang::Stmt* body) { return escapes(body, 0, 0); } + +LoopUnrollExits::LoopUnrollExits(const clang::Stmt* body) { + if (containsLoopEscape(body)) + exact_ = false; + auto writes = collectMemoryWrites(body); + memory_bases_ = std::move(writes.bases); + unknown_memory_write_ = writes.unknown_target; +} + +void LoopUnrollExits::havoc(SymbolicEnv& env, + const std::vector& vars) const { + havocAssignedVars(env, vars); + // Array element and member stores from the truncated unroll would survive + // the scalar havoc: replace each written aggregate with a fresh value of + // its sort. + static unsigned counter = 0; + auto fresh = [&](const z3::sort& sort) { + const std::string name = "loop_memory_havoc_" + std::to_string(counter++); + return env.ctx().constant(name.c_str(), sort); + }; + for (const clang::VarDecl* vd : memory_bases_) { + if (auto array = env.getArray(vd)) + env.updateArray(vd, fresh(array->array.get_sort())); + else if (auto current = env.tryGet(vd)) + env.replace(vd, fresh(current->get_sort())); + } + // A store through a pointer may have written any tracked heap array. + if (unknown_memory_write_) { + env.havocHeapArrays(); + env.markOverApproximated("loop-truncated-memory-write"); + } +} + +bool LoopUnrollExits::guard(bool may_continue, bool may_exit) { + if (!may_continue) { + exited_ = true; + return false; + } + // Both branches feasible: the loop may exit at this iteration, and that + // exit's state is not the one the unroll carries forward. + if (may_exit) + exact_ = false; + return true; +} + +} // namespace fold::detect diff --git a/src/detect/meson.build b/src/detect/meson.build index 5e5701a..92acc0d 100644 --- a/src/detect/meson.build +++ b/src/detect/meson.build @@ -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', diff --git a/src/detect/null_deref.cpp b/src/detect/null_deref.cpp index 9148ea7..3468e5a 100644 --- a/src/detect/null_deref.cpp +++ b/src/detect/null_deref.cpp @@ -36,6 +36,7 @@ #include "fold/ir/def_use.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/expr_hash.hpp" #include "fold/symbolic/heap_model.hpp" #include "fold/symbolic/safety_observer.hpp" @@ -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::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard); - } - if (artifact_result == z3::sat) { - m = solver_->get_model(); - } - } else { - if (result == z3::unsat) - rememberUnsatCore(*solver_, path, hazard); - if (result == z3::sat) - m = solver_->get_model(); } + // Only a reconciled verdict leaves `solver_` holding a matching model or core. + if (result == z3::unsat) + rememberUnsatCore(*solver_, path, hazard); + if (result == z3::sat) + m = solver_->get_model(); } else { local_s.set(":timeout", static_cast(budget_.per_query.count())); if (supportsParam(local_s.get_param_descrs(), "smt.threads")) { @@ -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::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; diff --git a/src/detect/oob_access.cpp b/src/detect/oob_access.cpp index dbff3cb..79fb441 100644 --- a/src/detect/oob_access.cpp +++ b/src/detect/oob_access.cpp @@ -34,6 +34,7 @@ #include "fold/detect/z3_model_support.hpp" #include "fold/fuzz/param_schema.hpp" #include "fold/symbolic/encoder.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/encoder_detail.hpp" #include "fold/symbolic/expr_hash.hpp" #include "fold/symbolic/heap_model.hpp" @@ -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(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(*solver_, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = + symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { @@ -323,6 +327,9 @@ class OOBObserver : public SafetyObserver { static_cast(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(local_s, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = + symbolic::recheckPortfolioVerdict(local_s, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( 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(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(*solver_, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { stats_.accumulate(solver_->statistics(), result); } - if (budget_.portfolio && result == z3::unsat) { - auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = solver_->check(assumptions); - stats_.elapsed += std::chrono::duration_cast( - std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(*solver_, path, hazard, detector_name); - } - } else if (result == z3::unsat) { + if (result == z3::unsat) { rememberUnsatCore(*solver_, path, hazard, detector_name); } } else { @@ -522,20 +534,14 @@ class OOBObserver : public SafetyObserver { s, assumptions, static_cast(budget_.per_query.count()), stats_) : symbolic::checkAdaptive(s, assumptions, static_cast(budget_.per_query.count())); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(s, assumptions, result, stats_); stats_.elapsed += std::chrono::duration_cast( std::chrono::steady_clock::now() - t0); if (stats_.profiling_enabled && !budget_.portfolio) { stats_.accumulate(s.statistics(), result); } - if (budget_.portfolio && result == z3::unsat) { - auto artifact_t0 = std::chrono::steady_clock::now(); - z3::check_result artifact_result = s.check(assumptions); - stats_.elapsed += std::chrono::duration_cast( - std::chrono::steady_clock::now() - artifact_t0); - if (artifact_result == z3::unsat) { - rememberUnsatCore(s, path, unsafe, detector_name); - } - } else if (result == z3::unsat) { + if (result == z3::unsat) { rememberUnsatCore(s, path, unsafe, detector_name); } } @@ -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> 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()) { diff --git a/src/detect/static_ptr_asymmetry.cpp b/src/detect/static_ptr_asymmetry.cpp index eaefebe..789aa2f 100644 --- a/src/detect/static_ptr_asymmetry.cpp +++ b/src/detect/static_ptr_asymmetry.cpp @@ -319,7 +319,9 @@ std::vector detectStaticPtrAsymmetryInContext(clang::ASTContext& ctx) { Finding f; f.kind = FindingKind::NullDeref; - f.confidence = Confidence::Proved; + // A cross-function discipline pattern, not a solver result: the + // unchecked function may be unreachable while the pointer is null. + f.confidence = Confidence::Heuristic; f.locations.push_back(locOf(ctx, loc, fd->getQualifiedNameAsString())); f.id = std::string("static-ptr-asymmetry:") + f.locations.front().file + ":" + std::to_string(f.locations.front().line) + ":" + diff --git a/src/detect/taint_track.cpp b/src/detect/taint_track.cpp index 6ec5c6a..69aa3dd 100644 --- a/src/detect/taint_track.cpp +++ b/src/detect/taint_track.cpp @@ -20,45 +20,47 @@ #include "fold/detect/model_validation.hpp" #include "fold/detect/security_walker.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" namespace fold::detect { namespace { -const std::vector kSources = {{"scanf", 1, "untrusted input"}, - {"fscanf", 2, "untrusted input"}, - {"sscanf", 2, "untrusted input"}, - {"recv", 1, "network input"}, - {"recvfrom", 1, "network input"}, - {"read", 1, "file/socket input"}, - {"fread", 0, "file input"}, - {"fgets", 0, "file input"}, - {"gets", 0, "file input"}, - {"getc", -1, "file input"}, - {"getchar", -1, "stdin input"}, - {"getenv", -1, "environment variable"}, - {"socket", -1, "network handle"}, - {"accept", -1, "network handle"}, - {"curl_easy_perform", -1, "network response"}, - {"curl_easy_getinfo", 2, "network metadata"}, - {"queryParam", -1, "URL query parameter"}, - {"get_query_param", -1, "URL query parameter"}, - {"get_form_param", -1, "Form data parameter"}, - {"read_header", -1, "HTTP header"}, - {"Query", -1, "Database query result"}, - {"get", -1, "Map/Request lookup"}, - {"readString", -1, "deserialized string"}, - {"readStringVector", -1, "deserialized string list"}, - {"readStringMap", -1, "deserialized string map"}, - {"readStringArray", 2, "deserialized string array"}, - {"fromJson", -1, "JSON deserialization source"}}; +const std::vector kSources = { + {"scanf", 1, "untrusted input"}, + {"fscanf", 2, "untrusted input"}, + {"sscanf", 2, "untrusted input"}, + {"recv", 1, "network input"}, + {"recvfrom", 1, "network input"}, + {"read", 1, "file/socket input"}, + {"fread", 0, "file input"}, + {"fgets", 0, "file input"}, + {"gets", 0, "file input"}, + {"getc", -1, "file input"}, + {"getchar", -1, "stdin input"}, + {"getenv", -1, "environment variable"}, + {"socket", -1, "network handle"}, + {"accept", -1, "network handle"}, + {"curl_easy_perform", -1, "network response"}, + {"curl_easy_getinfo", 2, "network metadata"}, + {"queryParam", -1, "URL query parameter", false}, + {"get_query_param", -1, "URL query parameter", false}, + {"get_form_param", -1, "Form data parameter", false}, + {"read_header", -1, "HTTP header", false}, + {"Query", -1, "Database query result", false}, + {"get", -1, "Map/Request lookup", false}, + {"readString", -1, "deserialized string", false}, + {"readStringVector", -1, "deserialized string list", false}, + {"readStringMap", -1, "deserialized string map", false}, + {"readStringArray", 2, "deserialized string array", false}, + {"fromJson", -1, "JSON deserialization source", false}}; const std::vector kSinks = { {"sqlite3_prepare_v2", 1, "SQL injection", taint_domain::kSql}, {"sqlite3_prepare_v3", 1, "SQL injection", taint_domain::kSql}, {"PQexecParams", 1, "SQL injection", taint_domain::kSql}, - {"execute", -1, "database execution", taint_domain::kSql}, - {"query", -1, "database query", taint_domain::kSql}, + {"execute", -1, "database execution", taint_domain::kSql, false}, + {"query", -1, "database query", taint_domain::kSql, false}, {"send", -1, "network transmission", taint_domain::kNetwork}, {"write", -1, "file/socket write", taint_domain::kNetwork}, {"open", 0, "path access", taint_domain::kPath}, @@ -218,8 +220,11 @@ std::string canonicalSinkName(const std::string& callee_name) { return isExecFamilySink(callee_name) ? "exec" : callee_name; } -bool sinkMatches(const TaintSink& entry, const std::string& callee_name) { - return entry.func == callee_name; +// A libc/POSIX entry matches only the C library function itself: a method or +// namespaced function that shares the name (`Shell::system`) is not the sink. +bool sinkMatches(const TaintSink& entry, const std::string& callee_name, + const clang::CallExpr* call) { + return entry.func == callee_name && (!entry.c_api || isCLibraryCallee(call)); } } // namespace @@ -276,7 +281,7 @@ void TaintTracker::onBinaryArith(BinOp op, const z3::expr& lhs, const z3::expr& bool TaintTracker::isSourceCall(const clang::CallExpr* call, const std::string& callee_name, TaintSource& source) const { for (const auto& entry : kSources) { - if (entry.func == callee_name) { + if (entry.func == callee_name && (!entry.c_api || isCLibraryCallee(call))) { if (callee_name == "get" && call) { if (const auto* callee = call->getDirectCallee()) { if (callee->isInStdNamespace()) { @@ -300,7 +305,7 @@ bool TaintTracker::isSourceCall(const clang::CallExpr* call, const std::string& bool TaintTracker::isSinkCall(const std::string& callee_name, TaintSink& sink) const { for (const auto& entry : kSinks) { - if (sinkMatches(entry, callee_name)) { + if (entry.func == callee_name) { sink = entry; return true; } @@ -675,7 +680,7 @@ void TaintTracker::onCallExpr(const fold::ir::Call& call_ir, bool matched_sink = false; for (const auto& sink : kSinks) { - if (!sinkMatches(sink, callee_name)) + if (!sinkMatches(sink, callee_name, call)) continue; matched_sink = true; bool tainted = false; diff --git a/src/detect/unreachable.cpp b/src/detect/unreachable.cpp index 35d3ae4..5e3f428 100644 --- a/src/detect/unreachable.cpp +++ b/src/detect/unreachable.cpp @@ -21,6 +21,7 @@ #include #include "fold/detect/incremental_cache.hpp" +#include "fold/detect/loop_havoc.hpp" #include "fold/symbolic/cfg_helpers.hpp" #include "fold/symbolic/encoder.hpp" #include "fold/symbolic/loop_bound_pin.hpp" @@ -230,32 +231,52 @@ class UnreachableBodyWalker { bool unrollLoop(const clang::Expr* cond, const clang::Stmt* body, const clang::Expr* inc, SymbolicEnv& env, z3::expr& path) { + std::vector assigned = detect::collectAssignedVars(cond); + detect::appendAssignedVars(assigned, detect::collectAssignedVars(body)); + detect::appendAssignedVars(assigned, detect::collectAssignedVars(inc)); + const z3::expr entry_path = path; + detect::LoopUnrollExits exits(body); for (int iter = 0; iter < budget_.loop_unroll; ++iter) { z3::expr body_path = path; if (cond) { const EncodingPrecisionContext precision_before = env.tag(); z3::expr guard = encodeCondition(cond, ctx_, env); - if (precisionWorsened(precision_before, env)) + if (precisionWorsened(precision_before, env)) { + exits.guardNotModeled(); break; + } if (env.trackedAssumptions().empty()) { SourcePathAssumeOptions options{ .prune_infeasible = true, .timeout_ms = static_cast(budget_.per_query.count())}; auto assumed = SourcePathState{env}.withPath(path).assume(guard, options); - if (!assumed.truthy.has_value()) + if (!exits.guard(assumed.truthy.has_value(), assumed.falsy.has_value())) break; env = std::move(assumed.truthy->env()); body_path = env.currentPath(); + } else { + exits.guardNotModeled(); } + } else { + exits.guardNotModeled(); } - if (!body) + if (!body) { + exits.bodyStopped(); break; - if (!walk(body, env, body_path)) + } + if (!walk(body, env, body_path)) { + exits.bodyStopped(); break; + } if (inc) { (void)encodeExpr(inc, ctx_, env); } } + // The same loop-exit soundness rule as dead-branch / always-condition. + if (!exits.exact()) { + exits.havoc(env, assigned); + path = entry_path; + } return true; } diff --git a/src/detect/unused_function.cpp b/src/detect/unused_function.cpp index 940f819..b07c544 100644 --- a/src/detect/unused_function.cpp +++ b/src/detect/unused_function.cpp @@ -219,7 +219,8 @@ std::vector detectUnusedFunctionsInContext(clang::ASTContext& ctx) { Finding f; f.kind = FindingKind::UnusedFunction; - f.confidence = Confidence::Proved; + // A call-graph fact read off the AST, not a solver result. + f.confidence = Confidence::Syntactic; f.locations.push_back(locOf(fd, ctx)); f.id = stableQualityFindingId("unused-function", stableFunctionId(fd)); f.message = "Static function `" + fd->getNameAsString() + diff --git a/src/detect/use_after_free.cpp b/src/detect/use_after_free.cpp index 6ed43df..3d8bc38 100644 --- a/src/detect/use_after_free.cpp +++ b/src/detect/use_after_free.cpp @@ -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& 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(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(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(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(budget_.per_query.count())); @@ -477,6 +494,8 @@ class UseAfterFreeObserver : public SafetyObserver { s, assumptions, static_cast(budget_.per_query.count()), stats_) : s.check(assumptions); + if (budget_.portfolio) + result = symbolic::recheckPortfolioVerdict(s, assumptions, result, 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; diff --git a/src/detect/z3_model_support.cpp b/src/detect/z3_model_support.cpp new file mode 100644 index 0000000..e7e0660 --- /dev/null +++ b/src/detect/z3_model_support.cpp @@ -0,0 +1,53 @@ +#include "fold/detect/z3_model_support.hpp" + +#include +#include +#include + +#include +#include + +namespace fold::detect { + +SourceIntTypes sourceIntTypesOf(const clang::FunctionDecl* fn, const clang::ASTContext& ctx) { + SourceIntTypes types; + if (fn == nullptr) + return types; + std::set ambiguous; + auto add = [&](const clang::VarDecl* vd) { + const clang::QualType type = vd->getType().getCanonicalType(); + if (!type->isIntegerType() || type->isDependentType() || vd->getName().empty()) + return; + const SourceIntType info{static_cast(ctx.getTypeSize(type)), + type->isSignedIntegerType()}; + const std::string name = vd->getNameAsString(); + const auto [it, inserted] = types.emplace(name, info); + if (!inserted && (it->second.width != info.width || it->second.is_signed != info.is_signed)) + ambiguous.insert(name); + }; + for (const auto* param : fn->parameters()) + add(param); + struct Visitor : clang::RecursiveASTVisitor { + std::function add; + bool VisitVarDecl(clang::VarDecl* vd) { + add(vd); + return true; + } + } visitor; + visitor.add = add; + if (fn->hasBody()) + visitor.TraverseStmt(fn->getBody()); + for (const auto& name : ambiguous) + types.erase(name); + return types; +} + +std::string formatSourceIntValue(uint64_t raw, SourceIntType type) { + if (type.width == 0 || type.width >= 64) + return type.is_signed ? std::to_string(static_cast(raw)) : std::to_string(raw); + const uint64_t truncated = raw & ((uint64_t{1} << type.width) - 1); + return type.is_signed ? formatSignedBitVector(truncated, type.width) + : std::to_string(truncated); +} + +} // namespace fold::detect diff --git a/src/report/findings_json_report.cpp b/src/report/findings_json_report.cpp index a257756..d8ca43a 100644 --- a/src/report/findings_json_report.cpp +++ b/src/report/findings_json_report.cpp @@ -7,15 +7,17 @@ namespace fold { -void writeFindingsJson(std::ostream& out, const std::vector& findings) { +void writeFindingsJson(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage) { json encoded = json::array(); for (const auto& finding : findings) encoded.push_back(findingToJson(finding)); - out << json{{"output_version", kFindingsJsonOutputVersion}, - {"tool", {{"name", "fold"}, {"version", foldVersion()}}}, - {"findings", encoded}} - .dump(2) - << '\n'; + json document{{"output_version", kFindingsJsonOutputVersion}, + {"tool", {{"name", "fold"}, {"version", foldVersion()}}}, + {"findings", encoded}}; + if (coverage != nullptr) + document["coverage"] = coverageToJson(*coverage); + out << document.dump(2) << '\n'; } } // namespace fold diff --git a/src/report/meson.build b/src/report/meson.build index 0998969..e343c53 100644 --- a/src/report/meson.build +++ b/src/report/meson.build @@ -7,6 +7,7 @@ fold_core_sources += files( 'findings_json_report.cpp', 'markdown.cpp', 'patch_writer.cpp', + 'scan_coverage.cpp', 'sarif.cpp', 'triage.cpp', ) diff --git a/src/report/sarif.cpp b/src/report/sarif.cpp index db365c0..0377718 100644 --- a/src/report/sarif.cpp +++ b/src/report/sarif.cpp @@ -404,7 +404,8 @@ void writeSarif(std::ostream& out, const std::vector& findings) { writeFilteredSarif(out, deduped); } -void writeFilteredSarif(std::ostream& out, const std::vector& findings) { +void writeFilteredSarif(std::ostream& out, const std::vector& findings, + const ScanCoverage* coverage) { const json tool = { {"driver", { @@ -421,7 +422,10 @@ void writeFilteredSarif(std::ostream& out, const std::vector& findings) out << R"({"$schema":"https://json.schemastore.org/sarif-2.1.0.json",)" R"("version":"2.1.0","runs":[{"tool":)" - << tool.dump() << R"(,"results":[)"; + << tool.dump(); + if (coverage != nullptr) + out << R"(,"invocations":)" << json::array({coverageToSarifInvocation(*coverage)}).dump(); + out << R"(,"results":[)"; for (std::size_t index = 0; index < findings.size(); ++index) { if (index != 0) out << ','; diff --git a/src/report/scan_coverage.cpp b/src/report/scan_coverage.cpp new file mode 100644 index 0000000..c25a636 --- /dev/null +++ b/src/report/scan_coverage.cpp @@ -0,0 +1,47 @@ +#include "fold/report/scan_coverage.hpp" + +namespace fold { + +void ScanCoverage::merge(const ScanCoverage& other) { + if (!other.tracked) + return; + tracked = true; + tus_attempted += other.tus_attempted; + tus_analyzed += other.tus_analyzed; + gaps.insert(gaps.end(), other.gaps.begin(), other.gaps.end()); +} + +nlohmann::json coverageToJson(const ScanCoverage& coverage) { + nlohmann::json gaps = nlohmann::json::array(); + for (const auto& gap : coverage.gaps) + gaps.push_back({{"file", gap.file}, {"reason", gap.reason}}); + return {{"tracked", coverage.tracked}, + {"complete", !coverage.incomplete()}, + {"tus_attempted", coverage.tus_attempted}, + {"tus_analyzed", coverage.tus_analyzed}, + {"gaps", gaps}}; +} + +nlohmann::json coverageToSarifInvocation(const ScanCoverage& coverage) { + nlohmann::json notifications = nlohmann::json::array(); + for (const auto& gap : coverage.gaps) { + notifications.push_back( + {{"level", "error"}, + {"descriptor", {{"id", "fold/coverage/" + gap.reason}}}, + {"message", {{"text", "translation unit not analyzed (" + gap.reason + ")"}}}, + {"locations", + nlohmann::json::array( + {{{"physicalLocation", {{"artifactLocation", {{"uri", gap.file}}}}}}})}}); + } + if (coverage.tracked && coverage.tus_attempted > 0 && coverage.tus_analyzed == 0 && + coverage.gaps.empty()) { + notifications.push_back({{"level", "error"}, + {"descriptor", {{"id", "fold/coverage/none-analyzed"}}}, + {"message", {{"text", "no translation unit was analyzed"}}}}); + } + return {{"executionSuccessful", !coverage.incomplete()}, + {"toolExecutionNotifications", notifications}, + {"properties", {{"coverage", coverageToJson(coverage)}}}}; +} + +} // namespace fold diff --git a/src/symbolic/encoder_callee_names.cpp b/src/symbolic/encoder_callee_names.cpp index 0e795a0..faede4f 100644 --- a/src/symbolic/encoder_callee_names.cpp +++ b/src/symbolic/encoder_callee_names.cpp @@ -7,6 +7,8 @@ #include #include +#include "fold/frontend/stable_identity.hpp" + namespace fold { std::string calleeName(const clang::CallExpr* ce) { @@ -61,6 +63,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(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 {}; diff --git a/src/symbolic/encoder_expr.cpp b/src/symbolic/encoder_expr.cpp index 06b3b7c..ce2cb40 100644 --- a/src/symbolic/encoder_expr.cpp +++ b/src/symbolic/encoder_expr.cpp @@ -611,6 +611,12 @@ z3::expr encodeExpr(ir::Expr expr_ir, const clang::ASTContext& ctx, SymbolicEnv& // is now empty — any unmigrated AST kind falls through to the // unsupported-node bail at the function end. + if (const auto* trait = dyn_cast(e)) { + if (auto value = symbolic::typeTraitConstant(ctx, trait)) + return markEncoded("UnaryExprOrTypeTraitExpr", + env.ctx().bv_val(static_cast(*value), kBitvecWidth)); + } + recordBailedNode(expr->getStmtClassName(), std::string("expr kind ") + expr->getStmtClassName()); recordPrecision(env, EncodingPrecision::UnsupportedNode, diff --git a/src/symbolic/encoder_expr_arms.cpp b/src/symbolic/encoder_expr_arms.cpp index d7a91fd..6d9a104 100644 --- a/src/symbolic/encoder_expr_arms.cpp +++ b/src/symbolic/encoder_expr_arms.cpp @@ -575,7 +575,10 @@ z3::expr encodeCallExprArm(const clang::CallExpr* ce, const clang::ASTContext& c } return returnCallValue(name, env.ctx().bv_val(0, kBitvecWidth), false); } - if (isMallocLikeCall(name)) { + // Heap models apply only to the C library functions, not to a project + // function or method that shares the name (`mine::free`, `Pool::free`). + const bool c_library_callee = isCLibraryCallee(ce); + if (c_library_callee && isMallocLikeCall(name)) { z3::expr size = env.ctx().bv_val(0, kBitvecWidth); bool is_stack = (name == "alloca" || name == "_alloca" || name == "__builtin_alloca"); if (name == "malloc" && ce->getNumArgs() >= 1) { @@ -606,7 +609,7 @@ z3::expr encodeCallExprArm(const clang::CallExpr* ce, const clang::ASTContext& c } return returnCallValue(name, ptr); } - if (isFreeCall(name) && ce->getNumArgs() >= 1) { + if (c_library_callee && isFreeCall(name) && ce->getNumArgs() >= 1) { z3::expr ptr = coerceToBv(env, arg_values[0]); bool known_region = env.heapModel().isTrackedPointer(ptr); bool already_freed = env.heapModel().isFreed(ptr); diff --git a/src/symbolic/encoder_type_queries.cpp b/src/symbolic/encoder_type_queries.cpp index 4072115..e948745 100644 --- a/src/symbolic/encoder_type_queries.cpp +++ b/src/symbolic/encoder_type_queries.cpp @@ -1,6 +1,7 @@ #include "fold/symbolic/encoder_type_queries.hpp" #include +#include #include #include "fold/symbolic/encoder.hpp" @@ -46,4 +47,19 @@ z3::expr byteWidthExpr(SymbolicEnv& env, const clang::ASTContext& ctx, const cla return env.ctx().bv_val(typeSizeBytes(ctx, qt), kBitvecWidth); } +std::optional typeTraitConstant(const clang::ASTContext& ctx, + const clang::UnaryExprOrTypeTraitExpr* expr) { + if (expr == nullptr || expr->isValueDependent() || expr->isTypeDependent()) + return std::nullopt; + clang::Expr::EvalResult result; + if (!expr->EvaluateAsInt(result, ctx) || !result.Val.isInt()) + return std::nullopt; + const llvm::APSInt& value = result.Val.getInt(); + if (value.isSigned() && value.isNegative()) + return std::nullopt; + if (value.getActiveBits() > 64) + return std::nullopt; + return value.getZExtValue(); +} + } // namespace fold::symbolic diff --git a/src/symbolic/summary_encoder.cpp b/src/symbolic/summary_encoder.cpp index d8c902f..841326c 100644 --- a/src/symbolic/summary_encoder.cpp +++ b/src/symbolic/summary_encoder.cpp @@ -21,6 +21,7 @@ #include "fold/detect/incremental_cache.hpp" #include "fold/detect/summary_store.hpp" #include "fold/symbolic/cfg_helpers.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/safety_observer.hpp" namespace fold { @@ -165,7 +166,7 @@ class SummaryMetadataCollector : public clang::RecursiveASTVisitorgetDirectCallee() : nullptr; if (!callee) return true; - std::string qname = qualifiedFunctionName(callee); + std::string qname = summaryStoreKey(callee); if (!qname.empty()) { callees.insert(qname); callee_decls.emplace(std::move(qname), callee); @@ -292,7 +293,7 @@ class SummaryPreconditionRecorder : public SafetyObserver { const z3::expr& path, const ir::SourceLoc& /*loc*/, const SymbolicEnv* /*env*/ = nullptr) override { const auto* call = call_ir.asClangCallExpr(); - const std::string callee_name = qualifiedCalleeName(call); + const std::string callee_name = summaryStoreKeyForCall(call); if (callee_name.empty()) return; const auto* summary = detect::SummaryStore::instance().lookup(callee_name); @@ -521,7 +522,7 @@ class SummaryWalker { return false; } if (const auto* ce = dyn_cast(stmt)) { - const std::string callee_name = qualifiedCalleeName(ce); + const std::string callee_name = summaryStoreKeyForCall(ce); if (!callee_name.empty()) { auto& store = detect::SummaryStore::instance(); const auto* summary = store.lookup(callee_name); @@ -569,7 +570,7 @@ class SummaryWalker { private: std::optional summarizeCallReturn(const clang::CallExpr* ce, const z3::expr& path) { - const std::string callee_name = qualifiedCalleeName(ce); + const std::string callee_name = summaryStoreKeyForCall(ce); if (callee_name.empty()) return std::nullopt; @@ -656,7 +657,7 @@ std::optional summarizeImpl(const clang::FunctionDecl* fd, params.push_back(p); std::vector exits; - SummaryWalker walker(ctx, env, exits, params, qualifiedFunctionName(fd)); + SummaryWalker walker(ctx, env, exits, params, summaryStoreKey(fd)); z3::expr path = env.ctx().bool_val(true); bool ok = walker.walk(fd->getBody(), path); SoundnessTag tag = env.tag(); @@ -695,7 +696,7 @@ std::optional computeSummaryForDefinition(const clang if (!def) return std::nullopt; - std::string qualified_name = qualifiedFunctionName(def); + std::string qualified_name = summaryStoreKey(def); if (qualified_name.empty()) return std::nullopt; @@ -807,7 +808,7 @@ summarizeLeafFunctionSymbolically(const clang::FunctionDecl* fd, const clang::AS SummaryPreconditionRecorder preconditions(ctx, env, raw_inputs, input_names); env.setObserver(&preconditions); std::vector exits; - SummaryWalker walker(ctx, env, exits, params, qualifiedFunctionName(fd), &preconditions); + SummaryWalker walker(ctx, env, exits, params, summaryStoreKey(fd), &preconditions); z3::expr path = env.ctx().bool_val(true); bool ok = walker.walk(fd->getBody(), path); @@ -899,7 +900,7 @@ summarizeLeafFunctionSymbolically(const clang::FunctionDecl* fd, const clang::AS SummaryMetadataCollector metadata; metadata.TraverseStmt(fd->getBody()); - const std::string caller_name = qualifiedFunctionName(fd); + const std::string caller_name = summaryStoreKey(fd); summary.reads_globals = std::move(metadata.reads_globals); summary.writes_globals = std::move(metadata.writes_globals); bool params_unchanged = can_emit_value_summary; @@ -943,7 +944,7 @@ const symbolic::SymbolicSummary* ensureSymbolicSummary(const clang::FunctionDecl if (!fd) return nullptr; - std::string qualified_name = qualifiedFunctionName(fd); + std::string qualified_name = summaryStoreKey(fd); if (qualified_name.empty()) return nullptr; diff --git a/src/symbolic/tactics.cpp b/src/symbolic/tactics.cpp index 77b3ff9..d05d3d3 100644 --- a/src/symbolic/tactics.cpp +++ b/src/symbolic/tactics.cpp @@ -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); diff --git a/tests/integration/meson.build b/tests/integration/meson.build index f0264dd..355da01 100644 --- a/tests/integration/meson.build +++ b/tests/integration/meson.build @@ -44,7 +44,10 @@ test_subprocess_fanout = executable( # fan-out can spawn it. fold_bin = meson.project_build_root() / 'src' / 'cli' / 'fold' test('subprocess_fanout', test_subprocess_fanout, - depends: [], # fold executable target lives in src/cli — referenced via path + # fold lives in src/cli and is referenced via path. The failure worker is + # build_by_default: false, so without this dependency `meson test` ran the + # recovery cases against a helper that was never built and failed them. + depends: [fanout_failure_worker], env: { 'FOLD_FIXTURES_DIR': join_paths(meson.current_source_dir(), '..', 'fixtures'), 'FOLD_WORKER_BINARY': fold_bin, diff --git a/tests/integration/test_cli_paths.cpp b/tests/integration/test_cli_paths.cpp index a4269a6..dd2577b 100644 --- a/tests/integration/test_cli_paths.cpp +++ b/tests/integration/test_cli_paths.cpp @@ -476,3 +476,47 @@ TEST_CASE("fold scan formats have truthful distinct contracts", "[cli][contract] REQUIRE(log_text.find(input_type_warning, log_text.find(input_type_warning) + 1) == std::string::npos); } + +TEST_CASE("fold scan fails when a translation unit is not analyzed", "[cli][coverage]") { + // A TU that failed to parse used to leave no trace: no findings, exit 0. + const std::string fold_bin = locateFoldBinary(); + if (fold_bin.empty()) { + WARN("could not locate fold binary; skipping CLI coverage test"); + return; + } + + TempDir dir; + const auto good = dir.path / "good.cpp"; + const auto broken = dir.path / "broken.cpp"; + writeFile(good, "int add(int a, int b) { return a + b; }\n"); + writeFile(broken, "#include \"does_not_exist.h\"\nint f(int x) { return x; }\n"); + + const auto scan = [&](const std::filesystem::path& source, const std::string& format, + const std::filesystem::path& report) { + const std::string command = "\"" + fold_bin + "\" --quiet scan --detectors div-by-zero " + + "--format " + format + " \"" + source.string() + "\" > \"" + + report.string() + "\" 2>/dev/null"; + return commandExitCode(std::system(command.c_str())); + }; + + SECTION("clean TU: complete coverage, exit 0 (control)") { + const auto report = dir.path / "good.json"; + REQUIRE(scan(good, "findings-json", report) == 0); + const auto json = nlohmann::json::parse(readFile(report)); + CHECK(json["coverage"]["complete"] == true); + CHECK(json["coverage"]["tus_analyzed"] == 1); + } + SECTION("broken TU: gap in findings JSON, exit 2") { + const auto report = dir.path / "broken.json"; + REQUIRE(scan(broken, "findings-json", report) == 2); + const auto json = nlohmann::json::parse(readFile(report)); + CHECK(json["coverage"]["complete"] == false); + CHECK(json["coverage"]["gaps"][0]["reason"] == "compile-errors"); + } + SECTION("broken TU: SARIF on stdout stays parseable and records the failure") { + const auto report = dir.path / "broken.sarif"; + REQUIRE(scan(broken, "sarif", report) == 2); + const auto sarif = nlohmann::json::parse(readFile(report)); + CHECK(sarif["runs"][0]["invocations"][0]["executionSuccessful"] == false); + } +} diff --git a/tests/integration/test_cross_tu_security.cpp b/tests/integration/test_cross_tu_security.cpp index a2c4e82..793c284 100644 --- a/tests/integration/test_cross_tu_security.cpp +++ b/tests/integration/test_cross_tu_security.cpp @@ -1,4 +1,7 @@ +#include +#include #include +#include #include #include @@ -21,6 +24,7 @@ #include "fold/detect/summary_store.hpp" #include "fold/frontend/comp_db.hpp" #include "fold/ir/call_graph.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" namespace { @@ -37,6 +41,28 @@ struct TempDir { ~TempDir() { std::filesystem::remove_all(path); } }; +// SummaryStore key (USR-based) of the function `name` defined in `path`, +// computed from the same file the scan parsed. +std::string summaryKeyIn(const std::filesystem::path& path, const std::string& name) { + std::ifstream in(path); + const std::string code((std::istreambuf_iterator(in)), std::istreambuf_iterator()); + auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, path.string()); + if (!unit) + return {}; + struct Finder : clang::RecursiveASTVisitor { + std::string name; + const clang::FunctionDecl* found = nullptr; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (!found && fd->getNameAsString() == name) + found = fd; + return true; + } + } finder; + finder.name = name; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + return fold::summaryStoreKey(finder.found); +} + void writeFile(const std::filesystem::path& path, const std::string& content) { std::ofstream(path) << content; } @@ -478,8 +504,10 @@ TEST_CASE("symbolic summary priming reaches recursive SCC fixpoint", "[scan][sum auto result = fold::cli::runDetectorsOnShard(*db, opts, {caller.string(), callee.string()}, /*include_clone_clustering=*/false); - const auto* a_summary = fold::detect::SummaryStore::instance().lookup("a"); - const auto* b_summary = fold::detect::SummaryStore::instance().lookup("b"); + const auto* a_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(caller, "a")); + const auto* b_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(callee, "b")); REQUIRE(b_summary != nullptr); REQUIRE(a_summary != nullptr); REQUIRE(!a_summary->param_pre.empty()); @@ -520,10 +548,10 @@ TEST_CASE("symbolic summaries distinguish internal linkage functions by file", (void)fold::cli::runDetectorsOnShard(*db, opts, {unsafe.string(), safe.string()}, /*include_clone_clustering=*/false); - const auto* unsafe_summary = fold::detect::SummaryStore::instance().lookup( - std::string("require_nonzero@") + unsafe.string()); - const auto* safe_summary = fold::detect::SummaryStore::instance().lookup( - std::string("require_nonzero@") + safe.string()); + const auto* unsafe_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(unsafe, "require_nonzero")); + const auto* safe_summary = + fold::detect::SummaryStore::instance().lookup(summaryKeyIn(safe, "require_nonzero")); REQUIRE(unsafe_summary != nullptr); REQUIRE(safe_summary != nullptr); diff --git a/tests/integration/test_mcp_stdio.cpp b/tests/integration/test_mcp_stdio.cpp index 75de10e..922fd30 100644 --- a/tests/integration/test_mcp_stdio.cpp +++ b/tests/integration/test_mcp_stdio.cpp @@ -57,13 +57,19 @@ struct TempDir { std::filesystem::path path; TempDir() + // Must stay under the working directory: the MCP server rejects paths + // outside its workspace root. : path(std::filesystem::current_path() / (".fold-mcp-test-" + std::to_string(std::chrono::steady_clock::now().time_since_epoch().count()))) { std::filesystem::create_directories(path); } - ~TempDir() { std::filesystem::remove_all(path); } + // Non-throwing: a destructor that throws during unwinding terminates. + ~TempDir() { + std::error_code ec; + std::filesystem::remove_all(path, ec); + } }; void writeFile(const std::filesystem::path& path, const std::string& content) { diff --git a/tests/integration/test_subprocess_fanout.cpp b/tests/integration/test_subprocess_fanout.cpp index b941e83..88c172f 100644 --- a/tests/integration/test_subprocess_fanout.cpp +++ b/tests/integration/test_subprocess_fanout.cpp @@ -172,6 +172,60 @@ TEST_CASE("SubprocessFanout single worker == serial path", "[fanout][unit]") { REQUIRE(parallel.size() == serial.findings.size()); } +TEST_CASE("quarantined TUs are coverage gaps in serial and fan-out scans", + "[fanout][quarantine][coverage]") { + // A TU skipped because a prior run quarantined it was not analysed. The + // serial path dropped it from the attempted set (a complete scan with it + // missing); the fan-out path reported it as frontend-failed. + auto fixtures = locateFixtures(); + writeCompileDb(fixtures); + std::string err; + auto db = fold::loadCompilationDatabase(fixtures, err); + REQUIRE(db); + auto files = db->getAllFiles(); + REQUIRE(files.size() == 3); + + const auto unique = std::to_string(std::chrono::steady_clock::now().time_since_epoch().count()); + const auto quarantine = + std::filesystem::temp_directory_path() / ("fold-quarantine-coverage-" + unique); + fold::cli::appendQuarantine(quarantine.string(), files[0], SIGSEGV); + + fold::cli::ScanOptions opts; + opts.compile_db = fixtures; + opts.detectors = {"clone"}; + opts.min_body_stmts = 1; + opts.quarantine_dir = quarantine.string(); + + auto quarantinedGap = [&](const fold::ScanCoverage& coverage) { + CHECK(coverage.tus_attempted == 3); + CHECK(coverage.tus_analyzed == 2); + REQUIRE(coverage.gaps.size() == 1); + CHECK(fold::cli::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{"fanout-test:after.cpp", "fanout-test:before.cpp"}); const auto quarantined = fold::cli::loadQuarantine(quarantine.string()); - REQUIRE(quarantined.contains(fold::cli::normalizeQuarantinePath(files[1]))); - REQUIRE(quarantined.contains(fold::cli::normalizeQuarantinePath(files[2]))); + REQUIRE(quarantined.contains(fold::cli::normalizeTuPath(files[1]))); + REQUIRE(quarantined.contains(fold::cli::normalizeTuPath(files[2]))); std::ifstream input(quarantine / "quarantine.txt"); const std::string records((std::istreambuf_iterator(input)), std::istreambuf_iterator()); diff --git a/tests/unit/meson.build b/tests/unit/meson.build index c50faf8..0fe30c2 100644 --- a/tests/unit/meson.build +++ b/tests/unit/meson.build @@ -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', diff --git a/tests/unit/test_encoder_callee_names.cpp b/tests/unit/test_encoder_callee_names.cpp index 9cee950..25c4b8b 100644 --- a/tests/unit/test_encoder_callee_names.cpp +++ b/tests/unit/test_encoder_callee_names.cpp @@ -153,3 +153,30 @@ TEST_CASE("qualifiedCalleeName resolves through a direct CallExpr", TEST_CASE("qualifiedCalleeName returns empty for null", "[encoder][callee_names][qualified]") { REQUIRE(fold::qualifiedCalleeName(nullptr).empty()); } + +TEST_CASE("isCLibraryCallee: only C library functions, never members or namespaced lookalikes", + "[encoder-callee-names][library]") { + auto unit = parse("extern \"C\" void free(void*);\n" + "namespace std { using ::free; }\n" + "namespace mine { void free(void*) {} }\n" + "struct Pool { void free(void*) {} };\n" + "void global_helper(void*) {}\n" + "void f(void* p, Pool& pool, void (*fp)(void*)) {\n" + " free(p);\n" + " std::free(p);\n" + " mine::free(p);\n" + " pool.free(p);\n" + " global_helper(p);\n" + " fp(p);\n" + "}\n"); + REQUIRE(unit); + const auto calls = collectCalls(*unit, "f"); + REQUIRE(calls.size() == 6); + CHECK(fold::isCLibraryCallee(calls[0])); // ::free (extern "C") + CHECK(fold::isCLibraryCallee(calls[1])); // std::free resolves to ::free + CHECK_FALSE(fold::isCLibraryCallee(calls[2])); // mine::free + CHECK_FALSE(fold::isCLibraryCallee(calls[3])); // Pool::free + CHECK_FALSE(fold::isCLibraryCallee(calls[4])); // global C++ function, not extern "C" + CHECK_FALSE(fold::isCLibraryCallee(calls[5])); // indirect call + CHECK_FALSE(fold::isCLibraryCallee(nullptr)); +} diff --git a/tests/unit/test_int_overflow.cpp b/tests/unit/test_int_overflow.cpp index c0f7d88..88174a1 100644 --- a/tests/unit/test_int_overflow.cpp +++ b/tests/unit/test_int_overflow.cpp @@ -9,6 +9,7 @@ #include "fold/detect/cross_tu_cache.hpp" #include "fold/detect/int_overflow.hpp" +#include "fold/detect/z3_model_support.hpp" #include "fold/report/finding.hpp" #include "fold/symbolic/budget.hpp" @@ -669,3 +670,30 @@ TEST_CASE("int-overflow: CFString size output contract proves length-1 safe", std::fprintf(stderr, "CFSTRING-POS findings=%zu\n", findings.size()); REQUIRE(findings.empty()); } + +TEST_CASE("int-overflow: witnesses use the source type's width and signedness", + "[int_overflow][witness]") { + // Symbols are 64-bit; only the low 32 bits carry an `int`. Witnesses were + // printed from the whole bitvector, e.g. a=2147483648 or + // a=-9223372034707292160 for `int a`. + auto r = run("int sum(int a, int b) { int x = a + b; x += a; return x; }\n"); + REQUIRE_FALSE(r.findings.empty()); + for (const auto& f : r.findings) { + for (const auto& [name, value] : f.evidence.counterexample) { + const long long v = std::stoll(value); + CHECK(v >= -2147483648LL); + CHECK(v <= 2147483647LL); + } + } +} + +TEST_CASE("formatSourceIntValue truncates and signs", "[int_overflow][witness]") { + using fold::detect::formatSourceIntValue; + CHECK(formatSourceIntValue(0x80000000ULL, {32, true}) == "-2147483648"); + CHECK(formatSourceIntValue(0x8000000080000000ULL, {32, true}) == "-2147483648"); + CHECK(formatSourceIntValue(0xBFFFFFFFULL, {32, true}) == "-1073741825"); + CHECK(formatSourceIntValue(0x1FFFFFFFFULL, {32, false}) == "4294967295"); + CHECK(formatSourceIntValue(7, {32, true}) == "7"); + CHECK(formatSourceIntValue(0xFFFFFFFFFFFFFFFFULL, {64, true}) == "-1"); + CHECK(formatSourceIntValue(0xFFULL, {8, true}) == "-1"); +} diff --git a/tests/unit/test_library_callee_identity.cpp b/tests/unit/test_library_callee_identity.cpp new file mode 100644 index 0000000..d2890e3 --- /dev/null +++ b/tests/unit/test_library_callee_identity.cpp @@ -0,0 +1,136 @@ +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/cross_tu_cache.hpp" +#include "fold/detect/double_free.hpp" +#include "fold/detect/taint_track.hpp" +#include "fold/detect/use_after_free.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" + +// Library models (malloc/free, taint sources and sinks) were selected by the +// callee's bare identifier, so a project function that merely shares a libc +// name was modeled as libc: `mine::free(p)` followed by `free(p)` was a Proved +// double-free. Models now require the resolved declaration to be a C library +// function (global scope, namespace std, or extern "C"; never a member). + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::size_t countKind(const std::vector& findings, fold::FindingKind kind) { + std::size_t n = 0; + for (const auto& f : findings) + if (f.kind == kind) + ++n; + return n; +} + +std::vector runDoubleFree(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectDoubleFreeInContext(unit->getASTContext(), b, s); +} + +std::vector runUseAfterFree(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + return fold::detectUseAfterFreeInContext(unit->getASTContext()); +} + +std::vector runTaint(const std::string& code) { + fold::detect::CrossTUCache::instance().clear(); + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectTaintTrackInContext(unit->getASTContext(), b, s); +} + +const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n" + "extern \"C\" void free(void*);\n"; + +} // namespace + +TEST_CASE("heap model: a namespaced function named free is not libc free", + "[library-callee][double-free]") { + const std::string code = kLibc + "namespace mine { inline void free(void*) {} }\n" + "int f() {\n" + " int* p = static_cast(malloc(sizeof(int)));\n" + " if (!p) return 0;\n" + " *p = 1;\n" + " mine::free(p);\n" + " int v = *p;\n" + " free(p);\n" + " return v;\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); + CHECK(countKind(runUseAfterFree(code), fold::FindingKind::UseAfterFree) == 0); +} + +TEST_CASE("heap model: a member function named free is not libc free", + "[library-callee][double-free]") { + const std::string code = kLibc + "struct Pool { void free(void*) {} };\n" + "void f(Pool& pool) {\n" + " void* p = malloc(8);\n" + " if (!p) return;\n" + " pool.free(p);\n" + " free(p);\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); +} + +TEST_CASE("heap model: libc free twice is still a double free", "[library-callee][double-free]") { + // Negative control: the fix must not drop the real model. + const std::string code = kLibc + "void f() {\n" + " void* p = malloc(8);\n" + " if (!p) return;\n" + " free(p);\n" + " free(p);\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 1); +} + +TEST_CASE("taint: a member function named system is not a command sink", + "[library-callee][taint]") { + const std::string code = "extern \"C\" char* getenv(const char*);\n" + "struct Shell { int system(const char*) { return 0; } };\n" + "int f(Shell& sh) { return sh.system(getenv(\"CMD\")); }\n"; + CHECK(countKind(runTaint(code), fold::FindingKind::TaintTrack) == 0); +} + +TEST_CASE("taint: libc system with tainted input is still a sink", "[library-callee][taint]") { + const std::string code = "extern \"C\" char* getenv(const char*);\n" + "extern \"C\" int system(const char*);\n" + "int f() { return system(getenv(\"CMD\")); }\n"; + CHECK(countKind(runTaint(code), fold::FindingKind::TaintTrack) == 1); +} + +TEST_CASE("heap model: a global C++ function named free is not libc free", + "[library-callee][double-free][global]") { + // A global-scope C++ overload (no extern "C", not in a system header) is a + // project function that shares libc's name, not the library function. + const std::string code = kLibc + "struct Obj { int v; };\n" + "void free(Obj*) {}\n" + "int f() {\n" + " Obj* o = static_cast(malloc(sizeof(Obj)));\n" + " if (!o) return 0;\n" + " o->v = 1;\n" + " free(o);\n" + " int v = o->v;\n" + " free(o);\n" + " return v;\n" + "}\n"; + CHECK(countKind(runDoubleFree(code), fold::FindingKind::DoubleFree) == 0); + CHECK(countKind(runUseAfterFree(code), fold::FindingKind::UseAfterFree) == 0); +} diff --git a/tests/unit/test_loop_exit_soundness.cpp b/tests/unit/test_loop_exit_soundness.cpp new file mode 100644 index 0000000..744a80c --- /dev/null +++ b/tests/unit/test_loop_exit_soundness.cpp @@ -0,0 +1,226 @@ +#include +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/always_condition.hpp" +#include "fold/detect/dead_branch.hpp" +#include "fold/detect/loop_havoc.hpp" +#include "fold/detect/unreachable.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/modeling_options.hpp" + +// Bounded loop unrolling followed only the path on which the loop guard stays +// true. When the guard could also be false (a symbolic bound), that early exit +// was dropped, so the state after the loop was "the loop ran loop_unroll +// times" and conditions on it were reported as Proved dead / always-true or +// always-false. These cases were all Proved before the fix. + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::vector runDead(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectDeadBranchesInContext(unit->getASTContext(), b, s); +} + +std::vector runAlways(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectAlwaysConditionsInContext(unit->getASTContext(), b, s); +} + +std::vector runUnreachable(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + return fold::detectUnreachableCodeInContext(unit->getASTContext(), b, s); +} + +std::size_t proved(const std::vector& findings) { + std::size_t n = 0; + for (const auto& f : findings) + if (f.confidence == fold::Confidence::Proved) + ++n; + return n; +} + +// Symbolic bound: the loop may run zero times, or more than loop_unroll times. +const std::string kSymbolicLoops = + "int a0(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s == 0) return 7; return 0; }\n" + "int a1(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s > 100) return 7; return 0; }\n" + "int a2(unsigned n) { int s = 0; while (n > 0) { s += 1; n--; }" + " if (s == 0) return 7; return 0; }\n" + "int a3(unsigned n) { int s = 0; for (unsigned i = 0; i < n; ++i) { s += 1; }" + " if (s > 5) return 1; return 0; }\n"; + +// Constant bound within the unroll budget: the unroll sees the loop's only +// exit, so the post-loop state is exact and a genuinely dead branch stays +// provable. +const std::string kExactLoop = "int e(int x) { int s = 0; for (int i = 0; i < 3; ++i) { s += 1; }" + " if (s == 7) return -1; return s + x; }\n"; + +// Constant bound, but a `break` offers a second way out whose state the +// unroll does not follow. +const std::string kBreakLoop = + "int b(int x) { int s = 0; for (int i = 0; i < 3; ++i) { if (x == i) break; s += 1; }" + " if (s == 0) return -1; return s; }\n"; + +} // namespace + +TEST_CASE("dead: a branch after a symbolic-bound loop is not proven dead", "[dead][loop]") { + CHECK(proved(runDead(kSymbolicLoops)) == 0); +} + +TEST_CASE("always-condition: a condition after a symbolic-bound loop is not proven constant", + "[always][loop]") { + CHECK(proved(runAlways(kSymbolicLoops)) == 0); +} + +TEST_CASE("unreachable: code after a symbolic-bound loop is not proven unreachable", + "[unreachable][loop]") { + CHECK(proved(runUnreachable(kSymbolicLoops)) == 0); +} + +TEST_CASE("dead: a loop the unroll exits exactly keeps its precision", "[dead][loop]") { + // Negative control for the fix: havocking every loop would silence this too. + CHECK(proved(runDead(kExactLoop)) == 1); +} + +TEST_CASE("dead: a break out of a constant loop is an exit the unroll did not follow", + "[dead][loop]") { + CHECK(proved(runDead(kBreakLoop)) == 0); +} + +namespace { + +// The body of the first loop statement in the translation unit. +const clang::Stmt* firstLoopBody(clang::ASTUnit& unit) { + struct Finder : clang::RecursiveASTVisitor { + const clang::Stmt* body = nullptr; + bool VisitForStmt(clang::ForStmt* s) { + if (!body) + body = s->getBody(); + return true; + } + bool VisitWhileStmt(clang::WhileStmt* s) { + if (!body) + body = s->getBody(); + return true; + } + } finder; + finder.TraverseDecl(unit.getASTContext().getTranslationUnitDecl()); + return finder.body; +} + +bool escapesIn(const std::string& code) { + auto unit = parse(code); + REQUIRE(unit); + const auto* body = firstLoopBody(*unit); + REQUIRE(body); + return fold::detect::containsLoopEscape(body); +} + +} // namespace + +TEST_CASE("loop escape: a break out of the loop escapes; a nested one does not", "[loop_havoc]") { + CHECK(escapesIn("void f(int x){ for(int i=0;i<3;++i){ if(x) break; } }")); + CHECK(escapesIn("void f(int x){ while(x){ goto out; } out:; }")); + CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ for(;;){ break; } } }")); + CHECK_FALSE(escapesIn( + "void f(int x){ for(int i=0;i<3;++i){ switch(x){ case 1: break; default: break; } } }")); + CHECK_FALSE(escapesIn("void f(int x){ for(int i=0;i<3;++i){ x += i; } }")); +} + +TEST_CASE("loop exits: exact only when the unroll leaves along the only exit", "[loop_havoc]") { + SECTION("guard falsified after iterations that could not exit") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(/*may_continue=*/true, /*may_exit=*/false)); + CHECK_FALSE(exits.guard(/*may_continue=*/false, /*may_exit=*/true)); + CHECK(exits.exact()); + } + SECTION("an iteration that could also exit makes the state inexact") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(true, true)); + CHECK_FALSE(exits.guard(false, true)); + CHECK_FALSE(exits.exact()); + } + SECTION("the unroll budget running out is not an exit") { + fold::detect::LoopUnrollExits exits(nullptr); + CHECK(exits.guard(true, false)); + CHECK_FALSE(exits.exact()); + } + SECTION("an unmodeled guard or a stopped body is never exact") { + fold::detect::LoopUnrollExits unmodeled(nullptr); + unmodeled.guardNotModeled(); + CHECK_FALSE(unmodeled.guard(false, true)); + CHECK_FALSE(unmodeled.exact()); + fold::detect::LoopUnrollExits stopped(nullptr); + stopped.bodyStopped(); + CHECK_FALSE(stopped.guard(false, true)); + CHECK_FALSE(stopped.exact()); + } +} + +// Review finding: a `continue` arm is dropped by the walkers (the arm always +// exits the iteration), so iterations that took it are not modeled even when +// the guard sequence is exact. `x == 2` holds only when y == 0. +const std::string kContinueLoop = + "int c(int y) { int x = 0; for (int i = 0; i < 2; i++) { if (y) continue; x++; }" + " if (x == 2) return 1; return 0; }\n"; + +TEST_CASE("a loop with continue is not treated as an exact unroll", "[loop][continue]") { + CHECK(proved(runAlways(kContinueLoop)) == 0); + CHECK(proved(runDead(kContinueLoop)) == 0); + CHECK(proved(runUnreachable(kContinueLoop)) == 0); +} + +// Review finding: a truncated unroll havocs scalar variables but kept array +// element writes from the partial unroll. With n == 0, buf[0] is never set. +const std::string kArrayWriteLoop = "int w(unsigned n) { int buf[4] = {0, 0, 0, 0};" + " for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;" + " if (buf[0] == 1) return 1; return 0; }\n"; + +// The same through a pointer: the store may have reached any heap array. +const std::string kPointerWriteLoop = + "#include \n" + "int pw(unsigned n) { int* buf = static_cast(std::calloc(4, sizeof(int)));" + " if (!buf) return 0;" + " for (unsigned i = 0; i < n && i < 4; i++) buf[i] = 1;" + " int r = buf[0] == 1 ? 1 : 0; std::free(buf); return r; }\n"; + +TEST_CASE("array writes in a truncated loop do not survive into proofs", "[loop][memory]") { + CHECK(proved(runAlways(kArrayWriteLoop)) == 0); + CHECK(proved(runDead(kArrayWriteLoop)) == 0); + CHECK(proved(runUnreachable(kArrayWriteLoop)) == 0); + CHECK(proved(runAlways(kPointerWriteLoop)) == 0); + CHECK(proved(runDead(kPointerWriteLoop)) == 0); +} + +// Review finding: unreachable omitted the opaque-loop rule. A call can change +// the loop variable through a pointer, which assigned-variable collection +// does not see. +const std::string kOpaqueCallLoop = "void advance(int* p);\n" + "int u() { int i = 0; while (i < 3) { advance(&i); i++; }" + " if (i != 3) { int k = i * 2; return k; } return 0; }\n"; + +TEST_CASE("unreachable havocs loops that contain calls", "[unreachable][loop][opaque]") { + CHECK(proved(runUnreachable(kOpaqueCallLoop)) == 0); + CHECK(proved(runDead(kOpaqueCallLoop)) == 0); +} diff --git a/tests/unit/test_model_validation.cpp b/tests/unit/test_model_validation.cpp index baa2461..1428499 100644 --- a/tests/unit/test_model_validation.cpp +++ b/tests/unit/test_model_validation.cpp @@ -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); +} diff --git a/tests/unit/test_proved_requires_exact_model.cpp b/tests/unit/test_proved_requires_exact_model.cpp new file mode 100644 index 0000000..f6c4989 --- /dev/null +++ b/tests/unit/test_proved_requires_exact_model.cpp @@ -0,0 +1,211 @@ +#include +#include +#include + +#include +#include +#include +#include +#include + +#include "fold/detect/dead_statement.hpp" +#include "fold/detect/double_free.hpp" +#include "fold/detect/oob_access.hpp" +#include "fold/detect/static_ptr_asymmetry.hpp" +#include "fold/detect/unused_function.hpp" +#include "fold/detect/use_after_free.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_type_queries.hpp" + +// docs/research/soundness.md: `proved` means an exact bounded model +// established the property. These detectors assigned Proved without one: +// from a heap-model flag (double-free), a cross-function pattern +// (static-ptr-asymmetry), an AST fact (unused-function, dead-statement), or a +// SAT result whose encoding precision was never checked (stdlib OOB copy, +// use-after-free under an unknown call). + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::optional confidenceOf(const std::vector& findings, + fold::FindingKind kind) { + for (const auto& f : findings) + if (f.kind == kind) + return f.confidence; + return std::nullopt; +} + +const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n" + "extern \"C\" void free(void*);\n" + "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n"; + +} // namespace + +TEST_CASE("double-free without a solver query is Heuristic", "[proved-contract][double-free]") { + auto unit = + parse(kLibc + "void f() { void* p = malloc(8); if (!p) return; free(p); free(p); }"); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto c = confidenceOf(fold::detectDoubleFreeInContext(unit->getASTContext(), b, s), + fold::FindingKind::DoubleFree); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("static-ptr-asymmetry is a pattern, not a proof", "[proved-contract][static-ptr]") { + auto unit = parse("struct S { int v; };\n" + "static S* g_state = nullptr;\n" + "int checked() { if (!g_state) return 0; return g_state->v; }\n" + "int unchecked() { return g_state->v; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectStaticPtrAsymmetryInContext(unit->getASTContext()), + fold::FindingKind::NullDeref); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("unused static function is an AST fact: Syntactic", "[proved-contract][unused]") { + auto unit = parse("static int helper(int x) { return x + 1; }\nint api(int x) { return x; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectUnusedFunctionsInContext(unit->getASTContext()), + fold::FindingKind::UnusedFunction); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Syntactic); +} + +TEST_CASE("statement after return is an AST fact: Syntactic", "[proved-contract][dead-stmt]") { + auto unit = parse("int f(int x) { return x; x += 1; }\n"); + REQUIRE(unit); + const auto c = confidenceOf(fold::detectDeadStatementsInContext(unit->getASTContext()), + fold::FindingKind::DeadStatement); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Syntactic); +} + +TEST_CASE("stdlib copy overflow without encoding precision is Heuristic", + "[proved-contract][oob]") { + auto unit = parse(kLibc + "void f(const char* src) { char buf[8]; memcpy(buf, src, 16); }"); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto c = confidenceOf(fold::detectOOBAccessInContext(unit->getASTContext(), b, s), + fold::FindingKind::OOBAccess); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); +} + +TEST_CASE("heap use-after-free keeps Proved only on an exact encoding", "[proved-contract][uaf]") { + // The SAT-backed heap use-after-free surfaces through the OOB detector + // (`uaf-access`). + auto uafConfidence = [](const std::string& code) -> std::optional { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) + if (f.id.rfind("uaf-access:", 0) == 0) + return f.confidence; + return std::nullopt; + }; + SECTION("exact: stays Proved (control)") { + const auto c = uafConfidence( + kLibc + "int f() { int* p = (int*)malloc(sizeof(int)); free(p); return p[0]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Proved); + } + SECTION("an over-approximated operation on the path: Heuristic") { + const auto c = uafConfidence(kLibc + "extern int opaque(int);\n" + "int f(int k) { int* p = (int*)malloc(sizeof(int));" + " int n = opaque(k); free(p); return p[n - n]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); + } +} + +namespace { + +// Value of the first sizeof/alignof in `code`, as the encoder would see it. +std::optional firstTypeTrait(const std::string& code, bool c_mode = false) { + auto unit = c_mode ? clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c11"}, "input.c") + : parse(code); + REQUIRE(unit); + struct Finder : clang::RecursiveASTVisitor { + const clang::UnaryExprOrTypeTraitExpr* found = nullptr; + bool VisitUnaryExprOrTypeTraitExpr(clang::UnaryExprOrTypeTraitExpr* e) { + if (!found) + found = e; + return true; + } + } finder; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + REQUIRE(finder.found); + return fold::symbolic::typeTraitConstant(unit->getASTContext(), finder.found); +} + +} // namespace + +TEST_CASE("type-trait constants are exact for complete types only", "[proved-contract][sizeof]") { + // sizeof was an unsupported node, which marked every `malloc(sizeof(T))` + // path imprecise and so could never back a Proved finding. + CHECK(firstTypeTrait("unsigned long f() { return sizeof(int); }") == 4u); + CHECK(firstTypeTrait( + "struct S { char c; double d; }; unsigned long f() { return sizeof(S); }") == 16u); + CHECK(firstTypeTrait("unsigned long f() { return alignof(double); }") == 8u); + // A VLA's size is a runtime value: not a constant. + CHECK_FALSE(firstTypeTrait("unsigned long f(int n) { char buf[n]; return sizeof(buf); }", + /*c_mode=*/true) + .has_value()); +} + +TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding", + "[proved-contract][oob]") { + auto oobConfidence = [](const std::string& code) -> std::optional { + auto unit = parse(code); + REQUIRE(unit); + fold::SolverBudget b; + fold::SolverStats s; + for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) + if (f.id.rfind("oob-access:", 0) == 0) + return f.confidence; + return std::nullopt; + }; + SECTION("exact: stays Proved (control)") { + const auto c = oobConfidence("int f() { int a[4] = {0}; return a[4]; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Proved); + } + SECTION("an over-approximated operation on the path: Heuristic") { + const auto c = oobConfidence("extern int opaque(int);\n" + "int f(int k) { int a[4] = {0}; int n = opaque(k);" + " if (n > 2) return a[4]; return 0; }"); + REQUIRE(c.has_value()); + CHECK(*c == fold::Confidence::Heuristic); + } +} + +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); +} diff --git a/tests/unit/test_scan_coverage.cpp b/tests/unit/test_scan_coverage.cpp new file mode 100644 index 0000000..c66e8a3 --- /dev/null +++ b/tests/unit/test_scan_coverage.cpp @@ -0,0 +1,112 @@ +#include +#include +#include +#include +#include +#include + +#include "fold/cli/clang_shard_tu.hpp" +#include "fold/report/findings_json_report.hpp" +#include "fold/report/sarif.hpp" +#include "fold/report/scan_coverage.hpp" + +// A TU the front end could not parse used to vanish: the report had no trace +// of it and the scan exited 0, indistinguishable from a clean scan. Coverage +// now records every requested TU that was not analyzed on a clean AST. + +namespace { + +std::string tmp(const std::string& name) { + return (std::filesystem::temp_directory_path() / name).string(); +} + +} // namespace + +TEST_CASE("tuCoverage classifies every requested TU", "[coverage]") { + const std::vector requested{tmp("ok.cpp"), tmp("broken.cpp"), tmp("missing.cpp"), + tmp("slow.cpp")}; + const std::vector outcomes{ + {tmp("ok.cpp"), ""}, + {tmp("broken.cpp"), "compile-errors"}, + {tmp("slow.cpp"), "timeout"}, + }; + const auto coverage = fold::cli::tuCoverage(requested, outcomes); + CHECK(coverage.tracked); + CHECK(coverage.tus_attempted == 4); + CHECK(coverage.tus_analyzed == 1); + REQUIRE(coverage.gaps.size() == 3); + CHECK(coverage.gaps[0].file == tmp("broken.cpp")); + CHECK(coverage.gaps[0].reason == "compile-errors"); + CHECK(coverage.gaps[1].file == tmp("missing.cpp")); + CHECK(coverage.gaps[1].reason == "frontend-failed"); + CHECK(coverage.gaps[2].reason == "timeout"); + CHECK(coverage.incomplete()); +} + +TEST_CASE("tuCoverage matches paths across spellings", "[coverage]") { + // The compile DB may spell a path differently than the front end does. + const auto dir = std::filesystem::temp_directory_path(); + const std::string dotted = (dir / "sub" / ".." / "a.cpp").string(); + const auto coverage = fold::cli::tuCoverage({dotted}, {{(dir / "a.cpp").string(), ""}}); + CHECK(coverage.tus_analyzed == 1); + CHECK_FALSE(coverage.incomplete()); +} + +TEST_CASE("coverage: complete, untracked and empty scans", "[coverage]") { + SECTION("every TU analyzed is complete (control)") { + const auto coverage = fold::cli::tuCoverage({tmp("a.cpp")}, {{tmp("a.cpp"), ""}}); + CHECK_FALSE(coverage.incomplete()); + } + SECTION("an untracked lane is never incomplete") { + fold::ScanCoverage coverage; + coverage.tus_attempted = 3; + CHECK_FALSE(coverage.incomplete()); + } + SECTION("attempted TUs with none analyzed is incomplete even without gaps") { + fold::ScanCoverage coverage; + coverage.tracked = true; + coverage.tus_attempted = 2; + CHECK(coverage.incomplete()); + } + SECTION("merge sums counts and keeps gaps; an untracked side is ignored") { + auto a = fold::cli::tuCoverage({tmp("a.cpp")}, {{tmp("a.cpp"), ""}}); + const auto b = fold::cli::tuCoverage({tmp("b.cpp")}, {}); + a.merge(b); + a.merge(fold::ScanCoverage{}); + CHECK(a.tus_attempted == 2); + CHECK(a.tus_analyzed == 1); + CHECK(a.gaps.size() == 1); + } +} + +TEST_CASE("reports carry coverage", "[coverage][report]") { + const auto coverage = + fold::cli::tuCoverage({tmp("broken.cpp")}, {{tmp("broken.cpp"), "compile-errors"}}); + SECTION("SARIF: invocation is unsuccessful and names the TU") { + std::ostringstream out; + fold::writeFilteredSarif(out, {}, &coverage); + const auto sarif = nlohmann::json::parse(out.str()); + const auto& invocation = sarif["runs"][0]["invocations"][0]; + CHECK(invocation["executionSuccessful"] == false); + const auto& note = invocation["toolExecutionNotifications"][0]; + CHECK(note["level"] == "error"); + CHECK(note["locations"][0]["physicalLocation"]["artifactLocation"]["uri"] == + tmp("broken.cpp")); + CHECK(invocation["properties"]["coverage"]["tus_analyzed"] == 0); + } + SECTION("findings JSON: coverage object") { + std::ostringstream out; + fold::writeFindingsJson(out, {}, &coverage); + const auto report = nlohmann::json::parse(out.str()); + CHECK(report["coverage"]["complete"] == false); + CHECK(report["coverage"]["gaps"][0]["reason"] == "compile-errors"); + } + SECTION("no coverage argument leaves the documents unchanged") { + std::ostringstream sarif_out; + fold::writeFilteredSarif(sarif_out, {}); + CHECK_FALSE(nlohmann::json::parse(sarif_out.str())["runs"][0].contains("invocations")); + std::ostringstream json_out; + fold::writeFindingsJson(json_out, {}); + CHECK_FALSE(nlohmann::json::parse(json_out.str()).contains("coverage")); + } +} diff --git a/tests/unit/test_summary_key_identity.cpp b/tests/unit/test_summary_key_identity.cpp new file mode 100644 index 0000000..5447813 --- /dev/null +++ b/tests/unit/test_summary_key_identity.cpp @@ -0,0 +1,141 @@ +#include +#include +#include + +#include +#include +#include +#include + +#include "fold/detect/null_deref.hpp" +#include "fold/detect/summary_store.hpp" +#include "fold/report/finding.hpp" +#include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" +#include "fold/symbolic/summary.hpp" +#include "fold/symbolic/summary_encoder.hpp" + +// Function summaries were stored under the qualified name, which overloads +// share: `take(int*, int)` (dereferences p) and `take(int*, long)` (checks p) +// both mapped to "take", so whichever was summarized first answered for both. +// A caller of the null-checking overload then inherited a nonnull +// precondition it does not have, and vice versa. Summaries are now keyed by +// the declaration's USR. + +namespace { + +std::unique_ptr parse(const std::string& code) { + return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp"); +} + +std::vector definitionsNamed(clang::ASTUnit& unit, + const std::string& name) { + struct Finder : clang::RecursiveASTVisitor { + std::string name; + std::vector found; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (fd->getNameAsString() == name && fd->isThisDeclarationADefinition()) + found.push_back(fd); + return true; + } + } finder; + finder.name = name; + finder.TraverseDecl(unit.getASTContext().getTranslationUnitDecl()); + return finder.found; +} + +bool requiresNonNull(const fold::symbolic::SymbolicSummary* summary, unsigned index) { + if (summary == nullptr) + return false; + const auto it = summary->param_pre.find(index); + if (it == summary->param_pre.end()) + return false; + for (const auto& term : it->second) + if (term.kind == "nonnull") + return true; + return false; +} + +} // namespace + +TEST_CASE("overloads get separate summaries", "[summary-key]") { + fold::detect::SummaryStore::instance().clear(); + auto unit = parse("int take(int* p, int) { return *p; }\n" + "int take(int* p, long) { return p ? *p : 0; }\n"); + REQUIRE(unit); + const auto defs = definitionsNamed(*unit, "take"); + REQUIRE(defs.size() == 2); + const auto& ctx = unit->getASTContext(); + + SECTION("dereferencing overload first") { + CHECK(requiresNonNull(fold::ensureSymbolicSummary(defs[0], ctx), 0)); + CHECK_FALSE(requiresNonNull(fold::ensureSymbolicSummary(defs[1], ctx), 0)); + } + SECTION("null-checking overload first") { + CHECK_FALSE(requiresNonNull(fold::ensureSymbolicSummary(defs[1], ctx), 0)); + CHECK(requiresNonNull(fold::ensureSymbolicSummary(defs[0], ctx), 0)); + } + fold::detect::SummaryStore::instance().clear(); +} + +TEST_CASE("summary keys: identity across redeclarations, not across names", "[summary-key]") { + auto unit = parse("int f(int* p);\n" + "int f(int* p) { return *p; }\n" + "namespace a { int g(int* p) { return *p; } }\n" + "namespace b { int g(int* p) { return p ? *p : 0; } }\n"); + REQUIRE(unit); + struct Finder : clang::RecursiveASTVisitor { + std::vector f_decls; + std::vector g_defs; + bool VisitFunctionDecl(clang::FunctionDecl* fd) { + if (fd->getNameAsString() == "f") + f_decls.push_back(fd); + if (fd->getNameAsString() == "g") + g_defs.push_back(fd); + return true; + } + } finder; + finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl()); + REQUIRE(finder.f_decls.size() == 2); + REQUIRE(finder.g_defs.size() == 2); + CHECK(fold::summaryStoreKey(finder.f_decls[0]) == fold::summaryStoreKey(finder.f_decls[1])); + CHECK(fold::summaryStoreKey(finder.g_defs[0]) != fold::summaryStoreKey(finder.g_defs[1])); + CHECK_FALSE(fold::summaryStoreKey(finder.f_decls[0]).empty()); + CHECK(fold::summaryStoreKey(nullptr).empty()); +} + +TEST_CASE("null-deref: a cross-TU call uses its own overload's summary", + "[summary-key][null-deref]") { + // TU 1 defines both overloads and summarizes them (the dereferencing one + // last). TU 2 sees only declarations, so its call resolves through the + // store alone, and passes null to the overload that checks. + const std::string defs = "int take(int* p, long) { return p ? *p : 0; }\n" + "int take(int* p, int) { return *p; }\n"; + const std::string caller = "int take(int* p, long);\n" + "int take(int* p, int);\n" + "int caller() { int* q = nullptr; return take(q, 1L); }\n" + "int control() { int* q = nullptr; return take(q, 1); }\n"; + fold::detect::SummaryStore::instance().clear(); + auto defs_unit = parse(defs); + REQUIRE(defs_unit); + for (const auto* fd : definitionsNamed(*defs_unit, "take")) + (void)fold::ensureSymbolicSummary(fd, defs_unit->getASTContext()); + + auto caller_unit = parse(caller); + REQUIRE(caller_unit); + fold::SolverBudget b; + fold::SolverStats s; + const auto findings = fold::detectNullDerefInContext(caller_unit->getASTContext(), b, s); + fold::detect::SummaryStore::instance().clear(); + std::size_t in_caller = 0; + std::size_t in_control = 0; + for (const auto& f : findings) { + if (!f.locations.empty() && f.locations.front().line == 3) + ++in_caller; + if (!f.locations.empty() && f.locations.front().line == 4) + ++in_control; + } + CHECK(in_caller == 0); + // Control: the dereferencing overload's precondition still applies. + CHECK(in_control == 1); +} diff --git a/tests/unit/test_symbolic_summary.cpp b/tests/unit/test_symbolic_summary.cpp index cabf182..b14b3c4 100644 --- a/tests/unit/test_symbolic_summary.cpp +++ b/tests/unit/test_symbolic_summary.cpp @@ -11,6 +11,7 @@ #include "fold/detect/null_deref.hpp" #include "fold/detect/summary_store.hpp" #include "fold/symbolic/budget.hpp" +#include "fold/symbolic/encoder_callee_names.hpp" #include "fold/symbolic/summary_encoder.hpp" namespace { @@ -37,7 +38,7 @@ void primeLeafSummary(clang::ASTUnit& unit, const std::string& name) { REQUIRE(fd != nullptr); auto summary = fold::summarizeLeafFunctionSymbolically(fd, ctx); REQUIRE(summary); - fold::detect::SummaryStore::instance().store(name, *summary); + fold::detect::SummaryStore::instance().store(fold::summaryStoreKey(fd), *summary); } } // namespace diff --git a/tests/unit/test_tu_quarantine.cpp b/tests/unit/test_tu_quarantine.cpp index e345e0c..893cdb8 100644 --- a/tests/unit/test_tu_quarantine.cpp +++ b/tests/unit/test_tu_quarantine.cpp @@ -36,7 +36,7 @@ TEST_CASE("TU quarantine loads signal suffixes and ignores comments", "[cli][qua const auto paths = fold::cli::loadQuarantine(temp.path().string()); REQUIRE(paths.size() == 1); - CHECK(paths.contains(fold::cli::normalizeQuarantinePath(source.string()))); + CHECK(paths.contains(fold::cli::normalizeTuPath(source.string()))); } TEST_CASE("TU quarantine append is normalized and idempotent", "[cli][quarantine]") { @@ -51,11 +51,11 @@ TEST_CASE("TU quarantine append is normalized and idempotent", "[cli][quarantine const auto paths = fold::cli::loadQuarantine(temp.path().string()); REQUIRE(paths.size() == 1); - CHECK(paths.contains(fold::cli::normalizeQuarantinePath(source.string()))); + CHECK(paths.contains(fold::cli::normalizeTuPath(source.string()))); std::ifstream input(temp.path() / "quarantine.txt"); std::string line; REQUIRE(std::getline(input, line)); - CHECK(line == fold::cli::normalizeQuarantinePath(source.string()) + "\tsignal:6"); + CHECK(line == fold::cli::normalizeTuPath(source.string()) + "\tsignal:6"); CHECK_FALSE(std::getline(input, line)); }