18658728485

Committed 18 Oct 2025 05:56PM UTC coverage: 88.47% (+0.4%) from 88.11%

Build # 18658728485

Build Type

push

github

Committed by

elazarg

Commit Message

Bump external/bpf_conformance from `8f3c2fe` to `6fa6a20`

Bumps [external/bpf_conformance](https://github.com/Alan-Jowett/bpf_conformance) from `8f3c2fe` to `6fa6a20`.
- [Release notes](https://github.com/Alan-Jowett/bpf_conformance/releases)
- [Commits](https://github.com/Alan-Jowett/bpf_conformance/compare/8f3c2fe88...<a class=hub.com/Alan-Jowett/ebpf-verifier/commit/6fa6a20ac6fd3612ea9338312a67408687b9f06b">6fa6a20ac)

---
updated-dependencies:
- dependency-name: external/bpf_conformance
  dependency-version: 6fa6a20ac6fd3612ea9338312a67408687b9f06b
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>

Run Details

8954 of 10121 relevant lines covered (88.47%)

18293099.16 hits per line

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

77.97

/src/crab_verifier.cpp

// Copyright (c) Prevail Verifier contributors.
// SPDX-License-Identifier: MIT
/**
 *  This module is about selecting the numerical and memory domains, initiating
 *  the verification process and returning the results.
 **/

#include <map>
#include <ranges>
#include <string>

#include "asm_files.hpp"
#include "asm_syntax.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/fwd_analyzer.hpp"
#include "crab/var_registry.hpp"
#include "crab_utils/lazy_allocator.hpp"
#include "crab_verifier.hpp"
#include "string_constraints.hpp"

using std::string;

namespace prevail {
thread_local LazyAllocator<ProgramInfo> thread_local_program_info;
thread_local ebpf_verifier_options_t thread_local_options;
void ebpf_verifier_clear_before_analysis();

bool Invariants::is_valid_after(const Label& label, const StringInvariant& state) const {
    const EbpfDomain abstract_state =
        EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);
    return abstract_state <= invariants.at(label).post;
}

StringInvariant Invariants::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }

Interval Invariants::exit_value() const { return invariants.at(Label::exit).post.get_r0(); }

int Invariants::max_loop_count() const {
    ExtendedNumber max_loop_count{0};
    // Gather the upper bound of loop counts from post-invariants.
    for (const auto& inv_pair : std::views::values(invariants)) {
        max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound());
    }
    const auto m = max_loop_count.number();
    if (m && m->fits<int32_t>()) {
        return m->cast_to<int32_t>();
    }
    return std::numeric_limits<int>::max();
}

Invariants analyze(const Program& prog, EbpfDomain&& entry_invariant) {
    return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};
}

Invariants analyze(const Program& prog) {
    ebpf_verifier_clear_before_analysis();
    return analyze(prog, EbpfDomain::setup_entry(thread_local_options.setup_constraints));
}

Invariants analyze(const Program& prog, const StringInvariant& entry_invariant) {
    ebpf_verifier_clear_before_analysis();
    return analyze(prog, EbpfDomain::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));
}

bool Invariants::verified(const Program& prog) const {
    for (const auto& [label, inv_pair] : invariants) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        for (const Assertion& assertion : prog.assertions_at(label)) {
            if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {
                return false;
            }
        }
    }
    return true;
}

Report Invariants::check_assertions(const Program& prog) const {
    Report report;
    for (const auto& [label, inv_pair] : invariants) {
        if (inv_pair.pre.is_bottom()) {
            continue;
        }
        for (const Assertion& assertion : prog.assertions_at(label)) {
            const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);
            for (const auto& msg : warnings) {
                report.warnings[label].emplace_back(msg);
            }
        }
        if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {
            if (inv_pair.post.is_bottom()) {
                const auto s = to_string(*passume);
                report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");
            }
        }
    }
    return report;
}

void ebpf_verifier_clear_before_analysis() {
    clear_thread_local_state();
    variable_registry.clear();
}

