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>

Run Details

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.08

/src/fwd_analyzer.cpp

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

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

namespace prevail {

thread_local LazyAllocator<ProgramInfo> thread_local_program_info;
thread_local ebpf_verifier_options_t thread_local_options;

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

void ebpf_verifier_clear_thread_local_state() {
    thread_local_program_info.clear();
    clear_thread_local_state();
    ZoneDomain::clear_thread_local_state();
    EbpfDomain::clear_thread_local_state();
}

class InterleavedFwdFixpointIterator final {
    const Program& _prog;
    const Cfg& _cfg;
    const Wto _wto;
    AnalysisResult& result;

    /// number of narrowing iterations. If the narrowing operator is
    /// indeed a narrowing operator this parameter is not
    /// needed. However, there are abstract domains for which an actual
    /// narrowing operation is not available so we must enforce
    /// termination.
    static constexpr unsigned int _descending_iterations = 2000000;

    /// 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; }

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

    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);

        // Dependency extraction intentionally runs on the pre-state *before*
        // ebpf_domain_transform mutates it, because extract_instruction_deps
        // needs the unmodified domain to resolve stack offsets.  We use .at()
        // (result.invariants.at(label).deps) because the entry was already
        // created during initialization.  This must also run before assertion
        // checks so that failing instructions still have deps recorded —
        // compute_failure_slices seeds its backward worklist from them.
        if (thread_local_options.verbosity_opts.collect_instruction_deps) {
            result.invariants.at(label).deps = extract_instruction_deps(ins, pre);
        }

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

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

    explicit InterleavedFwdFixpointIterator(const Program& prog, AnalysisResult& result)
        : _prog(prog), _cfg(prog.cfg()), _wto(prog.cfg()), result(result) {
        for (const auto& label : _cfg.labels()) {
            result.invariants.emplace(label, InvariantMapPair{EbpfDomain::bottom(), {}, EbpfDomain::bottom()});
        }
    }

    static std::optional<VerificationError> check_loop_bound(const Program& prog, const Label& label,
                                                             const EbpfDomain& pre) {
        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);
        }
        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)) {
                set_error(label, std::move(*error));
            }
        }
    }

    int max_loop_count() const {
        ExtendedNumber loop_count{0};
        // Gather the upper bound of loop counts from post-invariants.
        for (const auto& inv_pair : std::views::values(result.invariants)) {
            loop_count = std::max(loop_count, inv_pair.post.get_loop_count_upper_bound());
        }
        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 Program& prog, EbpfDomain entry_inv);
};

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

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

static EbpfDomain extrapolate(const EbpfDomain& before, const EbpfDomain& after, const unsigned int iteration) {
    /// number of iterations until triggering widening
    constexpr auto _widening_delay = 2;

    if (iteration < _widening_delay) {
        return before | after;
    }
    return before.widen(after, iteration == _widening_delay);
}

static EbpfDomain refine(const EbpfDomain& before, const EbpfDomain& after, const unsigned int iteration) {
    if (iteration == 1) {
        return before & after;
    } else {
        return before.narrow(after);
    }
}

