cprover
json.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_JSON_H
11 #define CPROVER_UTIL_JSON_H
12 
13 #include <vector>
14 #include <map>
15 #include <iosfwd>
16 #include <string>
17 
18 #include "irep.h"
19 #include "range.h"
20 
21 class json_objectt;
22 class json_arrayt;
23 
24 class jsont
25 {
26 protected:
27  typedef std::vector<jsont> arrayt;
28  typedef std::map<std::string, jsont> objectt;
29 
30 public:
31  enum class kindt
32  {
33  J_STRING,
34  J_NUMBER,
35  J_OBJECT,
36  J_ARRAY,
37  J_TRUE,
38  J_FALSE,
39  J_NULL
40  };
41 
43 
44  bool is_string() const
45  {
46  return kind==kindt::J_STRING;
47  }
48 
49  bool is_number() const
50  {
51  return kind==kindt::J_NUMBER;
52  }
53 
54  bool is_object() const
55  {
56  return kind==kindt::J_OBJECT;
57  }
58 
59  bool is_array() const
60  {
61  return kind==kindt::J_ARRAY;
62  }
63 
64  bool is_boolean() const
65  {
66  return kind == kindt::J_TRUE || kind == kindt::J_FALSE;
67  }
68 
69  bool is_true() const
70  {
71  return kind==kindt::J_TRUE;
72  }
73 
74  bool is_false() const
75  {
76  return kind==kindt::J_FALSE;
77  }
78 
79  bool is_null() const
80  {
81  return kind==kindt::J_NULL;
82  }
83 
84  jsont():kind(kindt::J_NULL)
85  {
86  }
87 
88  void output(std::ostream &out) const
89  {
90  output_rec(out, 0);
91  }
92 
93  void swap(jsont &other);
94 
95  static jsont json_boolean(bool value)
96  {
98  }
99 
100  void clear()
101  {
102  value.clear();
104  object.clear();
105  array.clear();
106  }
107 
110 
111  // this presumes that this is an object
112  const jsont &operator[](const std::string &key) const
113  {
114  objectt::const_iterator it=object.find(key);
115  if(it==object.end())
116  return null_json_object;
117  else
118  return it->second;
119  }
120 
121  void output_rec(std::ostream &, unsigned indent) const;
122 
123  static const jsont null_json_object;
124 
125  static void output_key(std::ostream &out, const std::string &key);
126 
127  static void
128  output_object(std::ostream &out, const objectt &object, unsigned indent);
129 
130  std::string value;
131 
132 protected:
135 
136  static void escape_string(const std::string &, std::ostream &);
137 
138  explicit jsont(kindt _kind):kind(_kind)
139  {
140  }
141 
142  jsont(kindt _kind, std::string _value) : kind(_kind), value(std::move(_value))
143  {
144  }
145 
146  jsont(kindt _kind, arrayt &&entries) : kind(_kind), array(std::move(entries))
147  {
148  }
149 
150  jsont(kindt _kind, objectt &&objects)
151  : kind(_kind), object(std::move(objects))
152  {
153  }
154 };
155 
156 inline std::ostream &operator<<(std::ostream &out, const jsont &src)
157 {
158  src.output(out);
159  return out;
160 }
161 
162 class json_arrayt:public jsont
163 {
164 public:
165  json_arrayt():jsont(kindt::J_ARRAY)
166  {
167  }
168 
169  explicit json_arrayt(std::initializer_list<jsont> &&initializer_list)
170  : jsont(kindt::J_ARRAY, arrayt{initializer_list})
171  {
172  }
173 
174  template <typename begin_iteratort, typename end_iteratort>
175  json_arrayt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
176  : jsont(
177  kindt::J_ARRAY,
178  arrayt(
179  std::forward<begin_iteratort>(begin_iterator),
180  std::forward<end_iteratort>(end_iterator)))
181  {
182  static_assert(
183  std::is_same<
184  typename std::decay<begin_iteratort>::type,
185  typename std::decay<end_iteratort>::type>::value,
186  "The iterators must be of the same type.");
187  }
188 
189  template <typename iteratort>
190  explicit json_arrayt(ranget<iteratort> &&range)
191  : jsont(kindt::J_ARRAY, arrayt{range.begin(), range.end()})
192  {
193  }
194 
195  void resize(std::size_t size)
196  {
197  array.resize(size);
198  }
199 
200  std::size_t size() const
201  {
202  return array.size();
203  }
204 
205  bool empty() const
206  {
207  return array.empty();
208  }
209 
211  {
212  array.push_back(json);
213  return array.back();
214  }
215 
217  {
218  array.push_back(std::move(json));
219  return array.back();
220  }
221 
223  {
224  array.push_back(jsont());
225  return array.back();
226  }
227 
228  template <typename... argumentst>
229  void emplace_back(argumentst &&... arguments)
230  {
231  array.emplace_back(std::forward<argumentst>(arguments)...);
232  }
233 
234  arrayt::iterator begin()
235  {
236  return array.begin();
237  }
238 
239  arrayt::const_iterator begin() const
240  {
241  return array.begin();
242  }
243 
244  arrayt::const_iterator cbegin() const
245  {
246  return array.cbegin();
247  }
248 
249  arrayt::iterator end()
250  {
251  return array.end();
252  }
253 
254  arrayt::const_iterator end() const
255  {
256  return array.end();
257  }
258 
259  arrayt::const_iterator cend() const
260  {
261  return array.cend();
262  }
263 
264  typedef jsont value_type; // NOLINT(readability/identifiers)
265 };
266 
267 class json_stringt:public jsont
268 {
269 public:
270  explicit json_stringt(std::string _value)
271  : jsont(kindt::J_STRING, std::move(_value))
272  {
273  }
274 
275 #ifndef USE_STD_STRING
276  explicit json_stringt(const irep_idt &_value)
277  : jsont(kindt::J_STRING, id2string(_value))
278  {
279  }
280 #endif
281 
283  explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value)
284  {
285  }
286 };
287 
288 class json_numbert:public jsont
289 {
290 public:
291  explicit json_numbert(const std::string &_value):
292  jsont(kindt::J_NUMBER, _value)
293  {
294  }
295 };
296 
297 class json_objectt:public jsont
298 {
299 public:
300  using value_type = objectt::value_type;
301  using iterator = objectt::iterator;
302  using const_iterator = objectt::const_iterator;
303 
304  json_objectt():jsont(kindt::J_OBJECT)
305  {
306  }
307 
308  explicit json_objectt(
309  std::initializer_list<typename objectt::value_type> &&initializer_list)
310  : jsont(kindt::J_OBJECT, objectt{initializer_list})
311  {
312  }
313 
314  template <typename begin_iteratort, typename end_iteratort>
315  json_objectt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
316  : jsont(
317  kindt::J_OBJECT,
318  objectt(
319  std::forward<begin_iteratort>(begin_iterator),
320  std::forward<end_iteratort>(end_iterator)))
321  {
322  static_assert(
323  std::is_same<
324  typename std::decay<begin_iteratort>::type,
325  typename std::decay<end_iteratort>::type>::value,
326  "The iterators must be of the same type.");
327  }
328 
329  template <typename iteratort>
330  explicit json_objectt(ranget<iteratort> &&range)
331  : jsont(kindt::J_OBJECT, objectt{range.begin(), range.end()})
332  {
333  }
334 
335  jsont &operator[](const std::string &key)
336  {
337  return object[key];
338  }
339 
340  const jsont &operator[](const std::string &key) const
341  {
342  const_iterator it = object.find(key);
343  if(it==object.end())
344  return null_json_object;
345  else
346  return it->second;
347  }
348 
350  {
351  return object.insert(it, std::move(value));
352  }
353 
354  iterator find(const std::string &key)
355  {
356  return object.find(key);
357  }
358 
359  const_iterator find(const std::string &key) const
360  {
361  return object.find(key);
362  }
363 
364  std::size_t size() const
365  {
366  return object.size();
367  }
368 
370  {
371  return object.begin();
372  }
373 
375  {
376  return object.begin();
377  }
378 
380  {
381  return object.cbegin();
382  }
383 
385  {
386  return object.end();
387  }
388 
390  {
391  return object.end();
392  }
393 
395  {
396  return object.cend();
397  }
398 };
399 
400 class json_truet:public jsont
401 {
402 public:
403  json_truet():jsont(kindt::J_TRUE) { }
404 };
405 
406 class json_falset:public jsont
407 {
408 public:
409  json_falset():jsont(kindt::J_FALSE) { }
410 };
411 
412 class json_nullt:public jsont
413 {
414 public:
415  json_nullt():jsont(kindt::J_NULL) { }
416 };
417 
419 {
421  return static_cast<json_arrayt &>(*this);
422 }
423 
425 {
427  return static_cast<json_arrayt &>(json);
428 }
429 
430 inline const json_arrayt &to_json_array(const jsont &json)
431 {
433  return static_cast<const json_arrayt &>(json);
434 }
435 
437 {
439  return static_cast<json_objectt &>(*this);
440 }
441 
443 {
445  return static_cast<json_objectt &>(json);
446 }
447 
448 inline const json_objectt &to_json_object(const jsont &json)
449 {
451  return static_cast<const json_objectt &>(json);
452 }
453 
455 {
457  return static_cast<json_stringt &>(json);
458 }
459 
460 inline const json_stringt &to_json_string(const jsont &json)
461 {
463  return static_cast<const json_stringt &>(json);
464 }
465 
466 bool operator==(const jsont &left, const jsont &right);
467 
468 #endif // CPROVER_UTIL_JSON_H
json_arrayt::json_arrayt
json_arrayt()
Definition: json.h:165
json_falset::json_falset
json_falset()
Definition: json.h:409
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:289
json_objectt::insert
iterator insert(const_iterator it, value_type value)
Definition: json.h:349
json_arrayt::empty
bool empty() const
Definition: json.h:205
json_truet
Definition: json.h:401
jsont::operator[]
const jsont & operator[](const std::string &key) const
Definition: json.h:112
json_stringt::json_stringt
json_stringt(const irep_idt &_value)
Definition: json.h:276
json_arrayt::push_back
jsont & push_back(jsont &&json)
Definition: json.h:216
json_arrayt::resize
void resize(std::size_t size)
Definition: json.h:195
json_objectt::operator[]
jsont & operator[](const std::string &key)
Definition: json.h:335
json_objectt::iterator
objectt::iterator iterator
Definition: json.h:301
jsont::output
void output(std::ostream &out) const
Definition: json.h:88
json_arrayt::emplace_back
void emplace_back(argumentst &&... arguments)
Definition: json.h:229
jsont::object
objectt object
Definition: json.h:134
jsont::jsont
jsont()
Definition: json.h:84
jsont::is_true
bool is_true() const
Definition: json.h:69
json_objectt::find
iterator find(const std::string &key)
Definition: json.h:354
jsont::kindt::J_FALSE
@ J_FALSE
json_arrayt::value_type
jsont value_type
Definition: json.h:264
json_objectt::operator[]
const jsont & operator[](const std::string &key) const
Definition: json.h:340
jsont::null_json_object
static const jsont null_json_object
Definition: json.h:123
json_objectt::value_type
objectt::value_type value_type
Definition: json.h:300
json_objectt::json_objectt
json_objectt(std::initializer_list< typename objectt::value_type > &&initializer_list)
Definition: json.h:308
json_arrayt::json_arrayt
json_arrayt(ranget< iteratort > &&range)
Definition: json.h:190
jsont::arrayt
std::vector< jsont > arrayt
Definition: json.h:27
json_objectt::const_iterator
objectt::const_iterator const_iterator
Definition: json.h:302
jsont::escape_string
static void escape_string(const std::string &, std::ostream &)
Definition: json.cpp:16
to_json_array
json_arrayt & to_json_array(jsont &json)
Definition: json.h:424
jsont::make_object
json_objectt & make_object()
Definition: json.h:436
jsont
Definition: json.h:25
jsont::kindt::J_ARRAY
@ J_ARRAY
json_arrayt::end
arrayt::iterator end()
Definition: json.h:249
jsont::kindt::J_NUMBER
@ J_NUMBER
json_arrayt::push_back
jsont & push_back()
Definition: json.h:222
json_arrayt
Definition: json.h:163
json_objectt::end
const_iterator end() const
Definition: json.h:389
jsont::is_number
bool is_number() const
Definition: json.h:49
jsont::kindt::J_OBJECT
@ J_OBJECT
json_objectt
Definition: json.h:298
json_numbert::json_numbert
json_numbert(const std::string &_value)
Definition: json.h:291
jsont::output_rec
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition: json.cpp:57
json_arrayt::begin
arrayt::iterator begin()
Definition: json.h:234
operator==
bool operator==(const jsont &left, const jsont &right)
Definition: json.cpp:167
jsont::kindt::J_STRING
@ J_STRING
jsont::is_null
bool is_null() const
Definition: json.h:79
json_objectt::size
std::size_t size() const
Definition: json.h:364
jsont::kindt::J_TRUE
@ J_TRUE
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
jsont::swap
void swap(jsont &other)
Definition: json.cpp:159
json_objectt::json_objectt
json_objectt()
Definition: json.h:304
json_objectt::json_objectt
json_objectt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
Definition: json.h:315
jsont::objectt
std::map< std::string, jsont > objectt
Definition: json.h:28
json_objectt::begin
iterator begin()
Definition: json.h:369
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
jsont::output_object
static void output_object(std::ostream &out, const objectt &object, unsigned indent)
Basic handling of the printing of a JSON object.
Definition: json.cpp:130
jsont::is_string
bool is_string() const
Definition: json.h:44
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
ranget
A range is a pair of a begin and an end iterators.
Definition: range.h:396
jsont::kindt::J_NULL
@ J_NULL
json_objectt::cbegin
const_iterator cbegin() const
Definition: json.h:379
json_falset
Definition: json.h:407
range.h
jsont::make_array
json_arrayt & make_array()
Definition: json.h:418
jsont::is_boolean
bool is_boolean() const
Definition: json.h:64
json_arrayt::end
arrayt::const_iterator end() const
Definition: json.h:254
json_arrayt::begin
arrayt::const_iterator begin() const
Definition: json.h:239
json_objectt::find
const_iterator find(const std::string &key) const
Definition: json.h:359
jsont::kindt
kindt
Definition: json.h:32
jsont::clear
void clear()
Definition: json.h:100
jsont::jsont
jsont(kindt _kind, objectt &&objects)
Definition: json.h:150
json_arrayt::cend
arrayt::const_iterator cend() const
Definition: json.h:259
jsont::jsont
jsont(kindt _kind, arrayt &&entries)
Definition: json.h:146
json_arrayt::json_arrayt
json_arrayt(std::initializer_list< jsont > &&initializer_list)
Definition: json.h:169
json_objectt::begin
const_iterator begin() const
Definition: json.h:374
json_stringt::json_stringt
json_stringt(const char *_value)
Constructon from string literal.
Definition: json.h:283
json_objectt::end
iterator end()
Definition: json.h:384
operator<<
std::ostream & operator<<(std::ostream &out, const jsont &src)
Definition: json.h:156
json_arrayt::size
std::size_t size() const
Definition: json.h:200
jsont::is_false
bool is_false() const
Definition: json.h:74
to_json_string
json_stringt & to_json_string(jsont &json)
Definition: json.h:454
json_objectt::cend
const_iterator cend() const
Definition: json.h:394
to_json_object
json_objectt & to_json_object(jsont &json)
Definition: json.h:442
jsont::array
arrayt array
Definition: json.h:133
json_arrayt::cbegin
arrayt::const_iterator cbegin() const
Definition: json.h:244
jsont::jsont
jsont(kindt _kind, std::string _value)
Definition: json.h:142
jsont::is_array
bool is_array() const
Definition: json.h:59
json_arrayt::json_arrayt
json_arrayt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
Definition: json.h:175
json_truet::json_truet
json_truet()
Definition: json.h:403
jsont::is_object
bool is_object() const
Definition: json.h:54
jsont::jsont
jsont(kindt _kind)
Definition: json.h:138
json_objectt::json_objectt
json_objectt(ranget< iteratort > &&range)
Definition: json.h:330
jsont::kind
kindt kind
Definition: json.h:42
json_nullt::json_nullt
json_nullt()
Definition: json.h:415
jsont::json_boolean
static jsont json_boolean(bool value)
Definition: json.h:95
jsont::output_key
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:152
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:210
json_stringt::json_stringt
json_stringt(std::string _value)
Definition: json.h:270
json_nullt
Definition: json.h:413
irep.h
json_stringt
Definition: json.h:268
jsont::value
std::string value
Definition: json.h:130