#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>

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

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

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

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

// A statement after an unconditional return is unreachable.
constexpr const char* kAfterReturn = "int f(){ return 1; int x = 2; return x; }";

} // namespace

TEST_CASE("unreachable: code after return is flagged Proved", "[unreachable]") {
    auto findings = runUnreachable(kAfterReturn);
    REQUIRE(countUnreachable(findings) >= 1);
    for (const auto& f : findings)
        if (f.kind == fold::FindingKind::Unreachable)
            REQUIRE(f.confidence == fold::Confidence::Proved);
}

TEST_CASE("unreachable: no-exit-sibling function is prechecked safe", "[unreachable][prefilter]") {
    // A function whose compounds never have an always-exits child followed by
    // a later sibling cannot produce an unreachable finding; the walker is
    // skipped exactly and the precheck counter rises.
    fold::SolverStats stats;
    auto findings =
        runUnreachableWithStats("int f(int x){ if (x > 0) return x; return -x; }", stats);
    REQUIRE(countUnreachable(findings) == 0);
    CHECK(stats.functions_prechecked_safe >= 1);
}

TEST_CASE("unreachable: freestanding wiring is a parity no-op", "[unreachable][freestanding]") {
    // The loop-bound pin does not downgrade unreachable findings (they are not
    // UNSAT proofs over a loop bound) — the toggle is parity here, by design.
    fold::ModelingOptions on;
    on.suppress_loop_bound_always_conditions = true;
    on.havoc_external_symbols = true;
    on.havoc_statics_at_entry = true;
    auto base = runUnreachable(kAfterReturn);
    auto preset = runUnreachable(kAfterReturn, on);
    REQUIRE(countUnreachable(preset) == countUnreachable(base));
    for (const auto& f : preset)
        if (f.kind == fold::FindingKind::Unreachable)
            REQUIRE(f.confidence == fold::Confidence::Proved);
}

TEST_CASE("unreachable: prior imprecision does not hide exact post-return code",
          "[unreachable][precision]") {
    auto findings =
        runUnreachable("extern int g(); int f(){ g(); return 1; int x = 2; return x; }");
    REQUIRE(countUnreachable(findings) >= 1);
}

TEST_CASE("unreachable: false loop guard suppresses unreachable code inside the body",
          "[unreachable][loop]") {
    auto findings = runUnreachable("int f(){ while(false){ return 1; int x = 2; } return 0; }");
    REQUIRE(countUnreachable(findings) == 0);
}