From 3614bdce2bbbda87af38640ab7a0e124b6b63cca Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 8 Jan 2019 15:50:31 +0000 Subject: [PATCH 1/3] Make symbol table JSON output and input consistent This adapts the JSON symbol table output function show_symbol_table_json_ui() and the JSON symbol table input function symbol_table_from_json() to use a consistent format. --- src/goto-programs/show_symbol_table.cpp | 1 + src/json-symtab-language/json_symbol.cpp | 78 ++++++++++--------- .../json_symbol_table.cpp | 37 +++++++-- src/util/json_irep.cpp | 48 ++++++++---- 4 files changed, 105 insertions(+), 59 deletions(-) diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 73c8cf2c075..e64eb0b3ab5 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -196,6 +196,7 @@ static void show_symbol_table_json_ui( json_objectt symbol_json( {{"prettyName", json_stringt(symbol.pretty_name)}, + {"name", json_stringt(symbol.name)}, {"baseName", json_stringt(symbol.base_name)}, {"mode", json_stringt(symbol.mode)}, {"module", json_stringt(symbol.module)}, diff --git a/src/json-symtab-language/json_symbol.cpp b/src/json-symtab-language/json_symbol.cpp index 97ba071ec3f..cd6b0d79bee 100644 --- a/src/json-symtab-language/json_symbol.cpp +++ b/src/json-symtab-language/json_symbol.cpp @@ -69,44 +69,50 @@ symbolt symbol_from_json(const jsont &in) 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 == "baseName") + result.base_name = try_get_string(kv.second, "baseName"); 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 if(kv.first == "prettyName") + result.pretty_name = try_get_string(kv.second, "prettyName"); + else if(kv.first == "isType") + result.is_type = try_get_bool(kv.second, "isType"); + else if(kv.first == "isMacro") + result.is_macro = try_get_bool(kv.second, "isMacro"); + else if(kv.first == "isExported") + result.is_exported = try_get_bool(kv.second, "isExported"); + else if(kv.first == "isInput") + result.is_input = try_get_bool(kv.second, "isInput"); + else if(kv.first == "isOutput") + result.is_output = try_get_bool(kv.second, "isOutput"); + else if(kv.first == "isStateVar") + result.is_state_var = try_get_bool(kv.second, "isStateVar"); + else if(kv.first == "isProperty") + result.is_property = try_get_bool(kv.second, "isProperty"); + else if(kv.first == "isStaticLifetime") + result.is_static_lifetime = try_get_bool(kv.second, "isStaticLifetime"); + else if(kv.first == "isThreadLocal") + result.is_thread_local = try_get_bool(kv.second, "isThreadLocal"); + else if(kv.first == "isLvalue") + result.is_lvalue = try_get_bool(kv.second, "isLvalue"); + else if(kv.first == "isFileLocal") + result.is_file_local = try_get_bool(kv.second, "isFileLocal"); + else if(kv.first == "isExtern") + result.is_extern = try_get_bool(kv.second, "isExtern"); + else if(kv.first == "isVolatile") + result.is_volatile = try_get_bool(kv.second, "isVolatile"); + else if(kv.first == "isParameter") + result.is_parameter = try_get_bool(kv.second, "isParameter"); + else if(kv.first == "isAuxiliary") + result.is_auxiliary = try_get_bool(kv.second, "isAuxiliary"); + else if(kv.first == "isWeak") + result.is_weak = try_get_bool(kv.second, "isWeak"); + else if(kv.first == "prettyType") + { + } // ignore + else if(kv.first == "prettyValue") + { + } // ignore else throw deserialization_exceptiont( "symbol_from_json: unexpected key '" + kv.first + "'"); diff --git a/src/json-symtab-language/json_symbol_table.cpp b/src/json-symtab-language/json_symbol_table.cpp index 94033299c7c..6d835c76d34 100644 --- a/src/json-symtab-language/json_symbol_table.cpp +++ b/src/json-symtab-language/json_symbol_table.cpp @@ -15,15 +15,38 @@ Author: Chris Smowton, chris.smowton@diffblue.com void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table) { - if(!in.is_array()) + if(!in.is_object()) + { + throw deserialization_exceptiont( + "symbol_table_from_json: JSON input must be an object"); + } + + const json_objectt &json_object = to_json_object(in); + const auto it = json_object.find("symbolTable"); + + if(it == json_object.end()) + { throw deserialization_exceptiont( - "symbol_table_from_json: JSON input must be an array"); - for(const auto &js_symbol : to_json_array(in)) + "symbol_table_from_json: JSON object must have key `symbolTable`"); + } + + if(!it->second.is_object()) { - symbolt deserialized = symbol_from_json(js_symbol); - if(symbol_table.add(deserialized)) + throw deserialization_exceptiont( + "symbol_table_from_json: JSON symbol table must be an object"); + } + + const json_objectt &json_symbol_table = to_json_object(it->second); + + for(const auto &pair : json_symbol_table) + { + const jsont &json_symbol = pair.second; + + symbolt symbol = symbol_from_json(json_symbol); + + if(symbol_table.add(symbol)) throw deserialization_exceptiont( - "symbol_table_from_json: duplicate symbol name '" + - id2string(deserialized.name) + "'"); + "symbol_table_from_json: duplicate symbol name `" + + id2string(symbol.name) + "`"); } } diff --git a/src/util/json_irep.cpp b/src/util/json_irep.cpp index 57b97258d3d..8433bf84c5a 100644 --- a/src/util/json_irep.cpp +++ b/src/util/json_irep.cpp @@ -34,8 +34,7 @@ json_objectt json_irept::convert_from_irep(const irept &irep) const { json_objectt irep_object; - if(irep.id()!=ID_nil) - irep_object["id"]=json_stringt(irep.id_string()); + irep_object["id"] = json_stringt(irep.id_string()); convert_sub_tree("sub", irep.get_sub(), irep_object); convert_named_sub_tree("namedSub", irep.get_named_sub(), irep_object); @@ -97,27 +96,44 @@ void json_irept::convert_named_sub_tree( /// \return result - irep equivalent of input irept json_irept::convert_from_json(const jsont &in) const { - std::vector have_keys; - for(const auto &keyval : to_json_object(in)) - have_keys.push_back(keyval.first); - std::sort(have_keys.begin(), have_keys.end()); - if(have_keys!=std::vector{"comment", "id", "namedSub", "sub"}) + if(!in.is_object()) { throw deserialization_exceptiont( - "irep JSON representation is missing one of needed keys: " - "'id', 'sub', 'namedSub', 'comment'"); + "irep JSON representation must be an object"); } - irept out(in["id"].value); + const json_objectt &json_object = to_json_object(in); - for(const auto &sub : to_json_array(in["sub"])) - out.get_sub().push_back(convert_from_json(sub)); + irept out; - for(const auto &named_sub : to_json_object(in["namedSub"])) - out.add(named_sub.first)=convert_from_json(named_sub.second); + { + const auto it = json_object.find("id"); + + if(it != json_object.end()) + { + out.id(it->second.value); + } + } + + { + const auto it = json_object.find("sub"); + + if(it != json_object.end()) + { + for(const auto &sub : to_json_array(it->second)) + out.get_sub().push_back(convert_from_json(sub)); + } + } + + { + const auto it = json_object.find("namedSub"); - for(const auto &comment : to_json_object(in["comment"])) - out.add(comment.first)=convert_from_json(comment.second); + if(it != json_object.end()) + { + for(const auto &named_sub : to_json_object(it->second)) + out.add(named_sub.first) = convert_from_json(named_sub.second); + } + } return out; } From 13dac86f18128254447f1d070fa497b44bbbd0e7 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 8 Jan 2019 15:51:33 +0000 Subject: [PATCH 2/3] Add equality operators to symbolt and symbol_tablet This adds equality member operators to symbolt and symbol_tablet. They will be useful in unit tests to check that when outputting a symbol table in JSON and reading it back in again the same symbol table is obtained. --- src/util/symbol.cpp | 31 +++++++++++++++++++++++++++++ src/util/symbol.h | 2 ++ src/util/symbol_table.cpp | 41 +++++++++++++++++++++++++++++++++++++++ src/util/symbol_table.h | 2 ++ 4 files changed, 76 insertions(+) diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 74221d377be..58edd886cd3 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -144,3 +144,34 @@ bool symbolt::is_well_formed() const return true; } + +bool symbolt::operator==(const symbolt &other) const +{ + // clang-format off + return + type == other.type && + value == other.value && + location == other.location && + name == other.name && + module == other.module && + base_name == other.base_name && + mode == other.mode && + pretty_name == other.pretty_name && + is_type == other.is_type && + is_macro == other.is_macro && + is_exported == other.is_exported && + is_input == other.is_input && + is_output == other.is_output && + is_state_var == other.is_state_var && + is_property == other.is_property && + is_parameter == other.is_parameter && + is_auxiliary == other.is_auxiliary && + is_weak == other.is_weak && + is_lvalue == other.is_lvalue && + is_static_lifetime == other.is_static_lifetime && + is_thread_local == other.is_thread_local && + is_file_local == other.is_file_local && + is_extern == other.is_extern && + is_volatile == other.is_volatile; + // clang-format on +} diff --git a/src/util/symbol.h b/src/util/symbol.h index 83d03a3aa62..e0fa8cf446c 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -124,6 +124,8 @@ class symbolt /// Check that a symbol is well formed. bool is_well_formed() const; + + bool operator==(const symbolt &other) const; }; std::ostream &operator<<(std::ostream &out, const symbolt &symbol); diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp index 296b2cd0df4..6f3df0ded7e 100644 --- a/src/util/symbol_table.cpp +++ b/src/util/symbol_table.cpp @@ -6,6 +6,8 @@ #include #include +#include + /// Move or copy a new symbol to the symbol table. /// \remarks This is a nicer interface than move and achieves the same /// result as both move and add. @@ -219,3 +221,42 @@ void symbol_tablet::validate(const validation_modet vm) const "'"); } } + +bool symbol_tablet::operator==(const symbol_tablet &other) const +{ + // we cannot use == for comparing the multimaps as it compares the items + // sequentially, but the order of items with equal keys depends on the + // insertion order + + { + std::vector> v1( + internal_symbol_base_map.begin(), internal_symbol_base_map.end()); + + std::vector> v2( + other.internal_symbol_base_map.begin(), + other.internal_symbol_base_map.end()); + + std::sort(v1.begin(), v1.end()); + std::sort(v2.begin(), v2.end()); + + if(v1 != v2) + return false; + } + + { + std::vector> v1( + internal_symbol_module_map.begin(), internal_symbol_module_map.end()); + + std::vector> v2( + other.internal_symbol_module_map.begin(), + other.internal_symbol_module_map.end()); + + std::sort(v1.begin(), v1.end()); + std::sort(v2.begin(), v2.end()); + + if(v1 != v2) + return false; + } + + return internal_symbols == other.internal_symbols; +} diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index a3b5a11bea7..3846643e780 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -119,6 +119,8 @@ class symbol_tablet : public symbol_table_baset /// Check that the symbol table is well-formed void validate(const validation_modet vm = validation_modet::INVARIANT) const; + + bool operator==(const symbol_tablet &other) const; }; #endif // CPROVER_UTIL_SYMBOL_TABLE_H From a3f38e711a177315e47a18cd7b5c374d8857e98a Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 8 Jan 2019 15:52:26 +0000 Subject: [PATCH 3/3] Add unit test to check symbol table JSON input and output format consistency The unit test first outputs a symbol table to JSON via show_symbol_table() and then reads it back in again via symbol_table_from_json(). Then, it checks that the initial symbol table and the symbol table read back in again are equal. --- src/util/ui_message.h | 4 +- unit/Makefile | 1 + unit/json_symbol_table.cpp | 149 +++++++++++++++++++++++++++++++++++++ 3 files changed, 152 insertions(+), 2 deletions(-) create mode 100644 unit/json_symbol_table.cpp diff --git a/src/util/ui_message.h b/src/util/ui_message.h index 5abe1a2fb32..ff097811316 100644 --- a/src/util/ui_message.h +++ b/src/util/ui_message.h @@ -27,14 +27,14 @@ class ui_message_handlert : public message_handlert virtual ~ui_message_handlert(); - uit get_ui() const + virtual uit get_ui() const { return _ui; } virtual void flush(unsigned level) override; - json_stream_arrayt &get_json_stream() + virtual json_stream_arrayt &get_json_stream() { PRECONDITION(json_stream!=nullptr); return *json_stream; diff --git a/unit/Makefile b/unit/Makefile index d24a82f5d90..488597b4a3d 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -28,6 +28,7 @@ SRC += analyses/ai/ai.cpp \ goto-symex/ssa_equation.cpp \ interpreter/interpreter.cpp \ json/json_parser.cpp \ + json_symbol_table.cpp \ path_strategies.cpp \ pointer-analysis/value_set.cpp \ solvers/floatbv/float_utils.cpp \ diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp new file mode 100644 index 00000000000..5163a65dc3f --- /dev/null +++ b/unit/json_symbol_table.cpp @@ -0,0 +1,149 @@ +/// Author: Daniel Poetzl + +/// \file json symbol table read/write consistency + +#include + +#include + +#include +#include +#include +#include + +#include +#include + +#include +#include + +#include +#include +#include +#include +#include + +#include +#include + +#include + +class test_ui_message_handlert : public ui_message_handlert +{ +public: + explicit test_ui_message_handlert(std::ostream &out) + : ui_message_handlert(cmdlinet(), ""), json_stream_array(out, 0) + { + } + + uit get_ui() const + { + return uit::JSON_UI; + } + + json_stream_arrayt &get_json_stream() + { + return json_stream_array; + } + + json_stream_arrayt json_stream_array; +}; + +void get_goto_model(std::istream &in, goto_modelt &goto_model) +{ + optionst options; + cbmc_parse_optionst::set_default_options(options); + + messaget null_message(null_message_handler); + + language_filest language_files; + language_files.set_message_handler(null_message_handler); + + std::string filename(""); + + language_filet &language_file = language_files.add_file(filename); + + language_file.language = get_default_language(); + + languaget &language = *language_file.language; + language.set_message_handler(null_message_handler); + language.set_language_options(options); + + { + bool r = language.parse(in, filename); + REQUIRE(!r); + } + + language_file.get_modules(); + + { + bool r = language_files.typecheck(goto_model.symbol_table); + REQUIRE(!r); + } + + REQUIRE(!goto_model.symbol_table.has_symbol(goto_functionst::entry_point())); + + { + bool r = language_files.generate_support_functions(goto_model.symbol_table); + REQUIRE(!r); + } + + goto_convert( + goto_model.symbol_table, goto_model.goto_functions, null_message_handler); +} + +TEST_CASE("json symbol table read/write consistency") +{ + register_language(new_ansi_c_language); + + cmdlinet cmdline; + config.main = "main"; + config.set(cmdline); + + goto_modelt goto_model; + + // Get symbol table associated with goto program + + { + std::string program = "int main() { return 0; }\n"; + + std::istringstream in(program); + get_goto_model(in, goto_model); + } + + const symbol_tablet &symbol_table1 = goto_model.symbol_table; + + // Convert symbol table to json string + + std::ostringstream out; + + { + test_ui_message_handlert ui_message_handler(out); + REQUIRE(ui_message_handler.get_ui() == ui_message_handlert::uit::JSON_UI); + + show_symbol_table(symbol_table1, ui_message_handler); + } + + // Convert json string to symbol table + + symbol_tablet symbol_table2; + + { + std::istringstream in(out.str()); + jsont json; + + bool r = parse_json(in, "", null_message_handler, json); + REQUIRE(!r); + + REQUIRE(json.is_array()); + + const json_arrayt &json_array = to_json_array(json); + const jsont &json_symbol_table = *json_array.begin(); + + symbol_table_from_json(json_symbol_table, symbol_table2); + } + + // Finally check if symbol tables are consistent + + REQUIRE(symbol_table1 == symbol_table2); +}