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