Line data Source code
1 : // Author(s): Maurice Laveaux.
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 :
10 : #ifndef MCRL2_ATERMPP_ATERM_POOL_STORAGE_IMPLEMENTION_H
11 : #define MCRL2_ATERMPP_ATERM_POOL_STORAGE_IMPLEMENTION_H
12 : #pragma once
13 :
14 : #include <type_traits>
15 : #include <cstring>
16 : #include "mcrl2/utilities/stack_array.h"
17 : #include "mcrl2/atermpp/detail/aterm_pool.h"
18 :
19 :
20 :
21 : namespace atermpp
22 : {
23 : namespace detail
24 : {
25 :
26 : /// \brief Construct the proxy where its arguments are given by applying the converter
27 : /// to each element in the iterator.
28 : template<std::size_t N,
29 : typename InputIterator,
30 : typename TermConverter,
31 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value, void>::type* = nullptr,
32 : typename std::enable_if<std::is_convertible<
33 : typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
34 : aterm>::value, void>::type* = nullptr>
35 791082 : inline std::array<unprotected_aterm, N> construct_arguments(InputIterator it, InputIterator end, TermConverter converter)
36 : {
37 : // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
38 791082 : mcrl2::utilities::mcrl2_unused(end);
39 :
40 : // Copy the arguments into this array.
41 791082 : std::array<unprotected_aterm, N> arguments;
42 3070116 : for (size_t i = 0; i < N; ++i)
43 : {
44 2279034 : assert(it != end);
45 2279034 : arguments[i] = converter(*it);
46 :
47 2279034 : ++it;
48 : }
49 791082 : assert(it == end);
50 :
51 791082 : return arguments;
52 : }
53 :
54 : /// \brief Construct the proxy where its arguments are given by applying the converter
55 : /// to each element in the iterator.
56 : template<std::size_t N,
57 : typename InputIterator,
58 : typename TermConverter,
59 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value, void>::type* = nullptr,
60 : typename std::enable_if<std::is_same<
61 : typename std::invoke_result<TermConverter,
62 : typename InputIterator::value_type&,
63 : typename InputIterator::value_type>::type,
64 : void>::value, void>::type* = nullptr>
65 9273255 : inline std::array<unprotected_aterm, N> construct_arguments(InputIterator it, InputIterator end, TermConverter converter)
66 : {
67 : // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
68 9273255 : mcrl2::utilities::mcrl2_unused(end);
69 :
70 : // Copy the arguments into this array. Doesn't change any reference count, because they are unprotected terms.
71 9273255 : std::array<unprotected_aterm, N> arguments;
72 34837074 : for (size_t i = 0; i < N; ++i)
73 : {
74 25563819 : assert(it != end);
75 25563819 : typename InputIterator::value_type& t= *reinterpret_cast<typename InputIterator::value_type*>(&arguments[i]);
76 25563819 : converter(t, *it);
77 25563819 : ++it;
78 : }
79 9273255 : assert(it == end);
80 :
81 9273255 : return arguments;
82 : }
83 :
84 6273533 : void mark_term(const _aterm& root, std::stack<std::reference_wrapper<_aterm>>& todo)
85 : {
86 6273533 : if (!root.is_marked())
87 : {
88 : // Do not use the stack, because this might run out of stack memory for large lists.
89 10587 : todo.push(const_cast<_aterm&>(root));
90 :
91 : // Mark the term depth-first to reduce the maximum todo size required.
92 40005 : while (!todo.empty())
93 : {
94 29418 : _aterm& term = todo.top();
95 29418 : todo.pop();
96 :
97 : // Each term should be marked.
98 29418 : term.mark();
99 : // Determine the arity of the function application.
100 29418 : const std::size_t arity = term.function().arity();
101 29418 : _term_appl& term_appl = static_cast<_term_appl&>(term);
102 :
103 91937 : for (std::size_t i = 0; i < arity; ++i)
104 : {
105 : // Marks all arguments that are not already (marked as) reachable, because the current
106 : // term is reachable and as such its arguments are reachable as well.
107 62519 : _aterm& argument = *detail::address(term_appl.arg(i));
108 62519 : if (!argument.is_marked())
109 : {
110 18831 : argument.mark();
111 :
112 : // Add the argument to be explored as well.
113 18831 : todo.push(argument);
114 : }
115 : }
116 :
117 : }
118 : }
119 6273533 : }
120 :
121 : #define ATERM_POOL_STORAGE_TEMPLATES template<typename Element, typename Hash, typename Equals, std::size_t N>
122 : #define ATERM_POOL_STORAGE aterm_pool_storage<Element, Hash, Equals, N>
123 :
124 : ATERM_POOL_STORAGE_TEMPLATES
125 1430 : ATERM_POOL_STORAGE::aterm_pool_storage(aterm_pool& pool) :
126 1430 : m_pool(pool),
127 1430 : m_term_set(1 << 14)
128 1430 : {}
129 :
130 : ATERM_POOL_STORAGE_TEMPLATES
131 1 : void ATERM_POOL_STORAGE::add_deletion_hook(function_symbol sym, term_callback callback)
132 : {
133 1 : for (const auto& hook : m_deletion_hooks)
134 : {
135 0 : mcrl2::utilities::mcrl2_unused(hook);
136 0 : assert(hook.first != sym);
137 : }
138 1 : m_deletion_hooks.emplace_back(sym, callback);
139 1 : }
140 :
141 : ATERM_POOL_STORAGE_TEMPLATES
142 19731852 : bool ATERM_POOL_STORAGE::create_int(aterm& term, std::size_t value)
143 : {
144 19731852 : return emplace(term, value);
145 : }
146 :
147 : ATERM_POOL_STORAGE_TEMPLATES
148 1188023 : bool ATERM_POOL_STORAGE::create_term(aterm& term, const function_symbol& symbol)
149 : {
150 1188023 : assert(symbol.arity() == 0);
151 1188023 : return emplace(term, symbol);
152 : }
153 :
154 : template <std::size_t N>
155 46562858 : void store_in_argument_array_(std::size_t , std::array<unprotected_aterm, N>& )
156 46562858 : {}
157 :
158 : template <std::size_t N, class FUNCTION_OR_TERM_TYPE, typename... Args>
159 98625555 : void store_in_argument_array_(std::size_t i,
160 : std::array<unprotected_aterm, N>& argument_array,
161 : FUNCTION_OR_TERM_TYPE& function_or_term,
162 : const Args&... args)
163 : {
164 : if constexpr (std::is_convertible<FUNCTION_OR_TERM_TYPE,atermpp::aterm>::value)
165 : {
166 39337060 : argument_array[i]=function_or_term;
167 : }
168 : // check whether the function_or_term invoked on an empty argument yields an aterm.
169 : else if constexpr (mcrl2::utilities::is_applicable< FUNCTION_OR_TERM_TYPE, void>::value)
170 : {
171 : argument_array[i]=function_or_term();
172 : }
173 : // Otherwise function_or_term is supposed to have type void(term& result), putting the term in result.
174 : else
175 : {
176 : // function_or_term(static_cast<Term&>(argument_array[i]));
177 :
178 : typedef mcrl2::utilities::function_traits<decltype(&FUNCTION_OR_TERM_TYPE::operator())> traits;
179 59288495 : function_or_term(static_cast<typename traits::template arg<0>::type&>(argument_array[i]));
180 : }
181 98625553 : store_in_argument_array_(i+1, argument_array, args...);
182 98625551 : }
183 :
184 : template <std::size_t N, typename... Args>
185 46562860 : void store_in_argument_array(std::array<unprotected_aterm, N>& argument_array,
186 : const Args&... args)
187 : {
188 46562860 : store_in_argument_array_(0, argument_array, args...);
189 46562858 : }
190 :
191 :
192 :
193 : ATERM_POOL_STORAGE_TEMPLATES
194 : template<class ...Terms>
195 147845387 : bool ATERM_POOL_STORAGE::create_appl(aterm& term, const function_symbol& symbol, const Terms&... arguments)
196 : {
197 147845387 : assert(symbol.arity() == sizeof...(arguments));
198 : if constexpr (detail::are_terms<Terms...>::value)
199 : {
200 121003566 : return emplace(term, symbol, arguments...);
201 : }
202 : else
203 : {
204 26841821 : std::array<unprotected_aterm, N> argument_array;
205 :
206 : // Evaluate the functions or terms and put the result in "argument_array".
207 26841821 : store_in_argument_array(argument_array, arguments...);
208 :
209 26841819 : return emplace(term, symbol, argument_array.begin(), argument_array.end());
210 : }
211 : }
212 :
213 : ATERM_POOL_STORAGE_TEMPLATES
214 : template<typename ForwardIterator>
215 1011056 : bool ATERM_POOL_STORAGE::create_appl_iterator(aterm& term,
216 : const function_symbol& symbol,
217 : ForwardIterator begin,
218 : ForwardIterator end)
219 : {
220 1011056 : return emplace(term, symbol, begin, end);
221 : }
222 :
223 : ATERM_POOL_STORAGE_TEMPLATES
224 : template<typename InputIterator, typename TermConverter>
225 10064337 : bool ATERM_POOL_STORAGE::create_appl_iterator(aterm& term,
226 : const function_symbol& symbol,
227 : TermConverter converter,
228 : InputIterator begin,
229 : InputIterator end)
230 : {
231 10064337 : std::array<unprotected_aterm, N> arguments = construct_arguments<N>(begin, end, converter);
232 20128674 : return emplace(term, symbol, arguments);
233 : }
234 :
235 : ATERM_POOL_STORAGE_TEMPLATES
236 : template<typename ForwardIterator>
237 484 : bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
238 : const function_symbol& symbol,
239 : ForwardIterator begin,
240 : ForwardIterator end)
241 : {
242 484 : return emplace(term, symbol, begin, end);
243 : }
244 :
245 : ATERM_POOL_STORAGE_TEMPLATES
246 : template<typename InputIterator,
247 : typename TermConverter,
248 : typename std::enable_if<std::is_convertible<
249 : typename std::invoke_result<TermConverter, typename InputIterator::value_type>::type,
250 : aterm>::value, void>::type*>
251 29 : bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
252 : const function_symbol& symbol,
253 : TermConverter converter,
254 : InputIterator it,
255 : InputIterator end)
256 : {
257 : // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
258 29 : mcrl2::utilities::mcrl2_unused(end);
259 :
260 29 : MCRL2_DECLARE_STACK_ARRAY(arguments, unprotected_aterm, symbol.arity());
261 493 : for (std::size_t i = 0; i < symbol.arity(); ++i)
262 : {
263 464 : assert(it != end);
264 464 : arguments[i] = converter(*it);
265 464 : ++it;
266 : }
267 29 : assert(it == end);
268 :
269 : // Find or create a new term and return it.
270 58 : return emplace(term, symbol, arguments.begin(), arguments.end());
271 29 : }
272 :
273 : ATERM_POOL_STORAGE_TEMPLATES
274 : template<typename InputIterator,
275 : typename TermConverter,
276 : typename std::enable_if<std::is_same<
277 : typename std::invoke_result<TermConverter,
278 : typename InputIterator::value_type&,
279 : typename InputIterator::value_type>::type,
280 : void>::value, void>::type*>
281 1138 : bool ATERM_POOL_STORAGE::create_appl_dynamic(aterm& term,
282 : const function_symbol& symbol,
283 : TermConverter converter,
284 : InputIterator it,
285 : InputIterator end)
286 : {
287 : // The end is only used for debugging to ensure that the arity and std::distance(it, end) match.
288 1138 : mcrl2::utilities::mcrl2_unused(end);
289 :
290 1138 : MCRL2_DECLARE_STACK_ARRAY(arguments, unprotected_aterm, symbol.arity());
291 16486 : for (std::size_t i = 0; i < symbol.arity(); ++i)
292 : {
293 15348 : assert(it != end);
294 : // The construction below is possible as with protection sets the new term simply
295 : // overwrites the object at arguments[i].
296 15348 : converter(reinterpret_cast<typename InputIterator::value_type&>(arguments[i]), *it);
297 15348 : ++it;
298 : }
299 1138 : assert(it == end);
300 :
301 : // Find or create a new term and return it.
302 2276 : return emplace(term, symbol, arguments.begin(), arguments.end());
303 1138 : }
304 :
305 :
306 : ATERM_POOL_STORAGE_TEMPLATES
307 10150 : void ATERM_POOL_STORAGE::print_performance_stats(const char* identifier) const
308 : {
309 : if (EnableHashtableMetrics)
310 : {
311 : mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << ") hashtable:\n";
312 : print_performance_statistics(m_term_set);
313 : }
314 :
315 : if (EnableGarbageCollectionMetrics && m_erasedBlocks > 0)
316 : {
317 : mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << "): Consolidate removed " << m_erasedBlocks << " blocks.\n";
318 : }
319 :
320 : if (EnableCreationMetrics)
321 : {
322 : mCRL2log(mcrl2::log::info) << "g_term_pool(" << identifier << "): emplace() " << m_term_metric.message() << ".\n";
323 : }
324 10150 : }
325 :
326 : ATERM_POOL_STORAGE_TEMPLATES
327 10150 : void ATERM_POOL_STORAGE::sweep()
328 : {
329 : // Iterate over all terms and removes the ones that are marked.
330 256700 : for (auto it = m_term_set.begin(); it != m_term_set.end(); )
331 : {
332 246550 : const Element& term = *it;
333 :
334 246550 : if (!term.is_marked())
335 : {
336 : // For constants, i.e., arity zero and integer terms we do not mark, but use their reachability directly.
337 217132 : it = destroy(it);
338 : }
339 : else
340 : {
341 : // Reset terms that have been marked.
342 29418 : term.unmark();
343 29418 : ++it;
344 : }
345 : }
346 :
347 : if constexpr (EnableBlockAllocator)
348 : {
349 : // Clean up unnecessary blocks.
350 10150 : m_erasedBlocks = m_term_set.get_allocator().consolidate();
351 : }
352 10150 : }
353 :
354 : ATERM_POOL_STORAGE_TEMPLATES
355 380 : void ATERM_POOL_STORAGE::resize_if_needed()
356 : {
357 380 : m_term_set.rehash_if_needed();
358 380 : }
359 :
360 : /// PRIVATE FUNCTIONS
361 :
362 : ATERM_POOL_STORAGE_TEMPLATES
363 217132 : void ATERM_POOL_STORAGE::call_deletion_hook(unprotected_aterm term)
364 : {
365 217133 : for (const auto& [symbol, callback] : m_deletion_hooks)
366 : {
367 1 : if (symbol == term.function())
368 : {
369 1 : assert(verify_term(*detail::address(term)));
370 1 : callback(static_cast<const aterm&>(term));
371 : }
372 : }
373 217132 : }
374 :
375 :
376 : ATERM_POOL_STORAGE_TEMPLATES
377 9135 : bool ATERM_POOL_STORAGE::verify_mark()
378 : {
379 : // Check for consistency that if a term is marked then its arguments are as well.
380 261962 : for (const Element& term : m_term_set)
381 : {
382 243692 : if (term.is_marked() && term.function().arity() > 0)
383 : {
384 23083 : const _term_appl& ta = static_cast<_term_appl&>(const_cast<Element&>(term));
385 85602 : for (std::size_t i = 0; i < ta.function().arity(); ++i)
386 : {
387 62519 : assert(detail::address(ta.arg(i))->is_marked());
388 : }
389 : }
390 : }
391 9135 : return true;
392 : }
393 :
394 : ATERM_POOL_STORAGE_TEMPLATES
395 10150 : bool ATERM_POOL_STORAGE::verify_sweep()
396 : {
397 : // Check that no argument was removed from a reachable term.
398 49718 : for (const Element& term : m_term_set)
399 : {
400 : (void)term;
401 29418 : assert(verify_term(term));
402 : }
403 10150 : return true;
404 : }
405 :
406 : /// Private definitions
407 :
408 : ATERM_POOL_STORAGE_TEMPLATES
409 217132 : typename ATERM_POOL_STORAGE::iterator ATERM_POOL_STORAGE::destroy(iterator it)
410 : {
411 : // Store the term temporarily to be able to deallocate it after removing it from the set.
412 217132 : const Element& term = *it;
413 :
414 : // Trigger the deletion hook before the term is actually destroyed.
415 217132 : call_deletion_hook(&term);
416 :
417 : // Remove them from the hash table, will also destroy terms with fixed arity.
418 217132 : return m_term_set.erase(it);
419 : }
420 :
421 : ATERM_POOL_STORAGE_TEMPLATES
422 : template<typename ...Args>
423 179842304 : bool ATERM_POOL_STORAGE::emplace(aterm& term, Args&&... args)
424 : {
425 179842304 : auto [it, added] = m_term_set.emplace(std::forward<Args>(args)...);
426 179842304 : new (&term) atermpp::unprotected_aterm(&*it);
427 :
428 179842304 : if (added)
429 : {
430 : if (EnableCreationMetrics) { m_term_metric.miss(); }
431 : }
432 : else if (EnableCreationMetrics)
433 : {
434 : // A term was already found in the set.
435 : m_term_metric.hit();
436 : }
437 :
438 179842304 : return added;
439 : }
440 :
441 : ATERM_POOL_STORAGE_TEMPLATES
442 : constexpr bool ATERM_POOL_STORAGE::is_dynamic_storage() const
443 : {
444 : return N == DynamicNumberOfArguments;
445 : }
446 :
447 : ATERM_POOL_STORAGE_TEMPLATES
448 : template<std::size_t Arity>
449 1486466 : bool ATERM_POOL_STORAGE::verify_term(const _aterm& term)
450 : {
451 : // Check that a valid function symbol was used and that its arity belongs to this storage.
452 1486466 : assert(term.function().defined());
453 29419 : assert(Arity == DynamicNumberOfArguments ? true : term.function().arity() == N);
454 :
455 : // Check that all of its arguments are defined.
456 1486466 : if (term.function().arity() > 0)
457 : {
458 803595 : const _term_appl& ta = static_cast<const _term_appl&>(term);
459 803595 : assert(ta.function().defined());
460 2260642 : for (std::size_t i = 0; i < ta.function().arity(); ++i)
461 : {
462 1457047 : assert(ta.arg(i).defined());
463 1457047 : assert(&ta!=detail::address(ta.arg(i)));
464 1457047 : verify_term<DynamicNumberOfArguments>(*detail::address(ta.arg(i)));
465 : }
466 : }
467 1486466 : return true;
468 : }
469 :
470 : #undef ATERM_POOL_STORAGE_TEMPLATES
471 : #undef ATERM_POOL_STORAGE
472 :
473 : } // namespace detail
474 : } // namespace atermpp
475 :
476 : #endif
|
