29279923487

Committed 12 Jul 2026 11:38AM UTC coverage: 86.649% (+0.3%) from 86.386%

Build # 29279923487

Build Type

push

github

Committed by

web-flow

Commit Message

Drive sample verification tests from the inventory; parallelize CI (#1195)

Full-program verification of the ebpf-samples corpus was 17 C++ files
generated by scripts/generate_verify_project_tests.py from
test-data/elf_inventory.json, then compiled into the test binary. The
generated files duplicated the inventory and could drift from it (there
was no check keeping them in sync), and the whole corpus ran in one
single-threaded Catch2 process.

Data-driven tests (dedup)
-------------------------
- Add src/test/test_verify_samples.cpp, which reads elf_inventory.json at
  runtime (via yaml-cpp; JSON is a subset of YAML) and registers one
  Catch2 DYNAMIC_SECTION per (object, section[, program]). Adding or
  retagging a sample is now a JSON edit: no code generation, no recompile.
- Delete the 17 generated test_verify_<project>.cpp files and
  scripts/generate_verify_project_tests.py. The inventory is the single
  source of truth. A coverage-guard test asserts the registered projects
  match the inventory exactly, so a new project cannot be left untested.
- Trim test_verify.hpp to the ELF-parse cache and the VerifyIssueKind
  taxonomy the driver and the multithreading test still use.

  Catch2's [!shouldfail] is a compile-time per-TEST_CASE tag and cannot be
  applied per data-driven entry, so an expected_failure (a safe program
  the verifier is currently too imprecise to accept) is asserted as
  *still rejected* -- an xfail/golden marker. A verifier improvement that
  starts accepting it fails the case, prompting an inventory update; a
  regression on a passing program fails it too.

Parallel CI (ctest)
-------------------
- Register ctest entries: one per project (sharded by tag) plus a "unit"
  entry for everything else. The shard list is derived from the inventory
  via string(JSON), so it cannot drift from the corpus.
- CI runs `ctest -j` instead of a single `bin/tests` process. Locally, a
  full run drops from ~104s to ~42s on 16 cores (bounded by t... (continued)

Coverage Stats

9313 of 10748 relevant lines covered (86.65%)

6391896.2 hits per line

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

87.06

/src/crab/type_to_num.cpp

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

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

namespace prevail {

std::optional<Variable> TypeToNumDomain::primary_kind_variable_for_type(const Reg& reg) const {
    const auto type = types.get_type(reg);
    if (!type) {
        return {};
    }
    return prevail::primary_kind_variable_for_type(reg, *type);
}

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 = right;
        return;
    }
    if (right.is_bottom()) {
        return;
    }
    auto extra_invariants = collect_type_dependent_constraints(right);
    this->values |= right.values;
    for (const auto& [variable, interval] : extra_invariants) {
        values.set(variable, interval);
    }
}

void TypeToNumDomain::operator|=(const TypeToNumDomain& other) {
    if (is_bottom()) {
        *this = other;
        // No return: the zone in `other` may not be fully closed. Falling through
        // to join_selective triggers zone self-join, whose closure step tightens
        // difference constraints (e.g. r2.uvalue-r1.uvalue<=-2 vs <=-1).
    }
    if (other.is_bottom()) {
        return;
    }
    this->join_selective(other);
    this->types |= other.types;
}

void TypeToNumDomain::operator|=(TypeToNumDomain&& other) {
    if (is_bottom()) {
        *this = other;
    }
    if (other.is_bottom()) {
        return;
    }
    this->join_selective(other);
    this->types |= std::move(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()};
}

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

std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {
    std::vector<Variable> res;
    for (const Variable v : types.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;

    // A variable tracked in only one side can still have differing type info
    // (the other side treats it as top), so we iterate the union.
    std::set<Variable> type_vars;
    for (const Variable v : types.variables()) {
        type_vars.insert(v);
    }
    for (const Variable v : right.types.variables()) {
        type_vars.insert(v);
    }
    for (const Variable& type_var : type_vars) {
        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 {
    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 {
    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.restrict_to(reg_type(reg), TypeSet{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) {
    // Precondition: caller must have checked !is_bottom(). Currently survives a
    // bottom domain only because TypeDomain::variables_with_type returns empty
    // when bottom; encode the assumption so a future change there fails loudly.
    assert(!is_bottom());
    for (const Variable type_variable : types.variables_with_type(type)) {
        types.havoc_type(type_variable);
        values.havoc(variable_registry.kind_var(DataKind::uvalues, type_variable));
        forget_type_dependent_values(type_variable);
    }
}

void TypeToNumDomain::forget_type_dependent_values(const Variable type_variable) {
    assert(variable_registry.is_type(type_variable));
    for (const auto& kinds : type_to_kinds | std::views::values) {
        for (const DataKind kind : kinds) {
            values.havoc(variable_registry.kind_var(kind, type_variable));
        }
    }
}

void TypeToNumDomain::forget_type_dependent_values(const Reg& reg) { forget_type_dependent_values(reg_type(reg)); }

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

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

    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);
    values.havoc(r.socket_offset);
    values.havoc(r.btf_id_offset);
    values.havoc(r.alloc_mem_offset);
    values.havoc(r.alloc_mem_size);
}

void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {
    for (const DataKind kind : iterate_kinds()) {
        values.havoc(variable_registry.reg(kind, reg.v));
    }
}

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

TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {
    // Unlike join, widen must NOT re-add type-dependent constraints:
    // narrowing the widened result can defeat termination (see #960).
    return TypeToNumDomain{types.widen(other.types), values.widen(other.values)};
}

TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& other) const {
    return TypeToNumDomain{types.narrow(other.types), values.narrow(other.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 <cassert>
4	#include <ranges>
5
6	#include "arith/variable.hpp"
7	#include "crab/interval.hpp"
8	#include "crab/region_semantics.hpp"
9	#include "crab/type_domain.hpp"
10	#include "crab/type_to_num.hpp"
11	#include "crab/var_registry.hpp"
12
13	namespace prevail {
14
15	std::optional<Variable> TypeToNumDomain::primary_kind_variable_for_type(const Reg& reg) const {	27,284✔
16	const auto type = types.get_type(reg);	27,284✔
17	if (!type) {	27,284✔
18	return {};	4✔
19	}
20	return prevail::primary_kind_variable_for_type(reg, *type);	27,280✔
21	}
22
23	bool TypeToNumDomain::operator<=(const TypeToNumDomain& other) const {	720✔
24	if (is_bottom()) {	720✔
25	return true;
26	}
27	if (other.is_bottom()) {	720✔
28	return false;
29	}
30	// First, check the type domain.
31	// For example, if r1 in `this` has type {stack} and r1 in `other` has type {stack, packet},
32	// then `this` is less than or equal to `other`.
33	if (!(types <= other.types)) {	720✔
34	return false;	11✔
35	}
36	// Then, check the numeric domain with consideration of type-specific variables.
37	TypeToNumDomain tmp{other.types, other.values};	1,396✔
38	for (const Variable& v : this->get_nonexistent_kind_variables()) {	20,790✔
39	tmp.values.havoc(v);	30,138✔
40	}	349✔
41	return values <= tmp.values;	698✔
42	}	698✔
43
44	void TypeToNumDomain::join_selective(const TypeToNumDomain& right) {	216,946✔
45	if (is_bottom()) {	216,946✔
46	*this = right;	×
47	return;	×
48	}
49	if (right.is_bottom()) {	216,946✔
50	return;
51	}
52	auto extra_invariants = collect_type_dependent_constraints(right);	216,946✔
53	this->values \|= right.values;	216,946✔
54	for (const auto& [variable, interval] : extra_invariants) {	304,672✔
55	values.set(variable, interval);	87,726✔
56	}
57	}	216,946✔
58
59	void TypeToNumDomain::operator\|=(const TypeToNumDomain& other) {	217,874✔
60	if (is_bottom()) {	217,874✔
61	*this = other;	154,370✔
62	// No return: the zone in `other` may not be fully closed. Falling through
63	// to join_selective triggers zone self-join, whose closure step tightens
64	// difference constraints (e.g. r2.uvalue-r1.uvalue<=-2 vs <=-1).
65	}
66	if (other.is_bottom()) {	217,874✔
67	return;	464✔
68	}
69	this->join_selective(other);	216,946✔
70	this->types \|= other.types;	216,946✔
71	}
72
73	void TypeToNumDomain::operator\|=(TypeToNumDomain&& other) {	×
74	if (is_bottom()) {	×
75	*this = other;	×
76	}
77	if (other.is_bottom()) {	×
78	return;
79	}
80	this->join_selective(other);	×
81	this->types \|= std::move(other.types);	×
82	}
83
84	TypeToNumDomain TypeToNumDomain::operator&(const TypeToNumDomain& other) const {	716✔
85	if (auto type_inv = types.meet(other.types)) {	716✔
86	// TODO: remove unuseful variables from the numeric domain
87	return TypeToNumDomain{std::move(*type_inv), values & other.values};	1,074✔
88	}	716✔
89	return TypeToNumDomain{TypeDomain::top(), NumAbsDomain::bottom()};	×
90	}
91
92	TypeToNumDomain TypeToNumDomain::operator&(TypeToNumDomain&& other) const {	×
93	if (auto type_inv = types.meet(std::move(other.types))) {	×
94	// TODO: remove unuseful variables from the numeric domain
95	return TypeToNumDomain{std::move(*type_inv), values & std::move(other.values)};	×
96	}	×
97	return {TypeDomain::top(), NumAbsDomain::bottom()};	×
98	}
99
100	std::vector<Variable> TypeToNumDomain::get_nonexistent_kind_variables() const {	698✔
101	std::vector<Variable> res;	698✔
102	for (const Variable v : types.variables()) {	2,966✔
103	for (const auto& [type, kinds] : type_to_kinds) {	27,216✔
104	if (types.may_have_type(v, type)) {	24,948✔
105	continue;	7,970✔
106	}
107	for (const auto kind : kinds) {	37,070✔
108	Variable type_offset = variable_registry.kind_var(kind, v);	20,092✔
109	res.push_back(type_offset);	20,092✔
110	}
111	}
112	}	349✔
113	return res;	698✔
114	}	×
115
116	std::vector<std::tuple<Variable, Interval>>
117	TypeToNumDomain::collect_type_dependent_constraints(const TypeToNumDomain& right) const {	216,946✔
118	std::vector<std::tuple<Variable, Interval>> result;	216,946✔
119
120	// A variable tracked in only one side can still have differing type info
121	// (the other side treats it as top), so we iterate the union.
122	std::set<Variable> type_vars;	216,946✔
123	for (const Variable v : types.variables()) {	7,725,922✔
124	type_vars.insert(v);	7,508,976✔
125	}	108,473✔
126	for (const Variable v : right.types.variables()) {	7,738,982✔
127	type_vars.insert(v);	7,522,036✔
128	}	108,473✔
129	for (const Variable& type_var : type_vars) {	7,785,502✔
130	for (const auto& [type, kinds] : type_to_kinds) {	90,822,672✔
131	if (kinds.empty()) {	83,254,116✔
132	continue;	7,568,556✔
133	}
134	const bool in_left = types.may_have_type(type_var, type);	75,685,560✔
135	const bool in_right = right.types.may_have_type(type_var, type);	75,685,560✔
136
137	// If a type may be present in one domain but not the other, its
138	// dependent constraints must be explicitly preserved.
139	if (in_left != in_right) {	75,685,560✔
140	// Identify which domain contains the constraints.
141	const NumAbsDomain& source = in_left ? values : right.values;	2,009,648✔
142	for (const DataKind kind : kinds) {	4,675,256✔
143	Variable var = variable_registry.kind_var(kind, type_var);	2,665,608✔
144	Interval value = source.eval_interval(var);	2,665,608✔
145	if (!value.is_top()) {	2,665,608✔
146	result.emplace_back(var, value);	87,726✔
147	}
148	}
149	}
150	}
151	}
152
153	return result;	325,419✔
154	}	216,946✔
155
156	std::vector<TypeEncoding> TypeToNumDomain::enumerate_types(const Reg& reg) const {	206,540✔
157	if (!types.is_initialized(reg)) {	206,540✔
158	return {T_UNINIT};	16✔
159	}
160	return types.iterate_types(reg);	206,532✔
161	}
162
163	TypeToNumDomain
164	TypeToNumDomain::join_over_types(const Reg& reg,	154,368✔
165	const std::function<void(TypeToNumDomain&, TypeEncoding)>& transition) const {
166	if (!types.is_initialized(reg)) {	154,368✔
167	TypeToNumDomain res = *this;	×
168	transition(res, T_UNINIT);	×
169	return res;	×
170	}	×
171	TypeToNumDomain res = bottom();	154,368✔
172	const std::vector<TypeEncoding> valid_types = types.iterate_types(reg);	154,368✔
173	std::map<TypeEncoding, std::vector<DataKind>> valid_type_to_kinds;	154,368✔
174	for (const TypeEncoding type : valid_types) {	308,948✔
175	valid_type_to_kinds.emplace(type, type_to_kinds.at(type));	154,580✔
176	}
177	for (const TypeEncoding type : valid_types) {	308,948✔
178	TypeToNumDomain tmp(*this);	154,580✔
179	tmp.types.restrict_to(reg_type(reg), TypeSet{type});	154,580✔
180	// This might have changed the type variable of reg.
181	// It might also have changed the type variable of other registers, but we don't deal with that.
182	for (const auto& [other_type, kinds] : valid_type_to_kinds) {	309,584✔
183	if (other_type != type) {	155,004✔
184	for (const auto kind : kinds) {	1,248✔
185	tmp.values.havoc(variable_registry.kind_var(kind, reg_type(reg)));	1,236✔
186	}
187	}
188	}
189	transition(tmp, type);	154,580✔
190	res \|= tmp;	154,580✔
191	}	154,580✔
192	return res;	154,368✔
193	}	231,552✔
194
195	void TypeToNumDomain::havoc_all_locations_having_type(const TypeEncoding type) {	3,620✔
196	// Precondition: caller must have checked !is_bottom(). Currently survives a
197	// bottom domain only because TypeDomain::variables_with_type returns empty
198	// when bottom; encode the assumption so a future change there fails loudly.
199	assert(!is_bottom());	3,620✔
200	for (const Variable type_variable : types.variables_with_type(type)) {	85,680✔
201	types.havoc_type(type_variable);	82,060✔
202	values.havoc(variable_registry.kind_var(DataKind::uvalues, type_variable));	82,060✔
203	forget_type_dependent_values(type_variable);	82,060✔
204	}	3,620✔
205	}	3,620✔
206
207	void TypeToNumDomain::forget_type_dependent_values(const Variable type_variable) {	201,994✔
208	assert(variable_registry.is_type(type_variable));	201,994✔
209	for (const auto& kinds : type_to_kinds \| std::views::values) {	2,423,928✔
210	for (const DataKind kind : kinds) {	4,847,856✔
211	values.havoc(variable_registry.kind_var(kind, type_variable));	3,938,883✔
212	}
213	}
214	}	201,994✔
215
216	void TypeToNumDomain::forget_type_dependent_values(const Reg& reg) { forget_type_dependent_values(reg_type(reg)); }	119,668✔
217
218	void TypeToNumDomain::assign(const Reg& lhs, const Reg& rhs) {	95,020✔
219	if (lhs == rhs) {	142,529✔
220	return;	1✔
221	}
222	forget_type_dependent_values(lhs);	95,018✔
223	types.assign_type(lhs, rhs);	95,018✔
224
225	values.assign(reg_pack(lhs).uvalue, reg_pack(rhs).uvalue);	95,018✔
226
227	for (const auto& type : types.iterate_types(rhs)) {	190,058✔
228	for (const auto kind : type_to_kinds.at(type)) {	223,564✔
229	const auto lhs_var = variable_registry.kind_var(kind, reg_type(lhs));	128,524✔
230	values.assign(lhs_var, variable_registry.kind_var(kind, reg_type(rhs)));	192,786✔
231	}
232	}	95,018✔
233	}
234
235	void TypeToNumDomain::havoc_offsets(const Reg& reg) {	237,420✔
236	const RegPack r = reg_pack(reg);	237,420✔
237	values.havoc(r.ctx_offset);	237,420✔
238	values.havoc(r.map_fd);	237,420✔
239	values.havoc(r.map_fd_programs);	237,420✔
240	values.havoc(r.packet_offset);	237,420✔
241	values.havoc(r.shared_offset);	237,420✔
242	values.havoc(r.shared_region_size);	237,420✔
243	values.havoc(r.stack_offset);	237,420✔
244	values.havoc(r.stack_numeric_size);	237,420✔
245	values.havoc(r.socket_offset);	237,420✔
246	values.havoc(r.btf_id_offset);	237,420✔
247	values.havoc(r.alloc_mem_offset);	237,420✔
248	values.havoc(r.alloc_mem_size);	237,420✔
249	}	237,420✔
250
251	void TypeToNumDomain::havoc_register_except_type(const Reg& reg) {	322,338✔
252	for (const DataKind kind : iterate_kinds()) {	4,835,070✔
253	values.havoc(variable_registry.reg(kind, reg.v));	6,769,098✔
254	}	322,338✔
255	}	322,338✔
256
257	void TypeToNumDomain::havoc_register(const Reg& reg) {	247,902✔
258	types.havoc_type(reg);	247,902✔
259	havoc_register_except_type(reg);	247,902✔
260	}	247,902✔
261
262	TypeToNumDomain TypeToNumDomain::widen(const TypeToNumDomain& other) const {	174✔
263	// Unlike join, widen must NOT re-add type-dependent constraints:
264	// narrowing the widened result can defeat termination (see #960).
265	return TypeToNumDomain{types.widen(other.types), values.widen(other.values)};	261✔
266	}
267
268	TypeToNumDomain TypeToNumDomain::narrow(const TypeToNumDomain& other) const {	×
269	return TypeToNumDomain{types.narrow(other.types), values.narrow(other.values)};	×
270	}
271
272	StringInvariant TypeToNumDomain::to_set() const {	1,032✔
273	if (is_bottom()) {	1,032✔
274	return StringInvariant::bottom();	×
275	}
276	return types.to_set() + values.to_set();	1,548✔
277	}
278	} // namespace prevail

Alan-Jowett / ebpf-verifier / 29279923487

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