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 irep_idt &value=to_constant_expr(src).get_value();
41 
42  if(value!=ID_NULL &&
43  (value!=std::string(value.size(), '0') ||
45  src.operands().size()==1 &&
46  src.op0().id()!=ID_constant)
47  // try to simplify the constant pointer
48  return simplify_json_expr(src.op0(), ns);
49  }
50  }
51  else if(src.id()==ID_address_of &&
52  src.operands().size()==1 &&
53  src.op0().id()==ID_member &&
55  src.op0()).get_component_name()).find("@")!=std::string::npos)
56  {
57  // simplify expressions of the form &member_expr(object, @class_identifier)
58  return simplify_json_expr(src.op0(), ns);
59  }
60  else if(src.id()==ID_address_of &&
61  src.operands().size()==1 &&
62  src.op0().id()==ID_index &&
63  to_index_expr(src.op0()).index().id()==ID_constant &&
65  to_index_expr(src.op0()).index()).value_is_zero_string())
66  {
67  // simplify expressions of the form &array[0]
68  return simplify_json_expr(to_index_expr(src.op0()).array(), ns);
69  }
70  else if(src.id()==ID_member &&
71  src.operands().size()==1 &&
72  id2string(
73  to_member_expr(src).get_component_name())
74  .find("@")!=std::string::npos)
75  {
76  // simplify expressions of the form member_expr(object, @class_identifier)
77  return simplify_json_expr(src.op0(), ns);
78  }
79 
80  return src;
81 }
82 
84 {
85  json_objectt result;
86 
87  if(!location.get_working_directory().empty())
88  result["workingDirectory"] = json_stringt(location.get_working_directory());
89 
90  if(!location.get_file().empty())
91  result["file"] = json_stringt(location.get_file());
92 
93  if(!location.get_line().empty())
94  result["line"] = json_stringt(location.get_line());
95 
96  if(!location.get_column().empty())
97  result["column"] = json_stringt(location.get_column());
98 
99  if(!location.get_function().empty())
100  result["function"] = json_stringt(location.get_function());
101 
102  if(!location.get_java_bytecode_index().empty())
103  result["bytecodeIndex"] = json_stringt(location.get_java_bytecode_index());
104 
105  return result;
106 }
107 
116  const typet &type,
117  const namespacet &ns,
118  const irep_idt &mode)
119 {
120  if(type.id()==ID_symbol)
121  return json(ns.follow(type), ns, mode);
122 
123  json_objectt result;
124 
125  if(type.id()==ID_unsignedbv)
126  {
127  result["name"]=json_stringt("integer");
128  result["width"]=
129  json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
130  }
131  else if(type.id()==ID_signedbv)
132  {
133  result["name"]=json_stringt("integer");
134  result["width"]=
135  json_numbert(std::to_string(to_signedbv_type(type).get_width()));
136  }
137  else if(type.id()==ID_floatbv)
138  {
139  result["name"]=json_stringt("float");
140  result["width"]=
141  json_numbert(std::to_string(to_floatbv_type(type).get_width()));
142  }
143  else if(type.id()==ID_bv)
144  {
145  result["name"]=json_stringt("integer");
146  result["width"]=json_numbert(std::to_string(to_bv_type(type).get_width()));
147  }
148  else if(type.id()==ID_c_bit_field)
149  {
150  result["name"]=json_stringt("integer");
151  result["width"]=
152  json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
153  }
154  else if(type.id()==ID_c_enum_tag)
155  {
156  // we return the base type
157  return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
158  }
159  else if(type.id()==ID_fixedbv)
160  {
161  result["name"]=json_stringt("fixed");
162  result["width"]=
163  json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
164  }
165  else if(type.id()==ID_pointer)
166  {
167  result["name"]=json_stringt("pointer");
168  result["subtype"]=json(type.subtype(), ns, mode);
169  }
170  else if(type.id()==ID_bool)
171  {
172  result["name"]=json_stringt("boolean");
173  }
174  else if(type.id()==ID_array)
175  {
176  result["name"]=json_stringt("array");
177  result["subtype"]=json(type.subtype(), ns, mode);
178  }
179  else if(type.id()==ID_vector)
180  {
181  result["name"]=json_stringt("vector");
182  result["subtype"]=json(type.subtype(), ns, mode);
183  result["size"]=json(to_vector_type(type).size(), ns, mode);
184  }
185  else if(type.id()==ID_struct)
186  {
187  result["name"]=json_stringt("struct");
188  json_arrayt &members=result["members"].make_array();
189  const struct_typet::componentst &components=
190  to_struct_type(type).components();
191  for(const auto &component : components)
192  {
193  json_objectt &e=members.push_back().make_object();
194  e["name"] = json_stringt(component.get_name());
195  e["type"]=json(component.type(), ns, mode);
196  }
197  }
198  else if(type.id()==ID_union)
199  {
200  result["name"]=json_stringt("union");
201  json_arrayt &members=result["members"].make_array();
202  const union_typet::componentst &components=
203  to_union_type(type).components();
204  for(const auto &component : components)
205  {
206  json_objectt &e=members.push_back().make_object();
207  e["name"] = json_stringt(component.get_name());
208  e["type"]=json(component.type(), ns, mode);
209  }
210  }
211  else
212  result["name"]=json_stringt("unknown");
213 
214  return result;
215 }
216 
225  const exprt &expr,
226  const namespacet &ns,
227  const irep_idt &mode)
228 {
229  json_objectt result;
230 
231  const typet &type=ns.follow(expr.type());
232 
233  if(expr.id()==ID_constant)
234  {
235  std::unique_ptr<languaget> lang;
236  if(mode==ID_unknown)
237  lang=std::unique_ptr<languaget>(get_default_language());
238  else
239  {
240  lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
241  if(!lang)
242  lang=std::unique_ptr<languaget>(get_default_language());
243  }
244 
245  const typet &underlying_type=
246  type.id()==ID_c_bit_field?type.subtype():
247  type;
248 
249  std::string type_string;
250  bool error=lang->from_type(underlying_type, type_string, ns);
251  CHECK_RETURN(!error);
252 
253  std::string value_string;
254  lang->from_expr(expr, value_string, ns);
255 
256  const constant_exprt &constant_expr=to_constant_expr(expr);
257  if(type.id()==ID_unsignedbv ||
258  type.id()==ID_signedbv ||
259  type.id()==ID_c_bit_field)
260  {
261  std::size_t width=to_bitvector_type(type).get_width();
262 
263  result["name"]=json_stringt("integer");
264  result["binary"] = json_stringt(constant_expr.get_value());
265  result["width"]=json_numbert(std::to_string(width));
266  result["type"]=json_stringt(type_string);
267  result["data"]=json_stringt(value_string);
268  }
269  else if(type.id()==ID_c_enum)
270  {
271  result["name"]=json_stringt("integer");
272  result["binary"] = json_stringt(constant_expr.get_value());
273  result["width"]=json_numbert(type.subtype().get_string(ID_width));
274  result["type"]=json_stringt("enum");
275  result["data"]=json_stringt(value_string);
276  }
277  else if(type.id()==ID_c_enum_tag)
278  {
279  constant_exprt tmp;
280  tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
281  tmp.set_value(to_constant_expr(expr).get_value());
282  return json(tmp, ns, mode);
283  }
284  else if(type.id()==ID_bv)
285  {
286  result["name"]=json_stringt("bitvector");
287  result["binary"] = json_stringt(constant_expr.get_value());
288  }
289  else if(type.id()==ID_fixedbv)
290  {
291  result["name"]=json_stringt("fixed");
292  result["width"]=json_numbert(type.get_string(ID_width));
293  result["binary"] = json_stringt(constant_expr.get_value());
294  result["data"]=
295  json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
296  }
297  else if(type.id()==ID_floatbv)
298  {
299  result["name"]=json_stringt("float");
300  result["width"]=json_numbert(type.get_string(ID_width));
301  result["binary"] = json_stringt(constant_expr.get_value());
302  result["data"]=
303  json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
304  }
305  else if(type.id()==ID_pointer)
306  {
307  result["name"]=json_stringt("pointer");
308  result["type"]=json_stringt(type_string);
309  exprt simpl_expr=simplify_json_expr(expr, ns);
310  if(simpl_expr.get(ID_value)==ID_NULL ||
311  // remove typecast on NULL
312  (simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer &&
313  simpl_expr.op0().get(ID_value)==ID_NULL))
314  result["data"]=json_stringt(value_string);
315  else if(simpl_expr.id()==ID_symbol)
316  {
317  const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();
318  identifiert identifier(id2string(ptr_id));
320  !identifier.components.empty(),
321  "pointer identifier should have non-empty components");
322  result["data"]=json_stringt(identifier.components.back());
323  }
324  }
325  else if(type.id()==ID_bool)
326  {
327  result["name"]=json_stringt("boolean");
328  result["binary"]=json_stringt(expr.is_true()?"1":"0");
329  result["data"]=jsont::json_boolean(expr.is_true());
330  }
331  else if(type.id()==ID_c_bool)
332  {
333  result["name"]=json_stringt("integer");
334  result["width"]=json_numbert(type.get_string(ID_width));
335  result["type"]=json_stringt(type_string);
336  result["binary"]=json_stringt(expr.get_string(ID_value));
337  result["data"]=json_stringt(value_string);
338  }
339  else if(type.id()==ID_string)
340  {
341  result["name"]=json_stringt("string");
342  result["data"] = json_stringt(constant_expr.get_value());
343  }
344  else
345  {
346  result["name"]=json_stringt("unknown");
347  }
348  }
349  else if(expr.id()==ID_array)
350  {
351  result["name"]=json_stringt("array");
352  json_arrayt &elements=result["elements"].make_array();
353 
354  std::size_t index=0;
355 
356  forall_operands(it, expr)
357  {
358  json_objectt &e=elements.push_back().make_object();
359  e["index"]=json_numbert(std::to_string(index));
360  e["value"]=json(*it, ns, mode);
361  index++;
362  }
363  }
364  else if(expr.id()==ID_struct)
365  {
366  result["name"]=json_stringt("struct");
367 
368  // these are expected to have a struct type
369  if(type.id()==ID_struct)
370  {
371  const struct_typet &struct_type=to_struct_type(type);
372  const struct_typet::componentst &components=struct_type.components();
374  components.size()==expr.operands().size(),
375  "number of struct components should match with its type");
376 
377  json_arrayt &members=result["members"].make_array();
378  for(std::size_t m=0; m<expr.operands().size(); m++)
379  {
380  json_objectt &e=members.push_back().make_object();
381  e["value"]=json(expr.operands()[m], ns, mode);
382  e["name"] = json_stringt(components[m].get_name());
383  }
384  }
385  }
386  else if(expr.id()==ID_union)
387  {
388  result["name"]=json_stringt("union");
389 
390  const union_exprt &union_expr=to_union_expr(expr);
391  json_objectt &e=result["member"].make_object();
392  e["value"]=json(union_expr.op(), ns, mode);
393  e["name"] = json_stringt(union_expr.get_component_name());
394  }
395  else
396  result["name"]=json_stringt("unknown");
397 
398  return result;
399 }
The type of an expression.
Definition: type.h:22
const irep_idt & get_working_directory() const
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1296
exprt & op0()
Definition: expr.h:72
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
const exprt & op() const
Definition: std_expr.h:340
std::unique_ptr< languaget > get_default_language()
Returns the default language.
Definition: mode.cpp:138
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:50
const irep_idt & get_function() const
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::vector< componentt > componentst
Definition: std_types.h:243
const irep_idt & get_value() const
Definition: std_expr.h:4439
const componentst & components() const
Definition: std_types.h:245
static jsont json_boolean(bool value)
Definition: json.h:85
bool NULL_is_zero
Definition: config.h:87
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4422
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
Structure type.
Definition: std_types.h:297
configt config
Definition: config.cpp:23
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
json_arrayt & make_array()
Definition: json.h:284
const irep_idt & get_column() const
jsont & push_back(const jsont &json)
Definition: json.h:163
const irep_idt & id() const
Definition: irep.h:259
void set_value(const irep_idt &value)
Definition: std_expr.h:4444
const irep_idt & get_line() const
union constructor from single element
Definition: std_expr.h:1730
API to expression classes.
Expressions in JSON.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Abstract interface to support a programming language.
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1669
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
size_t size() const
Definition: dstring.h:89
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1212
std::size_t get_width() const
Definition: std_types.h:1138
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:747
static exprt simplify_json_expr(const exprt &src, const namespacet &ns)
Definition: json_expr.cpp:30
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1254
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
const irep_idt & get_file() const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1382
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
Base class for all expressions.
Definition: expr.h:42
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1782
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
irep_idt get_component_name() const
Definition: std_expr.h:1751
const irep_idt & get_java_bytecode_index() const
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a generic typet to a c_bit_field_typet.
Definition: std_types.h:1411
json_objectt & make_object()
Definition: json.h:290
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
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
operandst & operands()
Definition: expr.h:66
componentst components
Definition: identifier.h:30
bool empty() const
Definition: dstring.h:73
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83