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/string_constant.h>
17 #include <util/symbol.h>
18 #include <util/xml_irep.h>
19 
20 #include <langapi/language_util.h>
21 #include <util/arith_tools.h>
22 
23 #include "printf_formatter.h"
24 #include "structured_trace_util.h"
25 #include "xml_expr.h"
26 
29 {
30  for(auto &op : expr.operands())
32 
33  if(expr.id() == ID_string_constant)
34  expr = to_string_constant(expr).to_array_expr();
35 }
36 
40 static std::string
41 get_printable_xml(const namespacet &ns, const irep_idt &id, const exprt &expr)
42 {
43  std::string result = from_expr(ns, id, expr);
44 
45  if(!xmlt::is_printable_xml(result))
46  {
47  exprt new_expr = expr;
49  result = from_expr(ns, id, new_expr);
50 
51  // give up
52  if(!xmlt::is_printable_xml(result))
53  return {};
54  }
55 
56  return result;
57 }
58 
60 {
61  xmlt value_xml{"full_lhs_value"};
62 
63  const exprt &value = step.full_lhs_value;
64  if(value.is_nil())
65  return value_xml;
66 
67  const auto &lhs_object = step.get_lhs_object();
68  const irep_idt identifier =
69  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
70  value_xml.data = get_printable_xml(ns, identifier, value);
71 
72  const auto &bv_type = type_try_dynamic_cast<bitvector_typet>(value.type());
73  const auto &constant = expr_try_dynamic_cast<constant_exprt>(value);
74  if(bv_type && constant)
75  {
76  const auto width = bv_type->get_width();
77  // It is fine to pass `false` into the `is_signed` parameter, even for
78  // signed values, because the subsequent conversion to binary will result
79  // in the same value either way. E.g. if the value is `-1` for a signed 8
80  // bit value, this will convert to `255` which is `11111111` in binary,
81  // which is the desired result.
82  const auto binary_representation =
83  integer2binary(bvrep2integer(constant->get_value(), width, false), width);
84  value_xml.set_attribute("binary", binary_representation);
85  }
86  return value_xml;
87 }
88 
89 void convert(
90  const namespacet &ns,
91  const goto_tracet &goto_trace,
92  xmlt &dest)
93 {
94  dest=xmlt("goto_trace");
95 
96  source_locationt previous_source_location;
97 
98  for(const auto &step : goto_trace.steps)
99  {
100  const source_locationt &source_location=step.pc->source_location;
101 
102  xmlt xml_location;
103  if(source_location.is_not_nil() && !source_location.get_file().empty())
104  xml_location=xml(source_location);
105 
106  switch(step.type)
107  {
109  if(!step.cond_value)
110  {
111  xmlt &xml_failure=dest.new_element("failure");
112 
113  xml_failure.set_attribute_bool("hidden", step.hidden);
114  xml_failure.set_attribute("thread", std::to_string(step.thread_nr));
115  xml_failure.set_attribute("step_nr", std::to_string(step.step_nr));
116  xml_failure.set_attribute("reason", id2string(step.comment));
117  xml_failure.set_attribute("property", id2string(step.property_id));
118 
119  if(!xml_location.name.empty())
120  xml_failure.new_element().swap(xml_location);
121  }
122  break;
123 
126  {
127  auto lhs_object = step.get_lhs_object();
128  irep_idt identifier =
129  lhs_object.has_value() ? lhs_object->get_identifier() : irep_idt();
130  xmlt &xml_assignment = dest.new_element("assignment");
131 
132  if(!xml_location.name.empty())
133  xml_assignment.new_element().swap(xml_location);
134 
135  {
136  const symbolt *symbol;
137 
138  if(
139  lhs_object.has_value() &&
140  !ns.lookup(lhs_object->get_identifier(), symbol))
141  {
142  std::string type_string = from_type(ns, symbol->name, symbol->type);
143 
144  xml_assignment.set_attribute("mode", id2string(symbol->mode));
145  xml_assignment.set_attribute("identifier", id2string(symbol->name));
146  xml_assignment.set_attribute(
147  "base_name", id2string(symbol->base_name));
148  xml_assignment.set_attribute(
149  "display_name", id2string(symbol->display_name()));
150  xml_assignment.new_element("type").data = type_string;
151  }
152  }
153 
154  std::string full_lhs_string;
155 
156  if(step.full_lhs.is_not_nil())
157  full_lhs_string = get_printable_xml(ns, identifier, step.full_lhs);
158 
159  xml_assignment.new_element("full_lhs").data = full_lhs_string;
160  xml_assignment.new_element(full_lhs_value(step, ns));
161 
162  xml_assignment.set_attribute_bool("hidden", step.hidden);
163  xml_assignment.set_attribute("thread", std::to_string(step.thread_nr));
164  xml_assignment.set_attribute("step_nr", std::to_string(step.step_nr));
165 
166  xml_assignment.set_attribute(
167  "assignment_type",
168  step.assignment_type ==
170  ? "actual_parameter"
171  : "state");
172  break;
173  }
174 
176  {
177  printf_formattert printf_formatter(ns);
178  printf_formatter(id2string(step.format_string), step.io_args);
179  std::string text = printf_formatter.as_string();
180  xmlt &xml_output = dest.new_element("output");
181 
182  xml_output.new_element("text").data = text;
183 
184  xml_output.set_attribute_bool("hidden", step.hidden);
185  xml_output.set_attribute("thread", std::to_string(step.thread_nr));
186  xml_output.set_attribute("step_nr", std::to_string(step.step_nr));
187 
188  if(!xml_location.name.empty())
189  xml_output.new_element().swap(xml_location);
190 
191  for(const auto &arg : step.io_args)
192  {
193  xml_output.new_element("value").data =
194  get_printable_xml(ns, step.function_id, arg);
195  xml_output.new_element("value_expression").new_element(xml(arg, ns));
196  }
197  break;
198  }
199 
201  {
202  xmlt &xml_input = dest.new_element("input");
203  xml_input.new_element("input_id").data = id2string(step.io_id);
204 
205  xml_input.set_attribute_bool("hidden", step.hidden);
206  xml_input.set_attribute("thread", std::to_string(step.thread_nr));
207  xml_input.set_attribute("step_nr", std::to_string(step.step_nr));
208 
209  for(const auto &arg : step.io_args)
210  {
211  xml_input.new_element("value").data =
212  get_printable_xml(ns, step.function_id, arg);
213  xml_input.new_element("value_expression").new_element(xml(arg, ns));
214  }
215 
216  if(!xml_location.name.empty())
217  xml_input.new_element().swap(xml_location);
218  break;
219  }
220 
222  {
223  std::string tag = "function_call";
224  xmlt &xml_call_return = dest.new_element(tag);
225 
226  xml_call_return.set_attribute_bool("hidden", step.hidden);
227  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
228  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
229 
230  const symbolt &symbol = ns.lookup(step.called_function);
231  xmlt &xml_function = xml_call_return.new_element("function");
232  xml_function.set_attribute(
233  "display_name", id2string(symbol.display_name()));
234  xml_function.set_attribute("identifier", id2string(symbol.name));
235  xml_function.new_element() = xml(symbol.location);
236 
237  if(!xml_location.name.empty())
238  xml_call_return.new_element().swap(xml_location);
239  break;
240  }
241 
243  {
244  std::string tag = "function_return";
245  xmlt &xml_call_return = dest.new_element(tag);
246 
247  xml_call_return.set_attribute_bool("hidden", step.hidden);
248  xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
249  xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
250 
251  const symbolt &symbol = ns.lookup(step.called_function);
252  xmlt &xml_function = xml_call_return.new_element("function");
253  xml_function.set_attribute(
254  "display_name", id2string(symbol.display_name()));
255  xml_function.set_attribute("identifier", id2string(symbol.name));
256  xml_function.new_element() = xml(symbol.location);
257 
258  if(!xml_location.name.empty())
259  xml_call_return.new_element().swap(xml_location);
260  break;
261  }
262 
275  {
276  const auto default_step = ::default_step(step, previous_source_location);
277  if(default_step)
278  {
279  xmlt &xml_location_only =
281 
282  xml_location_only.set_attribute_bool("hidden", default_step->hidden);
283  xml_location_only.set_attribute(
284  "thread", std::to_string(default_step->thread_number));
285  xml_location_only.set_attribute(
286  "step_nr", std::to_string(default_step->step_number));
287 
288  xml_location_only.new_element(xml(default_step->location));
289  }
290 
291  break;
292  }
293  }
294 
295  if(source_location.is_not_nil() && !source_location.get_file().empty())
296  previous_source_location=source_location;
297  }
298 }
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:53
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:134
goto_trace_stept::get_lhs_object
optionalt< symbol_exprt > get_lhs_object() const
Definition: goto_trace.cpp:50
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
xmlt::is_printable_xml
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
convert
void convert(const namespacet &ns, const goto_tracet &goto_trace, xmlt &dest)
Definition: xml_goto_trace.cpp:89
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
to_string_constant
const string_constantt & to_string_constant(const exprt &expr)
Definition: string_constant.h:31
goto_tracet::steps
stepst steps
Definition: goto_trace.h:180
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
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:37
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:52
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:82
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:391
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
get_printable_xml
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....
Definition: xml_goto_trace.cpp:41
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
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
string_constantt::to_array_expr
array_exprt to_array_expr() const
convert string into array constant
Definition: string_constant.cpp:29
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
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:59
xmlt::swap
void swap(xmlt &xml)
Definition: xml.cpp:25
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:177
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
exprt::operands
operandst & operands()
Definition: expr.h:96
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
replace_string_constants_rec
static void replace_string_constants_rec(exprt &expr)
Rewrite all string constants to their array counterparts.
Definition: xml_goto_trace.cpp:28
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