Implement ebpf_check_constraints_at_label

src/asm_parse.hpp

@@ -3,7 +3,21 @@
 #pragma once
 
 #include <string>
+#include <vector>
 
 #include "asm_syntax.hpp"
+#include "crab/interval.hpp"
+#include "crab/linear_constraint.hpp"
 
 Instruction parse_instruction(const std::string& line, const std::map<std::string, label_t>& label_name_to_label);
+
+/***
+ * Parse a set of string form linear constraints into a vector of crab::linear_constraint_t
+ *
+ * @param[in] constraints: A set of string form linear constraints.
+ * @param[out] numeric_ranges: A vector of numeric ranges that are extracted from the constraints.
+ *
+ * @return A vector of crab::linear_constraint_t
+ */
+std::vector<crab::linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints,
+                                                          std::vector<crab::interval_t>& numeric_ranges);

src/asm_syntax.hpp

@@ -23,6 +23,29 @@ struct label_t {
     explicit label_t(const int index, const int to = -1, std::string stack_frame_prefix = {}) noexcept
         : from(index), to(to), stack_frame_prefix(std::move(stack_frame_prefix)) {}
 
+    explicit label_t(std::string_view string_label) {
+        auto pos = string_label.find(STACK_FRAME_DELIMITER);
+        if (pos != std::string_view::npos) {
+            stack_frame_prefix = std::string(string_label.substr(0, pos));
+            string_label = string_label.substr(pos + 1);
+        }
+
+        pos = string_label.find(':');
+        try {
+            if (pos != std::string_view::npos) {
+                from = std::stoi(std::string(string_label.substr(0, pos)));
+                to = std::stoi(std::string(string_label.substr(pos + 1)));
+            } else {
+                from = std::stoi(std::string(string_label));
+                to = -1;
+            }
+        } catch (const std::invalid_argument& e) {
+            throw std::invalid_argument("Invalid label format: " + std::string(string_label));
+        } catch (const std::out_of_range& e) {
+            throw std::out_of_range("Label value out of range: " + std::string(string_label));
+        }
+    }
+
     static label_t make_jump(const label_t& src_label, const label_t& target_label) {
         return label_t{src_label.from, target_label.from, target_label.stack_frame_prefix};
     }

src/config.cpp

@@ -14,4 +14,5 @@ const ebpf_verifier_options_t ebpf_verifier_default_options = {
     .allow_division_by_zero = true,
     .setup_constraints = true,
     .big_endian = false,
+    .store_pre_invariants = false,
 };

src/config.hpp

@@ -21,6 +21,8 @@ struct ebpf_verifier_options_t {
     bool big_endian;
 
     bool dump_btf_types_json;
+
+    bool store_pre_invariants; ///< Store pre-invariants for use in ebpf_check_constraints_at_label.
 };
 
 struct ebpf_verifier_stats_t {

src/crab_verifier.cpp

@@ -17,6 +17,7 @@
 #include "crab_utils/lazy_allocator.hpp"
 
 #include "asm_syntax.hpp"
+#include "asm_parse.hpp"
 #include "crab_verifier.hpp"
 #include "string_constraints.hpp"
 
@@ -161,6 +162,8 @@ static checks_db get_analysis_report(std::ostream& s, cfg_t& cfg, const crab::in
     return db;
 }
 
+static thread_local std::optional<crab::invariant_table_t> save_pre_invariants = std::nullopt;
+
 static checks_db get_ebpf_report(std::ostream& s, 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);
@@ -172,6 +175,9 @@ static checks_db get_ebpf_report(std::ostream& s, cfg_t& cfg, program_info info,
         // Get dictionaries of pre-invariants and post-invariants for each basic block.
         ebpf_domain_t entry_dom = ebpf_domain_t::setup_entry(true);
         auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_dom));
+        if (thread_local_options.store_pre_invariants) {
+            save_pre_invariants = pre_invariants;
+        }
         return get_analysis_report(s, cfg, pre_invariants, post_invariants, prog);
     } catch (std::runtime_error& e) {
         // Convert verifier runtime_error exceptions to failure.
@@ -221,6 +227,9 @@ std::tuple<string_invariant, bool> ebpf_analyze_program_for_test(std::ostream& o
     try {
         cfg_t cfg = prepare_cfg(prog, info, options.simplify, false);
         auto [pre_invariants, post_invariants] = run_forward_analyzer(cfg, std::move(entry_inv));
+        if (thread_local_options.store_pre_invariants) {
+            save_pre_invariants = pre_invariants;
+        }
         const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
         print_report(os, report, prog, false);
 
@@ -267,4 +276,63 @@ void ebpf_verifier_clear_thread_local_state() {
     global_program_info.clear();
     crab::domains::clear_thread_local_state();
     crab::domains::SplitDBM::clear_thread_local_state();
+    save_pre_invariants = std::nullopt;
+}
+
+bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_string,
+                                     const std::set<std::string>& constraints) try {
+    label_t label = label_t(label_string);
+    if (!save_pre_invariants.has_value()) {
+        os << "No pre-invariants available\n";
+        return false;
+    }
+    if (save_pre_invariants.value().find(label) == save_pre_invariants.value().end()) {
+        os << "No pre-invariants available for label " << label << "\n";
+        return false;
+    }
+    ebpf_domain_t from_inv(save_pre_invariants.value().at(label));
+    auto concrete_domain = ebpf_domain_t::from_constraints(constraints, false);
+
+    if (concrete_domain.is_bottom()) {
+        os << "The provided constraints are unsatisfiable (concrete domain is bottom)\n";
+        os << "Concrete constraints are self-contradictory\n";
+        os << concrete_domain << "\n";
+        return false;
+    }
+
+    if (from_inv.is_bottom()) {
+        os << "The abstract state is unreachable\n";
+        os << from_inv << "\n";
+        return false;
+    }
+
+    if ((from_inv & concrete_domain).is_bottom()) {
+        os << "Concrete state does not match invariant\n";
+
+        // Print the concrete state
+        os << "--- Concrete state ---\n";
+        os << concrete_domain << "\n";
+
+        os << "--- Abstract state ---\n";
+        os << from_inv << "\n";
+
+        return false;
+    }
+
+    return true;
+} catch (std::exception& e) {
+    os << "Error occurred while checking constraints: " << e.what() << "\n";
+    return false;
+}
+
+std::set<std::string> ebpf_get_invariants_at_label(const std::string& label)
+{
+    label_t l = label_t(label);
+    if (!save_pre_invariants.has_value()) {
+        return {};
+    }
+    if (save_pre_invariants.value().find(l) == save_pre_invariants.value().end()) {
+        return {};
+    }
+    return save_pre_invariants.value().at(l).to_set().value();
 }

src/crab_verifier.hpp

@@ -26,3 +26,26 @@ int create_map_crab(const EbpfMapType& map_type, uint32_t key_size, uint32_t val
 EbpfMapDescriptor* find_map_descriptor(int map_fd);
 
 void ebpf_verifier_clear_thread_local_state();
+
+/**
+ * @brief Given a label and a set of concrete constraints, check if the concrete constraints match the abstract
+ * verifier constraints at the label. Requires the `store_pre_invariants` option to be set.
+ *
+ * Abstract constraints are computed by the verifier and stored if the `store_pre_invariants` option is set.
+ *
+ * @param[in,out] os Print output to this stream.
+ * @param[in] label The location in the CFG to check against.
+ * @param[in] constraints The concrete state to check.
+ * @return true If the state is valid.
+ * @return false If the state is invalid.
+ */
+bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label,
+                                     const std::set<std::string>& constraints);
+/**
+ * @brief Get the invariants at a given label. Requires the `store_pre_invariants` option to be set.
+ *
+ * @param[in] label
+ * @return The set of invariants at the given label.
+ * @throw std::out_of_range If the label is not found.
+ */
+std::set<std::string> ebpf_get_invariants_at_label(const std::string& label);

src/ebpf_yaml.cpp

@@ -99,6 +99,7 @@ struct RawTestCase {
     vector<std::tuple<string, vector<string>>> raw_blocks;
     vector<string> post;
     std::set<string> messages;
+    std::map<std::string, std::set<std::string>> invariants_to_check;
 };
 
 static vector<string> parse_block(const YAML::Node& block_node) {
@@ -126,6 +127,19 @@ static std::set<string> as_set_empty_default(const YAML::Node& optional_node) {
     return vector_to_set(optional_node.as<vector<string>>());
 }
 
+static std::map<std::string, std::set<std::string>> parse_invariants_to_check(const YAML::Node& case_node) {
+    if (!case_node["invariants-to-check"].IsDefined()) {
+        return {};
+    }
+
+    std::map<std::string, std::set<std::string>> res;
+    for (const auto& node : case_node["invariants-to-check"]) {
+        res.emplace(node.first.as<string>(), vector_to_set(node.second.as<vector<string>>()));
+    }
+
+    return res;
+}
+
 static RawTestCase parse_case(const YAML::Node& case_node) {
     return RawTestCase{
         .test_case = case_node["test-case"].as<string>(),
@@ -134,6 +148,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"]),
+        .invariants_to_check = parse_invariants_to_check(case_node),
     };
 }
 
@@ -205,7 +220,9 @@ 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,
+                    .invariants_to_check = raw_case.invariants_to_check,
+                    };
 }
 
 static vector<TestCase> read_suite(const string& path) {
@@ -246,6 +263,10 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
         test_case.options.simplify = false;
     }
 
+    if (!test_case.invariants_to_check.empty()) {
+        test_case.options.store_pre_invariants = true;
+    }
+
     ebpf_context_descriptor_t context_descriptor{64, 0, 4, -1};
     EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);
 
