14231336081

Committed 02 Apr 2025 11:08PM UTC coverage: 87.272% (-0.9%) from 88.177%

Build # 14231336081

Build Type

push

github

Committed by

web-flow

Commit Message

Propogate ebpf_verifier_options_t to thread_local_options (#856)

Signed-off-by: Alan Jowett <alanjo@microsoft.com>

Run Details

5 of 5 new or added lines in 2 files covered. (100.0%)

58 existing lines in 19 files now uncovered.

8324 of 9538 relevant lines covered (87.27%)

4881701.3 hits per line

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

63.33

/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 crab::ebpf_domain_t;
using std::string;

thread_local crab::lazy_allocator<program_info> 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_t& label, const string_invariant& state) const {
    const ebpf_domain_t abstract_state =
        ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);
    return abstract_state <= invariants.at(label).post;
}

string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }

crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }

int Invariants::max_loop_count() const {
    crab::extended_number 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, ebpf_domain_t&& 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, ebpf_domain_t::setup_entry(thread_local_options.setup_constraints));
}

Invariants analyze(const Program& prog, const string_invariant& entry_invariant) {
    ebpf_verifier_clear_before_analysis();
    return analyze(prog,
                   ebpf_domain_t::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() {
    crab::domains::clear_thread_local_state();
    crab::variable_t::clear_thread_local_state();
}

void ebpf_verifier_clear_thread_local_state() {
    crab::CrabStats::clear_thread_local_state();
    thread_local_program_info.clear();
    crab::domains::clear_thread_local_state();
    crab::domains::SplitDBM::clear_thread_local_state();
}

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 crab::ebpf_domain_t;
21	using std::string;
22
UNCOV 23	thread_local crab::lazy_allocator<program_info> 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_t& label, const string_invariant& state) const {	×
UNCOV 28	const ebpf_domain_t abstract_state =	×
29	ebpf_domain_t::from_constraints(state.value(), thread_local_options.setup_constraints);	×
30	return abstract_state <= invariants.at(label).post;	×
31	}	×
32
33	string_invariant Invariants::invariant_at(const label_t& label) const { return invariants.at(label).post.to_set(); }	693✔
34
35	crab::interval_t Invariants::exit_value() const { return invariants.at(label_t::exit).post.get_r0(); }	219✔
36
37	int Invariants::max_loop_count() const {	×
38	crab::extended_number 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, ebpf_domain_t&& entry_invariant) {	1,246✔
51	return Invariants{run_forward_analyzer(prog, std::move(entry_invariant))};	2,491✔
52	}
53
54	Invariants analyze(const Program& prog) {	334✔
55	ebpf_verifier_clear_before_analysis();	334✔
56	return analyze(prog, ebpf_domain_t::setup_entry(thread_local_options.setup_constraints));	667✔
57	}
58
59	Invariants analyze(const Program& prog, const string_invariant& entry_invariant) {	912✔
60	ebpf_verifier_clear_before_analysis();	912✔
61	return analyze(prog,	912✔
62	ebpf_domain_t::from_constraints(entry_invariant.value(), thread_local_options.setup_constraints));	1,824✔
63	}
64
65	bool Invariants::verified(const Program& prog) const {	552✔
66	for (const auto& [label, inv_pair] : invariants) {	85,784✔
67	if (inv_pair.pre.is_bottom()) {	85,266✔
68	continue;	743✔
69	}
70	for (const Assertion& assertion : prog.assertions_at(label)) {	156,121✔
71	if (!ebpf_domain_check(inv_pair.pre, assertion).empty()) {	71,632✔
72	return false;	34✔
73	}
74	}	84,523✔
75	}
76	return true;
77	}
78
79	Report Invariants::check_assertions(const Program& prog) const {	693✔
80	Report report;	693✔
81	for (const auto& [label, inv_pair] : invariants) {	3,374✔
82	if (inv_pair.pre.is_bottom()) {	2,681✔
83	continue;	270✔
84	}
85	for (const Assertion& assertion : prog.assertions_at(label)) {	3,852✔
86	const auto warnings = ebpf_domain_check(inv_pair.pre, assertion);	1,441✔
87	for (const auto& msg : warnings) {	1,628✔
88	report.warnings[label].emplace_back(msg);	187✔
89	}
90	}	3,852✔
91	if (const auto passume = std::get_if<Assume>(&prog.instruction_at(label))) {	5,092✔
92	if (inv_pair.post.is_bottom()) {	279✔
93	const auto s = to_string(*passume);	96✔
94	report.reachability[label].emplace_back("Code becomes unreachable (" + s + ")");	288✔
95	}	96✔
96	}
97	}
98	return report;	693✔
99	}	×
100
101	void ebpf_verifier_clear_before_analysis() {	1,246✔
102	crab::domains::clear_thread_local_state();	1,246✔
103	crab::variable_t::clear_thread_local_state();	1,246✔
UNCOV 104	}	×
105
106	void ebpf_verifier_clear_thread_local_state() {	×
107	crab::CrabStats::clear_thread_local_state();	×
108	thread_local_program_info.clear();	×
109	crab::domains::clear_thread_local_state();	×
110	crab::domains::SplitDBM::clear_thread_local_state();	×
111	}	×

vbpf / ebpf-verifier / 14231336081

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