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