Skip to content

Commit 7c41491

Browse files
peterschrammelpeterschrammel
committed
JSON streaming
1 parent 8360233 commit 7c41491

File tree

6 files changed

+286
-19
lines changed

6 files changed

+286
-19
lines changed

‎src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ SRC = arith_tools.cpp \
3535
json.cpp \
3636
json_expr.cpp \
3737
json_irep.cpp \
38+
json_stream.cpp \
3839
language.cpp \
3940
language_file.cpp \
4041
lispexpr.cpp \

‎src/util/json.cpp

Lines changed: 27 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -66,23 +66,7 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const
6666

6767
case kindt::J_OBJECT:
6868
out << '{';
69-
for(objectt::const_iterator o_it=object.begin();
70-
o_it!=object.end();
71-
o_it++)
72-
{
73-
if(o_it!=object.begin())
74-
out << ',';
75-
76-
out << '\n';
77-
78-
out << std::string((indent+1)*2, ' ');
79-
80-
out << '"';
81-
escape_string(o_it->first, out);
82-
out << '"';
83-
out << ": ";
84-
o_it->second.output_rec(out, indent+1);
85-
}
69+
output_object(out, object, indent);
8670
if(!object.empty())
8771
{
8872
out << '\n';
@@ -133,6 +117,32 @@ void jsont::output_rec(std::ostream &out, unsigned indent) const
133117
}
134118
}
135119

120+
void jsont::output_object(std::ostream &out, const objectt &object, unsigned indent)
121+
{
122+
for(objectt::const_iterator o_it=object.begin();
123+
o_it!=object.end();
124+
o_it++)
125+
{
126+
if(o_it!=object.begin())
127+
out << ',';
128+
129+
out << '\n';
130+
131+
out << std::string((indent+1)*2, ' ');
132+
133+
jsont::output_key(out, o_it->first);
134+
o_it->second.output_rec(out, indent+1);
135+
}
136+
}
137+
138+
void jsont::output_key(std::ostream &out, const std::string &key)
139+
{
140+
out << '"';
141+
jsont::escape_string(key, out);
142+
out << '"';
143+
out << ": ";
144+
}
145+
136146
void jsont::swap(jsont &other)
137147
{
138148
std::swap(other.kind, kind);

‎src/util/json.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,7 +109,6 @@ class jsont
109109
protected:
110110
void output_rec(std::ostream &, unsigned indent) const;
111111
static void escape_string(const std::string &, std::ostream &);
112-
113112
static const jsont null_json_object;
114113

115114
explicit jsont(kindt _kind):kind(_kind)
@@ -127,8 +126,13 @@ class jsont
127126

128127
typedef std::map<std::string, jsont> objectt;
129128
objectt object;
129+
static void output_object(std::ostream &out, const objectt &object, unsigned indent);
130+
static void output_key(std::ostream &out, const std::string &key);
130131

131132
std::string value;
133+
134+
friend class json_stream_objectt;
135+
friend class json_stream_arrayt;
132136
};
133137

134138
inline std::ostream &operator<<(std::ostream &out, const jsont &src)

‎src/util/json_stream.cpp

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
#include "json_stream.h"
10+
11+
#include <ostream>
12+
13+
void json_streamt::output_delimiter()
14+
{
15+
if(!first)
16+
out << ',';
17+
else
18+
first = false;
19+
out << '\n';
20+
out << std::string((indent+1)*2, ' ');
21+
}
22+
23+
json_stream_arrayt::json_stream_arrayt(std::ostream &out, unsigned indent)
24+
: json_streamt(out, indent)
25+
{
26+
out << '[';
27+
}
28+
29+
void json_stream_arrayt::output_current()
30+
{
31+
if(!object.empty())
32+
{
33+
output_delimiter();
34+
object[""].output_rec(out, indent+1);
35+
object.clear();
36+
}
37+
if(current)
38+
{
39+
current->close();
40+
}
41+
}
42+
43+
void json_stream_arrayt::output_finalizer()
44+
{
45+
out << '\n' << std::string(indent*2, ' ');
46+
out << ']';
47+
}
48+
49+
json_stream_objectt::json_stream_objectt(std::ostream &out, unsigned indent)
50+
: json_streamt(out, indent)
51+
{
52+
out << '{';
53+
}
54+
55+
json_stream_arrayt &json_streamt::create_current_array()
56+
{
57+
current =
58+
std::unique_ptr<json_streamt>(new json_stream_arrayt(out, indent + 1));
59+
return static_cast<json_stream_arrayt &>(*current);
60+
}
61+
62+
json_stream_objectt &json_streamt::create_current_object()
63+
{
64+
current =
65+
std::unique_ptr<json_streamt>(new json_stream_objectt(out, indent + 1));
66+
return static_cast<json_stream_objectt &>(*current);
67+
}
68+
69+
json_stream_objectt &json_stream_arrayt::push_back_stream_object()
70+
{
71+
PRECONDITION(open);
72+
output_current();
73+
output_delimiter();
74+
return create_current_object();
75+
}
76+
77+
json_stream_arrayt &json_stream_arrayt::push_back_stream_array()
78+
{
79+
PRECONDITION(open);
80+
output_current();
81+
output_delimiter();
82+
return create_current_array();
83+
}
84+
85+
json_stream_objectt &json_stream_objectt::push_back_stream_object(const std::string &key)
86+
{
87+
PRECONDITION(open);
88+
output_current();
89+
output_delimiter();
90+
jsont::output_key(out, key);
91+
return create_current_object();
92+
}
93+
94+
json_stream_arrayt &json_stream_objectt::push_back_stream_array(const std::string &key)
95+
{
96+
PRECONDITION(open);
97+
output_current();
98+
output_delimiter();
99+
jsont::output_key(out, key);
100+
return create_current_array();
101+
}
102+
103+
void json_stream_objectt::output_current()
104+
{
105+
for(const auto &obj : object)
106+
{
107+
output_delimiter();
108+
jsont::output_key(out, obj.first);
109+
obj.second.output_rec(out, indent+1);
110+
}
111+
object.clear();
112+
if(current)
113+
{
114+
current->close();
115+
}
116+
}
117+
118+
void json_stream_objectt::output_finalizer()
119+
{
120+
jsont::output_object(out, object, indent);
121+
out << '\n' << std::string(indent*2, ' ');
122+
out << '}';
123+
}

