cprover
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
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
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)
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>
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#ifndef USE_STD_STRING
278 explicit json_stringt(const irep_idt &_value)
279 : jsont(kindt::J_STRING, id2string(_value))
280 {
281 }
282#endif
283
285 explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value)
286 {
287 }
288};
289
290class json_numbert:public jsont
291{
292public:
293 explicit json_numbert(const std::string &_value):
294 jsont(kindt::J_NUMBER, _value)
295 {
296 }
297};
298
299class json_objectt:public jsont
300{
301public:
302 using value_type = objectt::value_type;
303 using iterator = objectt::iterator;
304 using const_iterator = objectt::const_iterator;
305
309
310 explicit json_objectt(
311 std::initializer_list<typename objectt::value_type> &&initializer_list)
312 : jsont(kindt::J_OBJECT, objectt{initializer_list})
313 {
314 }
315
316 template <typename begin_iteratort, typename end_iteratort>
317 json_objectt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
318 : jsont(
320 objectt(
321 std::forward<begin_iteratort>(begin_iterator),
322 std::forward<end_iteratort>(end_iterator)))
323 {
324 static_assert(
325 std::is_same<
326 typename std::decay<begin_iteratort>::type,
327 typename std::decay<end_iteratort>::type>::value,
328 "The iterators must be of the same type.");
329 }
330
331 template <typename iteratort>
333 : jsont(kindt::J_OBJECT, objectt{range.begin(), range.end()})
334 {
335 }
336
337 jsont &operator[](const std::string &key)
338 {
339 return object[key];
340 }
341
342 const jsont &operator[](const std::string &key) const
343 {
344 const_iterator it = object.find(key);
345 if(it==object.end())
346 return null_json_object;
347 else
348 return it->second;
349 }
350
352 {
353 return object.insert(it, std::move(value));
354 }
355
356 iterator find(const std::string &key)
357 {
358 return object.find(key);
359 }
360
361 const_iterator find(const std::string &key) const
362 {
363 return object.find(key);
364 }
365
366 std::size_t size() const
367 {
368 return object.size();
369 }
370
372 {
373 return object.begin();
374 }
375
377 {
378 return object.begin();
379 }
380
382 {
383 return object.cbegin();
384 }
385
387 {
388 return object.end();
389 }
390
392 {
393 return object.end();
394 }
395
397 {
398 return object.cend();
399 }
400};
401
402class json_truet:public jsont
403{
404public:
406};
407
408class json_falset:public jsont
409{
410public:
412};
413
414class json_nullt:public jsont
415{
416public:
418};
419
421{
423 return static_cast<json_arrayt &>(*this);
424}
425
427{
429 return static_cast<json_arrayt &>(json);
430}
431
432inline const json_arrayt &to_json_array(const jsont &json)
433{
435 return static_cast<const json_arrayt &>(json);
436}
437
439{
441 return static_cast<json_objectt &>(*this);
442}
443
445{
447 return static_cast<json_objectt &>(json);
448}
449
451{
453 return static_cast<const json_objectt &>(json);
454}
455
457{
459 return static_cast<json_stringt &>(json);
460}
461
463{
465 return static_cast<const json_stringt &>(json);
466}
467
468bool operator==(const jsont &left, const jsont &right);
469
492
493#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:39
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:411
json_nullt()
Definition json.h:417
json_numbert(const std::string &_value)
Definition json.h:293
iterator begin()
Definition json.h:371
json_objectt()
Definition json.h:306
json_objectt(ranget< iteratort > &&range)
Definition json.h:332
const_iterator cend() const
Definition json.h:396
json_objectt(begin_iteratort &&begin_iterator, end_iteratort &&end_iterator)
Definition json.h:317
const_iterator cbegin() const
Definition json.h:381
const jsont & operator[](const std::string &key) const
Definition json.h:342
jsont & operator[](const std::string &key)
Definition json.h:337
const_iterator find(const std::string &key) const
Definition json.h:361
objectt::const_iterator const_iterator
Definition json.h:304
iterator find(const std::string &key)
Definition json.h:356
iterator end()
Definition json.h:386
objectt::value_type value_type
Definition json.h:302
iterator insert(const_iterator it, value_type value)
Definition json.h:351
const_iterator begin() const
Definition json.h:376
std::size_t size() const
Definition json.h:366
const_iterator end() const
Definition json.h:391
json_objectt(std::initializer_list< typename objectt::value_type > &&initializer_list)
Definition json.h:310
objectt::iterator iterator
Definition json.h:303
json_stringt(const char *_value)
Constructon from string literal.
Definition json.h:285
json_stringt(std::string _value)
Definition json.h:272
json_stringt(const irep_idt &_value)
Definition json.h:278
json_truet()
Definition json.h:405
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:420
bool is_array() const
Definition json.h:61
json_objectt & make_object()
Definition json.h:438
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:47
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:456
json_objectt & to_json_object(jsont &json)
Definition json.h:444
json_arrayt & to_json_array(jsont &json)
Definition json.h:426
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
Definition kdev_t.h:24
A range is a pair of a begin and an end iterators.
Definition range.h:396