do not chain equalities

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

Hide file tree

Showing 21 changed files with 523 additions and 512 deletions.
diff --git a/src/crab/split_dbm.cpp b/src/crab/split_dbm.cpp
@@ -1151,20 +1151,15 @@ string_invariant SplitDBM::to_set() const {
     }
 
     std::set<variable_t> representatives;
-    std::map<variable_t, std::string> equivalence_str;
+    std::set<std::string> result;
     for (const auto [vs, least] : equivalence_classes) {
         if (vs == least) {
-            representatives.insert(vs);
+            representatives.insert(least);
         } else {
-            equivalence_str[least] += "=" + vs.name();
+            result.insert(vs.name() + "=" + least.name());
         }
     }
 
-    std::set<std::string> result;
-    for (const auto& [v, eqs] : equivalence_str) {
-        result.insert(v.name() + eqs);
-    }
-
     // simplify: x - y <= k && y - x <= -k
     //        -> x <= y + k <= x
     //        -> x = y + k

diff --git a/test-data/add.yaml b/test-data/add.yaml
@@ -25,7 +25,7 @@ code:
 post:
   - r0.type=number
   - r0.svalue=[2147483649, 2147483651]
-  - r0.svalue=r0.uvalue
+  - r0.uvalue=r0.svalue
 ---
 test-case: add immediate to unknown number
 
@@ -89,7 +89,7 @@ code:
 post:
   - r1.type=number
   - r1.svalue=[10, 15]
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
 
 ---
 test-case: add constant register number to finite interval number
@@ -107,7 +107,7 @@ post:
   - r2.type=number
   - r2.svalue=5
   - r2.uvalue=5
-  - r1.svalue=r1.uvalue
+  - r1.uvalue=r1.svalue
   - r1.svalue-r2.svalue<=10
   - r2.svalue-r1.svalue<=-5
 
@@ -125,12 +125,12 @@ post:
   - r2.type=packet
   - r2.packet_offset=[3, 5]
   - r2.svalue=[10, 16]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
   - r7.type=number
   - r7.uvalue=[3, 5]
   - r2.packet_offset-r2.svalue<=-7
   - r2.svalue-r2.packet_offset<=11
-  - r2.packet_offset=r7.svalue
+  - r7.svalue=r2.packet_offset
 
 ---
 test-case: add constant register pointer to interval number
@@ -146,7 +146,7 @@ post:
   - r7.type=packet
   - r7.packet_offset=[3, 5]
   - r7.svalue=[10, 16]
-  - r7.svalue=r7.uvalue
+  - r7.uvalue=r7.svalue
   - r2.type=packet
   - r2.packet_offset=0
   - r2.svalue=[7, 11]

diff --git a/test-data/assign.yaml b/test-data/assign.yaml
@@ -23,9 +23,9 @@ code:
     r1 = r2;
 
 post:
-  - r1.type=r2.type
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.type=r1.type
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 
 ---
 test-case: re-assign immediate
@@ -98,8 +98,8 @@ code:
 post:
   - r1.type=packet
   - r1.packet_offset=0
-  - r1.svalue=s[504...511].svalue
-  - r1.uvalue=s[504...511].uvalue
+  - s[504...511].svalue=r1.svalue
+  - s[504...511].uvalue=r1.uvalue
   - r10.type=stack
   - r10.stack_offset=512
   - s[504...511].type=packet
@@ -131,8 +131,8 @@ code:
 post:
   - r1.type=packet
   - r1.packet_offset=0
-  - r1.svalue=s[504...511].svalue
-  - r1.uvalue=s[504...511].uvalue
+  - s[504...511].svalue=r1.svalue
+  - s[504...511].uvalue=r1.uvalue
   - r10.type=stack
   - r10.stack_offset=512
   - s[500...503].type=number
@@ -168,9 +168,9 @@ post:
   - r1.stack_offset=0
   - r2.type=stack
   - r2.stack_offset=0
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
-  - r1.stack_numeric_size=r2.stack_numeric_size
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
+  - r2.stack_numeric_size=r1.stack_numeric_size
 ---
 test-case: 32-bit assign register stack value
 
@@ -182,7 +182,7 @@ code:
 
 post:
   - r2.svalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
   - r10.type=stack
   - r10.stack_offset=512
 
@@ -204,8 +204,8 @@ post:
   - r2.type=shared
   - r2.shared_offset=0
   - r2.shared_region_size=16
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register shared value
 
@@ -220,7 +220,7 @@ post:
   - r1.shared_offset=0
   - r1.shared_region_size=16
   - r2.svalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -243,9 +243,9 @@ post:
   - r2.shared_region_size=16
   - r2.stack_offset=500
   - r2.stack_numeric_size=16
-  - r1.type=r2.type
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.type=r1.type
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit indirect assignment from context
 
@@ -256,7 +256,7 @@ code:
     r2 = *(u32 *)(r1 + 4)
 
 post:
-  - packet_size=r2.packet_offset
+  - r2.packet_offset=packet_size
   - r1.ctx_offset=0
   - r1.type=ctx
   - r1.svalue=[1, 2147418112]
@@ -294,32 +294,33 @@ post:
 ---
 test-case: assign register packet value
 
-pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+pre: ["r2.packet_offset=packet_size", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
 
 code:
   <start>: |
     r1 = r2
 
 post:
-  - packet_size=r1.packet_offset=r2.packet_offset
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r1.packet_offset=packet_size
+  - r2.packet_offset=packet_size
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
   - r1.type=packet
   - r1.svalue=[4098, 2147418112]
   - r2.type=packet
 ---
 test-case: 32-bit assign register packet value
 
-pre: ["packet_size=r2.packet_offset", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
+pre: ["r2.packet_offset=packet_size", "r2.type=packet", "r2.svalue=[4098, 2147418112]"]
 
 code:
   <start>: |
     w1 = r2
 
 post:
   - r1.svalue=[0, 4294967295]
-  - r1.svalue=r1.uvalue
-  - packet_size=r2.packet_offset
+  - r1.uvalue=r1.svalue
+  - r2.packet_offset=packet_size
   - r2.type=packet
   - r2.svalue=[4098, 2147418112]
 
@@ -341,8 +342,8 @@ post:
   - r1.uvalue=[1, 2147418112]
   - r2.ctx_offset=0
   - r2.type=ctx
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register context value
 
@@ -358,7 +359,7 @@ post:
   - r1.svalue=[1, 2147418112]
   - r1.uvalue=[1, 2147418112]
   - r2.svalue=[1, 2147418112]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -376,8 +377,8 @@ post:
   - r1.type=map_fd
   - r2.map_fd=1
   - r2.type=map_fd
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register map value
 
@@ -391,7 +392,7 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd
   - r2.svalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"
@@ -409,8 +410,8 @@ post:
   - r1.type=map_fd_programs
   - r2.map_fd=1
   - r2.type=map_fd_programs
-  - r1.svalue=r2.svalue
-  - r1.uvalue=r2.uvalue
+  - r2.svalue=r1.svalue
+  - r2.uvalue=r1.uvalue
 ---
 test-case: 32-bit assign register map programs value
 
@@ -424,7 +425,7 @@ post:
   - r1.map_fd=1
   - r1.type=map_fd_programs
   - r2.svalue=[0, 4294967295]
-  - r2.svalue=r2.uvalue
+  - r2.uvalue=r2.svalue
 
 messages:
   - "0: Invalid type (r1.type == number)"