@@ -256,6 +277,16 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
         ss, test_case.instruction_seq, test_case.assumed_pre_invariant, info, test_case.options);
     std::set<string> actual_messages = extract_messages(ss.str());
 
+    for (auto& [label, expected_invariant] : test_case.invariants_to_check) {
+        if (!ebpf_check_constraints_at_label(ss, label, expected_invariant)) {
+            // If debug is enabled, print the output of ebpf_check_constraints_at_label.
+            if (debug) {
+                std::cout << ss.str();
+            }
+            actual_messages.insert(label + ": Concrete invariants at do not match abstract invariants");
+        }
+    }
+
     if (actual_last_invariant == test_case.expected_post_invariant && actual_messages == test_case.expected_messages) {
         return {};
     }

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::map<std::string, std::set<std::string>> invariants_to_check; ///< Map from label to expected invariants, used for checking invariants at specific labels.
 };
 
 void foreach_suite(const std::string& path, const std::function<void(const TestCase&)>& f);

test-data/add.yaml

@@ -175,3 +175,87 @@ post:
   - r7.packet_offset-r7.uvalue<=-7
   - r7.svalue-r7.packet_offset<=11
   - r7.uvalue-r7.packet_offset<=11
+
+---
+test-case: check concrete state
+
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0", r1.type=number, r1.svalue=0, r1.uvalue=0, r2.type=number, r2.svalue=0, r2.uvalue=0]
+
+code:
+  <start>: |
+    r1 = 1
+    r2 = 2
+    r1 += r2
+    r0 = r1
+
+invariants-to-check:
+  1:
+    - r1.type=number
+    - r1.svalue=1
+    - r1.uvalue=1
+  2:
+    - r2.type=number
+    - r2.svalue=2
+    - r2.uvalue=2
+  3:
+    - r1.type=number
+    - r1.svalue=3
+    - r1.uvalue=3
+  -2:
+    - r0.type=number
+    - r0.svalue=3
+    - r0.uvalue=3
+
+post:
+  - r0.type=number
+  - r0.uvalue=3
+  - r0.svalue=3
+  - r1.type=number
+  - r1.svalue=3
+  - r1.uvalue=3
+  - r2.type=number
+  - r2.svalue=2
+  - r2.uvalue=2
+---
+test-case: check concrete state - negative
+
+pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0", r1.type=number, r1.svalue=0, r1.uvalue=0, r2.type=number, r2.svalue=0, r2.uvalue=0]
+
+code:
+  <start>: |
+    r1 = 1
+    r2 = 2
+    r1 += r2
+    r0 = r1
+
+invariants-to-check:
+  1:
+    - r1.type=number
+    - r1.svalue=1
+    - r1.uvalue=1
+  2:
+    - r2.type=number
+    - r2.svalue=2
+    - r2.uvalue=2
+  3:
+    - r1.type=number
+    - r1.svalue=2
+    - r1.uvalue=2
+  -2:
+    - r0.type=number
+    - r0.svalue=3
+    - r0.uvalue=3
+
+post:
+  - r0.type=number
+  - r0.uvalue=3
+  - r0.svalue=3
+  - r1.type=number
+  - r1.svalue=3
+  - r1.uvalue=3
+  - r2.type=number
+  - r2.svalue=2
+  - r2.uvalue=2
+
+messages:
+  - "3: Concrete invariants at do not match abstract invariants"