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

#include "fold/cli/finding_evidence.hpp"
#include "fold/cli/source_tu_runner.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/theory.hpp"

TEST_CASE("source detector stats enable every solver profile", "[source-tu-runner]") {
    fold::cli::SourceDetectorStats stats;
    stats.setProfilingEnabled(true);

    const std::vector<const fold::SolverStats*> all_stats = {
        &stats.dead,           &stats.equiv,           &stats.class_dup,
        &stats.div_by_zero,    &stats.null_deref,      &stats.int_overflow,
        &stats.int_truncation, &stats.sign_conversion, &stats.oob,
        &stats.taint_track,    &stats.sql_injection,   &stats.always_condition,
        &stats.unreachable,    &stats.double_free,     &stats.redundant_store,
        &stats.memory_leak,    &stats.use_after_move,
    };
    for (const auto* detector_stats : all_stats)
        REQUIRE(detector_stats->profiling_enabled);

    stats.setProfilingEnabled(false);
    for (const auto* detector_stats : all_stats)
        REQUIRE_FALSE(detector_stats->profiling_enabled);
}

TEST_CASE("solver query profiling stops detailed collection at its sample cap",
          "[source-tu-runner][profile]") {
    fold::SolverStats stats;
    stats.profiling_enabled = true;
    for (std::size_t index = 0; index < fold::SolverStats::kMaxQuerySamples; ++index)
        stats.recordQuerySample({});

    REQUIRE_FALSE(stats.querySampleCapacityAvailable());
    stats.recordQuerySample({});
    CHECK(stats.query_samples.size() == fold::SolverStats::kMaxQuerySamples);
    CHECK(stats.query_samples_dropped == 1);
}

TEST_CASE("finding evidence annotation is stable and slice-scoped", "[source-tu-runner]") {
    std::vector<fold::Finding> findings(2);
    findings[0].evidence.detector_name = "preserved";
    const std::vector<std::string> bail_reasons = {"unsupported-call", "deadline",
                                                   "unsupported-call"};

    fold::cli::annotateFindings(findings, 1, "null-deref", "exact", nullptr, &bail_reasons, true,
                                true);

    REQUIRE(findings[0].evidence.detector_name == "preserved");
    REQUIRE(findings[1].evidence.detector_name == "null-deref");
    REQUIRE(findings[1].evidence.proof_mode == "exact");
    REQUIRE(findings[1].evidence.bail_reasons ==
            std::vector<std::string>{"deadline", "unsupported-call"});
    REQUIRE(findings[1].evidence.is_summary_backed);
    REQUIRE(findings[1].evidence.has_cross_tu_corroboration);
}

TEST_CASE("finding evidence annotation preserves detector-specific proof metadata",
          "[source-tu-runner][evidence]") {
    std::vector<fold::Finding> findings(1);
    findings[0].evidence.detector_name = "div-by-zero";
    findings[0].evidence.proof_mode = "precondition";
    findings[0].evidence.bail_reasons = {"model-imprecise"};
    findings[0].evidence.is_summary_backed = true;

    const std::vector<std::string> common_bails = {"deadline", "model-imprecise"};
    fold::cli::annotateFindings(findings, 0, "composite", "exact", nullptr, &common_bails, false,
                                false);

    REQUIRE(findings[0].evidence.detector_name == "div-by-zero");
    REQUIRE(findings[0].evidence.proof_mode == "precondition");
    REQUIRE(findings[0].evidence.bail_reasons ==
            std::vector<std::string>{"deadline", "model-imprecise"});
    REQUIRE(findings[0].evidence.is_summary_backed);
    REQUIRE_FALSE(findings[0].evidence.has_cross_tu_corroboration);
}