13958948275

Committed 19 Mar 2025 11:53PM UTC coverage: 88.194% (-0.5%) from 88.66%

Build # 13958948275

Build Type

push

github

Committed by

web-flow

Commit Message

Finite domain (#849)

* Move arithmetic and bit operations functions to finite_domain.cpp
* Remove operator-= (now havoc) and operator+= (now add_constraint)
* Abort early when registers are not usable; clear type variable instead of explicitly assigning T_UNINIT. Update YAML tests accordingly
---------
Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

847 of 898 new or added lines in 11 files covered. (94.32%)

57 existing lines in 8 files now uncovered.

8628 of 9783 relevant lines covered (88.19%)

9034663.84 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

89.13

/src/crab/type_domain.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
// ReSharper disable CppMemberFunctionMayBeStatic

// This file is eBPF-specific, not derived from CRAB.
#include <functional>
#include <map>
#include <optional>

#include "crab/array_domain.hpp"
#include "crab/split_dbm.hpp"
#include "crab/type_domain.hpp"
#include "crab/type_encoding.hpp"
#include "crab/variable.hpp"
#include "crab_utils/debug.hpp"
#include "dsl_syntax.hpp"

namespace crab {

template <is_enum T>
static void operator++(T& t) {
    t = static_cast<T>(1 + static_cast<std::underlying_type_t<T>>(t));
}

std::vector<data_kind_t> iterate_kinds(const data_kind_t lb, const data_kind_t ub) {
    if (lb > ub) {
        CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);
    }
    if (lb < KIND_MIN || ub > KIND_MAX) {
        CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");
    }
    std::vector<data_kind_t> res;
    for (data_kind_t i = lb; i <= ub; ++i) {
        res.push_back(i);
    }
    return res;
}

std::vector<type_encoding_t> iterate_types(const type_encoding_t lb, const type_encoding_t ub) {
    if (lb > ub) {
        CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);
    }
    if (lb < T_MIN || ub > T_MAX) {
        CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");
    }
    std::vector<type_encoding_t> res;
    for (type_encoding_t i = lb; i <= ub; ++i) {
        res.push_back(i);
    }
    return res;
}

static constexpr auto S_UNINIT = "uninit";
static constexpr auto S_STACK = "stack";
static constexpr auto S_PACKET = "packet";
static constexpr auto S_CTX = "ctx";
static constexpr auto S_MAP_PROGRAMS = "map_fd_programs";
static constexpr auto S_MAP = "map_fd";
static constexpr auto S_NUM = "number";
static constexpr auto S_SHARED = "shared";

std::string name_of(const data_kind_t kind) {
    switch (kind) {
    case data_kind_t::ctx_offsets: return "ctx_offset";
    case data_kind_t::map_fds: return "map_fd";
    case data_kind_t::packet_offsets: return "packet_offset";
    case data_kind_t::shared_offsets: return "shared_offset";
    case data_kind_t::shared_region_sizes: return "shared_region_size";
    case data_kind_t::stack_numeric_sizes: return "stack_numeric_size";
    case data_kind_t::stack_offsets: return "stack_offset";
    case data_kind_t::svalues: return "svalue";
    case data_kind_t::types: return "type";
    case data_kind_t::uvalues: return "uvalue";
    }
    return {};
}

data_kind_t regkind(const std::string& s) {
    static const std::map<std::string, data_kind_t> string_to_kind{
        {"type", data_kind_t::types},
        {"ctx_offset", data_kind_t::ctx_offsets},
        {"map_fd", data_kind_t::map_fds},
        {"packet_offset", data_kind_t::packet_offsets},
        {"shared_offset", data_kind_t::shared_offsets},
        {"stack_offset", data_kind_t::stack_offsets},
        {"shared_region_size", data_kind_t::shared_region_sizes},
        {"stack_numeric_size", data_kind_t::stack_numeric_sizes},
        {"svalue", data_kind_t::svalues},
        {"uvalue", data_kind_t::uvalues},
    };
    if (string_to_kind.contains(s)) {
        return string_to_kind.at(s);
    }
    throw std::runtime_error(std::string() + "Bad kind: " + s);
}

std::ostream& operator<<(std::ostream& os, const type_encoding_t s) {
    switch (s) {
    case T_SHARED: return os << S_SHARED;
    case T_STACK: return os << S_STACK;
    case T_PACKET: return os << S_PACKET;
    case T_CTX: return os << S_CTX;
    case T_NUM: return os << S_NUM;
    case T_MAP: return os << S_MAP;
    case T_MAP_PROGRAMS: return os << S_MAP_PROGRAMS;
    case T_UNINIT: return os << S_UNINIT;
    default: CRAB_ERROR("Unsupported type encoding", s);
    }
}

