Merge pull request #1826 from goblint/var_eq-invariant

Reduce var_eq witness invariants from quadratic to linear

Author: sim642

src/analyses/varEq.ml

@@ -21,18 +21,23 @@ struct
       fold (fun s a ->
           if B.mem MyCFG.unknown_exp s then
             a
-          else
-            let module B_prod = BatSet.Make2 (Exp) (Exp) in
-            let s_prod = B_prod.cartesian_product s s in
-            let i = B_prod.Product.fold (fun (x, y) a ->
-                if Exp.compare x y < 0 && not (InvariantCil.exp_contains_tmp x) && not (InvariantCil.exp_contains_tmp y) && InvariantCil.exp_is_in_scope scope x && InvariantCil.exp_is_in_scope scope y then (* each equality only one way, no self-equalities *)
-                  let eq = BinOp (Eq, x, y, intType) in
+          else (
+            let s' = B.filter (fun x -> not (InvariantCil.exp_contains_tmp x) && InvariantCil.exp_is_in_scope scope x) s in
+            if B.cardinal s' >= 2 then (
+              (* instead of returning quadratically many pairwise equalities from a cluster,
+                 output linear number of equalities with just one expression *)
+              let lhs = B.choose s' in (* choose arbitrary expression for lhs *)
+              let rhss = B.remove lhs s' in (* and exclude it from rhs-s (no point in reflexive equality) *)
+              let i = B.fold (fun rhs a ->
+                  let eq = BinOp (Eq, lhs, rhs, intType) in
                   Invariant.(a && of_exp eq)
-                else
-                  a
-              ) s_prod (Invariant.top ())
-            in
-            Invariant.(a && i)
+                ) rhss (Invariant.top ())
+              in
+              Invariant.(a && i)
+            )
+            else (* cannot output any equalities between just 0 or 1 usable expressions *)
+              a
+          )
         ) ss (Invariant.top ())
   end
 

tests/regression/56-witness/71-var_eq-invariants.c

@@ -0,0 +1,7 @@
+// CRAM
+
+int main() {
+  int a, b, c, d;
+  a = b = c = d;
+  return 0;
+}

tests/regression/56-witness/71-var_eq-invariants.t

@@ -0,0 +1,43 @@
+  $ goblint --set ana.activated[+] var_eq --enable witness.yaml.enabled 71-var_eq-invariants.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 3
+    dead: 0
+    total lines: 3
+  [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+With 4 equal variables, there should be just 3 var_eq invariants, not 6.
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 71-var_eq-invariants.c
+          line: 6
+          column: 3
+          function: main
+        value: a == b
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 71-var_eq-invariants.c
+          line: 6
+          column: 3
+          function: main
+        value: a == c
+        format: c_expression
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 71-var_eq-invariants.c
+          line: 6
+          column: 3
+          function: main
+        value: a == d
+        format: c_expression