cprover
json_goto_trace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Traces of GOTO Programs
4 
5 Author: Daniel Kroening
6 
7  Date: November 2005
8 
9 \*******************************************************************/
10 
13 
14 #include "json_goto_trace.h"
15 #include "goto_trace.h"
16 
17 #include <util/json_expr.h>
18 #include <util/json.h>
19 #include <util/json_stream.h>
20 #include <util/arith_tools.h>
21 #include <util/config.h>
22 #include <util/invariant.h>
23 #include <util/simplify_expr.h>
24 #include <util/json_irep.h>
25 #include <langapi/language_util.h>
26 
35  json_objectt &json_failure,
36  const conversion_dependenciest &conversion_dependencies)
37 {
38  const goto_trace_stept &step = conversion_dependencies.step;
39  const jsont &location = conversion_dependencies.location;
40  const source_locationt &source_location =
41  conversion_dependencies.source_location;
42 
43  irep_idt property_id =
44  step.pc->is_assert()
45  ? source_location.get_property_id()
46  : step.pc->is_goto()
47  ? id2string(step.pc->source_location.get_function()) + ".unwind." +
48  std::to_string(step.pc->loop_number)
49  : "";
50 
51  json_failure["stepType"] = json_stringt("failure");
52  json_failure["hidden"] = jsont::json_boolean(step.hidden);
53  json_failure["internal"] = jsont::json_boolean(step.internal);
54  json_failure["thread"] = json_numbert(std::to_string(step.thread_nr));
55  json_failure["reason"] = json_stringt(step.comment);
56  json_failure["property"] = json_stringt(property_id);
57 
58  if(!location.is_null())
59  json_failure["sourceLocation"] = location;
60 }
61 
72  json_objectt &json_assignment,
73  const conversion_dependenciest &conversion_dependencies,
74  const trace_optionst &trace_options)
75 {
76  const goto_trace_stept &step = conversion_dependencies.step;
77  const jsont &json_location = conversion_dependencies.location;
78  const namespacet &ns = conversion_dependencies.ns;
79 
80  auto lhs_object=step.get_lhs_object();
81 
82  irep_idt identifier =
83  lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
84 
85  json_assignment["stepType"] = json_stringt("assignment");
86 
87  if(!json_location.is_null())
88  json_assignment["sourceLocation"] = json_location;
89 
90  std::string value_string, type_string, full_lhs_string;
91  json_objectt full_lhs_value;
92 
94  step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil");
95  exprt simplified = simplify_expr(step.full_lhs, ns);
96 
97  if(trace_options.json_full_lhs)
98  {
99  class comment_base_name_visitort : public expr_visitort
100  {
101  private:
102  const namespacet &ns;
103 
104  public:
105  explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
106  {
107  }
108 
109  void operator()(exprt &expr) override
110  {
111  if(expr.id() == ID_symbol)
112  {
113  const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
114 
115  if(expr.find(ID_C_base_name).is_not_nil())
116  INVARIANT(
117  expr.find(ID_C_base_name).id() == symbol.base_name,
118  "base_name comment does not match symbol's base_name");
119  else
120  expr.add(ID_C_base_name, irept(symbol.base_name));
121  }
122  }
123  };
124  comment_base_name_visitort comment_base_name_visitor(ns);
125  simplified.visit(comment_base_name_visitor);
126  }
127 
128  full_lhs_string = from_expr(ns, identifier, simplified);
129 
130  const symbolt *symbol;
131  irep_idt base_name, display_name;
132 
133  if(!ns.lookup(identifier, symbol))
134  {
135  base_name = symbol->base_name;
136  display_name = symbol->display_name();
137  if(type_string == "")
138  type_string = from_type(ns, identifier, symbol->type);
139 
140  json_assignment["mode"] = json_stringt(symbol->mode);
141  exprt simplified = simplify_expr(step.full_lhs_value, ns);
142 
143  full_lhs_value = json(simplified, ns, symbol->mode);
144  }
145  else
146  {
148  step.full_lhs_value.is_not_nil(),
149  "full_lhs_value in assignment must not be nil");
150  full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
151  }
152 
153  json_assignment["value"] = full_lhs_value;
154  json_assignment["lhs"] = json_stringt(full_lhs_string);
155  if(trace_options.json_full_lhs)
156  {
157  // Not language specific, still mangled, fully-qualified name of lhs
158  json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
159  }
160  json_assignment["hidden"] = jsont::json_boolean(step.hidden);
161  json_assignment["internal"] = jsont::json_boolean(step.internal);
162  json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr));
163 
164  json_assignment["assignmentType"] = json_stringt(
166  ? "actual-parameter"
167  : "variable");
168 }
169 
178  json_objectt &json_output,
179  const conversion_dependenciest &conversion_dependencies)
180 {
181  const goto_trace_stept &step = conversion_dependencies.step;
182  const jsont &location = conversion_dependencies.location;
183  const namespacet &ns = conversion_dependencies.ns;
184  const source_locationt &source_location = step.pc->source_location;
185 
186  json_output["stepType"] = json_stringt("output");
187  json_output["hidden"] = jsont::json_boolean(step.hidden);
188  json_output["internal"] = jsont::json_boolean(step.internal);
189  json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
190  json_output["outputID"] = json_stringt(step.io_id);
191 
192  // Recovering the mode from the function
193  irep_idt mode;
194  const symbolt *function_name;
195  if(ns.lookup(source_location.get_function(), function_name))
196  // Failed to find symbol
197  mode = ID_unknown;
198  else
199  mode = function_name->mode;
200  json_output["mode"] = json_stringt(mode);
201  json_arrayt &json_values = json_output["values"].make_array();
202 
203  for(const auto &arg : step.io_args)
204  {
205  arg.is_nil() ? json_values.push_back(json_stringt(""))
206  : json_values.push_back(json(arg, ns, mode));
207  }
208 
209  if(!location.is_null())
210  json_output["sourceLocation"] = location;
211 }
212 
221  json_objectt &json_input,
222  const conversion_dependenciest &conversion_dependencies)
223 {
224  const goto_trace_stept &step = conversion_dependencies.step;
225  const jsont &location = conversion_dependencies.location;
226  const namespacet &ns = conversion_dependencies.ns;
227  const source_locationt &source_location = step.pc->source_location;
228 
229  json_input["stepType"] = json_stringt("input");
230  json_input["hidden"] = jsont::json_boolean(step.hidden);
231  json_input["internal"] = jsont::json_boolean(step.internal);
232  json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
233  json_input["inputID"] = json_stringt(step.io_id);
234 
235  // Recovering the mode from the function
236  irep_idt mode;
237  const symbolt *function_name;
238  if(ns.lookup(source_location.get_function(), function_name))
239  // Failed to find symbol
240  mode = ID_unknown;
241  else
242  mode = function_name->mode;
243  json_input["mode"] = json_stringt(mode);
244  json_arrayt &json_values = json_input["values"].make_array();
245 
246  for(const auto &arg : step.io_args)
247  {
248  arg.is_nil() ? json_values.push_back(json_stringt(""))
249  : json_values.push_back(json(arg, ns, mode));
250  }
251 
252  if(!location.is_null())
253  json_input["sourceLocation"] = location;
254 }
255 
264  json_objectt &json_call_return,
265  const conversion_dependenciest &conversion_dependencies)
266 {
267  const goto_trace_stept &step = conversion_dependencies.step;
268  const jsont &location = conversion_dependencies.location;
269  const namespacet &ns = conversion_dependencies.ns;
270 
271  std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL)
272  ? "function-call"
273  : "function-return";
274 
275  json_call_return["stepType"] = json_stringt(tag);
276  json_call_return["hidden"] = jsont::json_boolean(step.hidden);
277  json_call_return["internal"] = jsont::json_boolean(step.internal);
278  json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
279 
280  const irep_idt &function_identifier =
282  : step.function;
283 
284  const symbolt &symbol = ns.lookup(function_identifier);
285  json_objectt &json_function = json_call_return["function"].make_object();
286  json_function["displayName"] = json_stringt(symbol.display_name());
287  json_function["identifier"] = json_stringt(function_identifier);
288  json_function["sourceLocation"] = json(symbol.location);
289 
290  if(!location.is_null())
291  json_call_return["sourceLocation"] = location;
292 }
293 
303  json_objectt &json_location_only,
304  const conversion_dependenciest &conversion_dependencies)
305 {
306  const goto_trace_stept &step = conversion_dependencies.step;
307  const jsont &location = conversion_dependencies.location;
308 
309  json_location_only["stepType"] = json_stringt("location-only");
310  json_location_only["hidden"] = jsont::json_boolean(step.hidden);
311  json_location_only["thread"] = json_numbert(std::to_string(step.thread_nr));
312  json_location_only["sourceLocation"] = location;
313 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
bool json_full_lhs
Definition: goto_trace.h:198
exprt simplify_expr(const exprt &src, const namespacet &ns)
irep_idt mode
Language mode.
Definition: symbol.h:49
io_argst io_args
Definition: goto_trace.h:116
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const irep_idt & get_function() const
Definition: json.h:23
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Traces of GOTO Programs.
static jsont json_boolean(bool value)
Definition: json.h:85
Symbol table entry.
Definition: symbol.h:27
TO_BE_DOCUMENTED.
Definition: goto_trace.h:30
goto_programt::const_targett pc
Definition: goto_trace.h:92
json_arrayt & make_array()
Definition: json.h:284
irep_idt called_function
Definition: goto_trace.h:120
jsont & push_back(const jsont &json)
Definition: json.h:163
irep_idt io_id
Definition: goto_trace.h:114
irep_idt function
Definition: goto_trace.h:91
const namespacet & ns
const irep_idt & id() const
Definition: irep.h:259
const source_locationt & source_location
Traces of GOTO Programs.
This is structure is here to facilitate passing arguments to the conversion functions.
Expressions in JSON.
unsigned thread_nr
Definition: goto_trace.h:95
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:42
Base class for tree-like data structures with sharing.
Definition: irep.h:156
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
const goto_trace_stept & step
bool is_null() const
Definition: json.h:69
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
void convert_input(json_objectt &json_input, const conversion_dependenciest &conversion_dependencies)
Convert an INPUT goto_trace step.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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:33
typet type
Type of symbol.
Definition: symbol.h:31
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
virtual void operator()(exprt &)
Definition: expr.h:325
void convert_decl(json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options)
Convert a DECL goto_trace step.
exprt full_lhs_value
Definition: goto_trace.h:111
void convert_default(json_objectt &json_location_only, const conversion_dependenciest &conversion_dependencies)
Convert all other types of steps not already handled by the other conversion functions.
irept & add(const irep_namet &name)
Definition: irep.cpp:305
std::string comment
Definition: goto_trace.h:102
json_objectt & make_object()
Definition: json.h:290
dstringt irep_idt
Definition: irep.h:32
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
const irep_idt & get_property_id() const
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void convert_return(json_objectt &json_call_return, const conversion_dependenciest &conversion_dependencies)
Convert a FUNCTION_RETURN goto_trace step.
assignment_typet assignment_type
Definition: goto_trace.h:87