22160684311

Committed 18 Feb 2026 09:20PM UTC coverage: 88.256% (+1.1%) from 87.142%

Build # 22160684311

Build Type

push

github

Committed by

elazarg

Commit Message

lint

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

Coverage Stats

78 of 82 new or added lines in 6 files covered. (95.12%)

402 existing lines in 18 files now uncovered.

10731 of 12159 relevant lines covered (88.26%)

837642.51 hits per line

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

91.18

/src/crab/var_registry.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
/*
 * Factories for variable names.
 */

#include "crab/var_registry.hpp"
#include "arith/variable.hpp"
#include "cfg/label.hpp"
#include "crab_utils/lazy_allocator.hpp"

namespace prevail {

Variable VariableRegistry::make(const std::string& name) {
    const auto it = std::ranges::find(names, name);
    if (it == names.end()) {
        names.emplace_back(name);
        return Variable(names.size() - 1);
    }
    return Variable(std::distance(names.begin(), it));
}

static std::vector<std::string> default_variable_names() {
    return std::vector<std::string>{
        "r0.svalue",
        "r0.uvalue",
        "r0.ctx_offset",
        "r0.map_fd",
        "r0.packet_offset",
        "r0.shared_offset",
        "r0.stack_offset",
        "r0.type",
        "r0.shared_region_size",
        "r0.stack_numeric_size",
        "r1.svalue",
        "r1.uvalue",
        "r1.ctx_offset",
        "r1.map_fd",
        "r1.packet_offset",
        "r1.shared_offset",
        "r1.stack_offset",
        "r1.type",
        "r1.shared_region_size",
        "r1.stack_numeric_size",
        "r2.svalue",
        "r2.uvalue",
        "r2.ctx_offset",
        "r2.map_fd",
        "r2.packet_offset",
        "r2.shared_offset",
        "r2.stack_offset",
        "r2.type",
        "r2.shared_region_size",
        "r2.stack_numeric_size",
        "r3.svalue",
        "r3.uvalue",
        "r3.ctx_offset",
        "r3.map_fd",
        "r3.packet_offset",
        "r3.shared_offset",
        "r3.stack_offset",
        "r3.type",
        "r3.shared_region_size",
        "r3.stack_numeric_size",
        "r4.svalue",
        "r4.uvalue",
        "r4.ctx_offset",
        "r4.map_fd",
        "r4.packet_offset",
        "r4.shared_offset",
        "r4.stack_offset",
        "r4.type",
        "r4.shared_region_size",
        "r4.stack_numeric_size",
        "r5.svalue",
        "r5.uvalue",
        "r5.ctx_offset",
        "r5.map_fd",
        "r5.packet_offset",
        "r5.shared_offset",
        "r5.stack_offset",
        "r5.type",
        "r5.shared_region_size",
        "r5.stack_numeric_size",
        "r6.svalue",
        "r6.uvalue",
        "r6.ctx_offset",
        "r6.map_fd",
        "r6.packet_offset",
        "r6.shared_offset",
        "r6.stack_offset",
        "r6.type",
        "r6.shared_region_size",
        "r6.stack_numeric_size",
        "r7.svalue",
        "r7.uvalue",
        "r7.ctx_offset",
        "r7.map_fd",
        "r7.packet_offset",
        "r7.shared_offset",
        "r7.stack_offset",
        "r7.type",
        "r7.shared_region_size",
        "r7.stack_numeric_size",
        "r8.svalue",
        "r8.uvalue",
        "r8.ctx_offset",
        "r8.map_fd",
        "r8.packet_offset",
        "r8.shared_offset",
        "r8.stack_offset",
        "r8.type",
        "r8.shared_region_size",
        "r8.stack_numeric_size",
        "r9.svalue",
        "r9.uvalue",
        "r9.ctx_offset",
        "r9.map_fd",
        "r9.packet_offset",
        "r9.shared_offset",
        "r9.stack_offset",
        "r9.type",
        "r9.shared_region_size",
        "r9.stack_numeric_size",
        "r10.svalue",
        "r10.uvalue",
        "r10.ctx_offset",
        "r10.map_fd",
        "r10.packet_offset",
        "r10.shared_offset",
        "r10.stack_offset",
        "r10.type",
        "r10.shared_region_size",
        "r10.stack_numeric_size",
        "data_size",
        "meta_size",
        "meta_offset",
        "packet_size",
    };
}

VariableRegistry::VariableRegistry() : names(default_variable_names()) {}

thread_local LazyAllocator<VariableRegistry> variable_registry;

std::ostream& operator<<(std::ostream& o, const Variable& v) { return o << variable_registry->name(v); }

std::ostream& operator<<(std::ostream& o, const DataKind& s) { return o << name_of(s); }

Variable VariableRegistry::reg(const DataKind kind, const int i) {
    return make("r" + std::to_string(i) + "." + name_of(kind));
}

Variable VariableRegistry::type_reg(const int i) {
    return make("r" + std::to_string(i) + "." + name_of(DataKind::types));
}

Variable VariableRegistry::stack_frame_var(const DataKind kind, const int i, const std::string& prefix) {
    return make(prefix + STACK_FRAME_DELIMITER + "r" + std::to_string(i) + "." + name_of(kind));
}

static std::string mk_scalar_name(const DataKind kind, const Number& o, const Number& size) {
    std::stringstream os;
    os << "s" << "[" << o;
    if (size != 1) {
        os << "..." << o + size - 1;
    }
    os << "]." << name_of(kind);
    return os.str();
}

Variable VariableRegistry::cell_var(const DataKind array, const Number& offset, const Number& size) {
    return make(mk_scalar_name(array, offset.cast_to<uint64_t>(), size));
}

// Given a type variable, get the associated variable of a given kind.
Variable VariableRegistry::kind_var(const DataKind kind, const Variable type_variable) {
    const std::string name = VariableRegistry::name(type_variable);
    const auto dot_pos = name.rfind('.');
    if (dot_pos == std::string::npos) {
        CRAB_ERROR("Variable name '", name, "' does not contain a dot");
    }
    return make(name.substr(0, dot_pos + 1) + name_of(kind));
}

Variable VariableRegistry::meta_offset() { return make("meta_offset"); }
Variable VariableRegistry::packet_size() { return make("packet_size"); }

bool VariableRegistry::is_min_only(const Variable& v) const {
    const auto& n = name(v);
    return n.ends_with(".stack_numeric_size") || n.ends_with(".shared_region_size") || n == "packet_size";
}

Variable VariableRegistry::loop_counter(const std::string& label) { return make("pc[" + label + "]"); }

static bool ends_with(const std::string& str, const std::string& suffix) {
    return str.size() >= suffix.size() && 0 == str.compare(str.size() - suffix.size(), suffix.size(), suffix);
}

std::vector<Variable> VariableRegistry::get_type_variables() {
    std::vector<Variable> res;
    for (const std::string& name : names) {
        if (ends_with(name, ".type")) {
            res.push_back(make(name));
        }
    }
    return res;
}

std::string VariableRegistry::name(const Variable& v) const { return names.at(v._id); }

[[nodiscard]]
bool VariableRegistry::is_type(const Variable& v) const {
    return name(v).ends_with(".type");
}

[[nodiscard]]
bool VariableRegistry::is_unsigned(const Variable& v) const {
    return name(v).ends_with(".uvalue");
}

bool VariableRegistry::is_in_stack(const Variable& v) const { return name(v)[0] == 's'; }

bool VariableRegistry::printing_order(const Variable& a, const Variable& b) {
    return variable_registry->name(a) < variable_registry->name(b);
}

std::vector<Variable> VariableRegistry::get_loop_counters() {
    std::vector<Variable> res;
    for (const std::string& name : names) {
        if (name.starts_with("pc")) {
            res.push_back(make(name));
        }
    }
    return res;
}
} // end namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	/*
4	* Factories for variable names.
5	*/
6
7	#include "crab/var_registry.hpp"
8	#include "arith/variable.hpp"
9	#include "cfg/label.hpp"
10	#include "crab_utils/lazy_allocator.hpp"
11
12	namespace prevail {
13
14	Variable VariableRegistry::make(const std::string& name) {	13,664,573✔
15	const auto it = std::ranges::find(names, name);	13,664,573✔
16	if (it == names.end()) {	13,664,573✔
17	names.emplace_back(name);	112,287✔
18	return Variable(names.size() - 1);	112,287✔
19	}
20	return Variable(std::distance(names.begin(), it));	20,333,342✔
21	}
22
23	static std::vector<std::string> default_variable_names() {	2,802✔
24	return std::vector<std::string>{	1,401✔
25	"r0.svalue",
26	"r0.uvalue",
27	"r0.ctx_offset",
28	"r0.map_fd",
29	"r0.packet_offset",
30	"r0.shared_offset",
31	"r0.stack_offset",
32	"r0.type",
33	"r0.shared_region_size",
34	"r0.stack_numeric_size",
35	"r1.svalue",
36	"r1.uvalue",
37	"r1.ctx_offset",
38	"r1.map_fd",
39	"r1.packet_offset",
40	"r1.shared_offset",
41	"r1.stack_offset",
42	"r1.type",
43	"r1.shared_region_size",
44	"r1.stack_numeric_size",
45	"r2.svalue",
46	"r2.uvalue",
47	"r2.ctx_offset",
48	"r2.map_fd",
49	"r2.packet_offset",
50	"r2.shared_offset",
51	"r2.stack_offset",
52	"r2.type",
53	"r2.shared_region_size",
54	"r2.stack_numeric_size",
55	"r3.svalue",
56	"r3.uvalue",
57	"r3.ctx_offset",
58	"r3.map_fd",
59	"r3.packet_offset",
60	"r3.shared_offset",
61	"r3.stack_offset",
62	"r3.type",
63	"r3.shared_region_size",
64	"r3.stack_numeric_size",
65	"r4.svalue",
66	"r4.uvalue",
67	"r4.ctx_offset",
68	"r4.map_fd",
69	"r4.packet_offset",
70	"r4.shared_offset",
71	"r4.stack_offset",
72	"r4.type",
73	"r4.shared_region_size",
74	"r4.stack_numeric_size",
75	"r5.svalue",
76	"r5.uvalue",
77	"r5.ctx_offset",
78	"r5.map_fd",
79	"r5.packet_offset",
80	"r5.shared_offset",
81	"r5.stack_offset",
82	"r5.type",
83	"r5.shared_region_size",
84	"r5.stack_numeric_size",
85	"r6.svalue",
86	"r6.uvalue",
87	"r6.ctx_offset",
88	"r6.map_fd",
89	"r6.packet_offset",
90	"r6.shared_offset",
91	"r6.stack_offset",
92	"r6.type",
93	"r6.shared_region_size",
94	"r6.stack_numeric_size",
95	"r7.svalue",
96	"r7.uvalue",
97	"r7.ctx_offset",
98	"r7.map_fd",
99	"r7.packet_offset",
100	"r7.shared_offset",
101	"r7.stack_offset",
102	"r7.type",
103	"r7.shared_region_size",
104	"r7.stack_numeric_size",
105	"r8.svalue",
106	"r8.uvalue",
107	"r8.ctx_offset",
108	"r8.map_fd",
109	"r8.packet_offset",
110	"r8.shared_offset",
111	"r8.stack_offset",
112	"r8.type",
113	"r8.shared_region_size",
114	"r8.stack_numeric_size",
115	"r9.svalue",
116	"r9.uvalue",
117	"r9.ctx_offset",
118	"r9.map_fd",
119	"r9.packet_offset",
120	"r9.shared_offset",
121	"r9.stack_offset",
122	"r9.type",
123	"r9.shared_region_size",
124	"r9.stack_numeric_size",
125	"r10.svalue",
126	"r10.uvalue",
127	"r10.ctx_offset",
128	"r10.map_fd",
129	"r10.packet_offset",
130	"r10.shared_offset",
131	"r10.stack_offset",
132	"r10.type",
133	"r10.shared_region_size",
134	"r10.stack_numeric_size",
135	"data_size",
136	"meta_size",
137	"meta_offset",
138	"packet_size",
139	};	326,433✔
140	}	7,005✔
141
142	VariableRegistry::VariableRegistry() : names(default_variable_names()) {}	2,802✔
143
144	thread_local LazyAllocator<VariableRegistry> variable_registry;	4,337✔
145
146	std::ostream& operator<<(std::ostream& o, const Variable& v) { return o << variable_registry->name(v); }	5,601✔
147
148	std::ostream& operator<<(std::ostream& o, const DataKind& s) { return o << name_of(s); }	×
149
150	Variable VariableRegistry::reg(const DataKind kind, const int i) {	8,231,244✔
151	return make("r" + std::to_string(i) + "." + name_of(kind));	16,462,488✔
152	}
153
154	Variable VariableRegistry::type_reg(const int i) {	996,040✔
155	return make("r" + std::to_string(i) + "." + name_of(DataKind::types));	1,982,992✔
156	}
157
158	Variable VariableRegistry::stack_frame_var(const DataKind kind, const int i, const std::string& prefix) {	406✔
159	return make(prefix + STACK_FRAME_DELIMITER + "r" + std::to_string(i) + "." + name_of(kind));	1,015✔
160	}
161
162	static std::string mk_scalar_name(const DataKind kind, const Number& o, const Number& size) {	167,754✔
163	std::stringstream os;	167,754✔
164	os << "s" << "[" << o;	167,754✔
165	if (size != 1) {	167,754✔
166	os << "..." << o + size - 1;	142,796✔
167	}
168	os << "]." << name_of(kind);	251,631✔
169	return os.str();	335,508✔
170	}	167,754✔
171
172	Variable VariableRegistry::cell_var(const DataKind array, const Number& offset, const Number& size) {	167,754✔
173	return make(mk_scalar_name(array, offset.cast_to<uint64_t>(), size));	251,631✔
174	}
175
176	// Given a type variable, get the associated variable of a given kind.
177	Variable VariableRegistry::kind_var(const DataKind kind, const Variable type_variable) {	748,634✔
178	const std::string name = VariableRegistry::name(type_variable);	748,634✔
179	const auto dot_pos = name.rfind('.');	748,634✔
180	if (dot_pos == std::string::npos) {	748,634✔
181	CRAB_ERROR("Variable name '", name, "' does not contain a dot");	×
182	}
183	return make(name.substr(0, dot_pos + 1) + name_of(kind));	1,497,268✔
184	}	374,317✔
185
186	Variable VariableRegistry::meta_offset() { return make("meta_offset"); }	29,920✔
187	Variable VariableRegistry::packet_size() { return make("packet_size"); }	25,070✔
188
189	bool VariableRegistry::is_min_only(const Variable& v) const {	2,243,542✔
190	const auto& n = name(v);	2,243,542✔
191	return n.ends_with(".stack_numeric_size") \|\| n.ends_with(".shared_region_size") \|\| n == "packet_size";	3,494,137✔
192	}	2,243,542✔
193
194	Variable VariableRegistry::loop_counter(const std::string& label) { return make("pc[" + label + "]"); }	616✔
195
196	static bool ends_with(const std::string& str, const std::string& suffix) {	28,416,798✔
197	return str.size() >= suffix.size() && 0 == str.compare(str.size() - suffix.size(), suffix.size(), suffix);	28,416,798✔
198	}
199
200	std::vector<Variable> VariableRegistry::get_type_variables() {	74,928✔
201	std::vector<Variable> res;	74,928✔
202	for (const std::string& name : names) {	28,491,726✔
203	if (ends_with(name, ".type")) {	42,628,457✔
204	res.push_back(make(name));	5,245,983✔
205	}
206	}
207	return res;	74,928✔
208	}	×
209
210	std::string VariableRegistry::name(const Variable& v) const { return names.at(v._id); }	3,019,720✔
211
212	[[nodiscard]]
UNCOV 213	bool VariableRegistry::is_type(const Variable& v) const {	×
UNCOV 214	return name(v).ends_with(".type");	×
215	}
216
217	[[nodiscard]]
218	bool VariableRegistry::is_unsigned(const Variable& v) const {	1,064✔
219	return name(v).ends_with(".uvalue");	1,064✔
220	}
221
222	bool VariableRegistry::is_in_stack(const Variable& v) const { return name(v)[0] == 's'; }	1,346✔
223
224	bool VariableRegistry::printing_order(const Variable& a, const Variable& b) {	2,470✔
225	return variable_registry->name(a) < variable_registry->name(b);	2,470✔
226	}
227
228	std::vector<Variable> VariableRegistry::get_loop_counters() {	638✔
229	std::vector<Variable> res;	638✔
230	for (const std::string& name : names) {	78,484✔
231	if (name.starts_with("pc")) {	77,846✔
232	res.push_back(make(name));	933✔
233	}
234	}
235	return res;	638✔
236	}	×
237	} // end namespace prevail

Alan-Jowett / ebpf-verifier / 22160684311

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