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 
24 {
25  json_objectt result;
26 
27  if(!location.get_file().empty())
28  result["file"]=json_stringt(id2string(location.get_file()));
29 
30  if(!location.get_line().empty())
31  result["line"]=json_stringt(id2string(location.get_line()));
32 
33  if(!location.get_column().empty())
34  result["column"]=json_stringt(id2string(location.get_column()));
35 
36  if(!location.get_function().empty())
37  result["function"]=json_stringt(id2string(location.get_function()));
38 
39  if(!location.get_java_bytecode_index().empty())
40  result["bytecode_index"]=
42 
43  return result;
44 }
45 
47  const typet &type,
48  const namespacet &ns)
49 {
50  if(type.id()==ID_symbol)
51  return json(ns.follow(type), ns);
52 
53  json_objectt result;
54 
55  if(type.id()==ID_unsignedbv)
56  {
57  result["name"]=json_stringt("integer");
58  result["width"]=
59  json_numbert(std::to_string(to_unsignedbv_type(type).get_width()));
60  }
61  else if(type.id()==ID_signedbv)
62  {
63  result["name"]=json_stringt("integer");
64  result["width"]=
65  json_numbert(std::to_string(to_signedbv_type(type).get_width()));
66  }
67  else if(type.id()==ID_floatbv)
68  {
69  result["name"]=json_stringt("float");
70  result["width"]=
71  json_numbert(std::to_string(to_floatbv_type(type).get_width()));
72  }
73  else if(type.id()==ID_bv)
74  {
75  result["name"]=json_stringt("integer");
76  result["width"]=json_numbert(std::to_string(to_bv_type(type).get_width()));
77  }
78  else if(type.id()==ID_c_bit_field)
79  {
80  result["name"]=json_stringt("integer");
81  result["width"]=
82  json_numbert(std::to_string(to_c_bit_field_type(type).get_width()));
83  }
84  else if(type.id()==ID_c_enum_tag)
85  {
86  // we return the base type
87  return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
88  }
89  else if(type.id()==ID_fixedbv)
90  {
91  result["name"]=json_stringt("fixed");
92  result["width"]=
93  json_numbert(std::to_string(to_fixedbv_type(type).get_width()));
94  }
95  else if(type.id()==ID_pointer)
96  {
97  result["name"]=json_stringt("pointer");
98  result["subtype"]=json(type.subtype(), ns);
99  }
100  else if(type.id()==ID_bool)
101  {
102  result["name"]=json_stringt("boolean");
103  }
104  else if(type.id()==ID_array)
105  {
106  result["name"]=json_stringt("array");
107  result["subtype"]=json(type.subtype(), ns);
108  }
109  else if(type.id()==ID_vector)
110  {
111  result["name"]=json_stringt("vector");
112  result["subtype"]=json(type.subtype(), ns);
113  result["size"]=json(to_vector_type(type).size(), ns);
114  }
115  else if(type.id()==ID_struct)
116  {
117  result["name"]=json_stringt("struct");
118  json_arrayt &members=result["members"].make_array();
119  const struct_typet::componentst &components=
120  to_struct_type(type).components();
121  for(const auto &component : components)
122  {
123  json_objectt &e=members.push_back().make_object();
124  e["name"]=json_stringt(id2string(component.get_name()));
125  e["type"]=json(component.type(), ns);
126  }
127  }
128  else if(type.id()==ID_union)
129  {
130  result["name"]=json_stringt("union");
131  json_arrayt &members=result["members"].make_array();
132  const union_typet::componentst &components=
133  to_union_type(type).components();
134  for(const auto &component : components)
135  {
136  json_objectt &e=members.push_back().make_object();
137  e["name"]=json_stringt(id2string(component.get_name()));
138  e["type"]=json(component.type(), ns);
139  }
140  }
141  else
142  result["name"]=json_stringt("unknown");
143 
144  return result;
145 }
146 
148  const exprt &expr,
149  const namespacet &ns)
150 {
151  json_objectt result;
152 
153  const typet &type=ns.follow(expr.type());
154 
155  if(expr.id()==ID_constant)
156  {
157  if(type.id()==ID_unsignedbv ||
158  type.id()==ID_signedbv ||
159  type.id()==ID_c_bit_field)
160  {
161  std::size_t width=to_bitvector_type(type).get_width();
162 
163  result["name"]=json_stringt("integer");
164  result["binary"]=json_stringt(expr.get_string(ID_value));
165  result["width"]=json_numbert(std::to_string(width));
166 
167  const typet &underlying_type=
168  type.id()==ID_c_bit_field?type.subtype():
169  type;
170 
171  bool is_signed=underlying_type.id()==ID_signedbv;
172 
173  std::string sig=is_signed?"":"unsigned ";
174 
175  if(width==config.ansi_c.char_width)
176  result["c_type"]=json_stringt(sig+"char");
177  else if(width==config.ansi_c.int_width)
178  result["c_type"]=json_stringt(sig+"int");
179  else if(width==config.ansi_c.short_int_width)
180  result["c_type"]=json_stringt(sig+"short int");
181  else if(width==config.ansi_c.long_int_width)
182  result["c_type"]=json_stringt(sig+"long int");
183  else if(width==config.ansi_c.long_long_int_width)
184  result["c_type"]=json_stringt(sig+"long long int");
185 
186  mp_integer i;
187  if(!to_integer(expr, i))
188  result["data"]=json_stringt(integer2string(i));
189  }
190  else if(type.id()==ID_c_enum)
191  {
192  result["name"]=json_stringt("integer");
193  result["binary"]=json_stringt(expr.get_string(ID_value));
194  result["width"]=json_numbert(type.subtype().get_string(ID_width));
195  result["c_type"]=json_stringt("enum");
196 
197  mp_integer i;
198  if(!to_integer(expr, i))
199  result["data"]=json_stringt(integer2string(i));
200  }
201  else if(type.id()==ID_c_enum_tag)
202  {
203  constant_exprt tmp;
204  tmp.type()=ns.follow_tag(to_c_enum_tag_type(type));
205  tmp.set_value(to_constant_expr(expr).get_value());
206  return json(tmp, ns);
207  }
208  else if(type.id()==ID_bv)
209  {
210  result["name"]=json_stringt("bitvector");
211  result["binary"]=json_stringt(expr.get_string(ID_value));
212  }
213  else if(type.id()==ID_fixedbv)
214  {
215  result["name"]=json_stringt("fixed");
216  result["width"]=json_numbert(type.get_string(ID_width));
217  result["binary"]=json_stringt(expr.get_string(ID_value));
218  result["data"]=
219  json_stringt(fixedbvt(to_constant_expr(expr)).to_ansi_c_string());
220  }
221  else if(type.id()==ID_floatbv)
222  {
223  result["name"]=json_stringt("float");
224  result["width"]=json_numbert(type.get_string(ID_width));
225  result["binary"]=json_stringt(expr.get_string(ID_value));
226  result["data"]=
227  json_stringt(ieee_floatt(to_constant_expr(expr)).to_ansi_c_string());
228  }
229  else if(type.id()==ID_pointer)
230  {
231  result["name"]=json_stringt("pointer");
232  result["binary"]=json_stringt(expr.get_string(ID_value));
233  if(expr.get(ID_value)==ID_NULL)
234  result["data"]=json_stringt("NULL");
235  }
236  else if(type.id()==ID_bool)
237  {
238  result["name"]=json_stringt("boolean");
239  result["binary"]=json_stringt(expr.is_true()?"1":"0");
240  result["data"]=jsont::json_boolean(expr.is_true());
241  }
242  else if(type.id()==ID_c_bool)
243  {
244  result["name"]=json_stringt("integer");
245  result["c_type"]=json_stringt("_Bool");
246  result["binary"]=json_stringt(expr.get_string(ID_value));
247  mp_integer b;
248  to_integer(to_constant_expr(expr), b);
249  result["data"]=json_stringt(integer2string(b));
250  }
251  else
252  {
253  result["name"]=json_stringt("unknown");
254  }
255  }
256  else if(expr.id()==ID_array)
257  {
258  result["name"]=json_stringt("array");
259  json_arrayt &elements=result["elements"].make_array();
260 
261  unsigned index=0;
262 
263  forall_operands(it, expr)
264  {
265  json_objectt &e=elements.push_back().make_object();
266  e["index"]=json_numbert(std::to_string(index));
267  e["value"]=json(*it, ns);
268  index++;
269  }
270  }
271  else if(expr.id()==ID_struct)
272  {
273  result["name"]=json_stringt("struct");
274 
275  // these are expected to have a struct type
276  if(type.id()==ID_struct)
277  {
278  const struct_typet &struct_type=to_struct_type(type);
279  const struct_typet::componentst &components=struct_type.components();
280  assert(components.size()==expr.operands().size());
281 
282  json_arrayt &members=result["members"].make_array();
283  for(unsigned m=0; m<expr.operands().size(); m++)
284  {
285  json_objectt &e=members.push_back().make_object();
286  e["value"]=json(expr.operands()[m], ns);
287  e["name"]=json_stringt(id2string(components[m].get_name()));
288  }
289  }
290  }
291  else if(expr.id()==ID_union)
292  {
293  result["name"]=json_stringt("union");
294 
295  assert(expr.operands().size()==1);
296 
297  json_objectt &e=result["member"].make_object();
298  e["value"]=json(expr.op0(), ns);
299  e["name"]=json_stringt(id2string(to_union_expr(expr).get_component_name()));
300  }
301  else
302  result["name"]=json_stringt("unknown");
303 
304  return result;
305 }
The type of an expression.
Definition: type.h:20
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
unsigned int_width
Definition: config.h:30
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
exprt & op0()
Definition: expr.h:84
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
const irep_idt & get_function() const
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
static jsont json_boolean(bool value)
Definition: json.h:83
unsigned short_int_width
Definition: config.h:34
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
unsigned char_width
Definition: config.h:33
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
json_arrayt & make_array()
Definition: json.h:228
const irep_idt & get_column() const
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
jsont & push_back(const jsont &json)
Definition: json.h:157
const irep_idt & id() const
Definition: irep.h:189
void set_value(const irep_idt &value)
Definition: std_expr.h:3707
const irep_idt & get_line() const
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:717
unsigned long_long_int_width
Definition: config.h:35
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:62
#define forall_operands(it, expr)
Definition: expr.h:17
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
Definition: std_expr.h:1441
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:1319
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
std::size_t get_width() const
Definition: std_types.h:1030
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const bv_typet & to_bv_type(const typet &type)
Cast a generic typet to a bv_typet.
Definition: std_types.h:1108
const irep_idt & get_file() const
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1247
Base class for all expressions.
Definition: expr.h:46
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const irep_idt & get_java_bytecode_index() const
json_objectt & make_object()
Definition: json.h:234
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
unsigned long_int_width
Definition: config.h:31
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
const vector_typet & to_vector_type(const typet &type)
Cast a generic typet to a vector_typet.
Definition: std_types.h:1589
bool empty() const
Definition: dstring.h:61
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1051