#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/sign_conversion.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"

namespace {

struct TestResult {
    std::vector<fold::Finding> findings;
    fold::SolverStats stats;
};

TestResult run(const std::string& code) {
    auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    auto findings = fold::detectSignConversionInContext(unit->getASTContext(), b, s);
    return {std::move(findings), s};
}

} // namespace

TEST_CASE("sign-conversion: signed to unsigned param conversion is latent",
          "[sign][signed-to-unsigned]") {
    auto [findings, stats] = run("unsigned f(int x){ unsigned y = x; return y; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::SignConversion);
    // Conversion of a function parameter is caller-precondition-dependent
    // (mirrors div-by-zero / int-overflow latent contract): the callee alone
    // cannot prove a negative value is reachable.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("sign-conversion: unsigned to signed is flagged", "[sign][unsigned-to-signed]") {
    auto [findings, stats] = run("int f(unsigned x){ int y = x; return y; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::SignConversion);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("sign-conversion: havoc-backed SAT result is heuristic", "[sign][havoc][precision]") {
    auto [findings, stats] = run("extern void mutate(int&); unsigned f(){ int x = 0; mutate(x); "
                                 "unsigned y = x; return y; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].confidence == fold::Confidence::Heuristic);
    REQUIRE(findings[0].evidence.proof_mode == "over-approximated");
    REQUIRE(stats.sat == 1);
}