15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

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

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

82.0

/src/crab/var_factory.cpp

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

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

namespace prevail {

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

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",
    };
}

thread_local LazyAllocator<std::vector<std::string>, default_variable_names> Variable::names;

void Variable::clear_thread_local_state() { names.clear(); }

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

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

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 Variable::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));
}

Variable Variable::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 Variable::kind_var(const DataKind kind, const Variable type_variable) {
    const std::string name = type_variable.name();
    return make(name.substr(0, name.rfind('.') + 1) + name_of(kind));
}

Variable Variable::meta_offset() { return make("meta_offset"); }
Variable Variable::packet_size() { return make("packet_size"); }
Variable Variable::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> Variable::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;
}

bool Variable::is_in_stack() const { return this->name()[0] == 's'; }

bool Variable::printing_order(const Variable& a, const Variable& b) { return a.name() < b.name(); }

std::vector<Variable> Variable::get_loop_counters() {
    std::vector<Variable> res;
    for (const std::string& name : *names) {
        if (name.find("pc") == 0) {
            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 "cfg/label.hpp"
8	#include "crab/variable.hpp"
9	#include "crab_utils/lazy_allocator.hpp"
10
11	namespace prevail {
12
13	Variable Variable::make(const std::string& name) {	36,840,824✔
14	const auto it = std::find(names->begin(), names->end(), name);	36,840,824✔
15	if (it == names->end()) {	36,840,824✔
16	names->emplace_back(name);	109,258✔
17	return Variable(names->size() - 1);	109,258✔
18	}
19	return Variable(std::distance(names->begin(), it));	55,097,357✔
20	}
21
22	std::vector<std::string> default_variable_names() {	2,942✔
23	return std::vector<std::string>{	1,471✔
24	"r0.svalue",
25	"r0.uvalue",
26	"r0.ctx_offset",
27	"r0.map_fd",
28	"r0.packet_offset",
29	"r0.shared_offset",
30	"r0.stack_offset",
31	"r0.type",
32	"r0.shared_region_size",
33	"r0.stack_numeric_size",
34	"r1.svalue",
35	"r1.uvalue",
36	"r1.ctx_offset",
37	"r1.map_fd",
38	"r1.packet_offset",
39	"r1.shared_offset",
40	"r1.stack_offset",
41	"r1.type",
42	"r1.shared_region_size",
43	"r1.stack_numeric_size",
44	"r2.svalue",
45	"r2.uvalue",
46	"r2.ctx_offset",
47	"r2.map_fd",
48	"r2.packet_offset",
49	"r2.shared_offset",
50	"r2.stack_offset",
51	"r2.type",
52	"r2.shared_region_size",
53	"r2.stack_numeric_size",
54	"r3.svalue",
55	"r3.uvalue",
56	"r3.ctx_offset",
57	"r3.map_fd",
58	"r3.packet_offset",
59	"r3.shared_offset",
60	"r3.stack_offset",
61	"r3.type",
62	"r3.shared_region_size",
63	"r3.stack_numeric_size",
64	"r4.svalue",
65	"r4.uvalue",
66	"r4.ctx_offset",
67	"r4.map_fd",
68	"r4.packet_offset",
69	"r4.shared_offset",
70	"r4.stack_offset",
71	"r4.type",
72	"r4.shared_region_size",
73	"r4.stack_numeric_size",
74	"r5.svalue",
75	"r5.uvalue",
76	"r5.ctx_offset",
77	"r5.map_fd",
78	"r5.packet_offset",
79	"r5.shared_offset",
80	"r5.stack_offset",
81	"r5.type",
82	"r5.shared_region_size",
83	"r5.stack_numeric_size",
84	"r6.svalue",
85	"r6.uvalue",
86	"r6.ctx_offset",
87	"r6.map_fd",
88	"r6.packet_offset",
89	"r6.shared_offset",
90	"r6.stack_offset",
91	"r6.type",
92	"r6.shared_region_size",
93	"r6.stack_numeric_size",
94	"r7.svalue",
95	"r7.uvalue",
96	"r7.ctx_offset",
97	"r7.map_fd",
98	"r7.packet_offset",
99	"r7.shared_offset",
100	"r7.stack_offset",
101	"r7.type",
102	"r7.shared_region_size",
103	"r7.stack_numeric_size",
104	"r8.svalue",
105	"r8.uvalue",
106	"r8.ctx_offset",
107	"r8.map_fd",
108	"r8.packet_offset",
109	"r8.shared_offset",
110	"r8.stack_offset",
111	"r8.type",
112	"r8.shared_region_size",
113	"r8.stack_numeric_size",
114	"r9.svalue",
115	"r9.uvalue",
116	"r9.ctx_offset",
117	"r9.map_fd",
118	"r9.packet_offset",
119	"r9.shared_offset",
120	"r9.stack_offset",
121	"r9.type",
122	"r9.shared_region_size",
123	"r9.stack_numeric_size",
124	"r10.svalue",
125	"r10.uvalue",
126	"r10.ctx_offset",
127	"r10.map_fd",
128	"r10.packet_offset",
129	"r10.shared_offset",
130	"r10.stack_offset",
131	"r10.type",
132	"r10.shared_region_size",
133	"r10.stack_numeric_size",
134	"data_size",
135	"meta_size",
136	};	336,859✔
137	}	7,355✔
138
139	thread_local LazyAllocator<std::vector<std::string>, default_variable_names> Variable::names;
140
141	void Variable::clear_thread_local_state() { names.clear(); }	2,502✔
142
143	Variable Variable::reg(const DataKind kind, const int i) { return make("r" + std::to_string(i) + "." + name_of(kind)); }	37,257,200✔
144
UNCOV 145	std::ostream& operator<<(std::ostream& o, const DataKind& s) { return o << name_of(s); }	×
146
147	static std::string mk_scalar_name(const DataKind kind, const Number& o, const Number& size) {	185,164✔
148	std::stringstream os;	185,164✔
149	os << "s" << "[" << o;	185,164✔
150	if (size != 1) {	185,164✔
151	os << "..." << o + size - 1;	241,308✔
152	}
153	os << "]." << name_of(kind);	277,746✔
154	return os.str();	370,328✔
155	}	185,164✔
156
157	Variable Variable::stack_frame_var(const DataKind kind, const int i, const std::string& prefix) {	2,420✔
158	return make(prefix + STACK_FRAME_DELIMITER + "r" + std::to_string(i) + "." + name_of(kind));	6,050✔
159	}
160
161	Variable Variable::cell_var(const DataKind array, const Number& offset, const Number& size) {	185,164✔
162	return make(mk_scalar_name(array, offset.cast_to<uint64_t>(), size));	277,746✔
163	}
164
165	// Given a type variable, get the associated variable of a given kind.
166	Variable Variable::kind_var(const DataKind kind, const Variable type_variable) {	14,782,384✔
167	const std::string name = type_variable.name();	14,782,384✔
168	return make(name.substr(0, name.rfind('.') + 1) + name_of(kind));	29,564,768✔
169	}	14,782,384✔
170
171	Variable Variable::meta_offset() { return make("meta_offset"); }	19,820✔
172	Variable Variable::packet_size() { return make("packet_size"); }	29,735✔
173	Variable Variable::loop_counter(const std::string& label) { return make("pc[" + label + "]"); }	520✔
174
175	static bool ends_with(const std::string& str, const std::string& suffix) {	32,266,698✔
176	return str.size() >= suffix.size() && 0 == str.compare(str.size() - suffix.size(), suffix.size(), suffix);	32,266,698✔
177	}
178
179	std::vector<Variable> Variable::get_type_variables() {	56,230✔
180	std::vector<Variable> res;	56,230✔
181	for (const std::string& name : *names) {	32,322,928✔
182	if (ends_with(name, ".type")) {	48,400,047✔
183	res.push_back(make(name));	4,833,246✔
184	}
185	}
186	return res;	56,230✔
UNCOV 187	}	×
188
189	bool Variable::is_in_stack() const { return this->name()[0] == 's'; }	1,946✔
190
191	bool Variable::printing_order(const Variable& a, const Variable& b) { return a.name() < b.name(); }	1,440✔
192
UNCOV 193	std::vector<Variable> Variable::get_loop_counters() {	×
UNCOV 194	std::vector<Variable> res;	×
195	for (const std::string& name : *names) {	×
196	if (name.find("pc") == 0) {	×
197	res.push_back(make(name));	×
198	}
199	}
UNCOV 200	return res;	×
UNCOV 201	}	×
202	} // end namespace prevail

Alan-Jowett / ebpf-verifier / 15194704016

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