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

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/test.desc → regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc

@@ -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$

src/goto-instrument/Makefile

@@ -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 \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -108,7 +108,6 @@ Author: Daniel Kroening, [email protected]
 #include "value_set_fi_fp_removal.h"
 
 #include "accelerate/accelerate.h"
-#include "synthesizer/enumerative_loop_invariant_synthesizer.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
@@ -1148,17 +1147,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
   }
 
-  if(cmdline.isset("synthesize-loop-invariants"))
-  {
-    log.warning() << "Loop invariant synthesizer is still work in progress. "
-                     "It only generates TRUE as invariants."
-                  << messaget::eom;
-
-    // Synthesize loop invariants and annotate them into `goto_model`
-    enumerative_loop_invariant_synthesizert synthesizer(goto_model, log);
-    annotate_invariants(synthesizer.synthesize_all(), goto_model, log);
-  }
-
   bool use_dfcc = cmdline.isset(FLAG_DFCC);
   if(use_dfcc)
   {
@@ -1978,7 +1966,6 @@ void goto_instrument_parse_optionst::help()
     "Code contracts:\n"
     HELP_DFCC
     HELP_LOOP_CONTRACTS
-    HELP_LOOP_INVARIANT_SYNTHESIZER
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT
     HELP_ENFORCE_CONTRACT_REC

src/goto-instrument/goto_instrument_parse_options.h

@@ -42,7 +42,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "contracts/contracts.h"
 #include "contracts/dynamic-frames/dfcc.h"
-#include "synthesizer/loop_invariant_synthesizer_base.h"
 #include "wmm/weak_memory.h"
 
 // clang-format off
@@ -120,7 +119,6 @@ Author: Daniel Kroening, [email protected]
   OPT_NONDET_VOLATILE \
   "(ensure-one-backedge-per-target)" \
   OPT_CONFIG_LIBRARY \
-  OPT_SYNTHESIZE_LOOP_INVARIANTS \
   // empty last line
 
 // clang-format on

src/goto-instrument/module_dependencies.txt

@@ -10,6 +10,5 @@ langapi # should go away
 linking
 pointer-analysis
 solvers
-synthesizer
 util
 wmm

src/goto-synthesizer/Makefile

@@ -1,14 +1,29 @@
-SRC = goto_synthesizer_languages.cpp \
+SRC = enumerative_loop_contracts_synthesizer.cpp \
+      expr_enumerator.cpp \
+      goto_synthesizer_languages.cpp \
       goto_synthesizer_main.cpp \
       goto_synthesizer_parse_options.cpp \
+      synthesizer_utils.cpp \
       # Empty last line
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
+      ../analyses/analyses$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-checker/goto-checker$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
+      ../goto-instrument/contracts/contracts$(OBJEXT) \
+      ../goto-instrument/contracts/utils$(OBJEXT) \
+      ../goto-instrument/contracts/instrument_spec_assigns$(OBJEXT) \
+      ../goto-instrument/contracts/memory_predicates$(OBJEXT) \
+      ../goto-instrument/contracts/inlining_decorator$(OBJEXT) \
+      ../goto-instrument/contracts/havoc_assigns_clause_targets$(OBJEXT) \
+      ../goto-instrument/havoc_utils$(OBJEXT) \
+      ../goto-instrument/loop_utils$(OBJEXT) \
+      ../goto-instrument/unwindset$(OBJEXT) \
+      ../goto-instrument/unwind$(OBJEXT) \
+      ../goto-instrument/nondet_static$(OBJEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../json/json$(LIBEXT) \

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp → src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -1,19 +1,19 @@
 /*******************************************************************\
 
-Module: Enumerative Loop Invariant Synthesizer
+Module: Enumerative Loop Contracts Synthesizer
 
 Author: Qinheping Hu
 
 \*******************************************************************/
 
 /// \file
-/// Enumerative Loop Invariant Synthesizer
+/// Enumerative Loop Contracts Synthesizer
 
-#include "enumerative_loop_invariant_synthesizer.h"
+#include "enumerative_loop_contracts_synthesizer.h"
 
 #include <analyses/natural_loops.h>
 
-void enumerative_loop_invariant_synthesizert::init_candidates()
+void enumerative_loop_contracts_synthesizert::init_candidates()
 {
   for(auto &function_p : goto_model.goto_functions.function_map)
   {
@@ -38,7 +38,7 @@ void enumerative_loop_invariant_synthesizert::init_candidates()
   }
 }
 
-invariant_mapt enumerative_loop_invariant_synthesizert::synthesize_all()
+invariant_mapt enumerative_loop_contracts_synthesizert::synthesize_all()
 {
   init_candidates();
 
@@ -47,7 +47,7 @@ invariant_mapt enumerative_loop_invariant_synthesizert::synthesize_all()
   return invariant_candiate_map;
 }
 
-exprt enumerative_loop_invariant_synthesizert::synthesize(loop_idt loop_id)
+exprt enumerative_loop_contracts_synthesizert::synthesize(loop_idt loop_id)
 {
   return true_exprt();
 }

src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h → src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h

@@ -1,41 +1,41 @@
 /*******************************************************************\
 
-Module: Enumerative Loop Invariant Synthesizer
+Module: Enumerative Loop Contracts Synthesizer
 
 Author: Qinheping Hu
 
 \*******************************************************************/
 
 /// \file
-/// Enumerative Loop Invariant Synthesizer
+/// Enumerative Loop Contracts Synthesizer
 
 // NOLINTNEXTLINE(whitespace/line_length)
-#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H
+#ifndef CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
 // NOLINTNEXTLINE(whitespace/line_length)
-#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H
+#define CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H
 
-#include "loop_invariant_synthesizer_base.h"
+#include "loop_contracts_synthesizer_base.h"
 
 class messaget;
 class goto_modelt;
 
-/// Enumerative loop invariant synthesizers.
+/// Enumerative loop contracts synthesizers.
 /// It is designed for `goto_model` containing only checks instrumented by
 /// `goto-instrument` with the `--pointer-check` flag.
 /// When other checks present, it will just enumerate candidates and check
 /// if they are valid.
-class enumerative_loop_invariant_synthesizert
-  : public loop_invariant_synthesizer_baset
+class enumerative_loop_contracts_synthesizert
+  : public loop_contracts_synthesizer_baset
 {
 public:
-  enumerative_loop_invariant_synthesizert(
+  enumerative_loop_contracts_synthesizert(
     const goto_modelt &goto_model,
     messaget &log)
-    : loop_invariant_synthesizer_baset(goto_model, log)
+    : loop_contracts_synthesizer_baset(goto_model, log)
   {
   }
 
-  /// This synthesizer guarantees that, with the synthesized loop invariants,
+  /// This synthesizer guarantees that, with the synthesized loop contracts,
   /// all checks in the annotated GOTO program pass.
   invariant_mapt synthesize_all() override;
   exprt synthesize(loop_idt loop_id) override;
@@ -48,4 +48,4 @@ class enumerative_loop_invariant_synthesizert
 };
 
 // NOLINTNEXTLINE(whitespace/line_length)
-#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_ENUMERATIVE_LOOP_INVARIANT_SYNTHESIZER_H
+#endif // CPROVER_GOTO_SYNTHESIZER_ENUMERATIVE_LOOP_CONTRACTS_SYNTHESIZER_H

src/goto-instrument/synthesizer/expr_enumerator.h → src/goto-synthesizer/expr_enumerator.h

@@ -6,8 +6,8 @@ Author: Qinheping Hu
 /// \file
 /// Enumerator Interface
 
-#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_EXPR_ENUMERATOR_H
-#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_EXPR_ENUMERATOR_H
+#ifndef CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H
+#define CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H
 
 #include <util/expr.h>
 
@@ -355,4 +355,4 @@ class recursive_enumerator_placeholdert : public enumerator_baset
   const enumerator_factoryt &factory;
 };
 
-#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_EXPR_ENUMERATOR_H
+#endif // CPROVER_GOTO_SYNTHESIZER_EXPR_ENUMERATOR_H