CBMC
json.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "json.h"
10 
11 #include "structured_data.h"
12 
13 #include <algorithm>
14 #include <ostream>
15 
17 
18 void jsont::escape_string(const std::string &src, std::ostream &out)
19 {
20  for(const auto &ch : src)
21  {
22  switch(ch)
23  {
24  case '\\':
25  case '"':
26  out << '\\';
27  out << ch;
28  break;
29 
30  case '\b':
31  out << "\\b";
32  break;
33 
34  case '\f':
35  out << "\\f";
36  break;
37 
38  case '\n':
39  out << "\\n";
40  break;
41 
42  case '\r':
43  out << "\\r";
44  break;
45 
46  case '\t':
47  out << "\\t";
48  break;
49 
50  default:
51  out << ch;
52  }
53  }
54 }
55 
59 void jsont::output_rec(std::ostream &out, unsigned indent) const
60 {
61  switch(kind)
62  {
63  case kindt::J_STRING:
64  out << '"';
65  escape_string(value, out);
66  out << '"';
67  break;
68 
69  case kindt::J_NUMBER:
70  out << value;
71  break;
72 
73  case kindt::J_OBJECT:
74  out << '{';
75  output_object(out, object, indent);
76  if(!object.empty())
77  {
78  out << '\n';
79  out << std::string(indent*2, ' ');
80  }
81  out << '}';
82  break;
83 
84  case kindt::J_ARRAY:
85  out << '[';
86 
87  if(array.empty())
88  out << ' ';
89  else
90  {
91  for(arrayt::const_iterator a_it=array.begin();
92  a_it!=array.end();
93  a_it++)
94  {
95  if(a_it!=array.begin())
96  out << ',';
97 
98  if(a_it->is_object())
99  {
100  out << '\n';
101  out << std::string((indent+1)*2, ' ');
102  }
103  else
104  out << ' ';
105 
106  a_it->output_rec(out, indent+1);
107  }
108 
109  if(array.back().is_object())
110  out << '\n' << std::string(indent*2, ' ');
111  else
112  out << ' ';
113  }
114 
115  out << ']';
116  break;
117 
118  case kindt::J_TRUE: out << "true"; break;
119 
120  case kindt::J_FALSE: out << "false"; break;
121 
122  case kindt::J_NULL: out << "null"; break;
123  }
124 }
125 
133  std::ostream &out,
134  const objectt &object,
135  unsigned indent)
136 {
137  for(objectt::const_iterator o_it = object.begin(); o_it != object.end();
138  o_it++)
139  {
140  if(o_it != object.begin())
141  out << ',';
142 
143  // A JSON object always starts with an opening brace,
144  // after which we put a newline.
145  out << '\n';
146 
147  out << std::string((indent + 1) * 2, ' ');
148 
149  jsont::output_key(out, o_it->first);
150  o_it->second.output_rec(out, indent + 1);
151  }
152 }
153 
154 void jsont::output_key(std::ostream &out, const std::string &key)
155 {
156  out << '"';
157  jsont::escape_string(key, out);
158  out << "\": ";
159 }
160 
161 void jsont::swap(jsont &other)
162 {
163  std::swap(other.kind, kind);
164  other.array.swap(array);
165  other.object.swap(object);
166  other.value.swap(value);
167 }
168 
169 bool operator==(const jsont &left, const jsont &right)
170 {
171  if(left.kind != right.kind)
172  return false;
173  switch(left.kind)
174  {
176  return true;
178  return true;
180  return true;
182  return left.value == right.value;
184  return left.value == right.value;
186  {
187  const auto &left_array = static_cast<const json_arrayt &>(left);
188  const auto &right_array = static_cast<const json_arrayt &>(right);
189  return left_array.size() == right_array.size() &&
190  std::equal(
191  left_array.begin(), left_array.end(), right_array.begin());
192  }
194  {
195  const auto &left_object = static_cast<const json_objectt &>(left);
196  const auto &right_object = static_cast<const json_objectt &>(right);
197  if(left_object.size() != left_object.size())
198  return false;
199  return std::all_of(
200  left_object.begin(),
201  left_object.end(),
202  [&](const std::pair<std::string, jsont> &pair) {
203  return right_object[pair.first] == pair.second;
204  });
205  }
206  }
207  UNREACHABLE;
208 }
209 
211 {
212  if(entry.is_leaf())
213  return entry.leaf_object();
214  else
215  {
216  json_objectt result;
217  for(const auto &sub_entry : entry.children())
218  {
219  result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
220  }
221  return std::move(result);
222  }
223 }
224 
226 {
227  if(data.data().size() == 0)
228  return jsont{};
229 
230  json_objectt result;
231  for(const auto &sub_entry : data.data())
232  {
233  result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
234  }
235  return std::move(result);
236 }
std::size_t size() const
Definition: json.h:202
Definition: json.h:27
arrayt array
Definition: json.h:135
static void escape_string(const std::string &, std::ostream &)
Definition: json.cpp:18
void output_rec(std::ostream &, unsigned indent) const
Recursive printing of the json object.
Definition: json.cpp:59
void swap(jsont &other)
Definition: json.cpp:161
static void output_key(std::ostream &out, const std::string &key)
Definition: json.cpp:154
std::string value
Definition: json.h:132
std::map< std::string, jsont > objectt
Definition: json.h:30
static const jsont null_json_object
Definition: json.h:125
kindt kind
Definition: json.h:44
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
A way of representing nested key/value data.
const std::map< labelt, structured_data_entryt > & data() const
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
jsont json_node(const structured_data_entryt &entry)
Definition: json.cpp:210
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
const std::map< labelt, structured_data_entryt > & children() const