Add --pointer-encoding-via-maps: solver-level array maps for pointer encoding

doc/man/cbmc.1

@@ -560,6 +560,9 @@ output smt incremental formula to the given file
 \fB\-\-write\-solver\-stats\-to\fR json\-file
 collect the solver query complexity
 .TP
+\fB\-\-pointer\-encoding\-via\-maps\fR
+use map-based pointer encoding instead of bit-packing
+.TP
 \fB\-\-refine\-strings\fR
 use string refinement (experimental)
 .TP

doc/man/goto-synthesizer.1

@@ -126,6 +126,9 @@ output smt incremental formula to the given file
 \fB\-\-write\-solver\-stats\-to\fR json\-file
 collect the solver query complexity
 .TP
+\fB\-\-pointer\-encoding\-via\-maps\fR
+use map-based pointer encoding instead of bit-packing
+.TP
 \fB\-\-arrays\-uf\-never\fR
 never turn arrays into uninterpreted functions
 .TP

doc/man/jbmc.1

@@ -464,6 +464,9 @@ output smt incremental formula to the given file
 \fB\-\-write\-solver\-stats\-to\fR \fIjson\-file\fR
 collect the solver query complexity
 .TP
+\fB\-\-pointer\-encoding\-via\-maps\fR
+use map-based pointer encoding instead of bit-packing
+.TP
 \fB\-\-no\-refine\-strings\fR
 turn off string refinement
 .TP

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 @@
+KNOWNBUG 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/Pointer_array6/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,13 @@
+KNOWNBUG pointer-encoding-via-maps
+main.c
+--no-malloc-may-fail
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Map-based pointer encoding does not correctly handle byte-level
+round-trips through pointer arrays. The misaligned byte_extract
+and byte_update operations produce incorrect values because the
+map encoding stores pointer indices rather than flat addresses.

regression/cbmc/Pointer_array6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-pointer-encoding-via-maps
 main.c
 --no-malloc-may-fail
 ^EXIT=0$

regression/cbmc/Pointer_difference2/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,19 @@
+CORE broken-smt-backend no-new-smt pointer-encoding-via-maps
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line 6 correct: SUCCESS
+^\[main.pointer.1\] line 8 same object violation in array - other_array: FAILURE$
+^\[main.assertion.3\] line 13 undefined behavior: FAILURE$
+^\[main.assertion.8\] line 28 end plus 2 is nondet: (UNKNOWN|FAILURE)$
+^\[main.pointer_arithmetic.\d+\] line 28 pointer relation: pointer outside object bounds in p: FAILURE$
+^\*\* 5 of \d+ failed
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+Map-based pointer encoding variant: fewer overflow failures because
+base addresses are constrained to the positive 32-bit range, so
+pointer-to-integer arithmetic doesn't overflow.

regression/cbmc/Pointer_difference2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend no-new-smt
+CORE broken-smt-backend no-new-smt no-pointer-encoding-via-maps
 main.c
 
 ^\[main.assertion.1\] line 6 correct: SUCCESS

regression/cbmc/String_Abstraction7/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,12 @@
+KNOWNBUG no-new-smt pointer-encoding-via-maps
+main.c
+--string-abstraction
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Map-based pointer encoding produces VERIFICATION ERROR with
+string abstraction. The string abstraction pass creates pointer
+expressions that the map encoding does not handle correctly.

regression/cbmc/String_Abstraction7/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE no-new-smt no-pointer-encoding-via-maps
 main.c
 --string-abstraction
 ^EXIT=0$

regression/cbmc/address_space_size_limit1/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,11 @@
+KNOWNBUG thorough-paths no-new-smt pointer-encoding-via-maps
+test.c
+--no-simplify --unwind 300 --object-bits 8
+^EXIT=6$
+^SIGNAL=0$
+too many addressed objects
+--
+--
+Map-based pointer encoding does not enforce the object-bits limit
+in the same way as the standard encoding, so the "too many
+addressed objects" error is not triggered.

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,4 +1,4 @@
-CORE thorough-paths no-new-smt
+CORE thorough-paths no-new-smt no-pointer-encoding-via-maps
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects

regression/cbmc/argc-and-argv/argv1.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-pointer-encoding-via-maps
 argv1.c
 
 ^EXIT=0$

regression/cbmc/argc-and-argv/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,13 @@
+KNOWNBUG pointer-encoding-via-maps
+argv1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Map-based pointer encoding does not correctly propagate
+argv[argc]==NULL through the array theory. The with-constraints
+fix for SSA-renamed indices is present but insufficient for the
+map encoding's pointer equality path.

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/memory_allocation1/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,13 @@
+KNOWNBUG pointer-encoding-via-maps
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Map-based pointer encoding does not correctly model
+__CPROVER_allocated_memory or integer-address pointer
+dereferences, causing different failures than the standard
+encoding.

regression/cbmc/memory_allocation1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE broken-smt-backend no-pointer-encoding-via-maps
 main.c
 
 ^EXIT=10$

regression/cbmc/mm_io1/test-pointer-encoding-via-maps.desc

@@ -0,0 +1,11 @@
+KNOWNBUG pointer-encoding-via-maps
+main.c
+--no-standard-checks
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Map-based pointer encoding does not correctly handle memory-mapped
+I/O pointer dispatch, causing assertion failures for reads from
+fixed addresses.

regression/cbmc/mm_io1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE no-pointer-encoding-via-maps
 main.c
 --no-standard-checks
 ^Replaced MMIO operations: 3 read\(s\), 1 write\(s\)