15194704016

Committed 22 May 2025 08:53AM UTC coverage: 88.11% (-0.07%) from 88.177%

Build # 15194704016

Build Type

push

github

Committed by

elazarg

Commit Message

uniform class names and explicit constructors for adapt_sgraph.hpp

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

Run Details

27 of 30 new or added lines in 1 file covered. (90.0%)

481 existing lines in 33 files now uncovered.

8552 of 9706 relevant lines covered (88.11%)

9089054.61 hits per line

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

67.24

/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_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::clear_thread_local_state();
}

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_utils/lazy_allocator.hpp"
17	#include "crab_verifier.hpp"
18	#include "string_constraints.hpp"
19
20	using std::string;
21
22	namespace prevail {
23	thread_local LazyAllocator<ProgramInfo> thread_local_program_info;
24	thread_local ebpf_verifier_options_t thread_local_options;
25	void ebpf_verifier_clear_before_analysis();
26
27	bool Invariants::is_valid_after(const Label& label, const StringInvariant& state) const {	×
28	const EbpfDomain abstract_state =
29	EbpfDomain::from_constraints(state.value(), thread_local_options.setup_constraints);	×
30	return abstract_state <= invariants.at(label).post;	×
31	}	×
32
33	StringInvariant Invariants::invariant_at(const Label& label) const { return invariants.at(label).post.to_set(); }	1,396✔
34
35	Interval Invariants::exit_value() const { return invariants.at(Label::exit).post.get_r0(); }	438✔
36
37	int Invariants::max_loop_count() const {	×
38	ExtendedNumber max_loop_count{0};	×
39	// Gather the upper bound of loop counts from post-invariants.
40	for (const auto& inv_pair : std::views::values(invariants)) {	×
41	max_loop_count = std::max(max_loop_count, inv_pair.post.get_loop_count_upper_bound());	×
42	}
43	const auto m = max_loop_count.number();	×
44	if (m && m->fits<int32_t>()) {	×
45	return m->cast_to<int32_t>();	×
46	}
47	return std::numeric_limits<int>::max();
48	}	×
49
50	Invariants analyze(const Program& prog, EbpfDomain&& entry_invariant) {	2,502✔
51	return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};	3,753✔
52	}
53
54	Invariants analyze(const Program& prog) {	668✔
55	ebpf_verifier_clear_before_analysis();	668✔
56	return analyze(prog, EbpfDomain::setup_entry(thread_local_options.setup_constraints));	1,001✔
57	}
58
59	Invariants analyze(const Program& prog, const StringInvariant& entry_invariant) {	1,834✔
60	ebpf_verifier_clear_before_analysis();	1,834✔
61	return analyze(prog, EbpfDomain::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));	2,751✔
62	}
63
64	bool Invariants::verified(const Program& prog) const {	1,104✔
65	for (const auto& [label, inv_pair] : invariants) {	171,568✔
66	if (inv_pair.pre.is_bottom()) {	170,532✔
67	continue;	1,486✔
68	}
69	for (const Assertion& assertion : prog.assertions_at(label)) {	312,242✔
70	if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {	143,264✔
71	return false;	68✔
72	}
73	}	169,046✔
74	}
75	return true;	518✔
76	}
77
78	Report Invariants::check_assertions(const Program& prog) const {	1,396✔
79	Report report;	1,396✔
80	for (const auto& [label, inv_pair] : invariants) {	6,794✔
81	if (inv_pair.pre.is_bottom()) {	5,398✔
82	continue;	540✔
83	}
84	for (const Assertion& assertion : prog.assertions_at(label)) {	7,772✔
85	const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);	2,914✔
86	for (const auto& msg : warnings) {	3,294✔
87	report.warnings[label].emplace_back(msg);	380✔
88	}
89	}	7,772✔
90	if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {	7,557✔
91	if (inv_pair.post.is_bottom()) {	560✔
92	const auto s = to_string(*passume);	192✔
93	report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");	384✔
94	}	192✔
95	}
96	}
97	return report;	1,396✔
UNCOV 98	}	×
99
100	void ebpf_verifier_clear_before_analysis() {	2,502✔
101	clear_thread_local_state();	2,502✔
102	Variable::clear_thread_local_state();	2,502✔
103	}	1,251✔
104
UNCOV 105	void ebpf_verifier_clear_thread_local_state() {	×
106	CrabStats::clear_thread_local_state();	×
107	thread_local_program_info.clear();	×
108	clear_thread_local_state();	×
109	SplitDBM::clear_thread_local_state();	×
110	}	×
111	} // namespace prevail

Alan-Jowett / ebpf-verifier / 15194704016

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