Merge pull request #3279 from tautschnig/array-is-uniform

Simplify and modernise array-is-uniform code

Author: Daniel Kroening

regression/cbmc/uniform_array1/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int A[] = {1, 1};
+  int i;
+  __CPROVER_assert(i < 0 || i > 1 || A[i] == 1, "valid access into array of 1");
+  __CPROVER_assert(A[i] == 1, "possible out-of-bounds access");
+  return 0;
+}

regression/cbmc/uniform_array1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 2 failed
+--
+^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -301,6 +301,7 @@ rm trace_options_json_extended/non-extended.desc
 rm trace_show_code/test.desc
 rm trace_show_function_calls/test.desc
 rm uncaught_exceptions_analysis1/test.desc
+rm uniform_array1/test.desc
 rm union11/union_list.desc
 rm union3/test.desc
 rm union5/test.desc

src/solvers/flattening/boolbv_index.cpp

@@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <cassert>
+#include <algorithm>
 
 #include <util/arith_tools.h>
 #include <util/cprover_prefix.h>
@@ -80,26 +80,16 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     // this rather than as a series of individual options.
     #define UNIFORM_ARRAY_HACK
     #ifdef UNIFORM_ARRAY_HACK
-    bool is_uniform = false;
+    bool is_uniform = array.id() == ID_array_of;
 
-    if(array.id()==ID_array_of)
+    if(array.id() == ID_constant || array.id() == ID_array)
     {
-      is_uniform = true;
-    }
-    else if(array.id()==ID_constant || array.id()==ID_array)
-    {
-      bool found_exception = false;
-      forall_expr(it, array.operands())
-      {
-        if(*it != array.op0())
-        {
-          found_exception = true;
-          break;
-        }
-      }
-
-      if(!found_exception)
-        is_uniform = true;
+      is_uniform =
+        array.operands().size() <= 1 ||
+        std::all_of(
+          ++array.operands().begin(),
+          array.operands().end(),
+          [&array](const exprt &expr) { return expr == array.op0(); });
     }
 
     if(is_uniform && prop.has_set_to())