Fix and optimize byte_extract lowering

1) Do not construct elements that would never be used. Handling of arrays was
broken before and mis-optimised for large arrays.
2) lower_byte_operators must not use bit-level operators on pointers
3) Ensure that lowering of unions and vectors is performed properly as well.
4) byte_extract lowering over Java strings

Author: tautschnig

regression/cbmc/union10/main.c

@@ -0,0 +1,23 @@
+typedef struct
+{
+  union {
+    int access[256];
+  };
+} S1;
+
+typedef struct
+{
+  int c;
+} S2;
+
+static S1 (* const l[1]) = {((S1 *) ((0x50000000UL) + 0x00000) )};
+
+void main()
+{
+  __CPROVER_allocated_memory(0x50000000UL, sizeof(S1));
+  l[0]->access[0] = 0;
+  __CPROVER_assert(l[0]->access[0] == 0, "holds");
+  __CPROVER_assert(l[0]->access[1] == 0, "should fail");
+  __CPROVER_allocated_memory(0x40000000UL + 0x40000, sizeof(S2));
+  ((S2 *) ((0x40000000UL) + 0x40000))->c = 0x0707;
+}

regression/cbmc/union10/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.2\] should fail: FAILURE$
+^\*\* 1 of 14 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Despite the large array inside the union, the test should complete within 10
+seconds. Simplify extractbits(concatenation(...)) is essential to make this
+possible. With 77236cc34 (Avoid nesting of ID_with/byte_update by rewriting
+byte_extract to use the root object) the test already is trivial, however.

src/solvers/flattening/boolbv_member.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/invariant.h>
 
 bvt boolbvt::convert_member(const member_exprt &expr)
 {
@@ -20,67 +21,34 @@ bvt boolbvt::convert_member(const member_exprt &expr)
 
   const bvt &struct_bv=convert_bv(struct_op);
 
-  if(struct_op_type.id()==ID_union)
-  {
-    return convert_bv(
-      byte_extract_exprt(byte_extract_id(),
-                         struct_op,
-                         from_integer(0, index_type()),
-                         expr.type()));
-  }
-  else if(struct_op_type.id()==ID_struct)
-  {
-    const irep_idt &component_name=expr.get_component_name();
-    const struct_typet::componentst &components=
-      to_struct_type(struct_op_type).components();
-
-    std::size_t offset=0;
-
-    for(struct_typet::componentst::const_iterator
-        it=components.begin();
-        it!=components.end();
-        it++)
-    {
-      const typet &subtype=it->type();
-      std::size_t sub_width=boolbv_width(subtype);
-
-      if(it->get_name()==component_name)
-      {
-        if(!base_type_eq(subtype, expr.type(), ns))
-        {
-          #if 0
-          std::cout << "DEBUG " << expr.pretty() << "\n";
-          #endif
+  const irep_idt &component_name = expr.get_component_name();
+  const struct_union_typet::componentst &components =
+    to_struct_union_type(struct_op_type).components();
 
-          error().source_location=expr.find_source_location();
-          error() << "member: component type does not match: "
-                  << subtype.pretty() << " vs. "
-                  << expr.type().pretty() << eom;
-          throw 0;
-        }
+  std::size_t offset = 0;
 
-        bvt bv;
-        bv.resize(sub_width);
-        assert(offset+sub_width<=struct_bv.size());
-
-        for(std::size_t i=0; i<sub_width; i++)
-          bv[i]=struct_bv[offset+i];
-
-        return bv;
-      }
+  for(const auto &comp : components)
+  {
+    const typet &subtype = comp.type();
+    const std::size_t sub_width = boolbv_width(subtype);
 
-      offset+=sub_width;
+    if(comp.get_name() == component_name)
+    {
+      DATA_INVARIANT(
+        base_type_eq(subtype, expr.type(), ns),
+        "component type expected to match expression type:\n" + expr.pretty());
+      DATA_INVARIANT(
+        offset + sub_width <= struct_bv.size(), "member access outside struct");
+
+      return
+        bvt(struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
     }
 
-    error().source_location=expr.find_source_location();
-    error() << "component " << component_name
-            << " not found in structure" << eom;
-    throw 0;
-  }
-  else
-  {
-    error().source_location=expr.find_source_location();
-    error() << "member takes struct or union operand" << eom;
-    throw 0;
+    if(struct_op_type.id() == ID_struct)
+      offset += sub_width;
   }
+
+  error().source_location = expr.find_source_location();
+  error() << "component " << component_name << " not found in structure" << eom;
+  throw 0;
 }