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  irep_idt identifier = step.lhs_object.get_identifier();
81 
82  json_assignment["stepType"] = json_stringt("assignment");
83 
84  if(!json_location.is_null())
85  json_assignment["sourceLocation"] = json_location;
86 
87  std::string value_string, type_string, full_lhs_string;
88  json_objectt full_lhs_value;
89 
91  step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil");
92  exprt simplified = simplify_expr(step.full_lhs, ns);
93 
94  if(trace_options.json_full_lhs)
95  {
96  class comment_base_name_visitort : public expr_visitort
97  {
98  private:
99  const namespacet &ns;
100 
101  public:
102  explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
103  {
104  }
105 
106  void operator()(exprt &expr) override
107  {
108  if(expr.id() == ID_symbol)
109  {
110  const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
111 
112  if(expr.find(ID_C_base_name).is_not_nil())
113  INVARIANT(
114  expr.find(ID_C_base_name).id() == symbol.base_name,
115  "base_name comment does not match symbol's base_name");
116  else
117  expr.add(ID_C_base_name, irept(symbol.base_name));
118  }
119  }
120  };
121  comment_base_name_visitort comment_base_name_visitor(ns);
122  simplified.visit(comment_base_name_visitor);
123  }
124 
125  full_lhs_string = from_expr(ns, identifier, simplified);
126 
127  const symbolt *symbol;
128  irep_idt base_name, display_name;
129 
130  if(!ns.lookup(identifier, symbol))
131  {
132  base_name = symbol->base_name;
133  display_name = symbol->display_name();
134  if(type_string == "")
135  type_string = from_type(ns, identifier, symbol->type);
136 
137  json_assignment["mode"] = json_stringt(symbol->mode);
138  exprt simplified = simplify_expr(step.full_lhs_value, ns);
139 
140  full_lhs_value = json(simplified, ns, symbol->mode);
141  }
142  else
143  {
145  step.full_lhs_value.is_not_nil(),
146  "full_lhs_value in assignment must not be nil");
147  full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
148  }
149 
150  json_assignment["value"] = full_lhs_value;
151  json_assignment["lhs"] = json_stringt(full_lhs_string);
152  if(trace_options.json_full_lhs)
153  {
154  // Not language specific, still mangled, fully-qualified name of lhs
155  json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
156  }
157  json_assignment["hidden"] = jsont::json_boolean(step.hidden);
158  json_assignment["internal"] = jsont::json_boolean(step.internal);
159  json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr));
160 
161  json_assignment["assignmentType"] = json_stringt(
163  ? "actual-parameter"
164  : "variable");
165 }
166 
175  json_objectt &json_output,
176  const conversion_dependenciest &conversion_dependencies)
177 {
178  const goto_trace_stept &step = conversion_dependencies.step;
179  const jsont &location = conversion_dependencies.location;
180  const namespacet &ns = conversion_dependencies.ns;
181  const source_locationt &source_location = step.pc->source_location;
182 
183  json_output["stepType"] = json_stringt("output");
184  json_output["hidden"] = jsont::json_boolean(step.hidden);
185  json_output["internal"] = jsont::json_boolean(step.internal);
186  json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
187  json_output["outputID"] = json_stringt(step.io_id);
188 
189  // Recovering the mode from the function
190  irep_idt mode;
191  const symbolt *function_name;
192  if(ns.lookup(source_location.get_function(), function_name))
193  // Failed to find symbol
194  mode = ID_unknown;
195  else
196  mode = function_name->mode;
197  json_output["mode"] = json_stringt(mode);
198  json_arrayt &json_values = json_output["values"].make_array();
199 
200  for(const auto &arg : step.io_args)
201  {
202  arg.is_nil() ? json_values.push_back(json_stringt(""))
203  : json_values.push_back(json(arg, ns, mode));
204  }
205 
206  if(!location.is_null())
207  json_output["sourceLocation"] = location;
208 }
209 
218  json_objectt &json_input,
219  const conversion_dependenciest &conversion_dependencies)
220 {
221  const goto_trace_stept &step = conversion_dependencies.step;
222  const jsont &location = conversion_dependencies.location;
223  const namespacet &ns = conversion_dependencies.ns;
224  const source_locationt &source_location = step.pc->source_location;
225 
226  json_input["stepType"] = json_stringt("input");
227  json_input["hidden"] = jsont::json_boolean(step.hidden);
228  json_input["internal"] = jsont::json_boolean(step.internal);
229  json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
230  json_input["inputID"] = json_stringt(step.io_id);
231 
232  // Recovering the mode from the function
233  irep_idt mode;
234  const symbolt *function_name;
235  if(ns.lookup(source_location.get_function(), function_name))
236  // Failed to find symbol
237  mode = ID_unknown;
238  else
239  mode = function_name->mode;
240  json_input["mode"] = json_stringt(mode);
241  json_arrayt &json_values = json_input["values"].make_array();
242 
243  for(const auto &arg : step.io_args)
244  {
245  arg.is_nil() ? json_values.push_back(json_stringt(""))
246  : json_values.push_back(json(arg, ns, mode));
247  }
248 
249  if(!location.is_null())
250  json_input["sourceLocation"] = location;
251 }
252 
261  json_objectt &json_call_return,
262  const conversion_dependenciest &conversion_dependencies)
263 {
264  const goto_trace_stept &step = conversion_dependencies.step;
265  const jsont &location = conversion_dependencies.location;
266  const namespacet &ns = conversion_dependencies.ns;
267 
268  std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL)
269  ? "function-call"
270  : "function-return";
271 
272  json_call_return["stepType"] = json_stringt(tag);
273  json_call_return["hidden"] = jsont::json_boolean(step.hidden);
274  json_call_return["internal"] = jsont::json_boolean(step.internal);
275  json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
276 
277  const symbolt &symbol = ns.lookup(step.identifier);
278  json_objectt &json_function = json_call_return["function"].make_object();
279  json_function["displayName"] = json_stringt(symbol.display_name());
280  json_function["identifier"] = json_stringt(step.identifier);
281  json_function["sourceLocation"] = json(symbol.location);
282 
283  if(!location.is_null())
284  json_call_return["sourceLocation"] = location;
285 }
286 
296  json_objectt &json_location_only,
297  const conversion_dependenciest &conversion_dependencies)
298 {
299  const goto_trace_stept &step = conversion_dependencies.step;
300  const jsont &location = conversion_dependencies.location;
301 
302  json_location_only["stepType"] = json_stringt("location-only");
303  json_location_only["hidden"] = jsont::json_boolean(step.hidden);
304  json_location_only["thread"] = json_numbert(std::to_string(step.thread_nr));
305  json_location_only["sourceLocation"] = location;
306 }
virtual void operator()(exprt &expr)
Definition: expr.h:165
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
bool json_full_lhs
Definition: goto_trace.h:213
exprt simplify_expr(const exprt &src, const namespacet &ns)
irep_idt mode
Language mode.
Definition: symbol.h:52
io_argst io_args
Definition: goto_trace.h:119
const irep_idt & get_function() const
const irep_idt & get_identifier() const
Definition: std_expr.h:128
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.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
TO_BE_DOCUMENTED.
Definition: goto_trace.h:36
goto_programt::const_targett pc
Definition: goto_trace.h:95
json_arrayt & make_array()
Definition: json.h:284
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
jsont & push_back(const jsont &json)
Definition: json.h:163
irep_idt io_id
Definition: goto_trace.h:117
const namespacet & ns
const irep_idt & id() const
Definition: irep.h:189
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:98
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Base class for tree-like data structures with sharing.
Definition: irep.h:86
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const goto_trace_stept & step
bool is_null() const
Definition: json.h:69
irep_idt identifier
Definition: goto_trace.h:123
void convert_assert(json_objectt &json_failure, const conversion_dependenciest &conversion_dependencies)
Convert an ASSERT goto_trace step.
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
Definition: symbol.h:57
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:32
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
ssa_exprt lhs_object
Definition: goto_trace.h:108
void convert_decl(json_objectt &json_assignment, const conversion_dependenciest &conversion_dependencies, const trace_optionst &trace_options)
Convert a DECL goto_trace step.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
exprt full_lhs_value
Definition: goto_trace.h:114
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:306
std::string comment
Definition: goto_trace.h:105
json_objectt & make_object()
Definition: json.h:290
void convert_output(json_objectt &json_output, const conversion_dependenciest &conversion_dependencies)
Convert an OUTPUT goto_trace step.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
const irep_idt & get_property_id() const
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
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:93