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 <cassert>
17 
18 #include <util/json_expr.h>
19 
20 #include <langapi/language_util.h>
21 
22 void convert(
23  const namespacet &ns,
24  const goto_tracet &goto_trace,
25  jsont &dest)
26 {
27  json_arrayt &dest_array=dest.make_array();
28 
29  source_locationt previous_source_location;
30 
31  for(const auto &step : goto_trace.steps)
32  {
33  const source_locationt &source_location=step.pc->source_location;
34 
35  jsont json_location;
36 
37  if(source_location.is_not_nil() && source_location.get_file()!="")
38  json_location=json(source_location);
39  else
40  json_location=json_nullt();
41 
42  switch(step.type)
43  {
45  if(!step.cond_value)
46  {
47  irep_idt property_id;
48 
49  if(step.pc->is_assert())
50  property_id=source_location.get_property_id();
51  else if(step.pc->is_goto()) // unwinding, we suspect
52  {
53  property_id=
54  id2string(step.pc->source_location.get_function())+
55  ".unwind."+std::to_string(step.pc->loop_number);
56  }
57 
58  json_objectt &json_failure=dest_array.push_back().make_object();
59 
60  json_failure["stepType"]=json_stringt("failure");
61  json_failure["hidden"]=jsont::json_boolean(step.hidden);
62  json_failure["thread"]=json_numbert(std::to_string(step.thread_nr));
63  json_failure["reason"]=json_stringt(id2string(step.comment));
64  json_failure["property"]=json_stringt(id2string(property_id));
65 
66  if(!json_location.is_null())
67  json_failure["sourceLocation"]=json_location;
68  }
69  break;
70 
73  {
74  irep_idt identifier=step.lhs_object.get_identifier();
75  json_objectt &json_assignment=dest_array.push_back().make_object();
76 
77  json_assignment["stepType"]=json_stringt("assignment");
78 
79  if(!json_location.is_null())
80  json_assignment["sourceLocation"]=json_location;
81 
82  std::string value_string, binary_string, type_string, full_lhs_string;
83  json_objectt full_lhs_value;
84 
85  if(step.full_lhs.is_not_nil())
86  full_lhs_string=from_expr(ns, identifier, step.full_lhs);
87 
88 #if 0
89  if(it.full_lhs_value.is_not_nil())
90  full_lhs_value_string=from_expr(ns, identifier, it.full_lhs_value);
91 #endif
92 
93  if(step.full_lhs_value.is_not_nil())
94  full_lhs_value = json(step.full_lhs_value, ns);
95 
96  const symbolt *symbol;
97  irep_idt base_name, display_name;
98 
99  if(!ns.lookup(identifier, symbol))
100  {
101  base_name=symbol->base_name;
102  display_name=symbol->display_name();
103  if(type_string=="")
104  type_string=from_type(ns, identifier, symbol->type);
105 
106  json_assignment["mode"]=json_stringt(id2string(symbol->mode));
107  }
108 
109  json_assignment["value"]=full_lhs_value;
110  json_assignment["lhs"]=json_stringt(full_lhs_string);
111  json_assignment["hidden"]=jsont::json_boolean(step.hidden);
112  json_assignment["thread"]=json_numbert(std::to_string(step.thread_nr));
113 
114  json_assignment["assignmentType"]=
115  json_stringt(
116  step.assignment_type==
118  "actual-parameter":
119  "variable");
120  }
121  break;
122 
124  {
125  json_objectt &json_output=dest_array.push_back().make_object();
126 
127  json_output["stepType"]=json_stringt("output");
128  json_output["hidden"]=jsont::json_boolean(step.hidden);
129  json_output["thread"]=json_numbert(std::to_string(step.thread_nr));
130  json_output["outputID"]=json_stringt(id2string(step.io_id));
131 
132  json_arrayt &json_values=json_output["values"].make_array();
133 
134  for(const auto &arg : step.io_args)
135  {
136  if(arg.is_nil())
137  json_values.push_back(json_stringt(""));
138  else
139  json_values.push_back(json(arg, ns));
140  }
141 
142  if(!json_location.is_null())
143  json_output["sourceLocation"]=json_location;
144  }
145  break;
146 
148  {
149  json_objectt &json_input=dest_array.push_back().make_object();
150 
151  json_input["stepType"]=json_stringt("input");
152  json_input["hidden"]=jsont::json_boolean(step.hidden);
153  json_input["thread"]=json_numbert(std::to_string(step.thread_nr));
154  json_input["inputID"]=json_stringt(id2string(step.io_id));
155 
156  json_arrayt &json_values=json_input["values"].make_array();
157 
158  for(const auto &arg : step.io_args)
159  {
160  if(arg.is_nil())
161  json_values.push_back(json_stringt(""));
162  else
163  json_values.push_back(json(arg, ns));
164  }
165 
166  if(!json_location.is_null())
167  json_input["sourceLocation"]=json_location;
168  }
169  break;
170 
173  {
174  std::string tag=
176  "function-call":"function-return";
177  json_objectt &json_call_return=dest_array.push_back().make_object();
178 
179  json_call_return["stepType"]=json_stringt(tag);
180  json_call_return["hidden"]=jsont::json_boolean(step.hidden);
181  json_call_return["thread"]=json_numbert(std::to_string(step.thread_nr));
182 
183  const symbolt &symbol=ns.lookup(step.identifier);
184  json_objectt &json_function=json_call_return["function"].make_object();
185  json_function["displayName"]=
187  json_function["identifier"]=json_stringt(id2string(step.identifier));
188  json_function["sourceLocation"]=json(symbol.location);
189 
190  if(!json_location.is_null())
191  json_call_return["sourceLocation"]=json_location;
192  }
193  break;
194 
195  default:
196  if(source_location!=previous_source_location)
197  {
198  // just the source location
199  if(!json_location.is_null())
200  {
201  json_objectt &json_location_only=dest_array.push_back().make_object();
202  json_location_only["stepType"]=json_stringt("location-only");
203  json_location_only["hidden"]=jsont::json_boolean(step.hidden);
204  json_location_only["thread"]=
205  json_numbert(std::to_string(step.thread_nr));
206  json_location_only["sourceLocation"]=json_location;
207  }
208  }
209  }
210 
211  if(source_location.is_not_nil() && source_location.get_file()!="")
212  previous_source_location=source_location;
213  }
214 }
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
irep_idt mode
Language mode.
Definition: symbol.h:55
Definition: json.h:21
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static jsont json_boolean(bool value)
Definition: json.h:83
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
stepst steps
Definition: goto_trace.h:150
json_arrayt & make_array()
Definition: json.h:228
jsont & push_back(const jsont &json)
Definition: json.h:157
Traces of GOTO Programs.
Expressions in JSON.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_null() const
Definition: json.h:67
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void convert(const namespacet &ns, const goto_tracet &goto_trace, jsont &dest)
const irep_idt & display_name() const
Definition: symbol.h:60
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
const irep_idt & get_file() const
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
json_objectt & make_object()
Definition: json.h:234
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
const irep_idt & get_property_id() const
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23