More options cleanup

Signed-off-by: Alan Jowett <[email protected]>

src/asm_files.cpp

@@ -88,7 +88,7 @@ static std::tuple<ELFIO::Elf64_Addr, unsigned char> get_value(const ELFIO::const
 
 // parse_maps_sections processes all maps sections in the provided ELF file by calling the platform-specific maps'
 // parser. The section index of each maps section is inserted into section_indices.
-static size_t parse_map_sections(const ebpf_verifier_options_t* options, const ebpf_platform_t* platform,
+static size_t parse_map_sections(const ebpf_verifier_options_t& options, const ebpf_platform_t* platform,
                                  const ELFIO::elfio& reader, vector<EbpfMapDescriptor>& map_descriptors,
                                  std::set<ELFIO::Elf_Half>& section_indices,
                                  const ELFIO::const_symbol_section_accessor& symbols) {
@@ -116,16 +116,15 @@ static size_t parse_map_sections(const ebpf_verifier_options_t* options, const e
             if (s->get_size() % map_record_size != 0) {
                 throw std::runtime_error("bad maps section size");
             }
-            platform->parse_maps_section(map_descriptors, s->get_data(), map_record_size, map_count, platform,
-                                         *options);
+            platform->parse_maps_section(map_descriptors, s->get_data(), map_record_size, map_count, platform, options);
         }
         section_indices.insert(s->get_index());
     }
     platform->resolve_inner_map_references(map_descriptors);
     return map_record_size;
 }
 
-vector<raw_program> read_elf(const string& path, const string& desired_section, const ebpf_verifier_options_t* options,
+vector<raw_program> read_elf(const string& path, const string& desired_section, const ebpf_verifier_options_t& options,
                              const ebpf_platform_t* platform) {
     if (std::ifstream stream{path, std::ios::in | std::ios::binary}) {
         return read_elf(stream, path, desired_section, options, platform);
@@ -280,10 +279,7 @@ std::map<std::string, size_t> parse_map_section(const libbtf::btf_type_data& btf
 }
 
 vector<raw_program> read_elf(std::istream& input_stream, const std::string& path, const std::string& desired_section,
-                             const ebpf_verifier_options_t* options, const ebpf_platform_t* platform) {
-    if (options == nullptr) {
-        options = &ebpf_verifier_default_options;
-    }
+                             const ebpf_verifier_options_t& options, const ebpf_platform_t* platform) {
     ELFIO::elfio reader;
     if (!reader.load(input_stream)) {
         throw std::runtime_error("Can't process ELF file " + path);
@@ -311,7 +307,7 @@ vector<raw_program> read_elf(std::istream& input_stream, const std::string& path
     if (btf) {
         // Parse the BTF type data.
         btf_data = vector_of<std::byte>(*btf);
-        if (options->dump_btf_types_json) {
+        if (options.dump_btf_types_json) {
             std::stringstream output;
             std::cout << "Dumping BTF data for" << path << std::endl;
             // Dump the BTF data to cout for debugging purposes.

src/asm_files.hpp

@@ -11,9 +11,9 @@
 
 std::vector<raw_program> read_raw(std::string path, program_info info);
 std::vector<raw_program> read_elf(const std::string& path, const std::string& desired_section,
-                                  const ebpf_verifier_options_t* options, const ebpf_platform_t* platform);
+                                  const ebpf_verifier_options_t& options, const ebpf_platform_t* platform);
 std::vector<raw_program> read_elf(std::istream& input_stream, const std::string& path,
-                                  const std::string& desired_section, const ebpf_verifier_options_t* options,
+                                  const std::string& desired_section, const ebpf_verifier_options_t& options,
                                   const ebpf_platform_t* platform);
 
 void write_binary_file(std::string path, const char* data, size_t size);

src/config.hpp

@@ -2,25 +2,26 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
+#include "crab/cfg.hpp"
+
 struct ebpf_verifier_options_t {
-    bool check_termination;
-    bool assume_assertions;
-    bool print_invariants;
-    bool print_failures;
-    bool simplify;
+    prepare_cfg_options cfg_opts;
+    bool assume_assertions = false;
+    bool print_invariants = false;
+    bool print_failures = false;
 
     // False to use actual map fd's, true to use mock fd's.
-    bool mock_map_fds;
+    bool mock_map_fds = true;
 
     // True to do additional checks for some things that would fail at runtime.
-    bool strict;
+    bool strict = false;
 
-    bool print_line_info;
-    bool allow_division_by_zero;
-    bool setup_constraints;
-    bool big_endian;
+    bool print_line_info = false;
+    bool allow_division_by_zero = true;
+    bool setup_constraints = true;
+    bool big_endian = false;
 
-    bool dump_btf_types_json;
+    bool dump_btf_types_json = false;
 };
 
 struct ebpf_verifier_stats_t {
@@ -29,5 +30,4 @@ struct ebpf_verifier_stats_t {
     int max_loop_count;
 };
 
-extern const ebpf_verifier_options_t ebpf_verifier_default_options;
 extern thread_local ebpf_verifier_options_t thread_local_options;

src/crab/cfg.hpp

@@ -623,7 +623,7 @@ struct prepare_cfg_options {
     /// When true, simplifies the control flow graph by merging basic blocks.
     bool simplify = true;
     /// When true, verifies that the program terminates.
-    bool check_for_termination = true;
+    bool check_for_termination = false;
     /// When true, ensures the program has a valid exit block.
     bool must_have_exit = true;
 };

src/crab/ebpf_domain.cpp

@@ -825,7 +825,7 @@ ebpf_domain_t ebpf_domain_t::calculate_constant_limits() {
         inv += r.shared_offset >= 0;
         inv += r.packet_offset <= variable_t::packet_size();
         inv += r.packet_offset >= 0;
-        if (thread_local_options.check_termination) {
+        if (thread_local_options.cfg_opts.check_for_termination) {
             for (const variable_t counter : variable_t::get_loop_counters()) {
                 inv += counter <= std::numeric_limits<int32_t>::max();
                 inv += counter >= 0;

src/crab/fwd_analyzer.cpp

@@ -116,13 +116,14 @@ class interleaved_fwd_fixpoint_iterator_t final {
 
     void operator()(const std::shared_ptr<wto_cycle_t>& cycle);
 
-    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv);
+    friend std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg,
+                                                                                ebpf_domain_t entry_inv);
 };
 
 std::pair<invariant_table_t, invariant_table_t> run_forward_analyzer(const cfg_t& cfg, ebpf_domain_t entry_inv) {
     // Go over the CFG in weak topological order (accounting for loops).
     interleaved_fwd_fixpoint_iterator_t analyzer(cfg);
-    if (thread_local_options.check_termination) {
+    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.

src/crab_verifier.cpp

@@ -94,7 +94,7 @@ static checks_db generate_report(const cfg_t& cfg, const crab::invariant_table_t
         }
     }
 
-    if (thread_local_options.check_termination) {
+    if (thread_local_options.cfg_opts.check_for_termination) {
         // Gather the upper bound of loop counts from post-invariants.
         for (const auto [label, inv] : post_invariants) {
             if (inv.is_bottom()) {
@@ -162,12 +162,13 @@ static checks_db get_analysis_report(std::ostream& s, const cfg_t& cfg, const cr
     return db;
 }
 
-static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info, const ebpf_verifier_options_t* options,
+static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info,
+                                 const ebpf_verifier_options_t& options,
                                  const std::optional<InstructionSeq>& prog = std::nullopt) {
     global_program_info = std::move(info);
     crab::domains::clear_global_state();
     crab::variable_t::clear_thread_local_state();
-    thread_local_options = *options;
+    thread_local_options = options;
 
     try {
         // Get dictionaries of pre-invariants and post-invariants for each basic block.
@@ -183,11 +184,8 @@ static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info
 }
 
 /// Returned value is true if the program passes verification.
-bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
-                       ebpf_verifier_stats_t* stats) {
-    if (options == nullptr) {
-        options = &ebpf_verifier_default_options;
-    }
+bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info,
+                       const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats) {
     const checks_db report = get_ebpf_report(s, cfg, info, options);
     if (stats) {
         stats->total_unreachable = report.total_unreachable;
@@ -220,10 +218,7 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
         throw std::runtime_error("Entry invariant is inconsistent");
     }
     try {
-        const cfg_t cfg = prepare_cfg(prog, info,
-                                      {.simplify = options.simplify,
-                                       .check_for_termination = options.check_termination,
-                                       .must_have_exit = false});
+        const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts);
         auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv));
         const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
         print_report(os, report, prog, false);
@@ -239,24 +234,19 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
 
 /// Returned value is true if the program passes verification.
 bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info,
-                         const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats) {
-    if (options == nullptr) {
-        options = &ebpf_verifier_default_options;
-    }
-
+                         const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats) {
     // Convert the instruction sequence to a control-flow graph
     // in a "passive", non-deterministic form.
-    const cfg_t cfg =
-        prepare_cfg(prog, info, {.simplify = options->simplify, .check_for_termination = options->check_termination});
+    const cfg_t cfg = prepare_cfg(prog, info, options.cfg_opts);
 
     std::optional<InstructionSeq> prog_opt = std::nullopt;
-    if (options->print_failures) {
+    if (options.print_failures) {
         prog_opt = prog;
     }
 
     const checks_db report = get_ebpf_report(os, cfg, info, options, prog_opt);
-    if (options->print_failures) {
-        print_report(os, report, prog, options->print_line_info);
+    if (options.print_failures) {
+        print_report(os, report, prog, options.print_line_info);
     }
     if (stats) {
         stats->total_unreachable = report.total_unreachable;

src/crab_verifier.hpp

@@ -7,11 +7,11 @@
 #include "spec_type_descriptors.hpp"
 #include "string_constraints.hpp"
 
-bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info, const ebpf_verifier_options_t* options,
-                       ebpf_verifier_stats_t* stats);
+bool run_ebpf_analysis(std::ostream& s, const cfg_t& cfg, const program_info& info,
+                       const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats);
 
 bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const program_info& info,
-                         const ebpf_verifier_options_t* options, ebpf_verifier_stats_t* stats);
+                         const ebpf_verifier_options_t& options, ebpf_verifier_stats_t* stats);
 
 using string_invariant_map = std::map<label_t, string_invariant>;
 

src/main/check.cpp

@@ -70,7 +70,7 @@ int main(int argc, char** argv) {
     // Always call ebpf_verifier_clear_thread_local_state on scope exit.
     at_scope_exit<ebpf_verifier_clear_thread_local_state> clear_thread_local_state;
 
-    ebpf_verifier_options_t ebpf_verifier_options = ebpf_verifier_default_options;
+    ebpf_verifier_options_t ebpf_verifier_options;
 
     crab::CrabEnableWarningMsg(false);
 
@@ -97,7 +97,7 @@ int main(int argc, char** argv) {
         ->capture_default_str()
         ->check(CLI::IsMember({"stats", "linux", "zoneCrab", "cfg"}));
 
-    app.add_flag("--termination,!--no-verify-termination", ebpf_verifier_options.check_termination,
+    app.add_flag("--termination,!--no-verify-termination", ebpf_verifier_options.cfg_opts.check_for_termination,
                  "Verify termination. Default: ignore")
         ->group("Features");
 
@@ -124,7 +124,7 @@ int main(int argc, char** argv) {
         ->expected(0, _conformance_groups.size())
         ->check(CLI::IsMember(_get_conformance_group_names()));
 
-    app.add_flag("--simplify,!--no-simplify", ebpf_verifier_options.simplify,
+    app.add_flag("--simplify,!--no-simplify", ebpf_verifier_options.cfg_opts.simplify,
                  "Simplify the CFG before analysis by merging chains of instructions into a single basic block. "
                  "Default: enabled")
         ->group("Verbosity");
@@ -193,7 +193,7 @@ int main(int argc, char** argv) {
     // Read a set of raw program sections from an ELF file.
     vector<raw_program> raw_progs;
     try {
-        raw_progs = read_elf(filename, desired_section, &ebpf_verifier_options, &platform);
+        raw_progs = read_elf(filename, desired_section, ebpf_verifier_options, &platform);
     } catch (std::runtime_error& e) {
         std::cerr << "error: " << e.what() << std::endl;
         return 1;
@@ -208,7 +208,7 @@ int main(int argc, char** argv) {
         if (!desired_section.empty() && raw_progs.empty()) {
             // We could not find the desired program, so get the full list
             // of possibilities.
-            raw_progs = read_elf(filename, string(), &ebpf_verifier_options, &platform);
+            raw_progs = read_elf(filename, string(), ebpf_verifier_options, &platform);
         }
         for (const raw_program& raw_prog : raw_progs) {
             std::cout << "section=" << raw_prog.section_name << " function=" << raw_prog.function_name << std::endl;
@@ -232,15 +232,12 @@ int main(int argc, char** argv) {
         print_map_descriptors(global_program_info->map_descriptors, out);
     }
 
-    prepare_cfg_options cfg_options = {.simplify = ebpf_verifier_options.simplify,
-                                       .check_for_termination = ebpf_verifier_options.check_termination};
-
     if (domain == "zoneCrab") {
         ebpf_verifier_stats_t verifier_stats;
         const auto [res, seconds] = timed_execution([&] {
-            return ebpf_verify_program(std::cout, prog, raw_prog.info, &ebpf_verifier_options, &verifier_stats);
+            return ebpf_verify_program(std::cout, prog, raw_prog.info, ebpf_verifier_options, &verifier_stats);
         });
-        if (res && ebpf_verifier_options.check_termination &&
+        if (res && ebpf_verifier_options.cfg_opts.check_for_termination &&
             (ebpf_verifier_options.print_failures || ebpf_verifier_options.print_invariants)) {
             std::cout << "Program terminates within " << verifier_stats.max_loop_count << " loop iterations\n";
         }
@@ -253,7 +250,7 @@ int main(int argc, char** argv) {
         return !res;
     } else if (domain == "stats") {
         // Convert the instruction sequence to a control-flow graph.
-        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, cfg_options);
+        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts);
 
         // Just print eBPF program stats.
         auto stats = collect_stats(cfg);
@@ -267,7 +264,7 @@ int main(int argc, char** argv) {
         std::cout << "\n";
     } else if (domain == "cfg") {
         // Convert the instruction sequence to a control-flow graph.
-        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, cfg_options);
+        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts);
         std::cout << cfg;
         std::cout << "\n";
     } else {

src/test/ebpf_yaml.cpp

@@ -168,10 +168,10 @@ static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string,
 }
 
 static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& raw_options) {
-    ebpf_verifier_options_t options = ebpf_verifier_default_options;
+    ebpf_verifier_options_t options;
 
     // Use ~simplify for YAML tests unless otherwise specified.
-    options.simplify = false;
+    options.cfg_opts.simplify = false;
 
     // All YAML tests use !setup_constraints.
     options.setup_constraints = false;
@@ -182,15 +182,18 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& ra
     // Default to not assuming assertions.
     options.assume_assertions = false;
 
+    // Permit test cases to not have an exit instruction.
+    options.cfg_opts.must_have_exit = false;
+
     for (const string& name : raw_options) {
         if (name == "!allow_division_by_zero") {
             options.allow_division_by_zero = false;
         } else if (name == "termination") {
-            options.check_termination = true;
+            options.cfg_opts.check_for_termination = true;
         } else if (name == "strict") {
             options.strict = true;
         } else if (name == "simplify") {
-            options.simplify = true;
+            options.cfg_opts.simplify = true;
         } else if (name == "big_endian") {
             options.big_endian = true;
         } else if (name == "!big_endian") {
@@ -248,7 +251,7 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
     if (debug) {
         test_case.options.print_failures = true;
         test_case.options.print_invariants = true;
-        test_case.options.simplify = false;
+        test_case.options.cfg_opts.simplify = false;
     }
 
     ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};
@@ -352,12 +355,12 @@ ConformanceTestResult run_conformance_test_case(const std::vector<std::byte>& me
 
     auto& prog = std::get<InstructionSeq>(prog_or_error);
 
-    ebpf_verifier_options_t options = ebpf_verifier_default_options;
+    ebpf_verifier_options_t options;
     if (debug) {
         print(prog, std::cout, {});
         options.print_failures = true;
         options.print_invariants = true;
-        options.simplify = false;
+        options.cfg_opts.simplify = false;
     }
 
     try {