27778108035

Committed 07 Jun 2026 06:51PM UTC coverage: 86.386% (-2.5%) from 88.93%

Build # 27778108035

Build Type

push

github

Committed by

elazarg

Commit Message

Release v0.2.5

Bump project version to 0.2.5 and add a CHANGELOG entry covering ELF loader hardening, numeric-domain soundness fixes, and the writable helper output initialization documentation update since v0.2.4. Also updates the using_installed_package example version requirement.

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

Coverage Stats

9125 of 10563 relevant lines covered (86.39%)

6334294.72 hits per line

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

93.33

/src/fwd_analyzer.cpp

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

#include "analysis_context.hpp"
#include "cfg/cfg.hpp"
#include "cfg/wto.hpp"
#include "config.hpp"
#include "crab/ebpf_domain.hpp"
#include "crab/extrapolator.hpp"
#include "ir/program.hpp"
#include "result.hpp"
#include "verifier.hpp"

namespace prevail {

// Resets the SplitDBM thread-local scratch buffer used for transient graph
// operations. Call between analyses to keep peak memory down.
void ebpf_verifier_clear_thread_local_state() { ZoneDomain::clear_thread_local_state(); }

class InterleavedFwdFixpointIterator final {
    const AnalysisContext& context;
    const Program& _prog;
    const Cfg& _cfg;
    const Wto _wto;
    AnalysisResult& result;
    Extrapolator _extrapolator;

    /// Used to skip the analysis until _entry is found
    bool _skip{true};

    [[nodiscard]]
    bool has_error(const Label& node) const {
        return result.invariants.at(node).error.has_value();
    }

    void set_error(const Label& node, VerificationError&& error) {
        result.failed = true;
        result.invariants.at(node).error = std::move(error);
    }

    void set_pre(const Label& label, EbpfDomain&& v) { result.invariants.at(label).pre = std::move(v); }
    void set_pre(const Label& label, const EbpfDomain& v) { result.invariants.at(label).pre = v; }

    [[nodiscard]]
    const EbpfDomain& get_pre(const Label& node) const {
        return result.invariants.at(node).pre;
    }

    [[nodiscard]]
    const EbpfDomain& get_post(const Label& node) const {
        return result.invariants.at(node).post;
    }

    void transform_to_post(const Label& label, EbpfDomain pre) {
        const auto& ins = _prog.instruction_at(label);

        if (context.options.verbosity_opts.collect_instruction_deps) {
            result.invariants.at(label).deps = extract_instruction_deps(ins, pre, context.runtime().total_stack_size());
        }

        if (!std::holds_alternative<IncrementLoopCounter>(ins)) {
            if (has_error(label)) {
                return;
            }
            for (const auto& assertion : _prog.assertions_at(label)) {
                if (auto error = ebpf_domain_check(pre, assertion, label, context)) {
                    set_error(label, std::move(*error));
                    return;
                }
            }
        }
        ebpf_domain_transform(pre, ins, context);

        result.invariants.at(label).post = std::move(pre);
    }

    EbpfDomain join_all_prevs(const Label& node) const {
        if (node == _cfg.entry_label()) {
            return get_pre(node);
        }
        EbpfDomain res = EbpfDomain::bottom();
        for (const Label& prev : _cfg.parents_of(node)) {
            res |= get_post(prev);
        }
        return res;
    }

    static std::vector<Variable> collect_loop_counters(const Wto& wto, bool check_for_termination) {
        std::vector<Variable> counters;
        if (check_for_termination) {
            wto.for_each_loop_head(
                [&](const Label& label) { counters.push_back(variable_registry.loop_counter(to_string(label))); });
        }
        return counters;
    }

    explicit InterleavedFwdFixpointIterator(const AnalysisContext& context, AnalysisResult& result)
        : context(context), _prog(context.program), _cfg(context.program.cfg()), _wto(context.program.cfg()),
          result(result), _extrapolator(context, collect_loop_counters(_wto, context.runtime().check_for_termination)) {
        for (const auto& label : _cfg.labels()) {
            result.invariants.emplace(label, InvariantMapPair{EbpfDomain::bottom(), {}, EbpfDomain::bottom()});
        }
    }