type_encoding_t string_to_type_encoding(const std::string& s) {
    static std::map<std::string, type_encoding_t> string_to_type{
        {S_UNINIT, T_UNINIT}, {S_MAP_PROGRAMS, T_MAP_PROGRAMS},
        {S_MAP, T_MAP},       {S_NUM, T_NUM},
        {S_CTX, T_CTX},       {S_STACK, T_STACK},
        {S_PACKET, T_PACKET}, {S_SHARED, T_SHARED},
    };
    if (string_to_type.contains(s)) {
        return string_to_type[s];
    }
    throw std::runtime_error(std::string("Unsupported type name: ") + s);
}
reg_pack_t reg_pack(const int i) {
    return {
        variable_t::reg(data_kind_t::svalues, i),
        variable_t::reg(data_kind_t::uvalues, i),
        variable_t::reg(data_kind_t::ctx_offsets, i),
        variable_t::reg(data_kind_t::map_fds, i),
        variable_t::reg(data_kind_t::packet_offsets, i),
        variable_t::reg(data_kind_t::shared_offsets, i),
        variable_t::reg(data_kind_t::stack_offsets, i),
        variable_t::reg(data_kind_t::types, i),
        variable_t::reg(data_kind_t::shared_region_sizes, i),
        variable_t::reg(data_kind_t::stack_numeric_sizes, i),
    };
}

void TypeDomain::add_extra_invariant(const NumAbsDomain& dst, std::map<variable_t, interval_t>& extra_invariants,
                                     const variable_t type_variable, const type_encoding_t type, const data_kind_t kind,
                                     const NumAbsDomain& src) const {
    const bool dst_has_type = has_type(dst, type_variable, type);
    const bool src_has_type = has_type(src, type_variable, type);
    variable_t v = variable_t::kind_var(kind, type_variable);

    // If type is contained in exactly one of dst or src,
    // we need to remember the value.
    if (dst_has_type && !src_has_type) {
        extra_invariants.emplace(v, dst.eval_interval(v));
    } else if (!dst_has_type && src_has_type) {
        extra_invariants.emplace(v, src.eval_interval(v));
    }
}

void TypeDomain::selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain&& src) const {
    // Some variables are type-specific.  Type-specific variables
    // for a register can exist in the domain whenever the associated
    // type value is present in the register's types interval (and the
    // value is not Top), and are absent otherwise.  That is, we want
    // to keep track of implications of the form
    // "if register R has type=T then R.T_offset has value ...".
    //
    // If a type value is legal in exactly one of the two domains, a
    // normal join operation would remove any type-specific variables
    // from the resulting merged domain since absence from the other
    // would be interpreted to mean Top.
    //
    // However, when the type value is not present in one domain,
    // any type-specific variables for that type are instead to be
    // interpreted as Bottom, so we want to preserve the values of any
    // type-specific variables from the other domain where the type
    // value is legal.
    //
    // Example input:
    //   r1.type=stack, r1.stack_offset=100
    //   r1.type=packet, r1.packet_offset=4
    // Output:
    //   r1.type={stack,packet}, r1.stack_offset=100, r1.packet_offset=4

    std::map<variable_t, interval_t> extra_invariants;
    if (!dst.is_bottom()) {
        for (const variable_t v : variable_t::get_type_variables()) {
            add_extra_invariant(dst, extra_invariants, v, T_CTX, data_kind_t::ctx_offsets, src);
            add_extra_invariant(dst, extra_invariants, v, T_MAP, data_kind_t::map_fds, src);
            add_extra_invariant(dst, extra_invariants, v, T_MAP_PROGRAMS, data_kind_t::map_fds, src);
            add_extra_invariant(dst, extra_invariants, v, T_PACKET, data_kind_t::packet_offsets, src);
            add_extra_invariant(dst, extra_invariants, v, T_SHARED, data_kind_t::shared_offsets, src);
            add_extra_invariant(dst, extra_invariants, v, T_STACK, data_kind_t::stack_offsets, src);
            add_extra_invariant(dst, extra_invariants, v, T_SHARED, data_kind_t::shared_region_sizes, src);
            add_extra_invariant(dst, extra_invariants, v, T_STACK, data_kind_t::stack_numeric_sizes, src);
        }
    }

    // Do a normal join operation on the domain.
    dst |= std::move(src);

    // Now add in the extra invariants saved above.
    for (const auto& [variable, interval] : extra_invariants) {
        dst.set(variable, interval);
    }
}

