Implement --show-symbol-table in JSON-UI mode

This provides a convenient format for filtering / selecting particular symbols.

Author: smowton

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;
   }
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -649,7 +649,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;
     }
 
@@ -829,7 +829,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;
   }
 

regression/goto-instrument/list-symbols-json/test.c

@@ -0,0 +1,5 @@
+
+int main(int argc, char** argv) {
+  int x = 5;
+  ++x;
+}

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

regression/goto-instrument/show-symbol-table-json/test.c

@@ -0,0 +1,5 @@
+
+int main(int argc, char** argv) {
+  int x = 5;
+  ++x;
+}

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

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;
     }
 

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;
   }
 

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;
     }
 

src/goto-programs/show_symbol_table.cpp

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <util/json_irep.h>
+
 #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<languaget> 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["pretty_name"] = json_stringt(symbol.pretty_name);
+    symbol_json["base_name"] = json_stringt(symbol.base_name);
+    symbol_json["mode"] = json_stringt(symbol.mode);
+    symbol_json["module"] = json_stringt(symbol.module);
+
+    symbol_json["pretty_type"] = json_stringt(type_str);
+    symbol_json["pretty_value"] = 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["is_type"] = jsont::json_boolean(symbol.is_type);
+    symbol_json["is_macro"] = jsont::json_boolean(symbol.is_macro);
+    symbol_json["is_exported"] = jsont::json_boolean(symbol.is_exported);
+    symbol_json["is_input"] = jsont::json_boolean(symbol.is_input);
+    symbol_json["is_output"] = jsont::json_boolean(symbol.is_output);
+    symbol_json["is_state_var"] = jsont::json_boolean(symbol.is_state_var);
+    symbol_json["is_property"] = jsont::json_boolean(symbol.is_property);
+    symbol_json["is_static_lifetime"] =
+      jsont::json_boolean(symbol.is_static_lifetime);
+    symbol_json["is_thread_local"] =
+      jsont::json_boolean(symbol.is_thread_local);
+    symbol_json["is_lvalue"] = jsont::json_boolean(symbol.is_lvalue);
+    symbol_json["is_file_local"] = jsont::json_boolean(symbol.is_file_local);
+    symbol_json["is_extern"] = jsont::json_boolean(symbol.is_extern);
+    symbol_json["is_volatile"] = jsont::json_boolean(symbol.is_volatile);
+    symbol_json["is_parameter"] = jsont::json_boolean(symbol.is_parameter);
+    symbol_json["is_auxiliary"] = jsont::json_boolean(symbol.is_auxiliary);
+    symbol_json["is_weak"] = 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<languaget> 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["pretty_name"] = json_stringt(symbol.pretty_name);
+    symbol_json["base_name"] = json_stringt(symbol.base_name);
+    symbol_json["mode"] = json_stringt(symbol.mode);
+    symbol_json["module"] = json_stringt(symbol.module);
+
+    symbol_json["pretty_type"] = 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,23 +297,26 @@ 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;
   }
 }
 
 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);
 }

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