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

@@ -7,10 +7,14 @@ cleanup()
 
 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`
@@ -29,7 +33,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.