Merge pull request #5750 from tautschnig/fix-5718

Fix unpack_array_vector to produce an array of bytes

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

@@ -475,26 +475,17 @@ static exprt unpack_array_vector(
         body};
     }
 
-    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();
-    }
+    const exprt array_vector_size = src.type().id() == ID_vector
+                                      ? to_vector_type(src.type()).size()
+                                      : to_array_type(src.type()).size();
 
     return array_comprehension_exprt{
       std::move(array_comprehension_index),
       std::move(body),
       array_typet{
-        *subtype,
-        mult_exprt{*array_vector_size,
-                   from_integer(el_bytes, array_vector_size->type())}}};
+        bv_typet{8},
+        mult_exprt{array_vector_size,
+                   from_integer(el_bytes, array_vector_size.type())}}};
   }
 
   exprt::operandst byte_operands;
@@ -1034,6 +1025,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)
   {