Enable regression tests of loop acceleration

With the bugs fixed in the preceding commit, tests run without crashing.
For some of them, however, the reported results are incorrect. These are
now marked as KNOWNBUG and need debugging at a later time.

Author: tautschnig

regression/CMakeLists.txt

@@ -52,6 +52,7 @@ add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
+add_subdirectory(acceleration)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-harness-multi-file-project)
 add_subdirectory(goto-cc-file-local)

regression/Makefile

@@ -27,6 +27,7 @@ DIRS = cbmc \
        statement-list \
        systemc \
        contracts \
+       acceleration \
        goto-harness \
        goto-harness-multi-file-project \
        goto-cc-file-local \

regression/acceleration/CMakeLists.txt

@@ -0,0 +1,12 @@
+if(WIN32)
+    set(is_windows true)
+else()
+    set(is_windows false)
+endif()
+
+add_test_pl_tests(
+  "../accelerate.sh \
+   $<TARGET_FILE:goto-cc> \
+   $<TARGET_FILE:goto-instrument> \
+   $<TARGET_FILE:cbmc> \
+   ${is_windows}")

regression/acceleration/Makefile

@@ -1,10 +1,24 @@
 default: tests.log
 
+include ../../src/config.inc
+include ../../src/common
+
+GOTO_INSTRUMENT_EXE=../../../src/goto-instrument/goto-instrument
+CBMC_EXE=../../../src/cbmc/cbmc
+
+ifeq ($(BUILD_ENV_),MSVC)
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cl
+	is_windows=true
+else
+	GOTO_CC_EXE=../../../src/goto-cc/goto-cc
+	is_windows=false
+endif
+
 test:
-	@../test.pl -c ../../../src/goto-instrument/accelerate/accelerate.sh
+	@../test.pl -e -p -c "../accelerate.sh $(GOTO_CC_EXE) $(GOTO_INSTRUMENT_EXE) $(CBMC_EXE) $(is_windows)"
 
 tests.log: ../test.pl
-	@../test.pl -c ../../../src/goto-instrument/accelerate/accelerate.sh
+	@../test.pl -e -p -c "../accelerate.sh $(GOTO_CC_EXE) $(GOTO_INSTRUMENT_EXE) $(CBMC_EXE) $(is_windows)"
 
 show:
 	@for dir in *; do \

regression/acceleration/accelerate.sh

@@ -2,20 +2,30 @@
 
 cleanup()
 {
-  rm -f $ofile $accfile $instrfile
+  rm -rf "$target_dir"
 }
 
 trap cleanup EXIT
 
-bindir=`dirname $0`
-goto_cc="$bindir/../../goto-cc/goto-cc"
-goto_instrument="$bindir/../goto-instrument"
-cbmc="$bindir/../../cbmc/cbmc"
+set -e
+
+goto_cc=$1
+goto_instrument=$2
+cbmc=$3
+is_windows=$4
+shift 4
+
 cfile=""
 cbmcargs=""
-ofile=`mktemp`
-instrfile=`mktemp`
-accfile=`mktemp`
+
+# create the temporary directory relative to the current directory, thus
+# avoiding file names that start with a "/", which confuses goto-cl (Windows)
+# when running in git-bash.
+target_dir="$(TMPDIR=. mktemp -d)"
+
+ofile="$target_dir/compiled.gb"
+instrfile="$target_dir/instrumented.gb"
+accfile="$target_dir/accelerated.gb"
 
 for a in "$@"
 do
@@ -29,7 +39,12 @@ case $a in
 esac
 done
 
-$goto_cc $cfile -o $ofile || exit 1
-$goto_instrument --inline --remove-pointers $ofile $instrfile || exit 1
-timeout 5 $goto_instrument --accelerate $instrfile $accfile
-timeout 5 $cbmc --unwind 5 --z3 $cbmcargs $accfile
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "$cfile" "/Fe$ofile"
+else
+  $goto_cc -o "$ofile" "$cfile"
+fi
+
+"$goto_instrument" --inline --remove-pointers "$ofile" "$instrfile"
+"$goto_instrument" --accelerate "$instrfile" "$accfile"
+"$cbmc" --unwind 5 $cbmcargs "$accfile"

regression/acceleration/array_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe2/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe3/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/array_unsafe4/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/const_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/diamond_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/functions_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/nested_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/overflow_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/phases_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/simple_unsafe1/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.

regression/acceleration/simple_unsafe4/test.desc

@@ -1,6 +1,8 @@
-CORE
+KNOWNBUG
 main.c
 --no-unwinding-assertions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+--
+The result spuriously is VERIFICATION SUCCESSFUL.