Merge pull request #3601 from tautschnig/json-api

Equip json_arrayt and json_objectt with a full API to enable hiding [blocks: #3602]

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -161,7 +161,7 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
         throw "the JSON file has a wrong format";
 
       // add jars from JSON config file to classpath
-      for(const jsont &file_entry : include_files.array)
+      for(const jsont &file_entry : to_json_array(include_files))
       {
         DATA_INVARIANT(
           file_entry.is_string() && has_suffix(file_entry.value, ".jar"),

jbmc/src/java_bytecode/java_class_loader_limit.cpp

@@ -74,7 +74,7 @@ void java_class_loader_limitt::setup_class_load_limit(
     jsont include_files=json_cp_config["classFiles"];
     if(!include_files.is_null() && !include_files.is_array())
       throw "the JSON file has a wrong format";
-    for(const jsont &file_entry : include_files.array)
+    for(const jsont &file_entry : to_json_array(include_files))
     {
       assert(file_entry.is_string());
       set_matcher.insert(file_entry.value);

src/goto-analyzer/taint_analysis.cpp

@@ -358,7 +358,7 @@ bool taint_analysist::operator()(
           json["file"] = json_stringt(i_it->source_location.get_file());
           json["line"]=
             json_numbert(id2string(i_it->source_location.get_line()));
-          json_result.array.push_back(json);
+          json_result.push_back(json);
         }
         else
         {

src/goto-analyzer/taint_parser.cpp

@@ -40,28 +40,25 @@ bool taint_parser(
     return true;
   }
 
-  for(jsont::arrayt::const_iterator
+  for(const auto &taint_spec : to_json_array(json))
-      it=json.array.begin();
-      it!=json.array.end();
-      it++)
   {
-    if(!it->is_object())
+    if(!taint_spec.is_object())
     {
       messaget message(message_handler);
       message.error() << "expecting an array of objects "
-                      << "in the taint file, but got "
+                      << "in the taint file, but got " << taint_spec
-                      << *it << messaget::eom;
+                      << messaget::eom;
       return true;
     }
 
     taint_parse_treet::rulet rule;
 
-    const std::string kind=(*it)["kind"].value;
+    const std::string kind = taint_spec["kind"].value;
-    const std::string function=(*it)["function"].value;
+    const std::string function = taint_spec["function"].value;
-    const std::string where=(*it)["where"].value;
+    const std::string where = taint_spec["where"].value;
-    const std::string taint=(*it)["taint"].value;
+    const std::string taint = taint_spec["taint"].value;
-    const std::string message=(*it)["message"].value;
+    const std::string message = taint_spec["message"].value;
-    const std::string id=(*it)["id"].value;
+    const std::string id = taint_spec["id"].value;
 
     if(kind=="source")
       rule.kind=taint_parse_treet::rulet::SOURCE;

src/goto-analyzer/unreachable_instructions.cpp

@@ -197,7 +197,7 @@ void unreachable_instructions(
     }
   }
 
-  if(json && !json_result.array.empty())
+  if(json && !json_result.empty())
     os << json_result << '\n';
 }
 
@@ -239,7 +239,7 @@ bool static_unreachable_instructions(
     }
   }
 
-  if(options.get_bool_option("json") && !json_result.array.empty())
+  if(options.get_bool_option("json") && !json_result.empty())
     out << json_result << '\n';
   else if(options.get_bool_option("xml"))
     out << xml_result << '\n';
@@ -369,7 +369,7 @@ static void list_functions(
     }
   }
 
-  if(options.get_bool_option("json") && !json_result.array.empty())
+  if(options.get_bool_option("json") && !json_result.empty())
     os << json_result << '\n';
   else if(options.get_bool_option("xml"))
     os << xml_result << '\n';

src/goto-cc/linker_script_merge.cpp

@@ -400,7 +400,7 @@ int linker_script_merget::ls_data2instructions(
 {
   goto_programt::instructionst initialize_instructions=gp.instructions;
   std::map<irep_idt, std::size_t> truncated_symbols;
-  for(auto &d : data["regions"].array)
+  for(auto &d : to_json_array(data["regions"]))
   {
     bool has_end=d["has-end-symbol"].is_true();
 
@@ -446,11 +446,13 @@ int linker_script_merget::ls_data2instructions(
 
     // Since the value of the pointer will be a random CBMC address, write a
     // note about the real address in the object file
-    auto it=std::find_if(data["addresses"].array.begin(),
+    auto it = std::find_if(
-                         data["addresses"].array.end(),
+      to_json_array(data["addresses"]).begin(),
-                         [&d](const jsont &add)
+      to_json_array(data["addresses"]).end(),
-                         { return add["sym"].value==d["start-symbol"].value; });
+      [&d](const jsont &add) {
-    if(it==data["addresses"].array.end())
+        return add["sym"].value == d["start-symbol"].value;
+      });
+    if(it == to_json_array(data["addresses"]).end())
     {
       error() << "Start: Could not find address corresponding to symbol '"
               << d["start-symbol"].value << "' (start of section)" << eom;
@@ -481,12 +483,12 @@ int linker_script_merget::ls_data2instructions(
       linker_values[d["end-symbol"].value]=std::make_pair(end_sym, array_end);
 
       auto entry = std::find_if(
-        data["addresses"].array.begin(),
+        to_json_array(data["addresses"]).begin(),
-        data["addresses"].array.end(),
+        to_json_array(data["addresses"]).end(),
         [&d](const jsont &add) {
           return add["sym"].value == d["end-symbol"].value;
         });
-      if(entry == data["addresses"].array.end())
+      if(entry == to_json_array(data["addresses"]).end())
       {
         error() << "Could not find address corresponding to symbol '"
                 << d["end-symbol"].value << "' (end of section)" << eom;
@@ -539,7 +541,7 @@ int linker_script_merget::ls_data2instructions(
   // address. These will have been declared extern too, so we need to give them
   // a value also. Here, we give them the actual value that they have in the
   // object file, since we're not assigning any object to them.
-  for(const auto &d : data["addresses"].array)
+  for(const auto &d : to_json_array(data["addresses"]))
   {
     auto it=linker_values.find(irep_idt(d["sym"].value));
     if(it!=linker_values.end())
@@ -591,7 +593,7 @@ int linker_script_merget::ls_data2instructions(
 #else
 {
   goto_programt::instructionst initialize_instructions=gp.instructions;
-  for(const auto &d : data["regions"].array)
+  for(const auto &d : to_json_array(data["regions"]))
   {
     unsigned start=safe_string2unsigned(d["start"].value);
     unsigned size=safe_string2unsigned(d["size"].value);
@@ -623,7 +625,7 @@ int linker_script_merget::ls_data2instructions(
     symbol_table.add(sym);
   }
 
-  for(const auto &d : data["addresses"].array)
+  for(const auto &d : to_json_array(data["addresses"]))
   {
     source_locationt loc;
     loc.set_file(linker_script);
@@ -738,38 +740,51 @@ int linker_script_merget::goto_and_object_mismatch(
 
 int linker_script_merget::linker_data_is_malformed(const jsont &data) const
 {
+  if(!data.is_object())
+    return true;
+
+  const json_objectt &data_object = to_json_object(data);
   return (
-    !(data.is_object() && data.object.find("regions") != data.object.end() &&
+    !(data_object.find("regions") != data_object.end() &&
-      data.object.find("addresses") != data.object.end() &&
+      data_object.find("addresses") != data_object.end() &&
       data["regions"].is_array() && data["addresses"].is_array() &&
       std::all_of(
-        data["addresses"].array.begin(),
+        to_json_array(data["addresses"]).begin(),
-        data["addresses"].array.end(),
+        to_json_array(data["addresses"]).end(),
         [](const jsont &j) {
-          return j.is_object() && j.object.find("val") != j.object.end() &&
+          if(!j.is_object())
-                 j.object.find("sym") != j.object.end() &&
+            return false;
-                 j["val"].is_number() && j["sym"].is_string();
+
+          const json_objectt &address = to_json_object(j);
+          return address.find("val") != address.end() &&
+                 address.find("sym") != address.end() &&
+                 address["val"].is_number() && address["sym"].is_string();
         }) &&
       std::all_of(
-        data["regions"].array.begin(),
+        to_json_array(data["regions"]).begin(),
-        data["regions"].array.end(),
+        to_json_array(data["regions"]).end(),
         [](const jsont &j) {
-          return j.is_object() && j.object.find("start") != j.object.end() &&
+          if(!j.is_object())
-                 j.object.find("size") != j.object.end() &&
+            return false;
-                 j.object.find("annot") != j.object.end() &&
+
-                 j.object.find("commt") != j.object.end() &&
+          const json_objectt &region = to_json_object(j);
-                 j.object.find("start-symbol") != j.object.end() &&
+          return region.find("start") != region.end() &&
-                 j.object.find("has-end-symbol") != j.object.end() &&
+                 region.find("size") != region.end() &&
-                 j.object.find("section") != j.object.end() &&
+                 region.find("annot") != region.end() &&
-                 j["start"].is_number() && j["size"].is_number() &&
+                 region.find("commt") != region.end() &&
-                 j["annot"].is_string() && j["start-symbol"].is_string() &&
+                 region.find("start-symbol") != region.end() &&
-                 j["section"].is_string() && j["commt"].is_string() &&
+                 region.find("has-end-symbol") != region.end() &&
-                 ((j["has-end-symbol"].is_true() &&
+                 region.find("section") != region.end() &&
-                   j.object.find("end-symbol") != j.object.end() &&
+                 region["start"].is_number() && region["size"].is_number() &&
-                   j["end-symbol"].is_string()) ||
+                 region["annot"].is_string() &&
-                  (j["has-end-symbol"].is_false() &&
+                 region["start-symbol"].is_string() &&
-                   j.object.find("size-symbol") != j.object.end() &&
+                 region["section"].is_string() && region["commt"].is_string() &&
-                   j.object.find("end-symbol") == j.object.end() &&
+                 ((region["has-end-symbol"].is_true() &&
-                   j["size-symbol"].is_string()));
+                   region.find("end-symbol") != region.end() &&
+                   region["end-symbol"].is_string()) ||
+                  (region["has-end-symbol"].is_false() &&
+                   region.find("size-symbol") != region.end() &&
+                   region.find("end-symbol") == region.end() &&
+                   region["size-symbol"].is_string()));
         })));
 }

src/json-symtab-language/json_symbol.cpp

@@ -48,7 +48,7 @@ symbolt symbol_from_json(const jsont &in)
     throw deserialization_exceptiont("symbol_from_json takes an object");
   symbolt result;
   json_irept json2irep(true);
-  for(const auto &kv : in.object)
+  for(const auto &kv : to_json_object(in))
   {
     if(kv.first == "type")
     {

src/json-symtab-language/json_symbol_table.cpp

@@ -18,7 +18,7 @@ void symbol_table_from_json(const jsont &in, symbol_tablet &symbol_table)
   if(!in.is_array())
     throw deserialization_exceptiont(
       "symbol_table_from_json: JSON input must be an array");
-  for(const auto &js_symbol : in.array)
+  for(const auto &js_symbol : to_json_array(in))
   {
     symbolt deserialized = symbol_from_json(js_symbol);
     if(symbol_table.add(deserialized))

src/json/parser.y

@@ -90,7 +90,7 @@ key_value_pair:
         {
           jsont tmp;
           json_parser.pop(tmp);
-          json_parser.top().object[json_parser.top().value].swap(tmp);
+          to_json_object(json_parser.top())[json_parser.top().value].swap(tmp);
           json_parser.top().value.clear(); // end abuse
         }
         ;
@@ -109,7 +109,7 @@ array_value:
         {
           jsont tmp;
           json_parser.pop(tmp);
-          json_parser.top().array.push_back(tmp);
+          to_json_array(json_parser.top()).push_back(tmp);
         }
         ;
 

src/util/json.h

@@ -22,6 +22,10 @@ class json_arrayt;
 
 class jsont
 {
+protected:
+  typedef std::vector<jsont> arrayt;
+  typedef std::map<std::string, jsont> objectt;
+
 public:
   enum class kindt
   {
@@ -112,7 +116,17 @@ public:
 
   static const jsont null_json_object;
 
+  static void output_key(std::ostream &out, const std::string &key);
+
+  static void
+  output_object(std::ostream &out, const objectt &object, unsigned indent);
+
+  std::string value;
+
 protected:
+  arrayt array;
+  objectt object;
+
   static void escape_string(const std::string &, std::ostream &);
 
   explicit jsont(kindt _kind):kind(_kind)
@@ -122,19 +136,6 @@ protected:
   jsont(kindt _kind, std::string _value) : kind(_kind), value(std::move(_value))
   {
   }
-
-public:
-  // should become protected
-  typedef std::vector<jsont> arrayt;
-  arrayt array;
-
-  typedef std::map<std::string, jsont> objectt;
-  objectt object;
-  static void
-  output_object(std::ostream &out, const objectt &object, unsigned indent);
-  static void output_key(std::ostream &out, const std::string &key);
-
-  std::string value;
 };
 
 inline std::ostream &operator<<(std::ostream &out, const jsont &src)
@@ -160,12 +161,23 @@ public:
     return array.size();
   }
 
+  bool empty() const
+  {
+    return array.empty();
+  }
+
   jsont &push_back(const jsont &json)
   {
     array.push_back(json);
     return array.back();
   }
 
+  jsont &push_back(jsont &&json)
+  {
+    array.push_back(std::move(json));
+    return array.back();
+  }
+
   jsont &push_back()
   {
     array.push_back(jsont());
@@ -178,32 +190,32 @@ public:
     array.emplace_back(std::forward<argumentst>(arguments)...);
   }
 
-  std::vector<jsont>::iterator begin()
+  arrayt::iterator begin()
   {
     return array.begin();
   }
 
-  std::vector<jsont>::const_iterator begin() const
+  arrayt::const_iterator begin() const
   {
     return array.begin();
   }
 
-  std::vector<jsont>::const_iterator cbegin() const
+  arrayt::const_iterator cbegin() const
   {
     return array.cbegin();
   }
 
-  std::vector<jsont>::iterator end()
+  arrayt::iterator end()
   {
     return array.end();
   }
 
-  std::vector<jsont>::const_iterator end() const
+  arrayt::const_iterator end() const
   {
     return array.end();
   }
 
-  std::vector<jsont>::const_iterator cend() const
+  arrayt::const_iterator cend() const
   {
     return array.cend();
   }
@@ -261,6 +273,48 @@ public:
     else
       return it->second;
   }
+
+  objectt::iterator find(const std::string &key)
+  {
+    return object.find(key);
+  }
+
+  objectt::const_iterator find(const std::string &key) const
+  {
+    return object.find(key);
+  }
+
+  objectt::iterator begin()
+  {
+    return object.begin();
+  }
+
+  objectt::const_iterator begin() const
+  {
+    return object.begin();
+  }
+
+  objectt::const_iterator cbegin() const
+  {
+    return object.cbegin();
+  }
+
+  objectt::iterator end()
+  {
+    return object.end();
+  }
+
+  objectt::const_iterator end() const
+  {
+    return object.end();
+  }
+
+  objectt::const_iterator cend() const
+  {
+    return object.cend();
+  }
+
+  typedef jsont value_type; // NOLINT(readability/identifiers)
 };
 
 class json_truet:public jsont
@@ -287,10 +341,34 @@ inline json_arrayt &jsont::make_array()
   return static_cast<json_arrayt &>(*this);
 }
 
+inline json_arrayt &to_json_array(jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_ARRAY);
+  return static_cast<json_arrayt &>(json);
+}
+
+inline const json_arrayt &to_json_array(const jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_ARRAY);
+  return static_cast<const json_arrayt &>(json);
+}
+
 inline json_objectt &jsont::make_object()
 {
   kind=kindt::J_OBJECT;
   return static_cast<json_objectt &>(*this);
 }
 
+inline json_objectt &to_json_object(jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_OBJECT);
+  return static_cast<json_objectt &>(json);
+}
+
+inline const json_objectt &to_json_object(const jsont &json)
+{
+  PRECONDITION(json.kind == jsont::kindt::J_OBJECT);
+  return static_cast<const json_objectt &>(json);
+}
+
 #endif // CPROVER_UTIL_JSON_H

src/util/json_irep.cpp

@@ -98,7 +98,7 @@ void json_irept::convert_named_sub_tree(
 irept json_irept::convert_from_json(const jsont &in) const
 {
   std::vector<std::string> have_keys;
-  for(const auto &keyval : in.object)
+  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"})
@@ -110,13 +110,13 @@ irept json_irept::convert_from_json(const jsont &in) const
 
   irept out(in["id"].value);
 
-  for(const auto &sub : in["sub"].array)
+  for(const auto &sub : to_json_array(in["sub"]))
     out.get_sub().push_back(convert_from_json(sub));
 
-  for(const auto &named_sub : in["namedSub"].object)
+  for(const auto &named_sub : to_json_object(in["namedSub"]))
     out.add(named_sub.first)=convert_from_json(named_sub.second);
 
-  for(const auto &comment : in["comment"].object)
+  for(const auto &comment : to_json_object(in["comment"]))
     out.add(comment.first)=convert_from_json(comment.second);
 
   return out;

unit/json/json_parser.cpp

@@ -49,8 +49,10 @@ SCENARIO("Loading JSON files")
           {
             REQUIRE_FALSE(valid_parse_error);
             REQUIRE(valid_json.is_object());
-            REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
+
-            REQUIRE(valid_json.object["hello"].value == "world");
+            const json_objectt &json_object = to_json_object(valid_json);
+            REQUIRE(json_object.find("hello") != json_object.end());
+            REQUIRE(json_object["hello"].value == "world");
           }
         }
       }
@@ -64,8 +66,10 @@ SCENARIO("Loading JSON files")
       {
         REQUIRE_FALSE(valid_parse_error);
         REQUIRE(valid_json.is_object());
-        REQUIRE(valid_json.object.find("hello") != valid_json.object.end());
+
-        REQUIRE(valid_json.object["hello"].value == "world");
+        const json_objectt &json_object = to_json_object(valid_json);
+        REQUIRE(json_object.find("hello") != json_object.end());
+        REQUIRE(json_object["hello"].value == "world");
         AND_WHEN("Loading the invalid JSON file")
         {
           jsont invalid_json;