21968098219

Committed 12 Feb 2026 11:19PM UTC coverage: 87.328% (+0.5%) from 86.783%

Build # 21968098219

Build Type

Pull #161

github

Committed by

web-flow

Commit Message

Merge fcfbad30c into f1f1d42d7

Pull Request Pull Request #161: Failure slice

Run Details

527 of 677 new or added lines in 8 files covered. (77.84%)

20 existing lines in 2 files now uncovered.

10020 of 11474 relevant lines covered (87.33%)

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

Alan-Jowett / ebpf-verifier / 21968098219

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