Merge in feature branch that adds gnat2goto compatibility

CMakeLists.txt

@@ -66,6 +66,7 @@ set_target_properties(
     goto-symex
     jsil
     json
+    json-symtab-language
     langapi
     linking
     pointer-analysis

jbmc/unit/CMakeLists.txt

@@ -26,6 +26,7 @@ target_link_libraries(java-unit
         goto-programs
         goto-instrument-lib
         cbmc-lib
+        json-symtab-language
 )
 
 add_test(

jbmc/unit/Makefile

@@ -108,6 +108,7 @@ CPROVER_LIBS =../src/java_bytecode/java_bytecode$(LIBEXT) \
               $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
               $(CPROVER_DIR)/src/cpp/cpp$(LIBEXT) \
               $(CPROVER_DIR)/src/json/json$(LIBEXT) \
+              $(CPROVER_DIR)/src/json-symtab-language/json-symtab-language$(LIBEXT) \
               $(CPROVER_DIR)/src/linking/linking$(LIBEXT) \
               $(CPROVER_DIR)/src/util/util$(LIBEXT) \
               $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \

src/CMakeLists.txt

@@ -89,6 +89,7 @@ add_subdirectory(goto-programs)
 add_subdirectory(goto-symex)
 add_subdirectory(jsil)
 add_subdirectory(json)
+add_subdirectory(json-symtab-language)
 add_subdirectory(langapi)
 add_subdirectory(linking)
 add_subdirectory(pointer-analysis)

src/Makefile

@@ -12,6 +12,7 @@ DIRS = analyses \
        goto-symex \
        jsil \
        json \
+       json-symtab-language \
        langapi \
        linking \
        pointer-analysis \
@@ -41,7 +42,7 @@ cpp.dir: ansi-c.dir linking.dir
 
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
-           jsil.dir
+           jsil.dir json-symtab-language.dir
 
 solvers.dir: util.dir langapi.dir
 

src/cbmc/CMakeLists.txt

@@ -17,6 +17,7 @@ target_link_libraries(cbmc-lib
     goto-programs
     goto-symex
     json
+    json-symtab-language
     langapi
     linking
     pointer-analysis

src/cbmc/Makefile

@@ -14,6 +14,8 @@ SRC = all_properties.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
+      ../json/json$(LIBEXT) \
+      ../json-symtab-language/json-symtab-language$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \

src/cbmc/cbmc_languages.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
+#include <json-symtab-language/json_symtab_language.h>
 
 #ifdef HAVE_JSIL
 #include <jsil/jsil_language.h>
@@ -24,8 +25,9 @@ void cbmc_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);
+  register_language(new_json_symtab_language);
 
-  #ifdef HAVE_JSIL
+#ifdef HAVE_JSIL
   register_language(new_jsil_language);
-  #endif
+#endif
 }

src/cbmc/module_dependencies.txt

@@ -5,6 +5,7 @@ goto-instrument
 goto-programs
 goto-symex
 jsil
+json-symtab-language
 langapi # should go away
 linking
 pointer-analysis

src/json-symtab-language/CMakeLists.txt

@@ -0,0 +1,6 @@
+file(GLOB_RECURSE sources "*.cpp" "*.h")
+add_library(json-symtab-language ${sources})
+
+generic_includes(json-symtab-language)
+
+target_link_libraries(json-symtab-language json util)

src/json-symtab-language/Makefile

@@ -0,0 +1,17 @@
+SRC = json_symtab_language.cpp \
+	json_symbol_table.cpp \
+	json_symbol.cpp 
+
+INCLUDES= -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = json-symtab-language$(LIBEXT)
+
+all: json-symtab-language$(LIBEXT)
+
+###############################################################################
+
+json-symtab-language$(LIBEXT): $(OBJ)
+	$(LINKLIB)

src/json-symtab-language/json_symbol.cpp

@@ -0,0 +1,116 @@
+/*******************************************************************\
+
+Module: JSON symbol deserialization
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#include "json_symbol.h"
+
+#include <util/exception_utils.h>
+#include <util/expr.h>
+#include <util/json_irep.h>
+#include <util/source_location.h>
+#include <util/type.h>
+
+/// Return string value for a given key if present in the json object.
+/// \param in: The json object that is getting fetched as a string.
+/// \param key: The key for the json value to be fetched.
+/// \return: A string value for the corresponding key.
+static const std::string &
+try_get_string(const jsont &in, const std::string &key)
+{
+  if(!in.is_string())
+    throw deserialization_exceptiont(
+      "symbol_from_json: expected string for key '" + key + "'");
+  return in.value;
+}
+
+/// Return boolean value for a given key if present in the json object.
+/// \param in: The json object that is getting fetched as a boolean.
+/// \param key: The key for the json value to be fetched.
+/// \return: A boolean value for the corresponding key.
+static bool try_get_bool(const jsont &in, const std::string &key)
+{
+  if(!(in.is_true() || in.is_false()))
+    throw deserialization_exceptiont(
+      "symbol_from_json: expected bool for key '" + key + "'");
+  return in.is_true();
+}
+
+/// Deserialise a json object to a symbolt.
+/// \param in: The json object that is getting fetched as an object.
+/// \return: A symbolt representing the json object.
+symbolt symbol_from_json(const jsont &in)
+{
+  if(!in.is_object())
+    throw deserialization_exceptiont("symbol_from_json takes an object");
+  symbolt result;
+  json_irept json2irep(true);
+  for(const auto &kv : in.object)
+  {
+    if(kv.first == "type")
+    {
+      irept irep = json2irep.convert_from_json(kv.second);
+      result.type = static_cast<typet &>(irep);
+    }
+    else if(kv.first == "value")
+    {
+      irept irep = json2irep.convert_from_json(kv.second);
+      result.value = static_cast<exprt &>(irep);
+    }
+    else if(kv.first == "location")
+    {
+      irept irep = json2irep.convert_from_json(kv.second);
+      result.location = static_cast<source_locationt &>(irep);
+    }
+    else if(kv.first == "name")
+      result.name = try_get_string(kv.second, "name");
+    else if(kv.first == "module")
+      result.module = try_get_string(kv.second, "module");
+    else if(kv.first == "base_name")
+      result.base_name = try_get_string(kv.second, "base_name");
+    else if(kv.first == "mode")
+      result.mode = try_get_string(kv.second, "mode");
+    else if(kv.first == "pretty_name")
+      result.pretty_name = try_get_string(kv.second, "pretty_name");
+    else if(kv.first == "is_type")
+      result.is_type = try_get_bool(kv.second, "is_type");
+    else if(kv.first == "is_macro")
+      result.is_macro = try_get_bool(kv.second, "is_macro");
+    else if(kv.first == "is_exported")
+      result.is_exported = try_get_bool(kv.second, "is_exported");
+    else if(kv.first == "is_input")
+      result.is_input = try_get_bool(kv.second, "is_input");
+    else if(kv.first == "is_output")
+      result.is_output = try_get_bool(kv.second, "is_output");
+    else if(kv.first == "is_state_var")
+      result.is_state_var = try_get_bool(kv.second, "is_state_var");
+    else if(kv.first == "is_property")
+      result.is_property = try_get_bool(kv.second, "is_property");
+    else if(kv.first == "is_static_lifetime")
+      result.is_static_lifetime = try_get_bool(kv.second, "is_static_lifetime");
+    else if(kv.first == "is_thread_local")
+      result.is_thread_local = try_get_bool(kv.second, "is_thread_local");
+    else if(kv.first == "is_lvalue")
+      result.is_lvalue = try_get_bool(kv.second, "is_lvalue");
+    else if(kv.first == "is_file_local")
+      result.is_file_local = try_get_bool(kv.second, "is_file_local");
+    else if(kv.first == "is_extern")
+      result.is_extern = try_get_bool(kv.second, "is_extern");
+    else if(kv.first == "is_volatile")
+      result.is_volatile = try_get_bool(kv.second, "is_volatile");
+    else if(kv.first == "is_parameter")
+      result.is_parameter = try_get_bool(kv.second, "is_parameter");
+    else if(kv.first == "is_auxiliary")
+      result.is_auxiliary = try_get_bool(kv.second, "is_auxiliary");
+    else if(kv.first == "is_weak")
+      result.is_weak = try_get_bool(kv.second, "is_weak");
+    else
+      throw deserialization_exceptiont(
+        "symbol_from_json: unexpected key '" + kv.first + "'");
+  }
+
+  return result;
+}

src/json-symtab-language/json_symbol.h

@@ -0,0 +1,17 @@
+/*******************************************************************\
+
+Module: JSON symbol deserialization
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H
+#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H
+
+#include <util/json.h>
+#include <util/symbol.h>
+
+symbolt symbol_from_json(const jsont &);
+
+#endif

src/json-symtab-language/json_symbol_table.cpp

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: JSON symbol table deserialization
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#include "json_symbol_table.h"
+#include "json_symbol.h"
+
+#include <util/exception_utils.h>
+#include <util/json.h>
+#include <util/symbol_table.h>
+
+void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
+{
+  if(!in.is_array())
+    throw deserialization_exceptiont(
+      "symbol_table_from_json: JSON input must be an array");
+  for(const auto &js_symbol : in.array)
+  {
+    symbolt deserialized = symbol_from_json(js_symbol);
+    if(symbol_table.add(deserialized))
+      throw deserialization_exceptiont(
+        "symbol_table_from_json: duplicate symbol name '" +
+        id2string(deserialized.name) + "'");
+  }
+}

src/json-symtab-language/json_symbol_table.h

@@ -0,0 +1,17 @@
+/*******************************************************************\
+
+Module: JSON symbol table deserialization
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_TABLE_H
+#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_TABLE_H
+
+class jsont;
+class symbol_tablet;
+
+void symbol_table_from_json(const jsont &, symbol_tablet &);
+
+#endif

src/json-symtab-language/json_symtab_language.cpp

@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+Module: JSON symbol table language. Accepts a JSON format symbol
+        table that has been produced out-of-process, e.g. by using
+        a compiler's front-end.
+
+Author: Chris Smowton, [email protected]
+
+\*******************************************************************/
+
+#include "json_symtab_language.h"
+#include "json_symbol_table.h"
+#include <json/json_parser.h>
+#include <util/namespace.h>
+
+/// Parse a goto program in json form.
+/// \param instream: The input stream
+/// \param path: A file path
+/// \return: boolean signifying success or failure of the parsing
+bool json_symtab_languaget::parse(
+  std::istream &instream,
+  const std::string &path)
+{
+  return parse_json(instream, path, get_message_handler(), parsed_json_file);
+}
+
+/// Typecheck a goto program in json form.
+/// \param symbol_table: The symbol table containing symbols read from file.
+/// \param module: A useless parameter, there for interface consistency.
+/// \return: boolean signifying success or failure of the typechecking.
+bool json_symtab_languaget::typecheck(
+  symbol_tablet &symbol_table,
+  const std::string &module)
+{
+  try
+  {
+    symbol_table_from_json(parsed_json_file, symbol_table);
+    return false;
+  }
+  catch(const std::string &str)
+  {
+    error() << "typecheck: " << str << eom;
+    return true;
+  }
+}
+
+/// Output the result of the parsed json file to the output stream
+/// passed as a parameter to this function.
+/// \param out: The stream to use to output the parsed_json_file.
+void json_symtab_languaget::show_parse(std::ostream &out)
+{
+  parsed_json_file.output(out);
+}