WIP 8 - Make partition variable a list

Signed-off-by: Alan Jowett <[email protected]>
Alan-Jowett · Jun 1, 2024 · cbb7370 · cbb7370
1 parent 652b856
commit cbb7370
Show file tree

Hide file tree

Showing 12 changed files with 187 additions and 42 deletions.
diff --git a/ebpf-samples b/ebpf-samples
diff --git a/src/config.cpp b/src/config.cpp
@@ -14,5 +14,4 @@ const ebpf_verifier_options_t ebpf_verifier_default_options = {
     .allow_division_by_zero = true,
     .setup_constraints = true,
     .big_endian = false,
-    .use_value_partitioning = true,
 };
diff --git a/src/config.hpp b/src/config.hpp
@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: MIT
 #pragma once
 
+#include <string>
+#include <vector>
+
 struct ebpf_verifier_options_t {
     bool check_termination;
     bool assume_assertions;
@@ -21,7 +24,7 @@ struct ebpf_verifier_options_t {
     bool big_endian;
 
     bool dump_btf_types_json;
-    bool use_value_partitioning;
+    std::vector<std::string> partition_keys;
 };
 
 struct ebpf_verifier_stats_t {

diff --git a/src/crab/ebpf_value_partition_domain.cpp b/src/crab/ebpf_value_partition_domain.cpp
@@ -23,8 +23,6 @@
 
 namespace crab {
 
-static std::string partition_key = "packet_size";
-
 ebpf_value_partition_domain_t::ebpf_value_partition_domain_t() : partitions(1) {}
 ebpf_value_partition_domain_t::ebpf_value_partition_domain_t(crab::domains::NumAbsDomain inv,
                                                              crab::domains::array_domain_t stack)
@@ -98,42 +96,25 @@ ebpf_value_partition_domain_t ebpf_value_partition_domain_t::join(const ebpf_val
     // For some reason, the <= operator on is not valid for sort, so we need to use a lambda and explicitly specify the
     // ordering predicate.
     std::sort(partitions.begin(), partitions.end(), [](const auto& lhs, const auto& rhs) {
-        auto lhs_interval = lhs.m_inv[variable_t::make(partition_key)];
-        auto rhs_interval = rhs.m_inv[variable_t::make(partition_key)];
-
-        if (lhs_interval.is_bottom()) {
-            return false;
-        }
-        if (rhs_interval.is_bottom()) {
-            return true;
-        }
-
-        if (lhs_interval.lb() < rhs_interval.lb()) {
-            return true;
-        } else if (lhs_interval.lb() > rhs_interval.lb()) {
-            return false;
-        } else {
-            return lhs_interval.ub() < rhs_interval.ub();
-        }
+        return compare_partitions(lhs, rhs) == partition_comparison_t::LESS_THAN;
     });
 
     // Perform a single pass over the partitions to merge them.
     // Partitions are sorted by packet size interval, so we can merge adjacent partitions.
     // If the packet size interval is different, we start a new partition.
     std::vector<ebpf_domain_t> merged_partitions;
 
-    // First partition is always added.
-    auto packet_size_interval = partitions[0].m_inv[variable_t::make(partition_key)];
-    merged_partitions.push_back(std::move(partitions[0]));
+    // Start with the first partition.
+    auto current_partition = 0;
+    merged_partitions.push_back(partitions[current_partition]);
 
     for (size_t i = 1; i < partitions.size(); i++) {
-        if (partitions[i].m_inv[variable_t::make(partition_key)] == packet_size_interval) {
+        if (compare_partitions(partitions[i], merged_partitions.back()) == partition_comparison_t::EQUAL) {
             // This partition has the same packet size interval as the previous one, merge them.
             merged_partitions.back() |= partitions[i];
         } else {
-            // This partition has a different packet size interval, add it to the list.
-            packet_size_interval = partitions[i].m_inv[variable_t::make(partition_key)];
-            merged_partitions.push_back(std::move(partitions[i]));
+            // Start a new partition.
+            merged_partitions.push_back(partitions[i]);
         }
     }
 
@@ -157,7 +138,8 @@ ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& ot
     return join(*this, other);
 }
 
-ebpf_value_partition_domain_t ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& other) const && {
+ebpf_value_partition_domain_t
+ebpf_value_partition_domain_t::operator|(const ebpf_value_partition_domain_t& other) const&& {
     return std::move(join(*this, other));
 }
 
@@ -222,9 +204,6 @@ string_invariant ebpf_value_partition_domain_t::to_set() {
 }
 
 void ebpf_value_partition_domain_t::initialize_loop_counter(label_t label) {
-    // Do we really need to merge all partitions here?
-    merge_all_partitions();
-
     for (auto& partition : partitions) {
         partition.initialize_loop_counter(label);
     }
@@ -263,7 +242,7 @@ bool ebpf_value_partition_domain_t::has_same_partitions(const ebpf_value_partiti
     }
 
     for (size_t i = 0; i < partitions.size(); i++) {
-        if (partitions[i].m_inv[variable_t::make(partition_key)] != other.partitions[i].m_inv[variable_t::make(partition_key)]) {
+        if (compare_partitions(partitions[i], other.partitions[i]) != partition_comparison_t::EQUAL) {
             return false;
         }
     }
@@ -288,4 +267,37 @@ void ebpf_value_partition_domain_t::merge_or_apply_to_all_partitions(
     }
 }
 
+ebpf_value_partition_domain_t::partition_comparison_t
+ebpf_value_partition_domain_t::compare_partitions(const ebpf_domain_t& lhs, const ebpf_domain_t& rhs) {
+    if (!partition_keys.has_value()) {
+        return partition_comparison_t::EQUAL;
+    }
+    // Loop over the partition key and compare each the corresponding interval in the two partitions.
+    for (const auto& partition_key : partition_keys.value()) {
+        auto lhs_interval = lhs.m_inv[variable_t::make(partition_key)];
+        auto rhs_interval = rhs.m_inv[variable_t::make(partition_key)];
+
+        if (lhs_interval.is_bottom()) {
+            if (!rhs_interval.is_bottom()) {
+                return partition_comparison_t::LESS_THAN;
+            }
+        } else if (rhs_interval.is_bottom()) {
+            return partition_comparison_t::GREATER_THAN;
+        } else {
+            if (lhs_interval.lb() < rhs_interval.lb()) {
+                return partition_comparison_t::LESS_THAN;
+            } else if (lhs_interval.lb() > rhs_interval.lb()) {
+                return partition_comparison_t::GREATER_THAN;
+            } else {
+                if (lhs_interval.ub() < rhs_interval.ub()) {
+                    return partition_comparison_t::LESS_THAN;
+                } else if (lhs_interval.ub() > rhs_interval.ub()) {
+                    return partition_comparison_t::GREATER_THAN;
+                }
+            }
+        }
+    }
+    return partition_comparison_t::EQUAL;
+}
+
 } // namespace crab
diff --git a/src/crab/ebpf_value_partition_domain.hpp b/src/crab/ebpf_value_partition_domain.hpp
@@ -31,6 +31,9 @@ class ebpf_value_partition_domain_t {
     ebpf_value_partition_domain_t(ebpf_domain_t ebpf_domain);
     ebpf_value_partition_domain_t(std::vector<ebpf_domain_t>&& partitions);
 
+    static void set_partition_keys(const std::vector<std::string>& keys) { partition_keys = {keys}; }
+    static void clear_partition_keys() { partition_keys.reset(); }
+
     // Generic abstract domain operations
     static ebpf_value_partition_domain_t top();
     static ebpf_value_partition_domain_t bottom();
@@ -130,7 +133,24 @@ class ebpf_value_partition_domain_t {
     void merge_or_apply_to_all_partitions(const ebpf_value_partition_domain_t& other,
                                           std::function<void(const ebpf_domain_t&, const ebpf_domain_t&)> f) const;
 
+
+    enum class partition_comparison_t {
+        LESS_THAN,
+        EQUAL,
+        GREATER_THAN,
+    };
+
+    /**
+     * @brief Compare two partitions based on the partition keys.
+     *
+     * @param[in] lhs Left-hand side of the comparison.
+     * @param[in] rhs Right-hand side of the comparison.
+     * @return partition_comparison_t The result of the comparison.
+     */
+    static partition_comparison_t compare_partitions(const ebpf_domain_t& lhs, const ebpf_domain_t& rhs);
+
     std::vector<ebpf_domain_t> partitions;
+    inline static thread_local std::optional<std::vector<std::string>> partition_keys = {};
 };
 
 } // namespace crab
diff --git a/src/crab_verifier.cpp b/src/crab_verifier.cpp
@@ -219,7 +219,8 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
                                                                  const program_info& info,
                                                                  const ebpf_verifier_options_t& options)
 {
-    if (options.use_value_partitioning) {
+    if (!options.partition_keys.empty()) {
+        ebpf_value_partition_domain_t::set_partition_keys(options.partition_keys);
         return ebpf_analyze_program_for_test_variant<ebpf_value_partition_domain_t>(os, prog, entry_invariant, info, options);
     }
     else {
@@ -239,7 +240,8 @@ bool ebpf_verify_program(std::ostream& os, const InstructionSeq& prog, const pro
     cfg_t cfg = prepare_cfg(prog, info, !options->no_simplify);
 
     checks_db report;
-    if (options->use_value_partitioning) {
+    if (!options->partition_keys.empty()) {
+        ebpf_value_partition_domain_t::set_partition_keys(options->partition_keys);
         report = get_ebpf_report<ebpf_value_partition_domain_t>(os, cfg, info, options);
     }
     else {
@@ -263,4 +265,5 @@ void ebpf_verifier_clear_thread_local_state() {
     global_program_info.clear();
     crab::domains::clear_thread_local_state();
     crab::domains::SplitDBM::clear_thread_local_state();
+    crab::ebpf_value_partition_domain_t::clear_partition_keys();
 }
diff --git a/src/ebpf_yaml.cpp b/src/ebpf_yaml.cpp
@@ -106,6 +106,7 @@ struct RawTestCase {
     vector<std::tuple<string, vector<string>>> raw_blocks;
     vector<string> post;
     std::set<string> messages;
+    vector<string> partition_keys;
 };
 
 static vector<string> parse_block(const YAML::Node& block_node) {
@@ -139,6 +140,7 @@ static RawTestCase parse_case(const YAML::Node& case_node) {
         .raw_blocks = parse_code(case_node["code"]),
         .post = case_node["post"].as<vector<string>>(),
         .messages = as_set_empty_default(case_node["messages"]),
+        .partition_keys = case_node["partition_keys"].IsDefined() ? case_node["partition_keys"].as<vector<string>>() : vector<string>(),
     };
 }
 
@@ -206,7 +208,8 @@ static TestCase read_case(const RawTestCase& raw_case) {
         .assumed_pre_invariant = read_invariant(raw_case.pre),
         .instruction_seq = raw_cfg_to_instruction_seq(raw_case.raw_blocks),
         .expected_post_invariant = read_invariant(raw_case.post),
-        .expected_messages = raw_case.messages
+        .expected_messages = raw_case.messages,
+        .partition_keys = raw_case.partition_keys,
     };
 }
 
@@ -247,6 +250,8 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
         test_case.options.no_simplify = true;
     }
 
+    test_case.options.partition_keys = test_case.partition_keys;
+
     ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};
     EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);
 

diff --git a/src/ebpf_yaml.hpp b/src/ebpf_yaml.hpp
@@ -14,6 +14,7 @@ struct TestCase {
     InstructionSeq instruction_seq;
     string_invariant expected_post_invariant;
     std::set<std::string> expected_messages;
+    std::vector<std::string> partition_keys;
 };
 
 void foreach_suite(const std::string& path, const std::function<void(const TestCase&)>& f);

diff --git a/src/main/check.cpp b/src/main/check.cpp
@@ -132,6 +132,9 @@ int main(int argc, char** argv) {
     app.add_flag("--line-info", ebpf_verifier_options.print_line_info, "Print line information");
     app.add_flag("--print-btf-types", ebpf_verifier_options.dump_btf_types_json, "Print BTF types");
 
+    std::string partition_variable;
+    app.add_option("--partition-variable", partition_variable, "Partition variable")->type_name("VARIABLE");
+
     std::string asmfile;
     app.add_option("--asm", asmfile, "Print disassembly to FILE")->type_name("FILE");
     std::string dotfile;
@@ -144,6 +147,11 @@ int main(int argc, char** argv) {
         ebpf_verifier_options.print_invariants = ebpf_verifier_options.print_failures = true;
     ebpf_verifier_options.allow_division_by_zero = !no_division_by_zero;
 
+    if (!partition_variable.empty()) {
+        // partition_variable is a comma-separated list of variables.
+        boost::split(ebpf_verifier_options.partition_keys, partition_variable, boost::is_any_of(","));
+    }
+
     // Enable default conformance groups, which don't include callx or packet.
     ebpf_platform_t platform = g_ebpf_platform_linux;
     platform.supported_conformance_groups = bpf_conformance_groups_t::default_groups;

diff --git a/src/test/test_verify.cpp b/src/test/test_verify.cpp
@@ -71,6 +71,13 @@ FAIL_UNMARSHAL("invalid", "invalid-lddw.o", ".text")
         VERIFY_SECTION(project, filename, section, nullptr, &g_ebpf_platform_linux, true); \
     }
 
+#define TEST_SECTION_WITH_PARTITION_KEY(project, filename, section, partition_key)                          \
+    TEST_CASE("./check ebpf-samples/" project "/" filename " " section, "[verify][samples][" project "]") { \
+        ebpf_verifier_options_t options = ebpf_verifier_default_options;                                    \
+        options.partition_keys.push_back(partition_key);                                                    \
+        VERIFY_SECTION(project, filename, section, &options, &g_ebpf_platform_linux, true);                 \
+    }
+
 #define TEST_PROGRAM(project, filename, section_name, program_name) \
     TEST_CASE("./check ebpf-samples/" project "/" filename " " program_name, "[verify][samples][" project "]") { \
         VERIFY_PROGRAM(project, filename, section_name, program_name, nullptr, &g_ebpf_platform_linux, true); \
@@ -558,11 +565,11 @@ TEST_SECTION_FAIL("cilium", "bpf_xdp_dsr_linux.o", "2/18")
 TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/10")
 TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/18")
 
-TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/19")
-TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/21")
+TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/19", "packet_size")
+TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/20", "packet_size")
+TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_dsr_linux.o", "2/21", "packet_size")
 
-TEST_SECTION("cilium", "bpf_xdp_snat_linux.o", "2/19")
-TEST_SECTION("cilium", "bpf_xdp_dsr_linux.o", "2/20")
+TEST_SECTION_WITH_PARTITION_KEY("cilium", "bpf_xdp_snat_linux.o", "2/19", "packet_size")
 
 TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/7")
 TEST_SECTION_FAIL("cilium", "bpf_xdp_snat_linux.o", "2/15")

diff --git a/src/test/test_yaml.cpp b/src/test/test_yaml.cpp
@@ -9,7 +9,10 @@
 
 #define YAML_CASE(path) \
     TEST_CASE("YAML suite: " path, "[yaml]") { \
-        foreach_suite(path, [&](const TestCase& test_case){ \
+        foreach_suite(path, [&](TestCase test_case){ \
+            if (test_case.partition_keys.size() == 1 && test_case.partition_keys[0] == "none") { \
+                test_case.partition_keys.clear(); \
+            } \
             std::optional<Failure> failure = run_yaml_test_case(test_case); \
             if (failure) { \
                 std::cout << "test case: " << test_case.name << "\n"; \
@@ -19,6 +22,24 @@
         }); \
     }
 
+#define YAML_CASE_WITH_PARTITION(path, partition) \
+    TEST_CASE("YAML suite: " path " with partition " partition, "[yaml]") { \
+        foreach_suite(path, [&](TestCase test_case){ \
+            if (test_case.partition_keys.size() == 1 && test_case.partition_keys[0] == "none") { \
+                /* Skip test cases that are not partitioned */ \
+                return; \
+            } \
+            test_case.partition_keys = {partition}; \
+            std::optional<Failure> failure = run_yaml_test_case(test_case); \
+            if (failure) { \
+                std::cout << "test case: " << test_case.name << "\n"; \
+                print_failure(*failure, std::cout); \
+            } \
+            REQUIRE(!failure); \
+        }); \
+    }
+
+
 YAML_CASE("test-data/add.yaml")
 YAML_CASE("test-data/assign.yaml")
 YAML_CASE("test-data/atomic.yaml")
@@ -39,3 +60,24 @@ YAML_CASE("test-data/stack.yaml")
 YAML_CASE("test-data/subtract.yaml")
 YAML_CASE("test-data/unop.yaml")
 YAML_CASE("test-data/unsigned.yaml")
+
+YAML_CASE_WITH_PARTITION("test-data/add.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/assign.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/atomic.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/bitop.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/call.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/callx.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/udivmod.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/sdivmod.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/full64.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/jump.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/loop.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/movsx.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/packet.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/parse.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/sext.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/shift.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/stack.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/subtract.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/unop.yaml", "packet_size");
+YAML_CASE_WITH_PARTITION("test-data/unsigned.yaml", "packet_size");
+ −		build/correlated_branch.o
+ −		build/correlated_branch2.o
+81 −0		src/correlated_branch2.c