Merge pull request #3974 from tautschnig/simplify-byte-extract-ext

Simplify byte_extract(constant, o, t) when sizeof(t) < sizeof(constant)

Author: tautschnig

regression/cbmc-library/memmove-01/constant.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+#include <stdio.h>
+#include <string.h>
+
+void sort_items_by_criteria(int *item, int left, int right)
+{
+  int lidx = left, ridx = (left + right) / 2 + 1,
+      lsize = (left + right) / 2 - left + 1;
+  int tmp;
+
+  if(right - left < 1)
+    return;
+  sort_items_by_criteria(item, left, (left + right) / 2);
+  sort_items_by_criteria(item, (left + right) / 2 + 1, right);
+
+  while(ridx <= right && lidx < ridx)
+  {
+    if(item[lidx] > item[ridx])
+    {
+      tmp = item[ridx];
+      memmove(item + lidx + 1, item + lidx, lsize * sizeof(int));
+      item[lidx] = tmp;
+      ++ridx;
+      ++lsize;
+    }
+    ++lidx;
+    --lsize;
+  }
+}
+
+int main(int argc, char *argv[])
+{
+  int a[7] = {0};
+
+  // CBMC in some past version reported wrong results for 256, -2147221455,
+  // -2147221455, -2147221455, 16, -2147483600, 16384
+  a[0] = 256;
+  a[1] = -2147221455;
+  a[2] = -2147221455;
+  a[3] = -2147221455;
+  a[4] = 16;
+  a[5] = -2147483600;
+  a[6] = 16384;
+
+  sort_items_by_criteria(a, 0, 6);
+
+  printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]);
+
+  assert(a[0] == -2147483600);
+  return 0;
+}

regression/cbmc-library/memmove-01/constant.desc

@@ -0,0 +1,9 @@
+CORE
+constant.c
+--unwind 17
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated \d+ VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring

regression/cbmc-library/memmove-01/main.c

@@ -32,7 +32,8 @@ int main(int argc, char *argv[])
 {
   int a[7];
 
-  //CBMC reports wrong results for 256, -2147221455, -2147221455, -2147221455, 16, -2147483600, 16384
+  // CBMC in some past version reported wrong results for 256, -2147221455,
+  // -2147221455, -2147221455, 16, -2147483600, 16384
   a[0] = 256;
   a[1] = -2147221455;
   a[2] = -2147221455;

src/util/simplify_expr.cpp

@@ -1779,9 +1779,26 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   const auto bits=
     expr2bits(expr.op(), expr.id()==ID_byte_extract_little_endian);
 
-  // exact match of length only - otherwise we might lose bits of
-  // flexible array members at the end of a struct
-  if(bits.has_value() && mp_integer(bits->size()) == *el_size + *offset * 8)
+  // make sure we don't lose bits with structs containing flexible array members
+  const bool struct_has_flexible_array_member = has_subtype(
+    expr.type(),
+    [&](const typet &type) {
+      if(type.id() != ID_struct && type.id() != ID_struct_tag)
+        return false;
+
+      const struct_typet &st = to_struct_type(ns.follow(type));
+      const auto &comps = st.components();
+      if(comps.empty() || comps.back().type().id() != ID_array)
+        return false;
+
+      const auto size =
+        numeric_cast<mp_integer>(to_array_type(comps.back().type()).size());
+      return !size.has_value() || *size <= 1;
+    },
+    ns);
+  if(
+    bits.has_value() && mp_integer(bits->size()) >= *el_size + *offset * 8 &&
+    !struct_has_flexible_array_member)
   {
     std::string bits_cut = std::string(
       bits.value(),