diff --git a/src/asm_cfg.cpp b/src/asm_cfg.cpp index acbbc169f..298da1207 100644 --- a/src/asm_cfg.cpp +++ b/src/asm_cfg.cpp @@ -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}); diff --git a/src/main/check.cpp b/src/main/check.cpp index 0d46ea2f3..3c4e3708e 100644 --- a/src/main/check.cpp +++ b/src/main/check.cpp @@ -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; @@ -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); diff --git a/src/program.hpp b/src/program.hpp index 2d8806311..06f97f088 100644 --- a/src/program.hpp +++ b/src/program.hpp @@ -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 { diff --git a/src/test/ebpf_yaml.cpp b/src/test/ebpf_yaml.cpp index afeef3846..a2273778e 100644 --- a/src/test/ebpf_yaml.cpp +++ b/src/test/ebpf_yaml.cpp @@ -245,7 +245,7 @@ std::optional 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 actual_messages = invariants.check_assertions(prog).all_messages(); @@ -362,10 +362,9 @@ ConformanceTestResult run_conformance_test_case(const std::vector& 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&) { diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp index 5fe19028f..45f6d467e 100644 --- a/src/test/test_verify.cpp +++ b/src/test/test_verify.cpp @@ -41,27 +41,27 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text") std::variant prog_or_error = unmarshal(raw_prog); \ const auto inst_seq = std::get_if(&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(&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(&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.