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.
60 lines
2.2 KiB
C++
60 lines
2.2 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/sign_conversion.hpp"
|
|
#include "fold/report/finding.hpp"
|
|
#include "fold/symbolic/budget.hpp"
|
|
|
|
namespace {
|
|
|
|
struct TestResult {
|
|
std::vector<fold::Finding> findings;
|
|
fold::SolverStats stats;
|
|
};
|
|
|
|
TestResult run(const std::string& code) {
|
|
auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
|
|
REQUIRE(unit);
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectSignConversionInContext(unit->getASTContext(), b, s);
|
|
return {std::move(findings), s};
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("sign-conversion: signed to unsigned param conversion is latent",
|
|
"[sign][signed-to-unsigned]") {
|
|
auto [findings, stats] = run("unsigned f(int x){ unsigned y = x; return y; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::SignConversion);
|
|
// Conversion of a function parameter is caller-precondition-dependent
|
|
// (mirrors div-by-zero / int-overflow latent contract): the callee alone
|
|
// cannot prove a negative value is reachable.
|
|
REQUIRE(findings[0].evidence.latent);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Latent);
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
}
|
|
|
|
TEST_CASE("sign-conversion: unsigned to signed is flagged", "[sign][unsigned-to-signed]") {
|
|
auto [findings, stats] = run("int f(unsigned x){ int y = x; return y; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::SignConversion);
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
}
|
|
|
|
TEST_CASE("sign-conversion: havoc-backed SAT result is heuristic", "[sign][havoc][precision]") {
|
|
auto [findings, stats] = run("extern void mutate(int&); unsigned f(){ int x = 0; mutate(x); "
|
|
"unsigned y = x; return y; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
|
|
REQUIRE(findings[0].evidence.proof_mode == "over-approximated");
|
|
REQUIRE(stats.sat == 1);
|
|
}
|