LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/rewrite - jittycpreamble.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 48 126 38.1 %
Date: 2020-02-28 00:44:21 Functions: 10 16 62.5 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Muck van Weerdenburg
       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/detail/rewrite/jittycpreamble.h
      10             : 
      11             : #ifndef __REWR_JITTYC_PREAMBLE_H
      12             : #define __REWR_JITTYC_PREAMBLE_H
      13             : 
      14             : #include "mcrl2/utilities/toolset_version_const.h"
      15             : #include "mcrl2/data/detail/rewrite/jitty_jittyc.h"
      16             : #include "mcrl2/data/detail/rewrite/jittyc.h"
      17             : 
      18             : using namespace mcrl2::data::detail;
      19             : using namespace mcrl2::data;
      20             : using atermpp::down_cast;
      21             : 
      22             : //
      23             : // Declaration of rewriter library interface
      24             : //
      25             : #ifdef _MSC_VER
      26             : #define DLLEXPORT __declspec(dllexport)
      27             : #else
      28             : #define DLLEXPORT
      29             : #endif // _MSC_VER
      30             : 
      31             : extern "C" {
      32             :   DLLEXPORT bool init(rewriter_interface* i, RewriterCompilingJitty* this_rewriter);
      33             : }
      34             : 
      35             : // A rewrite_term is a term that may or may not be in normal form. If the method"
      36             : // normal_form is invoked, it will calculate a normal form for itself as efficiently as possible."
      37             : template <class REWRITE_TERM>
      38             : static data_expression local_rewrite(const REWRITE_TERM& t)
      39             : {
      40             :   return t.normal_form();
      41             : }
      42             : 
      43           0 : static const data_expression& local_rewrite(const data_expression& t)
      44             : {
      45           0 :   return t;
      46             : } 
      47             : 
      48             : //
      49             : // Forward declarations
      50             : //
      51             : static void set_the_precompiled_rewrite_functions_in_a_lookup_table(RewriterCompilingJitty* this_rewriter);
      52             : static data_expression rewrite_aux(const data_expression& t, const bool arguments_in_normal_form, RewriterCompilingJitty* this_rewriter);
      53             : static inline data_expression rewrite_abstraction_aux(const abstraction& a, const data_expression& t, RewriterCompilingJitty* this_rewriter);
      54           0 : static data_expression rewrite_with_arguments_in_normal_form(const data_expression& t, RewriterCompilingJitty* this_rewriter)
      55             : {
      56           0 :   return rewrite_aux(t,true, this_rewriter);
      57             : }
      58        5354 : static data_expression rewrite(const data_expression& t, RewriterCompilingJitty* this_rewriter)
      59             : {
      60        5354 :   return rewrite_aux(t, false, this_rewriter);
      61             : }
      62             : 
      63             : //
      64             : // Type definitions
      65             : //
      66             : typedef data_expression (*rewriter_function)(const application&, RewriterCompilingJitty*);
      67             : 
      68             : // A class that contains terms which are explicitly tagged to be
      69             : // not in normal form. By invoking normal_form the normalform
      70             : // of this term is calculated.
      71             : class term_not_in_normal_form
      72             : {
      73             :   protected:
      74             :     const data_expression& m_term;
      75             :     RewriterCompilingJitty* this_rewriter;
      76             : 
      77             :   public:
      78       13062 :     term_not_in_normal_form(const data_expression& term, RewriterCompilingJitty* tr)
      79       13062 :        : m_term(term), this_rewriter(tr)
      80       13062 :     {}
      81             : 
      82       13004 :     data_expression normal_form() const
      83             :     {
      84       13004 :       return rewrite_aux(m_term,false, this_rewriter);
      85             :     }
      86             : };
      87             : 
      88             : // This is an abstraction, of which the arguments are not yet
      89             : // in normal form. This is done when the method "normal_form" is invoked.
      90             : template <class TERM_TO_BE_REWRITTEN>
      91             : class delayed_abstraction
      92             : {
      93             :   protected:
      94             :     const binder_type& m_binding_operator;
      95             :     const variable_list& m_variables;
      96             :     const TERM_TO_BE_REWRITTEN& m_body;
      97             :     RewriterCompilingJitty* this_rewriter;
      98             :   public:
      99             :     delayed_abstraction(const binder_type& binding_operator, 
     100             :                         const variable_list& variables, 
     101             :                         const TERM_TO_BE_REWRITTEN& body,
     102             :                         RewriterCompilingJitty* tr)
     103             :        : m_binding_operator(binding_operator), m_variables(variables), m_body(body), this_rewriter(tr)
     104             :     {}
     105             : 
     106             :     data_expression normal_form() const
     107             :     {
     108             :       const abstraction t(m_binding_operator,m_variables,local_rewrite(m_body));
     109             :       return rewrite_abstraction_aux(t,t,this_rewriter);
     110             :     }
     111             : };
     112             : 
     113             : 
     114             : struct rewrite_functor
     115             : {
     116             :   RewriterCompilingJitty* this_rewriter;
     117             : 
     118           0 :   rewrite_functor(RewriterCompilingJitty* tr)
     119           0 :    : this_rewriter(tr)
     120           0 :   {} 
     121             : 
     122           0 :   data_expression operator()(const data_expression& arg) const
     123             :   {
     124           0 :     return rewrite_aux(arg,false,this_rewriter);
     125             :   }
     126             : };
     127             : 
     128             : 
     129             : // Miscellaneous helper functions
     130             : //
     131             : static inline
     132             : const data_expression& pass_on(const data_expression& t)
     133             : {
     134             :   return t;
     135             : }
     136             : 
     137             : static inline
     138             : assignment_expression_list jittyc_local_push_front(assignment_expression_list l, const assignment& e)
     139             : {
     140             :   l.push_front(e);
     141             :   return l;
     142             : }
     143             : 
     144             : static inline
     145       13028 : std::size_t get_index(const function_symbol& func)
     146             : {
     147       13028 :   return mcrl2::core::index_traits<function_symbol, function_symbol_key_type, 2>::index(func);
     148             : }
     149             : 
     150             : static inline
     151        5330 : RewriterCompilingJitty::substitution_type& sigma(RewriterCompilingJitty* this_rewriter)
     152             : {
     153        5330 :   return *(this_rewriter->global_sigma);
     154             : }
     155             : 
     156             : static inline
     157       24871 : uintptr_t uint_address(const atermpp::aterm& t)
     158             : {
     159       24871 :   return reinterpret_cast<uintptr_t>(atermpp::detail::address(t));
     160             : }
     161             : 
     162             : //
     163             : // Rewriting functions
     164             : //
     165             : 
     166       13028 : static inline rewriter_function get_precompiled_rewrite_function(
     167             :              const function_symbol& f, 
     168             :              const std::size_t arity, 
     169             :              const bool arguments_in_normal_form, 
     170             :              RewriterCompilingJitty* this_rewriter)
     171             : {
     172       13028 :   const std::size_t index = get_index(f);
     173       13028 :   if (index>=this_rewriter->index_bound || arity>=this_rewriter->arity_bound)
     174             :   {
     175           0 :     return NULL;
     176             :   }
     177             : 
     178       13028 :   if (arguments_in_normal_form)
     179             :   {
     180           0 :     assert(this_rewriter -> arity_bound * index + arity<this_rewriter->functions_when_arguments_are_in_normal_form.size());
     181           0 :     return this_rewriter->functions_when_arguments_are_in_normal_form[this_rewriter->arity_bound * index + arity]; 
     182             :   }
     183       13028 :   assert(this_rewriter->arity_bound * index + arity<this_rewriter->functions_when_arguments_are_not_in_normal_form.size());
     184       13028 :   return this_rewriter->functions_when_arguments_are_not_in_normal_form[this_rewriter->arity_bound * index + arity];
     185             : }
     186             : 
     187             : static inline 
     188           0 : data_expression rewrite_abstraction_aux(const abstraction& head, const data_expression& a, RewriterCompilingJitty* this_rewriter)
     189             : {
     190           0 :   const binder_type& binder(head.binding_operator());
     191           0 :   if (is_lambda_binder(binder))
     192             :   {
     193           0 :     const data_expression& result=this_rewriter->rewrite_lambda_application(a, sigma(this_rewriter));
     194           0 :     assert(result.sort()==a.sort());
     195           0 :     return result;
     196             :   }
     197           0 :   if (is_exists_binder(binder))
     198             :   {
     199           0 :     const data_expression& result=this_rewriter->existential_quantifier_enumeration(a, sigma(this_rewriter));
     200           0 :     assert(result.sort()==a.sort());
     201           0 :     return result;
     202             :   }
     203           0 :   assert(is_forall_binder(binder));
     204           0 :   const data_expression& result=this_rewriter->universal_quantifier_enumeration(a, sigma(this_rewriter));
     205           0 :   assert(result.sort()==a.sort());
     206           0 :   return result;
     207             : }
     208             : 
     209             : 
     210             : static inline
     211           0 : data_expression rewrite_appl_aux(const application& t, RewriterCompilingJitty* this_rewriter)
     212             : {
     213           0 :   const data_expression& thead=get_nested_head(t);
     214           0 :   if (is_function_symbol(thead))
     215             :   {
     216           0 :     const std::size_t arity=recursive_number_of_args(t);
     217           0 :     const rewriter_function f = get_precompiled_rewrite_function(atermpp::down_cast<function_symbol>(thead),arity,false,this_rewriter);
     218           0 :     if (f != NULL)
     219             :     {
     220           0 :       const data_expression& result=f(t,this_rewriter);
     221           0 :       assert(t.sort()==result.sort());
     222           0 :       return result;
     223             :     }
     224           0 :     return application(rewrite_aux(t.head(),false,this_rewriter), t.begin(), t.end(), rewrite_functor(this_rewriter));
     225             :   }
     226             :   // Here the head symbol of, which can be deeply nested, is not a function_symbol.
     227           0 :   const data_expression& head0 = get_nested_head(t);
     228           0 :   const data_expression head = (is_variable(head0)
     229           0 :                              ? sigma(this_rewriter)(down_cast<const variable>(head0))
     230           0 :                              : (is_where_clause(head0)
     231           0 :                                ? this_rewriter->rewrite_where(atermpp::down_cast<where_clause>(head0), sigma(this_rewriter))
     232           0 :                                : head0));
     233             : 
     234             :   // Reconstruct term t.
     235           0 :   const application t1((head0 == head) ? t : replace_nested_head(t, head));
     236             : 
     237           0 :   const data_expression head1(get_nested_head(t1));
     238             :   // Here head1 has the shape
     239             :   // variable, function_symbol, lambda y1,....,ym.u, forall y1,....,ym.u or exists y1,....,ym.u,
     240           0 :   if (is_variable(head1))
     241             :   {
     242           0 :     return rewrite_all_arguments(t1, rewrite_functor(this_rewriter));
     243             :   }
     244             :   else
     245           0 :   if (is_abstraction(head1))
     246             :   {
     247           0 :     return rewrite_abstraction_aux(head1,t1,this_rewriter);
     248             :   }
     249             :   else
     250             :   {
     251           0 :     assert(is_function_symbol(head1));
     252           0 :     const std::size_t arity = recursive_number_of_args(t1);
     253           0 :     const rewriter_function f = get_precompiled_rewrite_function(down_cast<function_symbol>(head1),arity,false,this_rewriter);
     254           0 :     if (f != NULL)
     255             :     {
     256           0 :       const data_expression& result=f(t1,this_rewriter);
     257           0 :       assert(t1.sort()==result.sort());
     258           0 :       return result;
     259             :     }
     260           0 :     return application(rewrite_aux(head1,false,this_rewriter), t1.begin(), t1.end(), rewrite_functor(this_rewriter)); 
     261             :   }
     262             : }
     263             : 
     264             : static inline
     265       18358 : data_expression rewrite_aux(const data_expression& t, const bool arguments_in_normal_form, RewriterCompilingJitty* this_rewriter)
     266             : {
     267       18358 :   if (is_function_symbol(t))
     268             :   {
     269        4632 :     const std::size_t arity=0;
     270        4632 :     const rewriter_function f = get_precompiled_rewrite_function(down_cast<function_symbol>(t), arity, false,this_rewriter);
     271        4632 :     if (f != NULL)
     272             :     {
     273        9264 :       const data_expression& result=f(application(),this_rewriter); // The argument is not used.
     274        4632 :       assert(result.sort()==t.sort());
     275        4632 :       return result;
     276             :     }
     277           0 :     return t;
     278             :   }
     279             :   else
     280       13726 :   if (is_application_no_check(t))
     281             :   {
     282        8396 :     const application& appl = down_cast<application>(t);
     283        8396 :     const data_expression& head = appl.head();
     284        8396 :     if (is_function_symbol(head))
     285             :     {
     286        8396 :       const std::size_t appl_size=appl.size();
     287        8396 :       const rewriter_function f = get_precompiled_rewrite_function(down_cast<function_symbol>(head), appl_size, arguments_in_normal_form,this_rewriter);
     288        8396 :       if (f != NULL)
     289             :       {
     290       16792 :         const data_expression& result= f(appl,this_rewriter);
     291        8396 :         assert(result.sort()==t.sort());
     292        8396 :         return result;
     293             :       }
     294           0 :       return application(rewrite_aux(appl.head(),false, this_rewriter), appl.begin(), appl.end(), rewrite_functor(this_rewriter));
     295             :     }
     296             :     else
     297             :     {
     298           0 :       const data_expression& result=rewrite_appl_aux(appl,this_rewriter);
     299           0 :       assert(result.sort()==appl.sort());
     300           0 :       return result;
     301             :     }
     302             :   }
     303             :   else
     304        5330 :   if (is_variable(t))
     305             :   {
     306        5330 :     return sigma(this_rewriter)(down_cast<variable>(t));
     307             :   }
     308             :   else
     309           0 :   if (is_abstraction(t))
     310             :   {
     311           0 :     const abstraction& abstr(t);
     312           0 :     const binder_type& binder(abstr.binding_operator());
     313           0 :     if (is_exists_binder(binder))
     314             :     {
     315           0 :       const data_expression& result=this_rewriter->existential_quantifier_enumeration(t, sigma(this_rewriter));
     316           0 :       assert(result.sort()==t.sort());
     317           0 :       return result;
     318             :     }
     319           0 :     if (is_forall_binder(binder))
     320             :     {
     321           0 :       const data_expression& result=this_rewriter->universal_quantifier_enumeration(t, sigma(this_rewriter));
     322           0 :       assert(result.sort()==t.sort());
     323           0 :       return result;
     324             :     }
     325           0 :     assert(is_lambda_binder(binder));
     326           0 :     return this_rewriter->rewrite_single_lambda(abstr.variables(), abstr.body(), false, sigma(this_rewriter));
     327             :   }
     328             :   else
     329             :   {
     330           0 :     assert(is_where_clause(t));
     331           0 :     return this_rewriter->rewrite_where(down_cast<where_clause>(t), sigma(this_rewriter));
     332             :   }
     333             : }
     334             : 
     335             : static
     336           4 : void rewrite_cleanup()
     337             : {
     338           4 : }
     339             : 
     340           4 : bool init(rewriter_interface* i, RewriterCompilingJitty* this_rewriter)
     341             : {
     342             : #ifndef MCRL2_DISABLE_JITTYC_VERSION_CHECK
     343           4 :   if (mcrl2::utilities::MCRL2_VERSION != i->caller_toolset_version)
     344             :   {
     345           0 :     i->status = "rewriter version does not match the version of the calling application.";
     346           0 :     return false;
     347             :   }
     348             : #endif
     349           4 :   i->rewrite_external = &rewrite;
     350           4 :   i->rewrite_cleanup = &rewrite_cleanup;
     351             :   // this_rewriter = i->rewriter;
     352           4 :   set_the_precompiled_rewrite_functions_in_a_lookup_table(this_rewriter);
     353           4 :   i->status = "rewriter loaded successfully.";
     354           4 :   return true;
     355             : }
     356             : 
     357             : #endif // __REWR_JITTYC_PREAMBLE_H

Generated by: LCOV version 1.13