Array cell sensitivity

jbmc/regression/jbmc/array-cell-sensitivity1/Test.java

@@ -0,0 +1,10 @@
+public class Test {
+
+  public static void main(int unknown) {
+
+    int[] x = new int[10];
+    x[unknown] = 1;
+    x[1] = unknown;
+    assert (x[1] == unknown);
+  }
+}

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

@@ -0,0 +1,20 @@
+CORE
+Test.class
+--function Test.main --show-vcc --max-field-sensitivity-array-size 10
+symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
+symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
+symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
+symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
+symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
+symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
+symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
+symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
+symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
+symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that field sensitvity is still applied to an array of size 10
+when the max is set to 10.

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --show-vcc --max-field-sensitivity-array-size 9
+^EXIT=0$
+^SIGNAL=0$
+symex_dynamic::dynamic_2_array#[0-9]\[1\]
+--
+symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+--
+This checks that field sensitvity is not applied to an array of size 10
+when the max is set to 9.

jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--function Test.main --show-vcc --no-array-field-sensitivity
+^EXIT=0$
+^SIGNAL=0$
+symex_dynamic::dynamic_2_array#[0-9]\[1\]
+--
+symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+--
+This checks that field sensitvity is not applied to arrays when
+no-array-field-sensitivity is used.

jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

@@ -0,0 +1,22 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
+symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
+symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
+symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
+symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
+symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
+symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
+symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
+symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
+symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
+symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] =
+--
+This checks that a write to a Java array with an unknown index uses a whole-array
+write followed by array-cell expansion, but one targeting a constant index uses
+a single-cell symbol without expansion.

jbmc/regression/jbmc/array-cell-sensitivity2/Test.java

@@ -0,0 +1,21 @@
+public class Test {
+
+  public int data;
+  public Test[] children = new Test[2];
+
+  public static void main(int unknown) {
+
+    Test[] root = new Test[2];
+    Test node1 = new Test();
+    Test node2 = new Test();
+    root[0] = node1;
+    root[1] = node2;
+    node1.children[0] = unknown % 2 == 0 ? node1 : node2;
+    node1.children[1] = unknown % 3 == 0 ? node1 : node2;
+    node2.children[0] = unknown % 5 == 0 ? node1 : node2;
+    node2.children[1] = unknown % 7 == 0 ? node1 : node2;
+    int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
+    root[idx1].children[idx2].children[idx3].children[idx4].data = 1;
+    assert (node1.data == 1);
+  }
+}

jbmc/regression/jbmc/array-cell-sensitivity2/test.desc

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+symex_dynamic::dynamic_object6#3\.\.data =
+symex_dynamic::dynamic_object3#3\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data
+symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data
+--
+This checks that a write using a mix of field and array accessors uses a field-sensitive
+symbol (the data field of the possible ultimate target objects) rather than using
+a whole-struct write followed by an expansion.

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -135,6 +135,25 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   parse_java_language_options(cmdline, options);
   parse_java_object_factory_options(cmdline, options);
 
+  if(cmdline.isset("max-field-sensitivity-array-size"))
+  {
+    options.set_option(
+      "max-field-sensitivity-array-size",
+      cmdline.get_value("max-field-sensitivity-array-size"));
+  }
+
+  if(cmdline.isset("no-array-field-sensitivity"))
+  {
+    if(cmdline.isset("max-field-sensitivity-array-size"))
+    {
+      log.error()
+        << "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
+        << " must not be given together" << messaget::eom;
+      exit(CPROVER_EXIT_USAGE_ERROR);
+    }
+    options.set_option("no-array-field-sensitivity", true);
+  }
+
   if(cmdline.isset("show-symex-strategies"))
   {
     log.status() << show_path_strategies() << messaget::eom;

regression/cbmc-concurrency/norace_array1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/norace_array2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc-concurrency/struct_and_array1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc/Multi_Dimensional_Array3/test.desc

@@ -1,8 +1,11 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+With the SMT backend this incorrect result because of the bug documented here:
+https://github.com/diffblue/cbmc/issues/4749

regression/cbmc/address_space_size_limit3/main.i

@@ -92,6 +92,11 @@ void f__L_0x3c6_0()
 
 int main()
 {
+  int unknown;
+  // Avoid constant propagation solving for pointer-offsets of esp,
+  // which prevent demonstrating the object-size limitation this test
+  // intends to exhibit:
+  esp -= (unknown & 1);
   L_0x3fe_0: esp-=0x4;
   L_0x3fe_1: *(uint32_t*)(esp)=ebp;
   L_0x3ff_0: ebp=esp;

regression/cbmc/array-cell-sensitivity1/test.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int array[10];
+  array[argc] = 1;
+  array[1] = argc;
+  assert(array[1] == argc);
+}

regression/cbmc/array-cell-sensitivity1/test.desc

@@ -0,0 +1,21 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
+main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
+main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
+main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
+main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
+main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
+main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
+main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
+main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
+main::1::array!0@1#3\[\[1\]\] =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[[0-9]+\]
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol

regression/cbmc/array-cell-sensitivity1/test_execution.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity10/test.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  struct A other[2];
+  struct A *ptr = argc % 2 ? &other : &array[0];
+  ptr[argc].x = 1;
+  ptr[1].x = argc;
+  assert(ptr[1].x == argc);
+  assert(array[1].x == argc);
+}

regression/cbmc/array-cell-sensitivity10/test.desc

@@ -0,0 +1,32 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
+main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
+main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
+main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
+main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
+main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
+main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
+main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
+main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
+main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
+main::1::array!0@1#3\[\[1\]\]..x =
+main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
+main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
+main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
+main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
+main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
+main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
+main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
+main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
+main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
+main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This checks that a write with a non-constant index leads to a whole-array
+operation followed by expansion into individual array cells, while a write with
+a constant index leads to direct use of a single cell symbol, for the case where
+the array element is struct-typed and accessed via a pointer.

regression/cbmc/array-cell-sensitivity10/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 16.*SUCCESS$
+^\[main.assertion\.2\] line 17.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity11/test.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  int *ptr = argc % 2 ? &argc : &array[0].y;
+  *ptr = argc;
+  assert(*ptr == argc);
+  assert(array[1].y == argc);
+}

regression/cbmc/array-cell-sensitivity11/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[\[[1-9]\]\]
+main::1::array!0@1#[3-9]\[\[[0-9]\]\]
+--
+This checks that an array access made via a pointer to a member of the array's
+element struct type is executed using a field-sensitive symbol.

regression/cbmc/array-cell-sensitivity11/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.

regression/cbmc/array-cell-sensitivity12/test.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct A
+{
+  int x;
+  int y;
+};
+
+int main(int argc, char **argv)
+{
+  struct A array[10];
+  int *ptr = argc % 2 ? &array[0].x : &array[0].y;
+  *ptr = argc;
+  assert(*ptr == argc);
+  assert(array[0].y == argc);
+}

regression/cbmc/array-cell-sensitivity12/test.desc

@@ -0,0 +1,15 @@
+FUTURE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0\]\]..x =
+main::1::array!0@1#2\[\[0\]\]..y =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::array!0@1#[2-9]\[\[[1-9]\]\]
+main::1::array!0@1#[3-9]\[\[[0-9]\]\]
+--
+Ideally we should handle accesses to a pointer with a finite set of possible
+referents precisely, but because value_sett regards &array[0].x and &array[0].y
+as two different offsets into the same allocation and discards the precise offsets
+they point to, this is currently handled imprecisely with a byte_update operation.

regression/cbmc/array-cell-sensitivity12/test_execution.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+
+^VERIFICATION FAILED$
+^\[main.assertion\.1\] line 14.*SUCCESS$
+^\[main.assertion\.2\] line 15.*FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+The real test is in test.desc; this is a companion to check that the program under
+test actually behaves as expected.