goto instrument loop unwinding with strategies

Author: danpoe

regression/Makefile

@@ -1,4 +1,4 @@
-DIRS = ansi-c cbmc cpp goto-instrument
+DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind
 
 test:
 	$(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;)

regression/goto-instrument-unwind/Makefile

@@ -21,9 +21,10 @@ tests.log: ../test.pl
 clean:
 	@for dir in *; do \
                 if [ -d "$$dir" ]; then \
-                        rm $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
+                        rm -f $$dir/*.txt $$dir/*.dot $$dir/*.gb $$dir/*.out; \
                 fi; \
-        done;
+  done;
+	rm -f tests.log
 
 show:
 	@for dir in *; do \

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,8 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^EXIT=0$
+^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,8 @@
+CORE
+main.c
+--unwind 10 --unwinding-assertions
+^EXIT=0$
+^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,8 @@
+CORE
+main.c
+--unwind 9
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

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

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

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

regression/goto-instrument-unwind/continue-as-loops1/main.c

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

regression/goto-instrument-unwind/continue-as-loops1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--unwind 5 --continue-as-loops
+^Unwinding loop.*iteration 5
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^Unwinding loop.*iteration 6

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

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

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

@@ -1,6 +1,7 @@
 CORE
 main.c
-100
+--unwind 100 --partial-loops
+^EXIT=0$
 ^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,8 @@
+CORE
+main.c
+--unwind 10 --partial-loops
+^EXIT=0$
+^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,8 @@
+CORE
+main.c
+--unwind 100 --partial-loops
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -5,23 +5,14 @@ goto_cc=$src/goto-cc/goto-cc
 goto_instrument=$src/goto-instrument/goto-instrument
 cbmc=$src/cbmc/cbmc
 
-function usage() {
-  echo "Usage: chain unwind-num test_file.c"
-  exit 1
-}
+name=${@:$#}
+name=${name%.c}
 
-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
-  usage
-fi
+args=${@:1:$#-1}
 
 $goto_cc -o $name.gb $name.c
-$goto_instrument  $name.gb ${name}-unwound.gb --unwind $unwind_num
+$goto_instrument --show-goto-functions $name.gb
+$goto_instrument $args $name.gb ${name}-unwound.gb
+$goto_instrument --show-goto-functions ${name}-unwound.gb
 $cbmc ${name}-unwound.gb
+

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

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

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

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

regression/goto-instrument-unwind/unwindset-file1/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/unwindset-file1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 5 --unwindset-file unwindset.input --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument-unwind/unwindset-file1/unwindset.input

@@ -0,0 +1 @@
+main.0:10,main.1:10,main.2:10

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,8 @@
+CORE
+main.c
+--unwind 9 --unwindset main.0:10 --unwinding-assertions
+^EXIT=0$
+^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,9 @@
+CORE
+main.c
+--unwindset main.0:10 --unwinding-assertions
+^Unwinding loop
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring