diff --git a/CMakeLists.txt b/CMakeLists.txt index 281c306b7ee..71680800940 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -154,6 +154,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR "$" "$" "$" + "$" "$" "$" "$" @@ -221,6 +222,8 @@ cprover_default_properties( goto-analyzer-lib goto-cc goto-cc-lib + goto-contracts + goto-contracts-lib goto-checker goto-diff goto-diff-lib diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1578ca05d4f..7afce9cd69b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -108,6 +108,7 @@ add_subdirectory(util) add_subdirectory(cbmc) add_subdirectory(crangler) add_subdirectory(goto-cc) +add_subdirectory(goto-contracts) add_subdirectory(goto-instrument) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) diff --git a/src/Makefile b/src/Makefile index 86d03ffbe90..0ae3bf7706f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -7,6 +7,7 @@ DIRS = analyses \ crangler \ goto-analyzer \ goto-cc \ + goto-contracts \ goto-checker \ goto-diff \ goto-instrument \ @@ -31,6 +32,7 @@ all: cbmc.dir \ crangler.dir \ goto-analyzer.dir \ goto-cc.dir \ + goto-contracts.dir \ goto-diff.dir \ goto-instrument.dir \ goto-harness.dir \ @@ -63,6 +65,10 @@ cpp.dir: ansi-c.dir linking.dir crangler.dir: util.dir json.dir +goto-contracts.dir: util.dir goto-programs.dir langapi.dir \ + json.dir \ + goto-instrument.dir + languages: util.dir langapi.dir \ cpp.dir ansi-c.dir xmllang.dir assembler.dir \ jsil.dir json.dir json-symtab-language.dir statement-list.dir diff --git a/src/goto-contracts/CMakeLists.txt b/src/goto-contracts/CMakeLists.txt new file mode 100644 index 00000000000..58d76133320 --- /dev/null +++ b/src/goto-contracts/CMakeLists.txt @@ -0,0 +1,23 @@ +# Library +file(GLOB_RECURSE sources "*.cpp" "*.h") +list(REMOVE_ITEM sources + ${CMAKE_CURRENT_SOURCE_DIR}/goto_contracts_main.cpp +) +add_library(goto-contracts-lib ${sources}) + +generic_includes(goto-contracts-lib) + +target_link_libraries(goto-contracts-lib + ansi-c + cpp + big-int + goto-programs + langapi + util + json +) + +# Executable +add_executable(goto-contracts goto_contracts_main.cpp) +target_link_libraries(goto-contracts goto-contracts-lib) +install(TARGETS goto-contracts DESTINATION ${CMAKE_INSTALL_BINDIR}) diff --git a/src/goto-contracts/Makefile b/src/goto-contracts/Makefile new file mode 100644 index 00000000000..c4080d77ae2 --- /dev/null +++ b/src/goto-contracts/Makefile @@ -0,0 +1,34 @@ +SRC = goto_contracts_languages.cpp \ + goto_contracts_main.cpp \ + goto_contracts_parse_options.cpp \ + # Empty last line + +OBJ += ../ansi-c/ansi-c$(LIBEXT) \ + ../cpp/cpp$(LIBEXT) \ + ../big-int/big-int$(LIBEXT) \ + ../goto-programs/goto-programs$(LIBEXT) \ + ../langapi/langapi$(LIBEXT) \ + ../util/util$(LIBEXT) \ + ../json/json$(LIBEXT) \ + # Empty last line + +INCLUDES= -I .. + +LIBS = + +CLEANFILES = goto-contracts$(EXEEXT) goto-contracts$(LIBEXT) + +include ../config.inc +include ../common + +all: goto-contracts$(EXEEXT) + +############################################################################### + +goto-contracts$(EXEEXT): $(OBJ) + $(LINKBIN) + +.PHONY: goto-contracts-mac-signed + +goto-contracts-mac-signed: goto-contracts$(EXEEXT) + codesign -v -s $(OSX_IDENTITY) goto-contracts$(EXEEXT) diff --git a/src/goto-contracts/README.md b/src/goto-contracts/README.md new file mode 100644 index 00000000000..6a931162ddf --- /dev/null +++ b/src/goto-contracts/README.md @@ -0,0 +1,9 @@ +\ingroup module_hidden +\defgroup goto-contracts goto-contracts + +# Folder goto-contracts + +\author Michael Tautschnig + +The `goto-contracts/` contains all processing of function contracts and loop +invariants. diff --git a/src/goto-contracts/goto_contracts_languages.cpp b/src/goto-contracts/goto_contracts_languages.cpp new file mode 100644 index 00000000000..55e727fdd38 --- /dev/null +++ b/src/goto-contracts/goto_contracts_languages.cpp @@ -0,0 +1,23 @@ +/*******************************************************************\ + +Module: Language Registration + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Language Registration + +#include "goto_contracts_parse_options.h" + +#include + +#include +#include + +void goto_contracts_parse_optionst::register_languages() +{ + register_language(new_ansi_c_language); + register_language(new_cpp_language); +} diff --git a/src/goto-contracts/goto_contracts_main.cpp b/src/goto-contracts/goto_contracts_main.cpp new file mode 100644 index 00000000000..4c112e117d6 --- /dev/null +++ b/src/goto-contracts/goto_contracts_main.cpp @@ -0,0 +1,30 @@ +/*******************************************************************\ + +Module: Main Module + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Main Module + +#ifdef _MSC_VER +# include +#endif + +#include "goto_contracts_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_contracts_parse_optionst parse_options(argc, argv); + return parse_options.main(); +} diff --git a/src/goto-contracts/goto_contracts_parse_options.cpp b/src/goto-contracts/goto_contracts_parse_options.cpp new file mode 100644 index 00000000000..b43bc1a8c18 --- /dev/null +++ b/src/goto-contracts/goto_contracts_parse_options.cpp @@ -0,0 +1,105 @@ +/*******************************************************************\ + +Module: Main Module + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Main Module + +#include "goto_contracts_parse_options.h" + +#include +#include +#include + +#include + +#include + +/// invoke main modules +int goto_contracts_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(); + + get_goto_program(); + + // TODO + // read contracts from file, using Crangler's syntax + // ASSUME no recursion, function pointers, setjmp/longjmp + // create a queue of goto models + // for each element in the queue: + // reachability slice + // remove unused functions + // slice global init + // compute call graph + // walk call graph bottom-up + // if a function contract exists: + // copy goto model, mark function as top-level function + // compute assigns set, possibly doing inlining first + // replace all calls to this function by contract + // TODO: loops, dependencies, Makefile, generate contracts stubs, + // precondition, postcondition + + help(); + return CPROVER_EXIT_USAGE_ERROR; +} + +void goto_contracts_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()) + throw 0; + + goto_model = std::move(result.value()); + + config.set_from_symbol_table(goto_model.symbol_table); +} + +/// display command line help +void goto_contracts_parse_optionst::help() +{ + // clang-format off + std::cout << '\n' << banner_string("Goto-contracts", CBMC_VERSION) << '\n' + << align_center_with_border("Copyright (C) 2021") << '\n' + << align_center_with_border("Michael Tautschnig") << '\n' + << align_center_with_border("tautschn@amazon.com") << '\n' + << + "\n" + "Usage: Purpose:\n" + "\n" + " goto-contracts [-?] [-h] [--help] show help\n" + " goto-contracts in out apply contracts\n" + "\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" + "\n"; + // clang-format on +} diff --git a/src/goto-contracts/goto_contracts_parse_options.h b/src/goto-contracts/goto_contracts_parse_options.h new file mode 100644 index 00000000000..e1eecba9163 --- /dev/null +++ b/src/goto-contracts/goto_contracts_parse_options.h @@ -0,0 +1,45 @@ +/*******************************************************************\ + +Module: Command Line Parsing + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Command Line Parsing + +#ifndef CPROVER_GOTO_CONTRACTS_GOTO_CONTRACTS_PARSE_OPTIONS_H +#define CPROVER_GOTO_CONTRACTS_GOTO_CONTRACTS_PARSE_OPTIONS_H + +#include + +#include + +// clang-format off +#define GOTO_CONTRACTS_OPTIONS \ + "(verbosity):(version)(xml-ui)(json-ui)" \ + // empty last line + +// clang-format on + +class goto_contracts_parse_optionst : public parse_options_baset +{ +public: + int doit() override; + void help() override; + + goto_contracts_parse_optionst(int argc, const char **argv) + : parse_options_baset(GOTO_CONTRACTS_OPTIONS, argc, argv, "goto-contracts") + { + } + +protected: + void register_languages() override; + + void get_goto_program(); + + goto_modelt goto_model; +}; + +#endif // CPROVER_GOTO_CONTRACTS_GOTO_CONTRACTS_PARSE_OPTIONS_H diff --git a/src/goto-contracts/module_dependencies.txt b/src/goto-contracts/module_dependencies.txt new file mode 100644 index 00000000000..379ff6a35ad --- /dev/null +++ b/src/goto-contracts/module_dependencies.txt @@ -0,0 +1,3 @@ +goto-instrument +goto-programs +util