#include <z3++.h>

#include <catch2/catch_test_macros.hpp>
#include <cstddef>
#include <cstdint>

#include "fold/fuzz/model_to_bytes.hpp"

using fold::fuzz::extractIntegerBytes;
using fold::fuzz::extractPointerWitness;
using fold::fuzz::packLittleEndian;
using fold::fuzz::ParamWitness;
using fold::fuzz::PointerShape;
using fold::fuzz::WitnessKind;

namespace {

// Make a model that binds `c` to the given concrete value, then return
// the model and the constant expression for the caller to use.
struct ModelFixture {
    z3::context ctx;
    z3::solver solver{ctx};
    z3::expr c = ctx.bv_const("p", 64);

    z3::model materialize(std::uint64_t value) {
        solver.reset();
        solver.add(c == ctx.bv_val(value, 64));
        const auto res = solver.check();
        REQUIRE(res == z3::sat);
        return solver.get_model();
    }
};

} // namespace

TEST_CASE("packLittleEndian: 8-bit emits one byte", "[fuzz][bytes]") {
    auto out = packLittleEndian(0xABULL, 8);
    REQUIRE(out.size() == 1);
    REQUIRE(static_cast<std::uint8_t>(out[0]) == 0xAB);
}

TEST_CASE("packLittleEndian: 32-bit value packs in little-endian order", "[fuzz][bytes]") {
    auto out = packLittleEndian(0xDEADBEEFULL, 32);
    REQUIRE(out.size() == 4);
    REQUIRE(static_cast<std::uint8_t>(out[0]) == 0xEF);
    REQUIRE(static_cast<std::uint8_t>(out[1]) == 0xBE);
    REQUIRE(static_cast<std::uint8_t>(out[2]) == 0xAD);
    REQUIRE(static_cast<std::uint8_t>(out[3]) == 0xDE);
}

TEST_CASE("packLittleEndian: 64-bit full-width round-trip", "[fuzz][bytes]") {
    auto out = packLittleEndian(0x1122334455667788ULL, 64);
    REQUIRE(out.size() == 8);
    REQUIRE(static_cast<std::uint8_t>(out[0]) == 0x88);
    REQUIRE(static_cast<std::uint8_t>(out[7]) == 0x11);
}

TEST_CASE("packLittleEndian: non-byte-aligned width rounds up", "[fuzz][bytes]") {
    // 9-bit value: 0x1FF (all 9 bits set). Should produce 2 bytes:
    // low byte 0xFF, high byte with only bit-0 set (0x01).
    auto out = packLittleEndian(0x1FFULL, 9);
    REQUIRE(out.size() == 2);
    REQUIRE(static_cast<std::uint8_t>(out[0]) == 0xFF);
    REQUIRE(static_cast<std::uint8_t>(out[1]) == 0x01);
}

TEST_CASE("packLittleEndian: wide value masks to bit_width", "[fuzz][bytes]") {
    // 32-bit width with a value whose upper 32 bits are nonzero.
    // The upper bits must be dropped so the harness reads back the
    // value the source-language type would actually observe.
    auto out = packLittleEndian(0xFFFF'FFFF'AAAA'BBBBULL, 32);
    REQUIRE(out.size() == 4);
    REQUIRE(static_cast<std::uint8_t>(out[0]) == 0xBB);
    REQUIRE(static_cast<std::uint8_t>(out[3]) == 0xAA);
}

TEST_CASE("packLittleEndian: zero bit_width emits empty buffer", "[fuzz][bytes]") {
    auto out = packLittleEndian(0xDEADBEEFULL, 0);
    REQUIRE(out.empty());
}

TEST_CASE("extractIntegerBytes: BV-64 round-trips a 32-bit value", "[fuzz][bytes][model]") {
    ModelFixture fx;
    auto model = fx.materialize(0xDEADBEEFULL);

    ParamWitness w;
    w.kind = WitnessKind::Integer;
    w.bit_width = 32;
    w.is_signed = false;
    REQUIRE(extractIntegerBytes(model, fx.c, w));
    REQUIRE(w.bytes.size() == 4);
    REQUIRE(static_cast<std::uint8_t>(w.bytes[0]) == 0xEF);
    REQUIRE(static_cast<std::uint8_t>(w.bytes[3]) == 0xDE);
}

TEST_CASE("extractIntegerBytes: bit_width defaults to sort width", "[fuzz][bytes][model]") {
    ModelFixture fx;
    auto model = fx.materialize(0x42ULL);

    ParamWitness w;
    w.kind = WitnessKind::Integer;
    // Leave w.bit_width == 0 on purpose.
    REQUIRE(extractIntegerBytes(model, fx.c, w));
    REQUIRE(w.bit_width == 64);
    REQUIRE(w.bytes.size() == 8);
    REQUIRE(static_cast<std::uint8_t>(w.bytes[0]) == 0x42);
}

TEST_CASE("extractIntegerBytes: bool expression emits 0 or 1", "[fuzz][bytes][model]") {
    z3::context ctx;
    z3::solver solver(ctx);
    z3::expr b = ctx.bool_const("b");
    solver.add(b);
    REQUIRE(solver.check() == z3::sat);
    auto model = solver.get_model();

    ParamWitness w;
    w.kind = WitnessKind::Bool;
    w.bit_width = 8;
    REQUIRE(extractIntegerBytes(model, b, w));
    REQUIRE(w.bytes.size() == 1);
    REQUIRE(static_cast<std::uint8_t>(w.bytes[0]) == 1);
}

TEST_CASE("extractPointerWitness: zero value → ConcreteNull", "[fuzz][bytes][pointer]") {
    ModelFixture fx;
    auto model = fx.materialize(0);

    ParamWitness w;
    REQUIRE(extractPointerWitness(model, fx.c, /*default_buffer_bytes=*/64, w));
    REQUIRE(w.kind == WitnessKind::Pointer);
    REQUIRE(w.pointer.shape == PointerShape::ConcreteNull);
    REQUIRE(w.pointer.buffer_bytes == 0);
}

TEST_CASE("extractPointerWitness: non-zero value → NullableBuffer", "[fuzz][bytes][pointer]") {
    ModelFixture fx;
    auto model = fx.materialize(0xDEAD'BEEFULL);

    ParamWitness w;
    REQUIRE(extractPointerWitness(model, fx.c, /*default_buffer_bytes=*/128, w));
    REQUIRE(w.kind == WitnessKind::Pointer);
    REQUIRE(w.pointer.shape == PointerShape::NullableBuffer);
    REQUIRE(w.pointer.buffer_bytes == 128);
    REQUIRE(w.pointer.buffer_contents.empty());
}