#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/int_truncation.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::detectIntTruncationInContext(unit->getASTContext(), b, s);
    return {std::move(findings), s};
}

} // namespace

TEST_CASE("int-truncation: `char c = 256` in entry-less extern is latent",
          "[truncation][literal]") {
    auto [findings, stats] = run("int f(){ char c = 256; return c; }");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::IntTruncation);
    // `f` is an extern function in an entry-less TU (no bad()/good()/main):
    // the finding is caller-precondition at the file level (iter-291
    // function-level helper gate), so it is demoted to latent. Gold labels
    // only `_NN a` entry files, where this stays Proved via tuHasJulietEntry.
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.sat == 1);
}

TEST_CASE("int-truncation: bounded narrowing is suppressed", "[truncation][guarded]") {
    auto [findings, stats] =
        run("int f(int x){ if (x >= 0 && x < 100) { short s = x; return s; } return 0; }");
    REQUIRE(findings.empty());
    REQUIRE(stats.queries == 1);
    REQUIRE(stats.unsat == 1);
}

TEST_CASE("int-truncation: havoc-backed SAT result is latent (entry-less extern)",
          "[truncation][havoc][precision]") {
    auto [findings, stats] =
        run("extern void mutate(int&); int f(){ int x = 0; mutate(x); short y = x; return y; }");
    REQUIRE(findings.size() == 1);
    // `f` is an extern function in an entry-less TU (no bad()/good()/main):
    // the truncation of a caller-mutated value is caller-precondition, so the
    // finding is demoted to latent (iter-291 function-level helper gate).
    REQUIRE(findings[0].evidence.latent);
    REQUIRE(findings[0].confidence == fold::Confidence::Latent);
    REQUIRE(stats.sat == 1);
}