Merge pull request #1897 from goblint/witness-invariant-bitfield

Simplify witness invariants for bitfield domain

Author: sim642

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

@@ -624,19 +624,39 @@ 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 open GoblintCil.Cil in
+  let invariant_ikind e ik (z, o) =
+    assert (not (BArith.is_invalid (z, o)));
+    let open GoblintCil.Cil in
+    let ik_type = TInt (ik, []) in
+    let i1 =
       let def0 = z &: (!: o) in
+      if def0 =: BArith.zero_mask then
+        Invariant.none
+      else (
+        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
-      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
+      if def1 =: BArith.zero_mask then
+        Invariant.none
+      else (
+        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)
 
   let starting ik n =
     let (min_ik, max_ik) = Size.range ik in

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

@@ -1,6 +1,6 @@
 def_exc only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -35,7 +35,7 @@ def_exc only:
 
 interval only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -70,7 +70,7 @@ interval only:
 
 enums only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -96,7 +96,7 @@ enums only:
 
 congruence only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -113,7 +113,42 @@ congruence only:
 
 interval_set only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set --disable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: location_invariant
+        location:
+          file_name: 46-top-bool-invariant.c
+          line: 5
+          column: 3
+          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
+        format: c_expression
+
+bitfield only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --enable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -148,7 +183,7 @@ interval_set only:
 
 all:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --enable ana.int.bitfield 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -174,7 +209,7 @@ all:
 
 all without inexact-type-bounds:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --disable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --enable ana.int.bitfield 46-top-bool-invariant.c --disable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0

tests/regression/56-witness/47-top-int-invariant.t

@@ -1,6 +1,6 @@
 def_exc only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -35,7 +35,7 @@ def_exc only:
 
 interval only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -70,7 +70,7 @@ interval only:
 
 enums only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -105,7 +105,7 @@ enums only:
 
 congruence only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set --disable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -122,7 +122,7 @@ congruence only:
 
 interval_set only:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set --disable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -155,9 +155,26 @@ interval_set only:
         value: x <= 2147483647
         format: c_expression
 
+bitfield only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set --enable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content: []
+
 all:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --enable ana.int.bitfield 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
@@ -192,7 +209,7 @@ all:
 
 all without inexact-type-bounds:
 
-  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --disable witness.invariant.inexact-type-bounds
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.invariant-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --enable ana.int.bitfield 47-top-int-invariant.c --disable witness.invariant.inexact-type-bounds
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0