void InterleavedFwdFixpointIterator::operator()(const Label& node) {
    /** decide whether skip vertex or not **/
    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();

    /** decide whether to skip cycle or not **/
    bool entry_in_this_cycle = false;
    if (_skip) {
        // We only skip the analysis of cycle if entry_label is not a
        // component of it, included nested components.
        entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);
        _skip = !entry_in_this_cycle;
        if (_skip) {
            return;
        }
    }

    EbpfDomain invariant = EbpfDomain::bottom();
    if (entry_in_this_cycle) {
        invariant = get_pre(_cfg.entry_label());
    } else {
        const WtoNesting cycle_nesting = _wto.nesting(head);
        for (const Label& prev : _cfg.parents_of(head)) {
            if (!(_wto.nesting(prev) > cycle_nesting)) {
                invariant |= get_post(prev);
            }
        }
    }

    for (unsigned int iteration = 1;; ++iteration) {
        // Increasing iteration sequence with widening
        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);
            }
        }
        EbpfDomain new_pre = join_all_prevs(head);
        if (new_pre <= invariant) {
            // Post-fixpoint reached
            set_pre(head, new_pre);
            invariant = std::move(new_pre);
            break;
        } else {
            invariant = extrapolate(invariant, new_pre, iteration);
        }
    }

    for (unsigned int iteration = 1;; ++iteration) {
        // Decreasing iteration sequence with narrowing
        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);
            }
        }
        EbpfDomain new_pre = join_all_prevs(head);
        if (invariant <= new_pre) {
            // No more refinement possible(pre == new_pre)
            break;
        } else {
            if (iteration > _descending_iterations) {
                break;
            }
            invariant = refine(invariant, std::move(new_pre), iteration);
            set_pre(head, std::move(invariant));
        }
    }
}
AnalysisResult InterleavedFwdFixpointIterator::run(const Program& prog, EbpfDomain entry_inv) {
    // Go over the CFG in weak topological order (accounting for loops).
    AnalysisResult result;
    InterleavedFwdFixpointIterator analyzer(prog, result);
    if (thread_local_options.cfg_opts.check_for_termination) {
        // Initialize loop counters for potential loop headers.
        // This enables enforcement of upper bounds on loop iterations
        // during program verification.
        // TODO: Consider making this an instruction instead of an explicit call.
        analyzer._wto.for_each_loop_head(
            [&](const Label& label) { ebpf_domain_initialize_loop_counter(entry_inv, label); });
    }
    analyzer.set_pre(prog.cfg().entry_label(), std::move(entry_inv));
    for (const auto& component : analyzer._wto) {
        std::visit(analyzer, component);
    }
    if (!result.failed && thread_local_options.cfg_opts.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 <ranges>
4	#include <utility>
5	#include <variant>
6
7	#include "cfg/cfg.hpp"
8	#include "cfg/wto.hpp"
9	#include "config.hpp"
10	#include "crab/ebpf_domain.hpp"
11	#include "ir/program.hpp"
12	#include "result.hpp"
13	#include "verifier.hpp"
14
15	namespace prevail {
16
17	thread_local LazyAllocator<ProgramInfo> thread_local_program_info;	721✔
18	thread_local ebpf_verifier_options_t thread_local_options;
19
20	static void ebpf_verifier_clear_before_analysis() {	2,800✔
21	clear_thread_local_state();	2,800✔
22	variable_registry.clear();	2,800✔
23	}	2,800✔
24
25	void ebpf_verifier_clear_thread_local_state() {	1,442✔
26	thread_local_program_info.clear();	1,442✔
27	clear_thread_local_state();	1,442✔
28	ZoneDomain::clear_thread_local_state();	1,442✔
29	EbpfDomain::clear_thread_local_state();	1,442✔
30	}	1,442✔
31
32	class InterleavedFwdFixpointIterator final {	1,400✔
33	const Program& _prog;
34	const Cfg& _cfg;
35	const Wto _wto;
36	AnalysisResult& result;
37
38	/// number of narrowing iterations. If the narrowing operator is
39	/// indeed a narrowing operator this parameter is not
40	/// needed. However, there are abstract domains for which an actual
41	/// narrowing operation is not available so we must enforce
42	/// termination.
43	static constexpr unsigned int _descending_iterations = 2000000;
44
45	/// Used to skip the analysis until _entry is found
46	bool _skip{true};
47
48	[[nodiscard]]
49	bool has_error(const Label& node) const {	391,480✔
50	return result.invariants.at(node).error.has_value();	391,480✔
51	}
52
53	void set_error(const Label& node, VerificationError&& error) {	674✔
54	result.failed = true;	674✔
55	result.invariants.at(node).error = std::move(error);	674✔
56	}	674✔
57
58	void set_pre(const Label& label, EbpfDomain&& v) { result.invariants.at(label).pre = std::move(v); }	2,800✔
59	void set_pre(const Label& label, const EbpfDomain& v) { result.invariants.at(label).pre = v; }	391,686✔
60
61	EbpfDomain get_pre(const Label& node) const { return result.invariants.at(node).pre; }	2,800✔
62
63	EbpfDomain get_post(const Label& node) const { return result.invariants.at(node).post; }	422,056✔
64
65	void transform_to_post(const Label& label, EbpfDomain pre) {	391,686✔
66	const auto& ins = _prog.instruction_at(label);	391,686✔
67
68	// Dependency extraction intentionally runs on the pre-state before
69	// ebpf_domain_transform mutates it, because extract_instruction_deps
70	// needs the unmodified domain to resolve stack offsets. We use .at()
71	// (result.invariants.at(label).deps) because the entry was already
72	// created during initialization. This must also run before assertion
73	// checks so that failing instructions still have deps recorded —
74	// compute_failure_slices seeds its backward worklist from them.
75	if (thread_local_options.verbosity_opts.collect_instruction_deps) {	391,686✔
76	result.invariants.at(label).deps = extract_instruction_deps(ins, pre);	452✔
77	}
78
79	if (!std::holds_alternative<IncrementLoopCounter>(ins)) {	391,686✔
80	if (has_error(label)) {	391,480✔
81	return;
82	}
83	for (const auto& assertion : _prog.assertions_at(label)) {	735,294✔
84	// Avoid redundant errors.
85	if (auto error = ebpf_domain_check(pre, assertion, label)) {	344,466✔
86	set_error(label, std::move(*error));	652✔
87	return;	652✔
88	}	344,140✔
89	}	391,480✔
90	}
91	ebpf_domain_transform(pre, ins);	391,034✔
92
93	result.invariants.at(label).post = std::move(pre);	391,034✔
94	}
95
96	EbpfDomain join_all_prevs(const Label& node) const {	391,686✔
97	if (node == _cfg.entry_label()) {	587,529✔
98	return get_pre(node);	198,643✔
99	}
100	EbpfDomain res = EbpfDomain::bottom();	388,886✔
101	for (const Label& prev : _cfg.parents_of(node)) {	808,094✔
102	res \|= get_post(prev);	838,416✔
103	}
104	return res;	388,886✔
105	}	388,886✔
106
107	explicit InterleavedFwdFixpointIterator(const Program& prog, AnalysisResult& result)	2,800✔
108	: _prog(prog), _cfg(prog.cfg()), _wto(prog.cfg()), result(result) {	2,800✔
109	for (const auto& label : _cfg.labels()) {	393,632✔
110	result.invariants.emplace(label, InvariantMapPair{EbpfDomain::bottom(), {}, EbpfDomain::bottom()});	390,832✔
111	}
112	}	2,800✔
113
114	static std::optional<VerificationError> check_loop_bound(const Program& prog, const Label& label,	408✔
115	const EbpfDomain& pre) {
116	if (std::holds_alternative<IncrementLoopCounter>(prog.instruction_at(label))) {	408✔
117	const auto assertions = prog.assertions_at(label);	40✔
118	if (assertions.size() != 1) {	40✔
UNCOV 119	CRAB_ERROR("Expected exactly 1 assertion for IncrementLoopCounter");	×
120	}
121	return ebpf_domain_check(pre, assertions.front(), label);	40✔
122	}	40✔
123	return {};	368✔
124	}
125
126	void find_termination_errors(const Program& prog) {	42✔
127	for (const auto& [label, inv_pair] : result.invariants) {	480✔
128	if (inv_pair.pre.is_bottom()) {	438✔
129	continue;	30✔
130	}
131	if (auto error = check_loop_bound(prog, label, inv_pair.pre)) {	408✔
132	set_error(label, std::move(*error));	22✔
133	}	408✔
134	}
135	}	42✔
136
137	int max_loop_count() const {	20✔
138	ExtendedNumber loop_count{0};	20✔
139	// Gather the upper bound of loop counts from post-invariants.
140	for (const auto& inv_pair : std::views::values(result.invariants)) {	258✔
141	loop_count = std::max(loop_count, inv_pair.post.get_loop_count_upper_bound());	375✔
142	}
143	const auto m = loop_count.number();	20✔
144	if (m && m->fits<int32_t>()) {	20✔
145	return m->cast_to<int32_t>();	20✔
146	}
147	return std::numeric_limits<int>::max();
148	}
149
150	public:
151	void operator()(const Label& node);
152
153	void operator()(const std::shared_ptr<WtoCycle>& cycle);
154
155	static AnalysisResult run(const Program& prog, EbpfDomain entry_inv);
156	};
157
158	AnalysisResult analyze(const Program& prog) {	742✔
159	ebpf_verifier_clear_before_analysis();	742✔
160	return InterleavedFwdFixpointIterator::run(prog, EbpfDomain::setup_entry(thread_local_options.setup_constraints));	1,113✔
161	}
162
163	AnalysisResult analyze(const Program& prog, const StringInvariant& entry_invariant) {	2,058✔
164	ebpf_verifier_clear_before_analysis();	2,058✔
165	return InterleavedFwdFixpointIterator::run(	1,029✔
166	prog, EbpfDomain::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));	3,087✔
167	}
168
169	static EbpfDomain extrapolate(const EbpfDomain& before, const EbpfDomain& after, const unsigned int iteration) {	156✔
170	/// number of iterations until triggering widening
171	constexpr auto _widening_delay = 2;	156✔
172
173	if (iteration < _widening_delay) {	156✔
174	return before \| after;	48✔
175	}
176	return before.widen(after, iteration == _widening_delay);	108✔
177	}
178
UNCOV 179	static EbpfDomain refine(const EbpfDomain& before, const EbpfDomain& after, const unsigned int iteration) {	×
UNCOV 180	if (iteration == 1) {	×
181	return before & after;	×
182	} else {
UNCOV 183	return before.narrow(after);	×
184	}
185	}
186
187	void InterleavedFwdFixpointIterator::operator()(const Label& node) {	391,434✔
188	/ decide whether skip vertex or not /
189	if (_skip && node == _cfg.entry_label()) {	392,834✔
190	_skip = false;	2,800✔
191	}
192	if (_skip) {	391,434✔
UNCOV 193	return;	×
194	}
195
196	EbpfDomain pre = join_all_prevs(node);	391,434✔
197
198	set_pre(node, pre);	391,434✔
199	transform_to_post(node, std::move(pre));	587,151✔
200	}	391,434✔
201
202	void InterleavedFwdFixpointIterator::operator()(const std::shared_ptr<WtoCycle>& cycle) {	48✔
203	const Label head = cycle->head();	48✔
204
205	/ decide whether to skip cycle or not /
206	bool entry_in_this_cycle = false;	48✔
207	if (_skip) {	48✔
208	// We only skip the analysis of cycle if entry_label is not a
209	// component of it, included nested components.
UNCOV 210	entry_in_this_cycle = is_component_member(_cfg.entry_label(), cycle);	×
UNCOV 211	_skip = !entry_in_this_cycle;	×
UNCOV 212	if (_skip) {	×
UNCOV 213	return;	×
214	}
215	}
216
217	EbpfDomain invariant = EbpfDomain::bottom();	48✔
218	if (entry_in_this_cycle) {	48✔
UNCOV 219	invariant = get_pre(_cfg.entry_label());	×
220	} else {
221	const WtoNesting cycle_nesting = _wto.nesting(head);	48✔
222	for (const Label& prev : _cfg.parents_of(head)) {	144✔
223	if (!(_wto.nesting(prev) > cycle_nesting)) {	96✔
224	invariant \|= get_post(prev);	96✔
225	}
226	}
227	}	48✔
228
229	for (unsigned int iteration = 1;; ++iteration) {	102✔
230	// Increasing iteration sequence with widening
231	set_pre(head, invariant);	204✔
232	transform_to_post(head, invariant);	204✔
233	for (const auto& component : *cycle) {	1,406✔
234	const auto plabel = std::get_if<Label>(&component);	1,202✔
235	if (!plabel \|\| *plabel != head) {	1,202✔
236	std::visit(*this, component);	998✔
237	}
238	}
239	EbpfDomain new_pre = join_all_prevs(head);	204✔
240	if (new_pre <= invariant) {	204✔
241	// Post-fixpoint reached
242	set_pre(head, new_pre);	48✔
243	invariant = std::move(new_pre);	48✔
244	break;	48✔
245	} else {
246	invariant = extrapolate(invariant, new_pre, iteration);	234✔
247	}
248	}	258✔
249
250	for (unsigned int iteration = 1;; ++iteration) {	48✔
251	// Decreasing iteration sequence with narrowing
252	transform_to_post(head, invariant);	48✔
253
254	for (const auto& component : *cycle) {	326✔
255	const auto plabel = std::get_if<Label>(&component);	278✔
256	if (!plabel \|\| *plabel != head) {	278✔
257	std::visit(*this, component);	230✔
258	}
259	}
260	EbpfDomain new_pre = join_all_prevs(head);	48✔
261	if (invariant <= new_pre) {	48✔
262	// No more refinement possible(pre == new_pre)
263	break;	24✔
264	} else {
UNCOV 265	if (iteration > _descending_iterations) {	×
266	break;
267	}
UNCOV 268	invariant = refine(invariant, std::move(new_pre), iteration);	×
UNCOV 269	set_pre(head, std::move(invariant));	×
270	}
271	}	48✔
272	}	72✔
273	AnalysisResult InterleavedFwdFixpointIterator::run(const Program& prog, EbpfDomain entry_inv) {	2,800✔
274	// Go over the CFG in weak topological order (accounting for loops).
275	AnalysisResult result;	2,800✔
276	InterleavedFwdFixpointIterator analyzer(prog, result);	2,800✔
277	if (thread_local_options.cfg_opts.check_for_termination) {	2,800✔
278	// Initialize loop counters for potential loop headers.
279	// This enables enforcement of upper bounds on loop iterations
280	// during program verification.
281	// TODO: Consider making this an instruction instead of an explicit call.
282	analyzer._wto.for_each_loop_head(	42✔
283	[&](const Label& label) { ebpf_domain_initialize_loop_counter(entry_inv, label); });	82✔
284	}
285	analyzer.set_pre(prog.cfg().entry_label(), std::move(entry_inv));	2,800✔
286	for (const auto& component : analyzer._wto) {	393,054✔
287	std::visit(analyzer, component);	390,254✔
288	}
289	if (!result.failed && thread_local_options.cfg_opts.check_for_termination) {	2,800✔
290	analyzer.find_termination_errors(prog);	42✔
291	if (!result.failed) {	42✔
292	result.max_loop_count = analyzer.max_loop_count();	20✔
293	}
294	}
295	result.exit_value = analyzer.get_post(Label::exit).get_r0();	4,200✔
296	return result;	4,200✔
297	}	2,800✔
298
299	} // 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