cprover
Loading...
Searching...
No Matches
json_goto_trace.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs
4
5Author: Daniel Kroening
6
7 Date: November 2005
8
9\*******************************************************************/
10
13
14#include "json_goto_trace.h"
15
16#include <util/invariant.h>
17#include <util/simplify_expr.h>
18#include <util/symbol.h>
19
21
22#include "goto_trace.h"
23#include "json_expr.h"
24
33 json_objectt &json_failure,
34 const conversion_dependenciest &conversion_dependencies)
35{
36 const goto_trace_stept &step = conversion_dependencies.step;
37 const jsont &location = conversion_dependencies.location;
38
39 json_failure["stepType"] = json_stringt("failure");
40 json_failure["hidden"] = jsont::json_boolean(step.hidden);
41 json_failure["internal"] = jsont::json_boolean(step.internal);
42 json_failure["thread"] = json_numbert(std::to_string(step.thread_nr));
43 json_failure["reason"] = json_stringt(step.comment);
44 json_failure["property"] = json_stringt(step.property_id);
45
46 if(!location.is_null())
47 json_failure["sourceLocation"] = location;
48}
49
60 json_objectt &json_assignment,
61 const conversion_dependenciest &conversion_dependencies,
62 const trace_optionst &trace_options)
63{
64 const goto_trace_stept &step = conversion_dependencies.step;
65 const jsont &json_location = conversion_dependencies.location;
66 const namespacet &ns = conversion_dependencies.ns;
67
68 auto lhs_object=step.get_lhs_object();
69
70 irep_idt identifier =
71 lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
72
73 json_assignment["stepType"] = json_stringt("assignment");
74
75 if(!json_location.is_null())
76 json_assignment["sourceLocation"] = json_location;
77
78 std::string value_string, type_string, full_lhs_string;
80
82 step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil");
83 exprt simplified = simplify_expr(step.full_lhs, ns);
84
85 if(trace_options.json_full_lhs)
86 {
87 class comment_base_name_visitort : public expr_visitort
88 {
89 private:
90 const namespacet &ns;
91
92 public:
93 explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
94 {
95 }
96
97 void operator()(exprt &expr) override
98 {
99 if(expr.id() == ID_symbol)
100 {
101 const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
102
103 if(expr.find(ID_C_base_name).is_not_nil())
104 INVARIANT(
105 expr.find(ID_C_base_name).id() == symbol.base_name,
106 "base_name comment does not match symbol's base_name");
107 else
108 expr.add(ID_C_base_name, irept(symbol.base_name));
109 }
110 }
111 };
112 comment_base_name_visitort comment_base_name_visitor(ns);
113 simplified.visit(comment_base_name_visitor);
114 }
115
116 full_lhs_string = from_expr(ns, identifier, simplified);
117
118 const symbolt *symbol;
119 irep_idt base_name, display_name;
120
123 "full_lhs_value in assignment must not be nil");
124
125 if(!ns.lookup(identifier, symbol))
126 {
127 base_name = symbol->base_name;
128 display_name = symbol->display_name();
129 if(type_string.empty())
130 type_string = from_type(ns, identifier, symbol->type);
131
132 json_assignment["mode"] = json_stringt(symbol->mode);
133 const exprt simplified_expr = simplify_expr(step.full_lhs_value, ns);
134
135 full_lhs_value = json(simplified_expr, ns, symbol->mode);
136 }
137 else
138 {
139 full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
140 }
141
142 json_assignment["value"] = full_lhs_value;
143 json_assignment["lhs"] = json_stringt(full_lhs_string);
144 if(trace_options.json_full_lhs)
145 {
146 // Not language specific, still mangled, fully-qualified name of lhs
147 json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
148 }
149 json_assignment["hidden"] = jsont::json_boolean(step.hidden);
150 json_assignment["internal"] = jsont::json_boolean(step.internal);
151 json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr));
152
153 json_assignment["assignmentType"] = json_stringt(
155 ? "actual-parameter"
156 : "variable");
157}
158
167 json_objectt &json_output,
168 const conversion_dependenciest &conversion_dependencies)
169{
170 const goto_trace_stept &step = conversion_dependencies.step;
171 const jsont &location = conversion_dependencies.location;
172 const namespacet &ns = conversion_dependencies.ns;
173
174 json_output["stepType"] = json_stringt("output");
175 json_output["hidden"] = jsont::json_boolean(step.hidden);
176 json_output["internal"] = jsont::json_boolean(step.internal);
177 json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
178 json_output["outputID"] = json_stringt(step.io_id);
179
180 // Recovering the mode from the function
181 irep_idt mode;
182 const symbolt *function_name;
183 if(ns.lookup(step.function_id, function_name))
184 // Failed to find symbol
185 mode = ID_unknown;
186 else
187 mode = function_name->mode;
188 json_output["mode"] = json_stringt(mode);
189 json_arrayt &json_values = json_output["values"].make_array();
190
191 for(const auto &arg : step.io_args)
192 {
193 arg.is_nil() ? json_values.push_back(json_stringt(""))
194 : json_values.push_back(json(arg, ns, mode));
195 }
196
197 if(!location.is_null())
198 json_output["sourceLocation"] = location;
199}
200
209 json_objectt &json_input,
210 const conversion_dependenciest &conversion_dependencies)
211{
212 const goto_trace_stept &step = conversion_dependencies.step;
213 const jsont &location = conversion_dependencies.location;
214 const namespacet &ns = conversion_dependencies.ns;
215
216 json_input["stepType"] = json_stringt("input");
217 json_input["hidden"] = jsont::json_boolean(step.hidden);
218 json_input["internal"] = jsont::json_boolean(step.internal);
219 json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
220 json_input["inputID"] = json_stringt(step.io_id);
221
222 // Recovering the mode from the function
223 irep_idt mode;
224 const symbolt *function_name;
225 if(ns.lookup(step.function_id, function_name))
226 // Failed to find symbol
227 mode = ID_unknown;
228 else
229 mode = function_name->mode;
230 json_input["mode"] = json_stringt(mode);
231 json_arrayt &json_values = json_input["values"].make_array();
232
233 for(const auto &arg : step.io_args)
234 {
235 arg.is_nil() ? json_values.push_back(json_stringt(""))
236 : json_values.push_back(json(arg, ns, mode));
237 }
238
239 if(!location.is_null())
240 json_input["sourceLocation"] = location;
241}
242
251 json_objectt &json_call_return,
252 const conversion_dependenciest &conversion_dependencies)
253{
254 const goto_trace_stept &step = conversion_dependencies.step;
255 const jsont &location = conversion_dependencies.location;
256 const namespacet &ns = conversion_dependencies.ns;
257
258 std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL)
259 ? "function-call"
260 : "function-return";
261
262 json_call_return["stepType"] = json_stringt(tag);
263 json_call_return["hidden"] = jsont::json_boolean(step.hidden);
264 json_call_return["internal"] = jsont::json_boolean(step.internal);
265 json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
266
267 const irep_idt &function_identifier = step.called_function;
268
269 const symbolt &symbol = ns.lookup(function_identifier);
270 json_call_return["function"] =
271 json_objectt({{"displayName", json_stringt(symbol.display_name())},
272 {"identifier", json_stringt(function_identifier)},
273 {"sourceLocation", json(symbol.location)}});
274
275 if(!location.is_null())
276 json_call_return["sourceLocation"] = location;
277}
278
280 json_objectt &json_location_only,
282{
283 json_location_only["stepType"] =
285 json_location_only["hidden"] = jsont::json_boolean(default_step.hidden);
286 json_location_only["thread"] =
287 json_numbert(std::to_string(default_step.thread_number));
288 json_location_only["sourceLocation"] = json(default_step.location);
289}
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
virtual void operator()(exprt &)
Definition expr.h:369
Base class for all expressions.
Definition expr.h:54
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
Definition expr.cpp:255
Step of the trace of a GOTO program.
Definition goto_trace.h:50
optionalt< symbol_exprt > get_lhs_object() const
std::string comment
Definition goto_trace.h:123
irep_idt function_id
Definition goto_trace.h:111
unsigned thread_nr
Definition goto_trace.h:115
irep_idt property_id
Definition goto_trace.h:122
irep_idt called_function
Definition goto_trace.h:141
assignment_typet assignment_type
Definition goto_trace.h:107
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:106
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:116
jsont & push_back(const jsont &json)
Definition json.h:212
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
Definition json_irep.cpp:31
Definition json.h:27
json_arrayt & make_array()
Definition json.h:420
bool is_null() const
Definition json.h:81
static jsont json_boolean(bool value)
Definition json.h:97
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
irep_idt mode
Language mode.
Definition symbol.h:49
Traces of GOTO Programs.
dstringt irep_idt
Definition irep.h:37
Expressions in JSON.
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
void convert_decl(json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options)
Convert a DECL goto_trace step.
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
void convert_default(json_objectt &json_location_only, const default_trace_stept &default_step)
Convert all other types of steps not already handled by the other conversion functions.
Traces of GOTO Programs.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
This is structure is here to facilitate passing arguments to the conversion functions.
const goto_trace_stept & step
const namespacet & ns
Options for printing the trace using show_goto_trace.
Definition goto_trace.h:219
bool json_full_lhs
Add rawLhs property to trace.
Definition goto_trace.h:221
std::string default_step_name(const default_step_kindt &step_type)
Turns a default_step_kindt into a string that can be used in the trace.
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Symbol table entry.
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)