void ebpf_verifier_clear_thread_local_state() {
    CrabStats::clear_thread_local_state();
    thread_local_program_info.clear();
    clear_thread_local_state();
    SplitDBM::clear_thread_local_state();
}
} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: MIT
3	/**
4	* This module is about selecting the numerical and memory domains, initiating
5	* the verification process and returning the results.
6	**/
7
8	#include <map>
9	#include <ranges>
10	#include <string>
11
12	#include "asm_files.hpp"
13	#include "asm_syntax.hpp"
14	#include "crab/ebpf_domain.hpp"
15	#include "crab/fwd_analyzer.hpp"
16	#include "crab/var_registry.hpp"
17	#include "crab_utils/lazy_allocator.hpp"
18	#include "crab_verifier.hpp"
19	#include "string_constraints.hpp"
20
21	using std::string;
22
23	namespace prevail {
24	thread_local LazyAllocator<ProgramInfo> thread_local_program_info;	696✔
25	thread_local ebpf_verifier_options_t thread_local_options;
26	void ebpf_verifier_clear_before_analysis();
27
28	bool Invariants::is_valid_after(const Label& label, const StringInvariant& state) const {	×
29	const EbpfDomain abstract_state =
30	EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);	×
31	return abstract_state <= invariants.at(label).post;	×
32	}	×
33
34	StringInvariant Invariants::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }	1,384✔
35
36	Interval Invariants::exit_value() const { return invariants.at(Label::exit).post.get_r0(); }	444✔
37
38	int Invariants::max_loop_count() const {	×
39	ExtendedNumber max_loop_count{0};	×
40	// Gather the upper bound of loop counts from post-invariants.
41	for (const auto& inv_pair : std::views::values(invariants)) {	×
42	max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound());	×
43	}
44	const auto m = max_loop_count.number();	×
45	if (m && m->fits<int32_t>()) {	×
46	return m->cast_to<int32_t>();	×
47	}
48	return std::numeric_limits<int>::max();
49	}	×
50
51	Invariants analyze(const Program& prog, EbpfDomain&& entry_invariant) {	2,496✔
52	return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};	4,991✔
53	}
54
55	Invariants analyze(const Program& prog) {	668✔
56	ebpf_verifier_clear_before_analysis();	668✔
57	return analyze(prog, EbpfDomain::setup_entry(thread_local_options.setup_constraints));	1,001✔
58	}
59
60	Invariants analyze(const Program& prog, const StringInvariant& entry_invariant) {	1,828✔
61	ebpf_verifier_clear_before_analysis();	1,828✔
62	return analyze(prog, EbpfDomain::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));	2,742✔
63	}
64
65	bool Invariants::verified(const Program& prog) const {	1,110✔
66	for (const auto& [label, inv_pair] : invariants) {	171,614✔
67	if (inv_pair.pre.is_bottom()) {	170,574✔
68	continue;	1,486✔
69	}
70	for (const Assertion& assertion : prog.assertions_at(label)) {	312,304✔
71	if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {	143,286✔
72	return false;	70✔
73	}
74	}	169,088✔
75	}
76	return true;	520✔
77	}
78
79	Report Invariants::check_assertions(const Program& prog) const {	1,384✔
80	Report report;	1,384✔
81	for (const auto& [label, inv_pair] : invariants) {	6,734✔
82	if (inv_pair.pre.is_bottom()) {	5,350✔
83	continue;	526✔
84	}
85	for (const Assertion& assertion : prog.assertions_at(label)) {	7,708✔
86	const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);	2,884✔
87	for (const auto& msg : warnings) {	3,262✔
88	report.warnings[label].emplace_back(msg);	378✔
89	}
90	}	7,708✔
91	if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {	7,499✔
92	if (inv_pair.post.is_bottom()) {	548✔
93	const auto s = to_string(*passume);	182✔
94	report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");	364✔
95	}	182✔
96	}
97	}
98	return report;	1,384✔
99	}	×
100
101	void ebpf_verifier_clear_before_analysis() {	2,496✔
102	clear_thread_local_state();	2,496✔
103	variable_registry.clear();	2,496✔
104	}	2,496✔
105
106	void ebpf_verifier_clear_thread_local_state() {	1,392✔
107	CrabStats::clear_thread_local_state();	1,392✔
108	thread_local_program_info.clear();	1,392✔
109	clear_thread_local_state();	1,392✔
110	SplitDBM::clear_thread_local_state();	1,392✔
111	}	1,392✔
112	} // namespace prevail

Alan-Jowett / ebpf-verifier / 18658728485

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