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.h>
18 #include <util/expr_util.h>
19 #include <util/fixedbv.h>
20 #include <util/identifier.h>
21 #include <util/ieee_float.h>
22 #include <util/invariant.h>
23 #include <util/json.h>
24 #include <util/namespace.h>
25 #include <util/pointer_expr.h>
26 #include <util/std_expr.h>
27 
28 #include <langapi/language.h>
29 #include <langapi/mode.h>
30 
31 #include <memory>
32 
33 static exprt simplify_json_expr(const exprt &src)
34 {
35  if(src.id() == ID_constant)
36  {
37  if(src.type().id() == ID_pointer)
38  {
39  const constant_exprt &c = to_constant_expr(src);
40 
41  if(
42  c.get_value() != ID_NULL &&
44  src.operands().size() == 1 &&
45  to_unary_expr(src).op().id() != ID_constant)
46  // try to simplify the constant pointer
47  {
48  return simplify_json_expr(to_unary_expr(src).op());
49  }
50  }
51  }
52  else if(src.id() == ID_typecast)
53  {
54  return simplify_json_expr(to_typecast_expr(src).op());
55  }
56  else if(src.id() == ID_address_of)
57  {
58  const exprt &object = skip_typecast(to_address_of_expr(src).object());
59 
60  if(object.id() == ID_symbol)
61  {
62  // simplify expressions of the form &symbol
63  return simplify_json_expr(object);
64  }
65  else if(
66  object.id() == ID_member &&
67  id2string(to_member_expr(object).get_component_name()).find("@") !=
68  std::string::npos)
69  {
70  // simplify expressions of the form &member(object, @class_identifier)
71  return simplify_json_expr(object);
72  }
73  else if(
74  object.id() == ID_index &&
75  to_index_expr(object).index().id() == ID_constant &&
76  to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
77  {
78  // simplify expressions of the form &array[0]
79  return simplify_json_expr(to_index_expr(object).array());
80  }
81  }
82  else if(
83  src.id() == ID_member &&
84  id2string(to_member_expr(src).get_component_name()).find("@") !=
85  std::string::npos)
86  {
87  // simplify expressions of the form member_expr(object, @class_identifier)
88  return simplify_json_expr(to_member_expr(src).struct_op());
89  }
90 
91  return src;
92 }
93 
100 json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
101 {
102  json_objectt result;
103 
104  if(type.id() == ID_unsignedbv)
105  {
106  result["name"] = json_stringt("integer");
107  result["width"] =
108  json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
109  }
110  else if(type.id() == ID_signedbv)
111  {
112  result["name"] = json_stringt("integer");
113  result["width"] =
114  json_numbert(std::to_string(to_signedbv_type(type).get_width()));
115  }
116  else if(type.id() == ID_floatbv)
117  {
118  result["name"] = json_stringt("float");
119  result["width"] =
120  json_numbert(std::to_string(to_floatbv_type(type).get_width()));
121  }
122  else if(type.id() == ID_bv)
123  {
124  result["name"] = json_stringt("integer");
125  result["width"] =
126  json_numbert(std::to_string(to_bv_type(type).get_width()));
127  }
128  else if(type.id() == ID_c_bit_field)
129  {
130  result["name"] = json_stringt("integer");
131  result["width"] =
132  json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
133  }
134  else if(type.id() == ID_c_enum_tag)
135  {
136  // we return the base type
137  return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), 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).subtype(), 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).subtype(), 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).subtype(), 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  else
212  width = to_bitvector_type(src.type()).get_width();
213  const auto int_val = bvrep2integer(src.get_value(), width, false);
214  return integer2binary(int_val, width);
215 }
216 
223 json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
224 {
225  json_objectt result;
226 
227  if(expr.id() == ID_constant)
228  {
229  const constant_exprt &constant_expr = to_constant_expr(expr);
230 
231  const typet &type = expr.type();
232 
233  std::unique_ptr<languaget> lang;
234  if(mode != ID_unknown)
235  lang = std::unique_ptr<languaget>(get_language_from_mode(mode));
236  if(!lang)
237  lang = std::unique_ptr<languaget>(get_default_language());
238 
239  const typet &underlying_type =
240  type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
241 
242  std::string type_string;
243  bool error = lang->from_type(underlying_type, type_string, ns);
244  CHECK_RETURN(!error);
245 
246  std::string value_string;
247  lang->from_expr(expr, value_string, ns);
248 
249  if(
250  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
251  type.id() == ID_c_bit_field || type.id() == ID_c_bool)
252  {
253  std::size_t width = to_bitvector_type(type).get_width();
254 
255  result["name"] = json_stringt("integer");
256  result["binary"] = json_stringt(binary(constant_expr));
257  result["width"] = json_numbert(std::to_string(width));
258  result["type"] = json_stringt(type_string);
259  result["data"] = json_stringt(value_string);
260  }
261  else if(type.id() == ID_c_enum)
262  {
263  result["name"] = json_stringt("integer");
264  result["binary"] = json_stringt(binary(constant_expr));
265  result["width"] = json_numbert(std::to_string(
266  to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
267  result["type"] = json_stringt("enum");
268  result["data"] = json_stringt(value_string);
269  }
270  else if(type.id() == ID_c_enum_tag)
271  {
272  constant_exprt tmp(
273  to_constant_expr(expr).get_value(),
274  ns.follow_tag(to_c_enum_tag_type(type)));
275  return json(tmp, ns, mode);
276  }
277  else if(type.id() == ID_bv)
278  {
279  result["name"] = json_stringt("bitvector");
280  result["binary"] = json_stringt(binary(constant_expr));
281  }
282  else if(type.id() == ID_fixedbv)
283  {
284  result["name"] = json_stringt("fixed");
285  result["width"] =
286  json_numbert(std::to_string(to_bitvector_type(type).get_width()));
287  result["binary"] = json_stringt(binary(constant_expr));
288  result["data"] =
289  json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
290  }
291  else if(type.id() == ID_floatbv)
292  {
293  result["name"] = json_stringt("float");
294  result["width"] =
295  json_numbert(std::to_string(to_bitvector_type(type).get_width()));
296  result["binary"] = json_stringt(binary(constant_expr));
297  result["data"] =
298  json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
299  }
300  else if(type.id() == ID_pointer)
301  {
302  result["name"] = json_stringt("pointer");
303  result["type"] = json_stringt(type_string);
304  exprt simpl_expr = simplify_json_expr(expr);
305  if(
306  simpl_expr.get(ID_value) == ID_NULL ||
307  // remove typecast on NULL
308  (simpl_expr.id() == ID_constant &&
309  simpl_expr.type().id() == ID_pointer &&
310  to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
311  {
312  result["data"] = json_stringt(value_string);
313  }
314  else if(simpl_expr.id() == ID_symbol)
315  {
316  const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
317  identifiert identifier(id2string(ptr_id));
319  !identifier.components.empty(),
320  "pointer identifier should have non-empty components");
321  result["data"] = json_stringt(identifier.components.back());
322  }
323  }
324  else if(type.id() == ID_bool)
325  {
326  result["name"] = json_stringt("boolean");
327  result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
328  result["data"] = jsont::json_boolean(expr.is_true());
329  }
330  else if(type.id() == ID_string)
331  {
332  result["name"] = json_stringt("string");
333  result["data"] = json_stringt(constant_expr.get_value());
334  }
335  else
336  {
337  result["name"] = json_stringt("unknown");
338  }
339  }
340  else if(expr.id() == ID_array)
341  {
342  result["name"] = json_stringt("array");
343  json_arrayt &elements = result["elements"].make_array();
344 
345  std::size_t index = 0;
346 
347  forall_operands(it, expr)
348  {
349  json_objectt e{{"index", json_numbert(std::to_string(index))},
350  {"value", json(*it, ns, mode)}};
351  elements.push_back(std::move(e));
352  index++;
353  }
354  }
355  else if(expr.id() == ID_struct)
356  {
357  result["name"] = json_stringt("struct");
358 
359  const typet &type = ns.follow(expr.type());
360 
361  // these are expected to have a struct type
362  if(type.id() == ID_struct)
363  {
364  const struct_typet &struct_type = to_struct_type(type);
365  const struct_typet::componentst &components = struct_type.components();
367  components.size() == expr.operands().size(),
368  "number of struct components should match with its type");
369 
370  json_arrayt &members = result["members"].make_array();
371  for(std::size_t m = 0; m < expr.operands().size(); m++)
372  {
373  json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
374  {"name", json_stringt(components[m].get_name())}};
375  members.push_back(std::move(e));
376  }
377  }
378  }
379  else if(expr.id() == ID_union)
380  {
381  result["name"] = json_stringt("union");
382 
383  const union_exprt &union_expr = to_union_expr(expr);
384  result["member"] =
385  json_objectt({{"value", json(union_expr.op(), ns, mode)},
386  {"name", json_stringt(union_expr.get_component_name())}});
387  }
388  else
389  result["name"] = json_stringt("unknown");
390 
391  return result;
392 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:141
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: bitvector_types.h:191
ieee_floatt
Definition: ieee_float.h:120
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:168
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
identifiert::components
componentst components
Definition: identifier.h:30
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: bitvector_types.h:367
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
fixedbv.h
invariant.h
union_exprt
Union constructor from single element.
Definition: std_expr.h:1516
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:134
mode.h
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: bitvector_types.h:82
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1562
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
configt::ansi_c
struct configt::ansi_ct ansi_c
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
namespace.h
json_arrayt
Definition: json.h:165
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
expr.h
json_objectt
Definition: json.h:300
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
identifiert
Definition: identifier.h:19
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
languaget::from_type
virtual bool from_type(const typet &type, std::string &code, const namespacet &ns)
Formats the given type in a language-specific way.
Definition: language.cpp:46
identifier.h
to_c_enum_tag_type
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:317
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
languaget::from_expr
virtual bool from_expr(const exprt &expr, std::string &code, const namespacet &ns)
Formats the given expression in a language-specific way.
Definition: language.cpp:37
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
pointer_expr.h
API to expression classes for Pointers.
language.h
Abstract interface to support a programming language.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
json_expr.h
Expressions in JSON.
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:468
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:293
config
configt config
Definition: config.cpp:24
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: bitvector_types.h:241
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1524
to_c_bit_field_type
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:47
expr_util.h
Deprecated expression utility functions.
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:402
simplify_json_expr
static exprt simplify_json_expr(const exprt &src)
Definition: json_expr.cpp:33
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
ieee_float.h
json
json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
Output a CBMC type in json.
Definition: json_expr.cpp:100
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
json.h
config.h
fixedbvt
Definition: fixedbv.h:42
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:994
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2611
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
exprt::operands
operandst & operands()
Definition: expr.h:96
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
std_expr.h
API to expression classes.
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:97
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
c_types.h
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:138
json_stringt
Definition: json.h:270
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700