‎src/util/json_stream.h

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Peter Schrammel
6+
7+
\*******************************************************************/
8+
9+
10+
#ifndef CPROVER_UTIL_JSON_STREAM_H
11+
#define CPROVER_UTIL_JSON_STREAM_H
12+
13+
#include "json.h"
14+
#include "invariant.h"
15+
16+
class json_stream_objectt;
17+
class json_stream_arrayt;
18+
19+
class json_streamt
20+
{
21+
public:
22+
void close()
23+
{
24+
if(open)
25+
{
26+
output_current();
27+
output_finalizer();
28+
open = false;
29+
}
30+
}
31+
32+
protected:
33+
json_streamt(std::ostream &_out, unsigned _indent)
34+
: open(true), out(_out), indent(_indent), first(true), current(nullptr)
35+
{
36+
}
37+
38+
bool open;
39+
std::ostream &out;
40+
41+
unsigned indent;
42+
bool first;
43+
44+
typedef std::map<std::string, jsont> objectt;
45+
objectt object;
46+
47+
std::unique_ptr<json_streamt> current;
48+
json_stream_arrayt &create_current_array();
49+
json_stream_objectt &create_current_object();
50+
51+
void output_delimiter();
52+
53+
virtual void output_current()
54+
{
55+
// no-op
56+
}
57+
58+
virtual void output_finalizer()
59+
{
60+
// no-op
61+
}
62+
};
63+
64+
class json_stream_arrayt : public json_streamt
65+
{
66+
public:
67+
json_stream_arrayt(std::ostream &out, unsigned indent = 0);
68+
69+
~json_stream_arrayt()
70+
{
71+
close();
72+
}
73+
74+
void push_back(const jsont &json)
75+
{
76+
PRECONDITION(open);
77+
output_current();
78+
output_delimiter();
79+
json.output_rec(out, indent+1);
80+
}
81+
82+
jsont &push_back()
83+
{
84+
PRECONDITION(open);
85+
output_current();
86+
return object[""];
87+
}
88+
89+
json_stream_objectt &push_back_stream_object();
90+
json_stream_arrayt &push_back_stream_array();
91+
92+
protected:
93+
void output_current() override;
94+
void output_finalizer() override;
95+
};
96+
97+
class json_stream_objectt:public json_streamt
98+
{
99+
public:
100+
json_stream_objectt(std::ostream &out, unsigned indent = 0);
101+
102+
jsont &operator[](const std::string &key)
103+
{
104+
return object[key];
105+
}
106+
107+
~json_stream_objectt()
108+
{
109+
close();
110+
}
111+
112+
const jsont &operator[](const std::string &key) const
113+
{
114+
objectt::const_iterator it=object.find(key);
115+
if(it==object.end())
116+
return jsont::null_json_object;
117+
else
118+
return it->second;
119+
}
120+
121+
json_stream_objectt &push_back_stream_object(const std::string &key);
122+
json_stream_arrayt &push_back_stream_array(const std::string &key);
123+
124+
protected:
125+
void output_current() override;
126+
void output_finalizer() override;
127+
};
128+
129+
#endif // CPROVER_UTIL_JSON_STREAM_H

‎src/util/message.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,7 @@ class messaget
209209
return *this;
210210
}
211211

212-
mstreamt &operator << (const json_objectt &data)
212+
mstreamt &operator << (const jsont &data)
213213
{
214214
*this << eom; // force end of previous message
215215
if(message.message_handler)

0 commit comments

Comments
 (0)