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

Jump to bottom

Add FiniteDomain #678

Open
wants to merge 3 commits into
base: main
Choose a base branch
from
Open

Add FiniteDomain #678

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
d086ab8
add FiniteDomain
elazarg Sep 11, 2024
93c77f5
lint YAML
elazarg Sep 11, 2024
ce184b6
Merge branch 'main' into br-domain
elazarg Sep 24, 2024
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
4 changes: 4 additions & 0 deletions src/assertions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,10 @@ class AssertExtractor {
}
case Bin::Op::SUB:
if (std::holds_alternative<Reg>(ins.v)) {
if (std::get<Reg>(ins.v) == ins.dst) {
// We always allow rx -= rx
return {};
}
vector<Assert> res;
// disallow map-map since same type does not mean same offset
// TODO: map identities
Expand Down
11 changes: 9 additions & 2 deletions src/crab/add_bottom.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@

#include <optional>

#include "crab/finite_domain.hpp"
#include "crab/split_dbm.hpp"
#include "string_constraints.hpp"

Expand All @@ -12,7 +13,7 @@ namespace crab {
namespace domains {

class AddBottom final {
using T = SplitDBM;
using T = FiniteDomain;
std::optional<T> dom{};
AddBottom() {}

Expand All @@ -26,6 +27,12 @@ class AddBottom final {
AddBottom& operator=(const AddBottom& o) = default;
AddBottom& operator=(AddBottom&& o) = default;

explicit operator bool() const { return static_cast<bool>(dom); }

T* operator->() { return &dom.value(); }

const T* operator->() const { return &dom.value(); }

void set_to_top() {
if (dom) {
dom->set_to_top();
Expand Down Expand Up @@ -110,7 +117,7 @@ class AddBottom final {
if (!dom || !o.dom) {
return bottom();
}
if (auto res = (*dom).meet(*o.dom)) {
if (auto res = dom->meet(*o.dom)) {
return AddBottom(*res);
}
return bottom();
Expand Down
4 changes: 4 additions & 0 deletions src/crab/dsl_syntax.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,10 @@ inline linear_constraint_t operator>(const linear_expression_t& e, const number_

inline linear_constraint_t operator>(const number_t& n, const linear_expression_t& e) { return e < n; }

inline linear_constraint_t eq(const variable_t a, const variable_t b) {
return {a - b, constraint_kind_t::EQUALS_ZERO};
}

inline linear_constraint_t operator==(const linear_expression_t& e1, const linear_expression_t& e2) {
return linear_constraint_t(e1 - e2, constraint_kind_t::EQUALS_ZERO);
}
Expand Down
1,854 changes: 490 additions & 1,364 deletions src/crab/ebpf_domain.cpp
View file
Open in desktop

Large diffs are not rendered by default.

99 changes: 20 additions & 79 deletions src/crab/ebpf_domain.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@

#include <functional>
#include <optional>
#include <vector>

#include "crab/array_domain.hpp"
#include "crab/split_dbm.hpp"
Expand All @@ -24,7 +23,7 @@ class ebpf_domain_t final {

public:
ebpf_domain_t();
ebpf_domain_t(crab::domains::NumAbsDomain inv, crab::domains::array_domain_t stack);
ebpf_domain_t(domains::NumAbsDomain inv, const domains::array_domain_t& stack);

// Generic abstract domain operations
static ebpf_domain_t top();
Expand All @@ -35,25 +34,25 @@ class ebpf_domain_t final {
bool is_bottom() const;
[[nodiscard]]
bool is_top() const;
bool operator<=(const ebpf_domain_t& other);
bool operator<=(const ebpf_domain_t& other) const;
bool operator==(const ebpf_domain_t& other) const;
void operator|=(ebpf_domain_t&& other);
void operator|=(const ebpf_domain_t& other);
ebpf_domain_t operator|(ebpf_domain_t&& other) const;
ebpf_domain_t operator|(const ebpf_domain_t& other) const&;
ebpf_domain_t operator|(const ebpf_domain_t& other) &&;
ebpf_domain_t operator&(const ebpf_domain_t& other) const;
ebpf_domain_t widen(const ebpf_domain_t& other, bool to_constants);
ebpf_domain_t widening_thresholds(const ebpf_domain_t& other, const crab::iterators::thresholds_t& ts);
ebpf_domain_t narrow(const ebpf_domain_t& other);
ebpf_domain_t widen(const ebpf_domain_t& other, bool to_constants) const;
ebpf_domain_t widening_thresholds(const ebpf_domain_t& other, const thresholds_t& ts);
ebpf_domain_t narrow(const ebpf_domain_t& other) const;

typedef bool check_require_func_t(NumAbsDomain&, const linear_constraint_t&, std::string);
void set_require_check(std::function<check_require_func_t> f);
bound_t get_loop_count_upper_bound();
bound_t 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);
string_invariant to_set();
string_invariant to_set() const;

// abstract transformers
void operator()(const basic_block_t& bb);
Expand Down Expand Up @@ -85,68 +84,16 @@ class ebpf_domain_t final {
void operator()(const ZeroCtxOffset&);
void operator()(const IncrementLoopCounter&);

void initialize_loop_counter(label_t label);
void initialize_loop_counter(const label_t& label);
static ebpf_domain_t calculate_constant_limits();

private:
// private generic domain functions
void operator+=(const linear_constraint_t& cst);
void operator-=(variable_t var);

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(crab::arith_binop_t op, variable_t x, variable_t y, const number_t& z, int finite_width);
void apply(crab::arith_binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);
void apply(crab::bitwise_binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);
void apply(crab::bitwise_binop_t op, variable_t x, variable_t y, const number_t& k, int finite_width);
void apply(crab::binop_t op, variable_t x, variable_t y, const number_t& z, int finite_width);
void apply(crab::binop_t op, variable_t x, variable_t y, variable_t z, int finite_width);

void apply(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t x, variable_t y, variable_t z);
void apply_signed(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, variable_t y,
const number_t& z, int finite_width);
void apply_unsigned(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, variable_t y,
const number_t& z, int finite_width);
void apply_signed(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, variable_t y,
variable_t z, int finite_width);
void apply_unsigned(crab::domains::NumAbsDomain& inv, crab::binop_t op, variable_t xs, variable_t xu, 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& 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);

Expand All @@ -155,7 +102,6 @@ class ebpf_domain_t final {

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

static std::optional<variable_t> get_type_offset_variable(const Reg& reg, int type);
[[nodiscard]]
Expand All @@ -171,22 +117,17 @@ class ebpf_domain_t final {
[[nodiscard]]
std::optional<uint32_t> get_map_inner_map_fd(const Reg& map_fd_reg) const;
[[nodiscard]]
crab::interval_t get_map_key_size(const Reg& map_fd_reg) const;
interval_t get_map_key_size(const Reg& map_fd_reg) const;
[[nodiscard]]
crab::interval_t get_map_value_size(const Reg& map_fd_reg) const;
interval_t get_map_value_size(const Reg& map_fd_reg) const;
[[nodiscard]]
crab::interval_t get_map_max_entries(const Reg& map_fd_reg) const;
interval_t get_map_max_entries(const Reg& map_fd_reg) const;
void forget_packet_pointers();
void havoc_register(NumAbsDomain& inv, const Reg& reg);
void do_load_mapfd(const Reg& dst_reg, int mapfd, bool maybe_null);

static void overflow_signed(NumAbsDomain& inv, variable_t lhs, int finite_width);
static void overflow_unsigned(NumAbsDomain& inv, variable_t lhs, int finite_width);
static void overflow_bounds(NumAbsDomain& inv, variable_t lhs, number_t span, int finite_width, bool issigned);

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

void require(crab::domains::NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s);
void require(domains::NumAbsDomain& inv, const linear_constraint_t& cst, const std::string& s);

// memory check / load / store
void check_access_stack(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub);
Expand All @@ -196,17 +137,17 @@ class ebpf_domain_t final {
void check_access_shared(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub,
variable_t shared_region_size);

void recompute_stack_numeric_size(NumAbsDomain& inv, const Reg& reg);
void recompute_stack_numeric_size(NumAbsDomain& inv, variable_t type_variable);
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);

template <typename X, typename Y, typename Z>
void do_store_stack(crab::domains::NumAbsDomain& inv, const number_t& width, const linear_expression_t& addr,
X val_type, Y val_svalue, Z val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);
void do_store_stack(domains::NumAbsDomain& inv, const number_t& width, const linear_expression_t& addr, X val_type,
Y val_svalue, Z val_uvalue, const std::optional<reg_pack_t>& opt_val_reg);

template <typename Type, typename SValue, typename UValue>
void do_mem_store(const Mem& b, Type val_type, SValue val_svalue, UValue val_uvalue,
Expand All @@ -220,12 +161,12 @@ class ebpf_domain_t final {
/// Mapping from variables (including registers, types, offsets,
/// memory locations, etc.) to numeric intervals or relationships
/// to other variables.
crab::domains::NumAbsDomain m_inv;
domains::NumAbsDomain m_inv;

/// Represents the stack as a memory region, i.e., an array of bytes,
/// allowing mapping to variable in the m_inv numeric domains
/// while dealing with overlapping byte ranges.
crab::domains::array_domain_t stack;
domains::array_domain_t stack;

std::function<check_require_func_t> check_require{};
bool get_map_fd_range(const Reg& map_fd_reg, int32_t* start_fd, int32_t* end_fd) const;
Expand Down Expand Up @@ -266,8 +207,8 @@ class ebpf_domain_t final {
const std::function<void(NumAbsDomain&)>& if_true,
const std::function<void(NumAbsDomain&)>& if_false) const;
void selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain& src) const;
void add_extra_invariant(NumAbsDomain& dst, std::map<crab::variable_t, crab::interval_t>& extra_invariants,
variable_t type_variable, type_encoding_t type, crab::data_kind_t kind,
void add_extra_invariant(const NumAbsDomain& dst, std::map<variable_t, interval_t>& extra_invariants,
variable_t type_variable, type_encoding_t type, data_kind_t kind,
const NumAbsDomain& other) const;

[[nodiscard]]
Expand Down
Loading
Loading