Byte update lowering: make array update tails conditional

When updating an array/vector at a non-constant byte offset the update
value may affect multiple array/vector elements. The last such element
needs to be updated with however many bytes have not yet been used from
the update value. With a non-constant byte offset the size of remaining
bytes may be zero. Therefore, make the tail update use symbolic offsets
rather than constants.

When fixing this, it also became apparent that we must not use byte
extracts of non-constant extraction size to build update elements.
Instead, the update offset should be non-constant, and will actually
need to be negative on such occasions.

Author: tautschnig

regression/cbmc/Array_operations2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-cprover-smt-backend
 main.c
 
 ^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$

src/solvers/lowering/byte_operators.cpp

@@ -1550,17 +1550,14 @@ static exprt lower_byte_update_array_vector_unbounded(
              plus_exprt{last_index, from_integer(1, last_index.type())}}};
 
   // The actual value of a partial update at the end.
-  exprt last_update_value = lower_byte_operators(
+  exprt last_update_value = lower_byte_update(
     byte_update_exprt{
       src.id(),
       index_exprt{src.op(), last_index},
-      from_integer(0, src.offset().type()),
-      byte_extract_exprt{extract_opcode,
-                         value_as_byte_array,
-                         mult_exprt{typecast_exprt::conditional_cast(
-                                      last_index, subtype_size.type()),
-                                    subtype_size},
-                         array_typet{bv_typet{8}, tail_size}}},
+      unary_minus_exprt{mult_exprt{
+        typecast_exprt::conditional_cast(last_index, subtype_size.type()),
+        subtype_size}},
+      value_as_byte_array},
     ns);
 
   if_exprt array_comprehension_body{
@@ -1601,10 +1598,6 @@ static exprt lower_byte_update_array_vector_non_const(
   const optionalt<exprt> &non_const_update_bound,
   const namespacet &ns)
 {
-  const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
-                                    ? ID_byte_extract_little_endian
-                                    : ID_byte_extract_big_endian;
-
   // do all arithmetic below using index/offset types - the array theory
   // back-end is really picky about indices having the same type
   auto subtype_size_opt = size_of_expr(subtype, ns);
@@ -1625,6 +1618,8 @@ static exprt lower_byte_update_array_vector_non_const(
 
   // compute the number of bytes (from the update value) that are going to be
   // consumed for updating the first element
+  const exprt update_size =
+    from_integer(value_as_byte_array.operands().size(), subtype_size.type());
   exprt initial_bytes = minus_exprt{subtype_size, update_offset};
   exprt update_bound;
   if(non_const_update_bound.has_value())
@@ -1637,26 +1632,23 @@ static exprt lower_byte_update_array_vector_non_const(
     DATA_INVARIANT(
       value_as_byte_array.id() == ID_array,
       "value should be an array expression if the update bound is constant");
-    update_bound =
-      from_integer(value_as_byte_array.operands().size(), initial_bytes.type());
+    update_bound = update_size;
   }
   initial_bytes =
     if_exprt{binary_predicate_exprt{initial_bytes, ID_lt, update_bound},
              initial_bytes,
              update_bound};
   simplify(initial_bytes, ns);
 
-  // encode the first update: update the original element at first_index with
-  // initial_bytes-many bytes extracted from value_as_byte_array
-  exprt first_update_value = lower_byte_operators(
+  // encode the first update: update the original element at first_index (the
+  // actual update will only be initial_bytes-many bytes from
+  // value_as_byte_array)
+  exprt first_update_value = lower_byte_update(
     byte_update_exprt{
       src.id(),
       index_exprt{src.op(), first_index},
       update_offset,
-      byte_extract_exprt{extract_opcode,
-                         value_as_byte_array,
-                         from_integer(0, src.offset().type()),
-                         array_typet{bv_typet{8}, initial_bytes}}},
+      value_as_byte_array},
     ns);
 
   if(value_as_byte_array.id() != ID_array)
@@ -1691,56 +1683,44 @@ static exprt lower_byte_update_array_vector_non_const(
 
   with_exprt result{src.op(), first_index, first_update_value};
 
-  std::size_t i = 1;
-  for(; offset + step_size <= value_as_byte_array.operands().size();
-      offset += step_size, ++i)
-  {
+  auto lower_byte_update_array_vector_non_const_one_element =
+    [&src,
+     &first_index,
+     &initial_bytes,
+     &subtype_size,
+     &value_as_byte_array,
+     &ns,
+     &result](std::size_t i) -> void {
     exprt where = simplify_expr(
       plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
 
-    exprt offset_expr = simplify_expr(
-      plus_exprt{
+    exprt neg_offset_expr = simplify_expr(
+      unary_minus_exprt{plus_exprt{
         initial_bytes,
-        mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}},
+        mult_exprt{subtype_size, from_integer(i - 1, subtype_size.type())}}},
       ns);
 
-    exprt element = lower_byte_operators(
+    exprt element = lower_byte_update(
       byte_update_exprt{
         src.id(),
         index_exprt{src.op(), where},
-        from_integer(0, src.offset().type()),
-        byte_extract_exprt{extract_opcode,
-                           value_as_byte_array,
-                           std::move(offset_expr),
-                           array_typet{bv_typet{8}, subtype_size}}},
+        neg_offset_expr,
+        value_as_byte_array},
       ns);
 
     result.add_to_operands(std::move(where), std::move(element));
+  };
+
+  std::size_t i = 1;
+  for(; offset + step_size <= value_as_byte_array.operands().size();
+      offset += step_size, ++i)
+  {
+    lower_byte_update_array_vector_non_const_one_element(i);
   }
 
   // do the tail
   if(offset < value_as_byte_array.operands().size())
-  {
-    const std::size_t tail_size =
-      value_as_byte_array.operands().size() - offset;
-
-    exprt where = simplify_expr(
-      plus_exprt{first_index, from_integer(i, first_index.type())}, ns);
-
-    exprt element = lower_byte_operators(
-      byte_update_exprt{
-        src.id(),
-        index_exprt{src.op(), where},
-        from_integer(0, src.offset().type()),
-        byte_extract_exprt{
-          extract_opcode,
-          value_as_byte_array,
-          from_integer(offset, src.offset().type()),
-          array_typet{bv_typet{8}, from_integer(tail_size, size_type())}}},
-      ns);
-
-    result.add_to_operands(std::move(where), std::move(element));
-  }
+    lower_byte_update_array_vector_non_const_one_element(i);
 
   return simplify_expr(std::move(result), ns);
 }
@@ -2218,11 +2198,17 @@ static exprt lower_byte_update(
     const binary_predicate_exprt offset_ge_zero{
       offset_times_eight, ID_ge, from_integer(0, offset_type)};
 
-    if_exprt mask_shifted{offset_ge_zero,
-                          shl_exprt{mask, offset_times_eight},
-                          lshr_exprt{mask, offset_times_eight}};
+    if_exprt mask_shifted{
+      offset_ge_zero,
+      shl_exprt{mask, offset_times_eight},
+      lshr_exprt{mask, unary_minus_exprt{offset_times_eight}}};
     if(!is_little_endian)
+    {
       mask_shifted.true_case().swap(mask_shifted.false_case());
+      to_shift_expr(mask_shifted.true_case())
+        .distance()
+        .swap(to_shift_expr(mask_shifted.false_case()).distance());
+    }
 
     // original_bits &= ~mask
     bitand_exprt bitand_expr{val_before, bitnot_exprt{mask_shifted}};
@@ -2249,11 +2235,17 @@ static exprt lower_byte_update(
       zero_extended = value;
 
     // shift the value
-    if_exprt value_shifted{offset_ge_zero,
-                           shl_exprt{zero_extended, offset_times_eight},
-                           lshr_exprt{zero_extended, offset_times_eight}};
+    if_exprt value_shifted{
+      offset_ge_zero,
+      shl_exprt{zero_extended, offset_times_eight},
+      lshr_exprt{zero_extended, unary_minus_exprt{offset_times_eight}}};
     if(!is_little_endian)
+    {
       value_shifted.true_case().swap(value_shifted.false_case());
+      to_shift_expr(value_shifted.true_case())
+        .distance()
+        .swap(to_shift_expr(value_shifted.false_case()).distance());
+    }
 
     // original_bits |= newvalue
     bitor_exprt bitor_expr{bitand_expr, value_shifted};