LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/rewrite - jittyc.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 14 18 77.8 %
Date: 2020-02-28 00:44:21 Functions: 5 7 71.4 %
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/jittyc.h
      10             : 
      11             : #ifndef __REWR_JITTYC_H
      12             : #define __REWR_JITTYC_H
      13             : 
      14             : #include "mcrl2/data/detail/rewrite/jitty.h"
      15             : #include "mcrl2/data/detail/rewrite/match_tree.h"
      16             : #include "mcrl2/utilities/uncompiledlibrary.h"
      17             : #include "mcrl2/utilities/toolset_version.h"
      18             : #include "mcrl2/data/detail/rewrite/nfs_array.h"
      19             : 
      20             : #ifdef MCRL2_JITTYC_AVAILABLE
      21             : 
      22             : #include <utility>
      23             : #include <string>
      24             : 
      25             : namespace mcrl2
      26             : {
      27             : namespace data
      28             : {
      29             : namespace detail
      30             : {
      31             : 
      32             : typedef std::vector < sort_expression_list> sort_list_vector;
      33             : 
      34             : ///
      35             : /// \brief The normal_form_cache class stores normal forms of data_expressions that
      36             : ///        are inserted in it. By keeping the cache on the stack, the normal forms
      37             : ///        in it will not be freed by the ATerm library, and can therefore be used
      38             : ///        in the generated jittyc code.
      39             : ///
      40           4 : class normal_form_cache
      41             : {
      42             :   private:
      43             :     RewriterJitty& m_rewriter;
      44             :     std::set<data_expression> m_lookup;
      45             :   public:
      46           4 :     normal_form_cache(RewriterJitty& rewriter)
      47           4 :       : m_rewriter(rewriter)
      48             :     { 
      49           4 :     }
      50             :   
      51             :   ///
      52             :   /// \brief insert stores the normal form of t in the cache, and returns a string
      53             :   ///        that is a C++ representation of the stored normal form. This string can
      54             :   ///        be used by the generated rewriter as long as the cache object is alive,
      55             :   ///        and its clear() method has not been called.
      56             :   /// \param t The term to normalize.
      57             :   /// \return A C++ string that evaluates to the cached normal form of t.
      58             :   ///
      59         663 :   std::string insert(const data_expression& t)
      60             :   {
      61        1326 :     std::stringstream ss;
      62        1326 :     RewriterJitty::substitution_type sigma;
      63         663 :     auto pair = m_lookup.insert(m_rewriter(t, sigma));
      64         663 :     ss << "*reinterpret_cast<const data_expression*>(" << (void*)&(*pair.first) << ")";
      65        1326 :     return ss.str();
      66             :   }
      67             : 
      68             :   ///
      69             :   /// \brief clear clears the cache. This operation invalidates all the C++ strings
      70             :   ///        obtained via the insert() method.
      71             :   ///
      72           8 :   void clear()
      73             :   {
      74           8 :     m_lookup.clear();
      75           8 :   }
      76             : };
      77             : 
      78             : class RewriterCompilingJitty: public Rewriter
      79             : {
      80             :   public:
      81             :     typedef Rewriter::substitution_type substitution_type;
      82             :     typedef data_expression (*rewriter_function)(const application&, RewriterCompilingJitty*);
      83             : 
      84             :     RewriterCompilingJitty(const data_specification& DataSpec, const used_data_equation_selector &);
      85             :     virtual ~RewriterCompilingJitty();
      86             : 
      87             :     rewrite_strategy getStrategy();
      88             : 
      89             :     data_expression rewrite(const data_expression& term, substitution_type& sigma);
      90             : 
      91             :     // The variable global_sigma is a temporary store to maintain the substitution 
      92             :     // sigma during rewriting a single term. It is not a variable for public use. 
      93             :     substitution_type *global_sigma;
      94             :     // The data structures below are used to store the variable lists2
      95             :     // that are used in the compiling rewriter in forall, where and exists.
      96             :     std::vector<variable_list> rewriter_binding_variable_lists;
      97             :     std::map <variable_list, std::size_t> variable_list_indices1;
      98             :     std::size_t binding_variable_list_index(const variable_list& v);
      99           0 :     inline variable_list binding_variable_list_get(const std::size_t i)
     100             :     {
     101           0 :       return (rewriter_binding_variable_lists[i]);
     102             :     }
     103             : 
     104             :     // The data structures below are used to store single variables
     105             :     // that are bound in lambda, forall and exist operators. When required
     106             :     // in the compiled required, these variables can be retrieved from
     107             :     // the array rewriter_bound_variables. variable_indices0 is used
     108             :     // to prevent double occurrences in the vector.
     109             :     std::vector<variable> rewriter_bound_variables;
     110             :     std::map <variable, std::size_t> variable_indices0;
     111             :    
     112             :     // The following values are used to locate rewrite functions in the tables of
     113             :     // precompiled functions. 
     114             :     //   arity_bound -- The maximum occurring arity + 1
     115             :     //   index_bound -- The maximum occurring index + 1
     116             :     std::size_t arity_bound;
     117             :     std::size_t index_bound;
     118             : 
     119             :     std::size_t bound_variable_index(const variable& v);
     120           0 :     variable bound_variable_get(const std::size_t i)
     121             :     {
     122           0 :       return (rewriter_bound_variables[i]);
     123             :     }
     124             : 
     125             :     // The two arrays below are intended to contain the precompiled functions used
     126             :     // for rewriting. They are used to find the relevant compiled rewriting code quickly. 
     127             :     std::vector<rewriter_function> functions_when_arguments_are_not_in_normal_form;
     128             :     std::vector<rewriter_function> functions_when_arguments_are_in_normal_form;
     129             : 
     130             :     // Standard assignment operator.
     131             :     RewriterCompilingJitty& operator=(const RewriterCompilingJitty& other)=delete;
     132             : 
     133             :   private:
     134             :     class ImplementTree;
     135             :     friend class ImplementTree;
     136             :     
     137             :     RewriterJitty jitty_rewriter;
     138             :     std::set < data_equation > rewrite_rules;
     139             :     bool made_files;
     140             :     std::map<function_symbol, data_equation_list> jittyc_eqns;
     141             :     std::set<function_symbol> m_extra_symbols;
     142             : 
     143             :     std::shared_ptr<uncompiled_library> rewriter_so;
     144             :     normal_form_cache m_nf_cache;
     145             : 
     146             :     void (*so_rewr_cleanup)();
     147             :     data_expression(*so_rewr)(const data_expression&, RewriterCompilingJitty*);
     148             : 
     149             :     void add_base_nfs(nfs_array& a, const function_symbol& opid, std::size_t arity);
     150             :     void extend_nfs(nfs_array& a, const function_symbol& opid, std::size_t arity);
     151             :     bool opid_is_nf(const function_symbol& opid, std::size_t num_args);
     152             :     void calc_nfs_list(nfs_array& a, const application& args, variable_or_number_list nnfvars);
     153             :     bool calc_nfs(const data_expression& t, variable_or_number_list nnfvars);
     154             :     void CleanupRewriteSystem();
     155             :     void BuildRewriteSystem();
     156             :     void generate_code(const std::string& filename);
     157             :     void generate_rewr_functions(std::ostream& s, const data::function_symbol& func, const data_equation_list& eqs);
     158             :     bool lift_rewrite_rule_to_right_arity(data_equation& e, const std::size_t requested_arity);
     159             :     sort_list_vector get_residual_sorts(const sort_expression& s, const std::size_t actual_arity, const std::size_t requested_arity);
     160             :     match_tree_list create_strategy(const data_equation_list& rules, const std::size_t arity);
     161             : 
     162             : };
     163             : 
     164           4 : struct rewriter_interface
     165             : {
     166             :   std::string caller_toolset_version;
     167             :   std::string status;
     168             :   RewriterCompilingJitty* rewriter;
     169             :   data_expression (*rewrite_external)(const data_expression& t, RewriterCompilingJitty*);
     170             :   void (*rewrite_cleanup)();
     171             : };
     172             : 
     173             : }
     174             : }
     175             : }
     176             : 
     177             : #endif // MCRL2_JITTYC_AVAILABLE
     178             : 
     179             : #endif // __REWR_JITTYC_H

Generated by: LCOV version 1.13