From 495f109a6448c334b281fdfc0fd73de12a0aa064 Mon Sep 17 00:00:00 2001
From: Marek Trtik <marek.trtik@diffblue.com>
Date: Wed, 22 Nov 2017 10:53:54 +0000
Subject: [PATCH] Fixing member offset computation in presence of bitfields

The previous algorithm correctly identified the offset of the next non-bitfield
member, but would fail on consecutive bit-fields (fitting in one byte) as the
offset was eagerly incremented. Also cleanup this computation in all places that
used a similar algorithm.
---
 regression/cbmc/Bitfields3/main.c    | 53 ++++++++++++++++++++++++++++
 regression/cbmc/Bitfields3/test.desc |  8 +++++
 src/ansi-c/padding.cpp               | 15 ++++----
 src/util/pointer_offset_size.cpp     | 23 +++++++-----
 4 files changed, 82 insertions(+), 17 deletions(-)
 create mode 100644 regression/cbmc/Bitfields3/main.c
 create mode 100644 regression/cbmc/Bitfields3/test.desc

diff --git a/regression/cbmc/Bitfields3/main.c b/regression/cbmc/Bitfields3/main.c
new file mode 100644
index 00000000000..c3aa64072cb
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
new file mode 100644
index 00000000000..96c9b4bcd7b
--- /dev/null
+++ b/regression/cbmc/Bitfields3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index 3b87a6190d8..3139df62e52 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -199,9 +199,9 @@ 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;
       }
@@ -209,6 +209,9 @@ void add_padding(struct_typet &type, const namespacet &ns)
     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())
   {
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 27104f2292c..21dbdbb23f7 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/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())