Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Move checker and transformer to different cpp files #788

Merged
merged 1 commit into from
Nov 10, 2024
Merged

Move checker and transformer to different cpp files #788

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
444 changes: 444 additions & 0 deletions src/crab/ebpf_checker.cpp
View file
Open in desktop

Large diffs are not rendered by default.

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

Large diffs are not rendered by default.

174 changes: 21 additions & 153 deletions src/crab/ebpf_domain.hpp
View file
Open in desktop
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);
elazarg marked this conversation as resolved.
Show resolved Hide resolved

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
Loading