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 "namespace.h"
15 #include "expr.h"
16 #include "json.h"
17 #include "arith_tools.h"
18 #include "ieee_float.h"
19 #include "fixedbv.h"
20 #include "std_expr.h"
21 #include "config.h"
22 #include "identifier.h"
23 #include "invariant.h"
24 
25 #include <langapi/mode.h>
26 #include <langapi/language.h>
27 
28 #include <memory>
29 
31  const exprt &src,
32  const namespacet &ns)
33 {
34  if(src.id()==ID_constant)
35  {
36  const typet &type=ns.follow(src.type());
37 
38  if(type.id()==ID_pointer)
39  {
40  const constant_exprt &c = to_constant_expr(src);
41 
42  if(
43  c.get_value() != ID_NULL &&
45  src.operands().size() == 1 &&
46  to_unary_expr(src).op().id() != ID_constant)
47  // try to simplify the constant pointer
48  {
49  return simplify_json_expr(to_unary_expr(src).op(), ns);
50  }
51  }
52  }
53  else if(
54  src.id() == ID_address_of &&
55  to_address_of_expr(src).object().id() == ID_member &&
56  id2string(
57  to_member_expr(to_address_of_expr(src).object()).get_component_name())
58  .find("@") != std::string::npos)
59  {
60  // simplify expressions of the form &member_expr(object, @class_identifier)
61  return simplify_json_expr(to_address_of_expr(src).object(), ns);
62  }
63  else if(
64  src.id() == ID_address_of &&
65  to_address_of_expr(src).object().id() == ID_index &&
66  to_index_expr(to_address_of_expr(src).object()).index().id() ==
67  ID_constant &&
68  to_constant_expr(to_index_expr(to_address_of_expr(src).object()).index())
70  {
71  // simplify expressions of the form &array[0]
72  return simplify_json_expr(
73  to_index_expr(to_address_of_expr(src).object()).array(), ns);
74  }
75  else if(src.id()==ID_member &&
76  id2string(
77  to_member_expr(src).get_component_name())
78  .find("@")!=std::string::npos)
79  {
80  // simplify expressions of the form member_expr(object, @class_identifier)
81  return simplify_json_expr(to_member_expr(src).struct_op(), ns);
82  }
83 
84  return src;
85 }
86 
88 {
89  json_objectt result;
90 
91  if(!location.get_working_directory().empty())
92  result["workingDirectory"] = json_stringt(location.get_working_directory());
93 
94  if(!location.get_file().empty())
95  result["file"] = json_stringt(location.get_file());
96 
97  if(!location.get_line().empty())
98  result["line"] = json_stringt(location.get_line());
99 
100  if(!location.get_column().empty())
101  result["column"] = json_stringt(location.get_column());
102 
103  if(!location.get_function().empty())
104  result["function"] = json_stringt(location.get_function());
105 
106  if(!location.get_java_bytecode_index().empty())
107  result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
108 
109  return result;
110 }
111 
120  const typet &type,
121  const namespacet &ns,
122  const irep_idt &mode)
123 {
124  if(type.id() == ID_symbol_type)
125  return json(ns.follow(type), ns, mode);
126 
127  json_objectt result;
128 
129  if(type.id()==ID_unsignedbv)
130  {
131  result["name"]=json_stringt("integer");
132  result["width"]=
133  json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
134  }
135  else if(type.id()==ID_signedbv)
136  {
137  result["name"]=json_stringt("integer");
138  result["width"]=
139  json_numbert(std::to_string(to_signedbv_type(type).get_width()));
140  }
141  else if(type.id()==ID_floatbv)
142  {
143  result["name"]=json_stringt("float");
144  result["width"]=
145  json_numbert(std::to_string(to_floatbv_type(type).get_width()));
146  }
147  else if(type.id()==ID_bv)
148  {
149  result["name"]=json_stringt("integer");
150  result["width"]=json_numbert(std::to_string(to_bv_type(type).get_width()));
151  }
152  else if(type.id()==ID_c_bit_field)
153  {
154  result["name"]=json_stringt("integer");
155  result["width"]=
156  json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
157  }
158  else if(type.id()==ID_c_enum_tag)
159  {
160  // we return the base type
161  return json(
162  to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(),
163  ns,
164  mode);
165  }
166  else if(type.id()==ID_fixedbv)
167  {
168  result["name"]=json_stringt("fixed");
169  result["width"]=
170  json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
171  }
172  else if(type.id()==ID_pointer)
173  {
174  result["name"]=json_stringt("pointer");
175  result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
176  }
177  else if(type.id()==ID_bool)
178  {
179  result["name"]=json_stringt("boolean");
180  }
181  else if(type.id()==ID_array)
182  {
183  result["name"]=json_stringt("array");
184  result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
185  }
186  else if(type.id()==ID_vector)
187  {
188  result["name"]=json_stringt("vector");
189  result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
190  result["size"]=json(to_vector_type(type).size(), ns, mode);
191  }
192  else if(type.id()==ID_struct)
193  {
194  result["name"]=json_stringt("struct");
195  json_arrayt &members=result["members"].make_array();
196  const struct_typet::componentst &components=
197  to_struct_type(type).components();
198  for(const auto &component : components)
199  {
200  json_objectt &e=members.push_back().make_object();
201  e["name"] = json_stringt(component.get_name());
202  e["type"]=json(component.type(), ns, mode);
203  }
204  }
205  else if(type.id()==ID_union)
206  {
207  result["name"]=json_stringt("union");
208  json_arrayt &members=result["members"].make_array();
209  const union_typet::componentst &components=
210  to_union_type(type).components();
211  for(const auto &component : components)
212  {
213  json_objectt &e=members.push_back().make_object();
214  e["name"] = json_stringt(component.get_name());
215  e["type"]=json(component.type(), ns, mode);
216  }
217  }
218  else
219  result["name"]=json_stringt("unknown");
220 
221  return result;
222 }
223 
224 static std::string binary(const constant_exprt &src)
225 {
226  const auto width = to_bitvector_type(src.type()).get_width();
227  const auto int_val = bvrep2integer(src.get_value(), width, false);
228  return integer2binary(int_val, width);
229 }
230 
239  const exprt &expr,
240  const namespacet &ns,
241  const irep_idt &mode)
242 {
243  json_objectt result;
244 
245  const typet &type=ns.follow(expr.type());
246 
247  if(expr.id()==ID_constant)
248  {
249  std::unique_ptr<languaget> lang;
250  if(mode==ID_unknown)
251  lang=std::unique_ptr<languaget>(get_default_language());
252  else
253  {
254  lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
255  if(!lang)
256  lang=std::unique_ptr<languaget>(get_default_language());
257  }
258 
259  const typet &underlying_type =
260  type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
261 
262  std::string type_string;
263  bool error=lang->from_type(underlying_type, type_string, ns);
264  CHECK_RETURN(!error);
265 
266  std::string value_string;
267  lang->from_expr(expr, value_string, ns);
268 
269  const constant_exprt &constant_expr=to_constant_expr(expr);
270  if(type.id()==ID_unsignedbv ||
271  type.id()==ID_signedbv ||
272  type.id()==ID_c_bit_field)
273  {
274  std::size_t width=to_bitvector_type(type).get_width();
275 
276  result["name"]=json_stringt("integer");
277  result["binary"] = json_stringt(binary(constant_expr));
278  result["width"]=json_numbert(std::to_string(width));
279  result["type"]=json_stringt(type_string);
280  result["data"]=json_stringt(value_string);
281  }
282  else if(type.id()==ID_c_enum)
283  {
284  result["name"]=json_stringt("integer");
285  result["binary"] = json_stringt(binary(constant_expr));
286  result["width"] =
287  json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
288  result["type"]=json_stringt("enum");
289  result["data"]=json_stringt(value_string);
290  }
291  else if(type.id()==ID_c_enum_tag)
292  {
293  constant_exprt tmp(
294  to_constant_expr(expr).get_value(),
295  ns.follow_tag(to_c_enum_tag_type(type)));
296  return json(tmp, ns, mode);
297  }
298  else if(type.id()==ID_bv)
299  {
300  result["name"]=json_stringt("bitvector");
301  result["binary"] = json_stringt(binary(constant_expr));
302  }
303  else if(type.id()==ID_fixedbv)
304  {
305  result["name"]=json_stringt("fixed");
306  result["width"]=json_numbert(type.get_string(ID_width));
307  result["binary"] = json_stringt(binary(constant_expr));
308  result["data"]=
309  json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
310  }
311  else if(type.id()==ID_floatbv)
312  {
313  result["name"]=json_stringt("float");
314  result["width"]=json_numbert(type.get_string(ID_width));
315  result["binary"] = json_stringt(binary(constant_expr));
316  result["data"]=
317  json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
318  }
319  else if(type.id()==ID_pointer)
320  {
321  result["name"]=json_stringt("pointer");
322  result["type"]=json_stringt(type_string);
323  exprt simpl_expr=simplify_json_expr(expr, ns);
324  if(
325  simpl_expr.get(ID_value) == ID_NULL ||
326  // remove typecast on NULL
327  (simpl_expr.id() == ID_constant &&
328  simpl_expr.type().id() == ID_pointer &&
329  to_unary_expr(simpl_expr).op().get(ID_value) == ID_NULL))
330  {
331  result["data"]=json_stringt(value_string);
332  }
333  else if(simpl_expr.id()==ID_symbol)
334  {
335  const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();
336  identifiert identifier(id2string(ptr_id));
338  !identifier.components.empty(),
339  "pointer identifier should have non-empty components");
340  result["data"]=json_stringt(identifier.components.back());
341  }
342  }
343  else if(type.id()==ID_bool)
344  {
345  result["name"]=json_stringt("boolean");
346  result["binary"]=json_stringt(expr.is_true()?"1":"0");
347  result["data"]=jsont::json_boolean(expr.is_true());
348  }
349  else if(type.id()==ID_c_bool)
350  {
351  result["name"]=json_stringt("integer");
352  result["width"]=json_numbert(type.get_string(ID_width));
353  result["type"]=json_stringt(type_string);
354  result["binary"]=json_stringt(expr.get_string(ID_value));
355  result["data"]=json_stringt(value_string);
356  }
357  else if(type.id()==ID_string)
358  {
359  result["name"]=json_stringt("string");
360  result["data"] = json_stringt(constant_expr.get_value());
361  }
362  else
363  {
364  result["name"]=json_stringt("unknown");
365  }
366  }
367  else if(expr.id()==ID_array)
368  {
369  result["name"]=json_stringt("array");
370  json_arrayt &elements=result["elements"].make_array();
371 
372  std::size_t index=0;
373 
374  forall_operands(it, expr)
375  {
376  json_objectt &e=elements.push_back().make_object();
377  e["index"]=json_numbert(std::to_string(index));
378  e["value"]=json(*it, ns, mode);
379  index++;
380  }
381  }
382  else if(expr.id()==ID_struct)
383  {
384  result["name"]=json_stringt("struct");
385 
386  // these are expected to have a struct type
387  if(type.id()==ID_struct)
388  {
389  const struct_typet &struct_type=to_struct_type(type);
390  const struct_typet::componentst &components=struct_type.components();
392  components.size()==expr.operands().size(),
393  "number of struct components should match with its type");
394 
395  json_arrayt &members=result["members"].make_array();
396  for(std::size_t m=0; m<expr.operands().size(); m++)
397  {
398  json_objectt &e=members.push_back().make_object();
399  e["value"]=json(expr.operands()[m], ns, mode);
400  e["name"] = json_stringt(components[m].get_name());
401  }
402  }
403  }
404  else if(expr.id()==ID_union)
405  {
406  result["name"]=json_stringt("union");
407 
408  const union_exprt &union_expr=to_union_expr(expr);
409  json_objectt &e=result["member"].make_object();
410  e["value"]=json(union_expr.op(), ns, mode);
411  e["name"] = json_stringt(union_expr.get_component_name());
412  }
413  else
414  result["name"]=json_stringt("unknown");
415 
416  return result;
417 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:737
json_numbert
Definition: json.h:235
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
ieee_floatt
Definition: ieee_float.h:119
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:395
configt::ansi_ct::NULL_is_zero
bool NULL_is_zero
Definition: config.h:87
typet::subtype
const typet & subtype() const
Definition: type.h:38
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
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:349
address_of_exprt::object
exprt & object()
Definition: std_expr.h:3265
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:485
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:697
typet
The type of an expression, extends irept.
Definition: type.h:27
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
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
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
source_locationt::get_column
const irep_idt & get_column() const
Definition: source_location.h:52
exprt
Base class for all expressions.
Definition: expr.h:54
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:203
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:1890
invariant.h
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
configt::ansi_c
struct configt::ansi_ct ansi_c
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
namespace.h
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:47
to_bv_type
const bv_typet & to_bv_type(const typet &type)
Cast a typet to a bv_typet.
Definition: std_types.h:1205
json_arrayt
Definition: json.h:146
expr.h
json_objectt
Definition: json.h:244
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: std_types.h:1380
to_unsignedbv_type
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
Definition: std_types.h:1262
identifiert
Definition: identifier.h:18
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:3282
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
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
identifier.h
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
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:176
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:1491
language.h
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
json_expr.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
irept::id
const irep_idt & id() const
Definition: irep.h:259
dstringt::empty
bool empty() const
Definition: dstring.h:75
jsont::make_array
json_arrayt & make_array()
Definition: json.h:284
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
union_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:1863
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:425
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
source_locationt::get_java_bytecode_index
const irep_idt & get_java_bytecode_index() const
Definition: source_location.h:82
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:20
simplify_json_expr
static exprt simplify_json_expr(const exprt &src, const namespacet &ns)
Definition: json_expr.cpp:30
ieee_float.h
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1316
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
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:1442
config.h
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
fixedbvt
Definition: fixedbv.h:41
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
exprt::operands
operandst & operands()
Definition: expr.h:78
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
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:4384
source_locationt::get_working_directory
const irep_idt & get_working_directory() const
Definition: source_location.h:42
std_expr.h
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:85
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:163
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
get_default_language
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:138
json_stringt
Definition: json.h:214
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470