cprover
Loading...
Searching...
No Matches
json_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expressions in JSON
4
5Author: Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "json_expr.h"
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/config.h>
17#include <util/expr_util.h>
18#include <util/fixedbv.h>
19#include <util/identifier.h>
20#include <util/ieee_float.h>
21#include <util/invariant.h>
22#include <util/json.h>
23#include <util/namespace.h>
24#include <util/pointer_expr.h>
25#include <util/std_expr.h>
26
27#include <langapi/language.h>
28#include <langapi/mode.h>
29
30#include <memory>
31
32static exprt simplify_json_expr(const exprt &src)
33{
34 if(src.id() == ID_constant)
35 {
36 if(src.type().id() == ID_pointer)
37 {
38 const constant_exprt &c = to_constant_expr(src);
39
40 if(
41 c.get_value() != ID_NULL &&
42 (!c.value_is_zero_string() || !config.ansi_c.NULL_is_zero) &&
43 src.operands().size() == 1 &&
44 to_unary_expr(src).op().id() != ID_constant)
45 // try to simplify the constant pointer
46 {
47 return simplify_json_expr(to_unary_expr(src).op());
48 }
49 }
50 }
51 else if(src.id() == ID_typecast)
52 {
53 return simplify_json_expr(to_typecast_expr(src).op());
54 }
55 else if(src.id() == ID_address_of)
56 {
57 const exprt &object = skip_typecast(to_address_of_expr(src).object());
58
59 if(object.id() == ID_symbol)
60 {
61 // simplify expressions of the form &symbol
62 return simplify_json_expr(object);
63 }
64 else if(
65 object.id() == ID_member &&
66 id2string(to_member_expr(object).get_component_name()).find("@") !=
67 std::string::npos)
68 {
69 // simplify expressions of the form &member(object, @class_identifier)
70 return simplify_json_expr(object);
71 }
72 else if(
73 object.id() == ID_index &&
74 to_index_expr(object).index().id() == ID_constant &&
75 to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
76 {
77 // simplify expressions of the form &array[0]
78 return simplify_json_expr(to_index_expr(object).array());
79 }
80 }
81 else if(
82 src.id() == ID_member &&
83 id2string(to_member_expr(src).get_component_name()).find("@") !=
84 std::string::npos)
85 {
86 // simplify expressions of the form member_expr(object, @class_identifier)
87 return simplify_json_expr(to_member_expr(src).struct_op());
88 }
89
90 return src;
91}
92
99json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
100{
101 json_objectt result;
102
103 if(type.id() == ID_unsignedbv)
104 {
105 result["name"] = json_stringt("integer");
106 result["width"] =
107 json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
108 }
109 else if(type.id() == ID_signedbv)
110 {
111 result["name"] = json_stringt("integer");
112 result["width"] =
113 json_numbert(std::to_string(to_signedbv_type(type).get_width()));
114 }
115 else if(type.id() == ID_floatbv)
116 {
117 result["name"] = json_stringt("float");
118 result["width"] =
119 json_numbert(std::to_string(to_floatbv_type(type).get_width()));
120 }
121 else if(type.id() == ID_bv)
122 {
123 result["name"] = json_stringt("integer");
124 result["width"] =
125 json_numbert(std::to_string(to_bv_type(type).get_width()));
126 }
127 else if(type.id() == ID_c_bit_field)
128 {
129 result["name"] = json_stringt("integer");
130 result["width"] =
131 json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
132 }
133 else if(type.id() == ID_c_enum_tag)
134 {
135 // we return the underlying type
136 return json(
137 ns.follow_tag(to_c_enum_tag_type(type)).underlying_type(), ns, mode);
138 }
139 else if(type.id() == ID_fixedbv)
140 {
141 result["name"] = json_stringt("fixed");
142 result["width"] =
143 json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
144 }
145 else if(type.id() == ID_pointer)
146 {
147 result["name"] = json_stringt("pointer");
148 result["subtype"] = json(to_pointer_type(type).base_type(), ns, mode);
149 }
150 else if(type.id() == ID_bool)
151 {
152 result["name"] = json_stringt("boolean");
153 }
154 else if(type.id() == ID_array)
155 {
156 result["name"] = json_stringt("array");
157 result["subtype"] = json(to_array_type(type).element_type(), ns, mode);
158 result["size"] = json(to_array_type(type).size(), ns, mode);
159 }
160 else if(type.id() == ID_vector)
161 {
162 result["name"] = json_stringt("vector");
163 result["subtype"] = json(to_vector_type(type).element_type(), ns, mode);
164 result["size"] = json(to_vector_type(type).size(), ns, mode);
165 }
166 else if(type.id() == ID_struct)
167 {
168 result["name"] = json_stringt("struct");
169 json_arrayt &members = result["members"].make_array();
170 const struct_typet::componentst &components =
172 for(const auto &component : components)
173 {
174 json_objectt e{{"name", json_stringt(component.get_name())},
175 {"type", json(component.type(), ns, mode)}};
176 members.push_back(std::move(e));
177 }
178 }
179 else if(type.id() == ID_struct_tag)
180 {
181 return json(ns.follow_tag(to_struct_tag_type(type)), ns, mode);
182 }
183 else if(type.id() == ID_union)
184 {
185 result["name"] = json_stringt("union");
186 json_arrayt &members = result["members"].make_array();
187 const union_typet::componentst &components =
189 for(const auto &component : components)
190 {
191 json_objectt e{{"name", json_stringt(component.get_name())},
192 {"type", json(component.type(), ns, mode)}};
193 members.push_back(std::move(e));
194 }
195 }
196 else if(type.id() == ID_union_tag)
197 {
198 return json(ns.follow_tag(to_union_tag_type(type)), ns, mode);
199 }
200 else
201 result["name"] = json_stringt("unknown");
202
203 return result;
204}
205
206static std::string binary(const constant_exprt &src)
207{
208 std::size_t width;
209 if(src.type().id() == ID_c_enum)
211 .get_width();
212 else
213 width = to_bitvector_type(src.type()).get_width();
214 const auto int_val = bvrep2integer(src.get_value(), width, false);
215 return integer2binary(int_val, width);
216}
217
224json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
225{
226 json_objectt result;
227
228 if(expr.id() == ID_constant)
229 {
231
232 const typet &type = expr.type();
233
234 std::unique_ptr<languaget> lang;
235 if(mode != ID_unknown)
236 lang = std::unique_ptr<languaget>(get_language_from_mode(mode));
237 if(!lang)
238 lang = std::unique_ptr<languaget>(get_default_language());
239
240 const typet &underlying_type =
242 : type;
243
244 std::string type_string;
245 bool error = lang->from_type(underlying_type, type_string, ns);
246 CHECK_RETURN(!error);
247
248 std::string value_string;
249 lang->from_expr(expr, value_string, ns);
250
251 if(
252 type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
253 type.id() == ID_c_bit_field || type.id() == ID_c_bool)
254 {
255 std::size_t width = to_bitvector_type(type).get_width();
256
257 result["name"] = json_stringt("integer");
258 result["binary"] = json_stringt(binary(constant_expr));
259 result["width"] = json_numbert(std::to_string(width));
260 result["type"] = json_stringt(type_string);
261 result["data"] = json_stringt(value_string);
262 }
263 else if(type.id() == ID_c_enum)
264 {
265 result["name"] = json_stringt("integer");
266 result["binary"] = json_stringt(binary(constant_expr));
267 result["width"] = json_numbert(std::to_string(
268 to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()));
269 result["type"] = json_stringt("enum");
270 result["data"] = json_stringt(value_string);
271 }
272 else if(type.id() == ID_c_enum_tag)
273 {
275 to_constant_expr(expr).get_value(),
277 return json(tmp, ns, mode);
278 }
279 else if(type.id() == ID_bv)
280 {
281 result["name"] = json_stringt("bitvector");
282 result["binary"] = json_stringt(binary(constant_expr));
283 }
284 else if(type.id() == ID_fixedbv)
285 {
286 result["name"] = json_stringt("fixed");
287 result["width"] =
288 json_numbert(std::to_string(to_bitvector_type(type).get_width()));
289 result["binary"] = json_stringt(binary(constant_expr));
290 result["data"] =
291 json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
292 }
293 else if(type.id() == ID_floatbv)
294 {
295 result["name"] = json_stringt("float");
296 result["width"] =
297 json_numbert(std::to_string(to_bitvector_type(type).get_width()));
298 result["binary"] = json_stringt(binary(constant_expr));
299 result["data"] =
300 json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
301 }
302 else if(type.id() == ID_pointer)
303 {
304 result["name"] = json_stringt("pointer");
305 result["type"] = json_stringt(type_string);
307 if(
308 simpl_expr.get(ID_value) == ID_NULL ||
309 // remove typecast on NULL
310 (simpl_expr.id() == ID_constant &&
311 simpl_expr.type().id() == ID_pointer &&
313 {
314 result["data"] = json_stringt(value_string);
315 }
316 else if(simpl_expr.id() == ID_symbol)
317 {
319 identifiert identifier(id2string(ptr_id));
321 !identifier.components.empty(),
322 "pointer identifier should have non-empty components");
323 result["data"] = json_stringt(identifier.components.back());
324 }
325 }
326 else if(type.id() == ID_bool)
327 {
328 result["name"] = json_stringt("boolean");
329 result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
330 result["data"] = jsont::json_boolean(expr.is_true());
331 }
332 else if(type.id() == ID_string)
333 {
334 result["name"] = json_stringt("string");
335 result["data"] = json_stringt(constant_expr.get_value());
336 }
337 else
338 {
339 result["name"] = json_stringt("unknown");
340 }
341 }
342 else if(expr.id() == ID_array)
343 {
344 result["name"] = json_stringt("array");
345 json_arrayt &elements = result["elements"].make_array();
346
347 std::size_t index = 0;
348
349 forall_operands(it, expr)
350 {
351 json_objectt e{{"index", json_numbert(std::to_string(index))},
352 {"value", json(*it, ns, mode)}};
353 elements.push_back(std::move(e));
354 index++;
355 }
356 }
357 else if(expr.id() == ID_struct)
358 {
359 result["name"] = json_stringt("struct");
360
361 const typet &type = ns.follow(expr.type());
362
363 // these are expected to have a struct type
364 if(type.id() == ID_struct)
365 {
367 const struct_typet::componentst &components = struct_type.components();
369 components.size() == expr.operands().size(),
370 "number of struct components should match with its type");
371
372 json_arrayt &members = result["members"].make_array();
373 for(std::size_t m = 0; m < expr.operands().size(); m++)
374 {
375 json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
376 {"name", json_stringt(components[m].get_name())}};
377 members.push_back(std::move(e));
378 }
379 }
380 }
381 else if(expr.id() == ID_union)
382 {
383 result["name"] = json_stringt("union");
384
385 const union_exprt &union_expr = to_union_expr(expr);
386 result["member"] =
387 json_objectt({{"value", json(union_expr.op(), ns, mode)},
388 {"name", json_stringt(union_expr.get_component_name())}});
389 }
390 else
391 result["name"] = json_stringt("unknown");
392
393 return result;
394}
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
void base_type(typet &type, const namespacet &ns)
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:302
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:344
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:202
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
std::size_t get_width() const
Definition std_types.h:864
const typet & underlying_type() const
Definition c_types.h:30
const typet & underlying_type() const
Definition c_types.h:274
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition std_expr.h:2807
const irep_idt & get_value() const
Definition std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
componentst components
Definition identifier.h:30
const irep_idt & id() const
Definition irep.h:396
jsont & push_back(const jsont &json)
Definition json.h:212
json_arrayt & make_array()
Definition json.h:420
static jsont json_boolean(bool value)
Definition json.h:97
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
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:91
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
const irep_idt & get_identifier() const
Definition std_expr.h:109
The type of an expression, extends irept.
Definition type.h:29
Union constructor from single element.
Definition std_expr.h:1611
configt config
Definition config.cpp:25
#define forall_operands(it, expr)
Definition expr.h:18
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
static std::string binary(const constant_exprt &src)
static exprt simplify_json_expr(const exprt &src)
Definition json_expr.cpp:32
json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
Output a CBMC type in json.
Definition json_expr.cpp:99
Expressions in JSON.
Abstract interface to support a programming language.
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition mode.cpp:51
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition mode.cpp:139
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition mp_arith.cpp:64
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:48
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:328
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2751
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition std_expr.h:1657
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1040
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:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:832