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

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

#include "fold/detect/cross_tu_cache.hpp"
#include "fold/detect/div_by_zero.hpp"
#include "fold/detect/null_deref.hpp"
#include "fold/detect/summary_store.hpp"
#include "fold/symbolic/budget.hpp"
#include "fold/symbolic/encoder_callee_names.hpp"
#include "fold/symbolic/summary_encoder.hpp"

namespace {

std::unique_ptr<clang::ASTUnit> parse(const std::string& code, const std::string& file) {
    return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, file);
}

const clang::FunctionDecl* findFunction(clang::ASTUnit& unit, const std::string& name) {
    auto& ctx = unit.getASTContext();
    for (auto* decl : ctx.getTranslationUnitDecl()->decls()) {
        auto* fd = clang::dyn_cast<clang::FunctionDecl>(decl);
        if (!fd || !fd->hasBody())
            continue;
        if (fd->getQualifiedNameAsString() == name)
            return fd;
    }
    return nullptr;
}

void primeLeafSummary(clang::ASTUnit& unit, const std::string& name) {
    auto& ctx = unit.getASTContext();
    const auto* fd = findFunction(unit, name);
    REQUIRE(fd != nullptr);
    auto summary = fold::summarizeLeafFunctionSymbolically(fd, ctx);
    REQUIRE(summary);
    fold::detect::SummaryStore::instance().store(fold::summaryStoreKey(fd), *summary);
}

} // namespace

TEST_CASE("symbolic summary suppresses guarded transitive divisor", "[summary][div]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto callee = parse("int plus_one(int x){ return x + 1; }", "callee.cpp");
    auto caller = parse("int plus_one(int); int f(long y){ int z = (int)y; if (z != -1) return 10 "
                        "/ plus_one(z); return 0; }",
                        "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    primeLeafSummary(*callee, "plus_one");

    fold::SolverBudget budget;
    fold::SolverStats stats;
    auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), budget, stats);

    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.unsat == 1);
}

TEST_CASE("symbolic summary preserves transitive divisor hazard", "[summary][div][sat]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto callee = parse("int plus_one(int x){ return x + 1; }", "callee.cpp");
    auto caller = parse("int plus_one(int); int f(long y){ int z = (int)y; if (z == -1) return 10 "
                        "/ plus_one(z); return 0; }",
                        "caller.cpp");
    REQUIRE(callee);
    REQUIRE(caller);

    primeLeafSummary(*callee, "plus_one");

    fold::SolverBudget budget;
    fold::SolverStats stats;
    auto findings = fold::detectDivByZeroInContext(caller->getASTContext(), budget, stats);

    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::DivByZero);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("symbolic summaries compose through standalone calls", "[summary][div][transitive]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto unit = parse(R"(
        int plus_one_ref(int& x) { x = x + 1; return x; }
        int bump(int x) { plus_one_ref(x); return x; }
        int relay(int x) { return bump(x); }
        int f(int z) {
            if (z != -1)
                return 10 / relay(z);
            return 0;
        }
    )",
                      "transitive.cpp");
    REQUIRE(unit);

    auto& ctx = unit->getASTContext();
    const auto* bump = findFunction(*unit, "bump");
    const auto* relay = findFunction(*unit, "relay");
    REQUIRE(bump != nullptr);
    REQUIRE(relay != nullptr);

    const auto* bump_summary = fold::ensureSymbolicSummary(bump, ctx);
    REQUIRE(bump_summary != nullptr);
    REQUIRE(bump_summary->return_post != "arg0");

    const auto* relay_summary = fold::ensureSymbolicSummary(relay, ctx);
    REQUIRE(relay_summary != nullptr);
    REQUIRE(relay_summary->return_post == bump_summary->return_post);
}

