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

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

#include "fold/detect/dead_statement.hpp"
#include "fold/detect/double_free.hpp"
#include "fold/detect/oob_access.hpp"
#include "fold/detect/static_ptr_asymmetry.hpp"
#include "fold/detect/unused_function.hpp"
#include "fold/detect/use_after_free.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"
#include "fold/symbolic/encoder_type_queries.hpp"

// docs/research/soundness.md: `proved` means an exact bounded model
// established the property. These detectors assigned Proved without one:
// from a heap-model flag (double-free), a cross-function pattern
// (static-ptr-asymmetry), an AST fact (unused-function, dead-statement), or a
// SAT result whose encoding precision was never checked (stdlib OOB copy,
// use-after-free under an unknown call).

namespace {

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

std::optional<fold::Confidence> confidenceOf(const std::vector<fold::Finding>& findings,
                                             fold::FindingKind kind) {
    for (const auto& f : findings)
        if (f.kind == kind)
            return f.confidence;
    return std::nullopt;
}

const std::string kLibc = "extern \"C\" void* malloc(unsigned long);\n"
                          "extern \"C\" void free(void*);\n"
                          "extern \"C\" void* memcpy(void*, const void*, unsigned long);\n";

} // namespace

TEST_CASE("double-free without a solver query is Heuristic", "[proved-contract][double-free]") {
    auto unit =
        parse(kLibc + "void f() { void* p = malloc(8); if (!p) return; free(p); free(p); }");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    const auto c = confidenceOf(fold::detectDoubleFreeInContext(unit->getASTContext(), b, s),
                                fold::FindingKind::DoubleFree);
    REQUIRE(c.has_value());
    CHECK(*c == fold::Confidence::Heuristic);
}

TEST_CASE("static-ptr-asymmetry is a pattern, not a proof", "[proved-contract][static-ptr]") {
    auto unit = parse("struct S { int v; };\n"
                      "static S* g_state = nullptr;\n"
                      "int checked() { if (!g_state) return 0; return g_state->v; }\n"
                      "int unchecked() { return g_state->v; }\n");
    REQUIRE(unit);
    const auto c = confidenceOf(fold::detectStaticPtrAsymmetryInContext(unit->getASTContext()),
                                fold::FindingKind::NullDeref);
    REQUIRE(c.has_value());
    CHECK(*c == fold::Confidence::Heuristic);
}

TEST_CASE("unused static function is an AST fact: Syntactic", "[proved-contract][unused]") {
    auto unit = parse("static int helper(int x) { return x + 1; }\nint api(int x) { return x; }\n");
    REQUIRE(unit);
    const auto c = confidenceOf(fold::detectUnusedFunctionsInContext(unit->getASTContext()),
                                fold::FindingKind::UnusedFunction);
    REQUIRE(c.has_value());
    CHECK(*c == fold::Confidence::Syntactic);
}

TEST_CASE("statement after return is an AST fact: Syntactic", "[proved-contract][dead-stmt]") {
    auto unit = parse("int f(int x) { return x; x += 1; }\n");
    REQUIRE(unit);
    const auto c = confidenceOf(fold::detectDeadStatementsInContext(unit->getASTContext()),
                                fold::FindingKind::DeadStatement);
    REQUIRE(c.has_value());
    CHECK(*c == fold::Confidence::Syntactic);
}

TEST_CASE("stdlib copy overflow without encoding precision is Heuristic",
          "[proved-contract][oob]") {
    auto unit = parse(kLibc + "void f(const char* src) { char buf[8]; memcpy(buf, src, 16); }");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    const auto c = confidenceOf(fold::detectOOBAccessInContext(unit->getASTContext(), b, s),
                                fold::FindingKind::OOBAccess);
    REQUIRE(c.has_value());
    CHECK(*c == fold::Confidence::Heuristic);
}

