Add symtab2gb to enable linking of .json_symtab files

Right now we have the `goto-cc` tool to create goto binaries from C
files and link goto binaries together. This adds a similar type of
"linker" tool for the symtab language.

I had considered extending 'goto-cc' to handle symtab files as well,
however goto-cc (quite reasonably) makes some C-specific assumptions
about its input files, and I'd figured rather than working around that
it'd be easier to just have a simple command line tool to invoke
`goto_convert` and `link_goto_model` (which, in the end, is all we want
to do for json_symtabs).

CMakeLists.txt

@@ -141,6 +141,7 @@ set_target_properties(
     linking
     pointer-analysis
     solvers
+    symtab2gb
     testing-utils
     unit
     util

regression/CMakeLists.txt

@@ -52,3 +52,4 @@ add_subdirectory(contracts)
 add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
 add_subdirectory(linking-goto-binaries)
+add_subdirectory(symtab2gb)

regression/Makefile

@@ -27,6 +27,7 @@ DIRS = cbmc \
        contracts \
        goto-cc-file-local \
        linking-goto-binaries \
+       symtab2gb \
        # Empty last line
 
 # Run all test directories in sequence

regression/symtab2gb/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:symtab2gb> $<TARGET_FILE:cbmc>"
+)

regression/symtab2gb/Makefile

@@ -0,0 +1,27 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc'
+
+tests.log:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/symtab2gb/symtab2gb ../../../src/cbmc/cbmc'
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/symtab2gb/chain.sh

@@ -0,0 +1,6 @@
+#!/bin/bash
+symtab2gb_exe=$1
+cbmc_exe=$2
+
+$symtab2gb_exe "${@:3}"
+$cbmc_exe a.out

regression/symtab2gb/multiple_symtabs/README.md

