// Pin the two-channel non-null contract on SymbolicEnv before any
// consolidation refactor. M20 (markDefinitelyNonNull) is persistent
// across block boundaries; M25 (markBlockNonNull) is cleared at
// block exit but mustn't affect M20. isDefinitelyNonNull() consults
// both. Future single-set consolidation must preserve these semantics.

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

#include <array>
#include <catch2/catch_test_macros.hpp>
#include <cstddef>
#include <string>

#include "fold/ir/access_path.hpp"
#include "fold/ir/symbol.hpp"
#include "fold/symbolic/encoder.hpp"

namespace {

const clang::VarDecl* findVarInStmt(const clang::Stmt* statement, const std::string& name) {
    if (statement == nullptr)
        return nullptr;
    if (const auto* decl_stmt = clang::dyn_cast<clang::DeclStmt>(statement)) {
        for (const clang::Decl* declaration : decl_stmt->decls()) {
            if (const auto* variable = clang::dyn_cast<clang::VarDecl>(declaration);
                variable != nullptr && variable->getNameAsString() == name)
                return variable;
        }
    }
    for (const clang::Stmt* child : statement->children()) {
        if (const auto* variable = findVarInStmt(child, name))
            return variable;
    }
    return nullptr;
}

const clang::VarDecl* findLocalVar(clang::ASTContext& context, const std::string& name) {
    for (const clang::Decl* declaration : context.getTranslationUnitDecl()->decls()) {
        const auto* function = clang::dyn_cast<clang::FunctionDecl>(declaration);
        if (function != nullptr && function->hasBody()) {
            if (const auto* variable = findVarInStmt(function->getBody(), name))
                return variable;
        }
    }
    return nullptr;
}

void checkRestoredMetadata(const char* source, const char* name, unsigned bitwidth,
                           bool is_signed) {
    auto unit = clang::tooling::buildASTFromCodeWithArgs(source, {"-std=c++20"}, "input.cpp");
    REQUIRE(unit);

    const auto* declaration = findLocalVar(unit->getASTContext(), name);
    REQUIRE(declaration);

    auto env = fold::SymbolicEnv::create();
    auto phi_value = env.ctx().bv_const("phi_value", fold::kBitvecWidth);
    env.replace(declaration, phi_value);
    CHECK(env.getValueMeta(declaration).bitwidth == fold::kBitvecWidth);
    CHECK(env.getValueMeta(declaration).is_signed);

    auto current = env.getOrCreate(declaration, name, unit->getASTContext());
    CHECK(current.is_bv());
    const auto restored = env.getValueMeta(declaration);
    CHECK(restored.bitwidth == bitwidth);
    CHECK(restored.is_signed == is_signed);
}

// Symbol wraps an opaque void* for variable identity; tests never
// deref it, so distinct addresses from a static array are enough.
fold::ir::Symbol synthSymbol(std::size_t id) {
    static const std::array<int, 16> slots{};
    return fold::ir::Symbol{static_cast<const void*>(&slots.at(id))};
}

fold::ir::AccessPath synthPath(std::size_t id) {
    return fold::ir::AccessPath::local(synthSymbol(id), "slot", "test").field("member");
}

} // namespace

TEST_CASE("SymbolicEnv non-null: M20 mark is visible", "[symbolic-env][nonnull][m20]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(1);
    REQUIRE_FALSE(env.isDefinitelyNonNull(x));
    env.markDefinitelyNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: M25 mark is visible", "[symbolic-env][nonnull][m25]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(2);
    REQUIRE_FALSE(env.isDefinitelyNonNull(x));
    env.markBlockNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: clearBlockNonNull preserves M20",
          "[symbolic-env][nonnull][m20][m25]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(3);
    env.markDefinitelyNonNull(x);
    env.markBlockNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
    env.clearBlockNonNull(x);
    // M20 mark must survive an M25 clear.
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: clearDefinitelyNonNull preserves M25",
          "[symbolic-env][nonnull][m20][m25]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(4);
    env.markDefinitelyNonNull(x);
    env.markBlockNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
    env.clearDefinitelyNonNull(x);
    // M25 mark must survive an M20 clear.
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: clearing both removes the fact",
          "[symbolic-env][nonnull][m20][m25]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(5);
    env.markDefinitelyNonNull(x);
    env.markBlockNonNull(x);
    env.clearDefinitelyNonNull(x);
    env.clearBlockNonNull(x);
    REQUIRE_FALSE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: only M20 set, clearBlock is a no-op",
          "[symbolic-env][nonnull][m20]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(6);
    env.markDefinitelyNonNull(x);
    env.clearBlockNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: only M25 set, clearDefinitely is a no-op",
          "[symbolic-env][nonnull][m25]") {
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(7);
    env.markBlockNonNull(x);
    env.clearDefinitelyNonNull(x);
    REQUIRE(env.isDefinitelyNonNull(x));
}

