fd4a68dfff
Unit + integration coverage for the session's work: incremental project graph/index, pcode encoder, unreachable/dead-branch, equiv/cross-TU, div-by-zero/sign-conversion/int-truncation, use-after-free, quality-precision, scan-router profile, source TU runner, detector plan, and the eval fixtures.
98 lines
3.6 KiB
C++
98 lines
3.6 KiB
C++
#include <clang/Frontend/ASTUnit.h>
|
|
#include <clang/Tooling/Tooling.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <memory>
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
#include "fold/detect/unreachable.hpp"
|
|
#include "fold/report/finding.hpp"
|
|
#include "fold/symbolic/budget.hpp"
|
|
#include "fold/symbolic/modeling_options.hpp"
|
|
|
|
namespace {
|
|
|
|
std::unique_ptr<clang::ASTUnit> parse(const std::string& code) {
|
|
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
|
|
}
|
|
|
|
std::vector<fold::Finding>
|
|
runUnreachable(const std::string& code, const fold::ModelingOptions& m = fold::ModelingOptions{}) {
|
|
auto unit = parse(code);
|
|
REQUIRE(unit);
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
return fold::detectUnreachableCodeInContext(unit->getASTContext(), b, s, m);
|
|
}
|
|
|
|
std::vector<fold::Finding> runUnreachableWithStats(const std::string& code,
|
|
fold::SolverStats& out_stats) {
|
|
auto unit = parse(code);
|
|
REQUIRE(unit);
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectUnreachableCodeInContext(unit->getASTContext(), b, s);
|
|
out_stats = s;
|
|
return findings;
|
|
}
|
|
|
|
std::size_t countUnreachable(const std::vector<fold::Finding>& fs) {
|
|
std::size_t n = 0;
|
|
for (const auto& f : fs)
|
|
if (f.kind == fold::FindingKind::Unreachable)
|
|
++n;
|
|
return n;
|
|
}
|
|
|
|
// A statement after an unconditional return is unreachable.
|
|
constexpr const char* kAfterReturn = "int f(){ return 1; int x = 2; return x; }";
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("unreachable: code after return is flagged Proved", "[unreachable]") {
|
|
auto findings = runUnreachable(kAfterReturn);
|
|
REQUIRE(countUnreachable(findings) >= 1);
|
|
for (const auto& f : findings)
|
|
if (f.kind == fold::FindingKind::Unreachable)
|
|
REQUIRE(f.confidence == fold::Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("unreachable: no-exit-sibling function is prechecked safe", "[unreachable][prefilter]") {
|
|
// A function whose compounds never have an always-exits child followed by
|
|
// a later sibling cannot produce an unreachable finding; the walker is
|
|
// skipped exactly and the precheck counter rises.
|
|
fold::SolverStats stats;
|
|
auto findings =
|
|
runUnreachableWithStats("int f(int x){ if (x > 0) return x; return -x; }", stats);
|
|
REQUIRE(countUnreachable(findings) == 0);
|
|
CHECK(stats.functions_prechecked_safe >= 1);
|
|
}
|
|
|
|
TEST_CASE("unreachable: freestanding wiring is a parity no-op", "[unreachable][freestanding]") {
|
|
// The loop-bound pin does not downgrade unreachable findings (they are not
|
|
// UNSAT proofs over a loop bound) — the toggle is parity here, by design.
|
|
fold::ModelingOptions on;
|
|
on.suppress_loop_bound_always_conditions = true;
|
|
on.havoc_external_symbols = true;
|
|
on.havoc_statics_at_entry = true;
|
|
auto base = runUnreachable(kAfterReturn);
|
|
auto preset = runUnreachable(kAfterReturn, on);
|
|
REQUIRE(countUnreachable(preset) == countUnreachable(base));
|
|
for (const auto& f : preset)
|
|
if (f.kind == fold::FindingKind::Unreachable)
|
|
REQUIRE(f.confidence == fold::Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("unreachable: prior imprecision does not hide exact post-return code",
|
|
"[unreachable][precision]") {
|
|
auto findings =
|
|
runUnreachable("extern int g(); int f(){ g(); return 1; int x = 2; return x; }");
|
|
REQUIRE(countUnreachable(findings) >= 1);
|
|
}
|
|
|
|
TEST_CASE("unreachable: false loop guard suppresses unreachable code inside the body",
|
|
"[unreachable][loop]") {
|
|
auto findings = runUnreachable("int f(){ while(false){ return 1; int x = 2; } return 0; }");
|
|
REQUIRE(countUnreachable(findings) == 0);
|
|
}
|