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

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

#include "fold/detect/equiv.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"
#include "fold/symbolic/function_effects.hpp"

namespace {

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

fold::symbolic::FunctionEffects effectsFor(const std::string& code,
                                           const std::string& function_name) {
    auto unit = parse(code);
    REQUIRE(unit);
    for (const auto* declaration : unit->getASTContext().getTranslationUnitDecl()->decls()) {
        const auto* function = clang::dyn_cast<clang::FunctionDecl>(declaration);
        if (function && function->getNameAsString() == function_name && function->hasBody())
            return fold::symbolic::summarizeFunctionEffects(function);
    }
    FAIL("function not found: " << function_name);
    return {};
}

std::vector<fold::Finding> runEquiv(const std::string& code) {
    auto unit = parse(code);
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    fold::EquivOptions opts;
    opts.min_body_stmts = 1;
    return fold::detectEquivalentFunctionsInContext(unit->getASTContext(), b, s, opts);
}

std::uint64_t effectSummaryCallsFor(const std::string& code) {
    auto unit = parse(code);
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    s.profiling_enabled = true;
    fold::EquivOptions opts;
    opts.min_body_stmts = 1;
    fold::detectEquivalentFunctionsInContext(unit->getASTContext(), b, s, opts);
    return s.equiv_effect_summary_calls;
}

} // namespace

TEST_CASE("function effects distinguish local work from observable effects", "[equiv][effects]") {
    REQUIRE(effectsFor("int local(int x){ int y = x; y += 1; return y; }", "local")
                .isObservationallyPure());
    const auto external =
        effectsFor("int state; extern void unknown();"
                   "int effectful(int x){ state = x; unknown(); if(x < 0) throw x; return x; }",
                   "effectful");
    REQUIRE(external.known);
    REQUIRE(external.writes_external_state);
    REQUIRE(external.has_unknown_call);
    REQUIRE(external.may_throw);
    REQUIRE_FALSE(external.isObservationallyPure());

    const auto reference_write =
        effectsFor("int write_ref(int& output){ output = 7; return output; }", "write_ref");
    REQUIRE(reference_write.writes_external_state);
    REQUIRE_FALSE(reference_write.isObservationallyPure());

    const auto construction = effectsFor("struct Resource { Resource(); ~Resource(); };"
                                         "int construct(int x){ Resource resource; return x; }",
                                         "construct");
    REQUIRE(construction.has_unknown_call);
    REQUIRE_FALSE(construction.isObservationallyPure());
}

TEST_CASE("abs implemented two ways is Type-4 equivalent", "[equiv][abs]") {
    auto findings = runEquiv("int abs_a(int x){ if(x < 0) return -x; return x; }"
                             "int abs_b(int y){ return y < 0 ? -y : y; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::Equiv);
    REQUIRE(findings[0].confidence == fold::Confidence::Proved);
    REQUIRE(findings[0].evidence.quality.has_value());
    REQUIRE(findings[0].evidence.quality->classification == "pure-equivalence");
    REQUIRE(findings[0].evidence.quality->rank_reasons ==
            std::vector<std::string>{"return-proof", "effects-empty"});
}

TEST_CASE("x+x and x*2 are equivalent", "[equiv][double]") {
    auto findings = runEquiv("int dbl_a(int x){ return x + x; }"
                             "int dbl_b(int x){ return x * 2; }");
    REQUIRE(findings.size() == 1);
}

TEST_CASE("intra-TU equivalence profiles effect-summary calls", "[equiv][profile]") {
    REQUIRE(effectSummaryCallsFor("int dbl_a(int x){ return x + x; }"
                                  "int dbl_b(int x){ return x * 2; }") >= 2);
}

TEST_CASE("equal return values with different global writes are not equivalent",
          "[equiv][effects][negative]") {
    const auto findings = runEquiv("int state;"
                                   "int set_one(int x){ state = 1; return x + 1; }"
                                   "int set_two(int x){ state = 2; return x + 1; }");
    REQUIRE(findings.empty());
}

TEST_CASE("equal return values with different unknown calls are not equivalent",
          "[equiv][effects][negative]") {
    const auto findings = runEquiv("extern void effect_a(); extern void effect_b();"
                                   "int call_a(int x){ effect_a(); return x + 1; }"
                                   "int call_b(int x){ effect_b(); return x + 1; }");
    REQUIRE(findings.empty());
}

TEST_CASE("identity vs +1 is not equivalent", "[equiv][negative]") {
    auto findings = runEquiv("int id_a(int x){ return x; }"
                             "int off(int x){ return x + 1; }");
    REQUIRE(findings.empty());
}

TEST_CASE("signature mismatch produces no pair", "[equiv][sig]") {
    auto findings = runEquiv("int unary(int x){ return x; }"
                             "int binary(int x, int y){ return x; }");
    REQUIRE(findings.empty());
}

TEST_CASE("two functions returning the same constant are NOT flagged",
          "[equiv][trivial-constant]") {
    // The 2026-05-15 yams audit had 10/12 equiv findings of this shape:
    // unrelated functions that happen to return the same integer constant
    // (e.g., onnx ABI version vs boost protocol family). They prove
    // equivalent under the bounded model but are semantically unrelated
    // coincidences. The constant-return filter suppresses them.
    auto findings = runEquiv("int abi_version(){ return 1; }"
                             "int protocol_family(){ return 1; }");
    REQUIRE(findings.empty());
}

TEST_CASE("constant-return filter handles unary minus", "[equiv][trivial-constant]") {
    auto findings = runEquiv("int neg_a(){ return -1; }"
                             "int neg_b(){ return -1; }");
    REQUIRE(findings.empty());
}

TEST_CASE("constant-return filter handles bool literals", "[equiv][trivial-constant]") {
    auto findings = runEquiv("bool flag_a(){ return true; }"
                             "bool flag_b(){ return true; }");
    REQUIRE(findings.empty());
}

TEST_CASE("real equivalence with non-trivial body still fires under filter",
          "[equiv][trivial-constant][positive]") {
    // Pin that the filter doesn't over-suppress: bodies with arithmetic
    // (not pure constant returns) should still be flagged.
    auto findings = runEquiv("int dbl_a(int x){ return x + x; }"
                             "int dbl_b(int x){ return x * 2; }");
    REQUIRE(findings.size() == 1);
}