Fix bitfield domain producing trivial witness invariants

Author: sim642

src/cdomain/value/cdomains/int/bitfieldDomain.ml

@@ -624,19 +624,32 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   (* Invariant *)
 
-  let invariant_ikind e ik (z,o) =
-    if z =: BArith.one_mask && o =: BArith.one_mask then
-      Invariant.top ()
-    else if  BArith.is_invalid (z,o) then
-      Invariant.none
-    else
+  let invariant_ikind e ik (z, o) =
+    if BArith.is_invalid (z, o) then
+      Invariant.none (* TODO: should this ever even happen? *)
+    else (
       let open GoblintCil.Cil in
-      let def0 = z &: (!: o) in
-      let def1 = o &: (!: z) in
-      let (def0, def1) = BatTuple.Tuple2.mapn (kintegerCilint ik) (Ints_t.to_bigint def0, Ints_t.to_bigint def1) in
-      let exp0 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, (UnOp (BNot, e, TInt(ik,[]))), def0, TInt(ik,[]))), def0, intType)) in
-      let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in
-      Invariant.meet exp0 exp1
+      let ik_type = TInt (ik, []) in
+      let i1 =
+        let def0 = z &: (!: o) in
+        if def0 =: BArith.zero_mask then
+          Invariant.none
+        else (
+          let def0 = kintegerCilint ik (Ints_t.to_bigint def0) in
+          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, UnOp (BNot, e, ik_type), def0, ik_type)), def0, intType))
+        )
+      in
+      let i2 =
+        let def1 = o &: (!: z) in
+        if def1 =: BArith.zero_mask then
+          Invariant.none
+        else (
+          let def1 = kintegerCilint ik (Ints_t.to_bigint def1) in
+          Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, ik_type)), def1, intType))
+        )
+      in
+      Invariant.(i1 && i2)
+    )
 
   let starting ik n =
     let (min_ik, max_ik) = Size.range ik in

tests/regression/56-witness/46-top-bool-invariant.t

@@ -154,7 +154,7 @@ bitfield only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
-    location invariants: 4
+    location invariants: 3
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -171,15 +171,6 @@ bitfield only:
           function: main
         value: (_Bool)0 <= x
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 46-top-bool-invariant.c
-          line: 5
-          column: 3
-          function: main
-        value: (x & (_Bool)0) == (_Bool)0
-        format: c_expression
     - invariant:
         type: location_invariant
         location:

tests/regression/83-bitfield/00-simple-demo.t

@@ -5,7 +5,7 @@
     dead: 0
     total lines: 13
   [Info][Witness] witness generation summary:
-    location invariants: 26
+    location invariants: 24
     loop invariants: 0
     flow-insensitive invariants: 0
     total generation entries: 1
@@ -157,15 +157,6 @@
           function: main
         value: testvar == 235
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 00-simple-demo.c
-          line: 28
-          column: 3
-          function: main
-        value: (state & 0) == 0
-        format: c_expression
     - invariant:
         type: location_invariant
         location:
@@ -202,15 +193,6 @@
           function: main
         value: testvar == 1
         format: c_expression
-    - invariant:
-        type: location_invariant
-        location:
-          file_name: 00-simple-demo.c
-          line: 29
-          column: 1
-          function: main
-        value: (state & 0) == 0
-        format: c_expression
     - invariant:
         type: location_invariant
         location:

tests/regression/83-bitfield/15-svcomp-sum03-2.t

@@ -11,49 +11,13 @@
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (15-svcomp-sum03-2.c:10:9-10:10)
   [Info][Witness] witness generation summary:
     location invariants: 0
-    loop invariants: 8
+    loop invariants: 4
     flow-insensitive invariants: 0
     total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: invariant_set
     content:
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 15-svcomp-sum03-2.c
-          line: 10
-          column: 3
-          function: main
-        value: (loop1 & 0U) == 0U
-        format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 15-svcomp-sum03-2.c
-          line: 10
-          column: 3
-          function: main
-        value: (n1 & 0U) == 0U
-        format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 15-svcomp-sum03-2.c
-          line: 10
-          column: 3
-          function: main
-        value: (sn & 0U) == 0U
-        format: c_expression
-    - invariant:
-        type: loop_invariant
-        location:
-          file_name: 15-svcomp-sum03-2.c
-          line: 10
-          column: 3
-          function: main
-        value: (x & 0U) == 0U
-        format: c_expression
     - invariant:
         type: loop_invariant
         location:

tests/regression/witness/int.t/run.t

@@ -31,8 +31,7 @@
           line: 12
           column: 5
           function: main
-        value: (51 <= i && i <= 99) && ((~ i & (-0x7FFFFFFF-1)) == (-0x7FFFFFFF-1) &&
-          (i & 0) == 0)
+        value: (51 <= i && i <= 99) && (~ i & (-0x7FFFFFFF-1)) == (-0x7FFFFFFF-1)
         format: c_expression
     - invariant:
         type: location_invariant