Skip to content

Commit 0a37dd9

Browse files
peterschrammelpeterschrammel
committed
Use JSON streaming
1 parent 3a1cfd4 commit 0a37dd9

File tree

6 files changed

+289
-295
lines changed

6 files changed

+289
-295
lines changed

‎src/cbmc/all_properties.cpp

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -206,24 +206,23 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
206206

207207
case ui_message_handlert::uit::JSON_UI:
208208
{
209-
json_objectt json_result;
210-
json_arrayt &result_array=json_result["result"].make_array();
209+
json_stream_objectt &json_result = result().json_stream().push_back_stream_object();
210+
json_stream_arrayt &result_array =
211+
json_result.push_back_stream_array("result");
211212

212213
for(const auto &g : goal_map)
213214
{
214-
json_objectt &result=result_array.push_back().make_object();
215+
json_stream_objectt &result=result_array.push_back_stream_object();
215216
result["property"]=json_stringt(id2string(g.first));
216217
result["description"]=json_stringt(id2string(g.second.description));
217218
result["status"]=json_stringt(g.second.status_string());
218219

219220
if(g.second.status==goalt::statust::FAILURE)
220221
{
221-
jsont &json_trace=result["trace"];
222-
convert(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
222+
json_stream_arrayt &json_trace=result.push_back_stream_array("trace");
223+
convert<json_stream_arrayt>(bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
223224
}
224225
}
225-
226-
result() << json_result;
227226
}
228227
break;
229228
}

‎src/cbmc/bmc.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include <util/time_stopping.h>
2222
#include <util/message.h>
2323
#include <util/json.h>
24+
#include <util/json_stream.h>
2425
#include <util/cprover_prefix.h>
2526

2627
#include <langapi/mode.h>
@@ -81,18 +82,15 @@ void bmct::error_trace()
8182

8283
case ui_message_handlert::uit::JSON_UI:
8384
{
84-
json_objectt json;
85-
json_arrayt &result_array=json["results"].make_array();
86-
json_objectt &json_result=result_array.push_back().make_object();
85+
json_stream_objectt &json_result = status().json_stream().push_back_stream_object();
8786
const goto_trace_stept &step=goto_trace.steps.back();
8887
json_result["property"]=
8988
json_stringt(id2string(step.pc->source_location.get_property_id()));
9089
json_result["description"]=
9190
json_stringt(id2string(step.pc->source_location.get_comment()));
9291
json_result["status"]=json_stringt("failed");
93-
jsont &json_trace=json_result["trace"];
94-
convert(ns, goto_trace, json_trace, trace_options());
95-
status() << json_result;
92+
json_stream_arrayt &json_trace=json_result.push_back_stream_array("trace");
93+
convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options());
9694
}
9795
break;
9896
}

‎src/cbmc/bmc_cover.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -369,7 +369,7 @@ bool bmc_covert::operator()()
369369
json_objectt &result=tests_array.push_back().make_object();
370370
if(bmc.options.get_bool_option("trace"))
371371
{
372-
jsont &json_trace=result["trace"];
372+
json_arrayt &json_trace=result["trace"].make_array();
373373
convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
374374
}
375375
else

‎src/goto-programs/interpreter.cpp

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ Author: Daniel Kroening, [email protected]
2828
#include <json/json_parser.h>
2929

3030
#include "interpreter_class.h"
31+
#include "json_goto_trace.h"
3132
#include "remove_returns.h"
3233

