18949625295

Committed 28 Oct 2025 10:33AM UTC coverage: 87.448% (-1.0%) from 88.47%

Build # 18949625295

Build Type

push

github

Committed by

elazarg

Commit Message

Bump CLI11 to v2.6.1

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

9022 of 10317 relevant lines covered (87.45%)

10783407.68 hits per line

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

88.82

/src/crab/rcp.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
#include <ranges>

#include "arith/variable.hpp"
#include "crab/interval.hpp"
#include "crab/rcp.hpp"
#include "crab/type_domain.hpp"
#include "crab/var_registry.hpp"

namespace prevail {

std::optional<Variable> get_type_offset_variable(const Reg& reg, const int type) {
    RegPack r = reg_pack(reg);
    switch (type) {
    case T_CTX: return r.ctx_offset;
    case T_MAP: return r.map_fd;
    case T_MAP_PROGRAMS: return r.map_fd_programs;
    case T_PACKET: return r.packet_offset;
    case T_SHARED: return r.shared_offset;
    case T_STACK: return r.stack_offset;
    default: return {};
    }
}

std::optional<Variable> TypeToNumDomain::get_type_offset_variable(const Reg& reg) const {
    return prevail::get_type_offset_variable(reg, types.get_type(reg));
}

bool TypeToNumDomain::operator<=(const TypeToNumDomain& other) const {
    if (is_bottom()) {
        return true;
    }
    if (other.is_bottom()) {
        return false;
    }
    // First, check the type domain.
    // For example, if r1 in `this` has type {stack} and r1 in `other` has type {stack, packet},
    // then `this` is less than or equal to `other`.
    if (!(types <= other.types)) {
        return false;
    }
    // Then, check the numeric domain with consideration of type-specific variables.
    TypeToNumDomain tmp{other.types, other.values};
    for (const Variable& v : this->get_nonexistent_kind_variables()) {
        tmp.values.havoc(v);
    }
    return values <= tmp.values;
}

void TypeToNumDomain::join_selective(const TypeToNumDomain& right) {
    if (is_bottom()) {
        *this = std::move(right);
        return;
    }
    if (right.is_bottom()) {
        return;
    }
    auto extra_invariants = collect_type_dependent_constraints(right);
    this->values |= std::move(right.values);
    for (const auto& [variable, interval] : extra_invariants) {
        values.set(variable, interval);
    }
}

void TypeToNumDomain::operator|=(const TypeToNumDomain& other) {
    if (is_bottom()) {
        *this = other;
    }
    if (other.is_bottom()) {
        return;
    }
    this->join_selective(other);
    this->types = types | other.types;
}

TypeToNumDomain TypeToNumDomain::operator&(const TypeToNumDomain& other) const {
    if (auto type_inv = types.meet(other.types)) {
        // TODO: remove unuseful variables from the numeric domain
        return TypeToNumDomain{std::move(*type_inv), values & other.values};
    }
    return TypeToNumDomain{TypeDomain::top(), NumAbsDomain::bottom()};
}

std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {
    std::vector<Variable> res;
    for (const Variable v : variable_registry->get_type_variables()) {
        for (const auto& [type, kinds] : type_to_kinds) {
            if (types.may_have_type(v, type)) {
                continue;
            }
            for (const auto kind : kinds) {
                Variable type_offset = variable_registry->kind_var(kind, v);
                res.push_back(type_offset);
            }
        }
    }
    return res;
}

std::vector<std::tuple<Variable, Interval>>
TypeToNumDomain::collect_type_dependent_constraints(const TypeToNumDomain& right) const {
    std::vector<std::tuple<Variable, Interval>> result;

    for (const Variable& type_var : variable_registry->get_type_variables()) {
        for (const auto& [type, kinds] : type_to_kinds) {
            if (kinds.empty()) {
                continue;
            }
            const bool in_left = types.may_have_type(type_var, type);
            const bool in_right = right.types.may_have_type(type_var, type);

            // If a type may be present in one domain but not the other, its
            // dependent constraints must be explicitly preserved.
            if (in_left != in_right) {
                // Identify which domain contains the constraints.
                const NumAbsDomain& source = in_left ? values : right.values;
                for (const DataKind kind : kinds) {
                    Variable var = variable_registry->kind_var(kind, type_var);
                    Interval value = source.eval_interval(var);
                    if (!value.is_top()) {
                        result.emplace_back(var, value);
                    }
                }
            }
        }
    }

    return result;
}

std::vector<TypeEncoding> TypeToNumDomain::enumerate_types(const Reg& reg) const {
    using namespace dsl_syntax;
    if (!types.is_initialized(reg)) {
        return {T_UNINIT};
    }
    return types.iterate_types(reg);
}

TypeToNumDomain
TypeToNumDomain::join_over_types(const Reg& reg,
                                 const std::function<void(TypeToNumDomain&, TypeEncoding)>& transition) const {
    using namespace dsl_syntax;
    if (!types.is_initialized(reg)) {
        TypeToNumDomain res = *this;
        transition(res, T_UNINIT);
        return res;
    }
    TypeToNumDomain res = bottom();
    const std::vector<TypeEncoding> valid_types = types.iterate_types(reg);
    std::map<TypeEncoding, std::vector<DataKind>> valid_type_to_kinds;
    for (const TypeEncoding type : valid_types) {
        valid_type_to_kinds.emplace(type, type_to_kinds.at(type));
    }
    for (const TypeEncoding type : valid_types) {
        TypeToNumDomain tmp(*this);
        tmp.types.add_constraint(reg_type(reg) == type);
        // This might have changed the type variable of reg.
        // It might also have changed the type variable of other registers, but we don't deal with that.
        for (const auto& [other_type, kinds] : valid_type_to_kinds) {
            if (other_type != type) {
                for (const auto kind : kinds) {
                    tmp.values.havoc(variable_registry->kind_var(kind, reg_type(reg)));
                }
            }
        }
        transition(tmp, type);
        res |= tmp;
    }
    return res;
}

void TypeToNumDomain::havoc_all_locations_having_type(const TypeEncoding type) {
    for (const Variable type_variable : variable_registry->get_type_variables()) {
        if (types.may_have_type(type_variable, type)) {
            types.havoc_type(type_variable);
            values.havoc(variable_registry->kind_var(DataKind::svalues, type_variable));
            values.havoc(variable_registry->kind_var(DataKind::uvalues, type_variable));
            for (const DataKind kind : type_to_kinds.at(type)) {
                values.havoc(variable_registry->kind_var(kind, type_variable));
            }
        }
    }
}

void TypeToNumDomain::assume_type(const LinearConstraint& cst) {
    types.add_constraint(cst);
    if (types.inv.is_bottom()) {
        values.set_to_bottom();
    }
}

void TypeToNumDomain::assign(const Reg& lhs, const Reg& rhs) {
    if (lhs == rhs) {
        return;
    }
    types.assign_type(lhs, rhs);

    values.assign(reg_pack(lhs).svalue, reg_pack(rhs).svalue);
    values.assign(reg_pack(lhs).uvalue, reg_pack(rhs).uvalue);

    for (const auto& type : types.iterate_types(lhs)) {
        for (const auto& kind : type_to_kinds.at(type)) {
            values.havoc(variable_registry->kind_var(kind, reg_type(lhs)));
        }
    }
    for (const auto& type : types.iterate_types(rhs)) {
        for (const auto kind : type_to_kinds.at(type)) {
            const auto lhs_var = variable_registry->kind_var(kind, reg_type(lhs));
            values.assign(lhs_var, variable_registry->kind_var(kind, reg_type(rhs)));
        }
    }
}

void TypeToNumDomain::havoc_offsets(const Reg& reg) {
    const RegPack r = reg_pack(reg);
    values.havoc(r.ctx_offset);
    values.havoc(r.map_fd);
    values.havoc(r.map_fd_programs);
    values.havoc(r.packet_offset);
    values.havoc(r.shared_offset);
    values.havoc(r.shared_region_size);
    values.havoc(r.stack_offset);
    values.havoc(r.stack_numeric_size);
}

void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {
    const RegPack r = reg_pack(reg);
    havoc_offsets(reg);
    values.havoc(r.svalue);
    values.havoc(r.uvalue);
}

void TypeToNumDomain::havoc_register(const Reg& reg) {
    types.havoc_type(reg);
    havoc_register_except_type(reg);
}

TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {
    auto extra_invariants = collect_type_dependent_constraints(other);

    TypeToNumDomain res{types.widen(other.types), values.widen(other.values)};

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

TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& rcp) const {
    return TypeToNumDomain{types.narrow(rcp.types), values.narrow(rcp.values)};
}

StringInvariant TypeToNumDomain::to_set() const {
    if (is_bottom()) {
        return StringInvariant::bottom();
    }
    return types.to_set() + values.to_set();
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	#include <ranges>
4
5	#include "arith/variable.hpp"
6	#include "crab/interval.hpp"
7	#include "crab/rcp.hpp"
8	#include "crab/type_domain.hpp"
9	#include "crab/var_registry.hpp"
10
11	namespace prevail {
12
13	std::optional<Variable> get_type_offset_variable(const Reg& reg, const int type) {	17,544✔
14	RegPack r = reg_pack(reg);	17,544✔
15	switch (type) {	17,544✔
16	case T_CTX: return r.ctx_offset;	12✔
17	case T_MAP: return r.map_fd;	12✔
18	case T_MAP_PROGRAMS: return r.map_fd_programs;	×
19	case T_PACKET: return r.packet_offset;	5,528✔
20	case T_SHARED: return r.shared_offset;	146✔
21	case T_STACK: return r.stack_offset;	9,030✔
22	default: return {};	2,816✔
23	}
24	}
25
26	std::optional<Variable> TypeToNumDomain::get_type_offset_variable(const Reg& reg) const {	12,792✔
27	return prevail::get_type_offset_variable(reg, types.get_type(reg));	12,792✔
28	}
29
30	bool TypeToNumDomain::operator<=(const TypeToNumDomain& other) const {	502✔
31	if (is_bottom()) {	502✔
32	return true;	3✔
33	}
34	if (other.is_bottom()) {	496✔
35	return false;	1✔
36	}
37	// First, check the type domain.
38	// For example, if r1 in `this` has type {stack} and r1 in `other` has type {stack, packet},
39	// then `this` is less than or equal to `other`.
40	if (!(types <= other.types)) {	494✔
41	return false;	7✔
42	}
43	// Then, check the numeric domain with consideration of type-specific variables.
44	TypeToNumDomain tmp{other.types, other.values};	480✔
45	for (const Variable& v : this->get_nonexistent_kind_variables()) {	4,550✔
46	tmp.values.havoc(v);	4,070✔
47	}	240✔
48	return values <= tmp.values;	480✔
49	}	480✔
50
51	void TypeToNumDomain::join_selective(const TypeToNumDomain& right) {	286,606✔
52	if (is_bottom()) {	286,606✔
53	*this = std::move(right);	×
54	return;	×
55	}
56	if (right.is_bottom()) {	286,606✔
57	return;
58	}
59	auto extra_invariants = collect_type_dependent_constraints(right);	286,606✔
60	this->values \|= std::move(right.values);	286,606✔
61	for (const auto& [variable, interval] : extra_invariants) {	298,836✔
62	values.set(variable, interval);	12,230✔
63	}
64	}	286,606✔
65
66	void TypeToNumDomain::operator\|=(const TypeToNumDomain& other) {	447,944✔
67	if (is_bottom()) {	447,944✔
68	*this = other;	428,604✔
69	}
70	if (other.is_bottom()) {	447,944✔
71	return;	80,669✔
72	}
73	this->join_selective(other);	286,606✔
74	this->types = types \| other.types;	429,909✔
75	}
76
77	TypeToNumDomain TypeToNumDomain::operator&(const TypeToNumDomain& other) const {	38✔
78	if (auto type_inv = types.meet(other.types)) {	38✔
79	// TODO: remove unuseful variables from the numeric domain
80	return TypeToNumDomain{std::move(*type_inv), values & other.values};	57✔
81	}	38✔
82	return TypeToNumDomain{TypeDomain::top(), NumAbsDomain::bottom()};	×
83	}
84
85	std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {	480✔
86	std::vector<Variable> res;	480✔
87	for (const Variable v : variable_registry->get_type_variables()) {	8,825✔
88	for (const auto& [type, kinds] : type_to_kinds) {	66,760✔
89	if (types.may_have_type(v, type)) {	58,415✔
90	continue;	55,213✔
91	}
92	for (const auto kind : kinds) {	7,272✔
93	Variable type_offset = variable_registry->kind_var(kind, v);	4,070✔
94	res.push_back(type_offset);	4,070✔
95	}
96	}
97	}	240✔
98	return res;	480✔
99	}	×
100
101	std::vector<std::tuple<Variable, Interval>>
102	TypeToNumDomain::collect_type_dependent_constraints(const TypeToNumDomain& right) const {	286,690✔
103	std::vector<std::tuple<Variable, Interval>> result;	286,690✔
104
105	for (const Variable& type_var : variable_registry->get_type_variables()) {	13,663,221✔
106	for (const auto& [type, kinds] : type_to_kinds) {	107,012,248✔
107	if (kinds.empty()) {	93,635,717✔
108	continue;	13,376,531✔
109	}
110	const bool in_left = types.may_have_type(type_var, type);	80,259,186✔
111	const bool in_right = right.types.may_have_type(type_var, type);	80,259,186✔
112
113	// If a type may be present in one domain but not the other, its
114	// dependent constraints must be explicitly preserved.
115	if (in_left != in_right) {	80,259,186✔
116	// Identify which domain contains the constraints.
117	const NumAbsDomain& source = in_left ? values : right.values;	450,544✔
118	for (const DataKind kind : kinds) {	1,051,400✔
119	Variable var = variable_registry->kind_var(kind, type_var);	600,856✔
120	Interval value = source.eval_interval(var);	600,856✔
121	if (!value.is_top()) {	600,856✔
122	result.emplace_back(var, value);	12,230✔
123	}
124	}	600,856✔
125	}
126	}
127	}	143,345✔
128
129	return result;	286,690✔
130	}	×
131
132	std::vector<TypeEncoding> TypeToNumDomain::enumerate_types(const Reg& reg) const {	57,378✔
133	using namespace dsl_syntax;	28,689✔
134	if (!types.is_initialized(reg)) {	57,378✔
135	return {T_UNINIT};	×
136	}
137	return types.iterate_types(reg);	57,378✔
138	}
139
140	TypeToNumDomain
141	TypeToNumDomain::join_over_types(const Reg& reg,	32,668✔
142	const std::function<void(TypeToNumDomain&, TypeEncoding)>& transition) const {
143	using namespace dsl_syntax;	16,334✔
144	if (!types.is_initialized(reg)) {	32,668✔
145	TypeToNumDomain res = *this;	×
146	transition(res, T_UNINIT);	×
147	return res;	×
148	}	×
149	TypeToNumDomain res = bottom();	32,668✔
150	const std::vector<TypeEncoding> valid_types = types.iterate_types(reg);	32,668✔
151	std::map<TypeEncoding, std::vector<DataKind>> valid_type_to_kinds;	32,668✔
152	for (const TypeEncoding type : valid_types) {	65,520✔
153	valid_type_to_kinds.emplace(type, type_to_kinds.at(type));	32,852✔
154	}
155	for (const TypeEncoding type : valid_types) {	65,520✔
156	TypeToNumDomain tmp(*this);	32,852✔
157	tmp.types.add_constraint(reg_type(reg) == type);	49,278✔
158	// This might have changed the type variable of reg.
159	// It might also have changed the type variable of other registers, but we don't deal with that.
160	for (const auto& [other_type, kinds] : valid_type_to_kinds) {	66,072✔
161	if (other_type != type) {	33,220✔
162	for (const auto kind : kinds) {	1,084✔
163	tmp.values.havoc(variable_registry->kind_var(kind, reg_type(reg)));	716✔
164	}
165	}
166	}
167	transition(tmp, type);	32,852✔
168	res \|= tmp;	32,852✔
169	}	32,852✔
170	return res;	32,668✔
171	}	49,002✔
172
173	void TypeToNumDomain::havoc_all_locations_having_type(const TypeEncoding type) {	40✔
174	for (const Variable type_variable : variable_registry->get_type_variables()) {	1,314✔
175	if (types.may_have_type(type_variable, type)) {	1,274✔
176	types.havoc_type(type_variable);	874✔
177	values.havoc(variable_registry->kind_var(DataKind::svalues, type_variable));	874✔
178	values.havoc(variable_registry->kind_var(DataKind::uvalues, type_variable));	874✔
179	for (const DataKind kind : type_to_kinds.at(type)) {	1,748✔
180	values.havoc(variable_registry->kind_var(kind, type_variable));	874✔
181	}
182	}
183	}	40✔
184	}	40✔
185
186	void TypeToNumDomain::assume_type(const LinearConstraint& cst) {	×
187	types.add_constraint(cst);	×
188	if (types.inv.is_bottom()) {	×
189	values.set_to_bottom();	×
190	}
191	}	×
192
193	void TypeToNumDomain::assign(const Reg& lhs, const Reg& rhs) {	26,004✔
194	if (lhs == rhs) {	39,006✔
195	return;
196	}
197	types.assign_type(lhs, rhs);	26,004✔
198
199	values.assign(reg_pack(lhs).svalue, reg_pack(rhs).svalue);	26,004✔
200	values.assign(reg_pack(lhs).uvalue, reg_pack(rhs).uvalue);	26,004✔
201
202	for (const auto& type : types.iterate_types(lhs)) {	52,020✔
203	for (const auto& kind : type_to_kinds.at(type)) {	51,754✔
204	values.havoc(variable_registry->kind_var(kind, reg_type(lhs)));	25,738✔
205	}
206	}	13,002✔
207	for (const auto& type : types.iterate_types(rhs)) {	52,020✔
208	for (const auto kind : type_to_kinds.at(type)) {	51,754✔
209	const auto lhs_var = variable_registry->kind_var(kind, reg_type(lhs));	25,738✔
210	values.assign(lhs_var, variable_registry->kind_var(kind, reg_type(rhs)));	38,607✔
211	}
212	}	26,004✔
213	}
214
215	void TypeToNumDomain::havoc_offsets(const Reg& reg) {	151,528✔
216	const RegPack r = reg_pack(reg);	151,528✔
217	values.havoc(r.ctx_offset);	151,528✔
218	values.havoc(r.map_fd);	151,528✔
219	values.havoc(r.map_fd_programs);	151,528✔
220	values.havoc(r.packet_offset);	151,528✔
221	values.havoc(r.shared_offset);	151,528✔
222	values.havoc(r.shared_region_size);	151,528✔
223	values.havoc(r.stack_offset);	151,528✔
224	values.havoc(r.stack_numeric_size);	151,528✔
225	}	151,528✔
226
227	void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {	91,044✔
228	const RegPack r = reg_pack(reg);	91,044✔
229	havoc_offsets(reg);	91,044✔
230	values.havoc(r.svalue);	91,044✔
231	values.havoc(r.uvalue);	91,044✔
232	}	91,044✔
233
234	void TypeToNumDomain::havoc_register(const Reg& reg) {	70,906✔
235	types.havoc_type(reg);	70,906✔
236	havoc_register_except_type(reg);	70,906✔
237	}	70,906✔
238
239	TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {	84✔
240	auto extra_invariants = collect_type_dependent_constraints(other);	84✔
241
242	TypeToNumDomain res{types.widen(other.types), values.widen(other.values)};	126✔
243
244	// Now add in the extra invariants saved above.
245	for (const auto& [variable, interval] : extra_invariants) {	84✔
246	res.values.set(variable, interval);	×
247	}
248	return res;	126✔
249	}	84✔
250
251	TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& rcp) const {	×
252	return TypeToNumDomain{types.narrow(rcp.types), values.narrow(rcp.values)};	×
253	}
254
255	StringInvariant TypeToNumDomain::to_set() const {	1,384✔
256	if (is_bottom()) {	1,384✔
257	return StringInvariant::bottom();	434✔
258	}
259	return types.to_set() + values.to_set();	1,425✔
260	}
261	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18949625295

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