void TypeDomain::assign_type(NumAbsDomain& inv, const Reg& lhs, const Reg& rhs) {
    inv.assign(reg_pack(lhs).type, reg_pack(rhs).type);
}

void TypeDomain::assign_type(NumAbsDomain& inv, const std::optional<variable_t> lhs, const linear_expression_t& t) {
    inv.assign(lhs, t);
}

void TypeDomain::assign_type(NumAbsDomain& inv, const Reg& lhs, const std::optional<linear_expression_t>& rhs) {
    inv.assign(reg_pack(lhs).type, rhs);
}

void TypeDomain::havoc_type(NumAbsDomain& inv, const Reg& r) { inv.havoc(reg_pack(r).type); }

type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const linear_expression_t& v) const {
    const auto res = inv.eval_interval(v).singleton();
    if (!res) {
        return T_UNINIT;
    }
    return res->narrow<type_encoding_t>();
}

type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const Reg& r) const {
    const auto res = inv.eval_interval(reg_pack(r).type).singleton();
    if (!res) {
        return T_UNINIT;
    }
    return res->narrow<type_encoding_t>();
}

// Check whether a given type value is within the range of a given type variable's value.
bool TypeDomain::has_type(const NumAbsDomain& inv, const Reg& r, const type_encoding_t type) const {
    const interval_t interval = inv.eval_interval(reg_pack(r).type);
    return interval.contains(type);
}

bool TypeDomain::has_type(const NumAbsDomain& inv, const linear_expression_t& v, const type_encoding_t type) const {
    const interval_t interval = inv.eval_interval(v);
    return interval.contains(type);
}

NumAbsDomain TypeDomain::join_over_types(const NumAbsDomain& inv, const Reg& reg,
                                         const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const {
    interval_t types = inv.eval_interval(reg_pack(reg).type);
    if (types.is_bottom()) {
        return NumAbsDomain::bottom();
    }
    if (types.contains(T_UNINIT)) {
        NumAbsDomain res(inv);
        transition(res, T_UNINIT);
        return res;
    }
    NumAbsDomain res = NumAbsDomain::bottom();
    auto [lb, ub] = types.bound(T_MIN, T_MAX);
    for (type_encoding_t type : iterate_types(lb, ub)) {
        NumAbsDomain tmp(inv);
        transition(tmp, type);
        selectively_join_based_on_type(res, std::move(tmp)); // res |= tmp;
    }
    return res;
}

NumAbsDomain TypeDomain::join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition,
                                         const std::function<void(NumAbsDomain&)>& if_true,
                                         const std::function<void(NumAbsDomain&)>& if_false) const {
    NumAbsDomain true_case(inv.when(condition));
    if_true(true_case);

    NumAbsDomain false_case(inv.when(condition.negate()));
    if_false(false_case);

    return true_case | false_case;
}

static linear_constraint_t eq_types(const Reg& a, const Reg& b) {
    using namespace crab::dsl_syntax;
    return eq(reg_pack(a).type, reg_pack(b).type);
}

bool TypeDomain::same_type(const NumAbsDomain& inv, const Reg& a, const Reg& b) const {
    return inv.entail(eq_types(a, b));
}

bool TypeDomain::implies_type(const NumAbsDomain& inv, const linear_constraint_t& a,
                              const linear_constraint_t& b) const {
    return inv.when(a).entail(b);
}

bool TypeDomain::is_in_group(const NumAbsDomain& inv, const Reg& r, const TypeGroup group) const {
    using namespace crab::dsl_syntax;
    const variable_t t = reg_pack(r).type;
    switch (group) {
    case TypeGroup::number: return inv.entail(t == T_NUM);
    case TypeGroup::map_fd: return inv.entail(t == T_MAP);
    case TypeGroup::map_fd_programs: return inv.entail(t == T_MAP_PROGRAMS);
    case TypeGroup::ctx: return inv.entail(t == T_CTX);
    case TypeGroup::packet: return inv.entail(t == T_PACKET);
    case TypeGroup::stack: return inv.entail(t == T_STACK);
    case TypeGroup::shared: return inv.entail(t == T_SHARED);
    case TypeGroup::mem: return inv.entail(t >= T_PACKET);
    case TypeGroup::mem_or_num: return inv.entail(t >= T_NUM) && inv.entail(t != T_CTX);
    case TypeGroup::pointer: return inv.entail(t >= T_CTX);
    case TypeGroup::ptr_or_num: return inv.entail(t >= T_NUM);
    case TypeGroup::stack_or_packet: return inv.entail(t >= T_PACKET) && inv.entail(t <= T_STACK);
    case TypeGroup::singleton_ptr: return inv.entail(t >= T_CTX) && inv.entail(t <= T_STACK);
    default: CRAB_ERROR("Unsupported type group", group);
    }
}

