Convert invariant check to inline require

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

src/asm_parse.cpp

@@ -54,6 +54,9 @@ using crab::number_t;
 #define DOT "[.]"
 #define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_programs)\s*)_"
 
+// regex to match "require [assertion1, assertion2, ...]"
+#define REQUIRE R"_(\s*require\s*\[\s*(.*)\s*\]\s*)_"
+
 static const std::map<std::string, Bin::Op> str_to_binop = {
     {"", Bin::Op::MOV},        {"+", Bin::Op::ADD},   {"-", Bin::Op::SUB},     {"*", Bin::Op::MUL},
     {"/", Bin::Op::UDIV},      {"%", Bin::Op::UMOD},  {"|", Bin::Op::OR},      {"&", Bin::Op::AND},
@@ -133,7 +136,8 @@ static Deref deref(const std::string& width, const std::string& basereg, const s
     };
 }
 
-Instruction parse_instruction(const std::string& line, const std::map<std::string, label_t>& label_name_to_label) {
+InstructionOrConstraintsSet parse_instruction(const std::string& line,
+                                              const std::map<std::string, label_t>& label_name_to_label) {
     // treat ";" as a comment
     std::string text = line.substr(0, line.find(';'));
     const size_t end = text.find_last_not_of(' ');
@@ -221,6 +225,17 @@ Instruction parse_instruction(const std::string& line, const std::map<std::strin
         }
         return res;
     }
+    if (regex_match(text, m, regex(REQUIRE))) {
+        std::string constraints = m[1];
+        std::set<std::string> constraint_set;
+        std::vector<crab::interval_t> numeric_ranges;
+        std::regex re(R"(\s*,\s*)");
+        std::sregex_token_iterator first{constraints.begin(), constraints.end(), re, -1}, last;
+        for (; first != last; ++first) {
+            constraint_set.insert(*first);
+        }
+        return constraint_set;
+    }
     return Undefined{0};
 }
 