3334
const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
@@ -150,8 +151,8 @@ void interpretert::command()
150151
}
151152
else if(ch=='j')
152153
{
153-
jsont json_steps;
154-
convert(ns, steps, json_steps);
154+
json_arrayt json_steps;
155+
convert<json_arrayt>(ns, steps, json_steps);
155156
ch=tolower(command[1]);
156157
if(ch==' ')
157158
{

‎src/goto-programs/json_goto_trace.cpp

Lines changed: 0 additions & 275 deletions
Original file line numberDiff line numberDiff line change
@@ -11,279 +11,4 @@ Author: Daniel Kroening
1111
/// \file
1212
/// Traces of GOTO Programs
1313

14-
#include "json_goto_trace.h"
1514

16-
#include <util/json_expr.h>
17-
#include <util/arith_tools.h>
18-
#include <util/config.h>
19-
#include <util/invariant.h>
20-
#include <util/simplify_expr.h>
21-
22-
#include <langapi/language_util.h>
23-
#include <util/json_irep.h>
24-
25-
/// Produce a json representation of a trace.
26-
/// \param ns: a namespace
27-
/// \param goto_trace: a trace in a goto program
28-
/// \param dest: referecence to a json object in which the goto trace will be
29-
/// added
30-
void convert(
31-
const namespacet &ns,
32-
const goto_tracet &goto_trace,
33-
jsont &dest,
34-
trace_optionst trace_options)
35-
{
36-
json_arrayt &dest_array=dest.make_array();
37-
38-
source_locationt previous_source_location;
39-
40-
for(const auto &step : goto_trace.steps)
41-
{
42-
const source_locationt &source_location=step.pc->source_location;
43-
44-
jsont json_location;
45-
46-
if(source_location.is_not_nil() && source_location.get_file()!="")
47-
json_location=json(source_location);
48-
else
49-
json_location=json_nullt();
50-
51-
switch(step.type)
52-
{
53-
case goto_trace_stept::typet::ASSERT:
54-
if(!step.cond_value)
55-
{
56-
irep_idt property_id;
57-
58-
if(step.pc->is_assert())
59-
property_id=source_location.get_property_id();
60-
else if(step.pc->is_goto()) // unwinding, we suspect
61-
{
62-
property_id=
63-
id2string(step.pc->source_location.get_function())+
64-
".unwind."+std::to_string(step.pc->loop_number);
65-
}
66-
67-
json_objectt &json_failure=dest_array.push_back().make_object();
68-
69-
json_failure["stepType"]=json_stringt("failure");
70-
json_failure["hidden"]=jsont::json_boolean(step.hidden);
71-
json_failure["internal"]=jsont::json_boolean(step.internal);
72-
json_failure["thread"]=json_numbert(std::to_string(step.thread_nr));
73-
json_failure["reason"]=json_stringt(id2string(step.comment));
74-
json_failure["property"]=json_stringt(id2string(property_id));
75-
76-
if(!json_location.is_null())
77-
json_failure["sourceLocation"]=json_location;
78-
}
79-
break;
80-
81-
case goto_trace_stept::typet::ASSIGNMENT:
82-
case goto_trace_stept::typet::DECL:
83-
{
84-
irep_idt identifier=step.lhs_object.get_identifier();
85-
json_objectt &json_assignment=dest_array.push_back().make_object();
86-
87-
json_assignment["stepType"]=json_stringt("assignment");
88-
89-
if(!json_location.is_null())
90-
json_assignment["sourceLocation"]=json_location;
91-
92-
std::string value_string, binary_string, type_string, full_lhs_string;
93-
json_objectt full_lhs_value;
94-
95-
DATA_INVARIANT(
96-
step.full_lhs.is_not_nil(),
97-
"full_lhs in assignment must not be nil");
98-
exprt simplified=simplify_expr(step.full_lhs, ns);
99-
100-
if(trace_options.json_full_lhs)
101-
{
102-
class comment_base_name_visitort : public expr_visitort
103-
{
104-
private:
105-
const namespacet &ns;
106-
107-
public:
108-
explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
109-
{
110-
}
111-
112-
void operator()(exprt &expr) override
113-
{
114-
if(expr.id() == ID_symbol)
115-
{
116-
const symbolt &symbol = ns.lookup(expr.get(ID_identifier));
117-
if(expr.find(ID_C_base_name).is_not_nil())
118-
INVARIANT(
119-
expr.find(ID_C_base_name).id() == symbol.base_name,
120-
"base_name comment does not match symbol's base_name");
121-
else
122-
expr.add(ID_C_base_name, irept(symbol.base_name));
123-
}
124-
}
125-
};
126-
comment_base_name_visitort comment_base_name_visitor(ns);
127-
simplified.visit(comment_base_name_visitor);
128-
}
129-
130-
full_lhs_string=from_expr(ns, identifier, simplified);
131-
132-
const symbolt *symbol;
133-
irep_idt base_name, display_name;
134-
135-
if(!ns.lookup(identifier, symbol))
136-
{
137-
base_name=symbol->base_name;
138-
display_name=symbol->display_name();
139-
if(type_string=="")
140-
type_string=from_type(ns, identifier, symbol->type);
141-
142-
json_assignment["mode"]=json_stringt(id2string(symbol->mode));
143-
exprt simplified=simplify_expr(step.full_lhs_value, ns);
144-
145-
full_lhs_value=json(simplified, ns, symbol->mode);
146-
}
147-
else
148-
{
149-
DATA_INVARIANT(
150-
step.full_lhs_value.is_not_nil(),
151-
"full_lhs_value in assignment must not be nil");
152-
full_lhs_value=json(step.full_lhs_value, ns, ID_unknown);
153-
}
154-
155-
json_assignment["value"]=full_lhs_value;
156-
json_assignment["lhs"]=json_stringt(full_lhs_string);
157-
if(trace_options.json_full_lhs)
158-
{
159-
// Not language specific, still mangled, fully-qualified name of lhs
160-
json_assignment["rawLhs"] =
161-
json_irept(true).convert_from_irep(simplified);
162-
}
163-
json_assignment["hidden"]=jsont::json_boolean(step.hidden);
164-
json_assignment["internal"]=jsont::json_boolean(step.internal);
165-
json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));
166-
167-
json_assignment["assignmentType"]=
168-
json_stringt(
169-
step.assignment_type==
170-
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER?
171-
"actual-parameter":
172-
"variable");
173-
}
174-
break;
175-
176-
case goto_trace_stept::typet::OUTPUT:
177-
{
178-
json_objectt &json_output=dest_array.push_back().make_object();
179-
180-
json_output["stepType"]=json_stringt("output");
181-
json_output["hidden"]=jsont::json_boolean(step.hidden);
182-
json_output["internal"]=jsont::json_boolean(step.internal);
183-
json_output["thread"]=json_numbert(std::to_string(step.thread_nr));
184-
json_output["outputID"]=json_stringt(id2string(step.io_id));
185-
186-
// Recovering the mode from the function
187-
irep_idt mode;
188-
const symbolt *function_name;
189-
if(ns.lookup(source_location.get_function(), function_name))
190-
// Failed to find symbol
191-
mode=ID_unknown;
192-
else
193-
mode=function_name->mode;
194-
json_output["mode"]=json_stringt(id2string(mode));
195-
json_arrayt &json_values=json_output["values"].make_array();
196-
197-
for(const auto &arg : step.io_args)
198-
{
199-
if(arg.is_nil())
200-
json_values.push_back(json_stringt(""));
201-
else
202-
json_values.push_back(json(arg, ns, mode));
203-
}
204-
205-
if(!json_location.is_null())
206-
json_output["sourceLocation"]=json_location;
207-
}
208-
break;
209-
210-
case goto_trace_stept::typet::INPUT:
211-
{
212-
json_objectt &json_input=dest_array.push_back().make_object();
213-
214-
json_input["stepType"]=json_stringt("input");
215-
json_input["hidden"]=jsont::json_boolean(step.hidden);
216-
json_input["internal"]=jsont::json_boolean(step.internal);
217-
json_input["thread"]=json_numbert(std::to_string(step.thread_nr));
218-
json_input["inputID"]=json_stringt(id2string(step.io_id));
219-
220-
// Recovering the mode from the function
221-
irep_idt mode;
222-
const symbolt *function_name;
223-
if(ns.lookup(source_location.get_function(), function_name))
224-
// Failed to find symbol
225-
mode=ID_unknown;
226-
else
227-
mode=function_name->mode;
228-
json_input["mode"]=json_stringt(id2string(mode));
229-
json_arrayt &json_values=json_input["values"].make_array();
230-
231-
for(const auto &arg : step.io_args)
232-
{
233-
if(arg.is_nil())
234-
json_values.push_back(json_stringt(""));
235-
else
236-
json_values.push_back(json(arg, ns, mode));
237-
}
238-
239-
if(!json_location.is_null())
240-
json_input["sourceLocation"]=json_location;
241-
}
242-
break;
243-
244-
case goto_trace_stept::typet::FUNCTION_CALL:
245-
case goto_trace_stept::typet::FUNCTION_RETURN:
246-
{
247-
std::string tag=
248-
(step.type==goto_trace_stept::typet::FUNCTION_CALL)?
249-
"function-call":"function-return";
250-
json_objectt &json_call_return=dest_array.push_back().make_object();
251-
252-
json_call_return["stepType"]=json_stringt(tag);
253-
json_call_return["hidden"]=jsont::json_boolean(step.hidden);
254-
json_call_return["internal"]=jsont::json_boolean(step.internal);
255-
json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr));
256-
257-
const symbolt &symbol=ns.lookup(step.identifier);
258-
json_objectt &json_function=json_call_return["function"].make_object();
259-
json_function["displayName"]=
260-
json_stringt(id2string(symbol.display_name()));
261-
json_function["identifier"]=json_stringt(id2string(step.identifier));
262-
json_function["sourceLocation"]=json(symbol.location);
263-
264-
if(!json_location.is_null())
265-
json_call_return["sourceLocation"]=json_location;
266-
}
267-
break;
268-
269-
default:
270-
if(source_location!=previous_source_location)
271-
{
272-
// just the source location
273-
if(!json_location.is_null())
274-
{
275-
json_objectt &json_location_only=dest_array.push_back().make_object();
276-
json_location_only["stepType"]=json_stringt("location-only");
277-
json_location_only["hidden"]=jsont::json_boolean(step.hidden);
278-
json_location_only["internal"]=jsont::json_boolean(step.internal);
279-
json_location_only["thread"]=
280-
json_numbert(std::to_string(step.thread_nr));
281-
json_location_only["sourceLocation"]=json_location;
282-
}
283-
}
284-
}
285-
286-
if(source_location.is_not_nil() && source_location.get_file()!="")
287-
previous_source_location=source_location;
288-
}
289-
}

0 commit comments

Comments
 (0)