TEST_CASE("repeated nested summary computation stays stable across a reused scratch context",
          "[summary][scratch]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto unit = parse(R"(
        int id_val(int x) { return x; }
        int wrap(int x) { return id_val(x); }
        int outer(int x) { return wrap(x); }
    )",
                      "scratch_reuse.cpp");
    REQUIRE(unit);

    auto& ctx = unit->getASTContext();
    const auto* wrap = findFunction(*unit, "wrap");
    const auto* outer = findFunction(*unit, "outer");
    REQUIRE(wrap != nullptr);
    REQUIRE(outer != nullptr);

    // Compute the same summaries twice: the second pass exercises summary
    // recomputation from a cleared store. Copies are taken because
    // SummaryStore::lookupOrCompute returns pointers into its internal map,
    // which clear() invalidates.
    const auto wrap_first = *fold::ensureSymbolicSummary(wrap, ctx);
    const auto outer_first = *fold::ensureSymbolicSummary(outer, ctx);
    REQUIRE(!wrap_first.return_post.empty());
    REQUIRE(!outer_first.return_post.empty());

    fold::detect::SummaryStore::instance().clear();

    const auto* wrap_second = fold::ensureSymbolicSummary(wrap, ctx);
    const auto* outer_second = fold::ensureSymbolicSummary(outer, ctx);
    REQUIRE(wrap_second != nullptr);
    REQUIRE(outer_second != nullptr);

    REQUIRE(wrap_second->return_post == wrap_first.return_post);
    REQUIRE(outer_second->return_post == outer_first.return_post);
    REQUIRE(wrap_second->reads_globals == wrap_first.reads_globals);
    REQUIRE(wrap_second->writes_globals == wrap_first.writes_globals);
    for (const auto& [param, pre] : wrap_first.param_pre) {
        const auto it = wrap_second->param_pre.find(param);
        REQUIRE(it != wrap_second->param_pre.end());
        REQUIRE(it->second.size() == pre.size());
        for (std::size_t i = 0; i < pre.size(); ++i) {
            REQUIRE(it->second[i].kind == pre[i].kind);
            REQUIRE(it->second[i].expr == pre[i].expr);
        }
    }
}

TEST_CASE("symbolic summaries record divisor preconditions", "[summary][pre][div]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto unit = parse(R"(
        int div10(int x) { return 10 / x; }
        int relay(int x) { return div10(x); }
        int guarded(int x) { if (x != 0) return div10(x); return 0; }
    )",
                      "pre_div.cpp");
    REQUIRE(unit);

    auto& ctx = unit->getASTContext();
    const auto* div10 = findFunction(*unit, "div10");
    const auto* relay = findFunction(*unit, "relay");
    const auto* guarded = findFunction(*unit, "guarded");
    REQUIRE(div10 != nullptr);
    REQUIRE(relay != nullptr);
    REQUIRE(guarded != nullptr);

    const auto* div_summary = fold::ensureSymbolicSummary(div10, ctx);
    REQUIRE(div_summary != nullptr);
    REQUIRE(div_summary->param_pre.count(0) == 1);
    REQUIRE(div_summary->param_pre.at(0).front().kind == "nonzero");

    const auto* relay_summary = fold::ensureSymbolicSummary(relay, ctx);
    REQUIRE(relay_summary != nullptr);
    REQUIRE(relay_summary->param_pre.count(0) == 1);
    REQUIRE(relay_summary->param_pre.at(0).front().kind == "nonzero");

    const auto* guarded_summary = fold::ensureSymbolicSummary(guarded, ctx);
    if (guarded_summary != nullptr)
        REQUIRE(guarded_summary->param_pre.empty());
}

TEST_CASE("symbolic summaries retain the fallthrough side of an early-return guard",
          "[summary][pre][div][early-return]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto unit = parse(R"(
        int div10(int x) { return 10 / x; }
        int guarded(int x) { if (x == 0) return 0; return div10(x); }
    )",
                      "early_return.cpp");
    REQUIRE(unit);

    auto& ctx = unit->getASTContext();
    const auto* guarded = findFunction(*unit, "guarded");
    REQUIRE(guarded != nullptr);
    const auto* summary = fold::ensureSymbolicSummary(guarded, ctx);
    REQUIRE(summary != nullptr);
    REQUIRE(summary->param_pre.empty());
}

TEST_CASE("symbolic summaries record pointer preconditions", "[summary][pre][null]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto unit = parse(R"(
        int load(int* p) { return *p; }
        int relay(int* p) { return load(p); }
        int guarded(int* p) { if (p) return load(p); return 0; }
    )",
                      "pre_null.cpp");
    REQUIRE(unit);

    auto& ctx = unit->getASTContext();
    const auto* load = findFunction(*unit, "load");
    const auto* relay = findFunction(*unit, "relay");
    const auto* guarded = findFunction(*unit, "guarded");
    REQUIRE(load != nullptr);
    REQUIRE(relay != nullptr);
    REQUIRE(guarded != nullptr);

    const auto* load_summary = fold::ensureSymbolicSummary(load, ctx);
    REQUIRE(load_summary != nullptr);
    REQUIRE(load_summary->param_pre.count(0) == 1);
    REQUIRE(load_summary->param_pre.at(0).front().kind == "nonnull");

    const auto* relay_summary = fold::ensureSymbolicSummary(relay, ctx);
    REQUIRE(relay_summary != nullptr);
    REQUIRE(relay_summary->param_pre.count(0) == 1);
    REQUIRE(relay_summary->param_pre.at(0).front().kind == "nonnull");

    const auto* guarded_summary = fold::ensureSymbolicSummary(guarded, ctx);
    if (guarded_summary != nullptr)
        REQUIRE(guarded_summary->param_pre.empty());
}

