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