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  irep_idt identifier=step.lhs_object.get_identifier();
75  xmlt &xml_assignment=dest.new_element("assignment");
76 
77  if(xml_location.name!="")
78  xml_assignment.new_element().swap(xml_location);
79 
80  std::string value_string, type_string,
81  full_lhs_string, full_lhs_value_string;
82 
83  if(step.lhs_object_value.is_not_nil())
84  value_string=from_expr(ns, identifier, step.lhs_object_value);
85 
86  if(step.full_lhs.is_not_nil())
87  full_lhs_string=from_expr(ns, identifier, step.full_lhs);
88 
89  if(step.full_lhs_value.is_not_nil())
90  full_lhs_value_string=
91  from_expr(ns, identifier, step.full_lhs_value);
92 
93  if(step.lhs_object_value.type().is_not_nil())
94  type_string=
95  from_type(ns, identifier, step.lhs_object_value.type());
96 
97  const symbolt *symbol;
98  irep_idt base_name, display_name;
99 
100  if(!ns.lookup(identifier, symbol))
101  {
102  base_name=symbol->base_name;
103  display_name=symbol->display_name();
104  if(type_string=="")
105  type_string=from_type(ns, identifier, symbol->type);
106 
107  xml_assignment.set_attribute("mode", id2string(symbol->mode));
108  }
109 
110  xml_assignment.new_element("type").data=type_string;
111  xml_assignment.new_element("full_lhs").data=full_lhs_string;
112  xml_assignment.new_element("full_lhs_value").data=full_lhs_value_string;
113  xml_assignment.new_element("value").data=value_string;
114 
115  xml_assignment.set_attribute_bool("hidden", step.hidden);
116  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
117  xml_assignment.set_attribute("identifier", id2string(identifier));
118  xml_assignment.set_attribute("base_name", id2string(base_name));
119  xml_assignment.set_attribute("display_name", id2string(display_name));
120  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
121 
122  xml_assignment.set_attribute("assignment_type",
123  step.assignment_type==
125  "actual_parameter":"state");
126 
127  if(step.lhs_object_value.is_not_nil())
128  xml_assignment.new_element("value_expression").
129  new_element(xml(step.lhs_object_value, ns));
130  }
131  break;
132 
134  {
135  printf_formattert printf_formatter(ns);
136  printf_formatter(id2string(step.format_string), step.io_args);
137  std::string text=printf_formatter.as_string();
138  xmlt &xml_output=dest.new_element("output");
139 
140  xml_output.new_element("text").data=text;
141 
142  xml_output.set_attribute_bool("hidden", step.hidden);
143  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
144  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
145 
146  if(xml_location.name!="")
147  xml_output.new_element().swap(xml_location);
148 
149  for(const auto &arg : step.io_args)
150  {
151  xml_output.new_element("value").data =
152  from_expr(ns, step.pc->function, arg);
153  xml_output.new_element("value_expression").
154  new_element(xml(arg, ns));
155  }
156  }
157  break;
158 
160  {
161  xmlt &xml_input=dest.new_element("input");
162  xml_input.new_element("input_id").data=id2string(step.io_id);
163 
164  xml_input.set_attribute_bool("hidden", step.hidden);
165  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
166  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
167 
168  for(const auto &arg : step.io_args)
169  {
170  xml_input.new_element("value").data =
171  from_expr(ns, step.pc->function, arg);
172  xml_input.new_element("value_expression").
173  new_element(xml(arg, ns));
174  }
175 
176  if(xml_location.name!="")
177  xml_input.new_element().swap(xml_location);
178  }
179  break;
180 
183  {
184  std::string tag=
186  "function_call":"function_return";
187  xmlt &xml_call_return=dest.new_element(tag);
188 
189  xml_call_return.set_attribute_bool("hidden", step.hidden);
190  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
191  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
192 
193  const symbolt &symbol=ns.lookup(step.identifier);
194  xmlt &xml_function=xml_call_return.new_element("function");
195  xml_function.set_attribute(
196  "display_name", id2string(symbol.display_name()));
197  xml_function.set_attribute("identifier", id2string(step.identifier));
198  xml_function.new_element()=xml(symbol.location);
199 
200  if(xml_location.name!="")
201  xml_call_return.new_element().swap(xml_location);
202  }
203  break;
204 
205  default:
206  if(source_location!=previous_source_location)
207  {
208  // just the source location
209  if(xml_location.name!="")
210  {
211  xmlt &xml_location_only=dest.new_element("location-only");
212 
213  xml_location_only.set_attribute_bool("hidden", step.hidden);
214  xml_location_only.set_attribute(
215  "thread", std::to_string(step.thread_nr));
216  xml_location_only.set_attribute(
217  "step_nr", std::to_string(step.step_nr));
218 
219  xml_location_only.new_element().swap(xml_location);
220  }
221  }
222  }
223 
224  if(source_location.is_not_nil() && source_location.get_file()!="")
225  previous_source_location=source_location;
226  }
227 }
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:43
bool is_not_nil() const
Definition: irep.h:103
Symbol table entry.
irep_idt mode
Language mode.
Definition: symbol.h:52
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:30
printf Formatting
stepst steps
Definition: goto_trace.h:156
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:74
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:57
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
const irep_idt & get_file() const
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
std::string to_string(const string_constraintt &expr)
Used for debug printing.
TO_BE_DOCUMENTED.
Definition: goto_trace.h:152
const irep_idt & get_property_id() const
std::string as_string()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130