cprover
json_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expressions in JSON
4 
5 Author: 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 
32 static 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 &&
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 
99 json_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 =
171  to_struct_type(type).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 =
188  to_union_type(type).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 
206 static 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 
224 json_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  {
230  const constant_exprt &constant_expr = to_constant_expr(expr);
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 =
241  type.id() == ID_c_bit_field ? to_c_bit_field_type(type).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  {
274  constant_exprt tmp(
275  to_constant_expr(expr).get_value(),
276  ns.follow_tag(to_c_enum_tag_type(type)));
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);
306  exprt simpl_expr = simplify_json_expr(expr);
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 &&
312  to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
313  {
314  result["data"] = json_stringt(value_string);
315  }
316  else if(simpl_expr.id() == ID_symbol)
317  {
318  const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
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  {
366  const struct_typet &struct_type = to_struct_type(type);
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)
Definition: base_type.cpp:109
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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 union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
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
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
bool value_is_zero_string() const
Definition: std_expr.cpp:16
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 & get(const irep_idt &name) const
Definition: irep.cpp:45
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
const exprt & op() const
Definition: std_expr.h:293
Union constructor from single element.
Definition: std_expr.h:1611
irep_idt get_component_name() const
Definition: std_expr.h:1619
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
Definition: expr_util.cpp:216
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
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 pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
#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 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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1657
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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 array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool NULL_is_zero
Definition: config.h:194