    [[nodiscard]]
    static std::optional<VerificationError> check_loop_bound(const Program& prog, const Label& label,
                                                             const EbpfDomain& pre, const AnalysisContext& context) {
        if (std::holds_alternative<IncrementLoopCounter>(prog.instruction_at(label))) {
            const auto assertions = prog.assertions_at(label);
            if (assertions.size() != 1) {
                CRAB_ERROR("Expected exactly 1 assertion for IncrementLoopCounter");
            }
            return ebpf_domain_check(pre, assertions.front(), label, context);
        }
        return {};
    }

    void find_termination_errors(const Program& prog) {
        for (const auto& [label, inv_pair] : result.invariants) {
            if (inv_pair.pre.is_bottom()) {
                continue;
            }
            if (auto error = check_loop_bound(prog, label, inv_pair.pre, context)) {
                set_error(label, std::move(*error));
            }
        }
    }

    int max_loop_count() const {
        ExtendedNumber loop_count{0};
        for (const auto& inv_pair : std::views::values(result.invariants)) {
            loop_count = std::max(loop_count, inv_pair.post.get_loop_count_upper_bound(_extrapolator.loop_counters()));
        }
        const auto m = loop_count.number();
        if (m && m->fits<int32_t>()) {
            return m->cast_to<int32_t>();
        }
        return std::numeric_limits<int>::max();
    }

  public:
    void operator()(const Label& node);

    void operator()(const std::shared_ptr<WtoCycle>& cycle);

    static AnalysisResult run(const AnalysisContext& context, EbpfDomain entry_inv);
};

AnalysisResult analyze(const Program& prog, const VerifierOptions& options) {
    return analyze(AnalysisContext{prog, options});
}

AnalysisResult analyze(const AnalysisContext& context) {
    const auto* ctx = context.program_info().type.ctx_descriptor;
    const bool init_r1 = ctx != nullptr && ctx->size > 0;
    return InterleavedFwdFixpointIterator::run(context, EbpfDomain::setup_entry(init_r1, context));
}

AnalysisResult analyze(const EbpfDomain& entry_invariant, const AnalysisContext& context) {
    return InterleavedFwdFixpointIterator::run(context, entry_invariant);
}

void InterleavedFwdFixpointIterator::operator()(const Label& node) {
    if (_skip && node == _cfg.entry_label()) {
        _skip = false;
    }
    if (_skip) {
        return;
    }

    EbpfDomain pre = join_all_prevs(node);

    set_pre(node, pre);
    transform_to_post(node, std::move(pre));
}

void InterleavedFwdFixpointIterator::operator()(const std::shared_ptr<WtoCycle>& cycle) {
    const Label head = cycle->head();

    bool entry_in_this_cycle = false;
    if (_skip) {
        entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);
        _skip = !entry_in_this_cycle;
        if (_skip) {
            return;
        }
    }

    const auto initial_head_state = [&]() -> EbpfDomain {
        if (entry_in_this_cycle) {
            return get_pre(_cfg.entry_label());
        }
        const WtoNesting cycle_nesting = _wto.nesting(head);
        EbpfDomain inv = EbpfDomain::bottom();
        for (const Label& prev : _cfg.parents_of(head)) {
            if (!(_wto.nesting(prev) > cycle_nesting)) {
                inv |= get_post(prev);
            }
        }
        return inv;
    };

    const Extrapolator::Step propagate = [this, &head, &cycle](const EbpfDomain& invariant) {
        set_pre(head, invariant);
        transform_to_post(head, invariant);
        for (const auto& component : *cycle) {
            const auto plabel = std::get_if<Label>(&component);
            if (!plabel || *plabel != head) {
                std::visit(*this, component);
            }
        }
        return join_all_prevs(head);
    };

    set_pre(head, _extrapolator.compute_fixpoint(initial_head_state(), propagate));
}

