Loop shrinking

Enables proving properties in selected loops without having to unwind them.
Based on "Property Checking Array Programs Using Loop Shrinking" by Shrawan
Kumar, Amitabha Sanyal, Venkatesh R and Punit Shah, TACAS 2018.

Author: zhixing-xu

jbmc/unit/Makefile

@@ -126,6 +126,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/goto-instrument/reachability_slicer$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/nondet_static$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/full_slicer$(OBJEXT) \
+              $(CPROVER_DIR)/src/goto-instrument/abstract_loops$(OBJEXT) \
               $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \
               $(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
               $(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \

regression/cbmc/abstract-loops1/main.c

@@ -0,0 +1,23 @@
+#define ROW 10
+#define COL 10
+
+void main()
+{
+  int sum;
+  int image[ROW][COL];
+
+  // shrinkable
+  for(int j = 0; j < COL; j++)
+    image[0][j] = 0;
+
+  sum = 0;
+  // outer loop unshrinkable
+  // inner loop shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    image[i][0] = 0;
+    sum = sum + i;
+    for(int j = 0; j < COL; j++)
+      image[sum][j] = 0;
+  }
+}

regression/cbmc/abstract-loops1/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+ASSUME j < 10
+ASSUME j >= 0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loop with loop variable i is not shrunk (so it
+appears in unwinding). Loops with loop variable j are shrunk. The test also
+checks the constraints to the loop variable are correctly applied.

regression/cbmc/abstract-loops2/main.c

@@ -0,0 +1,36 @@
+#define ROW 3
+#define COL 10
+
+void boo(int r)
+{
+  int val = 0;
+  int image[ROW][COL];
+  ;
+  // shrinkable, and set as shrink target
+  for(int j = 0; j < COL; j++)
+  {
+    int c = j + val;
+    image[r][c] = val;
+  }
+}
+
+void main()
+{
+  int r;
+  int buffer[ROW];
+  // not shrinkable since r is used in mem-safe assertion in boo()
+  // and r update itself in loop
+  for(int i = 0; i < ROW; i++)
+  {
+    r = r + i;
+    boo(r);
+    buffer[i];
+  }
+
+  // shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(i);
+    buffer[i];
+  }
+}

regression/cbmc/abstract-loops2/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset boo.0,main.0 --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+ASSUME j < 10
+ASSUME j >= 0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrunk (so they
+appear in unwinding). Although the second loop in main is shrinkable, it is not
+in the target loop set provided by --abstractset, thus it shouldn't be shrunk.
+The test also ensures the loop in boo() with loop variable j is shrunk and the
+constraints are correctly applied.

regression/cbmc/abstract-loops3/main.c

@@ -0,0 +1,20 @@
+#include <stdlib.h>
+#define ROW 10
+
+void boo(int *x)
+{
+  *x = *x + 1;
+}
+
+void main()
+{
+  int *x = (int *)malloc(sizeof(int));
+  int buffer[ROW];
+  *x = 2;
+  // not shrinkable since x has a self-update in boo()
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(x);
+    buffer[*x] = 1;
+  }
+}

regression/cbmc/abstract-loops3/test.desc

@@ -0,0 +1,17 @@
+KNOWNBUG
+main.c
+--bounds-check --pointer-check --abstract-loops --abstractset main.0
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+--
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loops with loop variable i are not shrunk (so they
+appear in unwinding), even when the instruction that makes the loop unshrinkable
+is in another function.
+
+Requires #2646, #2694 to work.

regression/goto-instrument/abstract-loops1/main.c

@@ -0,0 +1,23 @@
+#define ROW 10
+#define COL 10
+
+void main()
+{
+  int sum;
+  int image[ROW][COL];
+
+  // shrinkable
+  for(int j = 0; j < COL; j++)
+    image[0][j] = 0;
+
+  sum = 0;
+  // outer loop unshrinkable
+  // inner loop shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    image[i][0] = 0;
+    sum = sum + i;
+    for(int j = 0; j < COL; j++)
+      image[sum][j] = 0;
+  }
+}

regression/goto-instrument/abstract-loops1/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--bounds-check --pointer-check --abstract-loops
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+main\.0
+ASSUME j < 10
+ASSUME j >= 0
+--
+main\.1
+main\.2
+ASSUME i < 10
+ASSUME i >= 0
+^warning: ignoring
+--
+This test ensures that the loop with loop variable i is not shrunk (so it
+appears in unwinding). Loops with loop variable j are shrunk. The test also
+checks the constraints to the loop variable are correctly applied.

regression/goto-instrument/abstract-loops2/main.c

@@ -0,0 +1,36 @@
+#define ROW 3
+#define COL 10
+
+void boo(int r)
+{
+  int val = 0;
+  int image[ROW][COL];
+  ;
+  // shrinkable, and set as shrink target
+  for(int j = 0; j < COL; j++)
+  {
+    int c = j + val;
+    image[r][c] = val;
+  }
+}
+
+void main()
+{
+  int r;
+  int buffer[ROW];
+  // not shrinkable since r is used in mem-safe assertion in boo()
+  // and r update itself in loop
+  for(int i = 0; i < ROW; i++)
+  {
+    r = r + i;
+    boo(r);
+    buffer[i];
+  }
+
+  // shrinkable
+  for(int i = 0; i < ROW; i++)
+  {
+    boo(i);
+    buffer[i];
+  }
+}