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 #include <util/arith_tools.h>
23 
24 #include "printf_formatter.h"
25 #include "structured_trace_util.h"
26 #include "xml_expr.h"
27 
29 {
30  xmlt value_xml{"full_lhs_value"};
31 
32  const exprt &value = step.full_lhs_value;
33  if(value.is_nil())
34  return value_xml;
35 
36  const auto &lhs_object = step.get_lhs_object();
37  const irep_idt identifier =
38  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
39  value_xml.data = from_expr(ns, identifier, value);
40 
41  const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type());
42  const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
43  if(bv_type && constant)
44  {
45  const auto width = bv_type->get_width();
46  // It is fine to pass `false` into the `is_signed` parameter, even for
47  // signed values, because the subsequent conversion to binary will result
48  // in the same value either way. E.g. if the value is `-1` for a signed 8
49  // bit value, this will convert to `255` which is `11111111` in binary,
50  // which is the desired result.
51  const auto binary_representation =
52  integer2binary(bvrep2integer(constant->get_value(), width, false), width);
53  value_xml.set_attribute("binary", binary_representation);
54  }
55  return value_xml;
56 }
57 
58 void convert(
59  const namespacet &ns,
60  const goto_tracet &goto_trace,
61  xmlt &dest)
62 {
63  dest=xmlt("goto_trace");
64 
65  source_locationt previous_source_location;
66 
67  for(const auto &step : goto_trace.steps)
68  {
69  const source_locationt &source_location=step.pc->source_location;
70 
71  xmlt xml_location;
72  if(source_location.is_not_nil() && !source_location.get_file().empty())
73  xml_location=xml(source_location);
74 
75  switch(step.type)
76  {
78  if(!step.cond_value)
79  {
80  xmlt &xml_failure=dest.new_element("failure");
81 
82  xml_failure.set_attribute_bool("hidden", step.hidden);
83  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
84  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
85  xml_failure.set_attribute("reason", id2string(step.comment));
86  xml_failure.set_attribute("property", id2string(step.property_id));
87 
88  if(!xml_location.name.empty())
89  xml_failure.new_element().swap(xml_location);
90  }
91  break;
92 
95  {
96  auto lhs_object = step.get_lhs_object();
97  irep_idt identifier =
98  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
99  xmlt &xml_assignment = dest.new_element("assignment");
100 
101  if(!xml_location.name.empty())
102  xml_assignment.new_element().swap(xml_location);
103 
104  {
105  const symbolt *symbol;
106 
107  if(
108  lhs_object.has_value() &&
109  !ns.lookup(lhs_object->get_identifier(), symbol))
110  {
111  std::string type_string = from_type(ns, symbol->name, symbol->type);
112 
113  xml_assignment.set_attribute("mode", id2string(symbol->mode));
114  xml_assignment.set_attribute("identifier", id2string(symbol->name));
115  xml_assignment.set_attribute(
116  "base_name", id2string(symbol->base_name));
117  xml_assignment.set_attribute(
118  "display_name", id2string(symbol->display_name()));
119  xml_assignment.new_element("type").data = type_string;
120  }
121  }
122 
123  std::string full_lhs_string;
124 
125  if(step.full_lhs.is_not_nil())
126  full_lhs_string = from_expr(ns, identifier, step.full_lhs);
127 
128  xml_assignment.new_element("full_lhs").data = full_lhs_string;
129  xml_assignment.new_element(full_lhs_value(step, ns));
130 
131  xml_assignment.set_attribute_bool("hidden", step.hidden);
132  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
133  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
134 
135  xml_assignment.set_attribute(
136  "assignment_type",
137  step.assignment_type ==
139  ? "actual_parameter"
140  : "state");
141  break;
142  }
143 
145  {
146  printf_formattert printf_formatter(ns);
147  printf_formatter(id2string(step.format_string), step.io_args);
148  std::string text = printf_formatter.as_string();
149  xmlt &xml_output = dest.new_element("output");
150 
151  xml_output.new_element("text").data = text;
152 
153  xml_output.set_attribute_bool("hidden", step.hidden);
154  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
155  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
156 
157  if(!xml_location.name.empty())
158  xml_output.new_element().swap(xml_location);
159 
160  for(const auto &arg : step.io_args)
161  {
162  xml_output.new_element("value").data =
163  from_expr(ns, step.function_id, arg);
164  xml_output.new_element("value_expression").new_element(xml(arg, ns));
165  }
166  break;
167  }
168 
170  {
171  xmlt &xml_input = dest.new_element("input");
172  xml_input.new_element("input_id").data = id2string(step.io_id);
173 
174  xml_input.set_attribute_bool("hidden", step.hidden);
175  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
176  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
177 
178  for(const auto &arg : step.io_args)
179  {
180  xml_input.new_element("value").data =
181  from_expr(ns, step.function_id, arg);
182  xml_input.new_element("value_expression").new_element(xml(arg, ns));
183  }
184 
185  if(!xml_location.name.empty())
186  xml_input.new_element().swap(xml_location);
187  break;
188  }
189 
191  {
192  std::string tag = "function_call";
193  xmlt &xml_call_return = dest.new_element(tag);
194 
195  xml_call_return.set_attribute_bool("hidden", step.hidden);
196  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
197  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
198 
199  const symbolt &symbol = ns.lookup(step.called_function);
200  xmlt &xml_function = xml_call_return.new_element("function");
201  xml_function.set_attribute(
202  "display_name", id2string(symbol.display_name()));
203  xml_function.set_attribute("identifier", id2string(symbol.name));
204  xml_function.new_element() = xml(symbol.location);
205 
206  if(!xml_location.name.empty())
207  xml_call_return.new_element().swap(xml_location);
208  break;
209  }
210 
212  {
213  std::string tag = "function_return";
214  xmlt &xml_call_return = dest.new_element(tag);
215 
216  xml_call_return.set_attribute_bool("hidden", step.hidden);
217  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
218  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
219 
220  const symbolt &symbol = ns.lookup(step.called_function);
221  xmlt &xml_function = xml_call_return.new_element("function");
222  xml_function.set_attribute(
223  "display_name", id2string(symbol.display_name()));
224  xml_function.set_attribute("identifier", id2string(symbol.name));
225  xml_function.new_element() = xml(symbol.location);
226 
227  if(!xml_location.name.empty())
228  xml_call_return.new_element().swap(xml_location);
229  break;
230  }
231 
244  {
245  const auto default_step = ::default_step(step, previous_source_location);
246  if(default_step)
247  {
248  xmlt &xml_location_only =
250 
251  xml_location_only.set_attribute_bool("hidden", default_step->hidden);
252  xml_location_only.set_attribute(
253  "thread", std::to_string(default_step->thread_number));
254  xml_location_only.set_attribute(
255  "step_nr", std::to_string(default_step->step_number));
256 
257  xml_location_only.new_element(xml(default_step->location));
258  }
259 
260  break;
261  }
262  }
263 
264  if(source_location.is_not_nil() && !source_location.get_file().empty())
265  previous_source_location=source_location;
266  }
267 }
default_step
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Definition: structured_trace_util.cpp:39
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::full_lhs_value
exprt full_lhs_value
Definition: goto_trace.h:132
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:49
goto_trace_stept::typet::ASSUME
@ ASSUME
arith_tools.h
printf_formattert
Definition: printf_formatter.h:21
printf_formatter.h
printf Formatting
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:58
default_step_name
std::string default_step_name(const default_step_kindt &step_type)
Turns a default_step_kindt into a string that can be used in the trace.
Definition: structured_trace_util.cpp:27
goto_tracet::steps
stepst steps
Definition: goto_trace.h:174
exprt
Base class for all expressions.
Definition: expr.h:53
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
goto_trace_stept
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:39
xml_goto_trace.h
Traces of GOTO Programs.
goto_trace_stept::typet::ASSIGNMENT
@ ASSIGNMENT
symbol.h
Symbol table entry.
irept::is_nil
bool is_nil() const
Definition: irep.h:398
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:21
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
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:401
goto_trace_stept::typet::GOTO
@ GOTO
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
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:72
goto_trace_stept::typet::ATOMIC_BEGIN
@ ATOMIC_BEGIN
full_lhs_value
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
Definition: xml_goto_trace.cpp:28
xmlt::swap
void swap(xmlt &xml)
Definition: xml.cpp:25
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
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
structured_trace_util.h
Utilities for printing location info steps in the trace in a format agnostic way.
goto_trace_stept::typet::FUNCTION_CALL
@ FUNCTION_CALL
xmlt::data
std::string data
Definition: xml.h:39
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:95
goto_trace_stept::typet::DEAD
@ DEAD
goto_trace_stept::typet::CONSTRAINT
@ CONSTRAINT