TEST_CASE("summary preconditions are checked at divisor callsites", "[summary][pre][div][call]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto callee = parse("int div10(int x){ return 10 / x; }", "callee.cpp");
    auto guarded = parse("int div10(int); int f(int z){ if (z != 0) return div10(z); return 0; }",
                         "guarded.cpp");
    auto unguarded = parse("int div10(int); int f(int z){ return div10(z); }", "unguarded.cpp");
    REQUIRE(callee);
    REQUIRE(guarded);
    REQUIRE(unguarded);

    primeLeafSummary(*callee, "div10");

    fold::SolverBudget budget;
    fold::SolverStats guarded_stats;
    auto guarded_findings =
        fold::detectDivByZeroInContext(guarded->getASTContext(), budget, guarded_stats);
    REQUIRE(guarded_findings.empty());
    REQUIRE(guarded_stats.queries == 1);
    REQUIRE(guarded_stats.unsat == 1);

    fold::SolverStats unguarded_stats;
    auto unguarded_findings =
        fold::detectDivByZeroInContext(unguarded->getASTContext(), budget, unguarded_stats);
    REQUIRE(unguarded_findings.size() == 1);
    REQUIRE(unguarded_findings[0].kind == fold::FindingKind::DivByZero);
    REQUIRE(unguarded_stats.queries == 1);
    REQUIRE(unguarded_stats.sat == 1);
}

TEST_CASE("summary pointer preconditions prove address-of locals nonnull",
          "[summary][pre][null][call]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    auto callee = parse("int load(int* p){ return *p; }", "callee.cpp");
    auto guarded = parse(R"(
        int load(int*);
        int f() {
            int x = 1;
            int* p = &x;
            return load(p);
        }
    )",
                         "guarded.cpp");
    auto unguarded = parse(R"(
        int load(int*);
        int f() {
            int* p = nullptr;
            return load(p);
        }
    )",
                           "unguarded.cpp");
    REQUIRE(callee);
    REQUIRE(guarded);
    REQUIRE(unguarded);

    primeLeafSummary(*callee, "load");

    fold::SolverBudget budget;
    fold::SolverStats guarded_stats;
    auto guarded_findings =
        fold::detectNullDerefInContext(guarded->getASTContext(), budget, guarded_stats);
    REQUIRE(guarded_findings.empty());
    REQUIRE(guarded_stats.queries == 0);
    REQUIRE(guarded_stats.unsat == 0);

    fold::SolverStats unguarded_stats;
    auto unguarded_findings =
        fold::detectNullDerefInContext(unguarded->getASTContext(), budget, unguarded_stats);
    REQUIRE(unguarded_findings.size() == 1);
    REQUIRE(unguarded_findings[0].kind == fold::FindingKind::NullDeref);
    REQUIRE(unguarded_stats.queries == 1);
    REQUIRE(unguarded_stats.sat == 1);
}

TEST_CASE("symbolic summaries preserve sysconf page-size non-zero return",
          "[summary][div][sysconf]") {
    fold::detect::CrossTUCache::instance().clear();
    fold::detect::SummaryStore::instance().clear();

    const std::string code = "extern \"C\" long sysconf(int);\n"
                             "long page_size() { return sysconf(" +
                             std::to_string(static_cast<int>(_SC_PAGESIZE)) +
                             "); }\n"
                             "long relay() { return page_size(); }\n"
                             "long f(long x) { return x / relay(); }\n";
    auto unit = parse(code, "sysconf_summary.cpp");
    REQUIRE(unit);

    fold::SolverBudget budget;
    fold::SolverStats stats;
    auto findings = fold::detectDivByZeroInContext(unit->getASTContext(), budget, stats);

    REQUIRE(findings.empty());
    REQUIRE(stats.sat == 0);
}