// RF-9: Rust IR → Z3 encoder unit tests.
//
// Validates that encodeRustIr can walk RustExprNode trees and fire
// SafetyObserver hooks for arithmetic, deref, and call hazards.

#include <z3++.h>

#include <catch2/catch_test_macros.hpp>

#include "fold/ir/expr.hpp"
#include "fold/ir/expr_json.hpp"
#include "fold/ir/opcode.hpp"
#include "fold/ir/source_loc.hpp"
#include "fold/report/finding.hpp"
#include "fold/symbolic/language_ir_observer.hpp"
#include "fold/symbolic/rust_ir_encoder.hpp"
#include "fold/symbolic/safety_observer.hpp"

using fold::ir::BinaryOpcode;
using fold::ir::Expr;
using fold::ir::RustExprNode;
using fold::ir::RustNodeArena;
using fold::ir::SourceLoc;
using fold::symbolic::encodeRustIr;

namespace {

// Minimal SafetyObserver that counts hook invocations.
struct CountingObserver : public fold::SafetyObserver {
    int deref_count = 0;
    int arith_count = 0;
    int div_count = 0;
    int call_count = 0;
    int subscript_count = 0;
    int function_start_count = 0;
    int function_end_count = 0;

    void onFunctionStart(const clang::FunctionDecl*, z3::solver*) override {
        ++function_start_count;
    }
    void onFunctionEnd(const clang::FunctionDecl*) override { ++function_end_count; }

    void onPointerDeref(const z3::expr&, const fold::ir::Expr&, const z3::expr&,
                        const clang::VarDecl*, const fold::ir::SourceLoc&,
                        const fold::symbolic::HeapAccessInfo*, const fold::DefUseContext*,
                        const fold::SymbolicEnv*) override {
        ++deref_count;
    }

    void onBinaryArith(BinOp, const z3::expr&, const z3::expr&, const fold::ir::Expr&,
                       const fold::ir::Expr&, const z3::expr&, const fold::ir::SourceLoc&, bool,
                       unsigned, const fold::SymbolicEnv*, const fold::DefUseContext*) override {
        ++arith_count;
    }

    void onDivision(const z3::expr&, const z3::expr&, const fold::ir::Expr&, const fold::ir::Expr&,
                    const z3::expr&, const fold::ir::SourceLoc&, bool, unsigned,
                    const fold::DefUseContext*, const fold::SymbolicEnv*) override {
        ++div_count;
    }

    void onLibraryCall(const fold::ir::Call&, const std::string&, const std::vector<z3::expr>&,
                       const z3::expr&, const fold::ir::SourceLoc&) override {
        ++call_count;
    }

    void onArraySubscript(const z3::expr&, int, const z3::expr&, const fold::ir::SourceLoc&,
                          const fold::symbolic::HeapAccessInfo*, const fold::DefUseContext*,
                          const fold::SymbolicEnv*, const clang::Expr*,
                          const clang::VarDecl*) override {
        ++subscript_count;
    }
};

} // namespace

TEST_CASE("Rust IR encoder fires function start/end hooks", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* root = arena.alloc();
    root->kind = Expr::Kind::IntegerLiteral;
    root->int_value = 42;
    root->int_width = 32;

    encodeRustIr(root, "test::empty_fn", ctx, obs);

    REQUIRE(obs.function_start_count == 1);
    REQUIRE(obs.function_end_count == 1);
}

TEST_CASE("Rust IR encoder fires deref observer for Deref nodes", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* ptr = arena.alloc();
    ptr->kind = Expr::Kind::DeclRef;
    ptr->declref_symbol = "crate::p";
    auto* deref = arena.alloc();
    deref->kind = Expr::Kind::Deref;
    deref->unary_sub = ptr;

    encodeRustIr(deref, "test::deref_fn", ctx, obs);

    REQUIRE(obs.deref_count == 1);
}

TEST_CASE("Rust IR encoder fires arithmetic observer for BinaryOp Add", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* lhs = arena.alloc();
    lhs->kind = Expr::Kind::IntegerLiteral;
    lhs->int_value = 100;
    lhs->int_width = 32;
    auto* rhs = arena.alloc();
    rhs->kind = Expr::Kind::DeclRef;
    rhs->declref_symbol = "crate::x";
    auto* add = arena.alloc();
    add->kind = Expr::Kind::BinaryOp;
    add->binary_op = BinaryOpcode::Add;
    add->binary_lhs = lhs;
    add->binary_rhs = rhs;

    encodeRustIr(add, "test::add_fn", ctx, obs);

    REQUIRE(obs.arith_count == 1);
}

TEST_CASE("Rust IR encoder fires division observer for BinaryOp Div", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* lhs = arena.alloc();
    lhs->kind = Expr::Kind::DeclRef;
    lhs->declref_symbol = "crate::a";
    auto* rhs = arena.alloc();
    rhs->kind = Expr::Kind::IntegerLiteral;
    rhs->int_value = 0;
    rhs->int_width = 32;
    auto* div = arena.alloc();
    div->kind = Expr::Kind::BinaryOp;
    div->binary_op = BinaryOpcode::Div;
    div->binary_lhs = lhs;
    div->binary_rhs = rhs;

    encodeRustIr(div, "test::div_fn", ctx, obs);

    REQUIRE(obs.div_count == 1);
}

