CBMC
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 
16 #include <util/invariant.h>
17 #include <util/namespace.h>
18 #include <util/simplify_expr.h>
19 #include <util/symbol.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "goto_trace.h"
24 #include "json_expr.h"
25 
34  json_objectt &json_failure,
35  const conversion_dependenciest &conversion_dependencies)
36 {
37  const goto_trace_stept &step = conversion_dependencies.step;
38  const jsont &location = conversion_dependencies.location;
39 
40  json_failure["stepType"] = json_stringt("failure");
41  json_failure["hidden"] = jsont::json_boolean(step.hidden);
42  json_failure["internal"] = jsont::json_boolean(step.internal);
43  json_failure["thread"] = json_numbert(std::to_string(step.thread_nr));
44  json_failure["reason"] = json_stringt(step.comment);
45  json_failure["property"] = json_stringt(step.property_id);
46 
47  if(!location.is_null())
48  json_failure["sourceLocation"] = location;
49 }
50 
61  json_objectt &json_assignment,
62  const conversion_dependenciest &conversion_dependencies,
63  const trace_optionst &trace_options)
64 {
65  const goto_trace_stept &step = conversion_dependencies.step;
66  const jsont &json_location = conversion_dependencies.location;
67  const namespacet &ns = conversion_dependencies.ns;
68 
69  auto lhs_object=step.get_lhs_object();
70 
71  irep_idt identifier =
72  lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
73 
74  json_assignment["stepType"] = json_stringt("assignment");
75 
76  if(!json_location.is_null())
77  json_assignment["sourceLocation"] = json_location;
78 
79  std::string value_string, type_string, full_lhs_string;
81 
83  step.full_lhs.is_not_nil(), "full_lhs in assignment must not be nil");
84  exprt simplified = simplify_expr(step.full_lhs, ns);
85 
86  if(trace_options.json_full_lhs)
87  {
88  class comment_base_name_visitort : public expr_visitort
89  {
90  private:
91  const namespacet &ns;
92 
93  public:
94  explicit comment_base_name_visitort(const namespacet &ns) : ns(ns)
95  {
96  }
97 
98  void operator()(exprt &expr) override
99  {
100  if(expr.id() == ID_symbol)
101  {
102  const symbolt &symbol = ns.lookup(to_symbol_expr(expr));
103 
104  if(expr.find(ID_C_base_name).is_not_nil())
105  INVARIANT(
106  expr.find(ID_C_base_name).id() == symbol.base_name,
107  "base_name comment does not match symbol's base_name");
108  else
109  expr.add(ID_C_base_name, irept(symbol.base_name));
110  }
111  }
112  };
113  comment_base_name_visitort comment_base_name_visitor(ns);
114  simplified.visit(comment_base_name_visitor);
115  }
116 
117  full_lhs_string = from_expr(ns, identifier, simplified);
118 
119  const symbolt *symbol;
120  irep_idt base_name, display_name;
121 
123  step.full_lhs_value.is_not_nil(),
124  "full_lhs_value in assignment must not be nil");
125 
126  if(!ns.lookup(identifier, symbol))
127  {
128  base_name = symbol->base_name;
129  display_name = symbol->display_name();
130  if(type_string.empty())
131  type_string = from_type(ns, identifier, symbol->type);
132 
133  json_assignment["mode"] = json_stringt(symbol->mode);
134  const exprt simplified_expr = simplify_expr(step.full_lhs_value, ns);
135 
136  full_lhs_value = json(simplified_expr, ns, symbol->mode);
137  }
138  else
139  {
140  full_lhs_value = json(step.full_lhs_value, ns, ID_unknown);
141  }
142 
143  json_assignment["value"] = full_lhs_value;
144  json_assignment["lhs"] = json_stringt(full_lhs_string);
145  if(trace_options.json_full_lhs)
146  {
147  // Not language specific, still mangled, fully-qualified name of lhs
148  json_assignment["rawLhs"] = json_irept(true).convert_from_irep(simplified);
149  }
150  json_assignment["hidden"] = jsont::json_boolean(step.hidden);
151  json_assignment["internal"] = jsont::json_boolean(step.internal);
152  json_assignment["thread"] = json_numbert(std::to_string(step.thread_nr));
153 
154  json_assignment["assignmentType"] = json_stringt(
156  ? "actual-parameter"
157  : "variable");
158 }
159 
168  json_objectt &json_output,
169  const conversion_dependenciest &conversion_dependencies)
170 {
171  const goto_trace_stept &step = conversion_dependencies.step;
172  const jsont &location = conversion_dependencies.location;
173  const namespacet &ns = conversion_dependencies.ns;
174 
175  json_output["stepType"] = json_stringt("output");
176  json_output["hidden"] = jsont::json_boolean(step.hidden);
177  json_output["internal"] = jsont::json_boolean(step.internal);
178  json_output["thread"] = json_numbert(std::to_string(step.thread_nr));
179  json_output["outputID"] = json_stringt(step.io_id);
180 
181  // Recovering the mode from the function
182  irep_idt mode;
183  const symbolt *function_name;
184  if(ns.lookup(step.function_id, function_name))
185  // Failed to find symbol
186  mode = ID_unknown;
187  else
188  mode = function_name->mode;
189  json_output["mode"] = json_stringt(mode);
190  json_arrayt &json_values = json_output["values"].make_array();
191 
192  for(const auto &arg : step.io_args)
193  {
194  arg.is_nil() ? json_values.push_back(json_stringt(""))
195  : json_values.push_back(json(arg, ns, mode));
196  }
197 
198  if(!location.is_null())
199  json_output["sourceLocation"] = location;
200 }
201 
210  json_objectt &json_input,
211  const conversion_dependenciest &conversion_dependencies)
212 {
213  const goto_trace_stept &step = conversion_dependencies.step;
214  const jsont &location = conversion_dependencies.location;
215  const namespacet &ns = conversion_dependencies.ns;
216 
217  json_input["stepType"] = json_stringt("input");
218  json_input["hidden"] = jsont::json_boolean(step.hidden);
219  json_input["internal"] = jsont::json_boolean(step.internal);
220  json_input["thread"] = json_numbert(std::to_string(step.thread_nr));
221  json_input["inputID"] = json_stringt(step.io_id);
222 
223  // Recovering the mode from the function
224  irep_idt mode;
225  const symbolt *function_name;
226  if(ns.lookup(step.function_id, function_name))
227  // Failed to find symbol
228  mode = ID_unknown;
229  else
230  mode = function_name->mode;
231  json_input["mode"] = json_stringt(mode);
232  json_arrayt &json_values = json_input["values"].make_array();
233 
234  for(const auto &arg : step.io_args)
235  {
236  arg.is_nil() ? json_values.push_back(json_stringt(""))
237  : json_values.push_back(json(arg, ns, mode));
238  }
239 
240  if(!location.is_null())
241  json_input["sourceLocation"] = location;
242 }
243 
252  json_objectt &json_call_return,
253  const conversion_dependenciest &conversion_dependencies)
254 {
255  const goto_trace_stept &step = conversion_dependencies.step;
256  const jsont &location = conversion_dependencies.location;
257  const namespacet &ns = conversion_dependencies.ns;
258 
259  std::string tag = (step.type == goto_trace_stept::typet::FUNCTION_CALL)
260  ? "function-call"
261  : "function-return";
262 
263  json_call_return["stepType"] = json_stringt(tag);
264  json_call_return["hidden"] = jsont::json_boolean(step.hidden);
265  json_call_return["internal"] = jsont::json_boolean(step.internal);
266  json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
267 
268  const irep_idt &function_identifier = step.called_function;
269 
270  const symbolt &symbol = ns.lookup(function_identifier);
271  json_call_return["function"] =
272  json_objectt({{"displayName", json_stringt(symbol.display_name())},
273  {"identifier", json_stringt(function_identifier)},
274  {"sourceLocation", json(symbol.location)}});
275 
276  if(!location.is_null())
277  json_call_return["sourceLocation"] = location;
278 }
279 
281  json_objectt &json_location_only,
283 {
284  json_location_only["stepType"] =
286  json_location_only["hidden"] = jsont::json_boolean(default_step.hidden);
287  json_location_only["thread"] =
288  json_numbert(std::to_string(default_step.thread_number));
289  json_location_only["sourceLocation"] = json(default_step.location);
290 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
virtual void operator()(exprt &)
Definition: expr.h:370
Base class for all expressions.
Definition: expr.h:56
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:237
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
std::string comment
Definition: goto_trace.h:124
exprt full_lhs_value
Definition: goto_trace.h:133
irep_idt function_id
Definition: goto_trace.h:111
io_argst io_args
Definition: goto_trace.h:138
unsigned thread_nr
Definition: goto_trace.h:115
irep_idt property_id
Definition: goto_trace.h:123
irep_idt called_function
Definition: goto_trace.h:142
assignment_typet assignment_type
Definition: goto_trace.h:107
std::optional< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:52
irep_idt io_id
Definition: goto_trace.h:136
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:364
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
irept & add(const irep_idt &name)
Definition: irep.cpp:103
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:418
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:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt mode
Language mode.
Definition: symbol.h:49
Traces of GOTO Programs.
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)
Definition: properties.cpp:120
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:534
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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:221
bool json_full_lhs
Add rawLhs property to trace.
Definition: goto_trace.h:223
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.
std::optional< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Symbol table entry.
dstringt irep_idt
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)