goto-contracts: Separate front-end for contracts

CMakeLists.txt

@@ -154,6 +154,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:driver>"
               "$<TARGET_FILE:goto-analyzer>"
               "$<TARGET_FILE:goto-cc>"
+              "$<TARGET_FILE:goto-contracts>"
               "$<TARGET_FILE:goto-diff>"
               "$<TARGET_FILE:goto-instrument>"
               "$<TARGET_FILE:janalyzer>"
@@ -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

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)

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

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})

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)

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.

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 <langapi/mode.h>
+
+#include <ansi-c/ansi_c_language.h>
+#include <cpp/cpp_language.h>
+
+void goto_contracts_parse_optionst::register_languages()
+{
+  register_language(new_ansi_c_language);
+  register_language(new_cpp_language);
+}

src/goto-contracts/goto_contracts_main.cpp

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Main Module
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Main Module
+
+#ifdef _MSC_VER
+#  include <util/unicode.h>
+#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();
+}

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 <util/config.h>
+#include <util/exit_codes.h>
+#include <util/version.h>
+
+#include <goto-programs/read_goto_binary.h>
+
+#include <iostream>
+
+/// 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("[email protected]") << '\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
+}

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 <util/parse_options.h>
+
+#include <goto-programs/goto_model.h>
+
+// 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

src/goto-contracts/module_dependencies.txt

@@ -0,0 +1,3 @@
+goto-instrument
+goto-programs
+util