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 
22 #include <langapi/language_util.h>
23 
24 void convert(
25  const namespacet &ns,
26  const goto_tracet &goto_trace,
27  xmlt &dest)
28 {
29  dest=xmlt("goto_trace");
30 
31  source_locationt previous_source_location;
32 
33  for(const auto &step : goto_trace.steps)
34  {
35  const source_locationt &source_location=step.pc->source_location;
36 
37  xmlt xml_location;
38  if(source_location.is_not_nil() && source_location.get_file()!="")
39  xml_location=xml(source_location);
40 
41  switch(step.type)
42  {
44  if(!step.cond_value)
45  {
46  irep_idt property_id;
47 
48  if(step.pc->is_assert())
49  property_id=source_location.get_property_id();
50  else if(step.pc->is_goto()) // unwinding, we suspect
51  {
52  property_id=
53  id2string(step.pc->source_location.get_function())+
54  ".unwind."+std::to_string(step.pc->loop_number);
55  }
56 
57  xmlt &xml_failure=dest.new_element("failure");
58 
59  xml_failure.set_attribute_bool("hidden", step.hidden);
60  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
61  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
62  xml_failure.set_attribute("reason", id2string(step.comment));
63  xml_failure.set_attribute("property", id2string(property_id));
64 
65  if(xml_location.name!="")
66  xml_failure.new_element().swap(xml_location);
67  }
68  break;
69 
72  {
73  irep_idt identifier=step.lhs_object.get_identifier();
74  xmlt &xml_assignment=dest.new_element("assignment");
75 
76  if(xml_location.name!="")
77  xml_assignment.new_element().swap(xml_location);
78 
79  std::string value_string, binary_string, type_string,
80  full_lhs_string, full_lhs_value_string;
81 
82  if(step.lhs_object_value.is_not_nil())
83  value_string=from_expr(ns, identifier, step.lhs_object_value);
84 
85  if(step.full_lhs.is_not_nil())
86  full_lhs_string=from_expr(ns, identifier, step.full_lhs);
87 
88  if(step.full_lhs_value.is_not_nil())
89  full_lhs_value_string=
90  from_expr(ns, identifier, step.full_lhs_value);
91 
92  if(step.lhs_object_value.type().is_not_nil())
93  type_string=
94  from_type(ns, identifier, step.lhs_object_value.type());
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  xml_assignment.set_attribute("mode", id2string(symbol->mode));
107  }
108 
109  xml_assignment.new_element("type").data=type_string;
110  xml_assignment.new_element("full_lhs").data=full_lhs_string;
111  xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
112  xml_assignment.new_element("value").data=value_string;
113 
114  xml_assignment.set_attribute_bool("hidden", step.hidden);
115  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
116  xml_assignment.set_attribute("identifier", id2string(identifier));
117  xml_assignment.set_attribute("base_name", id2string(base_name));
118  xml_assignment.set_attribute("display_name", id2string(display_name));
119  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
120 
121  xml_assignment.set_attribute("assignment_type",
122  step.assignment_type==
124  "actual_parameter":"state");
125 
126  if(step.lhs_object_value.is_not_nil())
127  xml_assignment.new_element("value_expression").
128  new_element(xml(step.lhs_object_value, ns));
129  }
130  break;
131 
133  {
134  printf_formattert printf_formatter(ns);
135  printf_formatter(id2string(step.format_string), step.io_args);
136  std::string text=printf_formatter.as_string();
137  xmlt &xml_output=dest.new_element("output");
138 
139  xml_output.new_element("text").data=text;
140 
141  xml_output.set_attribute_bool("hidden", step.hidden);
142  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
143  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
144 
145  if(xml_location.name!="")
146  xml_output.new_element().swap(xml_location);
147 
148  for(const auto &arg : step.io_args)
149  {
150  xml_output.new_element("value").data=from_expr(ns, "", arg);
151  xml_output.new_element("value_expression").
152  new_element(xml(arg, ns));
153  }
154  }
155  break;
156 
158  {
159  xmlt &xml_input=dest.new_element("input");
160  xml_input.new_element("input_id").data=id2string(step.io_id);
161 
162  xml_input.set_attribute_bool("hidden", step.hidden);
163  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
164  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
165 
166  for(const auto &arg : step.io_args)
167  {
168  xml_input.new_element("value").data=from_expr(ns, "", arg);
169  xml_input.new_element("value_expression").
170  new_element(xml(arg, ns));
171  }
172 
173  if(xml_location.name!="")
174  xml_input.new_element().swap(xml_location);
175  }
176  break;
177 
180  {
181  std::string tag=
183  "function_call":"function_return";
184  xmlt &xml_call_return=dest.new_element(tag);
185 
186  xml_call_return.set_attribute_bool("hidden", step.hidden);
187  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
188  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
189 
190  const symbolt &symbol=ns.lookup(step.identifier);
191  xmlt &xml_function=xml_call_return.new_element("function");
192  xml_function.set_attribute(
193  "display_name", id2string(symbol.display_name()));
194  xml_function.set_attribute("identifier", id2string(step.identifier));
195  xml_function.new_element()=xml(symbol.location);
196 
197  if(xml_location.name!="")
198  xml_call_return.new_element().swap(xml_location);
199  }
200  break;
201 
202  default:
203  if(source_location!=previous_source_location)
204  {
205  // just the source location
206  if(xml_location.name!="")
207  {
208  xmlt &xml_location_only=dest.new_element("location-only");
209 
210  xml_location_only.set_attribute_bool("hidden", step.hidden);
211  xml_location_only.set_attribute(
212  "thread", std::to_string(step.thread_nr));
213  xml_location_only.set_attribute(
214  "step_nr", std::to_string(step.step_nr));
215 
216  xml_location_only.new_element().swap(xml_location);
217  }
218  }
219  }
220 
221  if(source_location.is_not_nil() && source_location.get_file()!="")
222  previous_source_location=source_location;
223  }
224 }
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:63
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
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:104
Symbol table entry.
irep_idt mode
Language mode.
Definition: symbol.h:55
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string name
Definition: xml.h:30
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
printf Formatting
stepst steps
Definition: goto_trace.h:150
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
void swap(xmlt &xml)
Definition: xml.cpp:23
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
Traces of GOTO Programs.
std::string data
Definition: xml.h:30
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
xmlt & new_element(const std::string &name)
Definition: xml.h:86
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
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
const irep_idt & get_property_id() const
std::string as_string()