Add support for stack ranges in pre section of YAML tests

Signed-off-by: Dave Thaler <[email protected]>

src/crab/array_domain.cpp

@@ -667,5 +667,4 @@ array_domain_t array_domain_t::narrow(const array_domain_t& other) const {
 std::ostream& operator<<(std::ostream& o, const array_domain_t& dom) {
     return o << dom.num_bytes;
 }
-
 } // namespace crab::domains

src/crab/array_domain.hpp

@@ -83,6 +83,8 @@ class array_domain_t final {
 
     // Perform array stores over an array segment
     void store_numbers(NumAbsDomain& inv, variable_t _idx, variable_t _width);
+
+    void initialize_numbers(int lb, int width) { num_bytes.reset(lb, width); }
 };
 
 }

src/crab/ebpf_domain.cpp

@@ -1333,12 +1333,18 @@ void ebpf_domain_t::initialize_packet(ebpf_domain_t& inv) {
     }
 }
 
-ebpf_domain_t ebpf_domain_t::from_constraints(const std::vector<linear_constraint_t>& csts) {
-    // TODO: handle type constraints separately
+ebpf_domain_t ebpf_domain_t::from_constraints(const std::set<std::string>& constraints) {
     ebpf_domain_t inv;
-    for (const auto& cst: csts) {
+    auto numeric_ranges = std::vector<crab::interval_t>();
+    for (const auto& cst : parse_linear_constraints(constraints, numeric_ranges)) {
         inv += cst;
     }
+    for (const crab::interval_t& range : numeric_ranges) {
+        int start = (int)range.lb().number().value();
+        int width = 1 + (int)(range.ub() - range.lb()).number().value();
+        inv.stack.initialize_numbers(start, width);
+    }
+    // TODO: handle other stack type constraints
     return inv;
 }
 

src/crab/ebpf_domain.hpp

@@ -44,7 +44,7 @@ class ebpf_domain_t final {
     int get_instruction_count_upper_bound();
     static ebpf_domain_t setup_entry(bool check_termination);
 
-    static ebpf_domain_t from_constraints(const std::vector<linear_constraint_t>& csts);
+    static ebpf_domain_t from_constraints(const std::set<std::string>& constraints);
     string_invariant to_set();
 
     // abstract transformers

src/crab/var_factory.cpp

@@ -85,7 +85,7 @@ std::vector<variable_t> variable_t::get_type_variables() {
     }
     return res;
 }
-bool variable_t::is_in_stack() {
+bool variable_t::is_in_stack() const {
     return this->name()[0] == 's';
 }
 } // end namespace crab

src/crab/variable.hpp

@@ -60,7 +60,7 @@ class variable_t final {
     static variable_t meta_offset();
     static variable_t packet_size();
     static variable_t instruction_count();
-    bool is_in_stack();
+    [[nodiscard]] bool is_in_stack() const;
 
     struct Hasher {
         std::size_t operator()(const variable_t& v) const { return v.hash(); }

src/crab_verifier.cpp

@@ -187,7 +187,7 @@ ebpf_analyze_program_for_test(std::ostream& os, const InstructionSeq& prog, cons
                               bool no_simplify, bool check_termination) {
     ebpf_domain_t entry_inv = entry_invariant.is_bottom()
         ? ebpf_domain_t::bottom()
-        : ebpf_domain_t::from_constraints(parse_linear_constraints(entry_invariant.value()));
+        : ebpf_domain_t::from_constraints(entry_invariant.value());
     global_program_info = info;
     cfg_t cfg = prepare_cfg(prog, info, !no_simplify, false);
     auto [pre_invariants, post_invariants] = crab::run_forward_analyzer(cfg, entry_inv, check_termination);

src/ebpf_yaml.cpp

@@ -60,7 +60,7 @@ ebpf_platform_t g_platform_test = {
     .get_map_type = ebpf_get_map_type
 };
 
-static EbpfProgramType make_progran_type(const string& name, ebpf_context_descriptor_t* context_descriptor) {
+static EbpfProgramType make_program_type(const string& name, ebpf_context_descriptor_t* context_descriptor) {
     return EbpfProgramType{
         .name=name,
         .context_descriptor=context_descriptor,
@@ -198,7 +198,7 @@ static Diff<T> make_diff(const T& actual, const T& expected) {
 
 std::optional<Failure> run_yaml_test_case(const TestCase& test_case) {
     ebpf_context_descriptor_t context_descriptor{0, -1, -1, -1};
-    EbpfProgramType program_type = make_progran_type(test_case.name, &context_descriptor);
+    EbpfProgramType program_type = make_program_type(test_case.name, &context_descriptor);
 
     program_info info{&g_platform_test, {}, program_type};
 

src/string_constraints.cpp

@@ -23,6 +23,7 @@ using std::map;
 #define KIND R"_(\s*(type|value|offset|region_size)\s*)_"
 #define IMM R"_(\s*\[?([-+]?\d+)\]?\s*)_"
 #define INTERVAL R"_(\s*\[([-+]?\d+),\s*([-+]?\d+)\]?\s*)_"
+#define ARRAY_RANGE R"_(\s*\[([-+]?\d+)\.\.\.\s*([-+]?\d+)\]?\s*)_"
 
 #define DOT "[.]"
 #define TYPE R"_(\s*(shared|number|packet|stack|ctx|map_fd|map_fd_program)\s*)_"
@@ -64,7 +65,7 @@ static type_encoding_t string_to_type_encoding(const string& s) {
     throw std::runtime_error(string("Unsupported type name: ") + s);
 }
 
-std::vector<linear_constraint_t> parse_linear_constraints(const std::set<string>& constraints) {
+std::vector<linear_constraint_t> parse_linear_constraints(const std::set<string>& constraints, std::vector<crab::interval_t>& numeric_ranges) {
     using namespace crab::dsl_syntax;
 
     std::vector<linear_constraint_t> res;
@@ -102,6 +103,16 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<string>
             variable_t s = variable_t::reg(regkind(m[4]), regnum(m[3]));
             long diff = number(m[5]);
             res.push_back(d - s <= number_t(diff));
+        } else if (regex_match(cst_text, m, regex("s" ARRAY_RANGE DOT "type" "=" TYPE))) {
+            type_encoding_t type = string_to_type_encoding(m[3]);
+            if (type == type_encoding_t::T_NUM) {
+                numeric_ranges.push_back(crab::interval_t(number(m[1]), number(m[2])));
+            } else {
+                long lb = number(m[1]);
+                long ub = number(m[2]);
+                variable_t d = variable_t::cell_var(data_kind_t::types, lb, ub - lb + 1);
+                res.push_back(d == type);
+            }
         } else {
             throw std::runtime_error(string("Unknown constraint: ") + cst_text);
         }

src/string_constraints.hpp

@@ -8,6 +8,7 @@
 #include <string>
 #include <vector>
 
+#include "crab/interval.hpp"
 #include "crab/linear_constraint.hpp"
 
 struct string_invariant {
@@ -43,4 +44,4 @@ struct string_invariant {
     friend std::ostream& operator<<(std::ostream&, const string_invariant& inv);
 };
 
-std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints);
+std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints, std::vector<crab::interval_t>& numeric_ranges);

test-data/single-instruction-assignment.yaml

@@ -99,3 +99,36 @@ post:
   - r10.offset=512
   - s[504...511].type=packet
   - s[504...511].offset=0
+---
+test-case: stack extend numeric range
+
+pre: ["r10.type=stack", "r10.offset=512", "s[500...507].type=number"]
+
+code:
+  <start>: |
+    *(u64 *)(r10 - 8) = 0
+
+post:
+  - r10.type=stack
+  - r10.offset=512
+  - s[500...511].type=number
+  - s[504...511].value=0
+---
+test-case: stack narrow numeric range
+
+pre: ["r10.type=stack", "r10.offset=512", "r1.type=packet", "r1.offset=0", "s[500...507].type=number"]
+
+code:
+  <start>: |
+    *(u64 *)(r10 - 8) = r1
+
+post:
+  - r1.type=packet
+  - r1.offset=0
+  - r1.value=s[504...511].value
+  - r1.region_size=s[504...511].region_size
+  - r10.type=stack
+  - r10.offset=512
+  - s[500...503].type=number
+  - s[504...511].type=packet
+  - s[504...511].offset=0