#include <clang/AST/Decl.h>
#include <clang/AST/Expr.h>
#include <clang/AST/RecursiveASTVisitor.h>
#include <clang/Tooling/Tooling.h>

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

#include "fold/symbolic/encoder_nonnull.hpp"

namespace {

// Collect the initializer expression of the named local variable.
struct VarInitFinder : clang::RecursiveASTVisitor<VarInitFinder> {
    std::string target;
    const clang::Expr* init = nullptr;
    bool VisitVarDecl(clang::VarDecl* vd) {
        if (vd->getNameAsString() == target && vd->hasInit())
            init = vd->getInit();
        return true;
    }
};

const clang::Expr* initOf(clang::ASTUnit& unit, const std::string& name) {
    VarInitFinder f;
    f.target = name;
    f.TraverseDecl(unit.getASTContext().getTranslationUnitDecl());
    return f.init;
}

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

} // namespace

TEST_CASE("rhsProducesNonNullPointer: address-of is non-null", "[encoder][nonnull]") {
    auto unit = parse("struct S { int f; }; int arr[4]; int x; S s;"
                      "int* a = &x; int* b = &s.f; int* c = &arr[2];");
    REQUIRE(unit);
    // &x, &s.f, &arr[i] all yield definitely-non-null pointer values.
    REQUIRE(fold::rhsProducesNonNullPointer(initOf(*unit, "a")));
    REQUIRE(fold::rhsProducesNonNullPointer(initOf(*unit, "b")));
    REQUIRE(fold::rhsProducesNonNullPointer(initOf(*unit, "c")));
}

TEST_CASE("rhsProducesNonNullPointer: copies and null are not proven non-null",
          "[encoder][nonnull]") {
    auto unit = parse("int* g(); int* p; int* q = p; int* r = nullptr; int* s = g();");
    REQUIRE(unit);
    // A plain pointer copy, a null literal, and a call result are not, on their
    // own, proven non-null by this syntactic classifier.
    REQUIRE_FALSE(fold::rhsProducesNonNullPointer(initOf(*unit, "q")));
    REQUIRE_FALSE(fold::rhsProducesNonNullPointer(initOf(*unit, "r")));
    REQUIRE_FALSE(fold::rhsProducesNonNullPointer(initOf(*unit, "s")));
    REQUIRE_FALSE(fold::rhsProducesNonNullPointer(nullptr));
}