AnalysisResult InterleavedFwdFixpointIterator::run(const AnalysisContext& context, EbpfDomain entry_inv) {
    const Program& prog = context.program;
    AnalysisResult result;
    InterleavedFwdFixpointIterator analyzer(context, result);
    if (context.runtime().check_for_termination) {
        analyzer._wto.for_each_loop_head(
            [&](const Label& label) { ebpf_domain_initialize_loop_counter(entry_inv, label, context); });
    }
    analyzer.set_pre(prog.cfg().entry_label(), std::move(entry_inv));
    for (const auto& component : analyzer._wto) {
        std::visit(analyzer, component);
    }
    if (!result.failed && context.runtime().check_for_termination) {
        analyzer.find_termination_errors(prog);
        if (!result.failed) {
            result.max_loop_count = analyzer.max_loop_count();
        }
    }
    result.exit_value = analyzer.get_post(Label::exit).get_r0();
    return result;
}

} // namespace prevail

1	// Copyright (c) Prevail Verifier contributors.
2	// SPDX-License-Identifier: Apache-2.0
3	#include <cassert>
4	#include <ranges>
5	#include <utility>
6	#include <variant>
7
8	#include "analysis_context.hpp"
9	#include "cfg/cfg.hpp"
10	#include "cfg/wto.hpp"
11	#include "config.hpp"
12	#include "crab/ebpf_domain.hpp"
13	#include "crab/extrapolator.hpp"
14	#include "ir/program.hpp"
15	#include "result.hpp"
16	#include "verifier.hpp"
17
18	namespace prevail {
19
20	// Resets the SplitDBM thread-local scratch buffer used for transient graph
21	// operations. Call between analyses to keep peak memory down.
22	void ebpf_verifier_clear_thread_local_state() { ZoneDomain::clear_thread_local_state(); }	3,596✔
23
24	class InterleavedFwdFixpointIterator final {
25	const AnalysisContext& context;
26	const Program& _prog;
27	const Cfg& _cfg;
28	const Wto _wto;
29	AnalysisResult& result;
30	Extrapolator _extrapolator;
31
32	/// Used to skip the analysis until _entry is found
33	bool _skip{true};
34
35	[[nodiscard]]
36	bool has_error(const Label& node) const {	1,295,862✔
37	return result.invariants.at(node).error.has_value();	1,295,862✔
38	}
39
40	void set_error(const Label& node, VerificationError&& error) {	1,756✔
41	result.failed = true;	1,756✔
42	result.invariants.at(node).error = std::move(error);	1,756✔
43	}	1,756✔
44
45	void set_pre(const Label& label, EbpfDomain&& v) { result.invariants.at(label).pre = std::move(v); }	4,178✔
46	void set_pre(const Label& label, const EbpfDomain& v) { result.invariants.at(label).pre = v; }	1,296,078✔
47
48	[[nodiscard]]
49	const EbpfDomain& get_pre(const Label& node) const {	4,092✔
50	return result.invariants.at(node).pre;	6,138✔
51	}
52
53	[[nodiscard]]
54	const EbpfDomain& get_post(const Label& node) const {	1,396,640✔
55	return result.invariants.at(node).post;	2,094,960✔
56	}
57
58	void transform_to_post(const Label& label, EbpfDomain pre) {	1,296,078✔
59	const auto& ins = _prog.instruction_at(label);	1,296,078✔
60
61	if (context.options.verbosity_opts.collect_instruction_deps) {	1,296,078✔
62	result.invariants.at(label).deps = extract_instruction_deps(ins, pre, context.runtime().total_stack_size());	452✔
63	}
64
65	if (!std::holds_alternative<IncrementLoopCounter>(ins)) {	1,296,078✔
66	if (has_error(label)) {	1,295,862✔
67	return;	9✔
68	}
69	for (const auto& assertion : _prog.assertions_at(label)) {	2,391,944✔
70	if (auto error = ebpf_domain_check(pre, assertion, label, context)) {	1,097,834✔
71	set_error(label, std::move(*error));	1,734✔
72	return;	1,734✔
73	}	1,096,967✔
74	}	1,295,844✔
75	}
76	ebpf_domain_transform(pre, ins, context);	1,294,326✔
77
78	result.invariants.at(label).post = std::move(pre);	1,294,326✔
79	}
80
81	EbpfDomain join_all_prevs(const Label& node) const {	1,296,078✔
82	if (node == _cfg.entry_label()) {	1,944,117✔
83	return get_pre(node);	4,092✔
84	}
85	EbpfDomain res = EbpfDomain::bottom();	1,291,986✔
86	for (const Label& prev : _cfg.parents_of(node)) {	2,684,448✔
87	res \|= get_post(prev);	1,392,462✔
88	}
89	return res;	1,291,986✔
90	}	1,291,986✔
91
92	static std::vector<Variable> collect_loop_counters(const Wto& wto, bool check_for_termination) {	4,092✔
93	std::vector<Variable> counters;	4,092✔
94	if (check_for_termination) {	4,092✔
95	wto.for_each_loop_head(	44✔
96	[&](const Label& label) { counters.push_back(variable_registry.loop_counter(to_string(label))); });	107✔
97	}
98	return counters;	4,092✔
99	}	×
100
101	explicit InterleavedFwdFixpointIterator(const AnalysisContext& context, AnalysisResult& result)	4,092✔
102	: context(context), _prog(context.program), _cfg(context.program.cfg()), _wto(context.program.cfg()),	4,092✔
103	result(result), _extrapolator(context, collect_loop_counters(_wto, context.runtime().check_for_termination)) {	4,092✔
104	for (const auto& label : _cfg.labels()) {	1,329,730✔
105	result.invariants.emplace(label, InvariantMapPair{EbpfDomain::bottom(), {}, EbpfDomain::bottom()});	1,325,638✔
106	}
107	}	4,092✔
108
109	[[nodiscard]]
110	static std::optional<VerificationError> check_loop_bound(const Program& prog, const Label& label,	434✔
111	const EbpfDomain& pre, const AnalysisContext& context) {
112	if (std::holds_alternative<IncrementLoopCounter>(prog.instruction_at(label))) {	434✔
113	const auto assertions = prog.assertions_at(label);	42✔
114	if (assertions.size() != 1) {	42✔
115	CRAB_ERROR("Expected exactly 1 assertion for IncrementLoopCounter");	×
116	}
117	return ebpf_domain_check(pre, assertions.front(), label, context);	42✔
118	}	42✔
119	return {};	392✔
120	}
121
122	void find_termination_errors(const Program& prog) {	44✔
123	for (const auto& [label, inv_pair] : result.invariants) {	512✔
124	if (inv_pair.pre.is_bottom()) {	468✔
125	continue;	34✔
126	}
127	if (auto error = check_loop_bound(prog, label, inv_pair.pre, context)) {	434✔
128	set_error(label, std::move(*error));	22✔
129	}	434✔
130	}
131	}	44✔
132
133	int max_loop_count() const {	22✔
134	ExtendedNumber loop_count{0};	22✔
135	for (const auto& inv_pair : std::views::values(result.invariants)) {	290✔
136	loop_count = std::max(loop_count, inv_pair.post.get_loop_count_upper_bound(_extrapolator.loop_counters()));	422✔
137	}
138	const auto m = loop_count.number();	22✔
139	if (m && m->fits<int32_t>()) {	22✔
140	return m->cast_to<int32_t>();	22✔
141	}
142	return std::numeric_limits<int>::max();
143	}
144
145	public:
146	void operator()(const Label& node);
147
148	void operator()(const std::shared_ptr<WtoCycle>& cycle);
149
150	static AnalysisResult run(const AnalysisContext& context, EbpfDomain entry_inv);
151	};
152
153	AnalysisResult analyze(const Program& prog, const VerifierOptions& options) {	1,958✔
154	return analyze(AnalysisContext{prog, options});	3,916✔
155	}
156
157	AnalysisResult analyze(const AnalysisContext& context) {	1,986✔
158	const auto* ctx = context.program_info().type.ctx_descriptor;	1,986✔
159	const bool init_r1 = ctx != nullptr && ctx->size > 0;	1,986✔
160	return InterleavedFwdFixpointIterator::run(context, EbpfDomain::setup_entry(init_r1, context));	1,986✔
161	}
162
163	AnalysisResult analyze(const EbpfDomain& entry_invariant, const AnalysisContext& context) {	2,106✔
164	return InterleavedFwdFixpointIterator::run(context, entry_invariant);	2,106✔
165	}
166
167	void InterleavedFwdFixpointIterator::operator()(const Label& node) {	1,295,646✔
168	if (_skip && node == _cfg.entry_label()) {	1,297,692✔
169	_skip = false;	4,092✔
170	}
171	if (_skip) {	1,295,646✔
172	return;	×
173	}
174
175	EbpfDomain pre = join_all_prevs(node);	1,295,646✔
176
177	set_pre(node, pre);	1,295,646✔
178	transform_to_post(node, std::move(pre));	1,295,646✔
179	}	1,295,646✔
180
181	void InterleavedFwdFixpointIterator::operator()(const std::shared_ptr<WtoCycle>& cycle) {	86✔
182	const Label head = cycle->head();	86✔
183
184	bool entry_in_this_cycle = false;	86✔
185	if (_skip) {	86✔
186	entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);	×
187	_skip = !entry_in_this_cycle;	×
188	if (_skip) {	×
189	return;	×
190	}
191	}
192
193	const auto initial_head_state = [&]() -> EbpfDomain {	129✔
194	if (entry_in_this_cycle) {	86✔
195	return get_pre(_cfg.entry_label());	×
196	}
197	const WtoNesting cycle_nesting = _wto.nesting(head);	86✔
198	EbpfDomain inv = EbpfDomain::bottom();	86✔
199	for (const Label& prev : _cfg.parents_of(head)) {	258✔
200	if (!(_wto.nesting(prev) > cycle_nesting)) {	172✔
201	inv \|= get_post(prev);	86✔
202	}
203	}
204	return inv;	86✔
205	};	86✔
206
207	const Extrapolator::Step propagate = [this, &head, &cycle](const EbpfDomain& invariant) {	×
208	set_pre(head, invariant);	432✔
209	transform_to_post(head, invariant);	432✔
210	for (const auto& component : *cycle) {	4,256✔
211	const auto plabel = std::get_if<Label>(&component);	3,824✔
212	if (!plabel \|\| *plabel != head) {	3,819✔
213	std::visit(*this, component);	3,392✔
214	}
215	}
216	return join_all_prevs(head);	432✔
217	};	86✔
218
219	set_pre(head, _extrapolator.compute_fixpoint(initial_head_state(), propagate));	86✔
220	}	129✔
221
222	AnalysisResult InterleavedFwdFixpointIterator::run(const AnalysisContext& context, EbpfDomain entry_inv) {	4,092✔
223	const Program& prog = context.program;	4,092✔
224	AnalysisResult result;	4,092✔
225	InterleavedFwdFixpointIterator analyzer(context, result);	4,092✔
226	if (context.runtime().check_for_termination) {	4,092✔
227	analyzer._wto.for_each_loop_head(	44✔
228	[&](const Label& label) { ebpf_domain_initialize_loop_counter(entry_inv, label, context); });	86✔
229	}
230	analyzer.set_pre(prog.cfg().entry_label(), std::move(entry_inv));	4,092✔
231	for (const auto& component : analyzer._wto) {	1,296,432✔
232	std::visit(analyzer, component);	1,292,340✔
233	}
234	if (!result.failed && context.runtime().check_for_termination) {	4,092✔
235	analyzer.find_termination_errors(prog);	44✔
236	if (!result.failed) {	44✔
237	result.max_loop_count = analyzer.max_loop_count();	22✔
238	}
239	}
240	result.exit_value = analyzer.get_post(Label::exit).get_r0();	4,092✔
241	return result;	6,138✔
242	}	4,092✔
243
244	} // namespace prevail

Alan-Jowett / ebpf-verifier / 27778108035

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