Merge pull request #7297 from diffblue/union-large-array

performance improvement for large bitvectors

Author: tautschnig

regression/cbmc/bounds_check1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-z3-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$

regression/cbmc/union/union_large_array.c

@@ -0,0 +1,15 @@
+#define LARGE 100000
+
+// This is to test the efficiency of unions that contain a large array.
+union U
+{
+  char large_array[LARGE];
+  int something_else;
+};
+
+int main()
+{
+  union U u;
+  u.something_else = 1234;
+  __CPROVER_assert(0, "should fail");
+}

regression/cbmc/union/union_large_array.desc

@@ -0,0 +1,11 @@
+CORE broken-z3-smt-backend
+union_large_array.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main\.assertion\.1\] line \d+ should fail: FAILURE$
+^\*\* 1 of 1 failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--

src/solvers/flattening/boolbv_get.cpp

@@ -199,8 +199,8 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
   const std::size_t width = boolbv_width(type);
   PRECONDITION(bv.size() >= offset + width);
 
-  // most significant bit first
   std::string value;
+  value.reserve(width);
 
   for(std::size_t bit_nr=offset; bit_nr<offset+width; bit_nr++)
   {
@@ -214,9 +214,13 @@ exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset)
     }
     // clang-format on
 
-    value=ch+value;
+    value += ch;
   }
 
+  // The above collects bits starting with the least significant bit,
+  // but we need the most significant bit first.
+  std::reverse(value.begin(), value.end());
+
   switch(bvtype)
   {
   case bvtypet::IS_UNKNOWN: