Enable construction of JSON arrays and objects in place

This enables RAII and gets us close to writing JSON in source code while still
being efficient.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -453,8 +453,7 @@ int jbmc_parse_optionst::doit()
       break;
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_options;
-      json_options["options"] = options.to_json();
+      json_objectt json_options({{"options", options.to_json()}});
       debug() << json_options;
       break;
     }

src/analyses/ai.cpp

@@ -97,20 +97,17 @@ jsont ai_baset::output_json(
 
   forall_goto_program_instructions(i_it, goto_program)
   {
-    json_objectt location;
-    location["locationNumber"]=
-      json_numbert(std::to_string(i_it->location_number));
-    location["sourceLocation"]=
-      json_stringt(i_it->source_location.as_string());
-    location["abstractState"] =
-      abstract_state_before(i_it)->output_json(*this, ns);
-
     // Ideally we need output_instruction_json
     std::ostringstream out;
     goto_program.output_instruction(ns, identifier, out, *i_it);
-    location["instruction"]=json_stringt(out.str());
 
-    contents.push_back(location);
+    json_objectt location(
+      {{"locationNumber", json_numbert(std::to_string(i_it->location_number))},
+       {"sourceLocation", json_stringt(i_it->source_location.as_string())},
+       {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
+       {"instruction", json_stringt(out.str())}});
+
+    contents.push_back(std::move(location));
   }
 
   return std::move(contents);

src/analyses/dependence_graph.cpp

@@ -284,21 +284,20 @@ jsont dep_graph_domaint::output_json(
 
   for(const auto &cd : control_deps)
   {
-    json_objectt &link=graph.push_back().make_object();
-    link["locationNumber"]=
-      json_numbert(std::to_string(cd->location_number));
-    link["sourceLocation"]=json(cd->source_location);
-    link["type"]=json_stringt("control");
+    json_objectt link(
+      {{"locationNumber", json_numbert(std::to_string(cd->location_number))},
+       {"sourceLocation", json(cd->source_location)},
+       {"type", json_stringt("control")}});
+    graph.push_back(std::move(link));
   }
 
   for(const auto &dd : data_deps)
   {
-    json_objectt &link=graph.push_back().make_object();
-    link["locationNumber"]=
-      json_numbert(std::to_string(dd->location_number));
-    link["sourceLocation"]=json(dd->source_location);
-      json_stringt(dd->source_location.as_string());
-    link["type"]=json_stringt("data");
+    json_objectt link(
+      {{"locationNumber", json_numbert(std::to_string(dd->location_number))},
+       {"sourceLocation", json(dd->source_location)},
+       {"type", json_stringt("data")}});
+    graph.push_back(std::move(link));
   }
 
   return std::move(graph);

src/cbmc/bmc.cpp

@@ -176,8 +176,7 @@ void bmct::report_success(messaget &log, ui_message_handlert &handler)
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_result["cProverStatus"]=json_stringt("success");
+      json_objectt json_result({{"cProverStatus", json_stringt("success")}});
       log.result() << json_result;
     }
     break;
@@ -208,8 +207,7 @@ void bmct::report_failure(messaget &log, ui_message_handlert &handler)
 
   case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_result["cProverStatus"]=json_stringt("failure");
+      json_objectt json_result({{"cProverStatus", json_stringt("failure")}});
       log.result() << json_result;
     }
     break;

src/cbmc/bmc_cover.cpp

@@ -365,7 +365,6 @@ bool bmc_covert::operator()()
       json_arrayt &tests_array=json_result["tests"].make_array();
       for(const auto &test : tests)
       {
-        json_objectt &result=tests_array.push_back().make_object();
         if(bmc.options.get_bool_option("trace"))
         {
           json_arrayt &json_trace = json_result["trace"].make_array();
@@ -379,20 +378,21 @@ bool bmc_covert::operator()()
           {
             if(step.is_input())
             {
-              json_objectt json_input;
-              json_input["id"] = json_stringt(step.io_id);
+              json_objectt json_input({{"id", json_stringt(step.io_id)}});
               if(step.io_args.size()==1)
                 json_input["value"]=
                   json(step.io_args.front(), bmc.ns, ID_unknown);
-              json_test.push_back(json_input);
+              json_test.push_back(std::move(json_input));
             }
           }
         }
-        json_arrayt &goal_refs=result["coveredGoals"].make_array();
+        json_arrayt goal_refs;
         for(const auto &goal_id : test.covered_goals)
         {
           goal_refs.push_back(json_stringt(goal_id));
         }
+        tests_array.push_back(
+          json_objectt({{"coveredGoals", std::move(goal_refs)}}));
       }
 
       break;

src/goto-analyzer/taint_analysis.cpp

@@ -352,13 +352,13 @@ bool taint_analysist::operator()(
 
         if(use_json)
         {
-          json_objectt json;
-          json["bugClass"] =
-            json_stringt(i_it->source_location.get_property_class());
-          json["file"] = json_stringt(i_it->source_location.get_file());
-          json["line"]=
-            json_numbert(id2string(i_it->source_location.get_line()));
-          json_result.push_back(json);
+          json_objectt json(
+            {{"bugClass",
+              json_stringt(i_it->source_location.get_property_class())},
+             {"file", json_stringt(i_it->source_location.get_file())},
+             {"line",
+              json_numbert(id2string(i_it->source_location.get_line()))}});
+          json_result.push_back(std::move(json));
         }
         else
         {

src/goto-analyzer/unreachable_instructions.cpp

@@ -117,20 +117,19 @@ static void add_to_json(
   const dead_mapt &dead_map,
   json_arrayt &dest)
 {
-  json_objectt &entry=dest.push_back().make_object();
-
   PRECONDITION(!goto_program.instructions.empty());
   goto_programt::const_targett end_function=
     goto_program.instructions.end();
   --end_function;
   DATA_INVARIANT(end_function->is_end_function(),
                  "The last instruction in a goto-program must be END_FUNCTION");
 
-  entry["function"] = json_stringt(end_function->function);
-  entry["fileName"]=
-    json_stringt(concat_dir_file(
+  json_objectt entry(
+    {{"function", json_stringt(end_function->function)},
+     {"fileName",
+      json_stringt(concat_dir_file(
         id2string(end_function->source_location.get_working_directory()),
-        id2string(end_function->source_location.get_file())));
+        id2string(end_function->source_location.get_file())))}});
 
   json_arrayt &dead_ins=entry["unreachableInstructions"].make_array();
 
@@ -152,11 +151,13 @@ static void add_to_json(
     s.erase(s.size()-1);
 
     // print info for file actually with full path
-    json_objectt &i_entry=dead_ins.push_back().make_object();
     const source_locationt &l=it->second->source_location;
-    i_entry["sourceLocation"]=json(l);
-    i_entry["statement"]=json_stringt(s);
+    json_objectt i_entry(
+      {{"sourceLocation", json(l)}, {"statement", json_stringt(s)}});
+    dead_ins.push_back(std::move(i_entry));
   }
+
+  dest.push_back(std::move(entry));
 }
 
 void unreachable_instructions(
@@ -255,17 +256,16 @@ static void json_output_function(
   const source_locationt &last_location,
   json_arrayt &dest)
 {
-  json_objectt &entry=dest.push_back().make_object();
-
-  entry["function"] = json_stringt(function);
-  entry["file name"]=
-    json_stringt(concat_dir_file(
+  json_objectt entry(
+    {{"function", json_stringt(function)},
+     {"file name",
+      json_stringt(concat_dir_file(
         id2string(first_location.get_working_directory()),
-        id2string(first_location.get_file())));
-  entry["first line"]=
-    json_numbert(id2string(first_location.get_line()));
-  entry["last line"]=
-    json_numbert(id2string(last_location.get_line()));
+        id2string(first_location.get_file())))},
+     {"first line", json_numbert(id2string(first_location.get_line()))},
+     {"last line", json_numbert(id2string(last_location.get_line()))}});
+
+  dest.push_back(std::move(entry));
 }
 
 static void xml_output_function(

src/goto-diff/goto_diff_base.cpp

@@ -38,9 +38,9 @@ void goto_difft::output_functions() const
     }
     case ui_message_handlert::uit::JSON_UI:
     {
-      json_objectt json_result;
-      json_result["totalNumberOfFunctions"]=
-        json_stringt(std::to_string(total_functions_count));
+      json_objectt json_result(
+        {{"totalNumberOfFunctions",
+          json_stringt(std::to_string(total_functions_count))}});
       convert_function_group_json(
         json_result["newFunctions"].make_array(), new_functions, goto_model2);
       convert_function_group_json(

src/goto-instrument/unwind.cpp

@@ -336,15 +336,16 @@ jsont goto_unwindt::unwind_logt::output_log_json() const
   for(location_mapt::const_iterator it=location_map.begin();
       it!=location_map.end(); it++)
   {
-    json_objectt &object=json_unwound.push_back().make_object();
-
     goto_programt::const_targett target=it->first;
     unsigned location_number=it->second;
 
-    object["originalLocationNumber"]=json_numbert(std::to_string(
-      location_number));
-    object["newLocationNumber"]=json_numbert(std::to_string(
-      target->location_number));
+    json_objectt object(
+      {{"originalLocationNumber",
+        json_numbert(std::to_string(location_number))},
+       {"newLocationNumber",
+        json_numbert(std::to_string(target->location_number))}});
+
+    json_unwound.push_back(std::move(object));
   }
 
   return std::move(json_result);

src/goto-programs/goto_inline_class.cpp

@@ -881,26 +881,25 @@ jsont goto_inlinet::goto_inline_logt::output_inline_log_json() const
 
   for(const auto &it : log_map)
   {
-    json_objectt &object=json_inlined.push_back().make_object();
-
     goto_programt::const_targett start=it.first;
     const goto_inline_log_infot &info=it.second;
     goto_programt::const_targett end=info.end;
 
     PRECONDITION(start->location_number <= end->location_number);
 
-    object["call"]=json_numbert(std::to_string(info.call_location_number));
-    object["function"]=json_stringt(info.function.c_str());
+    json_arrayt json_orig(
+      {json_numbert(std::to_string(info.begin_location_number)),
+       json_numbert(std::to_string(info.end_location_number))});
+    json_arrayt json_new({json_numbert(std::to_string(start->location_number)),
+                          json_numbert(std::to_string(end->location_number))});
 
-    json_arrayt &json_orig=object["originalSegment"].make_array();
-    json_orig.push_back()=json_numbert(std::to_string(
-      info.begin_location_number));
-    json_orig.push_back()=json_numbert(std::to_string(
-      info.end_location_number));
+    json_objectt object(
+      {{"call", json_numbert(std::to_string(info.call_location_number))},
+       {"function", json_stringt(info.function.c_str())},
+       {"originalSegment", std::move(json_orig)},
+       {"inlinedSegment", std::move(json_new)}});
 
-    json_arrayt &json_new=object["inlinedSegment"].make_array();
-    json_new.push_back()=json_numbert(std::to_string(start->location_number));
-    json_new.push_back()=json_numbert(std::to_string(end->location_number));
+    json_inlined.push_back(std::move(object));
   }
 
   return std::move(json_result);

src/goto-programs/json_goto_trace.cpp

@@ -282,10 +282,10 @@ void convert_return(
                                                           : step.function;
 
   const symbolt &symbol = ns.lookup(function_identifier);
-  json_objectt &json_function = json_call_return["function"].make_object();
-  json_function["displayName"] = json_stringt(symbol.display_name());
-  json_function["identifier"] = json_stringt(function_identifier);
-  json_function["sourceLocation"] = json(symbol.location);
+  json_call_return["function"] =
+    json_objectt({{"displayName", json_stringt(symbol.display_name())},
+                  {"identifier", json_stringt(function_identifier)},
+                  {"sourceLocation", json(symbol.location)}});
 
   if(!location.is_null())
     json_call_return["sourceLocation"] = location;

src/goto-programs/loop_ids.cpp

@@ -88,9 +88,9 @@ void show_loop_ids_json(
       std::string id =
         id2string(function_identifier) + "." + std::to_string(loop_id);
 
-      json_objectt &loop=loops.push_back().make_object();
-      loop["name"]=json_stringt(id);
-      loop["sourceLocation"]=json(it->source_location);
+      loops.push_back(
+        json_objectt({{"name", json_stringt(id)},
+                      {"sourceLocation", json(it->source_location)}}));
     }
   }
 }

src/goto-programs/show_goto_functions_json.cpp

@@ -71,10 +71,8 @@ json_objectt show_goto_functions_jsont::convert(
       for(const goto_programt::instructiont &instruction :
         function.body.instructions)
       {
-        json_objectt instruction_entry=json_objectt();
-
-        instruction_entry["instructionId"]=
-          json_stringt(instruction.to_string());
+        json_objectt instruction_entry(
+          {{"instructionId", json_stringt(instruction.to_string())}});
 
         if(instruction.code.source_location().is_not_nil())
         {
@@ -99,7 +97,7 @@ json_objectt show_goto_functions_jsont::convert(
                 operand);
             operand_array.push_back(operand_object);
           }
-          instruction_entry["operands"]=operand_array;
+          instruction_entry["operands"] = std::move(operand_array);
         }
 
         if(!instruction.guard.is_true())
@@ -108,20 +106,17 @@ json_objectt show_goto_functions_jsont::convert(
             no_comments_irep_converter.convert_from_irep(
               instruction.guard);
 
-          instruction_entry["guard"]=guard_object;
+          instruction_entry["guard"] = std::move(guard_object);
         }
 
-        json_instruction_array.push_back(instruction_entry);
+        json_instruction_array.push_back(std::move(instruction_entry));
       }
 
-      json_function["instructions"]=json_instruction_array;
+      json_function["instructions"] = std::move(json_instruction_array);
     }
   }
 
-  json_objectt json_result;
-  json_result["functions"]=json_functions;
-
-  return json_result;
+  return json_objectt({{"functions", json_functions}});
 }
 
 /// Print the json object generated by