cprover
xml_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expressions in XML
4 
5 Author: Daniel Kroening
6 
7  Date: November 2005
8 
9 \*******************************************************************/
10 
13 
14 #include "xml_expr.h"
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/expr.h>
20 #include <util/fixedbv.h>
21 #include <util/ieee_float.h>
22 #include <util/invariant.h>
23 #include <util/namespace.h>
24 #include <util/pointer_expr.h>
25 #include <util/xml.h>
26 
27 xmlt xml(const typet &type, const namespacet &ns)
28 {
29  xmlt result;
30 
31  if(type.id() == ID_unsignedbv)
32  {
33  result.name = "integer";
34  result.set_attribute("width", to_unsignedbv_type(type).get_width());
35  }
36  else if(type.id() == ID_signedbv)
37  {
38  result.name = "integer";
39  result.set_attribute("width", to_signedbv_type(type).get_width());
40  }
41  else if(type.id() == ID_floatbv)
42  {
43  result.name = "float";
44  result.set_attribute("width", to_floatbv_type(type).get_width());
45  }
46  else if(type.id() == ID_bv)
47  {
48  result.name = "integer";
49  result.set_attribute("width", to_bv_type(type).get_width());
50  }
51  else if(type.id() == ID_c_bit_field)
52  {
53  result.name = "integer";
54  result.set_attribute("width", to_c_bit_field_type(type).get_width());
55  }
56  else if(type.id() == ID_c_enum_tag)
57  {
58  // we return the base type
59  return xml(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
60  }
61  else if(type.id() == ID_fixedbv)
62  {
63  result.name = "fixed";
64  result.set_attribute("width", to_fixedbv_type(type).get_width());
65  }
66  else if(type.id() == ID_pointer)
67  {
68  result.name = "pointer";
69  result.new_element("subtype").new_element() =
70  xml(to_pointer_type(type).subtype(), ns);
71  }
72  else if(type.id() == ID_bool)
73  {
74  result.name = "boolean";
75  }
76  else if(type.id() == ID_array)
77  {
78  result.name = "array";
79  result.new_element("subtype").new_element() =
80  xml(to_array_type(type).subtype(), ns);
81  result.new_element("size").new_element() =
82  xml(to_array_type(type).size(), ns);
83  }
84  else if(type.id() == ID_vector)
85  {
86  result.name = "vector";
87  result.new_element("subtype").new_element() =
88  xml(to_vector_type(type).subtype(), ns);
89  result.new_element("size").new_element() =
90  xml(to_vector_type(type).size(), ns);
91  }
92  else if(type.id() == ID_struct)
93  {
94  result.name = "struct";
95  const struct_typet::componentst &components =
96  to_struct_type(type).components();
97  for(const auto &component : components)
98  {
99  xmlt &e = result.new_element("member");
100  e.set_attribute("name", id2string(component.get_name()));
101  e.new_element("type").new_element() = xml(component.type(), ns);
102  }
103  }
104  else if(type.id() == ID_struct_tag)
105  {
106  return xml(ns.follow_tag(to_struct_tag_type(type)), ns);
107  }
108  else if(type.id() == ID_union)
109  {
110  result.name = "union";
111  const union_typet::componentst &components =
112  to_union_type(type).components();
113  for(const auto &component : components)
114  {
115  xmlt &e = result.new_element("member");
116  e.set_attribute("name", id2string(component.get_name()));
117  e.new_element("type").new_element() = xml(component.type(), ns);
118  }
119  }
120  else if(type.id() == ID_union_tag)
121  {
122  return xml(ns.follow_tag(to_union_tag_type(type)), ns);
123  }
124  else
125  result.name = "unknown";
126 
127  return result;
128 }
129 
130 xmlt xml(const exprt &expr, const namespacet &ns)
131 {
132  xmlt result;
133 
134  if(expr.id() == ID_constant)
135  {
136  const auto &constant_expr = to_constant_expr(expr);
137  const auto &value = constant_expr.get_value();
138 
139  const typet &type = expr.type();
140 
141  if(
142  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
143  type.id() == ID_c_bit_field || type.id() == ID_c_bool)
144  {
145  mp_integer i = numeric_cast_v<mp_integer>(constant_expr);
146  std::size_t width = to_bitvector_type(type).get_width();
147 
148  result.name = "integer";
149  result.set_attribute("binary", integer2binary(i, width));
150  result.set_attribute("width", width);
151 
152  const typet &underlying_type = type.id() == ID_c_bit_field
153  ? to_c_bit_field_type(type).subtype()
154  : type;
155 
156  bool is_signed = underlying_type.id() == ID_signedbv;
157 
158  std::string sig = is_signed ? "" : "unsigned ";
159 
160  if(type.id() == ID_c_bool)
161  result.set_attribute("c_type", "_Bool");
162  else if(width == config.ansi_c.char_width)
163  result.set_attribute("c_type", sig + "char");
164  else if(width == config.ansi_c.int_width)
165  result.set_attribute("c_type", sig + "int");
166  else if(width == config.ansi_c.short_int_width)
167  result.set_attribute("c_type", sig + "short int");
168  else if(width == config.ansi_c.long_int_width)
169  result.set_attribute("c_type", sig + "long int");
170  else if(width == config.ansi_c.long_long_int_width)
171  result.set_attribute("c_type", sig + "long long int");
172 
173  result.data = integer2string(i);
174  }
175  else if(type.id() == ID_c_enum)
176  {
177  const auto width =
178  to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
179 
180  const auto integer_value = bvrep2integer(value, width, false);
181  result.name = "integer";
182  result.set_attribute("binary", integer2binary(integer_value, width));
183  result.set_attribute("width", width);
184  result.set_attribute("c_type", "enum");
185 
186  result.data = integer2string(integer_value);
187  }
188  else if(type.id() == ID_c_enum_tag)
189  {
190  constant_exprt tmp(
191  constant_expr.get_value(), ns.follow_tag(to_c_enum_tag_type(type)));
192  return xml(tmp, ns);
193  }
194  else if(type.id() == ID_bv)
195  {
196  result.name = "bitvector";
197  result.set_attribute("binary", constant_expr.get_string(ID_value));
198  }
199  else if(type.id() == ID_fixedbv)
200  {
201  const auto width = to_fixedbv_type(type).get_width();
202  result.name = "fixed";
203  result.set_attribute("width", width);
204  result.set_attribute(
205  "binary", integer2binary(bvrep2integer(value, width, false), width));
206  result.data = fixedbvt(constant_expr).to_ansi_c_string();
207  }
208  else if(type.id() == ID_floatbv)
209  {
210  const auto width = to_floatbv_type(type).get_width();
211  result.name = "float";
212  result.set_attribute("width", width);
213  result.set_attribute(
214  "binary", integer2binary(bvrep2integer(value, width, false), width));
215  result.data = ieee_floatt(constant_expr).to_ansi_c_string();
216  }
217  else if(type.id() == ID_pointer)
218  {
219  const auto width = to_pointer_type(type).get_width();
220  result.name = "pointer";
221  result.set_attribute(
222  "binary", integer2binary(bvrep2integer(value, width, false), width));
223  if(constant_expr.get(ID_value) == ID_NULL)
224  result.data = "NULL";
225  }
226  else if(type.id() == ID_bool)
227  {
228  result.name = "boolean";
229  result.set_attribute("binary", constant_expr.is_true() ? "1" : "0");
230  result.data = constant_expr.is_true() ? "TRUE" : "FALSE";
231  }
232  else
233  {
234  result.name = "unknown";
235  }
236  }
237  else if(expr.id() == ID_array)
238  {
239  result.name = "array";
240 
241  unsigned index = 0;
242 
243  forall_operands(it, expr)
244  {
245  xmlt &e = result.new_element("element");
246  e.set_attribute("index", index);
247  e.new_element(xml(*it, ns));
248  index++;
249  }
250  }
251  else if(expr.id() == ID_struct)
252  {
253  result.name = "struct";
254 
255  const typet &type = ns.follow(expr.type());
256 
257  // these are expected to have a struct type
258  if(type.id() == ID_struct)
259  {
260  const struct_typet &struct_type = to_struct_type(type);
261  const struct_typet::componentst &components = struct_type.components();
262  PRECONDITION(components.size() == expr.operands().size());
263 
264  for(unsigned m = 0; m < expr.operands().size(); m++)
265  {
266  xmlt &e = result.new_element("member");
267  e.new_element() = xml(expr.operands()[m], ns);
268  e.set_attribute("name", id2string(components[m].get_name()));
269  }
270  }
271  }
272  else if(expr.id() == ID_union)
273  {
274  const union_exprt &union_expr = to_union_expr(expr);
275  result.name = "union";
276 
277  xmlt &e = result.new_element("member");
278  e.new_element(xml(union_expr.op(), ns));
279  e.set_attribute("member_name", id2string(union_expr.get_component_name()));
280  }
281  else
282  result.name = "unknown";
283 
284  return result;
285 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
ieee_floatt
Definition: ieee_float.h:120
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
typet
The type of an expression, extends irept.
Definition: type.h:28
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
ieee_floatt::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: ieee_float.h:269
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
fixedbv.h
invariant.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1516
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1562
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
namespace.h
xml.h
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
expr.h
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:114
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
fixedbvt::to_ansi_c_string
std::string to_ansi_c_string() const
Definition: fixedbv.h:62
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
xmlt::name
std::string name
Definition: xml.h:39
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
pointer_expr.h
API to expression classes for Pointers.
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:116
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
xml
xmlt xml(const typet &type, const namespacet &ns)
Definition: xml_expr.cpp:27
xmlt
Definition: xml.h:21
config
configt config
Definition: config.cpp:24
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1524
to_c_bit_field_type
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: c_types.h:47
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:402
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:198
ieee_float.h
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:115
fixedbvt
Definition: fixedbv.h:42
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
exprt::operands
operandst & operands()
Definition: expr.h:96
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
xmlt::data
std::string data
Definition: xml.h:39
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:111
c_types.h
xml_expr.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:112
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106