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 "arith_tools.h"
17 #include "config.h"
18 #include "expr.h"
19 #include "fixedbv.h"
20 #include "ieee_float.h"
21 #include "invariant.h"
22 #include "namespace.h"
23 #include "std_expr.h"
24 #include "xml.h"
25 
26 xmlt xml(const source_locationt &location)
27 {
28  xmlt result;
29 
30  result.name="location";
31 
32  if(!location.get_working_directory().empty())
33  result.set_attribute(
34  "working-directory", id2string(location.get_working_directory()));
35 
36  if(!location.get_file().empty())
37  result.set_attribute("file", id2string(location.get_file()));
38 
39  if(!location.get_line().empty())
40  result.set_attribute("line", id2string(location.get_line()));
41 
42  if(!location.get_column().empty())
43  result.set_attribute("column", id2string(location.get_column()));
44 
45  if(!location.get_function().empty())
46  result.set_attribute("function", id2string(location.get_function()));
47 
48  return result;
49 }
50 
52  const typet &type,
53  const namespacet &ns)
54 {
55  if(type.id() == ID_symbol_type)
56  return xml(ns.follow(type), ns);
57 
58  xmlt result;
59 
60  if(type.id()==ID_unsignedbv)
61  {
62  result.name="integer";
63  result.set_attribute("width", to_unsignedbv_type(type).get_width());
64  }
65  else if(type.id()==ID_signedbv)
66  {
67  result.name="integer";
68  result.set_attribute("width", to_signedbv_type(type).get_width());
69  }
70  else if(type.id()==ID_floatbv)
71  {
72  result.name="float";
73  result.set_attribute("width", to_floatbv_type(type).get_width());
74  }
75  else if(type.id()==ID_bv)
76  {
77  result.name="integer";
78  result.set_attribute("width", to_bv_type(type).get_width());
79  }
80  else if(type.id()==ID_c_bit_field)
81  {
82  result.name="integer";
83  result.set_attribute("width", to_c_bit_field_type(type).get_width());
84  }
85  else if(type.id()==ID_c_enum_tag)
86  {
87  // we return the base type
88  return xml(
89  to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(), ns);
90  }
91  else if(type.id()==ID_fixedbv)
92  {
93  result.name="fixed";
94  result.set_attribute("width", to_fixedbv_type(type).get_width());
95  }
96  else if(type.id()==ID_pointer)
97  {
98  result.name="pointer";
99  result.new_element("subtype").new_element() =
100  xml(to_pointer_type(type).subtype(), ns);
101  }
102  else if(type.id()==ID_bool)
103  {
104  result.name="boolean";
105  }
106  else if(type.id()==ID_array)
107  {
108  result.name="array";
109  result.new_element("subtype").new_element() =
110  xml(to_array_type(type).subtype(), ns);
111  }
112  else if(type.id()==ID_vector)
113  {
114  result.name="vector";
115  result.new_element("subtype").new_element() =
116  xml(to_vector_type(type).subtype(), ns);
117  result.new_element("size").new_element()=
118  xml(to_vector_type(type).size(), ns);
119  }
120  else if(type.id()==ID_struct)
121  {
122  result.name="struct";
123  const struct_typet::componentst &components=
124  to_struct_type(type).components();
125  for(const auto &component : components)
126  {
127  xmlt &e=result.new_element("member");
128  e.set_attribute("name", id2string(component.get_name()));
129  e.new_element("type").new_element()=xml(component.type(), ns);
130  }
131  }
132  else if(type.id()==ID_union)
133  {
134  result.name="union";
135  const union_typet::componentst &components=
136  to_union_type(type).components();
137  for(const auto &component : components)
138  {
139  xmlt &e=result.new_element("member");
140  e.set_attribute("name", id2string(component.get_name()));
141  e.new_element("type").new_element()=xml(component.type(), ns);
142  }
143  }
144  else
145  result.name="unknown";
146 
147  return result;
148 }
149 
151  const exprt &expr,
152  const namespacet &ns)
153 {
154  xmlt result;
155 
156  const typet &type=ns.follow(expr.type());
157 
158  if(expr.id()==ID_constant)
159  {
160  if(type.id()==ID_unsignedbv ||
161  type.id()==ID_signedbv ||
162  type.id()==ID_c_bit_field)
163  {
164  std::size_t width=to_bitvector_type(type).get_width();
165 
166  result.name="integer";
167  result.set_attribute(
168  "binary", integer2binary(numeric_cast_v<mp_integer>(expr), width));
169  result.set_attribute("width", width);
170 
171  const typet &underlying_type = type.id() == ID_c_bit_field
172  ? to_c_bit_field_type(type).subtype()
173  : type;
174 
175  bool is_signed=underlying_type.id()==ID_signedbv;
176 
177  std::string sig=is_signed?"":"unsigned ";
178 
179  if(width==config.ansi_c.char_width)
180  result.set_attribute("c_type", sig+"char");
181  else if(width==config.ansi_c.int_width)
182  result.set_attribute("c_type", sig+"int");
183  else if(width==config.ansi_c.short_int_width)
184  result.set_attribute("c_type", sig+"short int");
185  else if(width==config.ansi_c.long_int_width)
186  result.set_attribute("c_type", sig+"long int");
187  else if(width==config.ansi_c.long_long_int_width)
188  result.set_attribute("c_type", sig+"long long int");
189 
190  mp_integer i;
191  if(!to_integer(to_constant_expr(expr), i))
192  result.data=integer2string(i);
193  }
194  else if(type.id()==ID_c_enum)
195  {
196  result.name="integer";
197  result.set_attribute("binary", expr.get_string(ID_value));
198  result.set_attribute(
199  "width", to_c_enum_type(type).subtype().get_string(ID_width));
200  result.set_attribute("c_type", "enum");
201 
202  mp_integer i;
203  if(!to_integer(to_constant_expr(expr), i))
204  result.data=integer2string(i);
205  }
206  else if(type.id()==ID_c_enum_tag)
207  {
208  constant_exprt tmp(
209  to_constant_expr(expr).get_value(),
210  ns.follow_tag(to_c_enum_tag_type(type)));
211  return xml(tmp, ns);
212  }
213  else if(type.id()==ID_bv)
214  {
215  result.name="bitvector";
216  result.set_attribute("binary", expr.get_string(ID_value));
217  }
218  else if(type.id()==ID_fixedbv)
219  {
220  result.name="fixed";
221  result.set_attribute("width", type.get_string(ID_width));
222  result.set_attribute("binary", expr.get_string(ID_value));
224  }
225  else if(type.id()==ID_floatbv)
226  {
227  result.name="float";
228  result.set_attribute("width", type.get_string(ID_width));
229  result.set_attribute("binary", expr.get_string(ID_value));
231  }
232  else if(type.id()==ID_pointer)
233  {
234  result.name="pointer";
235  result.set_attribute("binary", expr.get_string(ID_value));
236  if(expr.get(ID_value)==ID_NULL)
237  result.data="NULL";
238  }
239  else if(type.id()==ID_bool)
240  {
241  result.name="boolean";
242  result.set_attribute("binary", expr.is_true()?"1":"0");
243  result.data=expr.is_true()?"TRUE":"FALSE";
244  }
245  else if(type.id()==ID_c_bool)
246  {
247  result.name="integer";
248  result.set_attribute("c_type", "_Bool");
249  result.set_attribute("binary", expr.get_string(ID_value));
250  const mp_integer b = numeric_cast_v<mp_integer>(expr);
251  result.data=integer2string(b);
252  }
253  else
254  {
255  result.name="unknown";
256  }
257  }
258  else if(expr.id()==ID_array)
259  {
260  result.name="array";
261 
262  unsigned index=0;
263 
264  forall_operands(it, expr)
265  {
266  xmlt &e=result.new_element("element");
267  e.set_attribute("index", index);
268  e.new_element(xml(*it, ns));
269  index++;
270  }
271  }
272  else if(expr.id()==ID_struct)
273  {
274  result.name="struct";
275 
276  // these are expected to have a struct type
277  if(type.id()==ID_struct)
278  {
279  const struct_typet &struct_type=to_struct_type(type);
280  const struct_typet::componentst &components=struct_type.components();
281  PRECONDITION(components.size() == expr.operands().size());
282 
283  for(unsigned m=0; m<expr.operands().size(); m++)
284  {
285  xmlt &e=result.new_element("member");
286  e.new_element()=xml(expr.operands()[m], ns);
287  e.set_attribute("name", id2string(components[m].get_name()));
288  }
289  }
290  }
291  else if(expr.id()==ID_union)
292  {
293  const union_exprt &union_expr = to_union_expr(expr);
294  result.name="union";
295 
296  xmlt &e=result.new_element("member");
297  e.new_element(xml(union_expr.op(), ns));
298  e.set_attribute("member_name", id2string(union_expr.get_component_name()));
299  }
300  else
301  result.name="unknown";
302 
303  return result;
304 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
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:737
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
ieee_floatt
Definition: ieee_float.h:119
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
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:349
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:697
typet
The type of an expression, extends irept.
Definition: type.h:27
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:22
is_signed
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
fixedbv.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:52
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1890
invariant.h
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
configt::ansi_c
struct configt::ansi_ct ansi_c
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
namespace.h
xml.h
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:47
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1205
expr.h
configt::ansi_ct::char_width
std::size_t char_width
Definition: config.h:33
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
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
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
xmlt::name
std::string name
Definition: xml.h:30
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:1491
configt::ansi_ct::long_long_int_width
std::size_t long_long_int_width
Definition: config.h:35
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
xmlt
Definition: xml.h:18
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1863
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
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:1316
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
config.h
configt::ansi_ct::short_int_width
std::size_t short_int_width
Definition: config.h:34
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
fixedbvt
Definition: fixedbv.h:41
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
exprt::operands
operandst & operands()
Definition: expr.h:78
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
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:4384
xmlt::data
std::string data
Definition: xml.h:30
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:42
std_expr.h
configt::ansi_ct::int_width
std::size_t int_width
Definition: config.h:30
xml_expr.h
configt::ansi_ct::long_int_width
std::size_t long_int_width
Definition: config.h:31
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106