#include <clang/Tooling/Tooling.h>

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

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

std::vector<fold::Finding> runDeadWithStats(const std::string& code, fold::SolverStats& out_stats) {
    auto unit = parse(code);
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectDeadBranchesInContext(unit->getASTContext(), b, s);
    out_stats = s;
    return findings;
}

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

} // namespace

TEST_CASE("if(false) is flagged as dead", "[dead][trivial]") {
    auto findings = runDead("int f(int x){ if(false){ return -1; } return x; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::Dead);
    REQUIRE(findings[0].confidence == fold::Confidence::Proved);
}

TEST_CASE("dead: if-free function is prechecked safe", "[dead][prefilter]") {
    // A function with no IfStmt can never emit a dead-branch finding (emit
    // happens only in walkIf's proveDead path); the walker is skipped and
    // the precheck counter rises.
    fold::SolverStats stats;
    auto findings = runDeadWithStats("int f(int x){ int y = x + 1; return y * 2; }", stats);
    REQUIRE(findings.empty());
    CHECK(stats.functions_prechecked_safe >= 1);
}

TEST_CASE("dead branch identity survives an unrelated preceding statement", "[dead][identity]") {
    const auto baseline = runDead("int f(int x){ if(false){ return -1; } return x; }");
    const auto transformed =
        runDead("int f(int x){ int unrelated = x + 1; if(false){ return -1; } return x; }");
    REQUIRE(baseline.size() == 1);
    REQUIRE(transformed.size() == 1);
    REQUIRE(baseline.front().id == transformed.front().id);
    REQUIRE(baseline.front().evidence.quality.has_value());
    REQUIRE(baseline.front().evidence.quality->classification == "symbolic-dead-branch");
    REQUIRE(baseline.front().evidence.quality->rank_reasons ==
            std::vector<std::string>{"path-predicate-unsat", "z3-proof"});
}

TEST_CASE("contradictory arithmetic conditions are flagged", "[dead][arith]") {
    auto findings = runDead("int f(int x){ if(x > 0 && x < 0){ return -1; } return x; }");
    REQUIRE(findings.size() == 1);
}

TEST_CASE("feasible if/else is NOT flagged", "[dead][live]") {
    auto findings = runDead("int f(int x){ if(x > 0){ return 1; } else { return -1; } }");
    REQUIRE(findings.empty());
}

TEST_CASE("narrow boolean conditions do not escape the QF_BV solver boundary",
          "[dead][translator]") {
    auto findings = runDead("int f(unsigned char state){ if(state){ return 1; } return 0; }");
    REQUIRE(findings.empty());
}

TEST_CASE("function call in condition causes bail (no findings)", "[dead][bailout]") {
    auto findings = runDead("extern int g();"
                            "int f(int x){ if(g() == 0){ return -1; } return x; }");
    REQUIRE(findings.empty());
}

TEST_CASE("prior imprecise statements do not hide exact dead branches", "[dead][precision]") {
    auto findings = runDead("extern int g();"
                            "int f(int x){ g(); if(false){ return -1; } return x; }");
    REQUIRE(countDead(findings) == 1);
}

TEST_CASE("loop bodies guarded by false conditions are not walked as reachable", "[dead][loop]") {
    auto findings = runDead("int f(){ while(false){ if(false){ return 1; } } return 0; }");
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("unsigned tautologies expose dead else arms", "[dead][unsigned]") {
    auto findings = runDead("int f(unsigned x){ if(x >= 0){ return 1; } else { return 0; } }");
    REQUIRE(countDead(findings) == 1);
}

TEST_CASE("if(true) flags the else-arm", "[dead][else]") {
    auto findings = runDead("int f(int x){ if(true){ return 1; } else { return 0; } }");
    REQUIRE(findings.size() == 1);
}

namespace {
// A dead else-arm that is dead ONLY because the induction variable is concrete
// during bounded unrolling (`i < 6` always true) — the gap-A loop-bound FP.
constexpr const char* kLoopBoundDead =
    "int f(){ int a = 0;"
    " for (int i = 0; i < 6; i++) { if (i < 6) { a = 1; } else { a = 2; } }"
    " return a; }";
} // namespace

TEST_CASE("gap A: loop-bound dead arms are suppressed by default", "[dead][freestanding]") {
    auto findings = runDead(kLoopBoundDead);
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("gap A: suppress-loop-bound toggle drops the loop-bound dead arm",
          "[dead][freestanding]") {
    fold::ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    auto findings = runDead(kLoopBoundDead, on);
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("gap A: a genuine dead branch still fires under the toggle", "[dead][freestanding]") {
    fold::ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    auto findings = runDead("int f(int x){ if(false){ return -1; } return x; }", on);
    REQUIRE(countDead(findings) == 1);
}

TEST_CASE("statement-like macro helper branches are not user dead branches", "[dead][macro]") {
    auto findings = runDead(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;
        }
    )");
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("if initializers are applied before proving dead arms", "[dead][control-flow][if-init]") {
    auto findings = runDead(R"(
        extern int* lookup(bool*);
        int classify() {
            bool valid = false;
            if (int* value = lookup(&valid); value != nullptr && valid)
                return *value;
            return 0;
        }
    )");
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("unsupported nested range control flow suppresses later dead proofs",
          "[dead][control-flow][fail-closed]") {
    auto findings = runDead(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;
        }
    )");
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("row-producing API loops do not create dead branches after bounded unroll",
          "[dead][loop]") {
    auto findings = runDead(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;
        }
    )");
    REQUIRE(countDead(findings) == 0);
}

TEST_CASE("bounded retry caps are not dead just because the unroll budget is smaller",
          "[dead][loop]") {
    auto findings = runDead(R"(
        int commit(bool ok, bool isLockError) {
            for (int attempt = 1;; ++attempt) {
                if (ok) {
                    return 0;
                }
                if (!isLockError || attempt >= 10) {
                    if (isLockError) {
                        return 2;
                    }
                    return 1;
                }
            }
        }
    )");
    REQUIRE(countDead(findings) == 0);
}