goto-instrument loop uwinding with strategies

Author: danpoe

regression/goto-instrument-unwind/assert1/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 10 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assert2/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/assert2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 9 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assert3/main.c

@@ -0,0 +1,9 @@
+
+int main()
+{
+  int i;
+  i = 0;
+  do {
+    i++;
+  } while(i < 10);
+}

regression/goto-instrument-unwind/assert3/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 10 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assume1/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(0);
+}

regression/goto-instrument-unwind/assume1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 10"
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument-unwind/assume2/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(0);
+}

regression/goto-instrument-unwind/assume2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 9"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/break-loop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/break-loop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-100
+"--unwind 100 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/continue-loop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/continue-loop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-100
+"--unwind 100 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/do-while-loop1/main.c

@@ -0,0 +1,27 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=10;
+  
+  const unsigned n=100;
+  unsigned c=0, i;
+
+  i=1;
+  do
+  {
+    f();
+    c++;
+    i++;
+  } while(i<=n);
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "do-while loop unwind (1)");
+}

regression/goto-instrument-unwind/do-while-loop1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 10 --partial-loops"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/do-while-loop2/main.c

@@ -0,0 +1,28 @@
+
+void f() {}
+
+int main()
+{
+  /**
+   * This is a test case for the unwind operation of goto-instrument;
+   * every loop will be unwound K times
+   **/
+  const unsigned K=100;
+  
+  const unsigned n=10;
+  unsigned c=0, i;
+
+  i=1;
+  do
+  {
+    f();
+    c++;
+    i++;
+  } while(i<=n);
+
+  unsigned eva=n;
+  if(K<eva) eva=K;
+  
+  __CPROVER_assert(c==eva, "do-while loop unwind (1)");
+
+}

regression/goto-instrument-unwind/do-while-loop2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 100 --partial-loops"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/empty-loop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/empty-loop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-100
+"--unwind 100 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/nested-loops1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/nested-loops2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/rest-loop1/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+  assert(i==10);
+}

regression/goto-instrument-unwind/rest-loop1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+"--unwind 5 --rest-loops"
+^Unwinding loop.*iteration 5
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Unwinding loop.*iteration 6

regression/goto-instrument-unwind/simple-loop1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-10
+"--unwind 10 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/simple-loop2/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
-100
+"--unwind 100 --partial-loops"
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --

regression/goto-instrument-unwind/unwind-chain.sh

@@ -6,22 +6,18 @@ goto_instrument=$src/goto-instrument/goto-instrument
 cbmc=$src/cbmc/cbmc
 
 function usage() {
-  echo "Usage: chain unwind-num test_file.c"
+  echo "Usage: chain <options> <testfile>"
   exit 1
 }
 
-echo "Usage: process test_file.c to goto program"
-
-if [ $# -eq 2 ]
-then
-  unwind_num=$1
-  name=`echo $2 | cut -d. -f1`
-  echo $unwind_num
-  echo $name
-else
+if [ $# -ne 2 ]; then
   usage
+  exit 1
 fi
 
+name=$(echo $2 | cut -d. -f1)
+
 $goto_cc -o $name.gb $name.c
-$goto_instrument  $name.gb ${name}-unwound.gb --unwind $unwind_num
+$goto_instrument $1 $name.gb ${name}-unwound.gb
+$goto_instrument --show-goto-functions ${name}-unwound.gb
 $cbmc ${name}-unwound.gb

regression/goto-instrument-unwind/unwindset1/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/unwindset1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwind 9 --unwindset main.0:10 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/unwindset2/main.c

@@ -0,0 +1,9 @@
+
+int main()
+{
+  int i;
+
+  for(i = 0; i < 10; i++) {}
+
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/unwindset2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--unwindset main.0:10 --unwinding-assertions"
+^Unwinding loop
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/unwindset3/main.c

@@ -0,0 +1,6 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/unwindset3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+"--unwind 10 --unwindset main.0:-1"
+^Unwinding loop
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/unwindset4/main.c

@@ -0,0 +1,22 @@
+
+void f()
+{
+  int i;
+  for (i = 0; i < 10; i++) {}
+}
+
+void g()
+{
+  int i;
+  for (i = 0; i < 10; i++) {}
+  for (i = 0; i < 10; i++) {}
+}
+
+int main()
+{
+  f();
+  g();
+
+  int i;
+  for(i = 0; i < 10; i++) {}
+}

regression/goto-instrument-unwind/unwindset4/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwindset main.0:10,f.0:10,g.0:10,g.1:10 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/unwindset5/main.c

@@ -0,0 +1,16 @@
+
+int main()
+{
+  int i;
+  for(i = 0; i < 10; i++) {
+    int j;
+    for(j = 0; j < 10; j++) {
+      int k;
+      k = 0;
+      while(k < 10)
+      {
+        k++;
+      }
+    }
+  }
+}

regression/goto-instrument-unwind/unwindset5/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+"--unwindset main.0:10,main.1:10,main.2:10 --unwinding-assertions"
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/zero-unwind1/main.c

@@ -0,0 +1,12 @@
+
+int main()
+{
+  int i;
+  int j = 0;
+
+  for(i = 0; i < 10; i++) {
+    j = 1;
+  }
+
+  assert(j == 0);
+}