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 
20 class json_objectt;
21 class json_arrayt;
22 
23 class jsont
24 {
25 public:
26  enum class kindt
27  {
28  J_STRING,
29  J_NUMBER,
30  J_OBJECT,
31  J_ARRAY,
32  J_TRUE,
33  J_FALSE,
34  J_NULL
35  };
36 
38 
39  bool is_string() const
40  {
41  return kind==kindt::J_STRING;
42  }
43 
44  bool is_number() const
45  {
46  return kind==kindt::J_NUMBER;
47  }
48 
49  bool is_object() const
50  {
51  return kind==kindt::J_OBJECT;
52  }
53 
54  bool is_array() const
55  {
56  return kind==kindt::J_ARRAY;
57  }
58 
59  bool is_true() const
60  {
61  return kind==kindt::J_TRUE;
62  }
63 
64  bool is_false() const
65  {
66  return kind==kindt::J_FALSE;
67  }
68 
69  bool is_null() const
70  {
71  return kind==kindt::J_NULL;
72  }
73 
74  jsont():kind(kindt::J_NULL)
75  {
76  }
77 
78  void output(std::ostream &out) const
79  {
80  output_rec(out, 0);
81  }
82 
83  void swap(jsont &other);
84 
85  static jsont json_boolean(bool value)
86  {
88  }
89 
90  void clear()
91  {
92  value.clear();
94  object.clear();
95  array.clear();
96  }
97 
100 
101  // this presumes that this is an object
102  const jsont &operator[](const std::string &key) const
103  {
104  objectt::const_iterator it=object.find(key);
105  if(it==object.end())
106  return null_json_object;
107  else
108  return it->second;
109  }
110 
111  void output_rec(std::ostream &, unsigned indent) const;
112 
113  static const jsont null_json_object;
114 
115 protected:
116  static void escape_string(const std::string &, std::ostream &);
117 
118  explicit jsont(kindt _kind):kind(_kind)
119  {
120  }
121 
122  jsont(kindt _kind, std::string _value) : kind(_kind), value(std::move(_value))
123  {
124  }
125 
126 public:
127  // should become protected
128  typedef std::vector<jsont> arrayt;
130 
131  typedef std::map<std::string, jsont> objectt;
133  static void
134  output_object(std::ostream &out, const objectt &object, unsigned indent);
135  static void output_key(std::ostream &out, const std::string &key);
136 
137  std::string value;
138 };
139 
140 inline std::ostream &operator<<(std::ostream &out, const jsont &src)
141 {
142  src.output(out);
143  return out;
144 }
145 
146 class json_arrayt:public jsont
147 {
148 public:
149  json_arrayt():jsont(kindt::J_ARRAY)
150  {
151  }
152 
153  void resize(std::size_t size)
154  {
155  array.resize(size);
156  }
157 
158  std::size_t size() const
159  {
160  return array.size();
161  }
162 
164  {
165  array.push_back(json);
166  return array.back();
167  }
168 
170  {
171  array.push_back(jsont());
172  return array.back();
173  }
174 
175  template <typename... argumentst>
176  void emplace_back(argumentst &&... arguments)
177  {
178  array.emplace_back(std::forward<argumentst>(arguments)...);
179  }
180 
181  std::vector<jsont>::iterator begin()
182  {
183  return array.begin();
184  }
185 
186  std::vector<jsont>::const_iterator begin() const
187  {
188  return array.begin();
189  }
190 
191  std::vector<jsont>::const_iterator cbegin() const
192  {
193  return array.cbegin();
194  }
195 
196  std::vector<jsont>::iterator end()
197  {
198  return array.end();
199  }
200 
201  std::vector<jsont>::const_iterator end() const
202  {
203  return array.end();
204  }
205 
206  std::vector<jsont>::const_iterator cend() const
207  {
208  return array.cend();
209  }
210 
211  typedef jsont value_type; // NOLINT(readability/identifiers)
212 };
213 
214 class json_stringt:public jsont
215 {
216 public:
217  explicit json_stringt(std::string _value)
218  : jsont(kindt::J_STRING, std::move(_value))
219  {
220  }
221 
222 #ifndef USE_STD_STRING
223  explicit json_stringt(const irep_idt &_value)
224  : jsont(kindt::J_STRING, id2string(_value))
225  {
226  }
227 #endif
228 
230  explicit json_stringt(const char *_value) : jsont(kindt::J_STRING, _value)
231  {
232  }
233 };
234 
235 class json_numbert:public jsont
236 {
237 public:
238  explicit json_numbert(const std::string &_value):
239  jsont(kindt::J_NUMBER, _value)
240  {
241  }
242 };
243 
244 class json_objectt:public jsont
245 {
246 public:
247  json_objectt():jsont(kindt::J_OBJECT)
248  {
249  }
250 
251  jsont &operator[](const std::string &key)
252  {
253  return object[key];
254  }
255 
256  const jsont &operator[](const std::string &key) const
257  {
258  objectt::const_iterator it=object.find(key);
259  if(it==object.end())
260  return null_json_object;
261  else
262  return it->second;
263  }
264 };
265 
266 class json_truet:public jsont
267 {
268 public:
269  json_truet():jsont(kindt::J_TRUE) { }
270 };
271 
272 class json_falset:public jsont
273 {
274 public:
275  json_falset():jsont(kindt::J_FALSE) { }
276 };
277 
278 class json_nullt:public jsont
279 {
280 public:
281  json_nullt():jsont(kindt::J_NULL) { }
282 };
283 
285 {
287  return static_cast<json_arrayt &>(*this);
288 }
289 
291 {
293  return static_cast<json_objectt &>(*this);
294 }
295 
296 #endif // CPROVER_UTIL_JSON_H
std::ostream & operator<<(std::ostream &out, const jsont &src)
Definition: json.h:140
bool is_object() const
Definition: json.h:49
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< jsont >::const_iterator cbegin() const
Definition: json.h:191
static void output_object(std::ostream &out, const objectt &object, unsigned indent)
Basic handling of the printing of a JSON object.
Definition: json.cpp:129
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:151
json_truet()
Definition: json.h:269
Definition: json.h:23
static jsont json_boolean(bool value)
Definition: json.h:85
bool is_number() const
Definition: json.h:44
STL namespace.
static void escape_string(const std::string &, std::ostream &)
Definition: json.cpp:15
json_arrayt & make_array()
Definition: json.h:284
jsont & push_back(const jsont &json)
Definition: json.h:163
std::map< std::string, jsont > objectt
Definition: json.h:131
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition: json.cpp:56
void output(std::ostream &out) const
Definition: json.h:78
const jsont & operator[](const std::string &key) const
Definition: json.h:256
json_stringt(const irep_idt &_value)
Definition: json.h:223
bool is_false() const
Definition: json.h:64
kindt
Definition: json.h:26
const jsont & operator[](const std::string &key) const
Definition: json.h:102
jsont value_type
Definition: json.h:211
bool is_null() const
Definition: json.h:69
objectt object
Definition: json.h:132
jsont(kindt _kind)
Definition: json.h:118
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
json_numbert(const std::string &_value)
Definition: json.h:238
std::vector< jsont >::iterator end()
Definition: json.h:196
jsont(kindt _kind, std::string _value)
Definition: json.h:122
bool is_true() const
Definition: json.h:59
std::vector< jsont >::const_iterator cend() const
Definition: json.h:206
std::vector< jsont >::const_iterator begin() const
Definition: json.h:186
jsont & operator[](const std::string &key)
Definition: json.h:251
bool is_string() const
Definition: json.h:39
bool is_array() const
Definition: json.h:54
std::string value
Definition: json.h:137
json_stringt(const char *_value)
Constructon from string literal.
Definition: json.h:230
std::vector< jsont >::const_iterator end() const
Definition: json.h:201
json_objectt()
Definition: json.h:247
static const jsont null_json_object
Definition: json.h:113
std::vector< jsont > arrayt
Definition: json.h:128
void resize(std::size_t size)
Definition: json.h:153
void swap(jsont &other)
Definition: json.cpp:158
json_arrayt()
Definition: json.h:149
json_objectt & make_object()
Definition: json.h:290
jsont()
Definition: json.h:74
json_nullt()
Definition: json.h:281
kindt kind
Definition: json.h:37
arrayt array
Definition: json.h:129
jsont & push_back()
Definition: json.h:169
json_falset()
Definition: json.h:275
std::size_t size() const
Definition: json.h:158
json_stringt(std::string _value)
Definition: json.h:217
std::vector< jsont >::iterator begin()
Definition: json.h:181
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
void clear()
Definition: json.h:90
void emplace_back(argumentst &&... arguments)
Definition: json.h:176