Merge pull request diffblue#3183 from tautschnig/cprover_bool-sizeof

tautschnig · web-flow · commit 7fd6f21a4aea · 2018-10-29T16:58:13.000Z
Evaluating sizeof over __CPROVER_bool requires special cases
diff --git a/regression/ansi-c/cprover_bool1/main.c b/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()
+{
+}
diff --git a/regression/ansi-c/cprover_bool1/test.desc b/regression/ansi-c/cprover_bool1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -985,6 +985,12 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
     error() << "sizeof cannot be applied to bit fields" << eom;
     throw 0;
   }
+  else if(type.id() == ID_bool)
+  {
+    err_location(expr);
+    error() << "sizeof cannot be applied to single bits" << eom;
+    throw 0;
+  }
   else if(type.id() == ID_empty)
   {
     // This is a gcc extension.
@@ -1740,6 +1746,13 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
     throw 0;
   }
 
+  if(op.type().id() == ID_bool)
+  {
+    err_location(expr);
+    error() << "cannot take address of a single bit" << eom;
+    throw 0;
+  }
+
   // special case: address of label
   if(op.id()==ID_label)
   {
diff --git a/src/ansi-c/padding.cpp b/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);
 
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
@@ -42,6 +42,12 @@ member_offset_iterator &member_offset_iterator::operator++()
       current.second += bit_field_bits / 8;
       bit_field_bits %= 8;
     }
+    else if(comp.type().id() == ID_bool)
+    {
+      ++bit_field_bits;
+      current.second += bit_field_bits / 8;
+      bit_field_bits %= 8;
+    }
     else
     {
       DATA_INVARIANT(
@@ -288,7 +294,16 @@ exprt member_offset_expr(
       bit_field_bits += w;
       const std::size_t bytes = bit_field_bits / 8;
       bit_field_bits %= 8;
-      result=plus_exprt(result, from_integer(bytes, result.type()));
+      if(bytes > 0)
+        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;
+      if(bytes > 0)
+        result = plus_exprt(result, from_integer(bytes, result.type()));
     }
     else
     {
@@ -315,6 +330,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 +359,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();
 
@@ -381,7 +416,16 @@ exprt size_of_expr(
         bit_field_bits += w;
         const std::size_t bytes = bit_field_bits / 8;
         bit_field_bits %= 8;
-        result=plus_exprt(result, from_integer(bytes, result.type()));
+        if(bytes > 0)
+          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;
+        if(bytes > 0)
+          result = plus_exprt(result, from_integer(bytes, result.type()));
       }
       else
       {
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -1947,10 +1947,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
         }
diff --git a/src/util/simplify_expr_struct.cpp b/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);

Original file line number	Diff line number	Diff line change
`@@ -1947,10 +1947,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)`
`1947`	`1947`	`{`
`1948`	`1948`	`const struct_typet &struct_type=to_struct_type(tp);`
`1949`	`1949`	`const irep_idt &component_name=with.where().get(ID_component_name);`
	`1950`	`+ const typet &c_type = struct_type.get_component(component_name).type();`
`1950`	`1951`
`1951`	`1952`	`// is this a bit field?`
`1952`		`- if(struct_type.get_component(component_name).type().id()==`
`1953`		`- ID_c_bit_field)`
	`1953`	`+ if(c_type.id() == ID_c_bit_field \|\| c_type.id() == ID_bool)`
`1954`	`1954`	`{`
`1955`	`1955`	`// don't touch -- might not be byte-aligned`
`1956`	`1956`	`}`