Skip to content

Propogate ebpf_verifier_options_t to thread_local_options #856

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
elazarg merged 2 commits into from
Apr 2, 2025
Merged

Propogate ebpf_verifier_options_t to thread_local_options #856

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
894ab61
Propogate ebpf_verifier_options_t to thread_local_options
Alan-Jowett Apr 1, 2025
ab247f4
Merge branch 'vbpf:main' into issue855
Alan-Jowett Apr 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions src/asm_cfg.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,16 +290,17 @@ static cfg_builder_t instruction_seq_to_cfg(const InstructionSeq& insts, const b
}

Program Program::from_sequence(const InstructionSeq& inst_seq, const program_info& info,
const prepare_cfg_options& options) {
const ebpf_verifier_options_t& options) {
thread_local_program_info.set(info);
thread_local_options = options;

// Convert the instruction sequence to a deterministic control-flow graph.
cfg_builder_t builder = instruction_seq_to_cfg(inst_seq, options.must_have_exit);
cfg_builder_t builder = instruction_seq_to_cfg(inst_seq, options.cfg_opts.must_have_exit);

// Detect loops using Weak Topological Ordering (WTO) and insert counters at loop entry points. WTO provides a
// hierarchical decomposition of the CFG that identifies all strongly connected components (cycles) and their entry
// points. These entry points serve as natural locations for loop counters that help verify program termination.
if (options.check_for_termination) {
if (options.cfg_opts.check_for_termination) {
const crab::wto_t wto{builder.prog.cfg()};
wto.for_each_loop_head([&](const label_t& label) -> void {
builder.insert_after(label, label_t::make_increment_counter(label), IncrementLoopCounter{label});
Expand Down
4 changes: 2 additions & 2 deletions src/main/check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ int main(int argc, char** argv) {
// Convert the instruction sequence to a control-flow graph.
try {
const auto verbosity = ebpf_verifier_options.verbosity_opts;
const Program prog = Program::from_sequence(inst_seq, raw_prog.info, ebpf_verifier_options.cfg_opts);
const Program prog = Program::from_sequence(inst_seq, raw_prog.info, ebpf_verifier_options);
if (domain == "cfg") {
print_program(prog, std::cout, verbosity.simplify);
return 0;
Expand Down Expand Up @@ -277,7 +277,7 @@ int main(int argc, char** argv) {
return !res;
} else if (domain == "stats") {
// Convert the instruction sequence to a control-flow graph.
const Program prog = Program::from_sequence(inst_seq, raw_prog.info, ebpf_verifier_options.cfg_opts);
const Program prog = Program::from_sequence(inst_seq, raw_prog.info, ebpf_verifier_options);

// Just print eBPF program stats.
auto stats = collect_stats(prog);
Expand Down
2 changes: 1 addition & 1 deletion src/program.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ class Program {
}

static Program from_sequence(const InstructionSeq& inst_seq, const program_info& info,
const prepare_cfg_options& options);
const ebpf_verifier_options_t& options);
};

class InvalidControlFlow final : public std::runtime_error {
Expand Down
5 changes: 2 additions & 3 deletions src/test/ebpf_yaml.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
program_info info{&g_platform_test, {}, program_type};
thread_local_options = test_case.options;
try {
const Program prog = Program::from_sequence(test_case.instruction_seq, info, test_case.options.cfg_opts);
const Program prog = Program::from_sequence(test_case.instruction_seq, info, test_case.options);
const Invariants invariants = analyze(prog, test_case.assumed_pre_invariant);
const string_invariant actual_last_invariant = invariants.invariant_at(label_t::exit);
const std::set<string> actual_messages = invariants.check_assertions(prog).all_messages();
Expand Down Expand Up @@ -362,10 +362,9 @@ ConformanceTestResult run_conformance_test_case(const std::vector<std::byte>& me
options.verbosity_opts.print_invariants = true;
options.verbosity_opts.simplify = false;
}
thread_local_options = options;

try {
const Program prog = Program::from_sequence(inst_seq, info, options.cfg_opts);
const Program prog = Program::from_sequence(inst_seq, info, options);
const Invariants invariants = analyze(prog, pre_invariant);
return ConformanceTestResult{.success = invariants.verified(prog), .r0_value = invariants.exit_value()};
} catch (const std::exception&) {
Expand Down
30 changes: 15 additions & 15 deletions src/test/test_verify.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,27 +41,27 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text")
std::variant<InstructionSeq, std::string> prog_or_error = unmarshal(raw_prog); \
const auto inst_seq = std::get_if<InstructionSeq>(&prog_or_error); \
REQUIRE(inst_seq != nullptr); \
Program prog = Program::from_sequence(*inst_seq, raw_prog.info, thread_local_options.cfg_opts); \
Program prog = Program::from_sequence(*inst_seq, raw_prog.info, thread_local_options); \
REQUIRE_THROWS_AS(analyze(prog), UnmarshalError); \
}

FAIL_ANALYZE("build", "badmapptr.o", "test")

// Verify a program in a section that may have multiple programs in it.
#define VERIFY_PROGRAM(dirname, filename, section_name, program_name, _options, platform, should_pass, count) \
do { \
thread_local_options = _options; \
const auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, section_name, {}, platform); \
REQUIRE(raw_progs.size() == count); \
for (const auto& raw_prog : raw_progs) { \
if (count == 1 || raw_prog.function_name == program_name) { \
const auto prog_or_error = unmarshal(raw_prog); \
const auto inst_seq = std::get_if<InstructionSeq>(&prog_or_error); \
REQUIRE(inst_seq != nullptr); \
const Program prog = Program::from_sequence(*inst_seq, raw_prog.info, thread_local_options.cfg_opts); \
REQUIRE(verify(prog) == should_pass); \
} \
} \
#define VERIFY_PROGRAM(dirname, filename, section_name, program_name, _options, platform, should_pass, count) \
do { \
thread_local_options = _options; \
const auto raw_progs = read_elf("ebpf-samples/" dirname "/" filename, section_name, {}, platform); \
REQUIRE(raw_progs.size() == count); \
for (const auto& raw_prog : raw_progs) { \
if (count == 1 || raw_prog.function_name == program_name) { \
const auto prog_or_error = unmarshal(raw_prog); \
const auto inst_seq = std::get_if<InstructionSeq>(&prog_or_error); \
REQUIRE(inst_seq != nullptr); \
const Program prog = Program::from_sequence(*inst_seq, raw_prog.info, thread_local_options); \
REQUIRE(verify(prog) == should_pass); \
} \
} \
} while (0)

// Verify a section with only one program in it.
Expand Down