#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);
}