From 86e8356565731207c8aef6c4d506176f11b4b5f3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 23 Feb 2017 18:39:14 +0000 Subject: [PATCH] Implement JSON symtab language frontend. Implement JSON symtab language, a new, more generic language frontend, able to read GOTO programs in JSON form, from any frontend that generates them. Currently this stands as the support frontend for our ADA conversion tool, GNAT2GOTO. --- CMakeLists.txt | 1 + jbmc/unit/CMakeLists.txt | 1 + jbmc/unit/Makefile | 1 + src/CMakeLists.txt | 1 + src/Makefile | 3 +- src/cbmc/CMakeLists.txt | 1 + src/cbmc/Makefile | 2 + src/cbmc/cbmc_languages.cpp | 6 +- src/cbmc/module_dependencies.txt | 1 + src/json-symtab-language/CMakeLists.txt | 6 + src/json-symtab-language/Makefile | 17 +++ src/json-symtab-language/json_symbol.cpp | 116 ++++++++++++++++++ src/json-symtab-language/json_symbol.h | 17 +++ .../json_symbol_table.cpp | 29 +++++ src/json-symtab-language/json_symbol_table.h | 17 +++ .../json_symtab_language.cpp | 53 ++++++++ .../json_symtab_language.h | 71 +++++++++++ .../module_dependencies.txt | 4 + unit/CMakeLists.txt | 1 + unit/Makefile | 1 + 20 files changed, 346 insertions(+), 3 deletions(-) create mode 100644 src/json-symtab-language/CMakeLists.txt create mode 100644 src/json-symtab-language/Makefile create mode 100644 src/json-symtab-language/json_symbol.cpp create mode 100644 src/json-symtab-language/json_symbol.h create mode 100644 src/json-symtab-language/json_symbol_table.cpp create mode 100644 src/json-symtab-language/json_symbol_table.h create mode 100644 src/json-symtab-language/json_symtab_language.cpp create mode 100644 src/json-symtab-language/json_symtab_language.h create mode 100644 src/json-symtab-language/module_dependencies.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 0c32e421f01..f10bf4ecf60 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -66,6 +66,7 @@ set_target_properties( goto-symex jsil json + json-symtab-language langapi linking pointer-analysis diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt index 0aaead7c9ed..75758675097 100644 --- a/jbmc/unit/CMakeLists.txt +++ b/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( diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 917e57d4fb5..77a13690282 100644 --- a/jbmc/unit/Makefile +++ b/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) \ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4022889e456..e38c855b6be 100644 --- a/src/CMakeLists.txt +++ b/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) diff --git a/src/Makefile b/src/Makefile index 020da636c97..604a22176fa 100644 --- a/src/Makefile +++ b/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 diff --git a/src/cbmc/CMakeLists.txt b/src/cbmc/CMakeLists.txt index b1cae0f8b01..967d5db430e 100644 --- a/src/cbmc/CMakeLists.txt +++ b/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 diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 85bf81e17fe..962bc1b7995 100644 --- a/src/cbmc/Makefile +++ b/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) \ diff --git a/src/cbmc/cbmc_languages.cpp b/src/cbmc/cbmc_languages.cpp index 55cc8cda97d..7d336f7defb 100644 --- a/src/cbmc/cbmc_languages.cpp +++ b/src/cbmc/cbmc_languages.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #ifdef HAVE_JSIL #include @@ -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 } diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt index 57d634ccfd7..ce595ebba96 100644 --- a/src/cbmc/module_dependencies.txt +++ b/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 diff --git a/src/json-symtab-language/CMakeLists.txt b/src/json-symtab-language/CMakeLists.txt new file mode 100644 index 00000000000..f297392dcc2 --- /dev/null +++ b/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) diff --git a/src/json-symtab-language/Makefile b/src/json-symtab-language/Makefile new file mode 100644 index 00000000000..3fb674732cf --- /dev/null +++ b/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) diff --git a/src/json-symtab-language/json_symbol.cpp b/src/json-symtab-language/json_symbol.cpp new file mode 100644 index 00000000000..ab470793d84 --- /dev/null +++ b/src/json-symtab-language/json_symbol.cpp @@ -0,0 +1,116 @@ +/*******************************************************************\ + +Module: JSON symbol deserialization + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include "json_symbol.h" + +#include +#include +#include +#include +#include + +/// 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(irep); + } + else if(kv.first == "value") + { + irept irep = json2irep.convert_from_json(kv.second); + result.value = static_cast(irep); + } + else if(kv.first == "location") + { + irept irep = json2irep.convert_from_json(kv.second); + result.location = static_cast(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; +} diff --git a/src/json-symtab-language/json_symbol.h b/src/json-symtab-language/json_symbol.h new file mode 100644 index 00000000000..63fa22f0438 --- /dev/null +++ b/src/json-symtab-language/json_symbol.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +Module: JSON symbol deserialization + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H +#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMBOL_H + +#include +#include + +symbolt symbol_from_json(const jsont &); + +#endif diff --git a/src/json-symtab-language/json_symbol_table.cpp b/src/json-symtab-language/json_symbol_table.cpp new file mode 100644 index 00000000000..efe150078f3 --- /dev/null +++ b/src/json-symtab-language/json_symbol_table.cpp @@ -0,0 +1,29 @@ +/*******************************************************************\ + +Module: JSON symbol table deserialization + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include "json_symbol_table.h" +#include "json_symbol.h" + +#include +#include +#include + +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) + "'"); + } +} diff --git a/src/json-symtab-language/json_symbol_table.h b/src/json-symtab-language/json_symbol_table.h new file mode 100644 index 00000000000..42e14a3ef54 --- /dev/null +++ b/src/json-symtab-language/json_symbol_table.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +Module: JSON symbol table deserialization + +Author: Chris Smowton, chris.smowton@diffblue.com + +\*******************************************************************/ + +#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 diff --git a/src/json-symtab-language/json_symtab_language.cpp b/src/json-symtab-language/json_symtab_language.cpp new file mode 100644 index 00000000000..8c9d9024b88 --- /dev/null +++ b/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, chris.smowton@diffblue.com + +\*******************************************************************/ + +#include "json_symtab_language.h" +#include "json_symbol_table.h" +#include +#include + +/// 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); +} diff --git a/src/json-symtab-language/json_symtab_language.h b/src/json-symtab-language/json_symtab_language.h new file mode 100644 index 00000000000..714b8487e6b --- /dev/null +++ b/src/json-symtab-language/json_symtab_language.h @@ -0,0 +1,71 @@ +/*******************************************************************\ + +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, chris.smowton@diffblue.com + +\*******************************************************************/ + +#ifndef CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H +#define CPROVER_JSON_SYMTAB_LANGUAGE_JSON_SYMTAB_LANGUAGE_H + +#include +#include + +#include +#include +#include +#include + +class json_symtab_languaget : public languaget +{ +public: + bool parse(std::istream &instream, const std::string &path) override; + + bool + typecheck(symbol_tablet &symbol_table, const std::string &module) override; + + void show_parse(std::ostream &out) override; + + bool to_expr( + const std::string &code, + const std::string &module, + exprt &expr, + const namespacet &ns) override + { + UNIMPLEMENTED; + } + + std::set extensions() const override + { + return {"json_symtab"}; + } + + std::unique_ptr new_language() override + { + return util_make_unique(); + } + + bool generate_support_functions(symbol_tablet &symbol_table) override + { + // check if entry point is already there + bool entry_point_exists = + symbol_table.symbols.find(goto_functionst::entry_point()) != + symbol_table.symbols.end(); + return !entry_point_exists; + } + + ~json_symtab_languaget() override = default; + +protected: + jsont parsed_json_file; +}; + +inline std::unique_ptr new_json_symtab_language() +{ + return util_make_unique(); +} + +#endif diff --git a/src/json-symtab-language/module_dependencies.txt b/src/json-symtab-language/module_dependencies.txt new file mode 100644 index 00000000000..b4db43a0dd0 --- /dev/null +++ b/src/json-symtab-language/module_dependencies.txt @@ -0,0 +1,4 @@ +goto-programs +json +langapi +util diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 6c06a0fc205..013a3dc01d3 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -37,6 +37,7 @@ target_link_libraries( goto-programs goto-instrument-lib cbmc-lib + json-symtab-language ) add_test( diff --git a/unit/Makefile b/unit/Makefile index 461f651c6dc..c699ce04eb0 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -104,6 +104,7 @@ BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ ../src/cpp/cpp$(LIBEXT) \ ../src/json/json$(LIBEXT) \ + ../src/json-symtab-language/json-symtab-language$(LIBEXT) \ ../src/linking/linking$(LIBEXT) \ ../src/util/util$(LIBEXT) \ ../src/big-int/big-int$(LIBEXT) \