CBMC
Loading...
Searching...
No Matches
json.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
22
23class json_objectt;
24class json_arrayt;
25
26class jsont
27{
28protected:
29 typedef std::vector<jsont> arrayt;
30 typedef std::map<std::string, jsont> objectt;
31
32public:
33 enum class kindt
34 {
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
87 {
88 }
89
90 void output(std::ostream &out) const
91 {
92 output_rec(out, 0);
93 }
94
95 void swap(jsont &other);
96
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
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
134protected:
137
138 static void escape_string(const std::string &, std::ostream &);
139
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
153 : kind(_kind), object(std::move(objects))
154 {
155 }
156};
157
158inline std::ostream &operator<<(std::ostream &out, const jsont &src)
159{
160 src.output(out);
161 return out;
162}
163
164class json_arrayt:public jsont
165{
166public:
170
171 explicit json_arrayt(std::initializer_list<jsont> &&initializer_list)
173 {
174 }
175
176 template <typename begin_iteratort, typename end_iteratort>
178 : jsont(
179 kindt::J_ARRAY,
180 arrayt(
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>
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
269class json_stringt:public jsont
270{
271public:
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
288class json_numbert:public jsont
289{
290public:
291 explicit json_numbert(const std::string &_value):
292 jsont(kindt::J_NUMBER, _value)
293 {
294 }
295};
296
297class json_objectt:public jsont
298{
299public:
300 using value_type = objectt::value_type;
301 using iterator = objectt::iterator;
302 using const_iterator = objectt::const_iterator;
303
307
308 explicit json_objectt(
309 std::initializer_list<typename objectt::value_type> &&initializer_list)
311 {
312 }
313
314 template <typename begin_iteratort, typename end_iteratort>
316 : jsont(
318 objectt(
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>
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
400class json_truet:public jsont
401{
402public:
404};
405
406class json_falset:public jsont
407{
408public:
410};
411
412class json_nullt:public jsont
413{
414public:
416};
417
419{
421 return static_cast<json_arrayt &>(*this);
422}
423
425{
427 return static_cast<json_arrayt &>(json);
428}
429
430inline 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
449{
451 return static_cast<const json_objectt &>(json);
452}
453
455{
457 return static_cast<json_stringt &>(json);
458}
459
461{
463 return static_cast<const json_stringt &>(json);
464}
465
466bool operator==(const jsont &left, const jsont &right);
467
489jsont to_json(const structured_datat &data);
490
491#endif // CPROVER_UTIL_JSON_H
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
jsont value_type
Definition json.h:266
jsont & push_back()
Definition json.h:224
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
jsont & push_back(const jsont &json)
Definition json.h:212
arrayt::const_iterator begin() const
Definition json.h:241
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
jsont & push_back(jsont &&json)
Definition json.h:218
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 jsont & operator[](const std::string &key) const
Definition json.h:340
jsont & operator[](const std::string &key)
Definition json.h:335
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
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
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
const jsont & operator[](const std::string &key) const
Definition json.h:114
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
std::ostream & operator<<(std::ostream &out, const jsont &src)
Definition json.h:158
jsont to_json(const structured_datat &data)
Convert the structured_datat into an json object.
Definition json.cpp:225
bool operator==(const jsont &left, const jsont &right)
Definition json.cpp:169
json_stringt & to_json_string(jsont &json)
Definition json.h:454
json_objectt & to_json_object(jsont &json)
Definition json.h:442
json_arrayt & to_json_array(jsont &json)
Definition json.h:424
STL namespace.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
#define PRECONDITION(CONDITION)
Definition invariant.h:463