21966480827

Committed 12 Feb 2026 10:19PM UTC coverage: 87.348% (+0.6%) from 86.783%

Build # 21966480827

Build Type

Pull #161

github

Committed by

web-flow

Commit Message

Merge a1219c8a3 into f1f1d42d7

Pull Request Pull Request #161: Failure slice

Coverage Stats

517 of 660 new or added lines in 8 files covered. (78.33%)

9 existing lines in 2 files now uncovered.

10011 of 11461 relevant lines covered (87.35%)

2950570.78 hits per line

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

91.19

/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() {
    CrabStats::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);

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

Alan-Jowett / ebpf-verifier / 21966480827

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