From 0d5e588767470302b80c1eed163a5cebcffe4c4b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 22 Aug 2018 12:48:39 +0100 Subject: [PATCH 1/3] Clean up show_symbol_table Don't use a std::set for a load-sort-read procedure; don't convert everything to and from std::string. --- src/goto-programs/show_symbol_table.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 771bc88da00..3e002f2ade7 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "show_symbol_table.h" +#include #include #include @@ -68,16 +69,16 @@ void show_symbol_table_plain( out << '\n' << "Symbols:" << '\n' << '\n'; // we want to sort alphabetically - std::set symbols; + std::vector symbols; + symbols.reserve(symbol_table.symbols.size()); for(const auto &symbol_pair : symbol_table.symbols) - { - symbols.insert(id2string(symbol_pair.first)); - } + symbols.push_back(id2string(symbol_pair.first)); + std::sort(symbols.begin(), symbols.end()); const namespacet ns(symbol_table); - for(const std::string &id : symbols) + for(const irep_idt &id : symbols) { const symbolt &symbol=ns.lookup(id); From c5901e089ffdea79570007bbfcdd661b75d2170e Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 22 Aug 2018 12:49:30 +0100 Subject: [PATCH 2/3] JSON stream: support streaming a key-value pair to an object Arrays already allow the equivalent operation, json_array_streamt::push_back(const jsont &) --- src/util/json_stream.h | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/util/json_stream.h b/src/util/json_stream.h index cbb4689a5de..40776fcbc64 100644 --- a/src/util/json_stream.h +++ b/src/util/json_stream.h @@ -169,6 +169,25 @@ class json_stream_objectt : public json_streamt return it->second; } + /// Push back a JSON element into the current object stream. + /// Note the pushed key won't be available via operator[], as it has been + /// output already. + /// Provided for compatibility with `jsont`. + /// \param key: new key to create in the streamed object + /// \param json: a non-streaming JSON element + void push_back(const std::string &key, const jsont &json) + { + PRECONDITION(open); + // Check the key is not already due to be output later: + PRECONDITION(!object.count(key)); + // To ensure consistency of the output, we flush and + // close the current child stream before printing the given element. + output_child_stream(); + output_delimiter(); + jsont::output_key(out, key); + json.output_rec(out, indent + 1); + } + json_stream_objectt &push_back_stream_object(const std::string &key); json_stream_arrayt &push_back_stream_array(const std::string &key); From 20e5d89221e856646824b622aca84f15359368f5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 22 Aug 2018 12:50:38 +0100 Subject: [PATCH 3/3] Implement --show-symbol-table in JSON-UI mode This provides a convenient format for filtering / selecting particular symbols. --- .../src/janalyzer/janalyzer_parse_options.cpp | 2 +- jbmc/src/jbmc/jbmc_parse_options.cpp | 4 +- .../goto-instrument/list-symbols-json/test.c | 5 + .../list-symbols-json/test.desc | 10 ++ .../show-symbol-table-json/test.c | 5 + .../show-symbol-table-json/test.desc | 10 ++ src/cbmc/cbmc_parse_options.cpp | 2 +- .../goto_analyzer_parse_options.cpp | 2 +- .../goto_instrument_parse_options.cpp | 4 +- src/goto-programs/show_symbol_table.cpp | 146 +++++++++++++++++- src/goto-programs/show_symbol_table.h | 8 +- 11 files changed, 181 insertions(+), 17 deletions(-) create mode 100644 regression/goto-instrument/list-symbols-json/test.c create mode 100644 regression/goto-instrument/list-symbols-json/test.desc create mode 100644 regression/goto-instrument/show-symbol-table-json/test.c create mode 100644 regression/goto-instrument/show-symbol-table-json/test.desc diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index fb2444ce954..b989d393b7e 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -377,7 +377,7 @@ int janalyzer_parse_optionst::doit() // show it? if(cmdline.isset("show-symbol-table")) { - ::show_symbol_table(goto_model.symbol_table, get_ui()); + ::show_symbol_table(goto_model.symbol_table, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index abcfc87057b..7291073a11a 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -652,7 +652,7 @@ int jbmc_parse_optionst::get_goto_program( if(cmdline.isset("show-symbol-table")) { show_symbol_table( - lazy_goto_model.symbol_table, ui_message_handler.get_ui()); + lazy_goto_model.symbol_table, ui_message_handler); return 0; } @@ -832,7 +832,7 @@ bool jbmc_parse_optionst::show_loaded_functions( if(cmdline.isset("show-symbol-table")) { show_symbol_table( - goto_model.get_symbol_table(), ui_message_handler.get_ui()); + goto_model.get_symbol_table(), ui_message_handler); return true; } diff --git a/regression/goto-instrument/list-symbols-json/test.c b/regression/goto-instrument/list-symbols-json/test.c new file mode 100644 index 00000000000..befe2fbb3aa --- /dev/null +++ b/regression/goto-instrument/list-symbols-json/test.c @@ -0,0 +1,5 @@ + +int main(int argc, char** argv) { + int x = 5; + ++x; +} diff --git a/regression/goto-instrument/list-symbols-json/test.desc b/regression/goto-instrument/list-symbols-json/test.desc new file mode 100644 index 00000000000..d0b14e48d19 --- /dev/null +++ b/regression/goto-instrument/list-symbols-json/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--list-symbols --json-ui +"symbolTable": \{ +"main": \{ +"main::1::x": \{ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/show-symbol-table-json/test.c b/regression/goto-instrument/show-symbol-table-json/test.c new file mode 100644 index 00000000000..befe2fbb3aa --- /dev/null +++ b/regression/goto-instrument/show-symbol-table-json/test.c @@ -0,0 +1,5 @@ + +int main(int argc, char** argv) { + int x = 5; + ++x; +} diff --git a/regression/goto-instrument/show-symbol-table-json/test.desc b/regression/goto-instrument/show-symbol-table-json/test.desc new file mode 100644 index 00000000000..8521d6158ff --- /dev/null +++ b/regression/goto-instrument/show-symbol-table-json/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--show-symbol-table --json-ui +"symbolTable": \{ +"main": \{ +"main::1::x": \{ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8f6e92cb262..6ad55eee81f 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -587,7 +587,7 @@ int cbmc_parse_optionst::get_goto_program( if(cmdline.isset("show-symbol-table")) { - show_symbol_table(goto_model, ui_message_handler.get_ui()); + show_symbol_table(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 038648adafd..27b51a179a3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -409,7 +409,7 @@ int goto_analyzer_parse_optionst::doit() // show it? if(cmdline.isset("show-symbol-table")) { - ::show_symbol_table(goto_model.symbol_table, get_ui()); + ::show_symbol_table(goto_model.symbol_table, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 085e7e0094c..cd4acd233c5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -464,7 +464,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("show-symbol-table")) { - ::show_symbol_table(goto_model, get_ui()); + ::show_symbol_table(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } @@ -519,7 +519,7 @@ int goto_instrument_parse_optionst::doit() if(cmdline.isset("list-symbols")) { - show_symbol_table_brief(goto_model, get_ui()); + show_symbol_table_brief(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp index 3e002f2ade7..9f5aaac1ec9 100644 --- a/src/goto-programs/show_symbol_table.cpp +++ b/src/goto-programs/show_symbol_table.cpp @@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "goto_model.h" void show_symbol_table_xml_ui() @@ -153,11 +155,139 @@ void show_symbol_table_plain( } } +static void show_symbol_table_json_ui( + const symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + json_stream_arrayt &out = message_handler.get_json_stream(); + + json_stream_objectt &result_wrapper = out.push_back_stream_object(); + json_stream_objectt &result = + result_wrapper.push_back_stream_object("symbolTable"); + + const namespacet ns(symbol_table); + json_irept irep_converter(true); + + for(const auto &id_and_symbol : symbol_table.symbols) + { + const symbolt &symbol = id_and_symbol.second; + + std::unique_ptr ptr; + + if(symbol.mode=="") + { + ptr=get_default_language(); + } + else + { + ptr=get_language_from_mode(symbol.mode); + } + + if(!ptr) + throw "symbol "+id2string(symbol.name)+" has unknown mode"; + + std::string type_str, value_str; + + if(symbol.type.is_not_nil()) + ptr->from_type(symbol.type, type_str, ns); + + if(symbol.value.is_not_nil()) + ptr->from_expr(symbol.value, value_str, ns); + + json_objectt symbol_json; + symbol_json["prettyName"] = json_stringt(symbol.pretty_name); + symbol_json["baseName"] = json_stringt(symbol.base_name); + symbol_json["mode"] = json_stringt(symbol.mode); + symbol_json["module"] = json_stringt(symbol.module); + + symbol_json["prettyType"] = json_stringt(type_str); + symbol_json["prettyValue"] = json_stringt(value_str); + + symbol_json["type"] = irep_converter.convert_from_irep(symbol.type); + symbol_json["value"] = irep_converter.convert_from_irep(symbol.value); + symbol_json["location"] = irep_converter.convert_from_irep(symbol.location); + + symbol_json["isType"] = jsont::json_boolean(symbol.is_type); + symbol_json["isMacro"] = jsont::json_boolean(symbol.is_macro); + symbol_json["isExported"] = jsont::json_boolean(symbol.is_exported); + symbol_json["isInput"] = jsont::json_boolean(symbol.is_input); + symbol_json["isOutput"] = jsont::json_boolean(symbol.is_output); + symbol_json["isStateVar"] = jsont::json_boolean(symbol.is_state_var); + symbol_json["isProperty"] = jsont::json_boolean(symbol.is_property); + symbol_json["isStaticLifetime"] = + jsont::json_boolean(symbol.is_static_lifetime); + symbol_json["isThreadLocal"] = + jsont::json_boolean(symbol.is_thread_local); + symbol_json["isLvalue"] = jsont::json_boolean(symbol.is_lvalue); + symbol_json["isFileLocal"] = jsont::json_boolean(symbol.is_file_local); + symbol_json["isExtern"] = jsont::json_boolean(symbol.is_extern); + symbol_json["isVolatile"] = jsont::json_boolean(symbol.is_volatile); + symbol_json["isParameter"] = jsont::json_boolean(symbol.is_parameter); + symbol_json["isAuxiliary"] = jsont::json_boolean(symbol.is_auxiliary); + symbol_json["isWeak"] = jsont::json_boolean(symbol.is_weak); + + result.push_back(id2string(symbol.name), symbol_json); + } +} + +static void show_symbol_table_brief_json_ui( + const symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + json_stream_arrayt &out = message_handler.get_json_stream(); + + json_stream_objectt &result_wrapper = out.push_back_stream_object(); + json_stream_objectt &result = + result_wrapper.push_back_stream_object("symbolTable"); + + const namespacet ns(symbol_table); + json_irept irep_converter(true); + + for(const auto &id_and_symbol : symbol_table.symbols) + { + const symbolt &symbol = id_and_symbol.second; + + std::unique_ptr ptr; + + if(symbol.mode=="") + { + ptr=get_default_language(); + } + else + { + ptr=get_language_from_mode(symbol.mode); + } + + if(!ptr) + throw "symbol "+id2string(symbol.name)+" has unknown mode"; + + std::string type_str, value_str; + + if(symbol.type.is_not_nil()) + ptr->from_type(symbol.type, type_str, ns); + + if(symbol.value.is_not_nil()) + ptr->from_expr(symbol.value, value_str, ns); + + json_objectt symbol_json; + symbol_json["prettyName"] = json_stringt(symbol.pretty_name); + symbol_json["baseName"] = json_stringt(symbol.base_name); + symbol_json["mode"] = json_stringt(symbol.mode); + symbol_json["module"] = json_stringt(symbol.module); + + symbol_json["prettyType"] = json_stringt(type_str); + + symbol_json["type"] = irep_converter.convert_from_irep(symbol.type); + + result.push_back(id2string(symbol.name), symbol_json); + } +} + void show_symbol_table( const symbol_tablet &symbol_table, - ui_message_handlert::uit ui) + ui_message_handlert &ui) { - switch(ui) + switch(ui.get_ui()) { case ui_message_handlert::uit::PLAIN: show_symbol_table_plain(symbol_table, std::cout); @@ -167,6 +297,9 @@ void show_symbol_table( show_symbol_table_xml_ui(); break; + case ui_message_handlert::uit::JSON_UI: + show_symbol_table_json_ui(symbol_table, ui); + default: break; } @@ -174,16 +307,16 @@ void show_symbol_table( void show_symbol_table( const goto_modelt &goto_model, - ui_message_handlert::uit ui) + ui_message_handlert &ui) { show_symbol_table(goto_model.symbol_table, ui); } void show_symbol_table_brief( const symbol_tablet &symbol_table, - ui_message_handlert::uit ui) + ui_message_handlert &ui) { - switch(ui) + switch(ui.get_ui()) { case ui_message_handlert::uit::PLAIN: show_symbol_table_brief_plain(symbol_table, std::cout); @@ -194,13 +327,14 @@ void show_symbol_table_brief( break; default: + show_symbol_table_brief_json_ui(symbol_table, ui); break; } } void show_symbol_table_brief( const goto_modelt &goto_model, - ui_message_handlert::uit ui) + ui_message_handlert &ui) { show_symbol_table_brief(goto_model.symbol_table, ui); } diff --git a/src/goto-programs/show_symbol_table.h b/src/goto-programs/show_symbol_table.h index 82e49128967..d5daa0eef9e 100644 --- a/src/goto-programs/show_symbol_table.h +++ b/src/goto-programs/show_symbol_table.h @@ -19,18 +19,18 @@ class goto_modelt; void show_symbol_table( const symbol_tablet &, - ui_message_handlert::uit ui); + ui_message_handlert &ui); void show_symbol_table_brief( const symbol_tablet &, - ui_message_handlert::uit ui); + ui_message_handlert &ui); void show_symbol_table( const goto_modelt &, - ui_message_handlert::uit ui); + ui_message_handlert &ui); void show_symbol_table_brief( const goto_modelt &, - ui_message_handlert::uit ui); + ui_message_handlert &ui); #endif // CPROVER_GOTO_PROGRAMS_SHOW_SYMBOL_TABLE_H