#include <z3++.h>

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

#include "fold/binary/binary_bb_observer.hpp"
#include "fold/ir/binary_expr.hpp"
#include "fold/ir/source_loc.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/safety_observer.hpp"

using namespace fold;
using namespace fold::binary;
using namespace fold::ir;
using namespace fold::symbolic;

namespace {

// Helper: build a synthetic SourceLoc for testing.
ir::SourceLoc testLoc(std::string file, std::uint32_t line) {
    ir::SourceLoc loc;
    loc.file = std::move(file);
    loc.line = line;
    loc.column = 0;
    return loc;
}

// Helper: count findings by detector name.
int countByDetector(const std::vector<Finding>& findings, const std::string& detector) {
    int count = 0;
    for (const auto& f : findings) {
        if (f.evidence.detector_name == detector)
            ++count;
    }
    return count;
}

// Helper: count findings by kind.
int countByKind(const std::vector<Finding>& findings, FindingKind kind) {
    int count = 0;
    for (const auto& f : findings) {
        if (f.kind == kind)
            ++count;
    }
    return count;
}

} // namespace

TEST_CASE("BinaryBBObserver: default-constructed observer emits no findings for empty run",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_func", &s);
    obs.onFunctionEndIr("test_func");

    REQUIRE(findings.empty());
}

// ── Null-pointer dereference ────────────────────────────────────

TEST_CASE("BinaryBBObserver: null-pointer deref triggers finding when ptr==0 under path",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_deref", &s);

    z3::expr ptr = z3_ctx->bv_val(0, 64); // null pointer
    ir::Expr ptrExpr;
    z3::expr path = z3_ctx->bool_val(true);
    ir::Symbol sym;
    auto loc = testLoc("/tmp/test_binary", 0x4010);

    obs.onPointerDerefIr(ptr, ptrExpr, path, sym, loc, nullptr, nullptr, nullptr);
    obs.onFunctionEndIr("test_deref");

    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == FindingKind::NullDeref);
    REQUIRE(findings[0].confidence == Confidence::Heuristic);
    REQUIRE(findings[0].evidence.detector_name == "binary-null-deref");
    REQUIRE(findings[0].evidence.backend == "binary");
    REQUIRE(findings[0].evidence.proof_mode == "binary-pcode-z3-heuristic");
    REQUIRE(findings[0].evidence.binary_vaddr == 0x4010);
    REQUIRE(findings[0].locations[0].function == "test_deref");
}

TEST_CASE("BinaryBBObserver: finding IDs are stable across observer instances",
          "[binary_bb_observer][identity]") {
    auto emit = [] {
        std::vector<Finding> findings;
        auto z3_ctx = std::make_shared<z3::context>();
        BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);
        z3::solver solver(*z3_ctx, "QF_BV");
        obs.onFunctionStartIr("stable", &solver);
        obs.onPointerDerefIr(z3_ctx->bv_val(0, 64), ir::Expr{}, z3_ctx->bool_val(true),
                             ir::Symbol{}, testLoc("/tmp/test_binary", 0x5150), nullptr, nullptr,
                             nullptr);
        obs.onFunctionEndIr("stable");
        REQUIRE(findings.size() == 1);
        return findings.front().id;
    };

    REQUIRE(emit() == emit());
}

TEST_CASE("BinaryBBObserver: non-null pointer does NOT trigger finding", "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_nonnull", &s);

    z3::expr ptr = z3_ctx->bv_val(0x7FFF0000, 64); // non-null
    ir::Expr ptrExpr;
    z3::expr path = z3_ctx->bool_val(true);
    ir::Symbol sym;
    auto loc = testLoc("/tmp/test_binary", 0x4020);

    obs.onPointerDerefIr(ptr, ptrExpr, path, sym, loc, nullptr, nullptr, nullptr);
    obs.onFunctionEndIr("test_nonnull");

    REQUIRE(findings.empty());
}

TEST_CASE("BinaryBBObserver: null deref not reachable when path excludes null",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_guarded", &s);

    // ptr is symbolic, but path asserts ptr != 0 (guarded deref)
    z3::expr ptr = z3_ctx->bv_const("ptr", 64);
    z3::expr guard = (ptr != z3_ctx->bv_val(0, 64)); // ptr != 0
    z3::expr path = guard;
    ir::Expr ptrExpr;
    ir::Symbol sym;
    auto loc = testLoc("/tmp/test_binary", 0x4030);

    obs.onPointerDerefIr(ptr, ptrExpr, path, sym, loc, nullptr, nullptr, nullptr);
    obs.onFunctionEndIr("test_guarded");

    // Z3 should prove UNSAT: path(ptr!=0) && hazard(ptr==0) is unsat
    REQUIRE(findings.empty());
}

// ── Division by zero ────────────────────────────────────────────

