// B2: counted-loop summarization. When a counted loop's trip count exceeds the
// unroll bound, the induction variable is bound to its full closed-form range
// and the body is walked once, so an in-body OOB at a high index is exposed
// (bounded unroll would only see i = 0,1,2 and miss it). Findings from the
// summarized walk are over-approximations and carry lower (heuristic)
// confidence, never Proved.
#include <clang/Frontend/ASTUnit.h>
#include <clang/Tooling/Tooling.h>

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

#include "fold/detect/cross_tu_cache.hpp"
#include "fold/detect/oob_access.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/budget.hpp"

namespace {

std::vector<fold::Finding> run(const std::string& code) {
    // Cross-TU cache is a singleton; clear it so a prior case's function
    // summary (these cases all define `f`) cannot leak buffer bounds across
    // cases the way separate `fold scan` invocations never would.
    fold::detect::CrossTUCache::instance().clear();
    auto unit = clang::tooling::buildASTFromCodeWithArgs(code, {"-std=c++20"}, "input.cpp");
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    return fold::detectOOBAccessInContext(unit->getASTContext(), b, s);
}

} // namespace

TEST_CASE("loop-summary: high-index OOB in a counted loop is found", "[loop][oob][summary]") {
    // i reaches 99; a[i] is out of bounds for i >= 10. Bounded unroll (3) only
    // sees a[0..2] and misses this; the summarized full range [0,99] exposes it.
    auto findings = run("void f(){ int a[10]; for (int i = 0; i < 100; ++i) a[i] = i; }");
    REQUIRE(findings.size() >= 1);
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    // Over-approximation: must NOT be reported as a proof.
    REQUIRE(findings[0].confidence != fold::Confidence::Proved);
}

TEST_CASE("loop-summary: affine (symbolic-bound) loop exposes potential OOB",
          "[loop][oob][summary]") {
    // `i < n` with n a parameter: i can reach >= 10 when n > 10, so a[i] is a
    // potential overflow. The affine summary binds i to [0, n) and exposes it
    // (bounded unroll sees only i=0,1,2). Over-approximation -> not Proved.
    auto findings = run("void f(int n){ int a[10]; for (int i = 0; i < n; ++i) a[i] = i; }");
    REQUIRE(findings.size() >= 1);
    REQUIRE(findings[0].kind == fold::FindingKind::OOBAccess);
    REQUIRE(findings[0].confidence != fold::Confidence::Proved);
}

TEST_CASE("loop-summary: in-bounds counted loop is not flagged", "[loop][oob][summary]") {
    // i in [0,99], a has 100 elements -> every access in bounds -> no finding.
    auto findings = run("void f(){ int a[100]; for (int i = 0; i < 100; ++i) a[i] = i; }");
    bool any_oob = std::any_of(findings.begin(), findings.end(), [](const fold::Finding& f) {
        return f.kind == fold::FindingKind::OOBAccess;
    });
    REQUIRE_FALSE(any_oob);
}