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

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

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

namespace {

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

std::vector<fold::Finding> runDead(const std::string& code) {
    auto unit = parse(code);
    REQUIRE(unit);
    fold::SolverBudget b;
    fold::SolverStats s;
    return fold::detectDeadBranchesInContext(unit->getASTContext(), b, s);
}

} // namespace

TEST_CASE("phi-merge: branch joining produces an unreachable downstream then", "[phi][dead]") {
    // Both arms assign x to a small positive constant. After phi-merge the
    // post-if value is ite(cond, 10, 20), which is provably never < 0. The
    // second `if (x < 0)` then-arm becomes unreachable only if the walker
    // merges the two arm states; without phi-merge the post-if x reverts to
    // the pre-if free symbolic value and x < 0 is trivially feasible.
    auto findings = runDead("int f(int arg){"
                            "  int x;"
                            "  if (arg > 0) { x = 10; } else { x = 20; }"
                            "  if (x < 0) { return 1; }"
                            "  return 0;"
                            "}");
    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == fold::FindingKind::Dead);
    REQUIRE(findings[0].confidence == fold::Confidence::Proved);
}

TEST_CASE("phi-merge: variable touched in one arm only inherits pre-if value", "[phi][dead]") {
    auto findings = runDead("int f(int arg){"
                            "  int x = 5;"
                            "  if (arg > 0) { x = 10; }"
                            "  if (x < 0) { return -1; }"
                            "  return x;"
                            "}");
    // Both possible values of x (5 or 10) are non-negative, so x < 0 is dead.
    REQUIRE(findings.size() == 1);
}