CBMC
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 structured_datat;
22 
23 class json_objectt;
24 class json_arrayt;
25 
26 class jsont
27 {
28 protected:
29  typedef std::vector<jsont> arrayt;
30  typedef std::map<std::string, jsont> objectt;
31 
32 public:
33  enum class kindt
34  {
35  J_STRING,
36  J_NUMBER,
37  J_OBJECT,
38  J_ARRAY,
39  J_TRUE,
40  J_FALSE,
41  J_NULL
42  };
43 
45 
46  bool is_string() const
47  {
48  return kind==kindt::J_STRING;
49  }
50 
51  bool is_number() const
52  {
53  return kind==kindt::J_NUMBER;
54  }
55 
56  bool is_object() const
57  {
58  return kind==kindt::J_OBJECT;
59  }
60 
61  bool is_array() const
62  {
63  return kind==kindt::J_ARRAY;
64  }
65 
66  bool is_boolean() const
67  {
68  return kind == kindt::J_TRUE || kind == kindt::J_FALSE;
69  }
70 
71  bool is_true() const
72  {
73  return kind==kindt::J_TRUE;
74  }
75 
76  bool is_false() const
77  {
78  return kind==kindt::J_FALSE;
79  }
80 
81  bool is_null() const
82  {
83  return kind==kindt::J_NULL;
84  }
85 
86  jsont():kind(kindt::J_NULL)
87  {
88  }
89 
90  void output(std::ostream &out) const
91  {
92  output_rec(out, 0);
93  }
94 
95  void swap(jsont &other);
96 
97  static jsont json_boolean(bool value)
98  {
100  }
101 
102  void clear()
103  {
104  value.clear();
106  object.clear();
107  array.clear();
108  }
109 
112 
113  // this presumes that this is an object
114  const jsont &operator[](const std::string &key) const
115  {
116  objectt::const_iterator it=object.find(key);
117  if(it==object.end())
118  return null_json_object;
119  else
120  return it->second;
121  }
122 
123  void output_rec(std::ostream &, unsigned indent) const;
124 
125  static const jsont null_json_object;
126 
127  static void output_key(std::ostream &out, const std::string &key);
128 
129  static void
130  output_object(std::ostream &out, const objectt &object, unsigned indent);
131 
132  std::string value;
133 
134 protected:
137 
138  static void escape_string(const std::string &, std::ostream &);
139 
140  explicit jsont(kindt _kind):kind(_kind)
141  {
142  }
143 
144  jsont(kindt _kind, std::string _value) : kind(_kind), value(std::move(_value))
145  {
146  }
147 
148  jsont(kindt _kind, arrayt &&entries) : kind(_kind), array(std::move(entries))
149  {
150  }
151 
152  jsont(kindt _kind, objectt &&objects)
153  : kind(_kind), object(std::move(objects))
154  {
155  }
156 };
157 
158 inline std::ostream &operator<<(std::ostream &out, const jsont &src)
159 {
160  src.output(out);
161  return out;
162 }
163 
164 class json_arrayt:public jsont
165 {
166 public:
167  json_arrayt():jsont(kindt::J_ARRAY)
168  {
169  }
170 
171  explicit json_arrayt(std::initializer_list<jsont> &&initializer_list)
172  : jsont(kindt::J_ARRAY, arrayt{initializer_list})
173  {
174  }
175 
176  template <typename begin_iteratort, typename end_iteratort>
177  json_arrayt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
178  : jsont(
179  kindt::J_ARRAY,
180  arrayt(
181  std::forward<begin_iteratort>(begin_iterator),
182  std::forward<end_iteratort>(end_iterator)))
183  {
184  static_assert(
185  std::is_same<
186  typename std::decay<begin_iteratort>::type,
187  typename std::decay<end_iteratort>::type>::value,
188  "The iterators must be of the same type.");
189  }
190 
191  template <typename iteratort>
192  explicit json_arrayt(ranget<iteratort> &&range)
193  : jsont(kindt::J_ARRAY, arrayt{range.begin(), range.end()})
194  {
195  }
196 
197  void resize(std::size_t size)
198  {
199  array.resize(size);
200  }
201 
202  std::size_t size() const
203  {
204  return array.size();
205  }
206 
207  bool empty() const
208  {
209  return array.empty();
210  }
211 
213  {
214  array.push_back(json);
215  return array.back();
216  }
217 
219  {
220  array.push_back(std::move(json));
221  return array.back();
222  }
223 
225  {
226  array.push_back(jsont());
227  return array.back();
228  }
229 
230  template <typename... argumentst>
231  void emplace_back(argumentst &&... arguments)
232  {
233  array.emplace_back(std::forward<argumentst>(arguments)...);
234  }
235 
236  arrayt::iterator begin()
237  {
238  return array.begin();
239  }
240 
241  arrayt::const_iterator begin() const
242  {
243  return array.begin();
244  }
245 
246  arrayt::const_iterator cbegin() const
247  {
248  return array.cbegin();
249  }
250 
251  arrayt::iterator end()
252  {
253  return array.end();
254  }
255 
256  arrayt::const_iterator end() const
257  {
258  return array.end();
259  }
260 
261  arrayt::const_iterator cend() const
262  {
263  return array.cend();
264  }
265 
266  typedef jsont value_type; // NOLINT(readability/identifiers)
267 };
268 
269 class json_stringt:public jsont
270 {
271 public:
272  explicit json_stringt(std::string _value)
273  : jsont(kindt::J_STRING, std::move(_value))
274  {
275  }
276 
277  explicit json_stringt(const irep_idt &_value)
278  : jsont(kindt::J_STRING, id2string(_value))
279  {
280  }
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 
489 jsont to_json(const structured_datat &data);
490 
491 #endif // CPROVER_UTIL_JSON_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
jsont & push_back(jsont &&json)
Definition: json.h:218
jsont & push_back(const jsont &json)
Definition: json.h:212
jsont value_type
Definition: json.h:266
void resize(std::size_t size)
Definition: json.h:197
arrayt::iterator end()
Definition: json.h:251
json_arrayt(ranget< iteratort > &&range)
Definition: json.h:192
arrayt::const_iterator end() const
Definition: json.h:256
arrayt::const_iterator begin() const
Definition: json.h:241
jsont & push_back()
Definition: json.h:224
arrayt::const_iterator cbegin() const
Definition: json.h:246
bool empty() const
Definition: json.h:207
json_arrayt()
Definition: json.h:167
void emplace_back(argumentst &&... arguments)
Definition: json.h:231
std::size_t size() const
Definition: json.h:202
json_arrayt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
Definition: json.h:177
arrayt::iterator begin()
Definition: json.h:236
arrayt::const_iterator cend() const
Definition: json.h:261
json_arrayt(std::initializer_list< jsont > &&initializer_list)
Definition: json.h:171
json_falset()
Definition: json.h:409
json_nullt()
Definition: json.h:415
json_numbert(const std::string &_value)
Definition: json.h:291
iterator begin()
Definition: json.h:369
json_objectt()
Definition: json.h:304
json_objectt(ranget< iteratort > &&range)
Definition: json.h:330
const_iterator cend() const
Definition: json.h:394
json_objectt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
Definition: json.h:315
const_iterator cbegin() const
Definition: json.h:379
const_iterator find(const std::string &key) const
Definition: json.h:359
objectt::const_iterator const_iterator
Definition: json.h:302
iterator find(const std::string &key)
Definition: json.h:354
iterator end()
Definition: json.h:384
objectt::value_type value_type
Definition: json.h:300
iterator insert(const_iterator it, value_type value)
Definition: json.h:349
const_iterator begin() const
Definition: json.h:374
std::size_t size() const
Definition: json.h:364
const_iterator end() const
Definition: json.h:389
const jsont & operator[](const std::string &key) const
Definition: json.h:340
jsont & operator[](const std::string &key)
Definition: json.h:335
json_objectt(std::initializer_list< typename objectt::value_type > &&initializer_list)
Definition: json.h:308
objectt::iterator iterator
Definition: json.h:301
json_stringt(const char *_value)
Constructon from string literal.
Definition: json.h:283
json_stringt(std::string _value)
Definition: json.h:272
json_stringt(const irep_idt &_value)
Definition: json.h:277
json_truet()
Definition: json.h:403
Definition: json.h:27
arrayt array
Definition: json.h:135
static void escape_string(const std::string &, std::ostream &)
Definition: json.cpp:18
bool is_false() const
Definition: json.h:76
kindt
Definition: json.h:34
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition: json.cpp:59
jsont(kindt _kind, arrayt &&entries)
Definition: json.h:148
json_arrayt & make_array()
Definition: json.h:418
bool is_array() const
Definition: json.h:61
json_objectt & make_object()
Definition: json.h:436
bool is_null() const
Definition: json.h:81
void swap(jsont &other)
Definition: json.cpp:161
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:154
const jsont & operator[](const std::string &key) const
Definition: json.h:114
bool is_number() const
Definition: json.h:51
std::string value
Definition: json.h:132
std::vector< jsont > arrayt
Definition: json.h:29
jsont()
Definition: json.h:86
void output(std::ostream &out) const
Definition: json.h:90
jsont(kindt _kind, objectt &&objects)
Definition: json.h:152
bool is_string() const
Definition: json.h:46
static jsont json_boolean(bool value)
Definition: json.h:97
bool is_true() const
Definition: json.h:71
std::map< std::string, jsont > objectt
Definition: json.h:30
bool is_boolean() const
Definition: json.h:66
void clear()
Definition: json.h:102
static const jsont null_json_object
Definition: json.h:125
bool is_object() const
Definition: json.h:56
kindt kind
Definition: json.h:44
jsont(kindt _kind, std::string _value)
Definition: json.h:144
static void output_object(std::ostream &out, const objectt &object, unsigned indent)
Basic handling of the printing of a JSON object.
Definition: json.cpp:132
objectt object
Definition: json.h:136
jsont(kindt _kind)
Definition: json.h:140
A way of representing nested key/value data.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
json_arrayt & to_json_array(jsont &json)
Definition: json.h:424
jsont to_json(const structured_datat &data)
Convert the structured_datat into an json object.
Definition: json.cpp:225
json_objectt & to_json_object(jsont &json)
Definition: json.h:442
std::ostream & operator<<(std::ostream &out, const jsont &src)
Definition: json.h:158
json_stringt & to_json_string(jsont &json)
Definition: json.h:454
bool operator==(const jsont &left, const jsont &right)
Definition: json.cpp:169
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
A range is a pair of a begin and an end iterators.
Definition: range.h:396