1 #include "check.h"
2 #include "is_one_step.h"
3 #include <cstddef>
4 #include <cassert>
5 #include <rumur/rumur.h>
6
7 using namespace rumur;
8
9 namespace {
10
11 class Checker : public ConstTraversal {
12
13 private:
14 bool is_tail = false;
15
16 std::vector<const Quantifier *> params;
17 ///< parameters in the ruleset context we are currently within
18
19 public:
visit_aliasdecl(const AliasDecl & n)20 void visit_aliasdecl(const AliasDecl &n) final {
21 // I think Uclid5 has nothing that could reasonably implement AliasDecl…?
22 throw Error("Uclid5 has no equivalent of alias declarations", n.loc);
23 }
24
visit_aliasrule(const AliasRule & n)25 void visit_aliasrule(const AliasRule &n) final {
26 // I think Uclid5 has nothing that could reasonably implement AliasRule…?
27 throw Error("Uclid5 has no equivalent of alias rules", n.loc);
28 }
29
visit_aliasstmt(const AliasStmt & n)30 void visit_aliasstmt(const AliasStmt &n) final {
31 // I think Uclid5 has nothing that could reasonably implement AliasStmt…?
32 throw Error("Uclid5 has no equivalent of alias statements", n.loc);
33 }
34
visit_clear(const Clear & n)35 void visit_clear(const Clear &n) final {
36 const Ptr<TypeExpr> type = n.rhs->type();
37
38 if (!type->is_simple())
39 throw Error("Clear of complex types is not supported", n.loc);
40 }
41
visit_div(const Div & n)42 void visit_div(const Div &n) final {
43 throw Error("Uclid5 has no equivalent of the division operator", n.loc);
44 }
45
visit_exists(const Exists & n)46 void visit_exists(const Exists &n) final {
47 // we could support this, but it seems rarely used so reject it for now
48 if (n.quantifier.type == nullptr && !is_one_step(n.quantifier.step))
49 throw Error("exists with a non-1 stride are not supported", n.loc);
50 }
51
visit_forall(const Forall & n)52 void visit_forall(const Forall &n) final {
53 // we could support this, but it seems rarely used so reject it for now
54 if (n.quantifier.type == nullptr && !is_one_step(n.quantifier.step))
55 throw Error("forall with a non-1 stride are not supported", n.loc);
56 }
57
visit_isundefined(const IsUndefined & n)58 void visit_isundefined(const IsUndefined &n) final {
59 throw Error("Uclid5 has no equivalent of the isundefined operator", n.loc);
60 }
61
visit_function(const Function & n)62 void visit_function(const Function &n) final {
63 assert(!is_tail && "incorrect tracking of tail statements");
64
65 for (const Ptr<VarDecl> &p : n.parameters)
66 p->visit(*this);
67 if (n.return_type != nullptr)
68 n.return_type->visit(*this);
69 for (const Ptr<Decl> &d : n.decls)
70 d->visit(*this);
71
72 // descend while only considering the last statement a tail
73 for (size_t i = 0; i + 1 < n.body.size(); ++i)
74 n.body[i]->visit(*this);
75 is_tail = true;
76 if (!n.body.empty())
77 n.body.back()->visit(*this);
78
79 // restore default is_tail state
80 is_tail = false;
81 }
82
visit_for(const For & n)83 void visit_for(const For &n) final {
84 n.quantifier.visit(*this);
85
86 // save current is_tail state
87 bool old_is_tail = is_tail;
88 is_tail = false;
89
90 for (size_t i = 0; i + 1 < n.body.size(); ++i)
91 n.body[i]->visit(*this);
92
93 // restore is_tail for the last statement in the block
94 is_tail = old_is_tail;
95
96 if (!n.body.empty())
97 n.body.back()->visit(*this);
98 }
99
visit_ifclause(const IfClause & n)100 void visit_ifclause(const IfClause &n) final {
101 if (n.condition != nullptr)
102 n.condition->visit(*this);
103
104 // save current is_tail state
105 bool old_is_tail = is_tail;
106 is_tail = false;
107
108 for (size_t i = 0; i + 1 < n.body.size(); ++i)
109 n.body[i]->visit(*this);
110
111 // restore is_tail for the last statement in the block
112 is_tail = old_is_tail;
113
114 if (!n.body.empty())
115 n.body.back()->visit(*this);
116 }
117
visit_lsh(const Lsh & n)118 void visit_lsh(const Lsh &n) final {
119 // TODO: technically we could implement this as a Uclid5 function. However,
120 // it is a little awkward because Uclid5 does not support generic functions
121 // so we would have to detect which types << is used with and emit a
122 // function for each of these.
123 throw Error("Uclid5 has no equivalent of the left shift operator", n.loc);
124 }
125
visit_mod(const Mod & n)126 void visit_mod(const Mod &n) final {
127 throw Error("Uclid5 has no equivalent of the modulo operator", n.loc);
128 }
129
visit_propertyrule(const PropertyRule & n)130 void visit_propertyrule(const PropertyRule &n) final {
131 if (n.property.category == Property::COVER)
132 throw Error("cover properties have no LTL equivalent in Uclid5", n.loc);
133
134 // forall quantifiers outside `G(F(…))` does not work in Uclid5
135 if (!params.empty() && n.property.category == Property::LIVENESS)
136 throw Error("liveness properties within rulesets cannot be translated to "
137 "Uclid5", n.loc);
138
139 for (const Quantifier *q : params) {
140 if (q->type == nullptr && !is_one_step(q->step))
141 throw Error("properties within rulesets using quantifiers with non-1 "
142 "steps are not supported", q->loc);
143 }
144
145 n.property.visit(*this);
146 }
147
visit_propertystmt(const PropertyStmt & n)148 void visit_propertystmt(const PropertyStmt &n) final {
149
150 if (n.property.category == Property::COVER)
151 throw Error("Uclid5 has no equivalent of cover statements", n.loc);
152
153 if (n.property.category == Property::LIVENESS)
154 throw Error("Ucild5 has no equivalent of liveness statements", n.loc);
155
156 n.property.visit(*this);
157 }
158
visit_put(const Put & n)159 void visit_put(const Put &n) final {
160 throw Error("Uclid5 has no equivalent of put statements except print, "
161 "which is only permitted in control blocks", n.loc);
162 }
163
visit_return(const Return & n)164 void visit_return(const Return &n) final {
165
166 // there seems to be no way to return early from a Uclid5 procedure
167 if (!is_tail)
168 throw Error("early return statements are not supported", n.loc);
169
170 if (n.expr != nullptr)
171 n.expr->visit(*this);
172 }
173
visit_rsh(const Rsh & n)174 void visit_rsh(const Rsh &n) final {
175 // TODO: technically we could implement this as a Uclid5 function. However,
176 // it is a little awkward because Uclid5 does not support generic functions
177 // so we would have to detect which types >> is used with and emit a
178 // function for each of these.
179 throw Error("Uclid5 has no equivalent of the right shift operator", n.loc);
180 }
181
visit_ruleset(const Ruleset & n)182 void visit_ruleset(const Ruleset &n) final {
183
184 for (const Quantifier &q : n.quantifiers) {
185 q.visit(*this);
186 // make each parameter visible to following children as we descend
187 params.push_back(&q);
188 }
189
190 for (const Ptr<Rule> &r : n.rules)
191 r->visit(*this);
192
193 assert(params.size() >= n.quantifiers.size() &&
194 "ruleset parameter management out of sync");
195 for (size_t i = 0; i < n.quantifiers.size(); ++i) {
196 size_t j __attribute__((unused))
197 = params.size() - n.quantifiers.size() + i;
198 assert(params[j] == &n.quantifiers[i] &&
199 "ruleset parameter management out of sync");
200 }
201
202 // remove the parameters as we ascend
203 params.resize(params.size() - n.quantifiers.size());
204 }
205
visit_simplerule(const SimpleRule & n)206 void visit_simplerule(const SimpleRule &n) final {
207 assert(!is_tail && "incorrect trackin of tail statements");
208
209 for (const Quantifier &q : n.quantifiers)
210 q.visit(*this);
211 for (const Ptr<AliasDecl> &a : n.aliases)
212 a->visit(*this);
213 if (n.guard != nullptr)
214 n.guard->visit(*this);
215 for (const Ptr<Decl> &d : n.decls)
216 d->visit(*this);
217
218 // descend while only considering the last statement a tail
219 for (size_t i = 0; i + 1 < n.body.size(); ++i)
220 n.body[i]->visit(*this);
221 is_tail = true;
222 if (!n.body.empty())
223 n.body.back()->visit(*this);
224
225 // restore default is_tail state
226 is_tail = false;
227 }
228
visit_startstate(const StartState & n)229 void visit_startstate(const StartState &n) final {
230 assert(!is_tail && "incorrect trackin of tail statements");
231
232 for (const Quantifier &q : n.quantifiers)
233 q.visit(*this);
234 for (const Ptr<AliasDecl> &a : n.aliases)
235 a->visit(*this);
236 for (const Ptr<Decl> &d : n.decls)
237 d->visit(*this);
238
239 // descend while only considering the last statement a tail
240 for (size_t i = 0; i + 1 < n.body.size(); ++i)
241 n.body[i]->visit(*this);
242 is_tail = true;
243 if (!n.body.empty())
244 n.body.back()->visit(*this);
245
246 // restore default is_tail state
247 is_tail = false;
248 }
249
visit_switchcase(const SwitchCase & n)250 void visit_switchcase(const SwitchCase &n) final {
251 for (const Ptr<Expr> &m : n.matches)
252 m->visit(*this);
253
254 // save current is_tail state
255 bool old_is_tail = is_tail;
256 is_tail = false;
257
258 for (size_t i = 0; i + 1 < n.body.size(); ++i)
259 n.body[i]->visit(*this);
260
261 // restore is_tail for the last statement in the block
262 is_tail = old_is_tail;
263
264 if (!n.body.empty())
265 n.body.back()->visit(*this);
266 }
267
visit_while(const While & n)268 void visit_while(const While &n) final {
269 n.condition->visit(*this);
270
271 // save current is_tail state
272 bool old_is_tail = is_tail;
273 is_tail = false;
274
275 for (size_t i = 0; i + 1 < n.body.size(); ++i)
276 n.body[i]->visit(*this);
277
278 // restore is_tail for the last statement in the block
279 is_tail = old_is_tail;
280
281 if (!n.body.empty())
282 n.body.back()->visit(*this);
283 }
284 };
285
286 } // namespace
287
check(const Node & n)288 void check(const Node &n) {
289 Checker c;
290 n.visit(c);
291 }
292