Add --paths tests for exploration strategies

This commit introduces a regression test suite specifically for testing
path exploration strategies when using cbmc with --paths. This test
suite is intended to ensure that paths are pushed and popped onto the
workqueue in the correct order as specified by their search strategy.
This commit contains a test suite for the FIFO exploration strategy.

This commit introduces a script for generating test.desc files. This is
needed because the multi-line regexes for matching the order of path
pushes and pops are very cumbersome to write and difficult to read.
Thus, the test.desc files are generated from a test.in file, which
includes a human-friendly description of what push, pop and execute
events should be expected during symbolic execution. A new script,
scripts/make_descs.py, interprets those events and generates a test.desc
from them before running the test suite.

Author: karkhaz

.gitignore

@@ -57,6 +57,9 @@ regression/**/*.smt2
 # regression/coverage file
 /regression/coverage_**
 
+# These files are generated from the test.in file in their directories
+regression/cbmc-path-fifo/*/test.desc
+
 # files stored by editors
 *~
 

regression/cbmc-path-fifo/Makefile

@@ -0,0 +1,23 @@
+default: tests.log
+
+test: gen-desc
+	@../test.pl -j 12 -p -c "../../../src/cbmc/cbmc --paths --verbosity 10"
+
+tests.log: ../test.pl gen-desc
+	@../test.pl -j 12 -p -c "../../../src/cbmc/cbmc --paths --verbosity 10"
+
+gen-desc:
+	@../../scripts/make_descs.py
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name 'test.desc' -execdir $(RM) '{}' \;
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cbmc-path-fifo/if/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int x;
+  if(x)
+    x = 1;
+  else
+    x = 0;
+}

regression/cbmc-path-fifo/if/test.in

@@ -0,0 +1,22 @@
+CORE
+main.c
+
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 4
+save line 7
+execute line 5
+any lines
+path is successful
+any lines
+execute line 4
+resume line 7
+execute line 7
+any lines
+path is successful
+end

regression/cbmc-path-fifo/loop-functional-correctness/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  int x;
+  __CPROVER_assume(x > 0);
+
+  while(x)
+    --x;
+
+  assert(x);
+}

regression/cbmc-path-fifo/loop-functional-correctness/test.in

@@ -0,0 +1,31 @@
+CORE
+main.c
+--unwind 2
+activate-multi-line-match
+SIGNAL=0
+EXIT=10
+--
+^warning: ignoring
+--
+This tests the following:
+
+- Symex saves the path that traverses the loop once, then the path that
+  traverses the loop twice;
+
+- Symex pops the path that traverses the loop once, then the path that
+  traverses the loop twice.
+
+The path that traverses the loop twice is the one that would cause an
+assertion failure, thus that result must appear last rather than second
+last.
+
+Test that the following happens in order:
+// Loop 0 times
+path is successful
+any lines
+// Loop once
+path is successful
+any lines
+// Loop twice
+path is unsuccessful
+end

regression/cbmc-path-fifo/nested-if/main.c

@@ -0,0 +1,18 @@
+int main()
+{
+  int x,y;
+  if(x)
+  {
+    if(y)
+      y = 1;
+    else
+      y = 0;
+  }
+  else
+  {
+    if(y)
+      y = 1;
+    else
+      y = 0;
+  }
+}

regression/cbmc-path-fifo/nested-if/test.in

@@ -0,0 +1,38 @@
+CORE
+main.c
+
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 4
+save line 13
+execute line 6
+save line 9
+execute line 7
+any lines
+path is successful
+any lines
+execute line 4
+resume line 13
+execute line 13
+save line 16
+execute line 14
+any lines
+path is successful
+any lines
+execute line 6
+resume line 9
+execute line 9
+any lines
+path is successful
+any lines
+execute line 13
+resume line 16
+execute line 16
+any lines
+path is successful
+end

regression/cbmc-path-fifo/simple-loop/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  int x;
+  while(x)
+  {
+    int y;
+  }
+  int y;
+}

regression/cbmc-path-fifo/simple-loop/test.in

@@ -0,0 +1,50 @@
+CORE
+main.c
+--unwind 2
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+--
+^warning: ignoring
+--
+Test that the following happens in order:
+execute line 4
+//
+// Save that the loop condition was never satisfied
+//
+save line 8
+execute line 6
+any lines
+execute line 4
+unwind
+//
+// Save that the loop condition was satisfied once but not twice
+//
+save line 8
+execute line 6
+any lines
+//
+// Escape the loop
+//
+execute line 8
+any lines
+path is successful
+//
+// Now do the first break out of the loop...
+//
+any lines
+execute line 4
+resume line 8
+execute line 8
+any lines
+path is successful
+//
+// ...and the second.
+//
+any lines
+execute line 4
+resume line 8
+execute line 8
+any lines
+path is successful
+end