1 /**++
2 Copyright (c) 2017 Microsoft Corporation and Matteo Marescotti
3 
4 Module Name:
5 
6     spacer_json.cpp
7 
8 Abstract:
9 
10     SPACER json marshalling support
11 
12 Author:
13 
14     Matteo Marescotti
15 
16 Notes:
17 
18 --*/
19 
20 #include <iomanip>
21 #include "spacer_context.h"
22 #include "spacer_json.h"
23 #include "spacer_util.h"
24 
25 namespace spacer {
26 
json_marshal(std::ostream & out,ast * t,ast_manager & m)27 static std::ostream &json_marshal(std::ostream &out, ast *t, ast_manager &m) {
28 
29     mk_epp pp = mk_epp(t, m);
30     std::ostringstream ss;
31     ss << pp;
32     out << "\"";
33     for (auto &c:ss.str()) {
34         switch (c) {
35         case '"':
36             out << "\\\"";
37             break;
38         case '\\':
39             out << "\\\\";
40             break;
41         case '\b':
42             out << "\\b";
43             break;
44         case '\f':
45             out << "\\f";
46             break;
47         case '\n':
48             out << "\\n";
49             break;
50         case '\r':
51             out << "\\r";
52             break;
53         case '\t':
54             out << "\\t";
55             break;
56         default:
57             if ('\x00' <= c && c <= '\x1f') {
58                 out << "\\u"
59                     << std::hex << std::setw(4) << std::setfill('0') << (int) c;
60             } else {
61                 out << c;
62             }
63         }
64     }
65     out << "\"";
66     return out;
67 }
68 
json_marshal(std::ostream & out,lemma * l)69 static std::ostream &json_marshal(std::ostream &out, lemma *l) {
70     out << "{"
71         << R"("init_level":")" << l->init_level()
72         << R"(", "level":")" << l->level()
73         << R"(", "expr":)";
74     json_marshal(out, l->get_expr(), l->get_ast_manager());
75     out << "}";
76     return out;
77 }
78 
json_marshal(std::ostream & out,const lemma_ref_vector & lemmas)79 static std::ostream &json_marshal(std::ostream &out, const lemma_ref_vector &lemmas) {
80 
81         std::ostringstream ls;
82         for (auto l:lemmas) {
83             ls << ((unsigned)ls.tellp() == 0 ? "" : ",");
84             json_marshal(ls, l);
85         }
86         out << "[" << ls.str() << "]";
87         return out;
88     }
89 
90 
register_lemma(lemma * l)91 void json_marshaller::register_lemma(lemma *l) {
92     if (l->has_pob()) {
93         m_relations[&*l->get_pob()][l->get_pob()->depth()].push_back(l);
94     }
95 }
96 
register_pob(pob * p)97 void json_marshaller::register_pob(pob *p) {
98     m_relations[p];
99 }
100 
marshal_lemmas_old(std::ostream & out) const101 void json_marshaller::marshal_lemmas_old(std::ostream &out) const {
102     unsigned pob_id = 0;
103     for (auto &pob_map:m_relations) {
104         std::ostringstream pob_lemmas;
105         for (auto &depth_lemmas : pob_map.second) {
106             pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",")
107                        << "\"" << depth_lemmas.first << "\":";
108             json_marshal(pob_lemmas, depth_lemmas.second);
109         }
110         if (pob_lemmas.tellp()) {
111             out << ((unsigned)out.tellp() == 0 ? "" : ",\n");
112             out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}";
113         }
114         pob_id++;
115     }
116 }
marshal_lemmas_new(std::ostream & out) const117 void json_marshaller::marshal_lemmas_new(std::ostream &out) const {
118     unsigned pob_id = 0;
119     for (auto &pob_map:m_relations) {
120         std::ostringstream pob_lemmas;
121         pob *n = pob_map.first;
122         unsigned i = 0;
123         for (auto *l : n->lemmas()) {
124             pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",")
125                        << "\"" << i++ << "\":";
126             lemma_ref_vector lemmas_vec;
127             lemmas_vec.push_back(l);
128             json_marshal(pob_lemmas, lemmas_vec);
129         }
130 
131         if (pob_lemmas.tellp()) {
132             out << ((unsigned)out.tellp() == 0 ? "" : ",\n");
133             out << "\"" << pob_id << "\":{" << pob_lemmas.str() << "}";
134         }
135         pob_id++;
136     }
137 }
138 
marshal(std::ostream & out) const139 std::ostream &json_marshaller::marshal(std::ostream &out) const {
140     std::ostringstream nodes;
141     std::ostringstream edges;
142     std::ostringstream lemmas;
143 
144     if (m_old_style)
145         marshal_lemmas_old(lemmas);
146     else
147         marshal_lemmas_new(lemmas);
148 
149     unsigned pob_id = 0;
150     unsigned depth = 0;
151     while (true) {
152         double root_expand_time = m_ctx->get_root().get_expand_time(depth);
153         bool a = false;
154         pob_id = 0;
155         for (auto &pob_map:m_relations) {
156             pob *n = pob_map.first;
157             double expand_time = n->get_expand_time(depth);
158             if (expand_time > 0) {
159                 a = true;
160                 std::ostringstream pob_expr;
161                 json_marshal(pob_expr, n->post(), n->get_ast_manager());
162 
163                 nodes << ((unsigned)nodes.tellp() == 0 ? "" : ",\n") <<
164                     "{\"id\":\"" << depth << n <<
165                     "\",\"relative_time\":\"" << expand_time / root_expand_time <<
166                     "\",\"absolute_time\":\"" << std::setprecision(2) << expand_time <<
167                     "\",\"predicate\":\"" << n->pt().head()->get_name() <<
168                     "\",\"expr_id\":\"" << n->post()->get_id() <<
169                     "\",\"pob_id\":\"" << pob_id <<
170                     "\",\"depth\":\"" << depth <<
171                     "\",\"expr\":" << pob_expr.str() << "}";
172                 if (n->parent()) {
173                     edges << ((unsigned)edges.tellp() == 0 ? "" : ",\n") <<
174                         "{\"from\":\"" << depth << n->parent() <<
175                         "\",\"to\":\"" << depth << n << "\"}";
176                 }
177             }
178             pob_id++;
179         }
180         if (!a) {
181             break;
182         }
183         depth++;
184     }
185     out << "{\n\"nodes\":[\n" << nodes.str() << "\n],\n";
186     out << "\"edges\":[\n" << edges.str() << "\n],\n";
187     out << "\"lemmas\":{\n" << lemmas.str() << "\n}\n}\n";
188     return out;
189 }
190 
191 }
192