Simplify configuration options

src/asm_cfg.cpp

@@ -359,16 +359,14 @@ std::map<std::string, int> collect_stats(const cfg_t& cfg) {
     return res;
 }
 
-// ISSUE: 774 - Rationalize the list of bools being passed to prepare_cfg.
-cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bool simplify,
-                  const bool check_for_termination, const bool must_have_exit) {
+cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const prepare_cfg_options& options) {
     // Convert the instruction sequence to a deterministic control-flow graph.
-    cfg_t det_cfg = instruction_seq_to_cfg(prog, must_have_exit);
+    cfg_t det_cfg = instruction_seq_to_cfg(prog, options.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 (check_for_termination) {
+    if (options.check_for_termination) {
         const wto_t wto(det_cfg);
         wto.for_each_loop_head(
             [&](const label_t& label) { det_cfg.get_node(label).insert_front(IncrementLoopCounter{label}); });
@@ -386,7 +384,7 @@ cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const bo
     // An abstract interpreter will keep values at every basic block,
     // so the fewer basic blocks we have, the less information it has to
     // keep track of.
-    if (simplify) {
+    if (options.simplify) {
         cfg.simplify();
     }
 

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,41 @@
 // 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;
+    // Options that control how the control flow graph is built.
+    prepare_cfg_options cfg_opts;
+
+    // True to assume prior failed assertions are true and continue verification.
+    bool assume_assertions = 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;
+
+    // True to allow division by zero and assume BPF ISA defined semantics.
+    bool allow_division_by_zero = true;
+
+    // Setup the entry constraints for a BPF program.
+    bool setup_constraints = true;
+
+    // True if the ELF file is built on a big endian system.
+    bool big_endian = false;
+
+    // Print the invariants for each basic block.
+    bool print_invariants = false;
+
+    // Print failures that occur during verification.
+    bool print_failures = false;
 
-    bool print_line_info;
-    bool allow_division_by_zero;
-    bool setup_constraints;
-    bool big_endian;
+    // When printing the control flow graph, print the line number of each instruction.
+    bool print_line_info = false;
 
-    bool dump_btf_types_json;
+    // Print the BTF types in JSON format.
+    bool dump_btf_types_json = false;
 };
 
 struct ebpf_verifier_stats_t {
@@ -29,5 +45,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

@@ -613,8 +613,16 @@ std::vector<std::string> stats_headers();
 
 std::map<std::string, int> collect_stats(const cfg_t&);
 
-cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, bool simplify, bool check_for_termination,
-                  bool must_have_exit = true);
+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 = false;
+    /// When true, ensures the program has a valid exit block.
+    bool must_have_exit = true;
+};
+
+cfg_t prepare_cfg(const InstructionSeq& prog, const program_info& info, const prepare_cfg_options& options);
 
 void explicate_assertions(cfg_t& cfg, const program_info& info);
 std::vector<Assert> get_assertions(Instruction ins, const program_info& info, const std::optional<label_t>& label);

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

@@ -124,7 +124,7 @@ class interleaved_fwd_fixpoint_iterator_t final {
 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()) {
@@ -163,12 +163,12 @@ static checks_db get_analysis_report(std::ostream& s, const cfg_t& cfg, const cr
 }
 
 static checks_db get_ebpf_report(std::ostream& s, const cfg_t& cfg, program_info info,
-                                 const ebpf_verifier_options_t* options,
+                                 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.
@@ -185,10 +185,7 @@ 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;
-    }
+                       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;
@@ -221,7 +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, options.simplify, options.check_termination, 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);
@@ -237,23 +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, options->simplify, 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;
@@ -235,9 +235,9 @@ int main(int argc, char** argv) {
     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";
         }
@@ -250,8 +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, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination);
+        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);
@@ -265,8 +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, ebpf_verifier_options.simplify, ebpf_verifier_options.check_termination);
+        const cfg_t cfg = prepare_cfg(prog, raw_prog.info, ebpf_verifier_options.cfg_opts);
         std::cout << cfg;
         std::cout << "\n";
     } else {