simplify invariant output

* print only one variable per equivalence class * update tests Signed-off-by: Elazar Gershuni <[email protected]>
vbpf · Nov 20, 2024 · 2f2966f · 2f2966f
1 parent 04f0e92
commit 2f2966f
Show file tree

Hide file tree

Showing 22 changed files with 266 additions and 556 deletions.
diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
@@ -1130,14 +1130,62 @@ string_invariant SplitDBM::to_set() const {
     if (this->is_top()) {
         return string_invariant::top();
     }
+    // Extract all the edges
+    SubGraph g_excl{this->g, 0};
+
+    std::map<variable_t, variable_t> equivalence_classes;
+    std::set<std::tuple<variable_t, variable_t, Weight>> diff_csts;
+    for (const vert_id s : g_excl.verts()) {
+        const variable_t vs = *rev_map.at(s);
+        variable_t least = vs;
+        for (const vert_id d : g_excl.succs(s)) {
+            const variable_t vd = *rev_map.at(d);
+            const Weight w = g_excl.edge_val(s, d);
+            if (w == 0) {
+                least = std::min(least, vd, variable_t::printing_order);
+            } else {
+                diff_csts.emplace(vd, vs, w);
+            }
+        }
+        equivalence_classes.insert_or_assign(vs, least);
+    }
+
+    std::set<variable_t> representatives;
+    std::map<variable_t, std::string> equivalence_str;
+    for (const auto [vs, least] : equivalence_classes) {
+        if (vs == least) {
+            representatives.insert(vs);
+        } else {
+            equivalence_str[least] += "=" + vs.name();
+        }
+    }
 
     std::set<std::string> result;
-    // Intervals
+    for (const auto& [v, eqs] : equivalence_str) {
+        result.insert(v.name() + eqs);
+    }
 
-    // Extract all the edges
-    SubGraph g_excl(this->g, 0);
+    // simplify: x - y <= k && y - x <= -k
+    //        -> x <= y + k <= x
+    //        -> x = y + k
+    for (const auto& [vd, vs, w] : diff_csts) {
+        if (!representatives.contains(vd) || !representatives.contains(vs)) {
+            continue;
+        }
+        auto dual = to_string(vs, vd, -w, false);
+        if (result.contains(dual)) {
+            assert(w != 0);
+            result.erase(dual);
+            result.insert(to_string(vd, vs, w, true));
+        } else {
+            result.insert(to_string(vd, vs, w, false));
+        }
+    }
+
+    // Intervals
     for (vert_id v : g_excl.verts()) {
-        if (!this->rev_map[v]) {
+        const auto pvar = this->rev_map[v];
+        if (!pvar || !representatives.contains(*pvar)) {
             continue;
         }
         if (!this->g.elem(0, v) && !this->g.elem(v, 0)) {
@@ -1147,7 +1195,7 @@ string_invariant SplitDBM::to_set() const {
                          this->g.elem(0, v) ? number_t(this->g.edge_val(0, v)) : extended_number::plus_infinity()};
         assert(!v_out.is_bottom());
 
-        variable_t variable = *this->rev_map[v];
+        variable_t variable = *pvar;
 
         std::stringstream elem;
         elem << variable;
@@ -1164,7 +1212,7 @@ string_invariant SplitDBM::to_set() const {
             }
         } else {
             elem << "=";
-            if (v_out.lb() == v_out.ub()) {
+            if (v_out.is_singleton()) {
                 elem << v_out.lb();
             } else {
                 elem << v_out;
@@ -1173,40 +1221,13 @@ string_invariant SplitDBM::to_set() const {
         result.insert(elem.str());
     }
 
-    std::set<std::tuple<variable_t, variable_t, Weight>> diff_csts;
-    for (vert_id s : g_excl.verts()) {
-        if (!this->rev_map[s]) {
-            continue;
-        }
-        variable_t vs = *this->rev_map[s];
-        for (vert_id d : g_excl.succs(s)) {
-            if (!this->rev_map[d]) {
-                continue;
-            }
-            variable_t vd = *this->rev_map[d];
-            diff_csts.emplace(vd, vs, g_excl.edge_val(s, d));
-        }
-    }
-    // simplify: x - y <= k && y - x <= -k
-    //        -> x <= y + k <= x
-    //        -> x = y + k
-    for (const auto& [vd, vs, w] : diff_csts) {
-        auto dual = to_string(vs, vd, -w, false);
-        if (result.count(dual)) {
-            result.erase(dual);
-            result.insert(to_string(vd, vs, w, true));
-        } else {
-            result.insert(to_string(vd, vs, w, false));
-        }
-    }
     return string_invariant{result};
 }
 
 std::ostream& operator<<(std::ostream& o, const SplitDBM& dom) { return o << dom.to_set(); }
 
 bool SplitDBM::eval_expression_overflow(const linear_expression_t& e, Weight& out) const {
-    [[maybe_unused]]
-    const bool overflow = convert_NtoW_overflow(e.constant_term(), out);
+    [[maybe_unused]] const bool overflow = convert_NtoW_overflow(e.constant_term(), out);
     assert(!overflow);
     for (const auto& [variable, coefficient] : e.variable_terms()) {
         Weight coef;

diff --git a/src/crab/var_factory.cpp b/src/crab/var_factory.cpp
@@ -191,6 +191,8 @@ std::vector<variable_t> variable_t::get_type_variables() {
 
 bool variable_t::is_in_stack() const { return this->name()[0] == 's'; }
 
+bool variable_t::printing_order(const variable_t& a, const variable_t& b) { return a.name() < b.name(); }
+
 std::vector<variable_t> variable_t::get_loop_counters() {
     std::vector<variable_t> res;
     for (const std::string& name : *names) {

diff --git a/src/crab/variable.hpp b/src/crab/variable.hpp
@@ -78,6 +78,7 @@ class variable_t final {
     static variable_t loop_counter(const std::string& label);
     [[nodiscard]]
     bool is_in_stack() const;
+    static bool printing_order(const variable_t& a, const variable_t& b);
 }; // class variable_t
 
 } // namespace crab
diff --git a/test-data/add.yaml b/test-data/add.yaml
@@ -25,7 +25,6 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483649, 2147483651]
-  - r0.uvalue=[2147483649, 2147483651]
   - r0.svalue=r0.uvalue
 ---
 test-case: add immediate to unknown number
@@ -90,7 +89,6 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.uvalue=[10, 15]
   - r1.svalue=r1.uvalue
 
 ---
@@ -106,15 +104,12 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.uvalue=[10, 15]
   - r2.type=number
   - r2.svalue=5
   - r2.uvalue=5
   - r1.svalue=r1.uvalue
   - r1.svalue-r2.svalue<=10
-  - r1.uvalue-r2.svalue<=10
   - r2.svalue-r1.svalue<=-5
-  - r2.svalue-r1.uvalue<=-5
 
 ---
 test-case: add interval number register to constant register pointer
@@ -130,19 +125,11 @@ post:
   - r2.type=packet
   - r2.packet_offset=[3, 5]
   - r2.svalue=[10, 16]
-  - r2.uvalue=[10, 16]
   - r2.svalue=r2.uvalue
   - r7.type=number
-  - r7.svalue=[3, 5]
   - r7.uvalue=[3, 5]
-  - r7.svalue-r2.svalue<=-7
-  - r7.svalue-r2.uvalue<=-7
-  - r2.svalue-r7.svalue<=11
-  - r2.uvalue-r7.svalue<=11
   - r2.packet_offset-r2.svalue<=-7
-  - r2.packet_offset-r2.uvalue<=-7
   - r2.svalue-r2.packet_offset<=11
-  - r2.uvalue-r2.packet_offset<=11
   - r2.packet_offset=r7.svalue
 
 ---
@@ -159,19 +146,14 @@ post:
   - r7.type=packet
   - r7.packet_offset=[3, 5]
   - r7.svalue=[10, 16]
-  - r7.uvalue=[10, 16]
   - r7.svalue=r7.uvalue
   - r2.type=packet
   - r2.packet_offset=0
   - r2.svalue=[7, 11]
   - r2.uvalue=[7, 11]
   - r2.svalue-r7.svalue<=-3
-  - r2.svalue-r7.uvalue<=-3
   - r7.svalue-r2.svalue<=5
-  - r7.uvalue-r2.svalue<=5
   - r2.packet_offset-r7.packet_offset<=-3
   - r7.packet_offset-r2.packet_offset<=5
   - r7.packet_offset-r7.svalue<=-7
-  - r7.packet_offset-r7.uvalue<=-7
   - r7.svalue-r7.packet_offset<=11
-  - r7.uvalue-r7.packet_offset<=11
diff --git a/test-data/assign.yaml b/test-data/assign.yaml
@@ -183,7 +183,6 @@ code:
 post:
   - r2.svalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
-  - r2.uvalue=[0, 4294967295]
   - r10.type=stack
   - r10.stack_offset=512
 
@@ -221,7 +220,6 @@ post:
   - r1.shared_offset=0
   - r1.shared_region_size=16
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -241,7 +239,6 @@ post:
   - r1.shared_region_size=16
   - r1.stack_offset=500
   - r1.stack_numeric_size=16
-  - r2.type in {stack, shared}
   - r2.shared_offset=0
   - r2.shared_region_size=16
   - r2.stack_offset=500
@@ -304,15 +301,12 @@ code:
     r1 = r2
 
 post:
-  - packet_size=r1.packet_offset
+  - packet_size=r1.packet_offset=r2.packet_offset
+  - r1.svalue=r2.svalue
+  - r1.uvalue=r2.uvalue
   - r1.type=packet
   - r1.svalue=[4098, 2147418112]
-  - packet_size=r2.packet_offset
   - r2.type=packet
-  - r2.svalue=[4098, 2147418112]
-  - r1.packet_offset=r2.packet_offset
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
 ---
 test-case: 32-bit assign register packet value
 
@@ -324,7 +318,6 @@ code:
 
 post:
   - r1.svalue=[0, 4294967295]
-  - r1.uvalue=[0, 4294967295]
   - r1.svalue=r1.uvalue
   - packet_size=r2.packet_offset
   - r2.type=packet
@@ -348,8 +341,6 @@ post:
   - r1.uvalue=[1, 2147418112]
   - r2.ctx_offset=0
   - r2.type=ctx
-  - r2.svalue=[1, 2147418112]
-  - r2.uvalue=[1, 2147418112]
   - r1.svalue=r2.svalue
   - r1.uvalue=r2.uvalue
 ---
@@ -367,7 +358,6 @@ post:
   - r1.svalue=[1, 2147418112]
   - r1.uvalue=[1, 2147418112]
   - r2.svalue=[1, 2147418112]
-  - r2.uvalue=[1, 2147418112]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -401,7 +391,6 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages:
@@ -435,7 +424,6 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd_programs
   - r2.svalue=[0, 4294967295]
-  - r2.uvalue=[0, 4294967295]
   - r2.svalue=r2.uvalue
 
 messages: