6134bb3c16
`(d & (d-1)) == 0 ? low & (d-1) : low % d` (simeon sketch_bucket) flagged `low % d` as division-by-zero, but the guard `(0 & -1) == 0` is TRUE when d==0, so the `%` arm is unreachable for a zero divisor. Teach conditionProvesNonZero that `x & (x-1)` clears the lowest set bit (zero iff x is 0 or a power of two): * `(x & (x-1)) == 0` false arm -> x != 0 * `(x & (x-1)) != 0` true arm -> x != 0 Also route the same check through analyzeDivCallee so the callsite precondition for the guarded divisor param is suppressed in the same TU. Verified: simeon.cpp:48 `proved` finding gone; positive repro 1->0, bare `a % d` still fires; 59 div-by-zero tests + full suite 137/137.
600 lines
27 KiB
C++
600 lines
27 KiB
C++
#include <clang/Tooling/Tooling.h>
|
|
|
|
#include <catch2/catch_test_macros.hpp>
|
|
#include <memory>
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
#include "fold/detect/cross_tu_cache.hpp"
|
|
#include "fold/detect/div_by_zero.hpp"
|
|
#include "fold/ir/access_path.hpp"
|
|
#include "fold/report/finding.hpp"
|
|
#include "fold/symbolic/budget.hpp"
|
|
#include "fold/symbolic/encoder.hpp"
|
|
|
|
namespace {
|
|
|
|
std::unique_ptr<clang::ASTUnit> parse(const std::string& code) {
|
|
return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
|
|
}
|
|
|
|
struct TestResult {
|
|
std::vector<fold::Finding> findings;
|
|
fold::SolverStats stats;
|
|
};
|
|
|
|
TestResult run(const std::string& code) {
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto unit = parse(code);
|
|
REQUIRE(unit);
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectDivByZeroInContext(unit->getASTContext(), b, s);
|
|
return {std::move(findings), s};
|
|
}
|
|
|
|
} // namespace
|
|
|
|
TEST_CASE("div-by-zero: literal `x / 0` is flagged", "[div][trivial]") {
|
|
auto [findings, stats] = run("int f(int x){ return x / 0; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::DivByZero);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Proved);
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: literal `x % 0` is flagged", "[div][mod]") {
|
|
auto [findings, stats] = run("int f(int x){ return x % 0; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(stats.queries == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: divisor is a non-zero literal", "[div][safe]") {
|
|
auto [findings, stats] = run("int f(int x){ return x / 2; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.queries == 0); // constant-folded
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: high-byte character literal does not crash", "[div][char-literal]") {
|
|
auto [findings, stats] = run("int f(int x){ return x / '\\xff'; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.sat == 0);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: unguarded symbolic divisor is flagged", "[div][symbolic]") {
|
|
auto [findings, stats] = run("int f(int x, int y){ return x / y; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].message.find("y=0") != std::string::npos);
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: `if (y != 0) return x/y;` is suppressed by guard", "[div][guarded]") {
|
|
auto [findings, stats] = run("int f(int x, int y){ if (y != 0) return x / y; return 0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.unsat == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: nested guard `if (y > 0)` also suppresses", "[div][guarded]") {
|
|
auto [findings, stats] = run("int f(int x, int y){ if (y > 0) return x / y; return 0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.queries == 1);
|
|
REQUIRE(stats.unsat == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: literal-infeasible if branch is pruned before walking sink",
|
|
"[div][guarded][prune]") {
|
|
auto [findings, stats] = run("int f(int x){ if (false) return x / 0; return 0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.branch_pruned_count >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: infeasible switch case is pruned before walking sink",
|
|
"[div][switch][prune]") {
|
|
auto [findings, stats] = run("int f(int x){ switch (1) { case 2: return x / 0;"
|
|
" default: return 0; } }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.branch_pruned_count >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: false loop guard is pruned before walking body sink",
|
|
"[div][loop][prune]") {
|
|
auto [findings, stats] = run("int f(int x){ while (false) { return x / 0; } return 0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.branch_pruned_count >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: short-circuit RHS is pruned when LHS makes it unreachable",
|
|
"[div][logical][prune]") {
|
|
auto [findings, stats] = run("int f(int x){ if (false && (x / 0)) return 1; return 0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.branch_pruned_count >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: member positive guard suppresses later member divisor",
|
|
"[div][guarded][member]") {
|
|
auto [findings, stats] = run("struct P { int total_; int done_; };"
|
|
"int f(P* p){ if (p->total_ > 0) return p->done_ / p->total_;"
|
|
" return 0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: implicit-this member positive guard suppresses member divisor",
|
|
"[div][guarded][member][this]") {
|
|
auto [findings, stats] = run("struct P { int total_; int done_;"
|
|
" int f(){ if (total_ > 0) return done_ / total_; return 0; }"
|
|
"};");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: switch-case implicit-this guard suppresses member divisor",
|
|
"[div][guarded][member][switch]") {
|
|
auto [findings, stats] = run("struct P { enum class Style { Percentage, Bar };"
|
|
" Style style_; int total_; int current_;"
|
|
" int f(){ switch(style_) { case Style::Percentage:"
|
|
" if (total_ > 0) { return (current_ * 100) / total_; }"
|
|
" return 0; case Style::Bar: return 0; } return 0; } }; ");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: positive double guard suppresses same-if divisor",
|
|
"[div][guarded][double]") {
|
|
auto [findings, stats] = run("double f(double cur, double total, double elapsed){"
|
|
" double rate = elapsed > 0.0 ? cur / elapsed : 0.0;"
|
|
" if (rate > 0.0 && cur < total) return (total - cur) / rate;"
|
|
" return 0.0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: positive factor guards suppress product divisor",
|
|
"[div][guarded][product]") {
|
|
auto [findings, stats] = run("float f(float dot, float qn, float cn){"
|
|
" if (qn <= 0.0f || cn <= 0.0f) return 0.0f;"
|
|
" return dot / (qn * cn); }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: empty guard and size alias suppress profile division",
|
|
"[div][guarded][alias][early-return]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> class vector { public: bool empty() const;"
|
|
" unsigned long size() const; }; }"
|
|
"unsigned long f(std::vector<int>& runs, unsigned long wall){"
|
|
" if (runs.empty()) return 0; unsigned long count = runs.size();"
|
|
" return wall / count + wall % count; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: guarded size alias suppresses divisor", "[div][guarded][alias]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> class vector { public: bool empty() const;"
|
|
" unsigned long size() const; }; }"
|
|
"double f(std::vector<int>& sections, double n){"
|
|
" if (!sections.empty() && sections.size() >= 2) {"
|
|
" unsigned long totalSecs = sections.size(); return n / totalSecs; }"
|
|
" return 0.0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: guarded member size alias suppresses divisor",
|
|
"[div][guarded][alias][member]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> class vector { public: bool empty() const;"
|
|
" unsigned long size() const; }; }"
|
|
"struct Sections { std::vector<int> sections; };"
|
|
"double f(Sections& docSections, double n){"
|
|
" if (!docSections.sections.empty() && docSections.sections.size() >= 2) {"
|
|
" unsigned long totalSecs = docSections.sections.size(); return n / totalSecs; }"
|
|
" return 0.0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: AccessPath casted member guard suppresses later member divisor",
|
|
"[div][guarded][member][access-path]") {
|
|
auto [findings, stats] =
|
|
run("struct P { int total_; int done_; };"
|
|
"int f(P* p){ if (((P*)p)->total_ > 0) return p->done_ / p->total_;"
|
|
" return 0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: by-ref call write invalidates cached range", "[div][range][call]") {
|
|
auto [findings, stats] = run("extern \"C\" int scanf(const char*, ...);\n"
|
|
"int f(){ int x = 1; scanf(\"%d\", &x); return 10 / x; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: unknown non-const reference call invalidates range",
|
|
"[div][range][call][havoc]") {
|
|
auto [findings, stats] =
|
|
run("extern void mutate(int&); int f(){ int x = 1; mutate(x); return 10 / x; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(stats.sat == 1);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
|
|
REQUIRE(findings[0].evidence.proof_mode == "over-approximated");
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: unknown call without mutable args preserves guarded divisor fact",
|
|
"[div][range][call][havoc]") {
|
|
auto [findings, stats] = run("extern void observe();"
|
|
"int f(int x){ if (x != 0) { observe(); return 10 / x; }"
|
|
" return 0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: AccessPath fact invalidation clears member ranges",
|
|
"[div][range][call][havoc][access-path]") {
|
|
auto env = fold::SymbolicEnv::create();
|
|
auto path = fold::ir::AccessPath::synthetic("doc")
|
|
.field("sections")
|
|
.stableQuery(fold::ir::AccessKind::Size);
|
|
env.setRange(path, fold::IntInterval{1, 64, false});
|
|
env.markDefinitelyNonNull(path);
|
|
env.cacheMember(path, env.ctx().bv_val(7, 64));
|
|
|
|
env.clearAccessPathFacts();
|
|
|
|
REQUIRE_FALSE(env.tryGetRange(path).has_value());
|
|
REQUIRE_FALSE(env.isDefinitelyNonNull(path));
|
|
REQUIRE_FALSE(env.tryGetMember(path).has_value());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: param divisor in non-juliet file stays non-latent",
|
|
"[div][evidence][precondition]") {
|
|
auto [findings, stats] = run("int f(int divisor){ return 10 / divisor; }");
|
|
REQUIRE(findings.size() == 1);
|
|
// The test harness is a non-juliet file (input.cpp) — like the
|
|
// security-bugs corpus (bug_variable.cpp), which gold labels directly.
|
|
// The param-latent demotion is scoped to juliet helper/good-variant
|
|
// filenames (iter-293), so this stays non-latent (Proved).
|
|
REQUIRE_FALSE(findings[0].evidence.latent);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Proved);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: cross-TU divisor param is found", "[div][crosstu]") {
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto callee = parse("int sink(int x, int y){ return x / y; }");
|
|
auto caller = parse("int sink(int, int); int f(int x, int y){ return sink(x, y); }");
|
|
REQUIRE(callee);
|
|
REQUIRE(caller);
|
|
|
|
fold::primeDivByZeroCrossTUCache(callee->getASTContext());
|
|
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), b, s);
|
|
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::DivByZero);
|
|
REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
|
|
REQUIRE(findings[0].message.find("sink") != std::string::npos);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: ternary member denominator guard suppresses", "[div][guarded][ternary]") {
|
|
auto [findings, stats] = run("struct P { unsigned long totalBytes; unsigned long done; };\n"
|
|
"double f(P progress){ return progress.totalBytes > 0 ? "
|
|
"(double)progress.done / progress.totalBytes : 0.0; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: early-return guard suppresses derived floating denominator",
|
|
"[div][guarded][early-return]") {
|
|
auto [findings, stats] = run("struct D { long count() const; };\n"
|
|
"double f(D elapsed, double bytes){ if(elapsed.count() == 0) "
|
|
"return 0.0; return bytes / (elapsed.count() / 1000.0); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: early-return <= zero guard suppresses later divisor",
|
|
"[div][guarded][early-return]") {
|
|
auto [findings, stats] = run(
|
|
"double f(double x, double divisor){ if(divisor <= 0.0) return 0.0; return x / divisor; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: early-return OR guard suppresses finite positive divisor",
|
|
"[div][guarded][early-return]") {
|
|
auto [findings, stats] = run("namespace std { bool isfinite(float); }\n"
|
|
"float f(float raw, float divisor){ if(!std::isfinite(divisor) || "
|
|
"divisor <= 0.0f) return -raw; return raw / divisor; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: callee early-return guard suppresses callsite precondition",
|
|
"[div][crosstu][guarded]") {
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto callee = parse("double decay(double hours, double half_life){ if(half_life <= 0.0) return "
|
|
"0.0; return hours / half_life; }");
|
|
auto caller = parse(
|
|
"double decay(double, double); double f(double h, double hl){ return decay(h, hl); }");
|
|
REQUIRE(callee);
|
|
REQUIRE(caller);
|
|
fold::primeDivByZeroCrossTUCache(callee->getASTContext());
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), b, s);
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: equality early-return guard suppresses callsite precondition",
|
|
"[div][crosstu][guarded]") {
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto callee = parse("int divide(int x, int denominator){ if(denominator == 0) return 0; "
|
|
"return x / denominator; }");
|
|
auto caller = parse(
|
|
"int divide(int, int); int f(int x, int denominator){ return divide(x, denominator); }");
|
|
REQUIRE(callee);
|
|
REQUIRE(caller);
|
|
fold::primeDivByZeroCrossTUCache(callee->getASTContext());
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), b, s);
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: early-return positive epsilon guard suppresses later divisor",
|
|
"[div][guarded][early-return]") {
|
|
auto [findings, stats] = run("double f(double part, double total){ if(total <= 1e-9) return "
|
|
"0.0; return part / total; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: callee positive epsilon guard suppresses callsite precondition",
|
|
"[div][crosstu][guarded]") {
|
|
fold::detect::CrossTUCache::instance().clear();
|
|
auto callee = parse("double share(double part, double total){ if(total <= 1e-9) return 0.0; "
|
|
"return part / total; }");
|
|
auto caller =
|
|
parse("double share(double, double); double f(double p, double t){ return share(p, t); }");
|
|
REQUIRE(callee);
|
|
REQUIRE(caller);
|
|
fold::primeDivByZeroCrossTUCache(callee->getASTContext());
|
|
fold::SolverBudget b;
|
|
fold::SolverStats s;
|
|
auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), b, s);
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: ternary empty guard suppresses size divisor", "[div][guarded][ternary]") {
|
|
auto [findings, stats] = run("namespace std { template<class T> class vector { public: bool "
|
|
"empty() const; unsigned long size() const; }; }\n"
|
|
"double f(std::vector<int>& xs, double n){ return xs.empty() ? "
|
|
"0.0 : n / static_cast<double>(xs.size()); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: prior empty return guard suppresses later size divisor",
|
|
"[div][guarded][early-return]") {
|
|
auto [findings, stats] = run("namespace std { template<class T> class vector { public: bool "
|
|
"empty() const; unsigned long size() const; }; }\n"
|
|
"double f(std::vector<int>& xs, double sum){ if(xs.empty()) { "
|
|
"return 0.0; } return sum / static_cast<double>(xs.size()); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: non-adjacent early return guard suppresses divisor",
|
|
"[div][clang][guarded]") {
|
|
auto [findings, stats] =
|
|
run("double g(); double f(double x){ double norm = g(); if(norm <= 0.0) return 0.0; double "
|
|
"total = 0.0; for(int i=0;i<3;++i){ total += x / norm; } return total; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: reassignment after early guard keeps divisor finding",
|
|
"[div][clang][guarded]") {
|
|
auto [findings, stats] =
|
|
run("double f(double x, double y){ if(y <= 0.0) return 0.0; y = 0.0; return x / y; }");
|
|
REQUIRE_FALSE(findings.empty());
|
|
REQUIRE(stats.sat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: ternary equality guard suppresses minus-one denominator",
|
|
"[div][clang][ternary]") {
|
|
auto [findings, stats] = run(
|
|
"unsigned long f(unsigned long maxChunks, unsigned long maxStart, unsigned long i){ return "
|
|
"(maxChunks == 1) ? 0 : (maxStart * i) / static_cast<unsigned long>(maxChunks - 1); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: positive plus nonnegative denominator suppresses", "[div][clang][arith]") {
|
|
auto [findings, stats] = run(
|
|
"float f(unsigned long rank){ return 1.0f / (1.0f + 0.1f * static_cast<float>(rank)); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: std max positive initializer suppresses divisor", "[div][clang][init]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> T max(T, T); }\n"
|
|
"unsigned long f(unsigned long n, unsigned long raw){ const unsigned long minChunk = "
|
|
"std::max<unsigned long>(1, raw); return n / minChunk; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: non-mutated positive initializer suppresses divisor",
|
|
"[div][clang][init]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> T max(T, T); }\n"
|
|
"double f(unsigned long n, unsigned long cap){ const unsigned long maxp = "
|
|
"std::max<unsigned long>(1, cap); double norm = static_cast<double>(maxp); return "
|
|
"static_cast<double>(n) / norm; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: address-taken positive initializer is not trusted", "[div][clang][init]") {
|
|
auto [findings, stats] = run("extern \"C\" int scanf(const char*, ...);\n"
|
|
"int f(){ int x = 1; scanf(\"%d\", &x); return 10 / x; }");
|
|
REQUIRE_FALSE(findings.empty());
|
|
REQUIRE(stats.sat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: bool alias guard proves divisor nonzero", "[div][clang][alias]") {
|
|
auto [findings, stats] = run(
|
|
"unsigned long f(unsigned long total, unsigned long workers){ "
|
|
"bool useParallel = workers > 1; if(!useParallel) return total; return total / workers; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: enclosing conjunction guard proves member divisor nonzero",
|
|
"[div][clang][guard]") {
|
|
auto [findings, stats] =
|
|
run("struct Exec { bool found; unsigned rank; }; "
|
|
"double f(Exec exec){ double sum = 0.0; if(exec.found && exec.rank > 0){ "
|
|
"sum += 1.0 / static_cast<double>(exec.rank); } return sum; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: guarded min result nonzero", "[div][clang][guard]") {
|
|
auto [findings, stats] =
|
|
run("namespace std { template<class T> T min(T, T); template<class T> T max(T, T); } "
|
|
"struct Pressure { unsigned long workers; }; "
|
|
"unsigned long f(unsigned long total, unsigned long count, unsigned long threshold, "
|
|
"Pressure pressure){ "
|
|
"bool useParallel = count >= threshold && pressure.workers > 1; if(!useParallel) "
|
|
"return total; "
|
|
"const unsigned long suggested = std::max<unsigned long>(1, count); "
|
|
"const unsigned long tasks = std::min<unsigned long>(pressure.workers, suggested); "
|
|
"return total / tasks; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: positive floating denominator from domain constants",
|
|
"[div][clang][init]") {
|
|
auto [findings, stats] = run(
|
|
"namespace std { template<class T> T max(T, T); } "
|
|
"struct Item { float termFrequency; unsigned long fileSize; }; "
|
|
"float f(Item item){ constexpr float k1 = 1.2f; constexpr float b = 0.75f; "
|
|
"constexpr float avgDocLength = 1000.0f; float tf = std::max(0.0f, item.termFrequency); "
|
|
"float denominator = tf + k1 * (1.0f - b + b * (static_cast<float>(item.fileSize) / "
|
|
"avgDocLength)); "
|
|
"return 1.0f / denominator; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: prior member increment proves divisor nonzero", "[div][clang][inc]") {
|
|
auto [findings, stats] =
|
|
run("struct Stats { unsigned long totalRequests; long avg; }; "
|
|
"struct Api { Stats stats_; void f(long duration){ stats_.totalRequests++; "
|
|
"long total = stats_.avg * (stats_.totalRequests - 1) + duration; "
|
|
"stats_.avg = total / stats_.totalRequests; } };");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: prior empty string guards prove max length nonzero",
|
|
"[div][clang][string]") {
|
|
auto [findings, stats] = run("namespace std { template<class T> T max(T, T); } "
|
|
"struct S { bool empty() const; unsigned long length() const; }; "
|
|
"float f(S s1, S s2){ if(s1.empty() && s2.empty()) return 1.0f; "
|
|
"if(s1.empty() || s2.empty()) return 0.0f; "
|
|
"unsigned long maxLen = std::max(s1.length(), s2.length()); "
|
|
"return 1.0f - (1.0f / static_cast<float>(maxLen)); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: prior isValid guard proves member divisor nonzero", "[div][clang][guard]") {
|
|
auto [findings, stats] =
|
|
run("struct Request { unsigned long results_per_page; unsigned long page; bool isValid() "
|
|
"const { "
|
|
"return results_per_page > 0 && results_per_page <= 100 && page > 0; } }; "
|
|
"unsigned long f(const Request& request, unsigned long total){ "
|
|
"if(!request.isValid()) return 0; "
|
|
"return (total + request.results_per_page - 1) / request.results_per_page; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: hash callback slot parameter is modeled non-zero", "[div][hash][curl]") {
|
|
auto [findings, stats] =
|
|
run("static unsigned my_hash(unsigned id, unsigned slots){ return id % slots; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
// Short-circuit hook-overlay (Lever 2): clang lowers `&&`/`||` into separate CFG
|
|
// blocks; the RHS-operand block inherits the LHS guard via a read-only hook-path
|
|
// overlay, so a divisor that is the RHS of a short-circuit is guarded. yams
|
|
// sqlite_vec_backend #6/#7.
|
|
TEST_CASE("div-by-zero: `||` short-circuit guards in-condition modulo", "[div][short-circuit]") {
|
|
auto [findings, stats] =
|
|
run("int f(int dim, int m){ if (m == 0 || dim % m != 0) return 0; return 1; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: `&&` short-circuit guards in-condition modulo", "[div][short-circuit]") {
|
|
auto [findings, stats] =
|
|
run("int f(int dim, int m){ if (m != 0 && dim % m == 0) return 1; return 0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: short-circuit guards a value-context modulo", "[div][short-circuit]") {
|
|
// No control statement — the `||` is a plain return expression.
|
|
auto [findings, stats] = run("bool f(int dim, int m){ return m == 0 || dim % m != 0; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: negated `!(A && B)` short-circuit guards modulo (assert shape)",
|
|
"[div][short-circuit][assert]") {
|
|
auto [findings, stats] =
|
|
run("extern void fail(); int f(int dim, int m){ if (!(m > 0 && dim % m == 0)) fail();"
|
|
" return 1; }");
|
|
REQUIRE(findings.empty());
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: short-circuit overlay does not mask an unguarded divisor",
|
|
"[div][short-circuit]") {
|
|
// LHS is opaque (says nothing about m), so the RHS divisor can still be zero
|
|
// and must still fire. (Call-LHS is gated out of the overlay entirely.)
|
|
auto [findings, stats] = run(
|
|
"extern bool g(int); int f(int n, int m){ if (g(m) && n / m > 1) return 1; return 0; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::DivByZero);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: power-of-two bitwise guard suppresses modulo divisor",
|
|
"[div][guarded][ternary][pow2]") {
|
|
// `(d & (d-1)) == 0` is TRUE when d==0, so the `%` arm is unreachable for a
|
|
// zero divisor: when the guard is false, d is neither 0 nor a power of two.
|
|
auto [findings, stats] =
|
|
run("unsigned f(unsigned long hash, unsigned d){ unsigned low = (unsigned)hash; "
|
|
"return (d & (d - 1)) == 0 ? low & (d - 1) : low % d; }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: power-of-two != guard true arm suppresses modulo divisor",
|
|
"[div][guarded][ternary][pow2]") {
|
|
// `(d & (d-1)) != 0` true arm excludes 0, so `low % d` is guarded.
|
|
auto [findings, stats] =
|
|
run("unsigned f(unsigned long hash, unsigned d){ unsigned low = (unsigned)hash; "
|
|
"return (d & (d - 1)) != 0 ? low % d : low & (d - 1); }");
|
|
REQUIRE(findings.empty());
|
|
REQUIRE(stats.abstract_unsat >= 1);
|
|
}
|
|
|
|
TEST_CASE("div-by-zero: power-of-two guard does not mask a bare modulo divisor",
|
|
"[div][pow2][negative]") {
|
|
// A bare `a % d` with unbounded d must still fire.
|
|
auto [findings, stats] = run("unsigned f(unsigned d){ return 100u % d; }");
|
|
REQUIRE(findings.size() == 1);
|
|
REQUIRE(findings[0].kind == fold::FindingKind::DivByZero);
|
|
}
|