Merge pull request #7429 from qinheping/goto-synthesizer-migration

SYNTHESIZER: Migrate loop-contracts synthesizer from goto-instrument to goto-synthesizer

Author: qinheping

CODEOWNERS

@@ -52,7 +52,6 @@
 /src/goto-harness/ @martin-cs @chris-ryder @peterschrammel
 /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
-/src/goto-instrument/synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig

doc/man/goto-instrument.1

@@ -999,9 +999,6 @@ force aggressive slicer to preserve all direct paths
 \fB\-\-apply\-loop\-contracts\fR
 check and use loop contracts when provided
 .TP
-\fB\-\-synthesize\-loop\-invariants\fR
-synthesize and apply loop invariants
-.TP
 \fB\-\-replace\-call\-with\-contract\fR \fIfun\fR
 replace calls to \fIfun\fR with \fIfun\fR's contract
 .TP

regression/CMakeLists.txt

@@ -66,6 +66,7 @@ add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
 add_subdirectory(contracts-dfcc)
+add_subdirectory(goto-synthesizer)
 add_subdirectory(acceleration)
 add_subdirectory(k-induction)
 add_subdirectory(goto-harness)

regression/Makefile

@@ -39,6 +39,7 @@ DIRS = cbmc \
        systemc \
        contracts \
        contracts-dfcc \
+       goto-synthesizer \
        acceleration \
        k-induction \
        goto-harness \

regression/goto-synthesizer/CMakeLists.txt

@@ -0,0 +1,43 @@
+if(WIN32)
+  set(is_windows true)
+else()
+  set(is_windows false)
+endif()
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only -X gcc-only)
+  set(gcc_only_string "-X;gcc-only;")
+else()
+  set(gcc_only "")
+  set(gcc_only_string "")
+endif()
+
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-synthesizer> $<TARGET_FILE:cbmc> ${is_windows}"
+)
+
+## Enabling these causes a very significant increase in the time taken to run the regressions
+
+#add_test_pl_profile(
+#    "cbmc-z3"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-synthesizer> '$<TARGET_FILE:cbmc> --z3' ${is_windows}"
+#    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-z3-backend;-X;thorough-z3-backend;${gcc_only_string}-s;z3"
+#    "CORE"
+#)
+
+#add_test_pl_profile(
+#    "cbmc-cprover-smt2"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-synthesizer> '$<TARGET_FILE:cbmc> --cprover-smt2' ${is_windows}"
+#    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt2-backend;-X;thorough-cprover-smt2-backend;${gcc_only_string}-s;cprover-smt2"
+#    "CORE"
+#)
+
+# solver appears on the PATH in Windows already
+#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+#  set_property(
+#    TEST "cbmc-cprover-smt2-CORE"
+#    PROPERTY ENVIRONMENT
+#      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+#  )
+#endif()

regression/goto-synthesizer/Makefile

@@ -0,0 +1,42 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+	GCC_ONLY = -X gcc-only
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+	GCC_ONLY =
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
+
+test-cprover-smt2:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
+					  -s cprover-smt2 $(GCC_ONLY)
+
+test-z3:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-synthesizer/goto-synthesizer "../../../src/cbmc/cbmc --z3" $(is_windows)' \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
+
+tests.log: ../test.pl test
+
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb *.smt2; \
+			cd ..; \
+		fi \
+	done

regression/goto-synthesizer/chain.sh

@@ -0,0 +1,44 @@
+#!/bin/bash
+
+set -e
+
+goto_cc=$1
+goto_synthesizer=$2
+cbmc=$3
+is_windows=$4
+
+name=${*:$#}
+name=${name%.c}
+
+args=${*:5:$#-5}
+if [[ "$args" != *" _ "* ]]
+then
+  args_inst=$args
+  args_cbmc=""
+else
+  args_inst="${args%%" _ "*}"
+  args_cbmc="${args#*" _ "}"
+fi
+
+if [[ "${is_windows}" == "true" ]]; then
+  $goto_cc "${name}.c" "/Fe${name}.gb"
+else
+  $goto_cc -o "${name}.gb" "${name}.c"
+fi
+
+rm -f "${name}-mod.gb"
+$goto_synthesizer ${args_inst} "${name}.gb" "${name}-mod.gb"
+if [ ! -e "${name}-mod.gb" ] ; then
+  cp "$name.gb" "${name}-mod.gb"
+elif echo $args_inst | grep -q -- "--dump-c" ; then
+  mv "${name}-mod.gb" "${name}-mod.c"
+
+  if [[ "${is_windows}" == "true" ]]; then
+    $goto_cc "${name}-mod.c" "/Fe${name}-mod.gb"
+  else
+    $goto_cc -o "${name}-mod.gb" "${name}-mod.c"
+  fi
+
+  rm "${name}-mod.c"
+fi
+$cbmc "${name}-mod.gb" ${args_cbmc}

regression/contracts/loop_invariant_synthesis_01/main.c renamed to regression/goto-synthesizer/loop_contracts_synthesis_01/main.c

@@ -1,6 +1,6 @@
 CORE
 main.c
---synthesize-loop-invariants --apply-loop-contracts
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[main\.\d+\] line 10 Check loop invariant before entry: SUCCESS$

regression/contracts/loop_invariant_synthesis_01/test.desc renamed to regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc

@@ -83,9 +83,6 @@ SRC = accelerate/accelerate.cpp \
       source_lines.cpp \
       splice_call.cpp \
       stack_depth.cpp \
-      synthesizer/enumerative_loop_invariant_synthesizer.cpp \
-      synthesizer/expr_enumerator.cpp \
-      synthesizer/synthesizer_utils.cpp \
       thread_instrumentation.cpp \
       undefined_functions.cpp \
       uninitialized.cpp \