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 <util/arith_tools.h>
17 #include <util/string_constant.h>
18 #include <util/symbol.h>
19 #include <util/xml_irep.h>
20 
21 #include <langapi/language_util.h>
22 
23 #include "goto_trace.h"
24 #include "printf_formatter.h"
25 #include "structured_trace_util.h"
26 #include "xml_expr.h"
27 
30 {
31  for(auto &op : expr.operands())
33 
34  if(expr.id() == ID_string_constant)
35  expr = to_string_constant(expr).to_array_expr();
36 }
37 
41 static std::string
42 get_printable_xml(const namespacet &ns, const irep_idt &id, const exprt &expr)
43 {
44  std::string result = from_expr(ns, id, expr);
45 
46  if(!xmlt::is_printable_xml(result))
47  {
48  exprt new_expr = expr;
50  result = from_expr(ns, id, new_expr);
51 
52  // give up
53  if(!xmlt::is_printable_xml(result))
54  return {};
55  }
56 
57  return result;
58 }
59 
61 {
62  xmlt value_xml{"full_lhs_value"};
63 
64  const exprt &value = step.full_lhs_value;
65  if(value.is_nil())
66  return value_xml;
67 
68  const auto &lhs_object = step.get_lhs_object();
69  const irep_idt identifier =
70  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
71  value_xml.data = get_printable_xml(ns, identifier, value);
72 
73  const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type());
74  const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
75  if(bv_type && constant)
76  {
77  const auto width = bv_type->get_width();
78  // It is fine to pass `false` into the `is_signed` parameter, even for
79  // signed values, because the subsequent conversion to binary will result
80  // in the same value either way. E.g. if the value is `-1` for a signed 8
81  // bit value, this will convert to `255` which is `11111111` in binary,
82  // which is the desired result.
83  const auto binary_representation =
84  integer2binary(bvrep2integer(constant->get_value(), width, false), width);
85  value_xml.set_attribute("binary", binary_representation);
86  }
87  return value_xml;
88 }
89 
90 void convert(
91  const namespacet &ns,
92  const goto_tracet &goto_trace,
93  xmlt &dest)
94 {
95  dest=xmlt("goto_trace");
96 
97  source_locationt previous_source_location;
98 
99  for(const auto &step : goto_trace.steps)
100  {
101  const source_locationt &source_location = step.pc->source_location();
102 
103  xmlt xml_location;
104  if(source_location.is_not_nil() && !source_location.get_file().empty())
105  xml_location=xml(source_location);
106 
107  switch(step.type)
108  {
110  if(!step.cond_value)
111  {
112  xmlt &xml_failure=dest.new_element("failure");
113 
114  xml_failure.set_attribute_bool("hidden", step.hidden);
115  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
116  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
117  xml_failure.set_attribute("reason", id2string(step.comment));
118  xml_failure.set_attribute("property", id2string(step.property_id));
119 
120  if(!xml_location.name.empty())
121  xml_failure.new_element().swap(xml_location);
122  }
123  break;
124 
127  {
128  auto lhs_object = step.get_lhs_object();
129  irep_idt identifier =
130  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
131  xmlt &xml_assignment = dest.new_element("assignment");
132 
133  if(!xml_location.name.empty())
134  xml_assignment.new_element().swap(xml_location);
135 
136  {
137  const symbolt *symbol;
138 
139  if(
140  lhs_object.has_value() &&
141  !ns.lookup(lhs_object->get_identifier(), symbol))
142  {
143  std::string type_string = from_type(ns, symbol->name, symbol->type);
144 
145  xml_assignment.set_attribute("mode", id2string(symbol->mode));
146  xml_assignment.set_attribute("identifier", id2string(symbol->name));
147  xml_assignment.set_attribute(
148  "base_name", id2string(symbol->base_name));
149  xml_assignment.set_attribute(
150  "display_name", id2string(symbol->display_name()));
151  xml_assignment.new_element("type").data = type_string;
152  }
153  }
154 
155  std::string full_lhs_string;
156 
157  if(step.full_lhs.is_not_nil())
158  full_lhs_string = get_printable_xml(ns, identifier, step.full_lhs);
159 
160  xml_assignment.new_element("full_lhs").data = full_lhs_string;
161  xml_assignment.new_element(full_lhs_value(step, ns));
162 
163  xml_assignment.set_attribute_bool("hidden", step.hidden);
164  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
165  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
166 
167  xml_assignment.set_attribute(
168  "assignment_type",
169  step.assignment_type ==
171  ? "actual_parameter"
172  : "state");
173  break;
174  }
175 
177  {
178  printf_formattert printf_formatter(ns);
179  printf_formatter(id2string(step.format_string), step.io_args);
180  std::string text = printf_formatter.as_string();
181  xmlt &xml_output = dest.new_element("output");
182 
183  xml_output.new_element("text").data = text;
184 
185  xml_output.set_attribute_bool("hidden", step.hidden);
186  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
187  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
188 
189  if(!xml_location.name.empty())
190  xml_output.new_element().swap(xml_location);
191 
192  for(const auto &arg : step.io_args)
193  {
194  xml_output.new_element("value").data =
195  get_printable_xml(ns, step.function_id, arg);
196  xml_output.new_element("value_expression").new_element(xml(arg, ns));
197  }
198  break;
199  }
200 
202  {
203  xmlt &xml_input = dest.new_element("input");
204  xml_input.new_element("input_id").data = id2string(step.io_id);
205 
206  xml_input.set_attribute_bool("hidden", step.hidden);
207  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
208  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
209 
210  for(const auto &arg : step.io_args)
211  {
212  xml_input.new_element("value").data =
213  get_printable_xml(ns, step.function_id, arg);
214  xml_input.new_element("value_expression").new_element(xml(arg, ns));
215  }
216 
217  if(!xml_location.name.empty())
218  xml_input.new_element().swap(xml_location);
219  break;
220  }
221 
223  {
224  std::string tag = "function_call";
225  xmlt &xml_call_return = dest.new_element(tag);
226 
227  xml_call_return.set_attribute_bool("hidden", step.hidden);
228  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
229  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
230 
231  const symbolt &symbol = ns.lookup(step.called_function);
232  xmlt &xml_function = xml_call_return.new_element("function");
233  xml_function.set_attribute(
234  "display_name", id2string(symbol.display_name()));
235  xml_function.set_attribute("identifier", id2string(symbol.name));
236  xml_function.new_element() = xml(symbol.location);
237 
238  if(!xml_location.name.empty())
239  xml_call_return.new_element().swap(xml_location);
240  break;
241  }
242 
244  {
245  std::string tag = "function_return";
246  xmlt &xml_call_return = dest.new_element(tag);
247 
248  xml_call_return.set_attribute_bool("hidden", step.hidden);
249  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
250  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
251 
252  const symbolt &symbol = ns.lookup(step.called_function);
253  xmlt &xml_function = xml_call_return.new_element("function");
254  xml_function.set_attribute(
255  "display_name", id2string(symbol.display_name()));
256  xml_function.set_attribute("identifier", id2string(symbol.name));
257  xml_function.new_element() = xml(symbol.location);
258 
259  if(!xml_location.name.empty())
260  xml_call_return.new_element().swap(xml_location);
261  break;
262  }
263 
276  {
277  const auto default_step = ::default_step(step, previous_source_location);
278  if(default_step)
279  {
280  xmlt &xml_location_only =
282 
283  xml_location_only.set_attribute_bool("hidden", default_step->hidden);
284  xml_location_only.set_attribute(
285  "thread", std::to_string(default_step->thread_number));
286  xml_location_only.set_attribute(
287  "step_nr", std::to_string(default_step->step_number));
288 
289  xml_location_only.new_element(xml(default_step->location));
290  }
291 
292  break;
293  }
294  }
295 
296  if(source_location.is_not_nil() && !source_location.get_file().empty())
297  previous_source_location=source_location;
298  }
299 }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:51
exprt full_lhs_value
Definition: goto_trace.h:132
Trace of a GOTO program.
Definition: goto_trace.h:175
stepst steps
Definition: goto_trace.h:178
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
std::string as_string()
const irep_idt & get_file() const
array_exprt to_array_expr() const
convert string into array constant
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
Definition: xml.h:21
void set_attribute_bool(const std::string &attribute, bool value)
Definition: xml.h:72
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
void swap(xmlt &xml)
Definition: xml.cpp:25
xmlt & new_element(const std::string &key)
Definition: xml.h:95
std::string data
Definition: xml.h:39
static bool is_printable_xml(const std::string &s)
Determine whether s does not contain any characters that cannot be escaped in XML 1....
Definition: xml.cpp:160
std::string name
Definition: xml.h:39
Traces of GOTO Programs.
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
printf Formatting
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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.
optionalt< default_trace_stept > default_step(const goto_trace_stept &step, const source_locationt &previous_source_location)
Utilities for printing location info steps in the trace in a format agnostic way.
Symbol table entry.
xmlt full_lhs_value(const goto_trace_stept &step, const namespacet &ns)
static std::string get_printable_xml(const namespacet &ns, const irep_idt &id, const exprt &expr)
Given an expression expr, produce a string representation that is printable in XML 1....
static void replace_string_constants_rec(exprt &expr)
Rewrite all string constants to their array counterparts.
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
Traces of GOTO Programs.