diff --git a/CMakeLists.txt b/CMakeLists.txt index 9b3cf172173..8142b40e31b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -157,6 +157,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR "$" "$" "$" + "$" "$" "$" "$" @@ -233,6 +234,8 @@ cprover_default_properties( goto-instrument-lib goto-programs goto-symex + goto-synthesizer + goto-synthesizer-lib jsil json json-symtab-language diff --git a/CODEOWNERS b/CODEOWNERS index e8456ac92b0..4dc3105e9d4 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -53,6 +53,7 @@ /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 /src/memory-analyzer/ @tautschnig @chris-ryder @kroening diff --git a/doc/man/goto-synthesizer.1 b/doc/man/goto-synthesizer.1 new file mode 100644 index 00000000000..edbf4138740 --- /dev/null +++ b/doc/man/goto-synthesizer.1 @@ -0,0 +1,40 @@ +.TH GOTO-SYNTHESIZER "1" "December 2022" "goto-synthesizer-5.59.0" "User Commands" +.SH NAME +goto\-synthesizer \- Synthesize and apply loop contracts of goto binaries. +.SH SYNOPSIS +.TP +.B goto\-synthesizer [\-?] [\-h] [\-\-help] +show help +.TP +.B goto\-synthesizer \-\-version +show version and exit +.TP +.B goto\-synthesizer [options] \fIin\fR [\fIout\fR] +perform synthesis and loop-contracts transformation +.SH DESCRIPTION +\fBgoto-synthesis\fR reads a GOTO binary, performs loop-contracts synthesis and +program transformation for the synthesized contracts, and then writes the +resulting program as GOTO binary on disk. +.SH OPTIONS +.SS "User-interface options:" +.TP +\fB\-\-xml\-ui\fR +use XML\-formatted output +.TP +\fB\-\-json\-ui\fR +use JSON\-formatted output +.TP +\fB\-\-verbosity\fR \fIn\fR +verbosity level +.SH ENVIRONMENT +All tools honor the TMPDIR environment variable when generating temporary +files and directories. +.SH BUGS +If you encounter a problem please create an issue at +.B https://github.com/diffblue/cbmc/issues +.SH SEE ALSO +.BR cbmc (1), +.BR goto-cc (1) +.BR goto-instrument (1) +.SH COPYRIGHT +2022, Qinheping Hu diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ecc6b2b3e66..b2bb12e8a49 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -117,6 +117,7 @@ add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) add_subdirectory(goto-harness) +add_subdirectory(goto-synthesizer) add_subdirectory(symtab2gb) if(UNIX OR WITH_MEMORY_ANALYZER) diff --git a/src/Makefile b/src/Makefile index 698292d6e60..e176aac6270 100644 --- a/src/Makefile +++ b/src/Makefile @@ -14,6 +14,7 @@ DIRS = analyses \ goto-harness \ goto-programs \ goto-symex \ + goto-synthesizer \ jsil \ json \ json-symtab-language \ @@ -36,6 +37,7 @@ all: cbmc.dir \ goto-diff.dir \ goto-instrument.dir \ goto-harness.dir \ + goto-synthesizer.dir \ symtab2gb.dir \ # Empty last line @@ -104,6 +106,10 @@ memory-analyzer.dir: util.dir goto-programs.dir langapi.dir linking.dir \ symtab2gb.dir: util.dir goto-programs.dir langapi.dir linking.dir \ json.dir json-symtab-language.dir ansi-c.dir +goto-synthesizer.dir: languages util.dir goto-programs.dir langapi.dir \ + json.dir goto-checker.dir \ + goto-instrument.dir + # building for a particular directory $(patsubst %, %.dir, $(DIRS)): @@ -180,7 +186,7 @@ doc : install: all for b in \ cbmc crangler \ - goto-analyzer goto-cc goto-diff goto-instrument goto-harness \ + goto-analyzer goto-cc goto-diff goto-instrument goto-harness goto-synthesizer \ symtab2gb ; do \ cp $$b/$$b $(PREFIX)/bin/ ; \ cp ../doc/man/$$b.1 $(PREFIX)/doc/man/man1/ ; \ diff --git a/src/goto-synthesizer/CMakeLists.txt b/src/goto-synthesizer/CMakeLists.txt new file mode 100644 index 00000000000..fb4d06cc985 --- /dev/null +++ b/src/goto-synthesizer/CMakeLists.txt @@ -0,0 +1,33 @@ +# Library +file(GLOB_RECURSE sources "*.cpp" "*.h") +list(REMOVE_ITEM sources + ${CMAKE_CURRENT_SOURCE_DIR}/goto_synthesizer_main.cpp +) +add_library(goto-synthesizer-lib ${sources}) + +generic_includes(goto-synthesizer-lib) + +target_link_libraries(goto-synthesizer-lib + ansi-c + cpp + big-int + goto-checker + goto-instrument-lib + goto-programs + langapi + util + json +) + +# Executable +add_executable(goto-synthesizer goto_synthesizer_main.cpp) +target_link_libraries(goto-synthesizer goto-synthesizer-lib) +install(TARGETS goto-synthesizer DESTINATION ${CMAKE_INSTALL_BINDIR}) + +# Man page +if(NOT WIN32) + install( + DIRECTORY ${CMAKE_SOURCE_DIR}/doc/man/ + DESTINATION ${CMAKE_INSTALL_MANDIR}/man1 + FILES_MATCHING PATTERN "goto-synthesizer*") +endif() diff --git a/src/goto-synthesizer/Makefile b/src/goto-synthesizer/Makefile new file mode 100644 index 00000000000..f59fa616396 --- /dev/null +++ b/src/goto-synthesizer/Makefile @@ -0,0 +1,36 @@ +SRC = goto_synthesizer_languages.cpp \ + goto_synthesizer_main.cpp \ + goto_synthesizer_parse_options.cpp \ + # Empty last line + +OBJ += ../ansi-c/ansi-c$(LIBEXT) \ + ../cpp/cpp$(LIBEXT) \ + ../linking/linking$(LIBEXT) \ + ../big-int/big-int$(LIBEXT) \ + ../goto-checker/goto-checker$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../util/util$(LIBEXT) \ + ../json/json$(LIBEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +CLEANFILES = goto-synthesizer$(EXEEXT) goto-synthesizer$(LIBEXT) + +include ../config.inc +include ../common + +all: goto-synthesizer$(EXEEXT) + +############################################################################### + +goto-synthesizer$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: goto-synthesizer-mac-signed + +goto-synthesizer-mac-signed: goto-synthesizer$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-synthesizer$(EXEEXT) diff --git a/src/goto-synthesizer/README.md b/src/goto-synthesizer/README.md new file mode 100644 index 00000000000..d49ee154f54 --- /dev/null +++ b/src/goto-synthesizer/README.md @@ -0,0 +1,8 @@ +\ingroup module_hidden +\defgroup goto-synthesizer goto-synthesizer + +# Folder goto-synthesizer + +\author Qinheping Hu + +The `goto-synthesizer/` contains all processing of loop-contracts synthesizer. diff --git a/src/goto-synthesizer/goto_synthesizer_languages.cpp b/src/goto-synthesizer/goto_synthesizer_languages.cpp new file mode 100644 index 00000000000..99e1f841640 --- /dev/null +++ b/src/goto-synthesizer/goto_synthesizer_languages.cpp @@ -0,0 +1,19 @@ +/*******************************************************************\ +Module: Language Registration +Author: Qinheping Hu +\*******************************************************************/ + +/// \file +/// Language Registration + +#include +#include +#include + +#include "goto_synthesizer_parse_options.h" + +void goto_synthesizer_parse_optionst::register_languages() +{ + register_language(new_ansi_c_language); + register_language(new_cpp_language); +} diff --git a/src/goto-synthesizer/goto_synthesizer_main.cpp b/src/goto-synthesizer/goto_synthesizer_main.cpp new file mode 100644 index 00000000000..c912ace9564 --- /dev/null +++ b/src/goto-synthesizer/goto_synthesizer_main.cpp @@ -0,0 +1,27 @@ +/*******************************************************************\ +Module: Main Module +Author: Qinheping Hu +\*******************************************************************/ + +/// \file +/// Main Module + +#ifdef _MSC_VER +# include +#endif + +#include "goto_synthesizer_parse_options.h" + +#ifdef _MSC_VER +int wmain(int argc, const wchar_t **argv_wide) +{ + auto vec = narrow_argv(argc, argv_wide); + auto narrow = to_c_str_array(std::begin(vec), std::end(vec)); + auto argv = narrow.data(); +#else +int main(int argc, const char **argv) +{ +#endif + goto_synthesizer_parse_optionst parse_options(argc, argv); + return parse_options.main(); +} diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp new file mode 100644 index 00000000000..a649c9b9b50 --- /dev/null +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp @@ -0,0 +1,92 @@ +/*******************************************************************\ +Module: Parse Options Module +Author: Qinheping Hu +\*******************************************************************/ + +/// \file +/// Main Module + +#include "goto_synthesizer_parse_options.h" + +#include +#include +#include + +#include + +#include + +/// invoke main modules +int goto_synthesizer_parse_optionst::doit() +{ + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << '\n'; + return CPROVER_EXIT_SUCCESS; + } + + if(cmdline.args.size() != 1 && cmdline.args.size() != 2) + { + help(); + return CPROVER_EXIT_USAGE_ERROR; + } + + messaget::eval_verbosity( + cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler); + + register_languages(); + + const auto result_get_goto_program = get_goto_program(); + if(result_get_goto_program != CPROVER_EXIT_SUCCESS) + return result_get_goto_program; + + // TODO + // Migrate synthesizer and tests from goto-instrument to goto-synthesizer + + help(); + return CPROVER_EXIT_USAGE_ERROR; +} + +int goto_synthesizer_parse_optionst::get_goto_program() +{ + log.status() << "Reading GOTO program from '" << cmdline.args[0] << "'" + << messaget::eom; + + config.set(cmdline); + + auto result = read_goto_binary(cmdline.args[0], ui_message_handler); + + if(!result.has_value()) + return CPROVER_EXIT_USAGE_ERROR; + + goto_model = std::move(result.value()); + + config.set_from_symbol_table(goto_model.symbol_table); + return CPROVER_EXIT_SUCCESS; +} + +/// display command line help +void goto_synthesizer_parse_optionst::help() +{ + // clang-format off + std::cout << '\n' << banner_string("Goto-synthesizer", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2022") << '\n' + << align_center_with_border("Qinheping Hu") << '\n' + << align_center_with_border("qinhh@amazon.com") << '\n' + << + "\n" + "Usage: Purpose:\n" + "\n" + " goto-synthesizer [-?] [-h] [--help] show help\n" + " goto-synthesizer in out synthesize and apply loop invariants.\n" // NOLINT(*) + "\n" + "Main options:\n" + "\n" + "Other options:\n" + " --version show version and exit\n" + " --xml-ui use XML-formatted output\n" + " --json-ui use JSON-formatted output\n" + " --verbosity # verbosity level\n" + "\n"; + // clang-format on +} diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.h b/src/goto-synthesizer/goto_synthesizer_parse_options.h new file mode 100644 index 00000000000..8d12624e277 --- /dev/null +++ b/src/goto-synthesizer/goto_synthesizer_parse_options.h @@ -0,0 +1,46 @@ +/*******************************************************************\ +Module: Command Line Parsing +Author: Qinheping Hu +\*******************************************************************/ + +/// \file +/// Command Line Parsing + +#ifndef CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H +#define CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H + +#include + +#include + +// clang-format off +#define GOTO_SYNTHESIZER_OPTIONS \ + "(verbosity):(version)(xml-ui)(json-ui)" \ + // empty last line + +// clang-format on + +class goto_synthesizer_parse_optionst : public parse_options_baset +{ +public: + int doit() override; + void help() override; + + goto_synthesizer_parse_optionst(int argc, const char **argv) + : parse_options_baset( + GOTO_SYNTHESIZER_OPTIONS, + argc, + argv, + "goto-synthesizer") + { + } + +protected: + void register_languages() override; + + int get_goto_program(); + + goto_modelt goto_model; +}; + +#endif // CPROVER_GOTO_SYNTHESIZER_GOTO_SYNTHESIZER_PARSE_OPTIONS_H diff --git a/src/goto-synthesizer/module_dependencies.txt b/src/goto-synthesizer/module_dependencies.txt new file mode 100644 index 00000000000..e0cd705e3c7 --- /dev/null +++ b/src/goto-synthesizer/module_dependencies.txt @@ -0,0 +1,7 @@ +ansi-c +cpp +goto-checker +goto-instrument +goto-programs +langapi +util