// Matrix row C8 — `/*@ requires p != null */` user contracts that
// seed SymbolicEnv at function entry. The parser is conservative: it
// recognises only `p != null` / `p != NULL` / `p != nullptr` shapes
// today. Anything else is silently ignored (no diagnostic, no
// accidental seeding). Future sessions can grow the grammar; these
// tests pin the v1 surface.
//
// Test-first per the encoder-test-first memory: contract behaviour is
// part of the encoder's semantic surface, so the test goes in before
// the source edit.

#include <clang/AST/Decl.h>
#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/null_deref.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"
#include "fold/symbolic/function_contracts.hpp"

namespace {

std::unique_ptr<clang::ASTUnit> parse(const std::string& code) {
    // -fparse-all-comments retains ordinary block/line comments (not
    // just doxygen-style). Without it, clang would drop `/*@ ... */`
    // before the AST sees it and the contract parser has nothing to
    // read.
    return clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20", "-fparse-all-comments"},
                                                    "input.cpp");
}

// Find the named top-level function in the TU.
const clang::FunctionDecl* findFn(clang::ASTContext& ctx, const std::string& name) {
    for (auto* decl : ctx.getTranslationUnitDecl()->decls()) {
        const auto* fd = clang::dyn_cast<clang::FunctionDecl>(decl);
        if (fd && fd->hasBody() && fd->getNameAsString() == name)
            return fd;
    }
    return nullptr;
}

std::vector<fold::Finding> runNullDeref(clang::ASTContext& ctx) {
    fold::SolverBudget b;
    fold::SolverStats s;
    return fold::detectNullDerefInContext(ctx, b, s);
}

} // namespace

TEST_CASE("function contracts: `requires p != null` parses to param index 0",
          "[contracts][parse]") {
    auto unit = parse(R"(
        /*@ requires p != null */
        int helper(int* p) { return *p; }
    )");
    REQUIRE(unit);
    const auto* fd = findFn(unit->getASTContext(), "helper");
    REQUIRE(fd != nullptr);
    auto nonnull = fold::symbolic::parseFunctionContracts(fd, unit->getASTContext());
    REQUIRE(nonnull == std::vector<unsigned>{0});
}

TEST_CASE("function contracts: `!= NULL` (C-style) and `!= nullptr` (C++) both parse",
          "[contracts][parse]") {
    auto unit = parse(R"(
        #define NULL ((void*)0)
        /*@ requires p != NULL */
        int helper_c(int* p) { return *p; }

        /*@ requires q != nullptr */
        int helper_cxx(int* q) { return *q; }
    )");
    REQUIRE(unit);
    auto& ctx = unit->getASTContext();
    REQUIRE(fold::symbolic::parseFunctionContracts(findFn(ctx, "helper_c"), ctx) ==
            std::vector<unsigned>{0});
    REQUIRE(fold::symbolic::parseFunctionContracts(findFn(ctx, "helper_cxx"), ctx) ==
            std::vector<unsigned>{0});
}

TEST_CASE("function contracts: multiple `requires` lines build a multi-param non-null set",
          "[contracts][parse][multi]") {
    auto unit = parse(R"(
        /*@ requires a != null
            requires c != null */
        int helper(int* a, int* b, int* c) { return *a + *c; }
    )");
    REQUIRE(unit);
    const auto* fd = findFn(unit->getASTContext(), "helper");
    auto nonnull = fold::symbolic::parseFunctionContracts(fd, unit->getASTContext());
    REQUIRE(nonnull.size() == 2);
    REQUIRE(std::find(nonnull.begin(), nonnull.end(), 0u) != nonnull.end());
    REQUIRE(std::find(nonnull.begin(), nonnull.end(), 2u) != nonnull.end());
}

TEST_CASE("function contracts: ordinary doc comments are ignored", "[contracts][parse][reject]") {
    // Plain doxygen / line comments next to a fn must NOT seed any
    // non-null facts. The /*@ ... */ marker is load-bearing.
    auto unit = parse(R"(
        /** ordinary doxygen — no contract here */
        int helper_doc(int* p) { return *p; }

        // plain line comment
        int helper_line(int* q) { return *q; }
    )");
    REQUIRE(unit);
    auto& ctx = unit->getASTContext();
    REQUIRE(fold::symbolic::parseFunctionContracts(findFn(ctx, "helper_doc"), ctx).empty());
    REQUIRE(fold::symbolic::parseFunctionContracts(findFn(ctx, "helper_line"), ctx).empty());
}

TEST_CASE("function contracts: unrecognised shapes parse to empty (no false seeds)",
          "[contracts][parse][reject]") {
    auto unit = parse(R"(
        /*@ requires p > 0
            requires q.foo == bar
            ensures result != null */
        int helper(int* p, int q) { return *p + q; }
    )");
    REQUIRE(unit);
    const auto* fd = findFn(unit->getASTContext(), "helper");
    // None of those shapes are recognised yet — silent reject, no
    // accidental seeding.
    REQUIRE(fold::symbolic::parseFunctionContracts(fd, unit->getASTContext()).empty());
}

TEST_CASE("function contracts: unknown param name parses to empty", "[contracts][parse][reject]") {
    auto unit = parse(R"(
        /*@ requires nonexistent != null */
        int helper(int* p) { return *p; }
    )");
    REQUIRE(unit);
    const auto* fd = findFn(unit->getASTContext(), "helper");
    REQUIRE(fold::symbolic::parseFunctionContracts(fd, unit->getASTContext()).empty());
}

TEST_CASE("function contracts: seeded helper does not flag callee deref",
          "[contracts][integration][end-to-end]") {
    // The callee-standalone-FP pattern from the fold-on-fold pass:
    // helper analyzed in isolation, parameter dereffed → finding fires.
    // With a /*@ requires */ contract, fold should treat the parameter
    // as proven non-null at function entry → no finding.
    auto unit = parse(R"(
        struct R { int v; };
        /*@ requires r != null */
        int methods(const R* r) { return r->v; }
    )");
    REQUIRE(unit);
    auto findings = runNullDeref(unit->getASTContext());
    REQUIRE(findings.empty());
}

TEST_CASE("function contracts: unannotated twin still flags",
          "[contracts][integration][end-to-end]") {
    // Negative twin of the integration test — without the contract,
    // the standalone analysis still fires. Confirms the contract is
    // what suppresses the finding above, not some unrelated change.
    auto unit = parse(R"(
        struct R { int v; };
        int methods(const R* r) { return r->v; }
    )");
    REQUIRE(unit);
    auto findings = runNullDeref(unit->getASTContext());
    REQUIRE_FALSE(findings.empty());
}