Byte updates using bit fields require extension to full bytes

A byte update with an update value that has a size that's not a multiple
of bytes must not overwrite bits that are not in the update value. We
previously generated extractbits expressions that would go out of
bounds, which tripped up the SMT solvers. No longer generating these
out-of-bounds expressions makes the SMT solvers happy on the Promotion3
test, which exercised this feature.

Author: tautschnig

regression/cbmc/Promotion3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/havoc_slice/test_struct_b_slice.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 test_struct_b_slice.c
 
 ^EXIT=10$

src/goto-programs/builtin_functions.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/prefix.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
+#include <util/simplify_expr.h>
 #include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
@@ -699,7 +700,7 @@ void goto_convertt::do_havoc_slice(
   t->source_location_nonconst().set_comment(
     "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
 
-  const array_typet array_type(char_type(), arguments[1]);
+  const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
 
   const symbolt &nondet_contents =
     new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);

src/solvers/lowering/byte_operators.cpp

@@ -2278,20 +2278,51 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
   // place.
   // 4) Construct a new object.
   optionalt<exprt> non_const_update_bound;
-  auto update_size_expr_opt = size_of_expr(src.value().type(), ns);
+  // update value, may require extension to full bytes
+  exprt update_value = src.value();
+  auto update_size_expr_opt = size_of_expr(update_value.type(), ns);
   CHECK_RETURN(update_size_expr_opt.has_value());
   simplify(update_size_expr_opt.value(), ns);
 
   if(!update_size_expr_opt.value().is_constant())
     non_const_update_bound = *update_size_expr_opt;
+  else
+  {
+    auto update_bits = pointer_offset_bits(update_value.type(), ns);
+    DATA_INVARIANT(
+      update_bits.has_value(), "constant size-of should imply fixed bit width");
+    const size_t update_bits_int = numeric_cast_v<size_t>(*update_bits);
+
+    if(update_bits_int % 8 != 0)
+    {
+      DATA_INVARIANT(
+        can_cast_type<bitvector_typet>(update_value.type()),
+        "non-byte aligned type expected to be a bitvector type");
+      size_t n_extra_bits = 8 - update_bits_int % 8;
+
+      endianness_mapt endianness_map(
+        src.op().type(), src.id() == ID_byte_update_little_endian, ns);
+      const auto bounds = map_bounds(
+        endianness_map, update_bits_int, update_bits_int + n_extra_bits - 1);
+      extractbits_exprt extra_bits{
+        src.op(), bounds.ub, bounds.lb, bv_typet{n_extra_bits}};
+
+      update_value =
+        concatenation_exprt{typecast_exprt::conditional_cast(
+                              update_value, bv_typet{update_bits_int}),
+                            extra_bits,
+                            bitvector_typet{update_value.type().id(),
+                                            update_bits_int + n_extra_bits}};
+    }
+  }
 
   const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
                                     ? ID_byte_extract_little_endian
                                     : ID_byte_extract_big_endian;
 
   const byte_extract_exprt byte_extract_expr{
     extract_opcode,
-    src.value(),
+    update_value,
     from_integer(0, src.offset().type()),
     array_typet{bv_typet{8}, *update_size_expr_opt}};