TEST_CASE("BinaryBBObserver: division by zero triggers finding when rhs==0 under path",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_div0", &s);

    z3::expr lhs = z3_ctx->bv_const("x", 64);
    z3::expr rhs = z3_ctx->bv_val(0, 64); // divisor is zero
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4040);

    obs.onBinaryArith(SafetyObserver::BinOp::Div, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      true /*signed*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_div0");

    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == FindingKind::DivByZero);
    REQUIRE(findings[0].confidence == Confidence::Heuristic);
    REQUIRE(findings[0].evidence.detector_name == "binary-div-by-zero");
    REQUIRE(findings[0].evidence.backend == "binary");
    REQUIRE(findings[0].evidence.proof_mode == "binary-pcode-z3-heuristic");
}

TEST_CASE("BinaryBBObserver: division with non-zero rhs does NOT trigger finding",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_div_ok", &s);

    z3::expr lhs = z3_ctx->bv_const("x", 64);
    z3::expr rhs = z3_ctx->bv_val(42, 64); // non-zero divisor
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4050);

    obs.onBinaryArith(SafetyObserver::BinOp::Div, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      true /*signed*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_div_ok");

    REQUIRE(findings.empty());
}

// ── Signed integer overflow ─────────────────────────────────────

TEST_CASE("BinaryBBObserver: signed ADD overflow INT_MAX + 1 triggers finding",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_add_overflow", &s);

    // INT32_MAX + 1 overflows in 32-bit signed
    z3::expr lhs = z3_ctx->bv_val(2147483647, 32); // INT32_MAX
    z3::expr rhs = z3_ctx->bv_val(1, 32);
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4060);

    obs.onBinaryArith(SafetyObserver::BinOp::Add, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      true /*signed*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_add_overflow");

    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == FindingKind::IntOverflow);
    REQUIRE(findings[0].confidence == Confidence::Heuristic);
    REQUIRE(findings[0].evidence.detector_name == "binary-int-overflow");
}

TEST_CASE("BinaryBBObserver: signed SUB overflow INT_MIN - 1 on 32-bit", "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_sub_overflow", &s);

    // INT32_MIN - 1 overflows (INT32_MIN = 0x80000000)
    z3::expr lhs = z3_ctx->bv_val(0x80000000, 32);
    z3::expr rhs = z3_ctx->bv_val(1, 32);
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4070);

    obs.onBinaryArith(SafetyObserver::BinOp::Sub, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      true /*signed*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_sub_overflow");

    REQUIRE(findings.size() == 1);
    REQUIRE(findings[0].kind == FindingKind::IntOverflow);
    REQUIRE(findings[0].evidence.detector_name == "binary-int-overflow");
}

TEST_CASE("BinaryBBObserver: safe ADD (2+3 on 32-bit) does NOT trigger overflow",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_add_safe", &s);

    z3::expr lhs = z3_ctx->bv_val(2, 32);
    z3::expr rhs = z3_ctx->bv_val(3, 32);
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4080);

    obs.onBinaryArith(SafetyObserver::BinOp::Add, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      true /*signed*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_add_safe");

    REQUIRE(findings.empty());
}

TEST_CASE("BinaryBBObserver: unsigned ADD does NOT trigger overflow finding",
          "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("test_unsigned_add", &s);

    // UINT32_MAX + 1 wraps to 0 (defined behavior for unsigned)
    z3::expr lhs = z3_ctx->bv_val(0xFFFFFFFF, 32);
    z3::expr rhs = z3_ctx->bv_val(1, 32);
    ir::Expr lhsExpr, rhsExpr;
    z3::expr path = z3_ctx->bool_val(true);
    auto loc = testLoc("/tmp/test_binary", 0x4090);

    obs.onBinaryArith(SafetyObserver::BinOp::Add, lhs, rhs, lhsExpr, rhsExpr, path, loc,
                      false /*unsigned*/, 32, nullptr, nullptr);
    obs.onFunctionEndIr("test_unsigned_add");

    REQUIRE(findings.empty());
}

// ── Multiple hazards in one function ────────────────────────────

TEST_CASE("BinaryBBObserver: multiple hazards emit multiple findings", "[binary_bb_observer]") {
    std::vector<Finding> findings;
    auto z3_ctx = std::make_shared<z3::context>();

    BinaryBBObserver obs(findings, "/tmp/test_binary", z3_ctx);

    z3::solver s(*z3_ctx, "QF_BV");
    obs.onFunctionStartIr("multi_hazard", &s);

    // 1. Null deref
    {
        z3::expr ptr = z3_ctx->bv_val(0, 64);
        ir::Expr ptrExpr;
        z3::expr path = z3_ctx->bool_val(true);
        ir::Symbol sym;
        auto loc = testLoc("/tmp/test_binary", 0x4100);
        obs.onPointerDerefIr(ptr, ptrExpr, path, sym, loc, nullptr, nullptr, nullptr);
    }

    // 2. Div by zero
    {
        z3::expr lhs = z3_ctx->bv_const("x", 64);
        z3::expr rhs = z3_ctx->bv_val(0, 64);
        ir::Expr lhsExpr, rhsExpr;
        z3::expr path = z3_ctx->bool_val(true);
        auto loc = testLoc("/tmp/test_binary", 0x4110);
        obs.onBinaryArith(SafetyObserver::BinOp::Div, lhs, rhs, lhsExpr, rhsExpr, path, loc, true,
                          32, nullptr, nullptr);
    }

    // 3. Int overflow
    {
        z3::expr lhs = z3_ctx->bv_val(2147483647, 32);
        z3::expr rhs = z3_ctx->bv_val(1, 32);
        ir::Expr lhsExpr, rhsExpr;
        z3::expr path = z3_ctx->bool_val(true);
        auto loc = testLoc("/tmp/test_binary", 0x4120);
        obs.onBinaryArith(SafetyObserver::BinOp::Add, lhs, rhs, lhsExpr, rhsExpr, path, loc, true,
                          32, nullptr, nullptr);
    }

    obs.onFunctionEndIr("multi_hazard");

    REQUIRE(findings.size() == 3);
    REQUIRE(countByKind(findings, FindingKind::NullDeref) == 1);
    REQUIRE(countByKind(findings, FindingKind::DivByZero) == 1);
    REQUIRE(countByKind(findings, FindingKind::IntOverflow) == 1);
}