#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/int_overflow.hpp"
#include "fold/detect/z3_model_support.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"

namespace {

struct TestResult {
    std::vector<fold::Finding> findings;
    fold::SolverStats stats;
};

TestResult runWith(const std::string& code, bool report_unsigned_wrap) {
    fold::detect::CrossTUCache::instance().clear();
    auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    fold::WalkOptions wo;
    wo.report_unsigned_wrap = report_unsigned_wrap;
    auto findings = fold::detectIntOverflowInContext(unit->getASTContext(), b, s, {}, wo);
    return {std::move(findings), s};
}

TestResult run(const std::string& code) { return runWith(code, /*report_unsigned_wrap=*/false); }

// Unsigned wraparound is defined behavior (not UB) and is OFF by default; the
// unsigned-wrap tests below opt back in via --report-unsigned-wrap.
TestResult runWithUnsignedWrap(const std::string& code) {
    return runWith(code, /*report_unsigned_wrap=*/true);
}

} // namespace

TEST_CASE("int-overflow: symbolic `a + b` is caller-precondition (latent)", "[overflow][add]") {
    auto [findings, stats] = run("int f(int a, int b){ return a + b; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
    // Arithmetic on function parameters is caller-precondition-dependent
    // (mirrors div-by-zero's parameter-divisor latent contract): the callee
    // alone cannot prove an extreme value is reachable.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(findings[0].message.find("a=") != std::string::npos);
    REQUIRE(findings[0].message.find("b=") != std::string::npos);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("int-overflow: symbolic `a * b` is heuristic-flagged", "[overflow][mul]") {
    auto [findings, stats] = run("int f(int a, int b){ return a * b; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("int-overflow: instantiated template arithmetic is reported at its call site",
          "[overflow][template][call]") {
    auto [findings, stats] = run("template <typename T> T add(T a, T b) { return a + b; }"
                                 "int use() { return add(2147483647, 1); }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(std::any_of(findings.begin(), findings.end(), [](const fold::Finding& finding) {
        return finding.id.find("int-overflow:call:") == 0;
    }));
}

TEST_CASE("int-overflow: safe concrete template arithmetic is not reported",
          "[overflow][template][call][safe]") {
    auto [findings, stats] = run("template <typename T> T add(T a, T b) { return a + b; }"
                                 "int use() { return add(1, 2); }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: division with non-minimum dividend skips Z3", "[overflow][div]") {
    auto [findings, stats] = run("int f(int x){ return 100 / x; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
    REQUIRE(stats.abstract_unsat == 1);
}

TEST_CASE("int-overflow: division by a value other than minus one skips Z3", "[overflow][div]") {
    auto [findings, stats] = run("int f(int x){ return x / 2; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
    REQUIRE(stats.abstract_unsat == 1);
}

TEST_CASE("int-overflow: signed minimum divided by symbolic value remains queried",
          "[overflow][div]") {
    auto [findings, stats] = run("int f(int x){ return (-2147483647 - 1) / x; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("int-overflow: repeated guarded arithmetic reuses asserted result facts",
          "[overflow][add][guarded]") {
    auto [findings, stats] = run("int f(int x, int y){ int acc = 0;"
                                 "if ((y + 0) >= 0) acc += 100 / x; acc += x + 0;"
                                 "if ((y + 1) >= 0) acc += 100 / x; acc += x + 1;"
                                 "return acc; }");
    REQUIRE(findings.size() == 2);
    REQUIRE(stats.queries == 5);
    REQUIRE(stats.abstract_unsat >= 4);
    REQUIRE(stats.branch_feasibility_checks == 0);
    REQUIRE(stats.branch_feasibility_fast_paths == 2);
}

TEST_CASE("int-overflow: branch fast path rejects constrained parameter domains",
          "[overflow][branch-feasibility]") {
    auto reassigned = run("int f(int x){ x = 0; if ((x + 1) >= 0) return x + 0; return 0; }");
    REQUIRE(reassigned.stats.branch_feasibility_fast_paths == 0);
    REQUIRE(reassigned.stats.branch_feasibility_checks == 2);

    auto boundary = run("int f(int x){ if (x >= (-2147483647 - 1)) return x + 0; return 0; }");
    REQUIRE(boundary.stats.branch_feasibility_fast_paths == 0);
    REQUIRE(boundary.stats.branch_feasibility_checks == 2);
}

TEST_CASE("int-overflow: constant 0 + 0 must NOT overflow", "[overflow][safe]") {
    // M18: the interval pre-pass proves `0 + 0` safe without touching Z3.
    // Track that separately from real solver UNSAT so profile SAT/UNSAT
    // totals stay comparable to the number of Z3 queries.
    auto [findings, stats] = run("int f(){ return 0 + 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.unsat == 0);
    REQUIRE(stats.abstract_unsat == 1);
    REQUIRE(stats.queries == 0);
}

TEST_CASE("int-overflow: range-bounded operands suppress finding", "[overflow][guarded]") {
    // The path predicate inside the then-arm constrains `a` and `b` to
    // [0, 1000), so `a + b` cannot overflow signed 64-bit.
    auto [findings, stats] = run("int f(int a, int b){"
                                 "  if (a >= 0 && a < 1000 && b >= 0 && b < 1000) return a + b;"
                                 "  return 0;"
                                 "}");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
    REQUIRE(stats.unsat == 0);
    REQUIRE(stats.abstract_unsat == 1);
}

TEST_CASE("int-overflow: loop induction bounds suppress finding", "[overflow][loop]") {
    auto [findings, stats] =
        run("int f(){ for (int i = 0; i < 100; ++i) return i + 1; return 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
    REQUIRE(stats.unsat == 0);
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("int-overflow: float arithmetic is pre-filtered", "[overflow][float]") {
    auto [findings, stats] = run("float f(float a, float b){ return a + b; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
}

TEST_CASE("int-overflow: unsigned arithmetic is pre-filtered", "[overflow][unsigned]") {
    auto [findings, stats] = run("unsigned f(unsigned a, unsigned b){ return a + b; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
}

TEST_CASE("int-overflow: mixed-width signed arithmetic uses promoted result width",
          "[overflow][mixed-width]") {
    auto [findings, stats] = run("long long f(long long val, int d){ "
                                 "if(d < 0 || d > 9) return 0; "
                                 "if(val > (9223372036854775807LL - d) / 10) return 0; "
                                 "return 1; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("int-overflow: mixed size_t and signed literal uses unsigned result type",
          "[overflow][unsigned][mixed]") {
    auto [findings, stats] =
        run("using size_t = decltype(sizeof(0)); size_t f(size_t n){ return n + 1; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
}

TEST_CASE("int-overflow: unsigned 64-bit max constant does not crash interval eval",
          "[overflow][wide-constant]") {
    auto [findings, stats] = run("int f(){ unsigned long long x = 18446744073709551615ULL; "
                                 "return x ? 1 : 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);

    auto [wide_findings, wide_stats] =
        run("int g(){ unsigned __int128 x = ((unsigned __int128)1 << 100); "
            "return x ? 1 : 0; }");
    REQUIRE(wide_findings.empty());
    REQUIRE(wide_stats.queries == 0);
}

TEST_CASE("int-overflow: negative concrete operands do not crash APInt construction",
          "[overflow][negative-constant]") {
    auto [findings, stats] = run("int f(){ return -1 + -1; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.sat == 0);
}

TEST_CASE("int-overflow: by-ref call write invalidates cached range", "[overflow][range][call]") {
    auto [findings, stats] = run("extern \"C\" int scanf(const char*, ...);\n"
                                 "int f(){ int x = 1; scanf(\"%d\", &x); return x * x; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("int-overflow: unsigned compound arithmetic is pre-filtered",
          "[overflow][unsigned-compound]") {
    auto [findings, stats] = run("unsigned f(unsigned a, unsigned b){ a += b; return a; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 0);
}

TEST_CASE("int-overflow: cross-TU arithmetic param is found", "[overflow][crosstu]") {
    fold::detect::CrossTUCache::instance().clear();
    auto callee = clang::tooling::buildASTFromCodeWithArgs(
        "int sink(int a, int b){ return a + b; }", {"-std=c++20"}, "callee.cpp");
    auto caller = clang::tooling::buildASTFromCodeWithArgs(
        "int sink(int, int); int f(int a, int b){ return sink(a, b); }", {"-std=c++20"},
        "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    fold::primeIntOverflowCrossTUCache(callee->getASTContext());

    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectIntOverflowInContext(caller->getASTContext(), b, s);

    REQUIRE(findings.size() == 2);
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
    REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
    REQUIRE(findings[0].message.find("sink") != std::string::npos);
}

TEST_CASE("int-overflow: cross-TU arithmetic param in a NAMESPACED callee is found",
          "[overflow][crosstu][namespace]") {
    // Gap 1 regression: primeIntOverflowCrossTUCache used to iterate only
    // top-level TU decls, so a callee defined inside a namespace was never
    // summarized and the cross-function finding silently vanished.
    fold::detect::CrossTUCache::instance().clear();
    auto callee = clang::tooling::buildASTFromCodeWithArgs(
        "namespace ns { int sink(int a, int b){ return a + b; } }", {"-std=c++20"}, "callee.cpp");
    auto caller = clang::tooling::buildASTFromCodeWithArgs(
        "namespace ns { int sink(int, int); } int f(int a, int b){ return ns::sink(a, b); }",
        {"-std=c++20"}, "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    fold::primeIntOverflowCrossTUCache(callee->getASTContext());

    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectIntOverflowInContext(caller->getASTContext(), b, s);

    bool found_callsite = std::any_of(findings.begin(), findings.end(), [](const fold::Finding& f) {
        return f.kind == fold::FindingKind::IntOverflow &&
               f.message.find("sink") != std::string::npos;
    });
    REQUIRE(found_callsite);
}

TEST_CASE("int-overflow: cross-TU unsigned arithmetic is not summarized as signed overflow",
          "[overflow][crosstu][unsigned]") {
    fold::detect::CrossTUCache::instance().clear();
    auto callee = clang::tooling::buildASTFromCodeWithArgs(
        "using size_t = decltype(sizeof(0)); size_t sink(size_t n){ return n + 1; }",
        {"-std=c++20"}, "callee.cpp");
    auto caller = clang::tooling::buildASTFromCodeWithArgs(
        "using size_t = decltype(sizeof(0)); size_t sink(size_t); "
        "size_t f(size_t n){ return sink(n); }",
        {"-std=c++20"}, "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    fold::primeIntOverflowCrossTUCache(callee->getASTContext());

    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectIntOverflowInContext(caller->getASTContext(), b, s);

    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: gmtime-populated tm formatting fields are bounded",
          "[overflow][time][tm]") {
    auto [findings, stats] =
        run("struct tm { int tm_sec; int tm_min; int tm_hour; int tm_mday; int tm_mon; "
            "int tm_year; };\n"
            "extern int curlx_gmtime(long, tm*);\n"
            "int f(long t){ tm stamp; if(curlx_gmtime(t, &stamp)) return 0; "
            "int year = stamp.tm_year + 1900; int mon = stamp.tm_mon + 1; "
            "return year || mon; }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: guarded time maxage addition is safe", "[overflow][time][guard]") {
    auto [findings, stats] = run("using time_t = long long;\n"
                                 "#define TIME_T_MAX 9223372036854775807LL\n"
                                 "extern time_t time(void*);\n"
                                 "time_t f(time_t maxage){ time_t secs = time(nullptr); "
                                 "if(maxage > (TIME_T_MAX - secs)) return TIME_T_MAX; "
                                 "else return maxage + secs; }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: local counter increments stay bounded from zero initializer",
          "[overflow][counter]") {
    auto [findings, stats] = run("int f(bool a, bool b, bool c, bool d){ int count = 0; "
                                 "if(a) count++; if(b) count++; if(c) count++; if(d) count++; "
                                 "return count; }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: local counter size accumulation is not overflow finding",
          "[overflow][counter]") {
    auto [findings, stats] =
        run("namespace std { template<class T> struct vector { int size(); }; } "
            "int f(std::vector<int>& v, bool a){ int count = 0; "
            "if(a) count++; count += static_cast<int>(v.size()); "
            "return count; }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: cross-TU UI formatting helpers are not arithmetic sinks",
          "[overflow][crosstu][ui]") {
    fold::detect::CrossTUCache::instance().clear();
    auto callee = clang::tooling::buildASTFromCodeWithArgs(
        "namespace yams { namespace cli { namespace ui { "
        "int section_header(int width){ int dashes = width - 4; return dashes; } "
        "void render_rows(int term_width){ int value_col = 2 + term_width; } "
        "}}}",
        {"-std=c++20"}, "ui_helpers.hpp");
    auto caller = clang::tooling::buildASTFromCodeWithArgs(
        "namespace yams { namespace cli { namespace ui { int section_header(int); void "
        "render_rows(int); }}} "
        "int f(int w){ yams::cli::ui::render_rows(w); return yams::cli::ui::section_header(w); }",
        {"-std=c++20"}, "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    fold::primeIntOverflowCrossTUCache(callee->getASTContext());

    fold::SolverBudget b;
    fold::SolverStats st;
    auto findings = fold::detectIntOverflowInContext(caller->getASTContext(), b, st);
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: cross-TU pointer difference is not signed arithmetic sink",
          "[overflow][crosstu][pointer]") {
    fold::detect::CrossTUCache::instance().clear();
    auto callee = clang::tooling::buildASTFromCodeWithArgs(
        "using size_t = decltype(sizeof(0)); using ptrdiff_t = decltype((char*)0 - (char*)0); "
        "bool hasBytes(const char* ptr, const char* end, size_t count){ "
        "return ptr <= end && static_cast<size_t>(end - ptr) >= count; }",
        {"-std=c++20"}, "callee.cpp");
    auto caller = clang::tooling::buildASTFromCodeWithArgs(
        "using size_t = decltype(sizeof(0)); bool hasBytes(const char*, const char*, size_t); "
        "bool f(const char* p, const char* e, size_t n){ return hasBytes(p, e, n); }",
        {"-std=c++20"}, "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    fold::primeIntOverflowCrossTUCache(callee->getASTContext());

    fold::SolverBudget b;
    fold::SolverStats st;
    auto findings = fold::detectIntOverflowInContext(caller->getASTContext(), b, st);
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: alias-positive loop guard proves minus one safe", "[overflow][guard]") {
    auto [findings, stats] =
        run("using streamoff = long long; "
            "bool f(streamoff fileSizeOff){ streamoff pos = fileSizeOff; "
            "while(pos > 0){ pos--; if(pos < fileSizeOff - 1) return true; } return false; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat + stats.unsat >= 1);
}

TEST_CASE("int-overflow: unsigned subtraction wraps when lhs < rhs", "[overflow][unsigned-wrap]") {
    auto [findings, stats] =
        runWithUnsignedWrap("unsigned f(unsigned a, unsigned b){ return a - b; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::UnsignedWrap);
    // Param-origin wrap is caller-precondition (latent), same as signed.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(findings[0].message.find("Unsigned") != std::string::npos);
    REQUIRE(findings[0].message.find("wraps") != std::string::npos);
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("int-overflow: unsigned constant subtraction does not wrap",
          "[overflow][unsigned-wrap][constant]") {
    auto [findings, stats] = runWithUnsignedWrap("unsigned f(){ return 20U - 18U; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("int-overflow: unsigned ternary guard proves subtraction safe",
          "[overflow][unsigned-wrap][guarded]") {
    auto guarded = runWithUnsignedWrap("unsigned long f(unsigned long lhs, unsigned long rhs) {"
                                       "return lhs > rhs ? lhs - rhs : 1; }");
    REQUIRE(guarded.findings.empty());
    REQUIRE(guarded.stats.abstract_unsat >= 1);

    auto unguarded = runWithUnsignedWrap("unsigned long f(unsigned long lhs, unsigned long rhs) {"
                                         "return lhs - rhs; }");
    REQUIRE_FALSE(unguarded.findings.empty());

    auto guarded_member =
        runWithUnsignedWrap("struct Config { unsigned long max; };"
                            "unsigned long f(Config config, unsigned long reserved) {"
                            "return config.max > reserved ? config.max - reserved : 1; }");
    REQUIRE(guarded_member.findings.empty());

    auto guarded_this_member = runWithUnsignedWrap(
        "struct Pool { unsigned long max; unsigned long f(unsigned long reserved) {"
        "return max > reserved ? max - reserved : 1; } };");
    REQUIRE(guarded_this_member.findings.empty());
}

TEST_CASE("int-overflow: unsigned multiplication wraps detected",
          "[overflow][unsigned-wrap][mul]") {
    auto [findings, stats] =
        runWithUnsignedWrap("unsigned f(unsigned a, unsigned b){ return a * b; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::UnsignedWrap);
    // Param-origin wrap is caller-precondition (latent), same as signed.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(findings[0].message.find("Unsigned") != std::string::npos);
    REQUIRE(stats.queries >= 1);
    REQUIRE(stats.sat >= 1);
}

TEST_CASE("int-overflow: unsigned mul with narrow operands is safe",
          "[overflow][unsigned-wrap][mul-safe]") {
    auto [findings, stats] = runWithUnsignedWrap("unsigned f(){ return 0xFFU * 0xFFFFU; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.abstract_unsat >= 1);
}

TEST_CASE("int-overflow: unsigned addition is not flagged as wrap",
          "[overflow][unsigned-wrap][add-safe]") {
    auto [findings, stats] = run("unsigned f(unsigned a, unsigned b){ return a + b; }");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: unsigned subtraction real-world len-minus-constant",
          "[overflow][unsigned-wrap][len-minus]") {
    auto [findings, stats] = runWithUnsignedWrap("unsigned f(unsigned len){ return len - 18; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::UnsignedWrap);
    // Param-origin wrap is caller-precondition (latent), same as signed.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(findings[0].message.find("subtraction wraps") != std::string::npos);
}

TEST_CASE("int-overflow: npos guard does not hide a real wrap on a different path",
          "[overflow][unsigned-wrap][npos-guard]") {
    auto [findings, stats] = runWithUnsignedWrap(
        "#include <string>\n"
        "typedef std::basic_string<char> StringType;\n"
        "unsigned long g(const std::string& path, unsigned long a, unsigned long b) {\n"
        "  if (a == StringType::npos) return a;\n"
        "  return b - 2;  // b is unconstrained - genuinely wraps when b < 2\n"
        "}\n");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::UnsignedWrap);
    REQUIRE(findings[0].message.find("wraps") != std::string::npos);
}

TEST_CASE("int-overflow: string_view::substr param is container-bounded (no FP)",
          "[overflow][string-index][container-bounded]") {
    // substr/append/insert do size()-pos / pos+count arithmetic bounded by the
    // container size invariant, so an unbounded `pos` at the call site must not
    // be exported as an overflow sink (chromium file_path.cc substr/append FPs).
    auto [findings, stats] = run("#include <string_view>\n"
                                 "std::string_view g(std::string_view path, unsigned long pos) {\n"
                                 "  return path.substr(pos);\n"
                                 "}\n");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: std::string::append param is container-bounded (no FP)",
          "[overflow][string-index][container-bounded]") {
    auto [findings, stats] =
        run("#include <string>\n"
            "void g(std::string& out, const std::string& suffix, unsigned long pos) {\n"
            "  out.append(suffix, pos);\n"
            "}\n");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: free-function arithmetic is still an overflow sink",
          "[overflow][string-index][container-bounded-negative]") {
    // Clean negative: a FREE function doing the same size()-pos style signed
    // arithmetic is NOT container-bounded, so it must still flag.
    auto [findings, stats] = run("int f(int size, int pos) { return size - pos; }");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
}

TEST_CASE("int-overflow: narrow array elements keep guarded table arithmetic safe",
          "[overflow][table-bounds]") {
    // Chromium file_path.cc gap: a UInt16 std::array element read must be
    // bounded to 16 bits; otherwise `lookup_offset + (c & 0xFF)` overflows
    // with impossible counterexamples (lookup_offset = 2^31).
    auto [findings, stats] = run("#include <array>\n"
                                 "int f() {\n"
                                 "  const std::array<unsigned short, 2816> table = {};\n"
                                 "  unsigned short lookup_offset = table[0];\n"
                                 "  unsigned short c = 0x41;\n"
                                 "  return (int)(lookup_offset + (c & 0x00FF));\n"
                                 "}\n");
    std::fprintf(stderr, "TABLE-POS findings=%zu\n", findings.size());
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: wide array elements keep a real overflow finding",
          "[overflow][table-bounds]") {
    // Clean negative: an int (32-bit) array element is genuinely unbounded,
    // so `lookup_offset + (c & 0xFF)` can still overflow int.
    auto [findings, stats] = run("#include <array>\n"
                                 "int g() {\n"
                                 "  const std::array<int, 256> table = {};\n"
                                 "  int lookup_offset = table[0];\n"
                                 "  unsigned short c = 0x41;\n"
                                 "  return lookup_offset + (c & 0x00FF);\n"
                                 "}\n");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
}

TEST_CASE("int-overflow: operator[] on narrow container elements keeps arithmetic safe",
          "[overflow][table-bounds]") {
    // std::array<std::uint16_t, N>::operator[] is a member call; its read must
    // be narrowed to the element type so guarded arithmetic cannot overflow
    // (chromium fixed-table bounds: file_path.cc:1454 standalone path).
    auto [findings, stats] = run("#include <array>\n"
                                 "#include <cstdint>\n"
                                 "int f() {\n"
                                 "  const std::array<std::uint16_t, 2816> table = {};\n"
                                 "  std::uint16_t lookup_offset = table[1];\n"
                                 "  std::uint16_t c = 0x41;\n"
                                 "  return (int)(lookup_offset + (c & 0x00FF));\n"
                                 "}\n");
    std::fprintf(stderr, "OPBRACKET-POS findings=%zu\n", findings.size());
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: direct narrow operator[] arithmetic stays bounded",
          "[overflow][table-bounds]") {
    auto [findings, stats] = run("#include <array>\n"
                                 "#include <cstdint>\n"
                                 "int f() {\n"
                                 "  const std::array<std::uint16_t, 2816> table = {};\n"
                                 "  std::uint16_t c = 0x41;\n"
                                 "  return static_cast<int>(table[0] + (c & 0x00FF));\n"
                                 "}\n");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: operator[] on wide elements keeps a real overflow finding",
          "[overflow][table-bounds]") {
    auto [findings, stats] = run("#include <array>\n"
                                 "int g() {\n"
                                 "  const std::array<int, 256> table = {};\n"
                                 "  int lookup_offset = table[1];\n"
                                 "  unsigned short c = 0x41;\n"
                                 "  return lookup_offset + (c & 0x00FF);\n"
                                 "}\n");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
}

TEST_CASE("int-overflow: narrow integer-returning call bounds initialized local",
          "[overflow][table-bounds][return-type]") {
    auto [findings, stats] = run("extern unsigned short read_offset();\n"
                                 "int f() {\n"
                                 "  unsigned short lookup_offset = read_offset();\n"
                                 "  unsigned short c = 0x41;\n"
                                 "  return lookup_offset + (c & 0x00FF);\n"
                                 "}\n");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: wide integer-returning call keeps real overflow",
          "[overflow][table-bounds][return-type]") {
    auto [findings, stats] = run("extern int read_offset();\n"
                                 "int g() {\n"
                                 "  int lookup_offset = read_offset();\n"
                                 "  unsigned short c = 0x41;\n"
                                 "  return lookup_offset + (c & 0x00FF);\n"
                                 "}\n");
    REQUIRE_FALSE(findings.empty());
    REQUIRE(findings[0].kind == fold::FindingKind::IntOverflow);
}

TEST_CASE("int-overflow: Chromium HFS fixed-table read stays element-bounded",
          "[overflow][table-bounds][chromium]") {
    auto [findings, stats] = run(R"cpp(
#include <array>
#include <cstddef>
#include <cstdint>
namespace base_icu { using UChar32 = int; }
using UInt16 = std::uint16_t;
extern base_icu::UChar32 ReadCodepoint(const std::uint8_t*, std::size_t, std::size_t,
                                       base_icu::UChar32*);
template <typename D, typename S> D checked_cast(S value) {
    return static_cast<D>(value);
}
#define CBU8_NEXT(string, index, length, codepoint) \
    ((codepoint) = ReadCodepoint(string, index, length, &(codepoint)))
#define DCHECK_GT(a, b) ((void)0)
const std::array<UInt16, 11 * 256> lower_case_table = {0x0100, 0x0200, 0x0000, 0x0300};
base_icu::UChar32 HFSReadNextNonIgnorableCodepoint(const char* string,
                                                   std::size_t length,
                                                   std::size_t* index) {
    base_icu::UChar32 codepoint = 0;
    while (*index < length && codepoint == 0) {
        CBU8_NEXT(reinterpret_cast<const std::uint8_t*>(string), *index, length, codepoint);
        DCHECK_GT(codepoint, 0);
        if (codepoint > 0 && codepoint <= 0xFFFF) {
            UInt16 unsigned_codepoint = checked_cast<UInt16>(codepoint);
            UInt16 lookup_offset = lower_case_table[unsigned_codepoint >> 8];
            if (lookup_offset != 0)
                codepoint = lower_case_table[lookup_offset + (unsigned_codepoint & 0x00FF)];
        }
    }
    return codepoint;
}
)cpp");
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: CFString size output contract proves length-1 safe",
          "[overflow][api-contract]") {
    // CFStringGetMaximumSizeOfFileSystemRepresentation returns the max size
    // INCLUDING the NUL terminator (>= 1 for valid strings); modeling that
    // contract proves `length - 1` safe without relying on the debug-only
    // DCHECK (chromium file_path.cc:1514).
    auto [findings, stats] =
        run("typedef long CFIndex;\n"
            "extern \"C\" CFIndex CFStringGetMaximumSizeOfFileSystemRepresentation(const void*);\n"
            "void resize(unsigned long);\n"
            "void f(const void* cfstring) {\n"
            "  CFIndex length = CFStringGetMaximumSizeOfFileSystemRepresentation(cfstring);\n"
            "  resize((unsigned long)length - 1);\n"
            "}\n");
    std::fprintf(stderr, "CFSTRING-POS findings=%zu\n", findings.size());
    REQUIRE(findings.empty());
}

TEST_CASE("int-overflow: witnesses use the source type's width and signedness",
          "[int_overflow][witness]") {
    // Symbols are 64-bit; only the low 32 bits carry an `int`. Witnesses were
    // printed from the whole bitvector, e.g. a=2147483648 or
    // a=-9223372034707292160 for `int a`.
    auto r = run("int sum(int a, int b) { int x = a + b; x += a; return x; }\n");
    REQUIRE_FALSE(r.findings.empty());
    for (const auto& f : r.findings) {
        for (const auto& [name, value] : f.evidence.counterexample) {
            const long long v = std::stoll(value);
            CHECK(v >= -2147483648LL);
            CHECK(v <= 2147483647LL);
        }
    }
}

TEST_CASE("formatSourceIntValue truncates and signs", "[int_overflow][witness]") {
    using fold::detect::formatSourceIntValue;
    CHECK(formatSourceIntValue(0x80000000ULL, {32, true}) == "-2147483648");
    CHECK(formatSourceIntValue(0x8000000080000000ULL, {32, true}) == "-2147483648");
    CHECK(formatSourceIntValue(0xBFFFFFFFULL, {32, true}) == "-1073741825");
    CHECK(formatSourceIntValue(0x1FFFFFFFFULL, {32, false}) == "4294967295");
    CHECK(formatSourceIntValue(7, {32, true}) == "7");
    CHECK(formatSourceIntValue(0xFFFFFFFFFFFFFFFFULL, {64, true}) == "-1");
    CHECK(formatSourceIntValue(0xFFULL, {8, true}) == "-1");
}