goto-synthesizer: Separate front-end for loop-contracts synthesizer

CMakeLists.txt

@@ -157,6 +157,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:goto-cc>"
               "$<TARGET_FILE:goto-diff>"
               "$<TARGET_FILE:goto-instrument>"
+              "$<TARGET_FILE:goto-synthesizer>"
               "$<TARGET_FILE:janalyzer>"
               "$<TARGET_FILE:jbmc>"
               "$<TARGET_FILE:jdiff>"
@@ -233,6 +234,8 @@ cprover_default_properties(
     goto-instrument-lib
     goto-programs
     goto-symex
+    goto-synthesizer
+    goto-synthesizer-lib
     jsil
     json
     json-symtab-language

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

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

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)

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/ ; \

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

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)

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.

src/goto-synthesizer/goto_synthesizer_languages.cpp

@@ -0,0 +1,19 @@
+/*******************************************************************\
+Module: Language Registration
+Author: Qinheping Hu
+\*******************************************************************/
+
+/// \file
+/// Language Registration
+
+#include <ansi-c/ansi_c_language.h>
+#include <cpp/cpp_language.h>
+#include <langapi/mode.h>
+
+#include "goto_synthesizer_parse_options.h"
+
+void goto_synthesizer_parse_optionst::register_languages()
+{
+  register_language(new_ansi_c_language);
+  register_language(new_cpp_language);
+}

src/goto-synthesizer/goto_synthesizer_main.cpp

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

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 <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_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("[email protected]") << '\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
+}

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

src/goto-synthesizer/module_dependencies.txt

@@ -0,0 +1,7 @@
+ansi-c
+cpp
+goto-checker
+goto-instrument
+goto-programs
+langapi
+util