Skip to content

Commit

Permalink
move checker and transformer to different cpp files
Browse files Browse the repository at this point in the history 
Signed-off-by: Elazar Gershuni <[email protected]>
  • Loading branch information
@elazarg
elazarg committed Nov 10, 2024
1 parent b825d2d commit e8dc875
Show file tree
Hide file tree
Showing 8 changed files with 3,052 additions and 3,028 deletions.
444 changes: 444 additions & 0 deletions src/crab/ebpf_checker.cpp
View file

Large diffs are not rendered by default.

2,801 changes: 92 additions & 2,709 deletions src/crab/ebpf_domain.cpp
View file

Large diffs are not rendered by default.

174 changes: 21 additions & 153 deletions src/crab/ebpf_domain.hpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,24 @@

namespace crab {

// Pointers in the BPF VM are defined to be 64 bits. Some contexts, like
// data, data_end, and meta in Linux's struct xdp_md are only 32 bit offsets
// from a base address not exposed to the program, but when a program is loaded,
// the offsets get replaced with 64-bit address pointers. However, we currently
// need to do pointer arithmetic on 64-bit numbers so for now we cap the interval
// to 32 bits.
constexpr int MAX_PACKET_SIZE = 0xffff;
constexpr int64_t PTR_MAX = std::numeric_limits<int32_t>::max() - MAX_PACKET_SIZE;

class ebpf_domain_t;

void ebpf_domain_transform(ebpf_domain_t& inv, const Instruction& ins);
void ebpf_domain_assume(ebpf_domain_t& dom, const Assertion& assertion);
std::vector<std::string> ebpf_domain_check(ebpf_domain_t& dom, const label_t& label, const Assertion& assertion);

// TODO: make this an explicit instruction
void ebpf_domain_initialize_loop_counter(ebpf_domain_t& dom, const label_t& label);

class ebpf_domain_t final {
friend class ebpf_checker;
friend class ebpf_transformer;
Expand Down Expand Up @@ -49,7 +67,10 @@ class ebpf_domain_t final {
static ebpf_domain_t calculate_constant_limits();
extended_number get_loop_count_upper_bound() const;

static ebpf_domain_t setup_entry(bool init_r1);
static ebpf_domain_t from_constraints(const std::set<std::string>& constraints, bool setup_constraints);
void initialize_packet();

string_invariant to_set() const;

private:
Expand Down Expand Up @@ -89,157 +110,4 @@ class ebpf_domain_t final {
TypeDomain type_inv;
};

class ebpf_checker final {
ebpf_domain_t& dom;
// shorthands:
NumAbsDomain& m_inv;
domains::array_domain_t& stack;
TypeDomain& type_inv;

public:
explicit ebpf_checker(ebpf_domain_t& dom) : dom(dom), m_inv(dom.m_inv), stack(dom.stack), type_inv(dom.type_inv) {}

void operator()(const Assertion&);

void operator()(const Addable&);
void operator()(const Comparable&);
void operator()(const FuncConstraint&);
void operator()(const ValidDivisor&);
void operator()(const TypeConstraint&);
void operator()(const ValidAccess&);
void operator()(const ValidCall&);
void operator()(const ValidMapKeyValue&);
void operator()(const ValidSize&);
void operator()(const ValidStore&);
void operator()(const ZeroCtxOffset&);
void operator()(const BoundedLoopCount&);

typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string);
void set_require_check(std::function<check_require_func_t> f);

private:
// memory check / load / store
void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
void check_access_context(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub) const;
void check_access_packet(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
std::optional<variable_t> packet_size) const;
void check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
variable_t shared_region_size) const;
std::function<check_require_func_t> check_require{};
std::string current_assertion;
void require(NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s) const;
};

class ebpf_transformer final {
ebpf_domain_t& dom;
// shorthands:
NumAbsDomain& m_inv;
domains::array_domain_t& stack;
TypeDomain& type_inv;

public:
explicit ebpf_transformer(ebpf_domain_t& dom)
: dom(dom), m_inv(dom.m_inv), stack(dom.stack), type_inv(dom.type_inv) {}

// abstract transformers
void operator()(const Assume&);
void operator()(const Bin&);
void operator()(const Call&);
void operator()(const CallLocal&);
void operator()(const Callx&);
void operator()(const Exit&);
void operator()(const Jmp&) const;
void operator()(const LoadMapFd&);
void operator()(const Atomic&);
void operator()(const Mem&);
void operator()(const Packet&);
void operator()(const Un&);
void operator()(const Undefined&);
void operator()(const IncrementLoopCounter&);

void initialize_loop_counter(const label_t& label);

static ebpf_domain_t setup_entry(bool init_r1);

private:
void assign(variable_t lhs, variable_t rhs);
void assign(variable_t x, const linear_expression_t& e);
void assign(variable_t x, int64_t e);

void apply(arith_binop_t op, variable_t x, variable_t y, const number_t& z, int finite_width);
void apply(arith_binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);
void apply(bitwise_binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);
void apply(bitwise_binop_t op, variable_t x, variable_t y, const number_t& k, int finite_width);
void apply(binop_t op, variable_t x, variable_t y, const number_t& z, int finite_width);
void apply(binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);

void add(const Reg& reg, int imm, int finite_width);
void add(variable_t lhs, variable_t op2);
void add(variable_t lhs, const number_t& op2);
void sub(variable_t lhs, variable_t op2);
void sub(variable_t lhs, const number_t& op2);
void add_overflow(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void add_overflow(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void sub_overflow(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void sub_overflow(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void neg(variable_t lhss, variable_t lhsu, int finite_width);
void mul(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void mul(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void sdiv(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void sdiv(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void udiv(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void udiv(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void srem(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void srem(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);
void urem(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void urem(variable_t lhss, variable_t lhsu, const number_t& op2, int finite_width);

void bitwise_and(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void bitwise_and(variable_t lhss, variable_t lhsu, const number_t& op2);
void bitwise_or(variable_t lhss, variable_t lhsu, variable_t op2, int finite_width);
void bitwise_or(variable_t lhss, variable_t lhsu, const number_t& op2);
void bitwise_xor(variable_t lhsss, variable_t lhsu, variable_t op2, int finite_width);
void bitwise_xor(variable_t lhss, variable_t lhsu, const number_t& op2);
void shl(const Reg& reg, int imm, int finite_width);
void shl_overflow(variable_t lhss, variable_t lhsu, variable_t op2);
void shl_overflow(variable_t lhss, variable_t lhsu, const number_t& op2);
void lshr(const Reg& reg, int imm, int finite_width);
void ashr(const Reg& dst_reg, const linear_expression_t& right_svalue, int finite_width);
void sign_extend(const Reg& dst_reg, const linear_expression_t& right_svalue, int finite_width, Bin::Op op);

void assume(const linear_constraint_t& cst);

/// Forget everything we know about the value of a variable.
void havoc(variable_t v);

/// Forget everything about all offset variables for a given register.
void havoc_offsets(const Reg& reg);

void scratch_caller_saved_registers();
void save_callee_saved_registers(const std::string& prefix);
void restore_callee_saved_registers(const std::string& prefix);
void havoc_subprogram_stack(const std::string& prefix);
void forget_packet_pointers();
void do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null);

void assign_valid_ptr(const Reg& dst_reg, bool maybe_null);

void recompute_stack_numeric_size(NumAbsDomain& inv, const Reg& reg) const;
void recompute_stack_numeric_size(NumAbsDomain& inv, variable_t type_variable) const;
void do_load_stack(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr, int width,
const Reg& src_reg);
void do_load_ctx(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr_vague, int width);
void do_load_packet_or_shared(NumAbsDomain& inv, const Reg& target_reg, const linear_expression_t& addr, int width);
void do_load(const Mem& b, const Reg& target_reg);

void do_store_stack(NumAbsDomain& inv, const linear_expression_t& addr, int width,
const linear_expression_t& val_type, const linear_expression_t& val_svalue,
const linear_expression_t& val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);

void do_mem_store(const Mem& b, const linear_expression_t& val_type, const linear_expression_t& val_svalue,
const linear_expression_t& val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);

static void initialize_packet(ebpf_domain_t& inv);
}; // end ebpf_domain_t

} // namespace crab
Loading

0 comments on commit e8dc875

Please sign in to comment.