Prototype: 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.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.

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-sensitivity10/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];
+  struct A *ptr = argc % 2 ? (struct A *)&argc : &array[0];
+  ptr[argc].x = 1;
+  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-sensitivity11/test.c

@@ -0,0 +1,15 @@
+#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(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-sensitivity12/test.c

@@ -0,0 +1,15 @@
+#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(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-sensitivity13/test.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+struct A
+{
+  int data;
+  struct A *children[2];
+};
+
+int main(int argc, char **argv)
+{
+  struct A root;
+  struct A node1, node2;
+  root.children[0] = argc % 2 ? &node1 : &node2;
+  root.children[1] = argc % 3 ? &node1 : &node2;
+  node1.children[0] = argc % 5 ? &node1 : &node2;
+  node1.children[1] = argc % 7 ? &node1 : &node2;
+  node2.children[0] = argc % 11 ? &node1 : &node2;
+  node2.children[1] = argc % 13 ? &node1 : &node2;
+  root.children[0]->children[1]->children[1]->children[0]->data = 1;
+  assert(node1.data == argc);
+}

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

@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.data =
+main::1::node2!0@1#2\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] =
+--
+This checks that mixed array and field accesses are executed using a field-sensitive
+symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and
+expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\])

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

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+struct A
+{
+  int data;
+  struct A *children[2];
+};
+
+int main(int argc, char **argv)
+{
+  struct A root;
+  struct A node1, node2;
+  root.children[0] = argc % 2 ? &node1 : &node2;
+  root.children[1] = argc % 3 ? &node1 : &node2;
+  node1.children[0] = argc % 5 ? &node1 : &node2;
+  node1.children[1] = argc % 7 ? &node1 : &node2;
+  node2.children[0] = argc % 11 ? &node1 : &node2;
+  node2.children[1] = argc % 13 ? &node1 : &node2;
+  int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
+  root.children[idx1]->children[idx2]->children[idx3]->children[idx4]->data = 1;
+  assert(node1.data == argc);
+}

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

@@ -0,0 +1,14 @@
+CORE
+test.c
+--show-vcc
+main::1::node1!0@1#2\.\.data =
+main::1::node2!0@1#2\.\.data =
+^EXIT=0$
+^SIGNAL=0$
+--
+main::1::node1!0@1#[3-9]\.\.children\[\[[01]\]\] =
+--
+This checks that mixed array and field accesses are executed using a field-sensitive
+symbol (main::1::node1!0@1#2..data) rather than by assigning the whole struct and
+expanding into field symbols (which would assign main::1::node1!0@1#3..children\[\[[01]\]\]),
+for the case where the array indices only become constant after propagation.

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

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

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

@@ -0,0 +1,13 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(-1 \+ main::argc!0@1#1, signedbv\[64\]\), 1\)
+main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
+^EXIT=0$
+^SIGNAL=0$
+--
+\[\[[0-9]+\]\]
+--
+This checks that arrays of uncertain size are always treated as aggregates and
+are not expanded into individual cell symbols (which use the [[index]] notation
+to distinguish them from the index operator (array[index]))

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

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

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

@@ -0,0 +1,23 @@
+CORE
+test.c
+--show-vcc
+main::1::array!0@1#2\[\[0]\] = main::1::array!0@1#1\[0\]
+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, even when the
+array is accessed via a pointer with other possible aliases.

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

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