[WIP] Array theory improvements

regression/CMakeLists.txt

@@ -8,6 +8,7 @@ macro(add_test_pl_profile name cmdline flag profile)
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
         LABELS "${profile};CBMC"
+        TIMEOUT 1200
     )
 endmacro(add_test_pl_profile)
 

regression/cbmc/Array_UF23/main.c

@@ -0,0 +1,21 @@
+/// \file
+/// Test that Ackermann constraints are reduced by the weak equivalence
+/// optimisation: derived arrays (with, if, etc.) do not need Ackermann
+/// constraints because they are implied by the with/if constraints plus
+/// Ackermann on base arrays.
+#include <stdlib.h>
+int main()
+{
+  size_t array_size;
+  int a[array_size];
+  int i0, i1, i2, i3, i4;
+
+  a[i0] = 0;
+  a[i1] = 1;
+  a[i2] = 2;
+  a[i3] = 3;
+  a[i4] = 4;
+
+  __CPROVER_assert(a[i0] >= 0, "a[i0] >= 0");
+  return 0;
+}

regression/cbmc/Array_UF23/test.desc

@@ -0,0 +1,13 @@
+CORE broken-refine-arrays broken-smt-backend no-new-smt
+main.c
+--arrays-uf-always --unwind 1 --show-array-constraints --json-ui
+"arrayAckermann": 60
+^EXIT=10$
+^SIGNAL=0$
+--
+"arrayAckermann": 110
+--
+Checks that the weak equivalence optimisation reduces Ackermann constraints.
+With 5 stores to the same unbounded array, the old code produced 110 Ackermann
+constraints (one per pair of indices per array term). The optimised code skips
+derived arrays (with, if, etc.) and produces only 60.

regression/cbmc/Array_operations2/test-arrays-uf-always.desc

