Evaluating sizeof over __CPROVER_bool requires special cases

__CPROVER_bool is just a single bit, and not part of any language standard
describing the semantics of sizeof. We can declare arrays of __CPROVER_bool,
which will thus have elements that are not aligned on byte boundaries. Using
sizeof with such an array thus requires specific handling.

Author: tautschnig

regression/ansi-c/cprover_bool1/main.c

@@ -0,0 +1,46 @@
+#define STATIC_ASSERT(condition) int some_array##__LINE__[(condition) ? 1 : -1]
+
+struct bits
+{
+  __CPROVER_bool b1;
+  __CPROVER_bool b2;
+  __CPROVER_bool b3;
+  __CPROVER_bool b4;
+  __CPROVER_bool b5;
+  __CPROVER_bool b6;
+  __CPROVER_bool b7;
+  __CPROVER_bool b8;
+  int i;
+};
+
+STATIC_ASSERT(sizeof(struct bits) == 2 * sizeof(int));
+
+#include <limits.h>
+
+#if CHAR_BIT >= 8
+#pragma pack(1)
+struct packed_bits
+{
+  __CPROVER_bool b1;
+  __CPROVER_bool b2;
+  __CPROVER_bool b3;
+  __CPROVER_bool b4;
+  __CPROVER_bool b5;
+  __CPROVER_bool b6;
+  __CPROVER_bool b7;
+  __CPROVER_bool b8;
+  int i;
+};
+#pragma pack()
+
+STATIC_ASSERT(sizeof(struct packed_bits) == sizeof(int) + 1);
+#endif
+
+// a _Bool is at least one byte wide
+STATIC_ASSERT(sizeof(_Bool[CHAR_BIT]) >= CHAR_BIT);
+// __CPROVER_bool is just a single bit
+STATIC_ASSERT(sizeof(__CPROVER_bool[CHAR_BIT]) == 1);
+
+int main()
+{
+}

regression/ansi-c/cprover_bool1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

src/ansi-c/c_typecheck_expr.cpp

@@ -977,7 +977,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
 
   exprt new_expr;
 
-  if(type.id()==ID_c_bit_field)
+  if(type.id() == ID_c_bit_field || type.id() == ID_bool)
   {
     err_location(expr);
     error() << "sizeof cannot be applied to bit fields" << eom;
@@ -1731,7 +1731,7 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
 
   exprt &op=expr.op0();
 
-  if(op.type().id()==ID_c_bit_field)
+  if(op.type().id() == ID_c_bit_field || op.type().id() == ID_bool)
   {
     err_location(expr);
     error() << "cannot take address of a bit field" << eom;

src/ansi-c/padding.cpp

@@ -226,6 +226,10 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
         const auto width = to_c_bit_field_type(it->type()).get_width();
         bit_field_bits += width;
       }
+      else if(it->type().id() == ID_bool)
+      {
+        ++bit_field_bits;
+      }
       else
       {
         // keep track of offset
@@ -281,6 +285,10 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
         const std::size_t width = to_c_bit_field_type(it->type()).get_width();
         bit_field_bits+=width;
       }
+      else if(it->type().id() == ID_bool)
+      {
+        ++bit_field_bits;
+      }
       else if(bit_field_bits!=0)
       {
         // not on a byte-boundary?
@@ -347,6 +355,18 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
         continue;
       }
     }
+    else if(it_type.id() == ID_bool)
+    {
+      a = alignment(it_type, ns);
+      if(max_alignment < a)
+        max_alignment = a;
+
+      ++bit_field_bits;
+      const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
+      offset += bytes;
+      continue;
+    }
     else
       a=alignment(it_type, ns);
 

src/util/pointer_offset_size.cpp

@@ -290,6 +290,13 @@ exprt member_offset_expr(
       bit_field_bits %= 8;
       result=plus_exprt(result, from_integer(bytes, result.type()));
     }
+    else if(c.type().id() == ID_bool)
+    {
+      ++bit_field_bits;
+      const std::size_t bytes = bit_field_bits / 8;
+      bit_field_bits %= 8;
+      result = plus_exprt(result, from_integer(bytes, result.type()));
+    }
     else
     {
       DATA_INVARIANT(
@@ -315,6 +322,15 @@ exprt size_of_expr(
   {
     const auto &array_type = to_array_type(type);
 
+    // special-case arrays of bits
+    if(array_type.subtype().id() == ID_bool)
+    {
+      auto bits = pointer_offset_bits(array_type, ns);
+
+      if(bits.has_value())
+        return from_integer((*bits + 7) / 8, size_type());
+    }
+
     exprt sub = size_of_expr(array_type.subtype(), ns);
     if(sub.is_nil())
       return nil_exprt();
@@ -335,7 +351,18 @@ exprt size_of_expr(
   }
   else if(type.id()==ID_vector)
   {
-    exprt sub = size_of_expr(to_vector_type(type).subtype(), ns);
+    const auto &vector_type = to_vector_type(type);
+
+    // special-case vectors of bits
+    if(vector_type.subtype().id() == ID_bool)
+    {
+      auto bits = pointer_offset_bits(vector_type, ns);
+
+      if(bits.has_value())
+        return from_integer((*bits + 7) / 8, size_type());
+    }
+
+    exprt sub = size_of_expr(vector_type.subtype(), ns);
     if(sub.is_nil())
       return nil_exprt();
 
@@ -383,6 +410,13 @@ exprt size_of_expr(
         bit_field_bits %= 8;
         result=plus_exprt(result, from_integer(bytes, result.type()));
       }
+      else if(c.type().id() == ID_bool)
+      {
+        ++bit_field_bits;
+        const std::size_t bytes = bit_field_bits / 8;
+        bit_field_bits %= 8;
+        result = plus_exprt(result, from_integer(bytes, result.type()));
+      }
       else
       {
         DATA_INVARIANT(

src/util/simplify_expr.cpp

@@ -1982,10 +1982,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
       {
         const struct_typet &struct_type=to_struct_type(tp);
         const irep_idt &component_name=with.where().get(ID_component_name);
+        const typet &c_type = struct_type.get_component(component_name).type();
 
         // is this a bit field?
-        if(struct_type.get_component(component_name).type().id()==
-           ID_c_bit_field)
+        if(c_type.id() == ID_c_bit_field || c_type.id() == ID_bool)
         {
           // don't touch -- might not be byte-aligned
         }

src/util/simplify_expr_struct.cpp

@@ -152,8 +152,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
       const struct_typet::componentt &component=
         struct_type.get_component(component_name);
 
-      if(component.is_nil() || component.type().id()==ID_c_bit_field)
+      if(
+        component.is_nil() || component.type().id() == ID_c_bit_field ||
+        component.type().id() == ID_bool)
+      {
         return true;
+      }
 
       // add member offset to index
       auto offset_int = member_offset(struct_type, component_name, ns);