311 lines
9.6 KiB
C++
311 lines
9.6 KiB
C++
// 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());
|
|
}
|