@@ -0,0 +1,19 @@
+The `*.json_symtab` in this directory was created from the Ada source
+files `*.adb` using the
+[gnat2goto](https://github.com/diffblue/gnat2goto) compiler.
+
+```
+gnat2goto user.adb # produces user.json_symtab
+
+# produces library.json_symtab
+# and user.json_symtab
+# the --no-cprover-start option is to prevent
+# emitting a __CPROVER_start function for these modules,
+# as there can only be one of those in a program
+
+gnat2goto --no-cprover-start library.adb
+gnat2goto --no-cprover-start user.adb
+```
+
+Note that as of now, this requires the patch found in
+[this PR](https://github.com/diffblue/gnat2goto/pull/212)

regression/symtab2gb/multiple_symtabs/entry_point.adb

@@ -0,0 +1,7 @@
+with User;
+with Library;
+procedure Entry_Point is
+begin
+  User;
+  Library (-5);
+end Entry_Point;

regression/symtab2gb/multiple_symtabs/library.adb

@@ -0,0 +1,7 @@
+procedure Library (X : Integer) is
+begin
+  -- Failure
+  pragma Assert (X < 10);
+  -- Success
+  pragma Assert (X > 0);
+end Library;

regression/symtab2gb/multiple_symtabs/library.ads

@@ -0,0 +1 @@
+procedure Library (X : Integer);

regression/symtab2gb/multiple_symtabs/test.desc

@@ -0,0 +1,10 @@
+CORE
+entry_point.json_symtab
+user.json_symtab library.json_symtab
+^EXIT=10$
+^SIGNAL=0$
+^\[1\] file library.adb line \d+ assertion: FAILURE$
+^\[2\] file library.adb line \d+ assertion: FAILURE$
+^VERIFICATION FAILED$
+--
+error

regression/symtab2gb/multiple_symtabs/user.adb

@@ -0,0 +1,6 @@
+with Library;
+
+procedure User is
+begin
+  Library (11);
+end User;

regression/symtab2gb/multiple_symtabs/user.ads

@@ -0,0 +1 @@
+procedure User;

regression/symtab2gb/single_symtab/README.md

@@ -0,0 +1,7 @@
+The `entry_point.json_symtab` in this directory was created from the Ada source
+file `entry_point.adb` using the
+[gnat2goto](https://github.com/diffblue/gnat2goto) compiler.
+
+```
+gnat2goto entry_point.adb
+```

regression/symtab2gb/single_symtab/entry_point.adb

@@ -0,0 +1,8 @@
+procedure Entry_Point is
+  X : constant Integer := 11;
+begin
+  -- Failure
+  pragma Assert (X < 10);
+  -- Success
+  pragma Assert (X > 0);
+end Entry_Point;

regression/symtab2gb/single_symtab/test.desc

@@ -0,0 +1,10 @@
+CORE
+entry_point.json_symtab
+
+^EXIT=10$
+^SIGNAL=0$
+^\[1\] file entry_point.adb line \d+ assertion: FAILURE$
+^\[2\] file entry_point.adb line \d+ assertion: SUCCESS$
+^VERIFICATION FAILED$
+--
+error

src/CMakeLists.txt

@@ -104,3 +104,4 @@ add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)
 add_subdirectory(goto-diff)
 add_subdirectory(goto-harness)
+add_subdirectory(symtab2gb)

src/Makefile

@@ -19,6 +19,7 @@ DIRS = analyses \
        linking \
        pointer-analysis \
        solvers \
+       symtab2gb \
        util \
        xmllang \
        # Empty last line
@@ -29,6 +30,7 @@ all: cbmc.dir \
      goto-diff.dir \
      goto-instrument.dir \
      goto-harness.dir \
+     symtab2gb.dir \
      # Empty last line
 
 ###############################################################################
@@ -70,6 +72,8 @@ goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \
 
 goto-cc.dir: languages goto-programs.dir linking.dir
 
+symtab2gb.dir: util.dir goto-programs.dir json-symtab-language.dir
+
 # building for a particular directory
 
 $(patsubst %, %.dir, $(DIRS)):

src/symtab2gb/CMakeLists.txt

@@ -0,0 +1,11 @@
+add_executable(symtab2gb
+        symtab2gb_main.cpp
+        symtab2gb_parse_options.cpp
+        symtab2gb_parse_options.h)
+
+generic_includes(symtab2gb)
+
+target_link_libraries(symtab2gb
+        util
+        goto-programs
+        json-symtab-language)

src/symtab2gb/Makefile

@@ -0,0 +1,35 @@
+SRC = \
+  symtab2gb_main.cpp \
+  symtab2gb_parse_options.cpp \
+  # Empty last line
+
+OBJ += \
+  ../util/util$(LIBEXT) \
+  ../goto-programs/goto-programs$(LIBEXT) \
+  ../big-int/big-int$(LIBEXT) \
+  ../langapi/langapi$(LIBEXT) \
+  ../linking/linking$(LIBEXT) \
+  ../json/json$(LIBEXT) \
+  ../json-symtab-language/json-symtab-language$(LIBEXT) \
+  # Empty last line
+
+INCLUDES= -I ..
+
+LIBS =
+
+CLEANFILES = symtab2gb$(EXEEXT)
+
+include ../config.inc
+include ../common
+
+all: symtab2gb$(EXEEXT)
+
+###############################################################################
+
+symtab2gb$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: symtab2gb-mac-signed
+
+symtab2gb-mac-signed: symtab2gb$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) symtab2gb2$(EXEEXT)

src/symtab2gb/module_dependencies.txt

@@ -0,0 +1,3 @@
+util
+json-symtab-language
+goto-programs

src/symtab2gb/symtab2gb_main.cpp

@@ -0,0 +1,18 @@
+/******************************************************************\
+
+Module: symtab2gb_main
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+/// \file
+/// symtab2gb Main Module
+
+#include "symtab2gb_parse_options.h"
+
+int main(int argc, const char *argv[])
+{
+  symtab2gb_parse_optionst parse_options{argc, argv};
+  return parse_options.main();
+}

src/symtab2gb/symtab2gb_parse_options.cpp

@@ -0,0 +1,138 @@
+/******************************************************************\
+
+Module: symtab2gb_parse_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include "symtab2gb_parse_options.h"
+
+#include <fstream>
+#include <iostream>
+#include <string>
+
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+#include <goto-programs/link_goto_model.h>
+#include <goto-programs/write_goto_binary.h>
+#include <json-symtab-language/json_symtab_language.h>
+#include <util/exception_utils.h>
+#include <util/exit_codes.h>
+#include <util/invariant.h>
+#include <util/optional.h>
+#include <util/version.h>
+
+symtab2gb_parse_optionst::symtab2gb_parse_optionst(int argc, const char *argv[])
+  : parse_options_baset{SYMTAB2GB_OPTIONS,
+                        argc,
+                        argv,
+                        std::string("SYMTAB2GB ") + CBMC_VERSION}
+{
+}
+
+static inline bool failed(bool error_indicator)
+{
+  return error_indicator;
+}
+
+static void run_symtab2gb(
+  const std::vector<std::string> &symtab_filenames,
+  const std::string &gb_filename)
+{
+  // try opening all the files first to make sure we can
+  // even read/write what we want
+  std::ofstream out_file{gb_filename, std::ios::binary};
+  if(!out_file.is_open())
+  {
+    throw system_exceptiont{"couldn't open output file `" + gb_filename + "'"};
+  }
+  std::vector<std::ifstream> symtab_files;
+  for(auto const &symtab_filename : symtab_filenames)
+  {
+    std::ifstream symtab_file{symtab_filename};
+    if(!symtab_file.is_open())
+    {
+      throw system_exceptiont{"couldn't open input file `" + symtab_filename +
+                              "'"};
+    }
+    symtab_files.emplace_back(std::move(symtab_file));
+  }
+
+  stream_message_handlert message_handler{std::cerr};
+
+  auto const symtab_language = new_json_symtab_language();
+  symtab_language->set_message_handler(message_handler);
+
+  goto_modelt linked_goto_model{};
+
+  for(std::size_t ix = 0; ix < symtab_files.size(); ++ix)
+  {
+    auto const &symtab_filename = symtab_filenames[ix];
+    auto &symtab_file = symtab_files[ix];
+    if(failed(symtab_language->parse(symtab_file, symtab_filename)))
+    {
+      throw invalid_source_file_exceptiont{
+        "failed to parse symbol table from file `" + symtab_filename + "'"};
+    }
+    symbol_tablet symtab{};
+    if(failed(symtab_language->typecheck(symtab, "<unused>")))
+    {
+      throw invalid_source_file_exceptiont{
+        "failed to typecheck symbol table from file `" + symtab_filename + "'"};
+    }
+    goto_modelt goto_model{};
+    goto_model.symbol_table = symtab;
+    goto_convert(goto_model, message_handler);
+    link_goto_model(linked_goto_model, goto_model, message_handler);
+  }
+  if(failed(write_goto_binary(out_file, linked_goto_model)))
+  {
+    throw system_exceptiont{"failed to write goto binary to " + gb_filename};
+  }
+}
+
+int symtab2gb_parse_optionst::doit()
+{
+  if(cmdline.isset("version"))
+  {
+    log.status() << CBMC_VERSION << '\n';
+    return CPROVER_EXIT_SUCCESS;
+  }
+  if(cmdline.args.empty())
+  {
+    throw invalid_command_line_argument_exceptiont{
+      "expect at least one input file", "<json-symtab-file>"};
+  }
+  std::vector<std::string> symtab_filenames = cmdline.args;
+  std::string gb_filename = "a.out";
+  if(cmdline.isset(SYMTAB2GB_OUT_FILE_OPT))
+  {
+    gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
+  }
+  run_symtab2gb(symtab_filenames, gb_filename);
+  return CPROVER_EXIT_SUCCESS;
+}
+
+void symtab2gb_parse_optionst::help()
+{
+  log.status()
+    << '\n'
+    << banner_string("symtab2gb", CBMC_VERSION) << '\n'
+    << align_center_with_border("Copyright (C) 2019") << '\n'
+    << align_center_with_border("Diffblue Ltd.") << '\n'
+    << align_center_with_border("info@diffblue.com") << '\n'
+    << '\n'
+    << "Usage:                                   Purpose:\n"
+    << '\n'
+    << "symtab2gb [-?] [-h] [--help]             show help\n"
+       "symtab2gb                                compile .json_symtabs\n"
+       "  <json-symtab-file>+                    to a single goto-binary\n"
+       "  [--out <outfile>]\n\n"
+       "<json-symtab-file>                       a CBMC symbol table in\n"
+       "                                         JSON format\n"
+       "--out <outfile>                          specify the filename of\n"
+       "                                         the resulting binary\n"
+       "                                         (default: a.out)\n"
+    << messaget::eom;
+}

src/symtab2gb/symtab2gb_parse_options.h

@@ -0,0 +1,32 @@
+/******************************************************************\
+
+Module: symtab2gb_parse_options
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#ifndef CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H
+#define CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H
+
+#include <util/parse_options.h>
+
+#define SYMTAB2GB_OUT_FILE_OPT "out"
+
+// clang-format off
+
+#define SYMTAB2GB_OPTIONS                                                      \
+  "(" SYMTAB2GB_OUT_FILE_OPT "):"                                              \
+// end options
+
+// clang-format on
+
+class symtab2gb_parse_optionst : public parse_options_baset
+{
+public:
+  symtab2gb_parse_optionst(int argc, const char *argv[]);
+  void help() override;
+  int doit() override;
+};
+
+#endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H