080bf9655f
Extend ir::Loop classification: a monotone single-induction-variable for-loop with a symbolic bound (e.g. `for (i=0; i<n; ++i)`) is now Affine (was General). The walker summarizes Affine loops like Counted ones — bind the induction variable to a fresh symbolic, assert its start bound plus the loop condition (encoded to a Z3 bool) as path constraints, walk the body once — exposing high-index OOB that bounded unroll misses. Findings are over-approximations (LoopHavoc/heuristic), never proved. Net effect on the gate: oob recall 0.531 -> 0.559, F1 0.637 -> 0.652 (precision dips 0.796 -> 0.782) — a contract-sanctioned over-approximation tradeoff. Also regenerate bench/fp-baseline.json deterministically from a clean run: the prior committed oob numbers (0.574) were not reproducible (transient warm-state artifact); fresh runs are now bit-identical, so the gate is reliable. Tests: test_ir_loop (affine classification), test_loop_summary (symbolic-bound OOB exposed, not proved). Suite green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
65 lines
2.9 KiB
C++
65 lines
2.9 KiB
C++
// B2: counted-loop summarization. When a counted loop's trip count exceeds the
|
|
// unroll bound, the induction variable is bound to its full closed-form range
|
|
// and the body is walked once, so an in-body OOB at a high index is exposed
|
|
// (bounded unroll would only see i = 0,1,2 and miss it). Findings from the
|
|
// summarized walk are over-approximations and carry lower (heuristic)
|
|
// confidence, never Proved.
|
|
#include <clang/Frontend/ASTUnit.h>
|
|
#include <clang/Tooling/Tooling.h>
|
|
|
|
#include <algorithm>
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <memory>
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
#include "fold/detect/cross_tu_cache.hpp"
|
|
#include "fold/detect/oob_access.hpp"
|
|
#include "fold/report/finding.hpp"
|
|
#include "fold/symbolic/budget.hpp"
|
|
|
|
namespace {
|
|
|
|
std::vector<fold::Finding> run(const std::string& code) {
|
|
// Cross-TU cache is a singleton; clear it so a prior case's function
|
|
// summary (these cases all define `f`) cannot leak buffer bounds across
|
|
// cases the way separate `fold scan` invocations never would.
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
|
|
REQUIRE(unit);
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
return fold::detectOOBAccessInContext(unit->getASTContext(), b, s);
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("loop-summary: high-index OOB in a counted loop is found", "[loop][oob][summary]") {
|
|
// i reaches 99; a[i] is out of bounds for i >= 10. Bounded unroll (3) only
|
|
// sees a[0..2] and misses this; the summarized full range [0,99] exposes it.
|
|
auto findings = run("void f(){ int a[10]; for (int i = 0; i < 100; ++i) a[i] = i; }");
|
|
REQUIRE(findings.size() >= 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
|
|
// Over-approximation: must NOT be reported as a proof.
|
|
REQUIRE(findings[0].confidence != fold::Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("loop-summary: affine (symbolic-bound) loop exposes potential OOB",
|
|
"[loop][oob][summary]") {
|
|
// `i < n` with n a parameter: i can reach >= 10 when n > 10, so a[i] is a
|
|
// potential overflow. The affine summary binds i to [0, n) and exposes it
|
|
// (bounded unroll sees only i=0,1,2). Over-approximation -> not Proved.
|
|
auto findings = run("void f(int n){ int a[10]; for (int i = 0; i < n; ++i) a[i] = i; }");
|
|
REQUIRE(findings.size() >= 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
|
|
REQUIRE(findings[0].confidence != fold::Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("loop-summary: in-bounds counted loop is not flagged", "[loop][oob][summary]") {
|
|
// i in [0,99], a has 100 elements -> every access in bounds -> no finding.
|
|
auto findings = run("void f(){ int a[100]; for (int i = 0; i < 100; ++i) a[i] = i; }");
|
|
bool any_oob = std::any_of(findings.begin(), findings.end(), [](const fold::Finding& f) {
|
|
return f.kind == fold::FindingKind::OOBAccess;
|
|
});
|
|
REQUIRE_FALSE(any_oob);
|
|
}
|