Merge pull request #2003 from tautschnig/bitfield-offset

[SV-COMP'18 14/19] Fixing member offset computation in presence of bitfields.

Author: Daniel Kroening

regression/cbmc/Bitfields3/main.c

@@ -0,0 +1,53 @@
+#include <stdlib.h>
+#include <assert.h>
+
+#pragma pack(1)
+struct A
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c : 2;
+  unsigned char d;
+};
+
+struct B
+{
+  unsigned char a;
+  unsigned char b : 2;
+  unsigned char c;
+  unsigned char d : 2;
+};
+
+struct C
+{
+  unsigned char a;
+  unsigned char b : 4;
+  unsigned char c : 4;
+  unsigned char d;
+};
+#pragma pack()
+
+int main(void)
+{
+  assert(sizeof(struct A) == 3);
+  struct A *p = malloc(3);
+  assert((unsigned char *)p + 2 == &(p->d));
+  p->c = 3;
+  if(p->c != 3)
+  {
+    free(p);
+  }
+  free(p);
+
+  assert(sizeof(struct B) == 4);
+  struct B *pb = malloc(4);
+  assert((unsigned char *)pb + 2 == &(pb->c));
+  free(pb);
+
+  assert(sizeof(struct C) == 3);
+  struct C *pc = malloc(3);
+  assert((unsigned char *)pc + 2 == &(pc->d));
+  free(pc);
+
+  return 0;
+}

regression/cbmc/Bitfields3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/padding.cpp

@@ -199,16 +199,19 @@ void add_padding(struct_typet &type, const namespacet &ns)
           max_alignment=a;
 
         std::size_t w=to_c_bit_field_type(it_type).get_width();
-        std::size_t bytes;
-        for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
-        bit_field_bits-=w;
+        bit_field_bits += w;
+        const std::size_t bytes = bit_field_bits / 8;
+        bit_field_bits %= 8;
         offset+=bytes;
         continue;
       }
     }
     else
       a=alignment(it_type, ns);
 
+    DATA_INVARIANT(
+      bit_field_bits == 0, "padding ensures offset at byte boundaries");
+
     // check minimum alignment
     if(a<config.ansi_c.alignment && !packed)
       a=config.ansi_c.alignment;
@@ -246,12 +249,6 @@ void add_padding(struct_typet &type, const namespacet &ns)
       offset+=size;
   }
 
-  if(bit_field_bits!=0)
-  {
-    // these are now assumed to be multiples of 8
-    offset+=bit_field_bits/8;
-  }
-
   // any explicit alignment for the struct?
   if(type.find(ID_C_alignment).is_not_nil())
   {

src/util/pointer_offset_size.cpp

@@ -42,11 +42,14 @@ member_offset_iterator &member_offset_iterator::operator++()
     {
       // take the extra bytes needed
       std::size_t w=to_c_bit_field_type(comp.type()).get_width();
-      for(; w>bit_field_bits; ++current.second, bit_field_bits+=8) {}
-      bit_field_bits-=w;
+      bit_field_bits += w;
+      current.second += bit_field_bits / 8;
+      bit_field_bits %= 8;
     }
     else
     {
+      DATA_INVARIANT(
+        bit_field_bits == 0, "padding ensures offset at byte boundaries");
       const typet &subtype=comp.type();
       mp_integer sub_size=pointer_offset_size(subtype, ns);
       if(sub_size==-1)
@@ -287,13 +290,15 @@ exprt member_offset_expr(
     if(it->type().id()==ID_c_bit_field)
     {
       std::size_t w=to_c_bit_field_type(it->type()).get_width();
-      std::size_t bytes;
-      for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
-      bit_field_bits-=w;
+      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()));
     }
     else
     {
+      DATA_INVARIANT(
+        bit_field_bits == 0, "padding ensures offset at byte boundaries");
       const typet &subtype=it->type();
       exprt sub_size=size_of_expr(subtype, ns);
       if(sub_size.is_nil())
@@ -381,13 +386,15 @@ exprt size_of_expr(
       if(it->type().id()==ID_c_bit_field)
       {
         std::size_t w=to_c_bit_field_type(it->type()).get_width();
-        std::size_t bytes;
-        for(bytes=0; w>bit_field_bits; ++bytes, bit_field_bits+=8) {}
-        bit_field_bits-=w;
+        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()));
       }
       else
       {
+        DATA_INVARIANT(
+          bit_field_bits == 0, "padding ensures offset at byte boundaries");
         const typet &subtype=it->type();
         exprt sub_size=size_of_expr(subtype, ns);
         if(sub_size.is_nil())