cprover
Loading...
Searching...
No Matches
xml_goto_trace.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Traces of GOTO Programs
4
5Author: Daniel Kroening
6
7 Date: November 2005
8
9\*******************************************************************/
10
13
14#include "xml_goto_trace.h"
15
16#include <util/arith_tools.h>
18#include <util/symbol.h>
19#include <util/xml_irep.h>
20
22
23#include "goto_trace.h"
24#include "printf_formatter.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
41static std::string
42get_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
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
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
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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
xmlt & new_element(const std::string &key)
Definition: xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
void swap(xmlt &xml)
Definition: xml.cpp:25
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 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.