LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - sort_type_checker.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 144 150 96.0 %
Date: 2024-03-08 02:52:28 Functions: 10 10 100.0 %
Legend: Lines: hit not hit

          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

Generated by: LCOV version 1.14