Enable construction of JSON arrays and objects in place

tautschnig · tautschnig · commit 64df79edce7d · 2019-01-04T14:14:24.000Z
This enables RAII and gets us close to writing JSON in source code while still
being efficient.
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/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;
     }
diff --git a/src/analyses/ai.cpp b/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);
diff --git a/src/analyses/dependence_graph.cpp b/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);
diff --git a/src/cbmc/bmc.cpp b/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;
diff --git a/src/cbmc/bmc_cover.cpp b/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;
diff --git a/src/goto-analyzer/taint_analysis.cpp b/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
         {
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/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(
diff --git a/src/goto-diff/goto_diff_base.cpp b/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(
diff --git a/src/goto-instrument/unwind.cpp b/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);
diff --git a/src/goto-programs/goto_inline_class.cpp b/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);
diff --git a/src/goto-programs/json_goto_trace.cpp b/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;
diff --git a/src/goto-programs/loop_ids.cpp b/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)}}));
     }
   }
 }
diff --git a/src/goto-programs/show_goto_functions_json.cpp b/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
diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
diff --git a/src/util/json.h b/src/util/json.h
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp

Original file line number	Diff line number	Diff line change
`@@ -453,8 +453,7 @@ int jbmc_parse_optionst::doit()`
`453`	`453`	`break;`
`454`	`454`	`case ui_message_handlert::uit::JSON_UI:`
`455`	`455`	`{`
`456`		`- json_objectt json_options;`
`457`		`- json_options["options"] = options.to_json();`
	`456`	`+ json_objectt json_options({{"options", options.to_json()}});`
`458`	`457`	`debug() << json_options;`
`459`	`458`	`break;`
`460`	`459`	`}`
Original file line number	Diff line number	Diff line change
`@@ -176,8 +176,7 @@ void bmct::report_success(messaget &log, ui_message_handlert &handler)`
`176`	`176`
`177`	`177`	`case ui_message_handlert::uit::JSON_UI:`
`178`	`178`	`{`
`179`		`- json_objectt json_result;`
`180`		`- json_result["cProverStatus"]=json_stringt("success");`
	`179`	`+ json_objectt json_result({{"cProverStatus", json_stringt("success")}});`
`181`	`180`	`log.result() << json_result;`
`182`	`181`	`}`
`183`	`182`	`break;`
`@@ -208,8 +207,7 @@ void bmct::report_failure(messaget &log, ui_message_handlert &handler)`
`208`	`207`
`209`	`208`	`case ui_message_handlert::uit::JSON_UI:`
`210`	`209`	`{`
`211`		`- json_objectt json_result;`
`212`		`- json_result["cProverStatus"]=json_stringt("failure");`
	`210`	`+ json_objectt json_result({{"cProverStatus", json_stringt("failure")}});`
`213`	`211`	`log.result() << json_result;`
`214`	`212`	`}`
`215`	`213`	`break;`
Original file line number	Diff line number	Diff line change
`@@ -365,7 +365,6 @@ bool bmc_covert::operator()()`
`365`	`365`	`json_arrayt &tests_array=json_result["tests"].make_array();`
`366`	`366`	`for(const auto &test : tests)`
`367`	`367`	`{`
`368`		`- json_objectt &result=tests_array.push_back().make_object();`
`369`	`368`	`if(bmc.options.get_bool_option("trace"))`
`370`	`369`	`{`
`371`	`370`	`json_arrayt &json_trace = json_result["trace"].make_array();`
`@@ -379,20 +378,21 @@ bool bmc_covert::operator()()`
`379`	`378`	`{`
`380`	`379`	`if(step.is_input())`
`381`	`380`	`{`
`382`		`- json_objectt json_input;`
`383`		`- json_input["id"] = json_stringt(step.io_id);`
	`381`	`+ json_objectt json_input({{"id", json_stringt(step.io_id)}});`
`384`	`382`	`if(step.io_args.size()==1)`
`385`	`383`	`json_input["value"]=`
`386`	`384`	`json(step.io_args.front(), bmc.ns, ID_unknown);`
`387`		`- json_test.push_back(json_input);`
	`385`	`+ json_test.push_back(std::move(json_input));`
`388`	`386`	`}`
`389`	`387`	`}`
`390`	`388`	`}`
`391`		`- json_arrayt &goal_refs=result["coveredGoals"].make_array();`
	`389`	`+ json_arrayt goal_refs;`
`392`	`390`	`for(const auto &goal_id : test.covered_goals)`
`393`	`391`	`{`
`394`	`392`	`goal_refs.push_back(json_stringt(goal_id));`
`395`	`393`	`}`
	`394`	`+ tests_array.push_back(`
	`395`	`+ json_objectt({{"coveredGoals", std::move(goal_refs)}}));`
`396`	`396`	`}`
`397`	`397`
`398`	`398`	`break;`
Original file line number	Diff line number	Diff line change
`@@ -38,9 +38,9 @@ void goto_difft::output_functions() const`
`38`	`38`	`}`
`39`	`39`	`case ui_message_handlert::uit::JSON_UI:`
`40`	`40`	`{`
`41`		`- json_objectt json_result;`
`42`		`- json_result["totalNumberOfFunctions"]=`
`43`		`- json_stringt(std::to_string(total_functions_count));`
	`41`	`+ json_objectt json_result(`
	`42`	`+ {{"totalNumberOfFunctions",`
	`43`	`+ json_stringt(std::to_string(total_functions_count))}});`
`44`	`44`	`convert_function_group_json(`
`45`	`45`	`json_result["newFunctions"].make_array(), new_functions, goto_model2);`
`46`	`46`	`convert_function_group_json(`