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/config.h>
16 #include <util/expr.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/std_expr.h>
25 
26 #include <langapi/language.h>
27 #include <langapi/mode.h>
28 
29 #include <memory>
30 
31 static exprt simplify_json_expr(const exprt &src)
32 {
33  if(src.id() == ID_constant)
34  {
35  if(src.type().id() == ID_pointer)
36  {
37  const constant_exprt &c = to_constant_expr(src);
38 
39  if(
40  c.get_value() != ID_NULL &&
42  src.operands().size() == 1 &&
43  to_unary_expr(src).op().id() != ID_constant)
44  // try to simplify the constant pointer
45  {
46  return simplify_json_expr(to_unary_expr(src).op());
47  }
48  }
49  }
50  else if(src.id() == ID_typecast)
51  {
52  return simplify_json_expr(to_typecast_expr(src).op());
53  }
54  else if(src.id() == ID_address_of)
55  {
56  const exprt &object = skip_typecast(to_address_of_expr(src).object());
57 
58  if(object.id() == ID_symbol)
59  {
60  // simplify expressions of the form &symbol
61  return simplify_json_expr(object);
62  }
63  else if(
64  object.id() == ID_member &&
65  id2string(to_member_expr(object).get_component_name()).find("@") !=
66  std::string::npos)
67  {
68  // simplify expressions of the form &member(object, @class_identifier)
69  return simplify_json_expr(object);
70  }
71  else if(
72  object.id() == ID_index &&
73  to_index_expr(object).index().id() == ID_constant &&
74  to_constant_expr(to_index_expr(object).index()).value_is_zero_string())
75  {
76  // simplify expressions of the form &array[0]
77  return simplify_json_expr(to_index_expr(object).array());
78  }
79  }
80  else if(
81  src.id() == ID_member &&
82  id2string(to_member_expr(src).get_component_name()).find("@") !=
83  std::string::npos)
84  {
85  // simplify expressions of the form member_expr(object, @class_identifier)
86  return simplify_json_expr(to_member_expr(src).struct_op());
87  }
88 
89  return src;
90 }
91 
98 json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
99 {
100  json_objectt result;
101 
102  if(type.id() == ID_unsignedbv)
103  {
104  result["name"] = json_stringt("integer");
105  result["width"] =
106  json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
107  }
108  else if(type.id() == ID_signedbv)
109  {
110  result["name"] = json_stringt("integer");
111  result["width"] =
112  json_numbert(std::to_string(to_signedbv_type(type).get_width()));
113  }
114  else if(type.id() == ID_floatbv)
115  {
116  result["name"] = json_stringt("float");
117  result["width"] =
118  json_numbert(std::to_string(to_floatbv_type(type).get_width()));
119  }
120  else if(type.id() == ID_bv)
121  {
122  result["name"] = json_stringt("integer");
123  result["width"] =
124  json_numbert(std::to_string(to_bv_type(type).get_width()));
125  }
126  else if(type.id() == ID_c_bit_field)
127  {
128  result["name"] = json_stringt("integer");
129  result["width"] =
130  json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
131  }
132  else if(type.id() == ID_c_enum_tag)
133  {
134  // we return the base type
135  return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
136  }
137  else if(type.id() == ID_fixedbv)
138  {
139  result["name"] = json_stringt("fixed");
140  result["width"] =
141  json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
142  }
143  else if(type.id() == ID_pointer)
144  {
145  result["name"] = json_stringt("pointer");
146  result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
147  }
148  else if(type.id() == ID_bool)
149  {
150  result["name"] = json_stringt("boolean");
151  }
152  else if(type.id() == ID_array)
153  {
154  result["name"] = json_stringt("array");
155  result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
156  result["size"] = json(to_array_type(type).size(), ns, mode);
157  }
158  else if(type.id() == ID_vector)
159  {
160  result["name"] = json_stringt("vector");
161  result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
162  result["size"] = json(to_vector_type(type).size(), ns, mode);
163  }
164  else if(type.id() == ID_struct)
165  {
166  result["name"] = json_stringt("struct");
167  json_arrayt &members = result["members"].make_array();
168  const struct_typet::componentst &components =
169  to_struct_type(type).components();
170  for(const auto &component : components)
171  {
172  json_objectt e{{"name", json_stringt(component.get_name())},
173  {"type", json(component.type(), ns, mode)}};
174  members.push_back(std::move(e));
175  }
176  }
177  else if(type.id() == ID_struct_tag)
178  {
179  return json(ns.follow_tag(to_struct_tag_type(type)), ns, mode);
180  }
181  else if(type.id() == ID_union)
182  {
183  result["name"] = json_stringt("union");
184  json_arrayt &members = result["members"].make_array();
185  const union_typet::componentst &components =
186  to_union_type(type).components();
187  for(const auto &component : components)
188  {
189  json_objectt e{{"name", json_stringt(component.get_name())},
190  {"type", json(component.type(), ns, mode)}};
191  members.push_back(std::move(e));
192  }
193  }
194  else if(type.id() == ID_union_tag)
195  {
196  return json(ns.follow_tag(to_union_tag_type(type)), ns, mode);
197  }
198  else
199  result["name"] = json_stringt("unknown");
200 
201  return result;
202 }
203 
204 static std::string binary(const constant_exprt &src)
205 {
206  std::size_t width;
207  if(src.type().id() == ID_c_enum)
209  else
210  width = to_bitvector_type(src.type()).get_width();
211  const auto int_val = bvrep2integer(src.get_value(), width, false);
212  return integer2binary(int_val, width);
213 }
214 
221 json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
222 {
223  json_objectt result;
224 
225  if(expr.id() == ID_constant)
226  {
227  const constant_exprt &constant_expr = to_constant_expr(expr);
228 
229  const typet &type = expr.type();
230 
231  std::unique_ptr<languaget> lang;
232  if(mode != ID_unknown)
233  lang = std::unique_ptr<languaget>(get_language_from_mode(mode));
234  if(!lang)
235  lang = std::unique_ptr<languaget>(get_default_language());
236 
237  const typet &underlying_type =
238  type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
239 
240  std::string type_string;
241  bool error = lang->from_type(underlying_type, type_string, ns);
242  CHECK_RETURN(!error);
243 
244  std::string value_string;
245  lang->from_expr(expr, value_string, ns);
246 
247  if(
248  type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
249  type.id() == ID_c_bit_field || type.id() == ID_c_bool)
250  {
251  std::size_t width = to_bitvector_type(type).get_width();
252 
253  result["name"] = json_stringt("integer");
254  result["binary"] = json_stringt(binary(constant_expr));
255  result["width"] = json_numbert(std::to_string(width));
256  result["type"] = json_stringt(type_string);
257  result["data"] = json_stringt(value_string);
258  }
259  else if(type.id() == ID_c_enum)
260  {
261  result["name"] = json_stringt("integer");
262  result["binary"] = json_stringt(binary(constant_expr));
263  result["width"] = json_numbert(std::to_string(
264  to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
265  result["type"] = json_stringt("enum");
266  result["data"] = json_stringt(value_string);
267  }
268  else if(type.id() == ID_c_enum_tag)
269  {
270  constant_exprt tmp(
271  to_constant_expr(expr).get_value(),
272  ns.follow_tag(to_c_enum_tag_type(type)));
273  return json(tmp, ns, mode);
274  }
275  else if(type.id() == ID_bv)
276  {
277  result["name"] = json_stringt("bitvector");
278  result["binary"] = json_stringt(binary(constant_expr));
279  }
280  else if(type.id() == ID_fixedbv)
281  {
282  result["name"] = json_stringt("fixed");
283  result["width"] =
284  json_numbert(std::to_string(to_bitvector_type(type).get_width()));
285  result["binary"] = json_stringt(binary(constant_expr));
286  result["data"] =
287  json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
288  }
289  else if(type.id() == ID_floatbv)
290  {
291  result["name"] = json_stringt("float");
292  result["width"] =
293  json_numbert(std::to_string(to_bitvector_type(type).get_width()));
294  result["binary"] = json_stringt(binary(constant_expr));
295  result["data"] =
296  json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
297  }
298  else if(type.id() == ID_pointer)
299  {
300  result["name"] = json_stringt("pointer");
301  result["type"] = json_stringt(type_string);
302  exprt simpl_expr = simplify_json_expr(expr);
303  if(
304  simpl_expr.get(ID_value) == ID_NULL ||
305  // remove typecast on NULL
306  (simpl_expr.id() == ID_constant &&
307  simpl_expr.type().id() == ID_pointer &&
308  to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
309  {
310  result["data"] = json_stringt(value_string);
311  }
312  else if(simpl_expr.id() == ID_symbol)
313  {
314  const irep_idt &ptr_id = to_symbol_expr(simpl_expr).get_identifier();
315  identifiert identifier(id2string(ptr_id));
317  !identifier.components.empty(),
318  "pointer identifier should have non-empty components");
319  result["data"] = json_stringt(identifier.components.back());
320  }
321  }
322  else if(type.id() == ID_bool)
323  {
324  result["name"] = json_stringt("boolean");
325  result["binary"] = json_stringt(expr.is_true() ? "1" : "0");
326  result["data"] = jsont::json_boolean(expr.is_true());
327  }
328  else if(type.id() == ID_string)
329  {
330  result["name"] = json_stringt("string");
331  result["data"] = json_stringt(constant_expr.get_value());
332  }
333  else
334  {
335  result["name"] = json_stringt("unknown");
336  }
337  }
338  else if(expr.id() == ID_array)
339  {
340  result["name"] = json_stringt("array");
341  json_arrayt &elements = result["elements"].make_array();
342 
343  std::size_t index = 0;
344 
345  forall_operands(it, expr)
346  {
347  json_objectt e{{"index", json_numbert(std::to_string(index))},
348  {"value", json(*it, ns, mode)}};
349  elements.push_back(std::move(e));
350  index++;
351  }
352  }
353  else if(expr.id() == ID_struct)
354  {
355  result["name"] = json_stringt("struct");
356 
357  const typet &type = ns.follow(expr.type());
358 
359  // these are expected to have a struct type
360  if(type.id() == ID_struct)
361  {
362  const struct_typet &struct_type = to_struct_type(type);
363  const struct_typet::componentst &components = struct_type.components();
365  components.size() == expr.operands().size(),
366  "number of struct components should match with its type");
367 
368  json_arrayt &members = result["members"].make_array();
369  for(std::size_t m = 0; m < expr.operands().size(); m++)
370  {
371  json_objectt e{{"value", json(expr.operands()[m], ns, mode)},
372  {"name", json_stringt(components[m].get_name())}};
373  members.push_back(std::move(e));
374  }
375  }
376  }
377  else if(expr.id() == ID_union)
378  {
379  result["name"] = json_stringt("union");
380 
381  const union_exprt &union_expr = to_union_expr(expr);
382  result["member"] =
383  json_objectt({{"value", json(union_expr.op(), ns, mode)},
384  {"name", json_stringt(union_expr.get_component_name())}});
385  }
386  else
387  result["name"] = json_stringt("unknown");
388 
389  return result;
390 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
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: std_types.h:721
json_numbert
Definition: json.h:291
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:316
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:88
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:217
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:303
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:29
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
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:1567
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
mode.h
to_union_expr
const union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
Definition: std_expr.h:1613
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
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:92
configt::ansi_c
struct configt::ansi_ct ansi_c
namespace.h
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1139
json_arrayt
Definition: json.h:165
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:81
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1362
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1248
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
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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
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:111
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: std_types.h:1471
language.h
Abstract interface to support a programming language.
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:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
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:515
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
config
configt config
Definition: config.cpp:24
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1575
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:401
simplify_json_expr
static exprt simplify_json_expr(const exprt &src)
Definition: json_expr.cpp:31
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
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:2047
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:98
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
json.h
to_floatbv_type
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1424
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:1775
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
exprt::operands
operandst & operands()
Definition: expr.h:95
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
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:3906
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:3914
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
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:3939