reorganize type domain (#701)

* reorganize type domain * streamline type set handling --------- Signed-off-by: Elazar Gershuni <[email protected]>
vbpf · Sep 29, 2024 · 7b6a27f · 7b6a27f
1 parent 12d3121
commit 7b6a27f
Show file tree

Hide file tree

Showing 19 changed files with 575 additions and 483 deletions.
diff --git a/src/asm_ostream.cpp b/src/asm_ostream.cpp
@@ -10,11 +10,13 @@
 #include "asm_syntax.hpp"
 #include "crab/cfg.hpp"
 #include "crab/interval.hpp"
+#include "crab/type_encoding.hpp"
 #include "crab/variable.hpp"
 #include "helpers.hpp"
 #include "platform.hpp"
 #include "spec_type_descriptors.hpp"
 
+using crab::TypeGroup;
 using std::optional;
 using std::string;
 using std::vector;
@@ -103,29 +105,6 @@ std::ostream& operator<<(std::ostream& os, Condition::Op op) {
 
 static string size(int w) { return string("u") + std::to_string(w * 8); }
 
-static std::string to_string(TypeGroup ts) {
-    switch (ts) {
-    case TypeGroup::number: return "number";
-    case TypeGroup::map_fd: return "map_fd";
-    case TypeGroup::map_fd_programs: return "map_fd_programs";
-    case TypeGroup::ctx: return "ctx";
-    case TypeGroup::packet: return "packet";
-    case TypeGroup::stack: return "stack";
-    case TypeGroup::shared: return "shared";
-    case TypeGroup::mem: return "{stack, packet, shared}";
-    case TypeGroup::pointer: return "{ctx, stack, packet, shared}";
-    case TypeGroup::non_map_fd: return "non_map_fd";
-    case TypeGroup::ptr_or_num: return "{number, ctx, stack, packet, shared}";
-    case TypeGroup::stack_or_packet: return "{stack, packet}";
-    case TypeGroup::singleton_ptr: return "{ctx, stack, packet}";
-    case TypeGroup::mem_or_num: return "{number, stack, packet, shared}";
-    default: assert(false);
-    }
-    return {};
-}
-
-std::ostream& operator<<(std::ostream& os, TypeGroup ts) { return os << to_string(ts); }
-
 std::ostream& operator<<(std::ostream& os, ValidStore const& a) {
     return os << a.mem << ".type != stack -> " << TypeConstraint{a.val, TypeGroup::number};
 }
@@ -181,7 +160,7 @@ std::ostream& operator<<(std::ostream& os, Comparable const& a) {
     if (a.or_r2_is_number) {
         os << TypeConstraint{a.r2, TypeGroup::number} << " or ";
     }
-    return os << typereg(a.r1) << " == " << typereg(a.r2) << " in " << to_string(TypeGroup::singleton_ptr);
+    return os << typereg(a.r1) << " == " << typereg(a.r2) << " in " << TypeGroup::singleton_ptr;
 }
 
 std::ostream& operator<<(std::ostream& os, Addable const& a) {
@@ -191,8 +170,7 @@ std::ostream& operator<<(std::ostream& os, Addable const& a) {
 std::ostream& operator<<(std::ostream& os, ValidDivisor const& a) { return os << a.reg << " != 0"; }
 
 std::ostream& operator<<(std::ostream& os, TypeConstraint const& tc) {
-    string types = to_string(tc.types);
-    string cmp_op = types[0] == '{' ? "in" : "==";
+    const string cmp_op = is_singleton_type(tc.types) ? "==" : "in";
     return os << typereg(tc.reg) << " " << cmp_op << " " << tc.types;
 }
 

diff --git a/src/asm_parse.cpp b/src/asm_parse.cpp
@@ -1,18 +1,17 @@
 // Copyright (c) Prevail Verifier contributors.
 // SPDX-License-Identifier: MIT
-#include <algorithm>
 #include <map>
 #include <regex>
 #include <sstream>
 #include <string>
-#include <unordered_set>
 
 #include <boost/lexical_cast.hpp>
 
 #include "asm_parse.hpp"
 #include "asm_unmarshal.hpp"
 #include "crab/dsl_syntax.hpp"
 #include "crab/linear_constraint.hpp"
+#include "crab/type_encoding.hpp"
 #include "platform.hpp"
 #include "string_constraints.hpp"
 
@@ -241,7 +240,7 @@ static InstructionSeq parse_program(std::istream& is) {
         std::smatch m;
         if (regex_search(line, m, regex(LABEL ":"))) {
             next_label = label_t(boost::lexical_cast<int>(m[1]));
-            if (seen_labels.count(*next_label) != 0) {
+            if (seen_labels.contains(*next_label)) {
                 throw std::invalid_argument("duplicate labels");
             }
             line = m.suffix();
@@ -278,56 +277,10 @@ static crab::variable_t special_var(const std::string& s) {
     throw std::runtime_error(std::string() + "Bad special variable: " + s);
 }
 
-static crab::data_kind_t regkind(const std::string& s) {
-    if (s == "type") {
-        return crab::data_kind_t::types;
-    }
-    if (s == "ctx_offset") {
-        return crab::data_kind_t::ctx_offsets;
-    }
-    if (s == "map_fd") {
-        return crab::data_kind_t::map_fds;
-    }
-    if (s == "packet_offset") {
-        return crab::data_kind_t::packet_offsets;
-    }
-    if (s == "shared_offset") {
-        return crab::data_kind_t::shared_offsets;
-    }
-    if (s == "stack_offset") {
-        return crab::data_kind_t::stack_offsets;
-    }
-    if (s == "shared_region_size") {
-        return crab::data_kind_t::shared_region_sizes;
-    }
-    if (s == "stack_numeric_size") {
-        return crab::data_kind_t::stack_numeric_sizes;
-    }
-    if (s == "svalue") {
-        return crab::data_kind_t::svalues;
-    }
-    if (s == "uvalue") {
-        return crab::data_kind_t::uvalues;
-    }
-    throw std::runtime_error(std::string() + "Bad kind: " + s);
-}
-
-static type_encoding_t string_to_type_encoding(const std::string& s) {
-    static std::map<std::string, type_encoding_t> string_to_type{
-        {std::string("uninit"), T_UNINIT}, {std::string("map_fd_programs"), T_MAP_PROGRAMS},
-        {std::string("map_fd"), T_MAP},    {std::string("number"), T_NUM},
-        {std::string("ctx"), T_CTX},       {std::string("stack"), T_STACK},
-        {std::string("packet"), T_PACKET}, {std::string("shared"), T_SHARED},
-    };
-    if (string_to_type.count(s)) {
-        return string_to_type[s];
-    }
-    throw std::runtime_error(std::string("Unsupported type name: ") + s);
-}
-
 std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::string>& constraints,
                                                           std::vector<crab::interval_t>& numeric_ranges) {
     using namespace crab::dsl_syntax;
+    using crab::regkind;
     using crab::variable_t;
 
     std::vector<linear_constraint_t> res;
@@ -357,7 +310,7 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::st
                                regex(REG DOT "type"
                                              "=" TYPE))) {
             variable_t d = variable_t::reg(crab::data_kind_t::types, regnum(m[1]));
-            res.push_back(d == string_to_type_encoding(m[2]));
+            res.push_back(d == crab::string_to_type_encoding(m[2]));
         } else if (regex_match(cst_text, m, regex(REG DOT KIND "=" IMM))) {
             variable_t d = variable_t::reg(regkind(m[2]), regnum(m[1]));
             number_t value;
@@ -387,8 +340,8 @@ std::vector<linear_constraint_t> parse_linear_constraints(const std::set<std::st
         } 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) {
+            crab::type_encoding_t type = crab::string_to_type_encoding(m[3]);
+            if (type == crab::type_encoding_t::T_NUM) {
                 numeric_ranges.emplace_back(signed_number(m[1]), signed_number(m[2]));
             } else {
                 number_t lb = signed_number(m[1]);

diff --git a/src/asm_syntax.hpp b/src/asm_syntax.hpp
@@ -298,23 +298,6 @@ struct Assume {
     constexpr bool operator==(const Assume&) const = default;
 };
 
-enum class TypeGroup {
-    number,
-    map_fd,
-    ctx,             ///< pointer to the special memory region named 'ctx'
-    packet,          ///< pointer to the packet
-    stack,           ///< pointer to the stack
-    shared,          ///< pointer to shared memory
-    map_fd_programs, ///< reg == T_MAP_PROGRAMS
-    non_map_fd,      ///< reg >= T_NUM
-    mem,             ///< shared | stack | packet = reg >= T_PACKET
-    mem_or_num,      ///< reg >= T_NUM && reg != T_CTX
-    pointer,         ///< reg >= T_CTX
-    ptr_or_num,      ///< reg >= T_NUM
-    stack_or_packet, ///< reg <= T_STACK && reg >= T_PACKET
-    singleton_ptr,   ///< reg <= T_STACK && reg >= T_CTX
-};
-
 /// Condition check whether something is a valid size.
 struct ValidSize {
     Reg reg;
@@ -383,6 +366,7 @@ struct ValidStore {
     constexpr bool operator==(const ValidStore&) const = default;
 };
 
+using crab::TypeGroup;
 struct TypeConstraint {
     Reg reg;
     TypeGroup types;

diff --git a/src/assertions.cpp b/src/assertions.cpp
@@ -9,6 +9,7 @@
 #include "crab/cfg.hpp"
 #include "platform.hpp"
 
+using crab::TypeGroup;
 using std::string;
 using std::to_string;
 using std::vector;
@@ -146,7 +147,7 @@ class AssertExtractor {
             res.emplace_back(ValidAccess{cond.left});
             res.emplace_back(ValidAccess{reg(cond.right)});
             if (cond.op != Condition::Op::EQ && cond.op != Condition::Op::NE) {
-                res.emplace_back(TypeConstraint{cond.left, TypeGroup::non_map_fd});
+                res.emplace_back(TypeConstraint{cond.left, TypeGroup::ptr_or_num});
             }
             res.emplace_back(Comparable{.r1 = cond.left, .r2 = reg(cond.right), .or_r2_is_number = false});
         }

diff --git a/src/crab/dsl_syntax.hpp b/src/crab/dsl_syntax.hpp
@@ -33,6 +33,16 @@ inline linear_constraint_t operator>=(const linear_expression_t& e1, const linea
 
 inline linear_constraint_t operator>(const linear_expression_t& e1, const linear_expression_t& e2) { return e2 < e1; }
 
+inline linear_constraint_t eq(const variable_t a, const variable_t b) {
+    using namespace crab::dsl_syntax;
+    return {a - b, constraint_kind_t::EQUALS_ZERO};
+}
+
+inline linear_constraint_t neq(const variable_t a, const variable_t b) {
+    using namespace crab::dsl_syntax;
+    return {a - b, constraint_kind_t::NOT_ZERO};
+}
+
 inline linear_constraint_t operator==(const linear_expression_t& e1, const linear_expression_t& e2) {
     return linear_constraint_t(e1 - e2, constraint_kind_t::EQUALS_ZERO);
 }