Add JSON symbol table

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

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

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

@@ -11,12 +11,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "show_symbol_table.h"
 
+#include <algorithm>
 #include <iostream>
 #include <memory>
 
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <util/json_irep.h>
+
 #include "goto_model.h"
 
 void show_symbol_table_xml_ui()
@@ -68,16 +71,16 @@ void show_symbol_table_plain(
   out << '\n' << "Symbols:" << '\n' << '\n';
 
   // we want to sort alphabetically
-  std::set<std::string> symbols;
+  std::vector<std::string> 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);
 
@@ -152,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["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<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["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);
@@ -166,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);
@@ -193,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

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