Merge pull request #6448 from tautschnig/bit-updates

Byte updates using bit fields require extension to full bytes

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, kroening@kroening.com
 #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,59 @@ 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);
+    // If the following invariant fails, then the type was only found to be
+    // constant via simplification. Such instances should be fixed at the place
+    // introducing these constant-but-not-constant_exprt type sizes.
+    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}};
+    }
+    else
+    {
+      update_size_expr_opt =
+        from_integer(update_bits_int / 8, update_size_expr_opt->type());
+    }
+  }
 
   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}};