Byte-update lowering: handle sub-byte sized bit fields

Extend the value to be updated to the update size immediately to avoid
extractbits operations that attempt to extract bits that do not exist.

Fixes: #5389

Author: tautschnig

regression/cbmc/byte_update13/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <string.h>
+
+struct blob
+{
+  unsigned dummy;
+  unsigned bit : 1;
+};
+
+int main()
+{
+  struct blob b;
+  struct blob b1 = b;
+
+  if(b.dummy <= sizeof(struct blob))
+    memset(&b, 0, b.dummy);
+
+  assert(b1.dummy != sizeof(struct blob) || b.bit == 0);
+}

regression/cbmc/byte_update13/test.desc

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

src/solvers/lowering/byte_operators.cpp

@@ -2136,10 +2136,30 @@ static exprt lower_byte_update(
         instantiate_byte_array(value_as_byte_array, 0, (type_bits + 7) / 8, ns);
     }
 
+    const std::size_t update_size = update_bytes.size();
+    const std::size_t width = std::max(type_bits, update_size * 8);
+
+    const bool is_little_endian = src.id() == ID_byte_update_little_endian;
+
+    exprt val_before =
+      typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
+    if(width > type_bits)
+    {
+      val_before =
+        concatenation_exprt{from_integer(0, bv_typet{width - type_bits}),
+                            val_before,
+                            bv_typet{width}};
+
+      if(!is_little_endian)
+        to_concatenation_expr(val_before)
+          .op0()
+          .swap(to_concatenation_expr(val_before).op1());
+    }
+
     if(non_const_update_bound.has_value())
     {
       const exprt src_as_bytes = unpack_rec(
-        src.op(),
+        val_before,
         src.id() == ID_byte_update_little_endian,
         mp_integer{0},
         mp_integer{update_bytes.size()},
@@ -2158,11 +2178,6 @@ static exprt lower_byte_update(
       }
     }
 
-    const std::size_t update_size = update_bytes.size();
-    const std::size_t width = std::max(type_bits, update_size * 8);
-
-    const bool is_little_endian = src.id() == ID_byte_update_little_endian;
-
     // build mask
     exprt mask;
     if(is_little_endian)
@@ -2186,20 +2201,6 @@ static exprt lower_byte_update(
       mask_shifted.true_case().swap(mask_shifted.false_case());
 
     // original_bits &= ~mask
-    exprt val_before =
-      typecast_exprt::conditional_cast(src.op(), bv_typet{type_bits});
-    if(width > type_bits)
-    {
-      val_before =
-        concatenation_exprt{from_integer(0, bv_typet{width - type_bits}),
-                            val_before,
-                            bv_typet{width}};
-
-      if(!is_little_endian)
-        to_concatenation_expr(val_before)
-          .op0()
-          .swap(to_concatenation_expr(val_before).op1());
-    }
     bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
 
     // concatenate and zero-extend the value
@@ -2242,6 +2243,14 @@ static exprt lower_byte_update(
           src.type()),
         ns);
     }
+    else if(width > type_bits)
+    {
+      return simplify_expr(
+        typecast_exprt::conditional_cast(
+          extractbits_exprt{bitor_expr, type_bits - 1, 0, bv_typet{type_bits}},
+          src.type()),
+        ns);
+    }
 
     return simplify_expr(
       typecast_exprt::conditional_cast(bitor_expr, src.type()), ns);