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