Merge pull request #5901 from tautschnig/enable-acceleration-tests

Enable acceleration tests

Author: NlightNFotis

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.

src/goto-instrument/accelerate/scratch_program.cpp

@@ -36,20 +36,20 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex_state = util_make_unique<goto_symex_statet>(
-    symex_targett::sourcet(goto_functionst::entry_point(), *this),
-    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
-    guard_manager,
-    [this](const irep_idt &id) {
-      return path_storage.get_unique_l2_index(id);
-    });
-
-  symex.symex_with_state(
-    *symex_state,
-    [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
+  goto_functiont this_goto_function;
+  this_goto_function.body.copy_from(*this);
+  auto get_goto_function =
+    [this, &this_goto_function](
+      const irep_idt &key) -> const goto_functionst::goto_functiont & {
+    if(key == goto_functionst::entry_point())
+      return this_goto_function;
+    else
       return functions.function_map.at(key);
-    },
-    symex_symbol_table);
+  };
+
+  symex_state = symex.initialize_entry_point_state(get_goto_function);
+
+  symex.symex_with_state(*symex_state, get_goto_function, symex_symbol_table);
 
   if(do_slice)
   {

src/goto-instrument/accelerate/scratch_program.h

@@ -33,6 +33,33 @@ Author: Matt Lewis
 
 #include "path.h"
 
+// Wrapper around goto_symext to make initialize_entry_point_state available.
+struct scratch_program_symext : public goto_symext
+{
+  scratch_program_symext(
+    message_handlert &mh,
+    const symbol_tablet &outer_symbol_table,
+    symex_target_equationt &_target,
+    const optionst &options,
+    path_storaget &path_storage,
+    guard_managert &guard_manager)
+    : goto_symext(
+        mh,
+        outer_symbol_table,
+        _target,
+        options,
+        path_storage,
+        guard_manager)
+  {
+  }
+
+  std::unique_ptr<statet>
+  initialize_entry_point_state(const get_goto_functiont &get_goto_function)
+  {
+    return goto_symext::initialize_entry_point_state(get_goto_function);
+  }
+};
+
 class scratch_programt:public goto_programt
 {
 public:
@@ -85,7 +112,7 @@ class scratch_programt:public goto_programt
   symex_target_equationt equation;
   path_fifot path_storage;
   optionst options;
-  goto_symext symex;
+  scratch_program_symext symex;
 
   std::unique_ptr<propt> satcheck;
   bv_pointerst satchecker;