// M28 phi-join: verify that non-null facts proven in BOTH arms of an
// if-statement survive the phi-merge in the summary encoder.
//
// security_walker.cpp already does this intersection in its walkIf;
// this test pins the same behavior for `summary_encoder::mergeBindings`
// so the two code paths stay in parity.

#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 "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;
}

const clang::VarDecl* findGlobalVar(clang::ASTUnit& unit, const std::string& name) {
    auto& ctx = unit.getASTContext();
    for (auto* decl : ctx.getTranslationUnitDecl()->decls()) {
        auto* vd = clang::dyn_cast<clang::VarDecl>(decl);
        if (!vd || !vd->hasGlobalStorage())
            continue;
        if (vd->getNameAsString() == name)
            return vd;
    }
    return nullptr;
}

} // namespace

TEST_CASE("M28: non-null facts intersected at phi-join survive in summary env",
          "[summary][phi][m28]") {
    // `f` takes only int params (summarizeFunction rejects pointer params via
    // isModeledType), but its body null-checks a global pointer `g_a` in both
    // arms of an if/else. Without M28 in the summary encoder, the post-if env
    // loses the non-null mark; with M28, it retains it (the intersection of
    // both arms' nonNullVars is non-empty).
    auto unit = parse(R"(
        int x;
        int y;
        int* g_p;
        int f(int cond) {
            if (cond) {
                g_p = &x;    // M23: address-of marks g_p non-null in then_env
            } else {
                g_p = &y;    // M23: address-of marks g_p non-null in else_env
            }
            // Post-if: both branches mark g_p non-null. M28 should retain.
            return 0;
        }
    )",
                      "m28.cpp");
    REQUIRE(unit);

    const auto* fd = findFunction(*unit, "f");
    REQUIRE(fd != nullptr);

    auto summary = fold::summarizeFunction(fd, unit->getASTContext());
    REQUIRE(summary);

    const clang::VarDecl* g_p = findGlobalVar(*unit, "g_p");
    REQUIRE(g_p != nullptr);
    REQUIRE(summary->env.isDefinitelyNonNull(g_p));
}