TEST_CASE("heap use-after-free keeps Proved only on an exact encoding", "[proved-contract][uaf]") {
    // The SAT-backed heap use-after-free surfaces through the OOB detector
    // (`uaf-access`).
    auto uafConfidence = [](const std::string& code) -> std::optional<fold::Confidence> {
        auto unit = parse(code);
        REQUIRE(unit);
        fold::SolverBudget b;
        fold::SolverStats s;
        for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s))
            if (f.id.rfind("uaf-access:", 0) == 0)
                return f.confidence;
        return std::nullopt;
    };
    SECTION("exact: stays Proved (control)") {
        const auto c = uafConfidence(
            kLibc + "int f() { int* p = (int*)malloc(sizeof(int)); free(p); return p[0]; }");
        REQUIRE(c.has_value());
        CHECK(*c == fold::Confidence::Proved);
    }
    SECTION("an over-approximated operation on the path: Heuristic") {
        const auto c = uafConfidence(kLibc + "extern int opaque(int);\n"
                                             "int f(int k) { int* p = (int*)malloc(sizeof(int));"
                                             " int n = opaque(k); free(p); return p[n - n]; }");
        REQUIRE(c.has_value());
        CHECK(*c == fold::Confidence::Heuristic);
    }
}

namespace {

// Value of the first sizeof/alignof in `code`, as the encoder would see it.
std::optional<std::uint64_t> firstTypeTrait(const std::string& code, bool c_mode = false) {
    auto unit = c_mode ? clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c11"}, "input.c")
                       : parse(code);
    REQUIRE(unit);
    struct Finder : clang::RecursiveASTVisitor<Finder> {
        const clang::UnaryExprOrTypeTraitExpr* found = nullptr;
        bool VisitUnaryExprOrTypeTraitExpr(clang::UnaryExprOrTypeTraitExpr* e) {
            if (!found)
                found = e;
            return true;
        }
    } finder;
    finder.TraverseDecl(unit->getASTContext().getTranslationUnitDecl());
    REQUIRE(finder.found);
    return fold::symbolic::typeTraitConstant(unit->getASTContext(), finder.found);
}

} // namespace

TEST_CASE("type-trait constants are exact for complete types only", "[proved-contract][sizeof]") {
    // sizeof was an unsupported node, which marked every `malloc(sizeof(T))`
    // path imprecise and so could never back a Proved finding.
    CHECK(firstTypeTrait("unsigned long f() { return sizeof(int); }") == 4u);
    CHECK(firstTypeTrait(
              "struct S { char c; double d; }; unsigned long f() { return sizeof(S); }") == 16u);
    CHECK(firstTypeTrait("unsigned long f() { return alignof(double); }") == 8u);
    // A VLA's size is a runtime value: not a constant.
    CHECK_FALSE(firstTypeTrait("unsigned long f(int n) { char buf[n]; return sizeof(buf); }",
                               /*c_mode=*/true)
                    .has_value());
}

TEST_CASE("constant-index array OOB keeps Proved only on an exact encoding",
          "[proved-contract][oob]") {
    auto oobConfidence = [](const std::string& code) -> std::optional<fold::Confidence> {
        auto unit = parse(code);
        REQUIRE(unit);
        fold::SolverBudget b;
        fold::SolverStats s;
        for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s))
            if (f.id.rfind("oob-access:", 0) == 0)
                return f.confidence;
        return std::nullopt;
    };
    SECTION("exact: stays Proved (control)") {
        const auto c = oobConfidence("int f() { int a[4] = {0}; return a[4]; }");
        REQUIRE(c.has_value());
        CHECK(*c == fold::Confidence::Proved);
    }
    SECTION("an over-approximated operation on the path: Heuristic") {
        const auto c = oobConfidence("extern int opaque(int);\n"
                                     "int f(int k) { int a[4] = {0}; int n = opaque(k);"
                                     " if (n > 2) return a[4]; return 0; }");
        REQUIRE(c.has_value());
        CHECK(*c == fold::Confidence::Heuristic);
    }
}

TEST_CASE("portfolio OOB verdicts are re-checked on the reporting solver",
          "[proved-contract][oob][portfolio]") {
    // The portfolio answers on its own solvers; the model used to be read from
    // the reporting solver without re-checking it, so the counterexample did
    // not satisfy the path (i=0 under `i > 5`).
    auto unit = parse("int f(int i) { int a[4] = {0}; if (i > 5) return a[i]; return 0; }");
    REQUIRE(unit);
    fold::SolverBudget b;
    b.portfolio = true;
    fold::SolverStats s;
    bool found = false;
    for (const auto& f : fold::detectOOBAccessInContext(unit->getASTContext(), b, s)) {
        if (f.id.rfind("oob-access:", 0) != 0)
            continue;
        found = true;
        REQUIRE(f.evidence.counterexample.size() == 1);
        CHECK(f.evidence.counterexample[0].first == "i");
        CHECK(std::stoll(f.evidence.counterexample[0].second) > 5);
    }
    CHECK(found);
}