Line data Source code
1 : // Author(s): Wieger Wesselink, Jan Friso Groote
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/data/sort_type_checker.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_DATA_SORT_TYPE_CHECKER_H
13 : #define MCRL2_DATA_SORT_TYPE_CHECKER_H
14 :
15 : #include "mcrl2/data/find.h"
16 : #include "mcrl2/data/sort_specification.h"
17 :
18 : namespace mcrl2
19 : {
20 :
21 : namespace data
22 : {
23 :
24 : class sort_type_checker
25 : {
26 : protected:
27 : sort_specification m_sort_specification; // Intentionally a copy. If this is a reference or pointer the
28 : // object to which this referred may disappear.
29 :
30 : public:
31 : /// \brief constructs a sort expression checker.
32 4637 : sort_type_checker(const sort_specification& sort_spec, bool must_check_aliases = true)
33 4637 : : m_sort_specification(sort_spec)
34 : {
35 4637 : check_sorts();
36 4636 : if (must_check_aliases)
37 : {
38 4635 : check_aliases();
39 : }
40 4637 : }
41 :
42 671685 : const sort_specification& get_sort_specification() const
43 : {
44 671685 : return m_sort_specification;
45 : }
46 :
47 : /** \brief Type check a sort expression.
48 : * Throws an exception if the expression is not well typed.
49 : * \param[in] x A sort expression that has not been type checked.
50 : **/
51 10531 : void operator()(const sort_expression& x) const
52 : {
53 10531 : check_sort_is_declared(x);
54 10531 : }
55 :
56 : protected:
57 : // Throws a runtime_error if a rewriting loop is detected via
58 : // basic sorts, function sorts or sort containers.
59 1180 : void check_alias_circularity(
60 : const data::basic_sort& lhs,
61 : const data::sort_expression& rhs,
62 : std::set<basic_sort> sort_already_seen,
63 : const std::map < basic_sort, sort_expression >& alias_map)
64 : {
65 1180 : if (data::is_basic_sort(rhs))
66 : {
67 303 : const basic_sort& sort=atermpp::down_cast<basic_sort>(rhs);
68 303 : if (sort == lhs)
69 : {
70 10 : throw mcrl2::runtime_error("Sort alias " + data::pp(lhs) + " is circularly defined.\n");
71 : }
72 293 : if (sort_already_seen.insert(sort).second && alias_map.count(sort)>0) // sort is newly added and there is an alias for this sort.
73 : {
74 99 : check_alias_circularity(lhs,alias_map.at(sort),sort_already_seen, alias_map);
75 : }
76 290 : sort_already_seen.erase(sort);
77 290 : return;
78 : }
79 877 : if (data::is_container_sort(rhs))
80 : {
81 134 : const container_sort& c=atermpp::down_cast<container_sort>(rhs);
82 139 : check_alias_circularity(lhs,c.element_sort(),sort_already_seen, alias_map);
83 129 : return;
84 : }
85 743 : if (data::is_function_sort(rhs))
86 : {
87 41 : const function_sort& sort=atermpp::down_cast<function_sort>(rhs);
88 81 : for(const sort_expression& s: sort.domain())
89 : {
90 42 : check_alias_circularity(lhs,s,sort_already_seen, alias_map);
91 : }
92 40 : check_alias_circularity(lhs,sort.codomain(),sort_already_seen, alias_map);
93 39 : return;
94 : }
95 : // Intentionally no further search is done through a structured sort, because aliases
96 : // can be circularly defined through structured sorts. Example: sort Tree = struct leaf | node(Tree,Tree);
97 702 : assert(is_structured_sort(rhs));
98 : }
99 :
100 4637 : void check_sorts()
101 : {
102 : // Check for double occurrences of sorts, as well as overlap with the five predefined basic sorts.
103 27822 : std::set<basic_sort> defined_sorts={ sort_pos::pos(), sort_nat::nat(), sort_int::int_(), sort_real::real_() };
104 4768 : for(const basic_sort& sort: get_sort_specification().user_defined_sorts())
105 : {
106 131 : if (!defined_sorts.insert(sort).second) // Sort did already exist.
107 : {
108 0 : throw mcrl2::runtime_error("Attempt to redeclare sort " + core::pp(sort.name()));
109 : }
110 : }
111 5514 : for(const alias& a: get_sort_specification().user_defined_aliases())
112 : {
113 878 : if (!defined_sorts.insert(a.name()).second) // Sort did already exist.
114 : {
115 1 : throw mcrl2::runtime_error("Attempt to redeclare sort in alias " + data::pp(a));
116 : }
117 : }
118 4637 : }
119 :
120 :
121 : // Throws an exception if there is a problem with the alias
122 4635 : void check_aliases()
123 : {
124 4635 : std::map < basic_sort, sort_expression > alias_map;
125 5496 : for(const alias& a: get_sort_specification().user_defined_aliases())
126 : {
127 861 : alias_map[a.name()]=a.reference();
128 : }
129 :
130 4635 : std::set<data::basic_sort> sort_already_seen;
131 5487 : for(const alias& a: get_sort_specification().user_defined_aliases())
132 : {
133 858 : check_for_sort_alias_loop_through_function_sort(a.name(),a.reference(), sort_already_seen, false, alias_map);
134 854 : assert(sort_already_seen.size()==0);
135 856 : check_alias_circularity(a.name(), a.reference(),sort_already_seen, alias_map);
136 852 : assert(sort_already_seen.size()==0);
137 : }
138 :
139 : try
140 : {
141 5481 : for(const alias& a: get_sort_specification().user_defined_aliases())
142 : {
143 852 : (*this)(a.reference()); // Type check sort expression.
144 : }
145 : }
146 0 : catch (mcrl2::runtime_error& e)
147 : {
148 0 : throw mcrl2::runtime_error(std::string(e.what()) + "\ntype checking of aliases failed");
149 0 : }
150 4641 : }
151 :
152 1831 : void check_for_sort_alias_loop_through_function_sort(
153 : const basic_sort& end_search,
154 : const sort_expression& start_search,
155 : std::set < basic_sort >& visited,
156 : const bool observed_a_sort_constructor,
157 : const std::map < basic_sort, sort_expression >& alias_map)
158 : {
159 1831 : if (is_basic_sort(start_search))
160 : {
161 712 : const basic_sort& s=atermpp::down_cast<basic_sort>(start_search);
162 712 : if (s==end_search)
163 : {
164 : // We found a loop.
165 71 : if (observed_a_sort_constructor)
166 : {
167 9 : throw mcrl2::runtime_error("sort " + data::pp(end_search) + " is recursively defined via a function sort, or a set or a bag type container");
168 : }
169 : }
170 :
171 703 : if (alias_map.count(s)==0 || visited.count(s)>0)
172 : {
173 : // start_search is not a sort alias, and hence not a recursive sort, or we have already seen sort s.
174 422 : return;
175 : }
176 281 : visited.insert(s);
177 281 : check_for_sort_alias_loop_through_function_sort(end_search,alias_map.at(s),visited,observed_a_sort_constructor,alias_map);
178 281 : visited.erase(s);
179 281 : return;
180 : }
181 :
182 1119 : if (is_container_sort(start_search))
183 : {
184 : // A loop through a list container is allowed, but a loop through a set or bag container
185 : // is problematic.
186 192 : const container_sort& start_search_container=atermpp::down_cast<container_sort>(start_search);
187 192 : check_for_sort_alias_loop_through_function_sort(
188 : end_search,
189 : start_search_container.element_sort(),
190 : visited,
191 388 : start_search_container.container_name()==set_container()||start_search_container.container_name()==bag_container(),
192 : alias_map);
193 190 : return;
194 : }
195 :
196 927 : if (is_function_sort(start_search))
197 : {
198 58 : const function_sort& f_start_search=atermpp::down_cast<function_sort>(start_search);
199 58 : check_for_sort_alias_loop_through_function_sort(end_search,f_start_search.codomain(),visited,true,alias_map);
200 105 : for(const sort_expression& s: f_start_search.domain())
201 : {
202 54 : check_for_sort_alias_loop_through_function_sort(end_search,s,visited,true,alias_map);
203 : }
204 : // end_search has not been found, so:
205 51 : return;
206 : }
207 :
208 869 : assert(is_structured_sort(start_search));
209 :
210 869 : const structured_sort& struct_start_search=atermpp::down_cast<structured_sort>(start_search);
211 2554 : for(const function_symbol& f: struct_start_search.constructor_functions())
212 : {
213 1688 : if (is_function_sort(f.sort()))
214 : {
215 332 : const sort_expression_list domain_sorts=function_sort(f.sort()).domain();
216 702 : for(const sort_expression& s: domain_sorts)
217 : {
218 373 : check_for_sort_alias_loop_through_function_sort(end_search,s,visited,observed_a_sort_constructor,alias_map);
219 : }
220 332 : }
221 869 : }
222 : }
223 :
224 :
225 : // Throws an exception if the sort x is not declared
226 30183 : void check_basic_sort_is_declared(const basic_sort& x) const
227 : {
228 30183 : if (sort_bool::is_bool(x) ||
229 21484 : sort_pos::is_pos(x) ||
230 16908 : sort_nat::is_nat(x) ||
231 59457 : sort_int::is_int(x) ||
232 7790 : sort_real::is_real(x))
233 : {
234 22555 : return;
235 : }
236 7628 : if (std::find(get_sort_specification().user_defined_sorts().begin(), get_sort_specification().user_defined_sorts().end(),x)!=
237 15256 : get_sort_specification().user_defined_sorts().end())
238 : {
239 1124 : return;
240 : }
241 10210 : for(const alias& a: get_sort_specification().user_defined_aliases())
242 : {
243 10210 : if (x==a.name())
244 : {
245 6504 : return;
246 : }
247 : }
248 0 : throw mcrl2::runtime_error("basic or defined sort " + data::pp(x) + " is not declared");
249 : }
250 :
251 : void check_sort_list_is_declared(const sort_expression_list& SortExprList) const
252 : {
253 : for(const sort_expression& s: SortExprList)
254 : {
255 : check_sort_is_declared(s);
256 : }
257 : }
258 :
259 34507 : void check_sort_is_declared(const sort_expression& x) const
260 : {
261 34507 : if (is_basic_sort(x))
262 : {
263 29714 : const basic_sort& bs = atermpp::down_cast<basic_sort>(x);
264 29714 : check_basic_sort_is_declared(bs);
265 : }
266 4793 : else if (is_container_sort(x))
267 : {
268 2789 : const container_sort& cs = atermpp::down_cast<container_sort>(x);
269 2789 : check_sort_is_declared(cs.element_sort());
270 : }
271 2004 : else if (is_function_sort(x))
272 : {
273 1354 : const function_sort& fs = atermpp::down_cast<function_sort>(x);
274 1354 : check_sort_is_declared(fs.codomain());
275 3226 : for(const sort_expression& s: fs.domain())
276 : {
277 1872 : check_sort_is_declared(s);
278 : }
279 : }
280 650 : else if (is_structured_sort(x))
281 : {
282 650 : const structured_sort& ss = atermpp::down_cast<structured_sort>(x);
283 1898 : for(const structured_sort_constructor& constructor: ss.constructors())
284 : {
285 1444 : for(const structured_sort_constructor_argument& arg: constructor.arguments())
286 : {
287 196 : check_sort_is_declared(arg.sort());
288 : }
289 : }
290 : }
291 : else
292 : {
293 0 : throw mcrl2::runtime_error("this is not a sort expression " + data::pp(x));
294 : }
295 34507 : }
296 :
297 4594 : void check_for_empty_constructor_domains(const function_symbol_vector& constructors)
298 : {
299 4594 : std::set<sort_expression> possibly_empty_constructor_sorts;
300 26943 : for(const function_symbol& constructor: constructors)
301 : {
302 22349 : const sort_expression& s = constructor.sort();
303 22349 : if (is_function_sort(s))
304 : {
305 : // if s is a constant sort, nothing needs to be added.
306 6664 : possibly_empty_constructor_sorts.insert(normalize_sorts(function_sort(s).codomain(),get_sort_specification()));
307 : }
308 : }
309 :
310 : // Walk through the constructors removing constructor sorts that are not empty,
311 : // until no more constructors sorts can be removed.
312 13967 : for(bool stable=false ; !stable ;)
313 : {
314 9373 : stable=true;
315 56158 : for(const function_symbol& constructor: constructors)
316 : {
317 46785 : const sort_expression& s = constructor.sort();
318 46785 : if (!is_function_sort(s))
319 : {
320 32459 : if (possibly_empty_constructor_sorts.erase(normalize_sorts(s,get_sort_specification()))==1) // True if one element has been removed.
321 : {
322 5477 : stable=false;
323 : }
324 : }
325 : else
326 : {
327 14326 : bool has_a_domain_sort_possibly_empty_sorts=false;
328 40504 : for(const sort_expression& sort: static_cast<const function_sort&>(s).domain())
329 : {
330 26178 : if (possibly_empty_constructor_sorts.find(normalize_sorts(sort, get_sort_specification()))!=possibly_empty_constructor_sorts.end())
331 : {
332 : //
333 865 : has_a_domain_sort_possibly_empty_sorts=true;
334 865 : continue;
335 : }
336 : }
337 14326 : if (!has_a_domain_sort_possibly_empty_sorts)
338 : {
339 : // Condition below is true if one element has been removed.
340 13463 : if (possibly_empty_constructor_sorts.erase(normalize_sorts(static_cast<const function_sort&>(s).codomain(),get_sort_specification()))==1)
341 : {
342 972 : stable=false;
343 : }
344 : }
345 : }
346 : }
347 : }
348 : // Print the sorts remaining in possibly_empty_constructor_sorts, as they must be empty
349 4594 : if (possibly_empty_constructor_sorts.empty())
350 : {
351 4589 : return; // There are no empty sorts
352 : }
353 : else
354 : {
355 5 : std::string reason="the following domains are empty due to recursive constructors:";
356 12 : for(const sort_expression& sort: possibly_empty_constructor_sorts)
357 : {
358 7 : reason = reason + "\n" + data::pp(sort);
359 : }
360 5 : throw mcrl2::runtime_error(reason);
361 5 : }
362 4594 : }
363 : };
364 :
365 : } // namespace data
366 :
367 : } // namespace mcrl2
368 :
369 : #endif // MCRL2_DATA_SORT_TYPE_CHECKER_H
|