Fix extractbits invariant for non-byte-aligned bitfields

regression/cbmc/extractbits-bitfield-typecast/main.c

@@ -0,0 +1,14 @@
+// Regression test for issue #8581
+// When unpacking a non-byte-aligned bitfield into bytes, extractbits
+// operations were created that exceeded the source bitvector width.
+typedef a;
+union
+{
+  signed : 28;
+  signed : 25;
+  a *b;
+} c = {10};
+main()
+{
+  d();
+}

regression/cbmc/extractbits-bitfield-typecast/test.desc

@@ -0,0 +1,7 @@
+CORE paths-lifo-expected-failure
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/lower_byte_operators.cpp

@@ -1055,8 +1055,26 @@ static exprt unpack_rec(
       }
     }
 
-    auto const src_as_bitvector = typecast_exprt::conditional_cast(
-      src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
+    // When the source width is not a multiple of the byte size, round up
+    // to the next byte boundary and zero-extend the source so that all
+    // byte-sized extractbits operations remain within bounds.
+    const mp_integer padded_bits =
+      total_bits % bits_per_byte == 0
+        ? total_bits
+        : total_bits + bits_per_byte - total_bits % bits_per_byte;
+    exprt src_as_bitvector;
+    if(padded_bits > total_bits)
+    {
+      src_as_bitvector = zero_extend_exprt{
+        typecast_exprt::conditional_cast(
+          src, bv_typet{numeric_cast_v<std::size_t>(total_bits)}),
+        bv_typet{numeric_cast_v<std::size_t>(padded_bits)}};
+    }
+    else
+    {
+      src_as_bitvector = typecast_exprt::conditional_cast(
+        src, bv_typet{numeric_cast_v<std::size_t>(total_bits)});
+    }
     auto const byte_type = bv_typet{bits_per_byte};
     exprt::operandst byte_operands;
     array_typet array_type{