PR feedback

Signed-off-by: Alan Jowett <alan.jowett@microsoft.com>

Author: Alan Jowett

src/config.cpp

@@ -14,5 +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,
+    .store_pre_invariants = false, // Enable this to permit usage of the ebpf_check_constraints_at_label and ebpf_get_invariants_at_label functions.
 };

src/crab_verifier.cpp

@@ -162,7 +162,13 @@ 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 thread_local std::optional<crab::invariant_table_t> saved_pre_invariants = std::nullopt;
+
+static void save_invariants_if_needed(const crab::invariant_table_t& pre_invariants) {
+    if (thread_local_options.store_pre_invariants) {
+        saved_pre_invariants = pre_invariants;
+    }
+}
 
 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) {
@@ -175,9 +181,7 @@ 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;
-        }
+        save_invariants_if_needed(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.
@@ -227,9 +231,7 @@ 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;
-        }
+        save_invariants_if_needed(pre_invariants);
         const checks_db report = get_analysis_report(std::cerr, cfg, pre_invariants, post_invariants);
         print_report(os, report, prog, false);
 
@@ -276,21 +278,21 @@ 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;
+    saved_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()) {
+    if (!saved_pre_invariants.has_value()) {
         os << "No pre-invariants available\n";
         return false;
     }
-    if (save_pre_invariants.value().find(label) == save_pre_invariants.value().end()) {
+    if (saved_pre_invariants.value().find(label) == saved_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));
+    ebpf_domain_t from_inv(saved_pre_invariants.value().at(label));
     auto concrete_domain = ebpf_domain_t::from_constraints(constraints, false);
 
     if (concrete_domain.is_bottom()) {
@@ -327,12 +329,14 @@ bool ebpf_check_constraints_at_label(std::ostream& os, const std::string& label_
 
 std::set<std::string> ebpf_get_invariants_at_label(const std::string& label)
 {
+    // If the label is malformed, throw an exception so the caller can handle it.
     label_t l = label_t(label);
-    if (!save_pre_invariants.has_value()) {
+
+    if (!saved_pre_invariants.has_value()) {
         return {};
     }
-    if (save_pre_invariants.value().find(l) == save_pre_invariants.value().end()) {
+    if (saved_pre_invariants.value().find(l) == saved_pre_invariants.value().end()) {
         return {};
     }
-    return save_pre_invariants.value().at(l).to_set().value();
+    return saved_pre_invariants.value().at(l).to_set().value();
 }

src/crab_verifier.hpp

@@ -32,6 +32,8 @@ void ebpf_verifier_clear_thread_local_state();
  * 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.
+ * These constraints represent the program state at a specific point in the control flow graph,
+ * as determined by the static analysis performed by the verifier.
  *
  * @param[in,out] os Print output to this stream.
  * @param[in] label The location in the CFG to check against.

src/test/ebpf_yaml.cpp

@@ -128,7 +128,7 @@ static std::set<string> as_set_empty_default(const YAML::Node& optional_node) {
 }
 
 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()) {
+    if (!case_node["invariants-to-check"].IsDefined() || case_node["invariants-to-check"].IsNull()) {
         return {};
     }
 
@@ -278,12 +278,14 @@ std::optional<Failure> run_yaml_test_case(TestCase test_case, bool debug) {
     std::set<string> actual_messages = extract_messages(ss.str());
 
     for (auto& [label, expected_invariant] : test_case.invariants_to_check) {
+        ss.str("");
+        ss.clear();
         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");
+            actual_messages.insert(label + ": Concrete invariants do not match abstract invariants");
         }
     }
 

test-data/add.yaml

@@ -189,19 +189,19 @@ code:
     r0 = r1
 
 invariants-to-check:
-  1:
+  1: # After the first assignment, r1 should be 1.
     - r1.type=number
     - r1.svalue=1
     - r1.uvalue=1
-  2:
+  2: # After the second assignment, r2 should be 2.
     - r2.type=number
     - r2.svalue=2
     - r2.uvalue=2
-  3:
+  3: # After the addition, r1 should be 3.
     - r1.type=number
     - r1.svalue=3
     - r1.uvalue=3
-  -2:
+  -2: # After the last assignment, r0 should be 3.
     - r0.type=number
     - r0.svalue=3
     - r0.uvalue=3
@@ -229,19 +229,19 @@ code:
     r0 = r1
 
 invariants-to-check:
-  1:
+  1: # After the first assignment, r1 should be 1.
     - r1.type=number
     - r1.svalue=1
     - r1.uvalue=1
-  2:
+  2: # After the second assignment, r2 should be 2.
     - r2.type=number
     - r2.svalue=2
     - r2.uvalue=2
-  3:
+  3: # After the addition, r1 should be 3. Invalid invariant to test negative case.
     - r1.type=number
     - r1.svalue=2
     - r1.uvalue=2
-  -2:
+  -2: # After the last assignment, r0 should be 3.
     - r0.type=number
     - r0.svalue=3
     - r0.uvalue=3
@@ -258,4 +258,4 @@ post:
   - r2.uvalue=2
 
 messages:
-  - "3: Concrete invariants at do not match abstract invariants"
+  - "3: Concrete invariants do not match abstract invariants"