Merge pull request #3726 from danpoe/fixes/json-symbol-table

Make JSON symbol table input and output consistent

Author: danpoe

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)},

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 + "'");

src/json-symtab-language/json_symbol_table.cpp

@@ -15,15 +15,38 @@ Author: Chris Smowton, [email protected]
 
 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) + "`");
   }
 }

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<std::string> 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<std::string>{"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;
 }

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

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

src/util/symbol_table.cpp

@@ -6,6 +6,8 @@
 #include <util/invariant.h>
 #include <util/validate.h>
 
+#include <set>
+
 /// 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<std::pair<irep_idt, irep_idt>> v1(
+      internal_symbol_base_map.begin(), internal_symbol_base_map.end());
+
+    std::vector<std::pair<irep_idt, irep_idt>> 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<std::pair<irep_idt, irep_idt>> v1(
+      internal_symbol_module_map.begin(), internal_symbol_module_map.end());
+
+    std::vector<std::pair<irep_idt, irep_idt>> 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;
+}

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

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;

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 \