Fix unpack_array_vector to produce an array of bytes

We wrongly created a return type (though not the underlying expression,
which was correct!) as an array of elements of the original subtype,
even though the sole purpose of unpack_array_vector is to turn the
original subtype into a sequence of bytes.

We seemingly neither had a test covering this code nor did we have
additional result verification in place. Both are now rectified: a new
regression test is added, and an invariant is checked right after
returning from unpack_rec (which may invoke unpack_array_vector).

Fixes: #5718

Author: tautschnig

regression/cbmc-library/memcpy-08/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+#include <string.h>
+
+int __VERIFIER_nondet_int();
+
+void main()
+{
+  size_t size;
+  __CPROVER_assume(size >= 2);
+  // limit the size to ensure size * sizeof(int) wouldn't overflow, and we don't
+  // reach the maximum object size
+  __CPROVER_assume(size <= 1000);
+
+  int *dest_buffer = malloc(size * sizeof(int));
+  int *src_buffer = malloc(size * sizeof(int));
+  src_buffer[0] = 42;
+  src_buffer[1] = __VERIFIER_nondet_int();
+
+  memcpy(dest_buffer, src_buffer, size * sizeof(int));
+  __CPROVER_assert(dest_buffer[0] == 42, "should pass");
+  __CPROVER_assert(dest_buffer[1] == 42, "should fail");
+}

regression/cbmc-library/memcpy-08/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\[main.assertion.1\] line 20 should pass: SUCCESS$
+^\[main.assertion.2\] line 21 should fail: FAILURE$
+^\*\* 1 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/solvers/lowering/byte_operators.cpp

@@ -476,23 +476,21 @@ static exprt unpack_array_vector(
     }
 
     optionalt<exprt> array_vector_size;
-    optionalt<typet> subtype;
     if(src.type().id() == ID_vector)
     {
       array_vector_size = to_vector_type(src.type()).size();
-      subtype = to_vector_type(src.type()).subtype();
     }
     else
     {
       array_vector_size = to_array_type(src.type()).size();
-      subtype = to_array_type(src.type()).subtype();
     }
 
+
     return array_comprehension_exprt{
       std::move(array_comprehension_index),
       std::move(body),
       array_typet{
-        *subtype,
+        bv_typet{8},
         mult_exprt{*array_vector_size,
                    from_integer(el_bytes, array_vector_size->type())}}};
   }
@@ -1034,6 +1032,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
   byte_extract_exprt unpacked(src);
   unpacked.op() = unpack_rec(
     src.op(), little_endian, lower_bound_int_opt, upper_bound_int_opt, ns);
+  CHECK_RETURN(
+    to_bitvector_type(to_type_with_subtype(unpacked.op().type()).subtype())
+      .get_width() == 8);
 
   if(src.type().id()==ID_array)
   {