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 MCRL2_DATA_DETAIL_REWR_JITTYC_H
      12             : #define MCRL2_DATA_DETAIL_REWR_JITTYC_H
      13             : 
      14             : #include <utility>
      15             : #include <string>
      16             : 
      17             : #include "mcrl2/utilities/uncompiledlibrary.h"
      18             : #include "mcrl2/utilities/toolset_version.h"
      19             : #include "mcrl2/atermpp/standard_containers/vector.h"
      20             : #include "mcrl2/data/detail/rewrite/jitty.h"
      21             : #include "mcrl2/data/detail/rewrite/match_tree.h"
      22             : #include "mcrl2/data/detail/rewrite/nfs_array.h"
      23             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      24             : 
      25             : #ifdef MCRL2_ENABLE_JITTYC
      26             : 
      27             : namespace mcrl2
      28             : {
      29             : namespace data
      30             : {
      31             : namespace detail
      32             : {
      33             : 
      34             : typedef std::vector < sort_expression_list> sort_list_vector;
      35             : 
      36             : ///
      37             : /// \brief The normal_form_cache class stores normal forms of data_expressions that
      38             : ///        are inserted in it. By keeping the cache on the stack, the normal forms
      39             : ///        in it will not be freed by the ATerm library, and can therefore be used
      40             : ///        in the generated jittyc code.
      41             : ///
      42             : class normal_form_cache
      43             : {
      44             :   private:
      45             :     std::set<data_expression> m_lookup;
      46             :   public:
      47           5 :     normal_form_cache()
      48           5 :     { 
      49           5 :     }
      50             : 
      51             :   // Caches cannot be copied or moved. The addresses in the cache must remain available the lifetime of 
      52             :   // all rewriters using this cache. 
      53             :     normal_form_cache(const normal_form_cache& ) = delete;
      54             :     normal_form_cache(normal_form_cache&& ) = delete;
      55             :     normal_form_cache& operator=(const normal_form_cache& ) = delete;
      56             :     normal_form_cache& operator=(normal_form_cache&& ) = delete;
      57             :   
      58             :   /// \brief insert stores the normal form of t in the cache, and returns a string
      59             :   ///        that is a C++ representation of the stored normal form. This string can
      60             :   ///        be used by the generated rewriter as long as the cache object is alive,
      61             :   ///        and its clear() method has not been called.
      62             :   /// \param t The term to normalize.
      63             :   /// \return A C++ string that evaluates to the cached normal form of t.
      64             :   ///
      65         926 :   std::string insert(const data_expression& t)
      66             :   {
      67         926 :     std::stringstream ss;
      68         926 :     const data_expression* cached_term = &*(m_lookup.insert(t).first);
      69         926 :     ss << "*reinterpret_cast<const data_expression*>(" << (void*)(cached_term) << ")";
      70        1852 :     return ss.str();
      71         926 :   }
      72             : 
      73             :   /// \brief Checks whether the cache is empty.
      74             :   /// \return A boolean indicating whether the cache is empty. 
      75           5 :   bool empty() const
      76             :   {
      77           5 :     return m_lookup.empty();
      78             :   }
      79             : 
      80           5 :   ~normal_form_cache()
      81             :   {
      82           5 :   }
      83             : };
      84             : 
      85             : class RewriterCompilingJitty: public Rewriter
      86             : {
      87             :   public:
      88             :     typedef Rewriter::substitution_type substitution_type;
      89             :     typedef void (*rewriter_function)(data_expression&, const application&, RewriterCompilingJitty*);
      90             : 
      91             :     RewriterCompilingJitty(const data_specification& DataSpec, const used_data_equation_selector&);
      92             :     virtual ~RewriterCompilingJitty();
      93             : 
      94             :     rewrite_strategy getStrategy();
      95             : 
      96             :     data_expression rewrite(const data_expression& term, substitution_type& sigma);
      97             : 
      98             :     void rewrite(data_expression& result, const data_expression& term, substitution_type& sigma);
      99             : 
     100             :     // The variable global_sigma is a temporary store to maintain the substitution 
     101             :     // sigma during rewriting a single term. It is not a variable for public use. 
     102             :     substitution_type *global_sigma;
     103             :     bool rewriting_in_progress;
     104             :     rewrite_stack m_rewrite_stack;
     105             : 
     106             :     // The data structures below are used to store the variable lists2
     107             :     // that are used in the compiling rewriter in forall, where and exists.
     108             :     std::vector<variable_list> rewriter_binding_variable_lists;
     109             :     std::map <variable_list, std::size_t> variable_list_indices1;
     110             :     std::size_t binding_variable_list_index(const variable_list& v);
     111           0 :     inline variable_list binding_variable_list_get(const std::size_t i)
     112             :     {
     113           0 :       return (rewriter_binding_variable_lists[i]);
     114             :     }
     115             : 
     116             :     // The data structures below are used to store single variables
     117             :     // that are bound in lambda, forall and exist operators. When required
     118             :     // in the compiled required, these variables can be retrieved from
     119             :     // the array rewriter_bound_variables. variable_indices0 is used
     120             :     // to prevent double occurrences in the vector.
     121             :     std::vector<variable> rewriter_bound_variables;
     122             :     std::map <variable, std::size_t> variable_indices0;
     123             :    
     124             :     // The following values are used to locate rewrite functions in the tables of
     125             :     // precompiled functions. 
     126             :     //   arity_bound -- The maximum occurring arity + 1
     127             :     //   index_bound -- The maximum occurring index + 1
     128             :     std::size_t arity_bound;
     129             :     std::size_t index_bound;
     130             : 
     131             :     std::size_t bound_variable_index(const variable& v);
     132           0 :     variable bound_variable_get(const std::size_t i)
     133             :     {
     134           0 :       return (rewriter_bound_variables[i]);
     135             :     }
     136             : 
     137             :     // The two arrays below are intended to contain the precompiled functions used
     138             :     // for rewriting. They are used to find the relevant compiled rewriting code quickly. 
     139             :     std::vector<rewriter_function> functions_when_arguments_are_not_in_normal_form;
     140             :     std::vector<rewriter_function> functions_when_arguments_are_in_normal_form;
     141             :  
     142             :     // The following vector is to store normal forms of constants, indexed by the sequence number in a constant. 
     143             :     std::vector<data_expression> normal_forms_for_constants;
     144             : 
     145             :     // Standard assignment operator.
     146             :     RewriterCompilingJitty& operator=(const RewriterCompilingJitty& other)=delete;
     147             : 
     148           0 :     std::shared_ptr<detail::Rewriter> clone()
     149             :     {
     150           0 :       return std::shared_ptr<Rewriter>(new RewriterCompilingJitty(*this));
     151             :     }
     152             : 
     153             :   protected:
     154             :     class ImplementTree;
     155             :     friend class ImplementTree;
     156             :     
     157             :     RewriterJitty jitty_rewriter;
     158             :     std::set < data_equation > rewrite_rules;
     159             :     const match_tree dummy=match_tree();
     160             :     bool made_files;
     161             :     std::map<function_symbol, data_equation_list> jittyc_eqns;
     162             :     std::set<function_symbol> m_extra_symbols;
     163             : 
     164             :     std::shared_ptr<uncompiled_library> rewriter_so;
     165             :     std::shared_ptr<normal_form_cache> m_nf_cache;
     166             : 
     167             :     // The rewriter maintains a copy of busy and forbidden flag,
     168             :     // to allow for faster access to them. These flags are used extensively and
     169             :     // in clang version 2021 access to them via the compiler, using tlv_get_access,
     170             :     // is relatively slow. It is expected that in some future version of the compiler
     171             :     // such access is faster, and no copy of these flags is needed anymore. 
     172             :   public:
     173             :     atermpp::detail::thread_aterm_pool* m_thread_aterm_pool;
     174             : 
     175             :   protected:
     176             :     // Copy construction. Not (yet) for public use.
     177           0 :     RewriterCompilingJitty(RewriterCompilingJitty& other) = default;
     178             : 
     179             :     void (*so_rewr_cleanup)();
     180             :     void (*so_rewr)(data_expression& result, const data_expression&, RewriterCompilingJitty*);
     181             : 
     182             :     void add_base_nfs(nfs_array& a, const function_symbol& opid, std::size_t arity);
     183             :     void extend_nfs(nfs_array& a, const function_symbol& opid, std::size_t arity);
     184             :     bool opid_is_nf(const function_symbol& opid, std::size_t num_args);
     185             :     void calc_nfs_list(nfs_array& a, const application& args, variable_or_number_list nnfvars);
     186             :     bool calc_nfs(const data_expression& t, variable_or_number_list nnfvars);
     187             :     void CleanupRewriteSystem();
     188             :     void BuildRewriteSystem();
     189             :     void generate_code(const std::string& filename);
     190             :     void generate_rewr_functions(std::ostream& s, const data::function_symbol& func, const data_equation_list& eqs);
     191             :     bool lift_rewrite_rule_to_right_arity(data_equation& e, const std::size_t requested_arity);
     192             :     sort_list_vector get_residual_sorts(const sort_expression& s, const std::size_t actual_arity, const std::size_t requested_arity);
     193             :     match_tree_list create_strategy(const data_equation_list& rules, const std::size_t arity);
     194             :     void term2seq(const data_expression& t, match_tree_list& s, std::size_t *var_cnt, const bool omit_head);
     195             :     match_tree_list create_sequence(const data_equation& rule, std::size_t* var_cnt);
     196             :     match_tree_list subst_var(const match_tree_list& l,
     197             :                                  const variable& old,
     198             :                                  const variable& new_val,
     199             :                                  const std::size_t num,
     200             :                                  const mutable_map_substitution<>& substs);
     201             :     match_tree build_tree(build_pars pars, std::size_t i);
     202             :     match_tree create_tree(const data_equation_list& rules);
     203             : 
     204           5 :   void thread_initialise()
     205             :   {
     206           5 :     mCRL2log(mcrl2::log::debug) << "Initialise busy/forbidden flags\n";
     207           5 :     m_thread_aterm_pool = &atermpp::detail::g_thread_term_pool();
     208           5 :   }
     209             : };
     210             : 
     211             : struct rewriter_interface
     212             : {
     213             :   std::string caller_toolset_version;
     214             :   std::string status;
     215             :   RewriterCompilingJitty* rewriter;
     216             :   void (*rewrite_external)(data_expression& result, const data_expression& t, RewriterCompilingJitty*);
     217             :   void (*rewrite_cleanup)();
     218             : };
     219             : 
     220             : }
     221             : }
     222             : }
     223             : 
     224             : #endif // MCRL2_ENABLE_JITTYC
     225             : 
     226             : #endif // MCRL2_DATA_DETAIL_REWR_JITTYC_H