TEST_CASE("SymbolicEnv non-null: AccessPath M20 and M25 channels are independent",
          "[symbolic-env][nonnull][access-path]") {
    auto env = fold::SymbolicEnv::create();
    const auto path = synthPath(10);
    REQUIRE_FALSE(env.isDefinitelyNonNull(path));

    env.markDefinitelyNonNull(path);
    env.markBlockNonNull(path);
    REQUIRE(env.isDefinitelyNonNull(path));

    env.clearBlockNonNull(path);
    REQUIRE(env.isDefinitelyNonNull(path));

    env.clearDefinitelyNonNull(path);
    REQUIRE_FALSE(env.isDefinitelyNonNull(path));
}

TEST_CASE("SymbolicEnv restores declaration metadata for existing bindings",
          "[symbolic-env][value-meta][cfg]") {
    SECTION("narrow unsigned declaration") {
        checkRestoredMetadata("int f() { unsigned short lookup_offset = 0; return lookup_offset; }",
                              "lookup_offset", 16, false);
    }
    SECTION("signed declaration") {
        checkRestoredMetadata("int f() { int value = 0; return value; }", "value", 32, true);
    }
}

TEST_CASE("SymbolicEnv facts: AccessPath ranges are stored separately from Symbol ranges",
          "[symbolic-env][access-path][range]") {
    auto env = fold::SymbolicEnv::create();
    const auto symbol = synthSymbol(11);
    const auto path = fold::ir::AccessPath::local(symbol, "slot", "test").field("size");

    env.setRange(symbol, fold::IntInterval{1, 3, false});
    env.setRange(path, fold::IntInterval{8, 16, false});

    REQUIRE(env.tryGetRange(symbol).has_value());
    REQUIRE(env.tryGetRange(path).has_value());
    CHECK(env.tryGetRange(symbol)->lo == 1);
    CHECK(env.tryGetRange(path)->lo == 8);

    env.clearRange(path);
    REQUIRE_FALSE(env.tryGetRange(path).has_value());
    REQUIRE(env.tryGetRange(symbol).has_value());
}

TEST_CASE("SymbolicEnv facts: AccessPath member cache is cleared with legacy cache",
          "[symbolic-env][access-path][member-cache]") {
    auto env = fold::SymbolicEnv::create();
    const auto path = synthPath(12);
    z3::expr value = env.ctx().bv_val(42, fold::kBitvecWidth);

    env.cacheMember(path, value);
    REQUIRE(env.tryGetMember(path).has_value());
    CHECK(z3::eq(*env.tryGetMember(path), value));

    env.clearMemberCache();
    REQUIRE_FALSE(env.tryGetMember(path).has_value());
}

TEST_CASE("SymbolicEnv non-null: nonNullVars() exposes M20 marks",
          "[symbolic-env][nonnull][m20][m28]") {
    // nonNullVars() is the M28 entry point — security_walker's walkIf
    // uses it to intersect the two branches' M20 sets at phi-merge.
    // Consolidation must keep this accessor returning ONLY the M20
    // set (block-scoped M25 marks shouldn't leak across phi-joins).
    auto env = fold::SymbolicEnv::create();
    const auto x = synthSymbol(8);
    const auto y = synthSymbol(9);
    env.markDefinitelyNonNull(x);
    env.markBlockNonNull(y);
    const auto& vars = env.nonNullVars();
    REQUIRE(vars.count(x) == 1);
    REQUIRE(vars.count(y) == 0); // M25 mark is NOT in the M20 set
}