cprover
Loading...
Searching...
No Matches
xml_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expressions in XML
4
5Author: 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_util.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
27xmlt 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 underlying type
59 return xml(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type(), 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).base_type(), 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).element_type(), 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).element_type(), 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 =
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 =
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
130xmlt xml(const exprt &expr, const namespacet &ns)
131{
132 xmlt result;
133
134 if(expr.is_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 =
153 type.id() == ID_c_bit_field
155 : type;
156
157 bool is_signed = underlying_type.id() == ID_signedbv;
158
159 std::string sig = is_signed ? "" : "unsigned ";
160
161 if(type.id() == ID_c_bool)
162 result.set_attribute("c_type", "_Bool");
163 else if(width == config.ansi_c.char_width)
164 result.set_attribute("c_type", sig + "char");
165 else if(width == config.ansi_c.int_width)
166 result.set_attribute("c_type", sig + "int");
167 else if(width == config.ansi_c.short_int_width)
168 result.set_attribute("c_type", sig + "short int");
169 else if(width == config.ansi_c.long_int_width)
170 result.set_attribute("c_type", sig + "long int");
171 else if(width == config.ansi_c.long_long_int_width)
172 result.set_attribute("c_type", sig + "long long int");
173
174 result.data = integer2string(i);
175 }
176 else if(type.id() == ID_c_enum)
177 {
178 const auto width =
179 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
180
181 const auto integer_value = bvrep2integer(value, width, false);
182 result.name = "integer";
183 result.set_attribute("binary", integer2binary(integer_value, width));
184 result.set_attribute("width", width);
185 result.set_attribute("c_type", "enum");
186
187 result.data = integer2string(integer_value);
188 }
189 else if(type.id() == ID_c_enum_tag)
190 {
191 constant_exprt tmp(
192 constant_expr.get_value(), ns.follow_tag(to_c_enum_tag_type(type)));
193 return xml(tmp, ns);
194 }
195 else if(type.id() == ID_bv)
196 {
197 result.name = "bitvector";
198 result.set_attribute("binary", constant_expr.get_string(ID_value));
199 }
200 else if(type.id() == ID_fixedbv)
201 {
202 const auto width = to_fixedbv_type(type).get_width();
203 result.name = "fixed";
204 result.set_attribute("width", width);
205 result.set_attribute(
206 "binary", integer2binary(bvrep2integer(value, width, false), width));
207 result.data = fixedbvt(constant_expr).to_ansi_c_string();
208 }
209 else if(type.id() == ID_floatbv)
210 {
211 const auto width = to_floatbv_type(type).get_width();
212 result.name = "float";
213 result.set_attribute("width", width);
214 result.set_attribute(
215 "binary", integer2binary(bvrep2integer(value, width, false), width));
216 result.data = ieee_floatt(constant_expr).to_ansi_c_string();
217 }
218 else if(type.id() == ID_pointer)
219 {
220 const auto width = to_pointer_type(type).get_width();
221 result.name = "pointer";
222 result.set_attribute(
223 "binary", integer2binary(bvrep2integer(value, width, false), width));
224 if(is_null_pointer(constant_expr))
225 result.data = "NULL";
226 }
227 else if(type.id() == ID_bool)
228 {
229 result.name = "boolean";
230 result.set_attribute("binary", constant_expr.is_true() ? "1" : "0");
231 result.data = constant_expr.is_true() ? "TRUE" : "FALSE";
232 }
233 else
234 {
235 result.name = "unknown";
236 }
237 }
238 else if(expr.id() == ID_array)
239 {
240 result.name = "array";
241
242 unsigned index = 0;
243
244 for(const auto &op : expr.operands())
245 {
246 xmlt &e = result.new_element("element");
247 e.set_attribute("index", index);
248 e.new_element(xml(op, ns));
249 index++;
250 }
251 }
252 else if(expr.id() == ID_struct)
253 {
254 result.name = "struct";
255
256 const struct_typet &struct_type =
257 expr.type().id() == ID_struct_tag
259 : to_struct_type(expr.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 else if(expr.id() == ID_union)
271 {
272 const union_exprt &union_expr = to_union_expr(expr);
273 result.name = "union";
274
275 xmlt &e = result.new_element("member");
276 e.new_element(xml(union_expr.op(), ns));
277 e.set_attribute("member_name", id2string(union_expr.get_component_name()));
278 }
279 else
280 result.name = "unknown";
281
282 return result;
283}
configt config
Definition config.cpp:25
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
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:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
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:377
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
std::size_t get_width() const
Definition std_types.h:920
const typet & underlying_type() const
Definition c_types.h:30
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2987
Base class for all expressions.
Definition expr.h:56
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
std::string to_ansi_c_string() const
Definition fixedbv.h:62
std::string to_ansi_c_string() const
Definition ieee_float.h:280
const irep_idt & id() const
Definition irep.h:388
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The type of an expression, extends irept.
Definition type.h:29
const exprt & op() const
Definition std_expr.h:391
Union constructor from single element.
Definition std_expr.h:1765
irep_idt get_component_name() const
Definition std_expr.h:1773
Definition xml.h:21
xmlt & new_element(const std::string &key)
Definition xml.h:95
void set_attribute(const std::string &attribute, unsigned value)
Definition xml.cpp:198
std::string data
Definition xml.h:39
std::string name
Definition xml.h:39
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
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:103
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:80
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1811
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3037
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1104
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
std::size_t long_long_int_width
Definition config.h:142
std::size_t long_int_width
Definition config.h:138
std::size_t short_int_width
Definition config.h:141
std::size_t char_width
Definition config.h:140
std::size_t int_width
Definition config.h:137
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45
xmlt xml(const typet &type, const namespacet &ns)
Definition xml_expr.cpp:27