@@ -246,7 +261,15 @@ static InstructionSeq parse_program(std::istream& is) {
         if (line.empty()) {
             continue;
         }
-        Instruction ins = parse_instruction(line, {});
+
+        auto ins_or_constraints = parse_instruction(line, {});
+
+        if (std::holds_alternative<ConstraintsSet>(ins_or_constraints)) {
+            continue;
+        }
+
+        Instruction ins = convert_to_original<Instruction>(ins_or_constraints).value_or(Undefined{0});
+
         if (std::holds_alternative<Undefined>(ins)) {
             continue;
         }

src/asm_parse.hpp

@@ -9,7 +9,8 @@
 #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);
+InstructionOrConstraintsSet 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

src/asm_syntax.hpp

@@ -449,8 +449,9 @@ struct BoundedLoopCount {
     static constexpr int limit = 100000;
 };
 
-using AssertionConstraint = std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize,
-                                         ValidMapKeyValue, ValidCall, TypeConstraint, FuncConstraint, ZeroCtxOffset, BoundedLoopCount>;
+using AssertionConstraint =
+    std::variant<Comparable, Addable, ValidDivisor, ValidAccess, ValidStore, ValidSize, ValidMapKeyValue, ValidCall,
+                 TypeConstraint, FuncConstraint, ZeroCtxOffset, BoundedLoopCount>;
 
 struct Assert {
     AssertionConstraint cst;
@@ -463,11 +464,48 @@ struct IncrementLoopCounter {
     bool operator==(const IncrementLoopCounter&) const = default;
 };
 
+// Helper metafunction to append a type to a variant
+template <typename Variant, typename NewType>
+struct append_to_variant;
+
+template <typename... Types, typename NewType>
+struct append_to_variant<std::variant<Types...>, NewType> {
+    using type = std::variant<Types..., NewType>;
+};
+
+// Helper metafunction to check if a type is in a variant
+template <typename Variant, typename T>
+struct is_type_in_variant;
+
+template <typename T, typename... Types>
+struct is_type_in_variant<std::variant<Types...>, T> : std::disjunction<std::is_same<T, Types>...> {};
+
+// Function to convert ExtendedVariant to OriginalVariant if it doesn't contain the new type
+template <typename OriginalVariant, typename ExtendedVariant>
+std::optional<OriginalVariant> convert_to_original(const ExtendedVariant& extendedVariant) {
+    std::optional<OriginalVariant> result;
+
+    std::visit(
+        [&result](auto&& arg) {
+            using T = std::decay_t<decltype(arg)>;
+            if constexpr (is_type_in_variant<OriginalVariant, T>::value) {
+                result = arg;
+            }
+        },
+        extendedVariant);
+    return result;
+}
+
 using Instruction = std::variant<Undefined, Bin, Un, LoadMapFd, Call, CallLocal, Callx, Exit, Jmp, Mem, Packet, Atomic,
                                  Assume, Assert, IncrementLoopCounter>;
 
+using ConstraintsSet = std::set<std::string>;
+using InstructionOrConstraintsSet = append_to_variant<Instruction, ConstraintsSet>::type;
 using LabeledInstruction = std::tuple<label_t, Instruction, std::optional<btf_line_info_t>>;
+using LabeleldConstraints = std::tuple<label_t, ConstraintsSet>;
 using InstructionSeq = std::vector<LabeledInstruction>;
+using ConstraintsSeq = std::vector<LabeleldConstraints>;
+using InstructionAndConstraintsSeq = std::tuple<InstructionSeq, ConstraintsSeq>;
 
 // cpu=v4 supports 32-bit PC offsets so we need a large enough type.
 using pc_t = size_t;

src/test/ebpf_yaml.cpp

@@ -99,7 +99,6 @@ 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) {
@@ -143,18 +142,16 @@ static std::map<std::string, std::set<std::string>> parse_invariants_to_check(co
 }
 
 static RawTestCase parse_case(const YAML::Node& case_node) {
-    return RawTestCase{
-        .test_case = case_node["test-case"].as<string>(),
-        .options = as_set_empty_default(case_node["options"]),
-        .pre = case_node["pre"].as<vector<string>>(),
-        .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),
-    };
+    return RawTestCase{.test_case = case_node["test-case"].as<string>(),
+                       .options = as_set_empty_default(case_node["options"]),
+                       .pre = case_node["pre"].as<vector<string>>(),
+                       .raw_blocks = parse_code(case_node["code"]),
+                       .post = case_node["post"].as<vector<string>>(),
+                       .messages = as_set_empty_default(case_node["messages"])};
 }
 
-static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string, vector<string>>>& raw_blocks) {
+static InstructionAndConstraintsSeq
+raw_cfg_to_instruction_seq(const vector<std::tuple<string, vector<string>>>& raw_blocks) {
     std::map<string, crab::label_t> label_name_to_label;
 
     int label_index = 0;
@@ -165,11 +162,21 @@ static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string,
     }
 
     InstructionSeq res;
+    ConstraintsSeq constraints;
     label_index = 0;
     for (const auto& [label_name, raw_block] : raw_blocks) {
         for (const string& line : raw_block) {
             try {
-                const Instruction& ins = parse_instruction(line, label_name_to_label);
+                const InstructionOrConstraintsSet& ins_or_constraints = parse_instruction(line, label_name_to_label);
+                if (std::holds_alternative<ConstraintsSet>(ins_or_constraints)) {
+                    constraints.emplace_back(label_index, std::get<ConstraintsSet>(ins_or_constraints));
+                    continue;
+                }
+                auto ins_opt = convert_to_original<Instruction>(ins_or_constraints);
+                if (!ins_opt) {
+                    continue;
+                }
+                const Instruction& ins = *ins_opt;
                 if (std::holds_alternative<Undefined>(ins)) {
                     std::cout << "text:" << line << "; ins: " << ins << "\n";
                 }
@@ -181,7 +188,7 @@ static InstructionSeq raw_cfg_to_instruction_seq(const vector<std::tuple<string,
             label_index++;
         }
     }
-    return res;
+    return {res, constraints};
 }
 
 static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& raw_options) {
@@ -225,14 +232,16 @@ static ebpf_verifier_options_t raw_options_to_options(const std::set<string>& ra
 }
 
 static TestCase read_case(const RawTestCase& raw_case) {
-    return TestCase{.name = raw_case.test_case,
-                    .options = raw_options_to_options(raw_case.options),
-                    .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,
-                    .invariants_to_check = raw_case.invariants_to_check,
-                    };
+    auto instruction_seq_and_constraints = raw_cfg_to_instruction_seq(raw_case.raw_blocks);
+    return TestCase{
+        .name = raw_case.test_case,
+        .options = raw_options_to_options(raw_case.options),
+        .assumed_pre_invariant = read_invariant(raw_case.pre),
+        .instruction_seq = std::get<0>(instruction_seq_and_constraints),
+        .expected_post_invariant = read_invariant(raw_case.post),
+        .expected_messages = raw_case.messages,
+        .invariants_to_check = std::get<1>(instruction_seq_and_constraints),
+    };
 }
 
 static vector<TestCase> read_suite(const string& path) {
@@ -287,8 +296,12 @@ 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) {
+    for (auto& [index, expected_invariant] : test_case.invariants_to_check) {
+        ss = {};
+        ss << index;
+        std::string label = ss.str();
         ss = {};
+
         try {
             if (!ebpf_check_constraints_at_label(ss, label, expected_invariant)) {
                 // If debug is enabled, print the output of ebpf_check_constraints_at_label.

src/test/ebpf_yaml.hpp

@@ -14,7 +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 validating program state at specific labels during test execution.
+    ConstraintsSeq invariants_to_check;
 };
 
 void foreach_suite(const std::string& path, const std::function<void(const TestCase&)>& f);

test-data/add.yaml

@@ -184,31 +184,13 @@ pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0", r1.type=number, r1.svalue=
 code:
   <start>: |
     r1 = 1
+    require [r1.type=number, r1.svalue=1, r1.uvalue=r1.svalue]
     r2 = 2
+    require [r2.type=number, r2.svalue=2, r2.uvalue=r2.svalue]
     r1 += r2
+    require [r1.type=number, r1.svalue=3, r1.uvalue=r1.svalue]
     r0 = r1
 
-invariants-to-check:
-  1:  # After the first assignment, r1 should be 1.
-    - r1.type=number
-    - r1.svalue=1
-    - r1.uvalue=1
-
-  2:  # After the second assignment, r2 should be 2.
-    - r2.type=number
-    - r2.svalue=2
-    - r2.uvalue=2
-
-  3:  # After the addition, r1 should be 3.
-    - r1.type=number
-    - r1.svalue=3
-    - r1.uvalue=3
-
-  -2:  # After the last assignment, r0 should be 3.
-    - r0.type=number
-    - r0.svalue=3
-    - r0.uvalue=3
-
 post:
   - r0.type=number
   - r0.uvalue=3
@@ -227,32 +209,13 @@ pre: ["r0.type=number", "r0.svalue=0", "r0.uvalue=0", r1.type=number, r1.svalue=
 code:
   <start>: |
     r1 = 1
+    require [r1.type=number, r1.svalue=1, r1.uvalue=r1.svalue]
     r2 = 2
+    require [r2.type=number, r2.svalue=2, r2.uvalue=r2.svalue]
     r1 += r2
+    require [r1.type=number, r1.svalue=2, r1.uvalue=r1.svalue]
     r0 = r1
 
-invariants-to-check:
-  1:  # After the first assignment, r1 should be 1.
-    - r1.type=number
-    - r1.svalue=1
-    - r1.uvalue=1
-
-  2:  # After the second assignment, r2 should be 2.
-    - r2.type=number
-    - r2.svalue=2
-    - r2.uvalue=2
-
-  3:  # After the addition, r1 should be 3.
-    # Using a value of 2 instead of 3 to ensure that the test fails (this is a negative test case).
-    - r1.type=number
-    - r1.svalue=2
-    - r1.uvalue=2
-
-  -2:  # After the last assignment, r0 should be 3.
-    - r0.type=number
-    - r0.svalue=3
-    - r0.uvalue=3
-
 post:
   - r0.type=number
   - r0.uvalue=3