Improve performance and fix limitations of flatten_byte_operators [blocks: #3725]

jbmc/regression/jbmc/nondet_propagation1/andNot_Bug.java

@@ -0,0 +1,13 @@
+public class andNot_Bug {
+  public static void main(int capacity) {
+    if(capacity < 1)
+      return;
+    boolean b1 = true;
+    boolean b2[] = new boolean[capacity];
+    b2[0] = false;
+
+    for (int i = 0; i < b2.length; i++) {
+      b1 = b1 && !b2[i];
+    }
+  }
+}

jbmc/regression/jbmc/nondet_propagation1/test.desc

@@ -0,0 +1,7 @@
+CORE
+andNot_Bug.class
+--depth 1600 --java-unwind-enum-static --java-max-vla-length 48 --unwind 4 --max-nondet-string-length 100  --function andNot_Bug.main
+^EXIT=0$
+^SIGNAL=0$
+--
+--

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

@@ -0,0 +1,16 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  char foo[1];
+  char result = 0;
+  int size;
+  __CPROVER_assume(size == 1);
+
+  memset(&result, 42, size);
+  __CPROVER_assert(result == 42, "should succeed");
+  result = 42;
+  memcpy(&result, foo, size);
+  __CPROVER_assert(result == 42, "should fail");
+}

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

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[main.assertion.1\] line 12 should succeed: SUCCESS$
+^\[main.assertion.2\] line 15 should fail: FAILURE$
+--
+^warning: ignoring

regression/cbmc/Endianness4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Endianness6/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$

regression/cbmc/Pointer_byte_extract5/no-simplify.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$

regression/cbmc/Pointer_byte_extract5/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --bounds-check --32
 ^EXIT=10$

regression/cbmc/Promotion3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

regression/cbmc/array_constraints1/test.desc

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

regression/cbmc/byte_update2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update4/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update6/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update8/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --little-endian
 ^EXIT=0$

regression/cbmc/byte_update9/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --big-endian
 ^EXIT=0$

regression/cbmc/gcc_c99-bool-1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 c99-bool-1.c
 
 ^EXIT=0$

regression/cbmc/memory_allocation1/test.desc

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

regression/cbmc/scanf1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.i
 --little-endian
 ^EXIT=10$

regression/cbmc/struct6/test.desc

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

regression/cbmc/union12/test.desc

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

regression/cbmc/union6/test.desc

@@ -1,8 +1,11 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test reports a VERIFICATION ERROR when running with the SMT2 solver on
+Windows only.

regression/cbmc/union7/test.desc

@@ -6,3 +6,6 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+This test reports a VERIFICATION ERROR when running with the SMT2 solver on
+Windows only.

regression/cbmc/union9/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/expr_util.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
@@ -40,7 +41,8 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
-  // if we extract from an unbounded array, call the flattening code
+  // array logic does not handle byte operators, thus lower when operating on
+  // unbounded arrays
   if(is_unbounded_array(expr.op().type()))
   {
     try

src/solvers/flattening/boolbv_byte_update.cpp

@@ -8,16 +8,37 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
+#include <util/throw_with_nested.h>
+
+#include <solvers/lowering/expr_lowering.h>
+#include <solvers/lowering/flatten_byte_extract_exceptions.h>
 
+#include "bv_conversion_exceptions.h"
 #include "bv_endianness_map.h"
 
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
+  // if we update (from) an unbounded array, lower the expression as the array
+  // logic does not handle byte operators
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    is_unbounded_array(expr.value().type()))
+  {
+    try
+    {
+      return convert_bv(lower_byte_update(expr, ns));
+    }
+    catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
+    {
+      util_throw_with_nested(
+        bitvector_conversion_exceptiont("Can't convert byte_update", expr));
+    }
+  }
+
   const exprt &op = expr.op();
   const exprt &offset_expr=expr.offset();
   const exprt &value=expr.value();

src/solvers/flattening/boolbv_index.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+#include <solvers/lowering/expr_lowering.h>
+
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
   const exprt &array=expr.array();
@@ -47,7 +49,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       for(std::size_t i=0; i<width; i++)
         bv[i]=prop.new_variable();
 
-      record_array_index(expr);
+      if(has_byte_operator(expr))
+        record_array_index(to_index_expr(lower_byte_operators(expr, ns)));
+      else
+        record_array_index(expr);
 
       // record type if array is a symbol
 

src/solvers/flattening/boolbv_member.cpp

@@ -9,9 +9,6 @@ Author: Daniel Kroening, [email protected]
 #include "boolbv.h"
 
 #include <util/base_type.h>
-#include <util/byte_operators.h>
-#include <util/arith_tools.h>
-#include <util/c_types.h>
 
 bvt boolbvt::convert_member(const member_exprt &expr)
 {
@@ -20,59 +17,40 @@ 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
-  {
-    INVARIANT(
-      struct_op_type.id() == ID_struct,
-      "member_exprt should denote access to a union or struct");
+  const irep_idt &component_name = expr.get_component_name();
+  const struct_union_typet::componentst &components =
+    to_struct_union_type(struct_op_type).components();
 
-    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;
 
-    std::size_t offset=0;
+  for(const auto &c : components)
+  {
+    const typet &subtype = c.type();
+    const std::size_t sub_width = boolbv_width(subtype);
 
-    for(const auto &c : components)
+    if(c.get_name() == component_name)
     {
-      const typet &subtype = c.type();
-      std::size_t sub_width=boolbv_width(subtype);
-
-      if(c.get_name() == component_name)
-      {
-        DATA_INVARIANT_WITH_DIAGNOSTICS(
-          base_type_eq(subtype, expr.type(), ns),
-          "struct component type shall match the member expression type",
-          subtype.pretty(),
-          expr.type().pretty());
-
-        bvt bv;
-        bv.resize(sub_width);
-        INVARIANT(
-          offset + sub_width <= struct_bv.size(),
-          "bitvector part corresponding to struct element shall be contained "
-          "within the full struct bitvector");
-
-        for(std::size_t i=0; i<sub_width; i++)
-          bv[i]=struct_bv[offset+i];
-
-        return bv;
-      }
-
-      offset+=sub_width;
+      DATA_INVARIANT_WITH_DIAGNOSTICS(
+        base_type_eq(subtype, expr.type(), ns),
+        "component type shall match the member expression type",
+        subtype.pretty(),
+        expr.type().pretty());
+      INVARIANT(
+        offset + sub_width <= struct_bv.size(),
+        "bitvector part corresponding to element shall be contained within the "
+        "full aggregate bitvector");
+
+      return bvt(
+        struct_bv.begin() + offset, struct_bv.begin() + offset + sub_width);
     }
 
-    INVARIANT_WITH_DIAGNOSTICS(
-      false,
-      "struct type shall contain component accessed by member expression",
-      expr.find_source_location(),
-      id2string(component_name));
+    if(struct_op_type.id() != ID_union)
+      offset += sub_width;
   }
+
+  INVARIANT_WITH_DIAGNOSTICS(
+    false,
+    "struct type shall contain component accessed by member expression",
+    expr.find_source_location(),
+    id2string(component_name));
 }

src/solvers/flattening/bv_pointers.cpp

@@ -453,13 +453,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else
   {
-    INVARIANT(
-      expr.id() != ID_byte_update_little_endian,
-      "byte-wise pointer updates are unsupported");
-
-    INVARIANT(
-      expr.id() != ID_byte_update_big_endian,
-      "byte-wise pointer updates are unsupported");
+    return SUB::convert_byte_update(to_byte_update_expr(expr));
   }
 
   return conversion_failed(expr);