#include <clang/Tooling/Tooling.h>

#include <catch2/catch_test_macros.hpp>
#include <memory>
#include <string>
#include <vector>

#include "fold/detect/always_condition.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> runAlways(const std::string& code, const fold::ModelingOptions& m) {
    auto unit = parse(code);
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    return fold::detectAlwaysConditionsInContext(unit->getASTContext(), b, s, m);
}

std::size_t countAlways(const std::vector<fold::Finding>& fs) {
    std::size_t n = 0;
    for (const auto& f : fs)
        if (f.kind == fold::FindingKind::AlwaysCondition)
            ++n;
    return n;
}

// A freestanding-style counted loop whose in-bound guard `i < 6` is a
// bounded-unroll artifact, not a real invariant.
constexpr const char* kCountedLoop =
    "void emit_mac(unsigned char* p){ for(int i=0;i<6;i++){ p[i]=0; } }";

} // namespace

TEST_CASE("gap A: loop-bound guards are suppressed by default", "[always][freestanding]") {
    fold::ModelingOptions off; // baseline: no toggles
    auto findings = runAlways(kCountedLoop, off);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("gap A: suppress-loop-bound toggle drops the loop-guard FP", "[always][freestanding]") {
    fold::ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    auto findings = runAlways(kCountedLoop, on);
    // The bounded-unroll loop guard no longer produces an always-condition.
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("gap A: a genuine non-loop tautology still fires under the toggle",
          "[always][freestanding]") {
    // `a == 5` with a constant `a` is a real always-true, not a loop bound — the
    // suppress-loop-bound toggle must NOT hide it.
    const char* code = "int classify(int x){ int a = 5; if (a == 5) { return x + 1; } return x; }";
    fold::ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    auto findings = runAlways(code, on);
    REQUIRE(countAlways(findings) >= 1);
}

TEST_CASE("explicit infinite loop controls are not code-quality findings", "[always][precision]") {
    fold::ModelingOptions options;
    auto findings =
        runAlways("void worker(){ while (true) {} } void worker2(){ do {} while (1); }", options);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("literal true ordinary branches remain code-quality findings", "[always][precision]") {
    fold::ModelingOptions options;
    auto findings = runAlways("int choose(){ if (true) return 1; return 0; }", options);
    REQUIRE(countAlways(findings) == 1);
}

TEST_CASE("prior imprecise statements do not hide exact always conditions", "[always][precision]") {
    fold::ModelingOptions options;
    auto findings =
        runAlways("extern int g(); int choose(){ g(); if (true) return 1; return 0; }", options);
    REQUIRE(countAlways(findings) == 1);
}

TEST_CASE("unsigned comparisons use unsigned ordering", "[always][unsigned]") {
    fold::ModelingOptions options;
    auto findings = runAlways("int choose(unsigned x){ if (x >= 0) return 1; return 0; }", options);
    REQUIRE(countAlways(findings) >= 1);
}

TEST_CASE("reused if condition preserves positive and clean-negative cases",
          "[always][control-flow][encoding-reuse]") {
    fold::ModelingOptions options;
    auto positive =
        runAlways("int positive(int x){ int a = 1; if (a == 1) return x; return 0; }", options);
    auto negative = runAlways("int negative(int x){ if (x > 0) return 1; return 0; }", options);
    REQUIRE(countAlways(positive) >= 1);
    REQUIRE(countAlways(negative) == 0);
}

TEST_CASE("phi-merge equal-arm values keep post-if analysis exact",
          "[always][control-flow][phi-merge]") {
    // Both arms assign the same constant, so ite(cond, v, v) reduces to v.
    // The equal-skip binds the joined value directly; a later condition on it
    // must still be provable (positive) and a genuinely open condition must
    // remain undecided (clean-negative).
    fold::ModelingOptions options;
    auto positive = runAlways("int same(int x){ int a = 0; if (x > 0) { a = 1; } else { a = 1; }"
                              " if (a == 1) return x; return 0; }",
                              options);
    auto negative = runAlways("int open(int x){ int a = 0; if (x > 0) { a = 1; } else { a = 2; }"
                              " if (a == 1) return x; return 0; }",
                              options);
    REQUIRE(countAlways(positive) >= 1);
    REQUIRE(countAlways(negative) == 0);
}

// Comparing two external linker-symbol addresses (the .data-copy idiom
// `dst < &_edata`). With concrete addresses one is always < the other (FP).
constexpr const char* kLinkerSymbolCompare =
    "extern int _sdata; extern int _edata;"
    "int region_ok(){ int* a = &_sdata; int* b = &_edata; if (a < b) { return 1; } return 0; }";

TEST_CASE("gap B: linker-symbol address compare is a Proved FP by default",
          "[always][freestanding]") {
    fold::ModelingOptions off;
    auto findings = runAlways(kLinkerSymbolCompare, off);
    REQUIRE(countAlways(findings) >= 1);
}

TEST_CASE("gap B: havoc-external-symbols clears the linker-symbol FP", "[always][freestanding]") {
    fold::ModelingOptions on;
    on.havoc_external_symbols = true;
    auto findings = runAlways(kLinkerSymbolCompare, on);
    // Both addresses are now opaque unknowns => `a < b` is genuinely undecided.
    REQUIRE(countAlways(findings) == 0);
}

// A mutable static local persists across calls, but the single-call model
// re-applies its initializer at entry, so the "first call" guard `heap == 0`
// looks always-true (the _sbrk OOM-branch idiom).
constexpr const char* kStaticState =
    "char* bump(int n){ static char* heap = (char*)0;"
    " if (heap == (char*)0) { return (char*)0; } heap += n; return heap; }";

TEST_CASE("gap D: static-at-initializer guard is a Proved FP by default",
          "[always][freestanding]") {
    fold::ModelingOptions off;
    auto findings = runAlways(kStaticState, off);
    REQUIRE(countAlways(findings) >= 1);
}

TEST_CASE("gap D: havoc-statics-at-entry clears the static-state FP", "[always][freestanding]") {
    fold::ModelingOptions on;
    on.havoc_statics_at_entry = true;
    auto findings = runAlways(kStaticState, on);
    // `heap` is now a free symbolic at entry => `heap == 0` is undecided.
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("statement-like macro helper branches are not user always-conditions",
          "[always][macro]") {
    fold::ModelingOptions options;
    auto findings = runAlways(R"(
        struct Result {
            bool has_value() const { return true; }
            int error() const { return 1; }
        };
        Result bind();
        #define YAMS_TRY(expr) do { auto r = (expr); if (!r.has_value()) return r.error(); } while (0)
        int save() {
            YAMS_TRY(bind());
            return 0;
        }
    )",
                              options);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("if initializers are applied before proving their conditions",
          "[always][control-flow][if-init]") {
    fold::ModelingOptions options;
    auto findings = runAlways(R"(
        extern int* lookup(bool*);
        int classify() {
            bool valid = false;
            if (int* value = lookup(&valid); value != nullptr && valid)
                return *value;
            return 0;
        }
    )",
                              options);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("strto end pointers are not assumed equal to their input",
          "[always][control-flow][api-model]") {
    fold::ModelingOptions options;
    auto findings = runAlways(R"(
        extern "C" unsigned long long strtoull(const char*, char**, int);
        int parse(const char* input) {
            char* end = nullptr;
            (void)strtoull(input, &end, 10);
            if (end != input && end != nullptr && *end == '\0')
                return 1;
            return 0;
        }
    )",
                              options);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("unsupported nested range control flow suppresses later proofs",
          "[always][control-flow][fail-closed]") {
    fold::ModelingOptions options;
    auto findings = runAlways(R"(
        int classify(bool inspect, int (&values)[2]) {
            bool found = false;
            if (false)
                return -1;
            if (inspect) {
                for (int value : values)
                    if (value != 0)
                        found = true;
            }
            if (found)
                return 1;
            return 0;
        }
    )",
                              options);
    REQUIRE(countAlways(findings) == 0);
}

TEST_CASE("row-producing API loops do not create whole-function always-conditions",
          "[always][loop]") {
    fold::ModelingOptions options;
    auto findings = runAlways(R"(
        extern "C" int sqlite3_step(void*);
        constexpr int SQLITE_ROW = 100;
        int check(void* stmt) {
            int rc = 0;
            int rowCount = 0;
            const char* firstLine = nullptr;
            while ((rc = sqlite3_step(stmt)) == SQLITE_ROW) {
                if (rowCount == 0) {
                    firstLine = "ok";
                }
                ++rowCount;
                if (rowCount >= 16) {
                    break;
                }
            }
            if (rowCount == 1 && firstLine != nullptr) {
                return 1;
            }
            return rc;
        }
    )",
                              options);
    REQUIRE(countAlways(findings) == 0);
}