TEST_CASE("Rust IR encoder fires library-call observer for transmute", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* arg = arena.alloc();
    arg->kind = Expr::Kind::DeclRef;
    arg->declref_symbol = "crate::x";
    auto* call = arena.alloc();
    call->kind = Expr::Kind::Call;
    call->callee_name = "transmute";
    call->call_args = {arg};

    encodeRustIr(call, "test::transmute_fn", ctx, obs);

    REQUIRE(obs.call_count == 1);
}

TEST_CASE("Rust IR encoder fires array-subscript observer", "[rust_ir][encoder]") {
    z3::context ctx;
    CountingObserver obs;

    RustNodeArena arena;
    auto* base = arena.alloc();
    base->kind = Expr::Kind::DeclRef;
    base->declref_symbol = "crate::xs";
    auto* idx = arena.alloc();
    idx->kind = Expr::Kind::IntegerLiteral;
    idx->int_value = 5;
    idx->int_width = 64;
    auto* sub = arena.alloc();
    sub->kind = Expr::Kind::ArraySubscript;
    sub->array_base = base;
    sub->array_index = idx;

    encodeRustIr(sub, "test::index_fn", ctx, obs);

    REQUIRE(obs.subscript_count == 1);
}

TEST_CASE("Rust IR encoder propagates MIR Assign into later division hazards",
          "[rust_ir][encoder][assign]") {
    z3::context ctx;
    std::vector<fold::Finding> findings;
    fold::symbolic::LanguageIrObserverOptions options;
    options.backend = "rust";
    options.enable_div_zero = true;
    auto observer = fold::symbolic::makeLanguageIrSafetyObserver(findings, std::move(options));

    RustNodeArena arena;
    auto* lhs = arena.alloc();
    lhs->kind = Expr::Kind::DeclRef;
    lhs->declref_symbol = "crate::x";

    auto* zero = arena.alloc();
    zero->kind = Expr::Kind::IntegerLiteral;
    zero->int_value = 0;
    zero->int_width = 32;

    auto* assign = arena.alloc();
    assign->kind = Expr::Kind::BinaryOp;
    assign->binary_op = BinaryOpcode::Assign;
    assign->binary_lhs = lhs;
    assign->binary_rhs = zero;

    auto* num = arena.alloc();
    num->kind = Expr::Kind::IntegerLiteral;
    num->int_value = 1;
    num->int_width = 32;

    auto* use = arena.alloc();
    use->kind = Expr::Kind::DeclRef;
    use->declref_symbol = "crate::x";

    auto* div = arena.alloc();
    div->kind = Expr::Kind::BinaryOp;
    div->binary_op = BinaryOpcode::Div;
    div->binary_lhs = num;
    div->binary_rhs = use;
    div->loc.file = "assign.rs";
    div->loc.line = 12;
    div->loc.column = 5;

    auto* seq = arena.alloc();
    seq->kind = Expr::Kind::Call;
    seq->callee_name = "mir_seq";
    seq->call_args = {assign, div};

    encodeRustIr(seq, "test::assign_div_zero", ctx, *observer);

    REQUIRE(findings.size() == 1);
    REQUIRE(findings.front().kind == fold::FindingKind::DivByZero);
    REQUIRE(findings.front().locations.front().line == 12);
}

TEST_CASE("Rust IR encoder overwrites MIR Assign state on reassignment",
          "[rust_ir][encoder][assign]") {
    z3::context ctx;
    std::vector<fold::Finding> findings;
    fold::symbolic::LanguageIrObserverOptions options;
    options.backend = "rust";
    options.enable_div_zero = true;
    auto observer = fold::symbolic::makeLanguageIrSafetyObserver(findings, std::move(options));

    RustNodeArena arena;
    auto* lhs1 = arena.alloc();
    lhs1->kind = Expr::Kind::DeclRef;
    lhs1->declref_symbol = "crate::x";
    auto* zero = arena.alloc();
    zero->kind = Expr::Kind::IntegerLiteral;
    zero->int_value = 0;
    zero->int_width = 32;
    auto* assign_zero = arena.alloc();
    assign_zero->kind = Expr::Kind::BinaryOp;
    assign_zero->binary_op = BinaryOpcode::Assign;
    assign_zero->binary_lhs = lhs1;
    assign_zero->binary_rhs = zero;

    auto* lhs2 = arena.alloc();
    lhs2->kind = Expr::Kind::DeclRef;
    lhs2->declref_symbol = "crate::x";
    auto* one = arena.alloc();
    one->kind = Expr::Kind::IntegerLiteral;
    one->int_value = 1;
    one->int_width = 32;
    auto* assign_one = arena.alloc();
    assign_one->kind = Expr::Kind::BinaryOp;
    assign_one->binary_op = BinaryOpcode::Assign;
    assign_one->binary_lhs = lhs2;
    assign_one->binary_rhs = one;

    auto* num = arena.alloc();
    num->kind = Expr::Kind::IntegerLiteral;
    num->int_value = 1;
    num->int_width = 32;
    auto* use = arena.alloc();
    use->kind = Expr::Kind::DeclRef;
    use->declref_symbol = "crate::x";
    auto* div = arena.alloc();
    div->kind = Expr::Kind::BinaryOp;
    div->binary_op = BinaryOpcode::Div;
    div->binary_lhs = num;
    div->binary_rhs = use;
    div->loc.file = "assign.rs";
    div->loc.line = 27;
    div->loc.column = 9;

    auto* seq = arena.alloc();
    seq->kind = Expr::Kind::Call;
    seq->callee_name = "mir_seq";
    seq->call_args = {assign_zero, assign_one, div};

    encodeRustIr(seq, "test::assign_overwrite", ctx, *observer);

    REQUIRE(findings.empty());
}