Merge pull request #1814 from goblint/bitfield-cast-bool

Fix bitfield `_Bool` casts

Author: sim642

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

@@ -281,6 +281,25 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in
     (norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
+  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
+    if ik = GoblintCil.IBool then (
+      let may_zero =
+        if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
+          BArith.zero
+        else
+          bot () (* must be non-zero, so may not be zero *)
+      in
+      let may_one =
+        if Ints_t.equal o BArith.zero_mask then (* one bit may be in no position (zero_mask) *)
+          bot () (* must be zero, so may not be one *)
+        else
+          BArith.one
+      in
+      (BArith.join may_zero may_one, {underflow=false; overflow=false})
+    )
+    else
+      cast_to ~suppress_ovwarn ?torg ~no_ov ik (z,o)
+
   let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
 
   let meet ik x y = norm ik @@ (BArith.meet x y)

tests/regression/83-bitfield/14-bool.c

@@ -0,0 +1,38 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.bitfield
+#include <goblint.h>
+
+int main() {
+  int i1 = 1;
+  int i123 = 123;
+  int im123 = -123;
+  int i128 = 128;
+  int im128 = -128;
+  int i0 = 0;
+  int irand; // rand
+
+  // assigning constant from other variable instead of integer constant, because integer constant swallows implicit cast to _Bool
+  _Bool b1 = i1;
+  _Bool b123 = i123; // NOWARN (overflow)
+  _Bool bm123 = im123; // NOWARN (underflow)
+  _Bool b128 = i128; // NOWARN (overflow)
+  _Bool bm128 = im128; // NOWARN (underflow)
+  _Bool bf = i0;
+  _Bool brand = irand; // NOWARN (underflow, overflow)
+
+  __goblint_check(b1);
+  __goblint_check(b1 == 1);
+  __goblint_check(b123);
+  __goblint_check(b123 == 1);
+  __goblint_check(bm123);
+  __goblint_check(bm123 == 1);
+  __goblint_check(b128);
+  __goblint_check(b128 == 1);
+  __goblint_check(bm128);
+  __goblint_check(bm128 == 1);
+  __goblint_check(!bf);
+  __goblint_check(bf == 0);
+  __goblint_check(brand); // UNKNOWN!
+  __goblint_check(brand == 0); // UNKNOWN!
+  __goblint_check(brand == 1); // UNKNOWN!
+  return 0;
+}