366 lines
13 KiB
C++
366 lines
13 KiB
C++
#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);
|
|
}
|