Fix bitfield witness invariants for _Bool and unsigned types

Author: sim642

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

@@ -635,17 +635,27 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type 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, e, def0, ik_type)), kintegerCilint ik Z.zero, intType))
+          let def0 = Ints_t.to_bigint def0 in
+          if fitsInInt ik def0 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
+            let def0 = kintegerCilint ik def0 in
+            Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def0, ik_type)), kintegerCilint ik Z.zero, intType))
+          )
+          else
+            Invariant.none
         )
       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))
+          let def1 = Ints_t.to_bigint def1 in
+          if fitsInInt ik def1 then ( (* At least for _Bool and unsigned types, kintegerCilint can give an incorrect mask if doesn't fit. See https://github.com/goblint/analyzer/pull/1897/changes#r2610251390. *)
+            let def1 = kintegerCilint ik def1 in
+            Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, ik_type)), def1, intType))
+          )
+          else
+            Invariant.none
         )
       in
       Invariant.(i1 && i2)

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: 3
+    location invariants: 2
     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)1) == (_Bool)0
-        format: c_expression
     - invariant:
         type: location_invariant
         location:

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

@@ -11,46 +11,10 @@
   [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: 4
+    loop invariants: 0
     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
+    content: []