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/symbol.h>
19 #include <util/xml_irep.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "printf_formatter.h"
24 #include "xml_expr.h"
25 
26 void convert(
27  const namespacet &ns,
28  const goto_tracet &goto_trace,
29  xmlt &dest)
30 {
31  dest=xmlt("goto_trace");
32 
33  source_locationt previous_source_location;
34 
35  for(const auto &step : goto_trace.steps)
36  {
37  const source_locationt &source_location=step.pc->source_location;
38 
39  xmlt xml_location;
40  if(source_location.is_not_nil() && !source_location.get_file().empty())
41  xml_location=xml(source_location);
42 
43  switch(step.type)
44  {
46  if(!step.cond_value)
47  {
48  xmlt &xml_failure=dest.new_element("failure");
49 
50  xml_failure.set_attribute_bool("hidden", step.hidden);
51  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
52  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
53  xml_failure.set_attribute("reason", id2string(step.comment));
54  xml_failure.set_attribute("property", id2string(step.property_id));
55 
56  if(!xml_location.name.empty())
57  xml_failure.new_element().swap(xml_location);
58  }
59  break;
60 
63  {
64  auto lhs_object = step.get_lhs_object();
65  irep_idt identifier =
66  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
67  xmlt &xml_assignment = dest.new_element("assignment");
68 
69  if(!xml_location.name.empty())
70  xml_assignment.new_element().swap(xml_location);
71 
72  {
73  auto lhs_object=step.get_lhs_object();
74 
75  const symbolt *symbol;
76 
77  if(
78  lhs_object.has_value() &&
79  !ns.lookup(lhs_object->get_identifier(), symbol))
80  {
81  const symbolt *symbol;
82 
83  if(lhs_object.has_value() &&
84  !ns.lookup(lhs_object->get_identifier(), symbol))
85  {
86  std::string type_string=from_type(ns, symbol->name, symbol->type);
87 
88  xml_assignment.set_attribute("mode", id2string(symbol->mode));
89  xml_assignment.set_attribute("identifier", id2string(symbol->name));
90  xml_assignment.set_attribute("base_name", id2string(symbol->base_name));
91  xml_assignment.set_attribute("display_name", id2string(symbol->display_name()));
92  xml_assignment.new_element("type").data=type_string;
93  }
94  }
95  }
96 
97  std::string full_lhs_string, full_lhs_value_string;
98 
99  if(step.full_lhs.is_not_nil())
100  full_lhs_string = from_expr(ns, identifier, step.full_lhs);
101 
102  if(step.full_lhs_value.is_not_nil())
103  full_lhs_value_string = from_expr(ns, identifier, step.full_lhs_value);
104 
105  xml_assignment.new_element("full_lhs").data = full_lhs_string;
106  xml_assignment.new_element("full_lhs_value").data = full_lhs_value_string;
107 
108  xml_assignment.set_attribute_bool("hidden", step.hidden);
109  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
110  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
111 
112  xml_assignment.set_attribute(
113  "assignment_type",
114  step.assignment_type ==
116  ? "actual_parameter"
117  : "state");
118  break;
119  }
120 
122  {
123  printf_formattert printf_formatter(ns);
124  printf_formatter(id2string(step.format_string), step.io_args);
125  std::string text = printf_formatter.as_string();
126  xmlt &xml_output = dest.new_element("output");
127 
128  xml_output.new_element("text").data = text;
129 
130  xml_output.set_attribute_bool("hidden", step.hidden);
131  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
132  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
133 
134  if(!xml_location.name.empty())
135  xml_output.new_element().swap(xml_location);
136 
137  for(const auto &arg : step.io_args)
138  {
139  xml_output.new_element("value").data =
140  from_expr(ns, step.function_id, arg);
141  xml_output.new_element("value_expression").new_element(xml(arg, ns));
142  }
143  break;
144  }
145 
147  {
148  xmlt &xml_input = dest.new_element("input");
149  xml_input.new_element("input_id").data = id2string(step.io_id);
150 
151  xml_input.set_attribute_bool("hidden", step.hidden);
152  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
153  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
154 
155  for(const auto &arg : step.io_args)
156  {
157  xml_input.new_element("value").data =
158  from_expr(ns, step.function_id, arg);
159  xml_input.new_element("value_expression").new_element(xml(arg, ns));
160  }
161 
162  if(!xml_location.name.empty())
163  xml_input.new_element().swap(xml_location);
164  break;
165  }
166 
168  {
169  std::string tag = "function_call";
170  xmlt &xml_call_return = dest.new_element(tag);
171 
172  xml_call_return.set_attribute_bool("hidden", step.hidden);
173  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
174  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
175 
176  const symbolt &symbol = ns.lookup(step.called_function);
177  xmlt &xml_function = xml_call_return.new_element("function");
178  xml_function.set_attribute(
179  "display_name", id2string(symbol.display_name()));
180  xml_function.set_attribute("identifier", id2string(symbol.name));
181  xml_function.new_element() = xml(symbol.location);
182 
183  if(!xml_location.name.empty())
184  xml_call_return.new_element().swap(xml_location);
185  break;
186  }
187 
189  {
190  std::string tag = "function_return";
191  xmlt &xml_call_return = dest.new_element(tag);
192 
193  xml_call_return.set_attribute_bool("hidden", step.hidden);
194  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
195  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
196 
197  const symbolt &symbol = ns.lookup(step.called_function);
198  xmlt &xml_function = xml_call_return.new_element("function");
199  xml_function.set_attribute(
200  "display_name", id2string(symbol.display_name()));
201  xml_function.set_attribute("identifier", id2string(symbol.name));
202  xml_function.new_element() = xml(symbol.location);
203 
204  if(!xml_location.name.empty())
205  xml_call_return.new_element().swap(xml_location);
206  break;
207  }
208 
221  if(source_location!=previous_source_location)
222  {
223  // just the source location
224  if(!xml_location.name.empty())
225  {
226  xmlt &xml_location_only=dest.new_element("location-only");
227 
228  xml_location_only.set_attribute_bool("hidden", step.hidden);
229  xml_location_only.set_attribute(
230  "thread", std::to_string(step.thread_nr));
231  xml_location_only.set_attribute(
232  "step_nr", std::to_string(step.step_nr));
233 
234  xml_location_only.new_element().swap(xml_location);
235  }
236  }
237  }
238 
239  if(source_location.is_not_nil() && !source_location.get_file().empty())
240  previous_source_location=source_location;
241  }
242 }
printf_formattert::as_string
std::string as_string()
Definition: printf_formatter.cpp:52
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_trace_stept::typet::LOCATION
@ LOCATION
goto_trace_stept::typet::ASSUME
@ ASSUME
printf_formattert
Definition: printf_formatter.h:21
printf_formatter.h
symbolt::display_name
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
convert
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
Definition: xml_goto_trace.cpp:26
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
xml_irep.h
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:32
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
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:140
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
goto_trace_stept::typet::OUTPUT
@ OUTPUT
goto_trace_stept::typet::FUNCTION_RETURN
@ FUNCTION_RETURN
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
goto_trace_stept::typet::DECL
@ DECL
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
goto_trace_stept::typet::ASSERT
@ ASSERT
language_util.h
goto_trace_stept::typet::NONE
@ NONE
xmlt::name
std::string name
Definition: xml.h:37
xml_goto_trace.h
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
symbol.h
Symbol table entry.
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER
@ ACTUAL_PARAMETER
goto_trace_stept::typet::INPUT
@ INPUT
goto_trace_stept::typet::ATOMIC_END
@ ATOMIC_END
xmlt
Definition: xml.h:19
goto_trace_stept::typet::SPAWN
@ SPAWN
source_locationt
Definition: source_location.h:20
goto_trace_stept::typet::MEMORY_BARRIER
@ MEMORY_BARRIER
goto_trace_stept::typet::SHARED_WRITE
@ SHARED_WRITE
goto_trace_stept::typet::GOTO
@ GOTO
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
xmlt::set_attribute_bool
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:70
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
xmlt::swap
void swap(xmlt &xml)
Definition: xml.cpp:24
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
goto_trace_stept::typet::SHARED_READ
@ SHARED_READ
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
xmlt::data
std::string data
Definition: xml.h:37
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
xml_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:93
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT