From 2a745f817ab56944c8a702d9e61e960d9e5d781c Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Mon, 12 Dec 2022 22:38:51 -0600 Subject: [PATCH] Migrate loop-contracts synthesizer from goto-instrument to goto-synthesizer --- CODEOWNERS | 1 - doc/man/goto-instrument.1 | 3 -- regression/CMakeLists.txt | 1 + regression/Makefile | 1 + regression/goto-synthesizer/CMakeLists.txt | 43 +++++++++++++++ regression/goto-synthesizer/Makefile | 42 +++++++++++++++ regression/goto-synthesizer/chain.sh | 44 ++++++++++++++++ .../loop_contracts_synthesis_01}/main.c | 0 .../loop_contracts_synthesis_01}/test.desc | 2 +- src/goto-instrument/Makefile | 3 -- .../goto_instrument_parse_options.cpp | 13 ----- .../goto_instrument_parse_options.h | 2 - src/goto-instrument/module_dependencies.txt | 1 - .../synthesizer/module_dependencies.txt | 8 --- src/goto-synthesizer/Makefile | 17 +++++- ...numerative_loop_contracts_synthesizer.cpp} | 12 ++--- .../enumerative_loop_contracts_synthesizer.h} | 24 ++++----- .../expr_enumerator.cpp | 0 .../expr_enumerator.h | 6 +-- .../goto_synthesizer_parse_options.cpp | 52 +++++++++++++++++++ .../loop_contracts_synthesizer_base.h} | 20 +++---- src/goto-synthesizer/module_dependencies.txt | 1 + .../synthesizer_utils.cpp | 0 .../synthesizer_utils.h | 6 +-- unit/CMakeLists.txt | 1 + unit/Makefile | 4 +- .../expr_enumerator/expr_enumerator.cpp | 2 +- .../expr_enumerator/module_dependencies.txt | 2 +- 28 files changed, 240 insertions(+), 71 deletions(-) create mode 100644 regression/goto-synthesizer/CMakeLists.txt create mode 100644 regression/goto-synthesizer/Makefile create mode 100755 regression/goto-synthesizer/chain.sh rename regression/{contracts/loop_invariant_synthesis_01 => goto-synthesizer/loop_contracts_synthesis_01}/main.c (100%) rename regression/{contracts/loop_invariant_synthesis_01 => goto-synthesizer/loop_contracts_synthesis_01}/test.desc (91%) delete mode 100644 src/goto-instrument/synthesizer/module_dependencies.txt rename src/{goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp => goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp} (77%) rename src/{goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h => goto-synthesizer/enumerative_loop_contracts_synthesizer.h} (60%) rename src/{goto-instrument/synthesizer => goto-synthesizer}/expr_enumerator.cpp (100%) rename src/{goto-instrument/synthesizer => goto-synthesizer}/expr_enumerator.h (98%) rename src/{goto-instrument/synthesizer/loop_invariant_synthesizer_base.h => goto-synthesizer/loop_contracts_synthesizer_base.h} (68%) rename src/{goto-instrument/synthesizer => goto-synthesizer}/synthesizer_utils.cpp (100%) rename src/{goto-instrument/synthesizer => goto-synthesizer}/synthesizer_utils.h (90%) rename unit/{goto-instrument => goto-synthesizer}/expr_enumerator/expr_enumerator.cpp (99%) rename unit/{goto-instrument => goto-synthesizer}/expr_enumerator/module_dependencies.txt (61%) diff --git a/CODEOWNERS b/CODEOWNERS index 4dc3105e9d4..649d38d6e5f 100644 --- a/CODEOWNERS +++ b/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 diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1 index 89c7c501175..567ca6bb0fd 100644 --- a/doc/man/goto-instrument.1 +++ b/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 diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index fee76490541..d3a5ae972af 100644 --- a/regression/CMakeLists.txt +++ b/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) diff --git a/regression/Makefile b/regression/Makefile index 9578500dcb5..dc734b936a4 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -39,6 +39,7 @@ DIRS = cbmc \ systemc \ contracts \ contracts-dfcc \ + goto-synthesizer \ acceleration \ k-induction \ goto-harness \ diff --git a/regression/goto-synthesizer/CMakeLists.txt b/regression/goto-synthesizer/CMakeLists.txt new file mode 100644 index 00000000000..0bae5992db2 --- /dev/null +++ b/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 $ $ $ ${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 $ $ '$ --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 $ $ '$ --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}:$" +# ) +#endif() diff --git a/regression/goto-synthesizer/Makefile b/regression/goto-synthesizer/Makefile new file mode 100644 index 00000000000..ae4556c8ea7 --- /dev/null +++ b/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 diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh new file mode 100755 index 00000000000..3751b4b8403 --- /dev/null +++ b/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} diff --git a/regression/contracts/loop_invariant_synthesis_01/main.c b/regression/goto-synthesizer/loop_contracts_synthesis_01/main.c similarity index 100% rename from regression/contracts/loop_invariant_synthesis_01/main.c rename to regression/goto-synthesizer/loop_contracts_synthesis_01/main.c diff --git a/regression/contracts/loop_invariant_synthesis_01/test.desc b/regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc similarity index 91% rename from regression/contracts/loop_invariant_synthesis_01/test.desc rename to regression/goto-synthesizer/loop_contracts_synthesis_01/test.desc index 1ff43bb978d..8b97754a993 100644 --- a/regression/contracts/loop_invariant_synthesis_01/test.desc +++ b/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$ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index bfa8ae84975..67deed54d59 100644 --- a/src/goto-instrument/Makefile +++ b/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 \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1a21921c827..978476edac2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -108,7 +108,6 @@ Author: Daniel Kroening, kroening@kroening.com #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 diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 6aa7343c6c6..785ea7450a8 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -42,7 +42,6 @@ Author: Daniel Kroening, kroening@kroening.com #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, kroening@kroening.com OPT_NONDET_VOLATILE \ "(ensure-one-backedge-per-target)" \ OPT_CONFIG_LIBRARY \ - OPT_SYNTHESIZE_LOOP_INVARIANTS \ // empty last line // clang-format on diff --git a/src/goto-instrument/module_dependencies.txt b/src/goto-instrument/module_dependencies.txt index 2d0fb1c54dd..cf5716d37ac 100644 --- a/src/goto-instrument/module_dependencies.txt +++ b/src/goto-instrument/module_dependencies.txt @@ -10,6 +10,5 @@ langapi # should go away linking pointer-analysis solvers -synthesizer util wmm diff --git a/src/goto-instrument/synthesizer/module_dependencies.txt b/src/goto-instrument/synthesizer/module_dependencies.txt deleted file mode 100644 index 290dab44704..00000000000 --- a/src/goto-instrument/synthesizer/module_dependencies.txt +++ /dev/null @@ -1,8 +0,0 @@ -analyses -ansi-c -goto-instrument/contracts -goto-instrument/synthesizer -goto-instrument -goto-programs -langapi -util diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile index f59fa616396..729d94d747a 100644 --- a/src/goto-synthesizer/Makefile +++ b/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) \ diff --git a/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp similarity index 77% rename from src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp rename to src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp index 67dbc3ed068..a7e60f0fa5c 100644 --- a/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.cpp +++ b/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 -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(); } diff --git a/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h b/src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h similarity index 60% rename from src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h rename to src/goto-synthesizer/enumerative_loop_contracts_synthesizer.h index 160531198f4..ba9b538e9a2 100644 --- a/src/goto-instrument/synthesizer/enumerative_loop_invariant_synthesizer.h +++ b/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 diff --git a/src/goto-instrument/synthesizer/expr_enumerator.cpp b/src/goto-synthesizer/expr_enumerator.cpp similarity index 100% rename from src/goto-instrument/synthesizer/expr_enumerator.cpp rename to src/goto-synthesizer/expr_enumerator.cpp diff --git a/src/goto-instrument/synthesizer/expr_enumerator.h b/src/goto-synthesizer/expr_enumerator.h similarity index 98% rename from src/goto-instrument/synthesizer/expr_enumerator.h rename to src/goto-synthesizer/expr_enumerator.h index 3a471901430..3369f989fca 100644 --- a/src/goto-instrument/synthesizer/expr_enumerator.h +++ b/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 @@ -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 diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp index a649c9b9b50..a241666b674 100644 --- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -13,6 +13,13 @@ Author: Qinheping Hu #include #include +#include +#include + +#include +#include + +#include "enumerative_loop_contracts_synthesizer.h" #include @@ -43,6 +50,51 @@ int goto_synthesizer_parse_optionst::doit() // TODO // Migrate synthesizer and tests from goto-instrument to goto-synthesizer + { + // Synthesize loop invariants and annotate them into `goto_model` + enumerative_loop_contracts_synthesizert synthesizer(goto_model, log); + annotate_invariants(synthesizer.synthesize_all(), goto_model, log); + + // Apply loop contracts. + std::set to_exclude_from_nondet_static( + cmdline.get_values("nondet-static-exclude").begin(), + cmdline.get_values("nondet-static-exclude").end()); + code_contractst contracts(goto_model, log); + contracts.apply_loop_contracts(to_exclude_from_nondet_static); + } + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + // add loop ids + goto_model.goto_functions.compute_loop_numbers(); + + // label the assertions + label_properties(goto_model); + + // recalculate numbers, etc. + goto_model.goto_functions.update(); + + // write new binary? + if(cmdline.args.size() == 2) + { + log.status() << "Writing GOTO program to '" << cmdline.args[1] << "'" + << messaget::eom; + + if(write_goto_binary(cmdline.args[1], goto_model, ui_message_handler)) + return CPROVER_EXIT_CONVERSION_FAILED; + else + return CPROVER_EXIT_SUCCESS; + } + else if(cmdline.args.size() < 2) + { + throw invalid_command_line_argument_exceptiont( + "Invalid number of positional arguments passed", + "[in] [out]", + "goto-instrument needs one input and one output file, aside from other " + "flags"); + } + help(); return CPROVER_EXIT_USAGE_ERROR; } diff --git a/src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h b/src/goto-synthesizer/loop_contracts_synthesizer_base.h similarity index 68% rename from src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h rename to src/goto-synthesizer/loop_contracts_synthesizer_base.h index 1c2fbca73f8..1be6c305917 100644 --- a/src/goto-instrument/synthesizer/loop_invariant_synthesizer_base.h +++ b/src/goto-synthesizer/loop_contracts_synthesizer_base.h @@ -1,16 +1,16 @@ /*******************************************************************\ -Module: Loop Invariant Synthesizer Interface +Module: Loop Contracts Synthesizer Interface Author: Qinheping Hu \*******************************************************************/ /// \file -/// Loop Invariant Synthesizer Interface +/// Loop Contracts Synthesizer Interface -#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H -#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H +#ifndef CPROVER_GOTO_SYNTHESIZER_LOOP_CONTRACTS_SYNTHESIZER_BASE_H +#define CPROVER_GOTO_SYNTHESIZER_LOOP_CONTRACTS_SYNTHESIZER_BASE_H #include @@ -23,20 +23,20 @@ Author: Qinheping Hu class messaget; -/// A base class for loop invariant synthesizers. -/// Provides a method for synthesizing loop invariants in a given `goto_model`. +/// A base class for loop contracts synthesizers. +/// Provides a method for synthesizing loop contracts in a given `goto_model`. /// /// Derived class should clarify what types of `goto_model` they targets, e.g., /// a `goto_model` contains only memory safety checks, or a `goto_model` /// contains both memory safety checks and correctness checks. -class loop_invariant_synthesizer_baset +class loop_contracts_synthesizer_baset { public: - loop_invariant_synthesizer_baset(const goto_modelt &goto_model, messaget &log) + loop_contracts_synthesizer_baset(const goto_modelt &goto_model, messaget &log) : goto_model(goto_model), log(log) { } - virtual ~loop_invariant_synthesizer_baset() = default; + virtual ~loop_contracts_synthesizer_baset() = default; /// Synthesize loop invariants that are inductive in the given GOTO program. /// @@ -52,4 +52,4 @@ class loop_invariant_synthesizer_baset messaget &log; }; -#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_LOOP_INVARIANT_SYNTHESIZER_BASE_H +#endif // CPROVER_GOTO_SYNTHESIZER_LOOP_CONTRACTS_SYNTHESIZER_BASE_H diff --git a/src/goto-synthesizer/module_dependencies.txt b/src/goto-synthesizer/module_dependencies.txt index e0cd705e3c7..2ce15c2eaad 100644 --- a/src/goto-synthesizer/module_dependencies.txt +++ b/src/goto-synthesizer/module_dependencies.txt @@ -1,3 +1,4 @@ +analyses ansi-c cpp goto-checker diff --git a/src/goto-instrument/synthesizer/synthesizer_utils.cpp b/src/goto-synthesizer/synthesizer_utils.cpp similarity index 100% rename from src/goto-instrument/synthesizer/synthesizer_utils.cpp rename to src/goto-synthesizer/synthesizer_utils.cpp diff --git a/src/goto-instrument/synthesizer/synthesizer_utils.h b/src/goto-synthesizer/synthesizer_utils.h similarity index 90% rename from src/goto-instrument/synthesizer/synthesizer_utils.h rename to src/goto-synthesizer/synthesizer_utils.h index 40620f7feac..a71f0413a87 100644 --- a/src/goto-instrument/synthesizer/synthesizer_utils.h +++ b/src/goto-synthesizer/synthesizer_utils.h @@ -6,8 +6,8 @@ Author: Qinheping Hu \*******************************************************************/ -#ifndef CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_SYNTHESIZER_UTILS_H -#define CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_SYNTHESIZER_UTILS_H +#ifndef CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H +#define CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H #include #include @@ -53,4 +53,4 @@ void annotate_invariants( goto_modelt &goto_model, messaget &log); -#endif // CPROVER_GOTO_INSTRUMENT_SYNTHESIZER_SYNTHESIZER_UTILS_H +#endif // CPROVER_GOTO_SYNTHESIZER_SYNTHESIZER_UTILS_H diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index c81399af77a..c0bf0765dea 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -84,6 +84,7 @@ target_link_libraries( goto-checker goto-programs goto-instrument-lib + goto-synthesizer-lib goto-symex cbmc-lib json-symtab-language diff --git a/unit/Makefile b/unit/Makefile index 904fb2c9210..6bc34935e2c 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -59,7 +59,7 @@ SRC += analyses/ai/ai.cpp \ goto-checker/report_util/is_property_less_than.cpp \ goto-instrument/cover_instrument.cpp \ goto-instrument/cover/cover_only.cpp \ - goto-instrument/expr_enumerator/expr_enumerator.cpp \ + goto-synthesizer/expr_enumerator/expr_enumerator.cpp \ goto-programs/allocate_objects.cpp \ goto-programs/goto_program_assume.cpp \ goto-programs/goto_program_dead.cpp \ @@ -248,7 +248,7 @@ BMC_DEPS =../src/cbmc/c_test_input_generator$(OBJEXT) \ ../src/goto-instrument/nondet_static$(OBJEXT) \ ../src/goto-instrument/full_slicer$(OBJEXT) \ ../src/goto-instrument/unwindset$(OBJEXT) \ - ../src/goto-instrument/synthesizer/expr_enumerator$(OBJEXT) \ + ../src/goto-synthesizer/expr_enumerator$(OBJEXT) \ ../src/xmllang/xmllang$(LIBEXT) \ ../src/goto-symex/goto-symex$(LIBEXT) \ ../src/jsil/jsil$(LIBEXT) \ diff --git a/unit/goto-instrument/expr_enumerator/expr_enumerator.cpp b/unit/goto-synthesizer/expr_enumerator/expr_enumerator.cpp similarity index 99% rename from unit/goto-instrument/expr_enumerator/expr_enumerator.cpp rename to unit/goto-synthesizer/expr_enumerator/expr_enumerator.cpp index be2955b15a3..f8d7b0c221b 100644 --- a/unit/goto-instrument/expr_enumerator/expr_enumerator.cpp +++ b/unit/goto-synthesizer/expr_enumerator/expr_enumerator.cpp @@ -12,7 +12,7 @@ Author: Qinheping Hu #include #include -#include +#include #include TEST_CASE("enumeratingsummation expressions", "[core]") diff --git a/unit/goto-instrument/expr_enumerator/module_dependencies.txt b/unit/goto-synthesizer/expr_enumerator/module_dependencies.txt similarity index 61% rename from unit/goto-instrument/expr_enumerator/module_dependencies.txt rename to unit/goto-synthesizer/expr_enumerator/module_dependencies.txt index 1c54d0c63ab..52a52f46eef 100644 --- a/unit/goto-instrument/expr_enumerator/module_dependencies.txt +++ b/unit/goto-synthesizer/expr_enumerator/module_dependencies.txt @@ -1,4 +1,4 @@ -goto-instrument +goto-synthesizer testing-utils util langapi