Add stack numbers info to post in YAML tests

For consistency with s[a..b].type=packet etc output, this uses
the same style of output for stack numeric ranges.

Signed-off-by: Dave Thaler <dthaler@microsoft.com>

src/crab/array_domain.cpp

@@ -628,6 +628,8 @@ bool array_domain_t::is_bottom() const { return num_bytes.is_bottom(); }
 
 bool array_domain_t::is_top() const { return num_bytes.is_top(); }
 
+string_invariant array_domain_t::to_set() const { return num_bytes.to_set(); }
+
 bool array_domain_t::operator<=(const array_domain_t& other) const { return num_bytes <= other.num_bytes; }
 
 bool array_domain_t::operator==(const array_domain_t& other) const {
@@ -665,4 +667,5 @@ 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

@@ -64,6 +64,7 @@ class array_domain_t final {
     array_domain_t narrow(const array_domain_t& other) const;
 
     friend std::ostream& operator<<(std::ostream& o, const array_domain_t& dom);
+    [[nodiscard]] string_invariant to_set() const;
 
     bool all_num(NumAbsDomain& inv, const linear_expression_t& lb, const linear_expression_t& ub);
 

src/crab/bitset_domain.cpp

@@ -25,3 +25,32 @@ std::ostream& operator<<(std::ostream& o, const bitset_domain_t& b) {
     o << "}";
     return o;
 }
+
+string_invariant bitset_domain_t::to_set() const
+{
+    if (this->is_bottom()) {
+        return string_invariant::bottom();
+    }
+    if (this->is_top()) {
+        return string_invariant::top();
+    }
+
+    std::set<std::string> result;
+    bool first = true;
+    for (int i = -EBPF_STACK_SIZE; i < 0; i++) {
+        if (non_numerical_bytes[EBPF_STACK_SIZE + i])
+            continue;
+        first = false;
+        std::string value = "s[" + std::to_string(EBPF_STACK_SIZE + i);
+        int j = i + 1;
+        for (; j < 0; j++)
+            if (non_numerical_bytes[EBPF_STACK_SIZE + j])
+                break;
+        if (j > i + 1)
+            value += "..." + std::to_string(EBPF_STACK_SIZE + j - 1);
+        value += "].type=number";
+        result.insert(value);
+        i = j;
+    }
+    return string_invariant{result};
+}

src/crab/bitset_domain.hpp

@@ -4,6 +4,7 @@
 #include <cassert>
 #include <bitset>
 
+#include "string_constraints.hpp"
 #include "spec_type_descriptors.hpp" // for EBPF_STACK_SIZE
 
 class bitset_domain_t final {
@@ -24,6 +25,8 @@ class bitset_domain_t final {
 
     [[nodiscard]] bool is_bottom() const { return false; }
 
+    [[nodiscard]] string_invariant to_set() const;
+
     bool operator<=(const bitset_domain_t& other) const {
         return (non_numerical_bytes | other.non_numerical_bytes) == other.non_numerical_bytes;
     }

src/crab/ebpf_domain.cpp

@@ -1304,7 +1304,7 @@ void ebpf_domain_t::operator()(const Bin& bin) {
 }
 
 string_invariant ebpf_domain_t::to_set() {
-    return this->m_inv.to_set();
+    return this->m_inv.to_set() + this->stack.to_set();
 }
 
 std::ostream& operator<<(std::ostream& o, const ebpf_domain_t& dom) {

src/string_constraints.cpp

@@ -120,6 +120,18 @@ string_invariant string_invariant::operator-(const string_invariant& b) const {
     return res;
 }
 
+// return a+b, taking account potential optional-none
+string_invariant string_invariant::operator+(const string_invariant& b) const {
+    if (this->is_bottom())
+        return b;
+    string_invariant res = *this;
+    for (const std::string& cst : b.value()) {
+        if (res.is_bottom() || !res.contains(cst))
+            res.maybe_inv->insert(cst);
+    }
+    return res;
+}
+
 std::ostream& operator<<(std::ostream& o, const string_invariant& inv) {
     if (inv.is_bottom()) {
         return o << "_|_";

src/string_constraints.hpp

@@ -32,6 +32,7 @@ struct string_invariant {
     }
 
     string_invariant operator-(const string_invariant& b) const;
+    string_invariant operator+(const string_invariant& b) const;
 
     bool operator==(const string_invariant& other) const { return maybe_inv == other.maybe_inv; }
 

test-data/single-instruction-assignment.yaml

@@ -63,6 +63,7 @@ code:
 post:
   - r10.type=stack
   - r10.offset=512
+  - s[504...511].type=number
   - s[504...511].value=0
 ---
 test-case: stack assign number register
@@ -78,6 +79,7 @@ post:
   - r1.value=0
   - r10.type=stack
   - r10.offset=512
+  - s[504...511].type=number
   - s[504...511].value=0
 ---
 test-case: stack assign packet register