@@ -0,0 +1,36 @@
+KNOWNBUG broken-cprover-smt-backend no-new-smt
+main.c
+--arrays-uf-always
+^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$
+^\[main.assertion.13\] line 35 assertion arr\[1\].c\[3\] == 0: FAILURE$
+^\[main.assertion.14\] line 36 assertion arr\[1\].c\[4\] == 0: FAILURE$
+^\*\* 3 of 21 failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+With --arrays-uf-always the array theory's union-find incorrectly conflates
+structurally different arrays that happen to have equal initial values.
+
+The SSA equations for the zero-initialised struct array produce:
+  arr#2[0].c = {0,0,0,0,0}
+  arr#2[1].c = {0,0,0,0,0}
+  arr#2[2].c = {0,0,0,0,0}
+
+Because all three equalities share the same RHS literal {0,0,0,0,0},
+record_array_equality transitively unifies arr#2[0].c, arr#2[1].c, and
+arr#2[2].c into a single equivalence class.  After __CPROVER_array_replace
+modifies arr (producing arr#3 via byte_update), the array theory cannot
+distinguish the three .c sub-arrays: constraints meant for arr#3[1].c
+(the replaced region) bleed into arr#3[0].c and arr#3[2].c, causing
+spurious failures on assertions 1-11 and 15-21.
+
+Without --arrays-uf-always the char[5] sub-arrays are small enough to be
+flattened to bitvectors, bypassing the array decision procedure entirely,
+so the test passes.
+
+Fixing this requires the union-find to distinguish "structurally same
+array" from "arrays with equal values", which is a fundamental change to
+the Nelson-Oppen style array decision procedure as used in CBMC.

regression/cbmc/Array_operations2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-cprover-smt-backend no-new-smt
+CORE broken-cprover-smt-backend no-new-smt broken-arrays-uf-always
 main.c
 
 ^\[main.assertion.12\] line 34 assertion arr\[1\].c\[2\] == 0: FAILURE$

regression/cbmc/CMakeLists.txt

@@ -32,6 +32,20 @@ add_test_pl_profile(
   "CORE"
 )
 
+add_test_pl_profile(
+    "cbmc-arrays-uf-always"
+    "$<TARGET_FILE:cbmc> --arrays-uf-always"
+    "-C;-X;broken-arrays-uf-always;-X;thorough-arrays-uf-always;-X;smt-backend;${gcc_only_string}-s;arrays-uf-always"
+    "CORE"
+)
+
+add_test_pl_profile(
+    "cbmc-arrays-uf-always-refine-arrays"
+    "$<TARGET_FILE:cbmc> --arrays-uf-always --refine-arrays"
+    "-C;-X;broken-arrays-uf-always;-X;thorough-arrays-uf-always;-X;broken-refine-arrays;-X;smt-backend;${gcc_only_string}-s;arrays-uf-always-refine-arrays"
+    "CORE"
+)
+
 # solver appears on the PATH in Windows already
 if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set_property(

regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend no-new-smt
+CORE broken-smt-backend no-new-smt broken-refine-arrays
 main.c
 --no-malloc-may-fail --smt2 --outfile -
 \(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)

regression/cbmc/arrays-uf-always-large-struct-soundness/main.c

@@ -0,0 +1,16 @@
+struct S
+{
+  int d[65];
+};
+
+unsigned nondet_unsigned(void);
+
+int main()
+{
+  struct S a[2];
+  a[0].d[0] = 1;
+  a[1].d[0] = 1;
+  unsigned i = nondet_unsigned();
+  __CPROVER_assume(i < 2);
+  __CPROVER_assert(a[i].d[0] == 1, "");
+}

regression/cbmc/arrays-uf-always-large-struct-soundness/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--arrays-uf-always --no-standard-checks
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+With --arrays-uf-always, indexing an array of structs containing array members
+with 65+ elements through a nondeterministic index must produce correct results.
+The bitvector solver connects the array symbol's map literals to the array
+theory's element-wise constraints so that struct-level equalities properly
+constrain the array elements.

regression/cbmc/arrays-uf-always-member-crash/main.c

@@ -0,0 +1,12 @@
+struct S
+{
+  int a[1];
+};
+
+int main()
+{
+  struct S x[2];
+  int i;
+  __CPROVER_assume(i >= 0 && i < 2);
+  __CPROVER_assert(x[i].a[0] == 0, "");
+}

regression/cbmc/arrays-uf-always-member-crash/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--arrays-uf-always --no-standard-checks
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Verify that --arrays-uf-always handles array-of-structs containing array
+members accessed through a nondet index. The arrays theory must accept member
+expressions where the struct operand is an index expression.

regression/cbmc/arrays-uf-always-member-soundness/main.c

@@ -0,0 +1,16 @@
+struct S
+{
+  int d[1];
+};
+
+int nondet_int(void);
+
+int main()
+{
+  struct S a[2];
+  a[0].d[0] = 1;
+  a[1].d[0] = 1;
+  int i = nondet_int();
+  __CPROVER_assume(i == 0 || i == 1);
+  __CPROVER_assert(a[i].d[0] == 1, "");
+}

regression/cbmc/arrays-uf-always-member-soundness/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--arrays-uf-always --no-standard-checks
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+With --arrays-uf-always, indexing an array of structs that contain array members
+through a nondeterministic index must produce correct results. The bitvector
+solver handles member expressions with non-symbol struct operands (e.g.,
+member(index(outer_array, i), field)) directly, bypassing the array theory.

regression/cbmc/bounds_check1/refine-arrays.desc

@@ -0,0 +1,18 @@
+CORE thorough-smt-backend no-new-smt
+main.c
+--no-malloc-may-fail --arrays-uf-always --refine-arrays
+^EXIT=10$
+^SIGNAL=0$
+\[\(.*\)i2\]: FAILURE
+dest\[\(.*\)j2\]: FAILURE
+payload\[\(.*\)[kl]2\]: FAILURE
+\*\* 7 of [0-9]+ failed
+--
+^warning: ignoring
+\[\(.*\)i\]: FAILURE
+dest\[\(.*\)j\]: FAILURE
+payload\[\(.*\)[kl]\]: FAILURE
+--
+Tests that --refine-arrays with --arrays-uf-always produces correct results
+and completes quickly. Without --refine-arrays this test takes ~85 seconds;
+with --refine-arrays the lazy with/if/Ackermann constraints reduce it to ~2s.

regression/cbmc/bounds_check1/test.desc

@@ -1,4 +1,4 @@
-CORE thorough-smt-backend no-new-smt
+CORE thorough-smt-backend no-new-smt thorough-arrays-uf-always
 main.c
 --no-malloc-may-fail
 ^EXIT=10$

regression/cbmc/trace-values/trace-values.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE no-new-smt broken-arrays-uf-always
 trace-values.c
 --no-malloc-may-fail --trace
 ^EXIT=10$

regression/libcprover-cpp/CMakeLists.txt

@@ -20,6 +20,7 @@ macro(add_test_pl_profile name cmdline flag profile)
     )
     set_tests_properties("${name}-${profile}" PROPERTIES
         LABELS "${profile};CBMC"
+        TIMEOUT 1200
     )
 endmacro(add_test_pl_profile)
 

src/goto-checker/solver_factory.cpp

@@ -204,7 +204,8 @@ get_sat_solver(message_handlert &message_handler, const optionst &options)
 {
   const bool no_simplifier = options.get_bool_option("beautify") ||
                              !options.get_bool_option("sat-preprocessor") ||
-                             options.get_bool_option("refine-strings");
+                             options.get_bool_option("refine-strings") ||
+                             options.get_bool_option("refine-arrays");
 
   if(options.is_set("sat-solver"))
   {