std::string typeset_to_string(const std::vector<type_encoding_t>& items) {
    std::stringstream ss;
    ss << "{";
    for (auto it = items.begin(); it != items.end(); ++it) {
        ss << *it;
        if (std::next(it) != items.end()) {
            ss << ", ";
        }
    }
    ss << "}";
    return ss.str();
}

bool is_singleton_type(const TypeGroup t) {
    switch (t) {
    case TypeGroup::number:
    case TypeGroup::map_fd:
    case TypeGroup::map_fd_programs:
    case TypeGroup::ctx:
    case TypeGroup::packet:
    case TypeGroup::stack:
    case TypeGroup::shared: return true;
    default: return false;
    }
}

std::ostream& operator<<(std::ostream& os, const TypeGroup ts) {
    using namespace crab;
    static const std::map<TypeGroup, std::string> string_to_type{
        {TypeGroup::number, S_NUM},
        {TypeGroup::map_fd, S_MAP},
        {TypeGroup::map_fd_programs, S_MAP_PROGRAMS},
        {TypeGroup::ctx, S_CTX},
        {TypeGroup::packet, S_PACKET},
        {TypeGroup::stack, S_STACK},
        {TypeGroup::shared, S_SHARED},
        {TypeGroup::mem, typeset_to_string({T_STACK, T_PACKET, T_SHARED})},
        {TypeGroup::pointer, typeset_to_string({T_CTX, T_STACK, T_PACKET, T_SHARED})},
        {TypeGroup::ptr_or_num, typeset_to_string({T_NUM, T_CTX, T_STACK, T_PACKET, T_SHARED})},
        {TypeGroup::stack_or_packet, typeset_to_string({T_STACK, T_PACKET})},
        {TypeGroup::singleton_ptr, typeset_to_string({T_CTX, T_STACK, T_PACKET})},
        {TypeGroup::mem_or_num, typeset_to_string({T_NUM, T_STACK, T_PACKET, T_SHARED})},
    };
    if (string_to_type.contains(ts)) {
        return os << string_to_type.at(ts);
    }
    CRAB_ERROR("Unsupported type group", ts);
}

} // namespace crab

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	// ReSharper disable CppMemberFunctionMayBeStatic
4
5	// This file is eBPF-specific, not derived from CRAB.
6	#include <functional>
7	#include <map>
8	#include <optional>
9
10	#include "crab/array_domain.hpp"
11	#include "crab/split_dbm.hpp"
12	#include "crab/type_domain.hpp"
13	#include "crab/type_encoding.hpp"
14	#include "crab/variable.hpp"
15	#include "crab_utils/debug.hpp"
16	#include "dsl_syntax.hpp"
17
18	namespace crab {
19
20	template <is_enum T>
21	static void operator++(T& t) {	124,696✔
22	t = static_cast<T>(1 + static_cast<std::underlying_type_t<T>>(t));	124,696✔
23	}	124,696✔
24
25	std::vector<data_kind_t> iterate_kinds(const data_kind_t lb, const data_kind_t ub) {	486✔
26	if (lb > ub) {	486✔
27	CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);	×
28	}
29	if (lb < KIND_MIN \|\| ub > KIND_MAX) {	486✔
30	CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");	×
31	}
32	std::vector<data_kind_t> res;	486✔
33	for (data_kind_t i = lb; i <= ub; ++i) {	5,346✔
34	res.push_back(i);	4,860✔
35	}
36	return res;	486✔
37	}	×
38
39	std::vector<type_encoding_t> iterate_types(const type_encoding_t lb, const type_encoding_t ub) {	119,522✔
40	if (lb > ub) {	119,522✔
41	CRAB_ERROR("lower bound ", lb, " is greater than upper bound ", ub);	×
42	}
43	if (lb < T_MIN \|\| ub > T_MAX) {	119,522✔
44	CRAB_ERROR("bounds ", lb, " and ", ub, " are out of range");	×
45	}
46	std::vector<type_encoding_t> res;	119,522✔
47	for (type_encoding_t i = lb; i <= ub; ++i) {	239,358✔
48	res.push_back(i);	119,836✔
49	}
50	return res;	119,522✔
51	}	×
52
53	static constexpr auto S_UNINIT = "uninit";
54	static constexpr auto S_STACK = "stack";
55	static constexpr auto S_PACKET = "packet";
56	static constexpr auto S_CTX = "ctx";
57	static constexpr auto S_MAP_PROGRAMS = "map_fd_programs";
58	static constexpr auto S_MAP = "map_fd";
59	static constexpr auto S_NUM = "number";
60	static constexpr auto S_SHARED = "shared";
61
62	std::string name_of(const data_kind_t kind) {	33,596,768✔
63	switch (kind) {	33,596,768✔
64	case data_kind_t::ctx_offsets: return "ctx_offset";	6,575,634✔
65	case data_kind_t::map_fds: return "map_fd";	9,400,882✔
66	case data_kind_t::packet_offsets: return "packet_offset";	6,563,442✔
67	case data_kind_t::shared_offsets: return "shared_offset";	6,563,578✔
68	case data_kind_t::shared_region_sizes: return "shared_region_size";	6,563,578✔
69	case data_kind_t::stack_numeric_sizes: return "stack_numeric_size";	9,985,612✔
70	case data_kind_t::stack_offsets: return "stack_offset";	9,984,184✔
71	case data_kind_t::svalues: return "svalue";	3,891,986✔
72	case data_kind_t::types: return "type";	3,822,030✔
73	case data_kind_t::uvalues: return "uvalue";	3,842,626✔
74	}
75	return {};	×
76	}
77
78	data_kind_t regkind(const std::string& s) {	4,526✔
79	static const std::map<std::string, data_kind_t> string_to_kind{	2,263✔
80	{"type", data_kind_t::types},	39✔
81	{"ctx_offset", data_kind_t::ctx_offsets},	39✔
82	{"map_fd", data_kind_t::map_fds},	39✔
83	{"packet_offset", data_kind_t::packet_offsets},	39✔
84	{"shared_offset", data_kind_t::shared_offsets},	39✔
85	{"stack_offset", data_kind_t::stack_offsets},	39✔
86	{"shared_region_size", data_kind_t::shared_region_sizes},	39✔
87	{"stack_numeric_size", data_kind_t::stack_numeric_sizes},	39✔
88	{"svalue", data_kind_t::svalues},	39✔
89	{"uvalue", data_kind_t::uvalues},	39✔
90	};	5,423✔
91	if (string_to_kind.contains(s)) {	4,526✔
92	return string_to_kind.at(s);	4,526✔
93	}
94	throw std::runtime_error(std::string() + "Bad kind: " + s);	×
95	}	78✔
96
97	std::ostream& operator<<(std::ostream& os, const type_encoding_t s) {	1,988✔
98	switch (s) {	1,988✔
99	case T_SHARED: return os << S_SHARED;	102✔
100	case T_STACK: return os << S_STACK;	248✔
101	case T_PACKET: return os << S_PACKET;	104✔
102	case T_CTX: return os << S_CTX;	98✔
103	case T_NUM: return os << S_NUM;	1,412✔
104	case T_MAP: return os << S_MAP;	18✔
105	case T_MAP_PROGRAMS: return os << S_MAP_PROGRAMS;	6✔
UNCOV 106	case T_UNINIT: return os << S_UNINIT;	×
107	default: CRAB_ERROR("Unsupported type encoding", s);	×
108	}
109	}
110
111	type_encoding_t string_to_type_encoding(const std::string& s) {	2,520✔
112	static std::map<std::string, type_encoding_t> string_to_type{	1,260✔
113	{S_UNINIT, T_UNINIT}, {S_MAP_PROGRAMS, T_MAP_PROGRAMS},	39✔
114	{S_MAP, T_MAP}, {S_NUM, T_NUM},	78✔
115	{S_CTX, T_CTX}, {S_STACK, T_STACK},	78✔
116	{S_PACKET, T_PACKET}, {S_SHARED, T_SHARED},	78✔
117	};	3,261✔
118	if (string_to_type.contains(s)) {	2,520✔
119	return string_to_type[s];	2,520✔
120	}
121	throw std::runtime_error(std::string("Unsupported type name: ") + s);	×
122	}	78✔
123	reg_pack_t reg_pack(const int i) {	1,860,358✔
124	return {	930,178✔
125	variable_t::reg(data_kind_t::svalues, i),	1,860,358✔
126	variable_t::reg(data_kind_t::uvalues, i),	1,860,358✔
127	variable_t::reg(data_kind_t::ctx_offsets, i),	1,860,358✔
128	variable_t::reg(data_kind_t::map_fds, i),	1,860,358✔
129	variable_t::reg(data_kind_t::packet_offsets, i),	1,860,358✔
130	variable_t::reg(data_kind_t::shared_offsets, i),	1,860,358✔
131	variable_t::reg(data_kind_t::stack_offsets, i),	1,860,358✔
132	variable_t::reg(data_kind_t::types, i),	1,860,358✔
133	variable_t::reg(data_kind_t::shared_region_sizes, i),	1,860,358✔
134	variable_t::reg(data_kind_t::stack_numeric_sizes, i),	1,860,358✔
135	};	1,860,358✔
136	}
137
138	void TypeDomain::add_extra_invariant(const NumAbsDomain& dst, std::map<variable_t, interval_t>& extra_invariants,	11,355,664✔
139	const variable_t type_variable, const type_encoding_t type, const data_kind_t kind,
140	const NumAbsDomain& src) const {
141	const bool dst_has_type = has_type(dst, type_variable, type);	11,355,664✔
142	const bool src_has_type = has_type(src, type_variable, type);	11,355,664✔
143	variable_t v = variable_t::kind_var(kind, type_variable);	11,355,664✔
144
145	// If type is contained in exactly one of dst or src,
146	// we need to remember the value.
147	if (dst_has_type && !src_has_type) {	11,355,664✔
148	extra_invariants.emplace(v, dst.eval_interval(v));	850,710✔
149	} else if (!dst_has_type && src_has_type) {	10,788,524✔
150	extra_invariants.emplace(v, src.eval_interval(v));	108,243✔
151	}
152	}	11,355,664✔
153
154	void TypeDomain::selectively_join_based_on_type(NumAbsDomain& dst, NumAbsDomain&& src) const {	144,016✔
155	// Some variables are type-specific. Type-specific variables
156	// for a register can exist in the domain whenever the associated
157	// type value is present in the register's types interval (and the
158	// value is not Top), and are absent otherwise. That is, we want
159	// to keep track of implications of the form
160	// "if register R has type=T then R.T_offset has value ...".
161	//
162	// If a type value is legal in exactly one of the two domains, a
163	// normal join operation would remove any type-specific variables
164	// from the resulting merged domain since absence from the other
165	// would be interpreted to mean Top.
166	//
167	// However, when the type value is not present in one domain,
168	// any type-specific variables for that type are instead to be
169	// interpreted as Bottom, so we want to preserve the values of any
170	// type-specific variables from the other domain where the type
171	// value is legal.
172	//
173	// Example input:
174	// r1.type=stack, r1.stack_offset=100
175	// r1.type=packet, r1.packet_offset=4
176	// Output:
177	// r1.type={stack,packet}, r1.stack_offset=100, r1.packet_offset=4
178
179	std::map<variable_t, interval_t> extra_invariants;	144,016✔
180	if (!dst.is_bottom()) {	144,016✔
181	for (const variable_t v : variable_t::get_type_variables()) {	1,443,976✔
182	add_extra_invariant(dst, extra_invariants, v, T_CTX, data_kind_t::ctx_offsets, src);	1,419,458✔
183	add_extra_invariant(dst, extra_invariants, v, T_MAP, data_kind_t::map_fds, src);	1,419,458✔
184	add_extra_invariant(dst, extra_invariants, v, T_MAP_PROGRAMS, data_kind_t::map_fds, src);	1,419,458✔
185	add_extra_invariant(dst, extra_invariants, v, T_PACKET, data_kind_t::packet_offsets, src);	1,419,458✔
186	add_extra_invariant(dst, extra_invariants, v, T_SHARED, data_kind_t::shared_offsets, src);	1,419,458✔
187	add_extra_invariant(dst, extra_invariants, v, T_STACK, data_kind_t::stack_offsets, src);	1,419,458✔
188	add_extra_invariant(dst, extra_invariants, v, T_SHARED, data_kind_t::shared_region_sizes, src);	1,419,458✔
189	add_extra_invariant(dst, extra_invariants, v, T_STACK, data_kind_t::stack_numeric_sizes, src);	1,419,458✔
190	}	24,518✔
191	}
192
193	// Do a normal join operation on the domain.
194	dst \|= std::move(src);	144,016✔
195
196	// Now add in the extra invariants saved above.
197	for (const auto& [variable, interval] : extra_invariants) {	709,190✔
198	dst.set(variable, interval);	565,174✔
199	}
200	}	144,016✔
201
202	void TypeDomain::assign_type(NumAbsDomain& inv, const Reg& lhs, const Reg& rhs) {	36,520✔
203	inv.assign(reg_pack(lhs).type, reg_pack(rhs).type);	36,520✔
204	}	36,520✔
205
206	void TypeDomain::assign_type(NumAbsDomain& inv, const std::optional<variable_t> lhs, const linear_expression_t& t) {	31,670✔
207	inv.assign(lhs, t);	31,670✔
208	}	31,670✔
209
210	void TypeDomain::assign_type(NumAbsDomain& inv, const Reg& lhs, const std::optional<linear_expression_t>& rhs) {	108,509✔
211	inv.assign(reg_pack(lhs).type, rhs);	108,509✔
212	}	108,509✔
213
214	void TypeDomain::havoc_type(NumAbsDomain& inv, const Reg& r) { inv.havoc(reg_pack(r).type); }	103,014✔
215
216	type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const linear_expression_t& v) const {	44,770✔
217	const auto res = inv.eval_interval(v).singleton();	44,770✔
218	if (!res) {	44,770✔
219	return T_UNINIT;	145✔
220	}
221	return res->narrow<type_encoding_t>();	44,480✔
222	}	44,770✔
223
224	type_encoding_t TypeDomain::get_type(const NumAbsDomain& inv, const Reg& r) const {	8✔
225	const auto res = inv.eval_interval(reg_pack(r).type).singleton();	12✔
226	if (!res) {	8✔
227	return T_UNINIT;	2✔
228	}
229	return res->narrow<type_encoding_t>();	4✔
230	}	8✔
231
232	// Check whether a given type value is within the range of a given type variable's value.
233	bool TypeDomain::has_type(const NumAbsDomain& inv, const Reg& r, const type_encoding_t type) const {	239,490✔
234	const interval_t interval = inv.eval_interval(reg_pack(r).type);	239,490✔
235	return interval.contains(type);	359,235✔
236	}	239,490✔
237
238	bool TypeDomain::has_type(const NumAbsDomain& inv, const linear_expression_t& v, const type_encoding_t type) const {	25,512,367✔
239	const interval_t interval = inv.eval_interval(v);	25,512,367✔
240	return interval.contains(type);	38,268,550✔
241	}	25,512,367✔
242
243	NumAbsDomain TypeDomain::join_over_types(const NumAbsDomain& inv, const Reg& reg,	120,610✔
244	const std::function<void(NumAbsDomain&, type_encoding_t)>& transition) const {
245	interval_t types = inv.eval_interval(reg_pack(reg).type);	120,610✔
246	if (types.is_bottom()) {	120,610✔
247	return NumAbsDomain::bottom();	×
248	}
249	if (types.contains(T_UNINIT)) {	120,610✔
250	NumAbsDomain res(inv);	1,114✔
251	transition(res, T_UNINIT);	1,114✔
252	return res;	1,114✔
253	}	1,114✔
254	NumAbsDomain res = NumAbsDomain::bottom();	119,496✔
255	auto [lb, ub] = types.bound(T_MIN, T_MAX);	119,496✔
256	for (type_encoding_t type : iterate_types(lb, ub)) {	239,280✔
257	NumAbsDomain tmp(inv);	119,784✔
258	transition(tmp, type);	119,784✔
259	selectively_join_based_on_type(res, std::move(tmp)); // res \|= tmp;	119,784✔
260	}	239,280✔
261	return res;	119,496✔
262	}	180,358✔
263
264	NumAbsDomain TypeDomain::join_by_if_else(const NumAbsDomain& inv, const linear_constraint_t& condition,	×
265	const std::function<void(NumAbsDomain&)>& if_true,
266	const std::function<void(NumAbsDomain&)>& if_false) const {
267	NumAbsDomain true_case(inv.when(condition));	×
268	if_true(true_case);	×
269
270	NumAbsDomain false_case(inv.when(condition.negate()));	×
271	if_false(false_case);	×
272
273	return true_case \| false_case;	×
274	}	×
275
276	static linear_constraint_t eq_types(const Reg& a, const Reg& b) {	18,852✔
277	using namespace crab::dsl_syntax;	9,426✔
278	return eq(reg_pack(a).type, reg_pack(b).type);	18,852✔
279	}
280
281	bool TypeDomain::same_type(const NumAbsDomain& inv, const Reg& a, const Reg& b) const {	18,852✔
282	return inv.entail(eq_types(a, b));	28,278✔
283	}
284
285	bool TypeDomain::implies_type(const NumAbsDomain& inv, const linear_constraint_t& a,	2,768✔
286	const linear_constraint_t& b) const {
287	return inv.when(a).entail(b);	4,152✔
288	}
289
290	bool TypeDomain::is_in_group(const NumAbsDomain& inv, const Reg& r, const TypeGroup group) const {	93,466✔
291	using namespace crab::dsl_syntax;	46,733✔
292	const variable_t t = reg_pack(r).type;	93,466✔
293	switch (group) {	93,466✔
294	case TypeGroup::number: return inv.entail(t == T_NUM);	70,827✔
295	case TypeGroup::map_fd: return inv.entail(t == T_MAP);	4,482✔
296	case TypeGroup::map_fd_programs: return inv.entail(t == T_MAP_PROGRAMS);	414✔
297	case TypeGroup::ctx: return inv.entail(t == T_CTX);	7,854✔
298	case TypeGroup::packet: return inv.entail(t == T_PACKET);	×
299	case TypeGroup::stack: return inv.entail(t == T_STACK);	×
300	case TypeGroup::shared: return inv.entail(t == T_SHARED);	×
301	case TypeGroup::mem: return inv.entail(t >= T_PACKET);	11,252✔
302	case TypeGroup::mem_or_num: return inv.entail(t >= T_NUM) && inv.entail(t != T_CTX);	2,380✔
303	case TypeGroup::pointer: return inv.entail(t >= T_CTX);	28,660✔
304	case TypeGroup::ptr_or_num: return inv.entail(t >= T_NUM);	26,252✔
305	case TypeGroup::stack_or_packet: return inv.entail(t >= T_PACKET) && inv.entail(t <= T_STACK);	×
306	case TypeGroup::singleton_ptr: return inv.entail(t >= T_CTX) && inv.entail(t <= T_STACK);	6,114✔
307	default: CRAB_ERROR("Unsupported type group", group);	×
308	}
309	}
310
311	std::string typeset_to_string(const std::vector<type_encoding_t>& items) {	50✔
312	std::stringstream ss;	50✔
313	ss << "{";	50✔
314	for (auto it = items.begin(); it != items.end(); ++it) {	186✔
315	ss << *it;	136✔
316	if (std::next(it) != items.end()) {	204✔
317	ss << ", ";	86✔
318	}
319	}
320	ss << "}";	50✔
321	return ss.str();	100✔
322	}	50✔
323
324	bool is_singleton_type(const TypeGroup t) {	2,156✔
325	switch (t) {	2,156✔
326	case TypeGroup::number:	1,052✔
327	case TypeGroup::map_fd:
328	case TypeGroup::map_fd_programs:
329	case TypeGroup::ctx:
330	case TypeGroup::packet:
331	case TypeGroup::stack:
332	case TypeGroup::shared: return true;	1,052✔
333	default: return false;	52✔
334	}
335	}
336
337	std::ostream& operator<<(std::ostream& os, const TypeGroup ts) {	4,352✔
338	using namespace crab;	2,176✔
339	static const std::map<TypeGroup, std::string> string_to_type{	2,176✔
340	{TypeGroup::number, S_NUM},	2✔
341	{TypeGroup::map_fd, S_MAP},	2✔
342	{TypeGroup::map_fd_programs, S_MAP_PROGRAMS},	2✔
343	{TypeGroup::ctx, S_CTX},	2✔
344	{TypeGroup::packet, S_PACKET},	2✔
345	{TypeGroup::stack, S_STACK},	2✔
346	{TypeGroup::shared, S_SHARED},	2✔
347	{TypeGroup::mem, typeset_to_string({T_STACK, T_PACKET, T_SHARED})},	8✔
348	{TypeGroup::pointer, typeset_to_string({T_CTX, T_STACK, T_PACKET, T_SHARED})},	8✔
349	{TypeGroup::ptr_or_num, typeset_to_string({T_NUM, T_CTX, T_STACK, T_PACKET, T_SHARED})},	8✔
350	{TypeGroup::stack_or_packet, typeset_to_string({T_STACK, T_PACKET})},	8✔
351	{TypeGroup::singleton_ptr, typeset_to_string({T_CTX, T_STACK, T_PACKET})},	8✔
352	{TypeGroup::mem_or_num, typeset_to_string({T_NUM, T_STACK, T_PACKET, T_SHARED})},	8✔
353	};	4,414✔
354	if (string_to_type.contains(ts)) {	4,352✔
355	return os << string_to_type.at(ts);	4,352✔
356	}
357	CRAB_ERROR("Unsupported type group", ts);	×
358	}	28✔
359
360	} // namespace crab

vbpf / ebpf-verifier / 13958948275

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous