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.t

@@ -4,7 +4,7 @@
     dead: 0
     total lines: 3
   [Info][Witness] witness generation summary:
-    location invariants: 6
+    location invariants: 3
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -41,30 +41,3 @@ With 4 equal variables, there should be just 3 var_eq invariants, not 6.
           function: main
         value: a == d
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 71-var_eq-invariants.c
-          line: 6
-          column: 3
-          function: main
-        value: b == c
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 71-var_eq-invariants.c
-          line: 6
-          column: 3
-          function: main
-        value: b == d
-        format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 71-var_eq-invariants.c
-          line: 6
-          column: 3
-          function: main
-        value: c == d
-        format: c_expression