cprover
xml_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 "xml_goto_trace.h"
15 
16 #include <cassert>
17 
18 #include <util/xml_expr.h>
19 #include <util/symbol.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "printf_formatter.h"
24 
25 void convert(
26  const namespacet &ns,
27  const goto_tracet &goto_trace,
28  xmlt &dest)
29 {
30  dest=xmlt("goto_trace");
31 
32  source_locationt previous_source_location;
33 
34  for(const auto &step : goto_trace.steps)
35  {
36  const source_locationt &source_location=step.pc->source_location;
37 
38  xmlt xml_location;
39  if(source_location.is_not_nil() && source_location.get_file()!="")
40  xml_location=xml(source_location);
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  xmlt &xml_failure=dest.new_element("failure");
59 
60  xml_failure.set_attribute_bool("hidden", step.hidden);
61  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
62  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
63  xml_failure.set_attribute("reason", id2string(step.comment));
64  xml_failure.set_attribute("property", id2string(property_id));
65 
66  if(xml_location.name!="")
67  xml_failure.new_element().swap(xml_location);
68  }
69  break;
70 
73  {
74  auto lhs_object=step.get_lhs_object();
75  irep_idt identifier=
76  lhs_object.has_value()?lhs_object->get_identifier():irep_idt();
77  xmlt &xml_assignment=dest.new_element("assignment");
78 
79  if(xml_location.name!="")
80  xml_assignment.new_element().swap(xml_location);
81 
82  {
83  auto lhs_object=step.get_lhs_object();
84 
85  const symbolt *symbol;
86 
87  if(lhs_object.has_value() &&
88  !ns.lookup(lhs_object->get_identifier(), symbol))
89  {
90  std::string type_string=from_type(ns, symbol->name, symbol->type);
91 
92  xml_assignment.set_attribute("mode", id2string(symbol->mode));
93  xml_assignment.set_attribute("identifier", id2string(symbol->name));
94  xml_assignment.set_attribute("base_name", id2string(symbol->base_name));
95  xml_assignment.set_attribute("display_name", id2string(symbol->display_name()));
96  xml_assignment.new_element("type").data=type_string;
97  }
98  }
99 
100  std::string full_lhs_string, full_lhs_value_string;
101 
102  if(step.full_lhs.is_not_nil())
103  full_lhs_string=from_expr(ns, identifier, step.full_lhs);
104 
105  if(step.full_lhs_value.is_not_nil())
106  full_lhs_value_string=
107  from_expr(ns, identifier, step.full_lhs_value);
108 
109  xml_assignment.new_element("full_lhs").data=full_lhs_string;
110  xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
111 
112  xml_assignment.set_attribute_bool("hidden", step.hidden);
113  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
114  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
115 
116  xml_assignment.set_attribute("assignment_type",
117  step.assignment_type==
119  "actual_parameter":"state");
120  }
121  break;
122 
124  {
125  printf_formattert printf_formatter(ns);
126  printf_formatter(id2string(step.format_string), step.io_args);
127  std::string text=printf_formatter.as_string();
128  xmlt &xml_output=dest.new_element("output");
129 
130  xml_output.new_element("text").data=text;
131 
132  xml_output.set_attribute_bool("hidden", step.hidden);
133  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
134  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
135 
136  if(xml_location.name!="")
137  xml_output.new_element().swap(xml_location);
138 
139  for(const auto &arg : step.io_args)
140  {
141  xml_output.new_element("value").data =
142  from_expr(ns, step.function, arg);
143  xml_output.new_element("value_expression").
144  new_element(xml(arg, ns));
145  }
146  }
147  break;
148 
150  {
151  xmlt &xml_input=dest.new_element("input");
152  xml_input.new_element("input_id").data=id2string(step.io_id);
153 
154  xml_input.set_attribute_bool("hidden", step.hidden);
155  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
156  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
157 
158  for(const auto &arg : step.io_args)
159  {
160  xml_input.new_element("value").data =
161  from_expr(ns, step.function, arg);
162  xml_input.new_element("value_expression").
163  new_element(xml(arg, ns));
164  }
165 
166  if(xml_location.name!="")
167  xml_input.new_element().swap(xml_location);
168  }
169  break;
170 
172  {
173  std::string tag = "function_call";
174  xmlt &xml_call_return = dest.new_element(tag);
175 
176  xml_call_return.set_attribute_bool("hidden", step.hidden);
177  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
178  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
179 
180  const symbolt &symbol = ns.lookup(step.called_function);
181  xmlt &xml_function = xml_call_return.new_element("function");
182  xml_function.set_attribute(
183  "display_name", id2string(symbol.display_name()));
184  xml_function.set_attribute("identifier", id2string(symbol.name));
185  xml_function.new_element() = xml(symbol.location);
186 
187  if(xml_location.name != "")
188  xml_call_return.new_element().swap(xml_location);
189  }
190  break;
191 
193  {
194  std::string tag = "function_return";
195  xmlt &xml_call_return=dest.new_element(tag);
196 
197  xml_call_return.set_attribute_bool("hidden", step.hidden);
198  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
199  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
200 
201  const symbolt &symbol = ns.lookup(step.function);
202  xmlt &xml_function=xml_call_return.new_element("function");
203  xml_function.set_attribute(
204  "display_name", id2string(symbol.display_name()));
205  xml_function.set_attribute("identifier", id2string(step.function));
206  xml_function.new_element()=xml(symbol.location);
207 
208  if(xml_location.name!="")
209  xml_call_return.new_element().swap(xml_location);
210  }
211  break;
212 
213  default:
214  if(source_location!=previous_source_location)
215  {
216  // just the source location
217  if(xml_location.name!="")
218  {
219  xmlt &xml_location_only=dest.new_element("location-only");
220 
221  xml_location_only.set_attribute_bool("hidden", step.hidden);
222  xml_location_only.set_attribute(
223  "thread", std::to_string(step.thread_nr));
224  xml_location_only.set_attribute(
225  "step_nr", std::to_string(step.step_nr));
226 
227  xml_location_only.new_element().swap(xml_location);
228  }
229  }
230  }
231 
232  if(source_location.is_not_nil() && source_location.get_file()!="")
233  previous_source_location=source_location;
234  }
235 }
irep_idt name
The unique identifier.
Definition: symbol.h:40
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:63
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
Symbol table entry.
irep_idt mode
Language mode.
Definition: symbol.h:49
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string name
Definition: xml.h:30
Symbol table entry.
Definition: symbol.h:27
printf Formatting
stepst steps
Definition: goto_trace.h:154
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
void swap(xmlt &xml)
Definition: xml.cpp:24
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Definition: xml.h:18
Traces of GOTO Programs.
std::string data
Definition: xml.h:30
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
const irep_idt & get_file() const
xmlt & new_element(const std::string &key)
Definition: xml.h:86
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
dstringt irep_idt
Definition: irep.h:32
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
const irep_idt & get_property_id() const
std::string as_string()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166