Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/core/dparser.cpp
      10             : /// \brief add your file description here.
      11             : 
      12             : #include <d.h>
      13             : #include "mcrl2/core/detail/dparser_functions.h"
      14             : #include "mcrl2/utilities/logger.h"
      15             : #include <iomanip>
      16             : #include <locale>
      17             : 
      18             : extern "C"
      19             : {
      20             :   extern D_ParserTables parser_tables_mcrl2;
      21             : }
      22             : 
      23             : namespace mcrl2 {
      24             : 
      25             : namespace core {
      26             : 
      27           4 : std::string parse_node::add_context(const std::string& message) const
      28             : {
      29           4 :   return detail::add_context(&node->start_loc, message);
      30             : }
      31             : 
      32      713001 : int parse_node::symbol() const
      33             : {
      34      713001 :   return node->symbol;
      35             : }
      36             : 
      37      722837 : int parse_node::child_count() const
      38             : {
      39      722837 :   return d_get_number_of_children(node);
      40             : }
      41             : 
      42             : // 0 <= i < child_count()
      43      564335 : parse_node parse_node::child(int i) const
      44             : {
      45      564335 :   return parse_node(d_get_child(node, i));
      46             : }
      47             : 
      48           0 : parse_node parse_node::find_in_tree(int symbol) const
      49             : {
      50           0 :   return parse_node(d_find_in_tree(node, symbol));
      51             : }
      52             : 
      53       99833 : std::string parse_node::string() const
      54             : {
      55       99833 :   return std::string(node->start_loc.s, node->end - node->start_loc.s);
      56             : }
      57             : 
      58           0 : std::string parse_node::tree() const
      59             : {
      60           0 :   if (child_count() < 2)
      61           0 :     return this->string();
      62           0 :   std::stringstream result;
      63           0 :   result << "(" << child(0).tree();
      64           0 :   for (int i = 1; i < child_count(); ++i)
      65           0 :     result << " " << child(i).tree();
      66           0 :   result << ")";
      67           0 :   return result.str();
      68           0 : }
      69             : 
      70           0 : int parse_node::column() const
      71             : {
      72           0 :   return node->start_loc.col;
      73             : }
      74             : 
      75           0 : int parse_node::line() const
      76             : {
      77           0 :   return node->start_loc.line;
      78             : }
      79             : 
      80           0 : std::string parse_node::pathname() const
      81             : {
      82           0 :   return std::string(node->start_loc.pathname);
      83             : }
      84             : 
      85      567489 : parse_node::~parse_node()
      86             : {
      87      567489 :   if (parser)
      88             :   {
      89        3153 :     free_D_ParseNode(parser, node);
      90             :   }
      91      567489 : }
      92             : 
      93             : // Prints a tree of
      94           0 : std::string parser_table::tree(const core::parse_node& node) const
      95             : {
      96           0 :   std::stringstream result;
      97           0 :   result << symbol_name(node) << "(";
      98           0 :   if (node.child_count() == 0)
      99           0 :     result << '"' << node.string() << '"';
     100             :   else
     101           0 :     result << tree(node.child(0));
     102           0 :   for (int i = 1; i < node.child_count(); ++i)
     103           0 :     result << " " << tree(node.child(i));
     104           0 :   result << ")";
     105           0 :   return result.str();
     106           0 : }
     107             : 
     108             : // Returns the number of symbols in the table
     109      301047 : unsigned int parser_table::symbol_count() const
     110             : {
     111      301047 :   return m_table.nsymbols;
     112             : }
     113             : 
     114             : // Returns the name of the i-th symbol
     115      834251 : std::string parser_table::symbol_name(unsigned int i) const
     116             : {
     117      834251 :   if (i >= m_table.nsymbols)
     118             :   {
     119           0 :     print();
     120           0 :     std::ostringstream out;
     121           0 :     out << "parser_table::symbol_name: index " << i << " out of bounds!";
     122           0 :     throw std::runtime_error(out.str());
     123           0 :   }
     124      834251 :   const char* name = m_table.symbols[i].name;
     125      834251 :   if (!name)
     126             :   {
     127           0 :     return "";
     128             :   }
     129      834251 :   return std::string(name);
     130             : }
     131             : 
     132       99827 : std::string parser_table::symbol_name(const parse_node& node) const
     133             : {
     134       99827 :   return symbol_name(node.symbol());
     135             : }
     136             : 
     137             : // Returns the 'start symbol' of the i-th symbol
     138        3154 : int parser_table::start_symbol(unsigned int i) const
     139             : {
     140        3154 :   return m_table.symbols[i].start_symbol;
     141             : }
     142             : 
     143             : // Returns true if the i-th symbol is of type D_SYMBOL_NTERM
     144      301047 : bool parser_table::is_term_symbol(unsigned int i) const
     145             : {
     146      301047 :   return m_table.symbols[i].kind == D_SYMBOL_NTERM;
     147             : }
     148             : 
     149        3154 : unsigned int parser_table::start_symbol_index(const std::string& name) const
     150             : {
     151      301047 :   for (unsigned int i = 0; i < symbol_count(); i++)
     152             :   {
     153      301047 :     if (is_term_symbol(i) && symbol_name(i) == name)
     154             :     {
     155        3154 :       return start_symbol(i);
     156             :     }
     157             :   }
     158           0 :   throw mcrl2::runtime_error("unknown start symbol '" + name + "'");
     159             :   return 0;
     160             : }
     161             : 
     162           0 : void parser_table::print() const
     163             : {
     164           0 :   std::clog << "--------------------" << std::endl;
     165           0 :   std::clog << "-   symbol table   -" << std::endl;
     166           0 :   std::clog << "--------------------" << std::endl;
     167           0 :   for (unsigned int i = 0; i < symbol_count(); i++)
     168             :   {
     169           0 :     std::clog << std::setw(3) << i << " " << symbol_name(i) << std::endl;
     170             :   }
     171           0 :   std::clog << "--------------------" << std::endl;
     172           0 : }
     173             : 
     174        3154 : parser::parser(D_ParserTables& tables, D_AmbiguityFn ambiguity_fn, D_SyntaxErrorFn syntax_error_fn, std::size_t max_error_message_count)
     175        3154 :   : m_table(tables)
     176             : {
     177        3154 :   detail::set_dparser_max_error_message_count(max_error_message_count);
     178        3154 :   m_parser = new_D_Parser(&tables, 0);
     179        3154 :   m_parser->initial_globals = this;
     180        3154 :   m_parser->save_parse_tree = 1;
     181        3154 :   m_parser->initial_scope = nullptr;
     182        3154 :   m_parser->dont_use_greediness_for_disambiguation = 1;
     183        3154 :   m_parser->dont_use_height_for_disambiguation = 1;
     184        3154 :   if (ambiguity_fn)
     185             :   {
     186        3150 :     m_parser->ambiguity_fn = ambiguity_fn;
     187             :   }
     188        3154 :   if (syntax_error_fn)
     189             :   {
     190        3150 :     m_parser->syntax_error_fn = syntax_error_fn;
     191             :   }
     192        3154 : }
     193             : 
     194        3154 : parser::~parser()
     195             : {
     196        3154 :   free_D_Parser(m_parser);
     197        3154 : }
     198             : 
     199      636692 : const parser_table& parser::symbol_table() const
     200             : {
     201      636692 :   return m_table;
     202             : }
     203             : 
     204        3154 : unsigned int parser::start_symbol_index(const std::string& name) const
     205             : {
     206        3154 :   return m_table.start_symbol_index(name);
     207             : }
     208             : 
     209        3154 : parse_node parser::parse(const std::string& text, unsigned int start_symbol_index, bool partial_parses)
     210             : {
     211        3154 :   detail::reset_dparser_error_message_count();
     212        3154 :   m_parser->start_state = start_symbol_index;
     213        3154 :   m_parser->partial_parses = partial_parses ? 1 : 0;
     214        3154 :   D_ParseNode* result = dparse(m_parser, const_cast<char*>(text.c_str()), static_cast<int>(text.size()));
     215        3154 :   if (!result || m_parser->syntax_errors)
     216             :   {    
     217           1 :     if (result != nullptr) {
     218           1 :       free_D_ParseNode(m_parser, result);
     219             :     }
     220           1 :     throw mcrl2::runtime_error("syntax error");
     221             :   }
     222        3153 :   return parse_node(result, m_parser);
     223             : }
     224             : 
     225           0 : void parser::print_symbol_table() const
     226             : {
     227           0 :   m_table.print();
     228           0 : }
     229             : 
     230           0 : std::string parser::indent(unsigned int count) const
     231             : {
     232           0 :   return std::string(count, ' ');
     233             : }
     234             : 
     235           0 : std::string parser::truncate(const std::string& s, unsigned int max_size) const
     236             : {
     237           0 :   std::string result = s.substr(0, max_size);
     238             : 
     239             :   // truncate at newline
     240           0 :   std::string::size_type pos = result.find('\n');
     241           0 :   if (pos != std::string::npos)
     242             :   {
     243           0 :     result = result.substr(0, pos);
     244             :   }
     245             : 
     246           0 :   return result;
     247           0 : }
     248             : 
     249           0 : void parser::print_tree(const parse_node& node, unsigned int level) const
     250             : {
     251           0 :   if (node)
     252             :   {
     253           0 :     std::string symbol = m_table.symbol_name(node.symbol());
     254           0 :     std::string prefix = indent(2 * level);
     255           0 :     std::cout << prefix << "--- " << symbol << " \"" << truncate(node.string()) << "\"" << std::endl;
     256           0 :     for (int i = 0; i <= node.child_count(); i++)
     257             :     {
     258           0 :       print_tree(node.child(i), level + 1);
     259             :     }
     260           0 :   }
     261           0 : }
     262             : 
     263           0 : void parser::destroy_parse_node(const parse_node& node)
     264             : {
     265           0 :   free_D_ParseNode(m_parser, node.node);
     266           0 : }
     267             : 
     268             : /// \brief Callback function for nodes in the parse tree
     269           0 : void parser::announce(D_ParseNode& node_ref)
     270             : {
     271           0 :   parse_node node(&node_ref);
     272           0 :   std::cout << "parsed " << m_table.symbol_name(node.symbol()) << " " << node.string() << std::endl;
     273           0 : }
     274             : 
     275             : namespace detail {
     276             : 
     277           5 : std::string add_context(const d_loc_t* loc, const std::string& message)
     278             : {
     279           5 :   std::stringstream s;
     280           5 :   s << "Line " << loc->line << ", column " << loc->col << ": "
     281           5 :     << message << std::endl;
     282           5 :   char* beg = loc->s - loc->col;
     283           5 :   char* end = loc->s;
     284          43 :   while (*end != '\0' && *end != '\n' && *end != '\r')
     285             :   {
     286          38 :     ++end;
     287             :   }
     288           5 :   std::string line(beg, end);
     289           5 :   s << "  " << line << std::endl;
     290          43 :   for (int i = 0; i < loc->col + 2; ++i)
     291             :   {
     292          38 :     s << ' ';
     293             :   }
     294           5 :   s << '^';
     295          10 :   return s.str();
     296           5 : }
     297             : 
     298             : inline
     299           0 : bool is_all_of_type(D_ParseNode* nodes[], int n, const char* type, const core::parser_table& table)
     300             : {
     301           0 :   for (int i = 0; i < n; i++)
     302             :   {
     303           0 :     core::parse_node node(nodes[i]);
     304           0 :     if (table.symbol_name(node) != type)
     305             :     {
     306           0 :       return false;
     307             :     }
     308           0 :   }
     309           0 :   return true;
     310             : }
     311             : 
     312             : inline
     313             : void print_ambiguous_nodes(D_ParseNode* nodes[], int n, const char* type, const core::parser_table& table)
     314             : {
     315             :   mCRL2log(log::verbose) << "--- " << type << " ambiguity" << std::endl;
     316             :   for (int i = 0; i < n; ++i)
     317             :   {
     318             :     core::parse_node vi(nodes[i]);
     319             :     // mCRL2log(log::verbose) << vi.tree() << " " << table.tree(vi) << std::endl;
     320             :     mCRL2log(log::verbose) << "ALT " << table.tree(vi) << std::endl;
     321             :   }
     322             : }
     323             : 
     324             : inline
     325             : void print_chosen_node(D_ParseNode* node, const core::parser_table& table)
     326             : {
     327             :   core::parse_node vi(node);
     328             :   mCRL2log(log::verbose) << "CHOOSE " << table.tree(vi) << std::endl;
     329             : }
     330             : 
     331             : /// \brief Function for resolving parser ambiguities.
     332           0 : D_ParseNode* ambiguity_fn(struct D_Parser * /*p*/, int n, struct D_ParseNode **v)
     333             : {
     334           0 :   core::parser_table table(parser_tables_mcrl2);
     335             : 
     336             :   // resolve PbesExpr ambiguities
     337           0 :   if (is_all_of_type(v, n, "PbesExpr", table))
     338             :   {
     339           0 :     D_ParseNode* result = nullptr;
     340           0 :     for (int i = 0; i < n; i++)
     341             :     {
     342           0 :       core::parse_node node(v[i]);
     343           0 :       if (table.symbol_name(node.child(0)) == "Id")
     344             :       {
     345           0 :         return v[i];
     346             :       }
     347           0 :       else if (table.symbol_name(node.child(0)) != "DataExpr")
     348             :       {
     349           0 :         result = v[i];
     350             :       }
     351           0 :     }
     352           0 :     if (result)
     353             :     {
     354           0 :       return result;
     355             :     }
     356           0 :     return v[0];
     357             :   }
     358             : 
     359             :   // resolve ActFrm ambiguities
     360           0 :   if (is_all_of_type(v, n, "ActFrm", table))
     361             :   {
     362             : //print_ambiguous_nodes(v, n, "ActFrm", table);
     363           0 :     D_ParseNode* result = nullptr;
     364           0 :     for (int i = 0; i < n; i++)
     365             :     {
     366           0 :       core::parse_node node(v[i]);
     367           0 :       if (table.symbol_name(node.child(0)) == "MultAct")
     368             :       {
     369             : //print_chosen_node(v[i], table);
     370           0 :         return v[i];
     371             :       }
     372           0 :       else if (table.symbol_name(node.child(0)) != "DataExpr")
     373             :       {
     374           0 :         result = v[i];
     375             :       }
     376           0 :     }
     377           0 :     if (result)
     378             :     {
     379             : //print_chosen_node(result, table);
     380           0 :       return result;
     381             :     }
     382             : //print_chosen_node(v[0], table);
     383           0 :     return v[0];
     384             :   }
     385             : 
     386             :   // resolve StateFrm ambiguities
     387           0 :   if (is_all_of_type(v, n, "StateFrm", table))
     388             :   {
     389             : //print_ambiguous_nodes(v, n, "StateFrm", table);
     390           0 :     D_ParseNode* result = nullptr;
     391           0 :     for (int i = 0; i < n; i++)
     392             :     {
     393           0 :       core::parse_node node(v[i]);
     394           0 :       if (table.symbol_name(node.child(0)) == "Id")
     395             :       {
     396             : //print_chosen_node(v[i], table);
     397           0 :         return v[i];
     398             :       }
     399           0 :       else if (table.symbol_name(node.child(0)) != "DataExpr")
     400             :       {
     401           0 :         result = v[i];
     402             :       }
     403           0 :     }
     404           0 :     if (result)
     405             :     {
     406             : //print_chosen_node(result, table);
     407           0 :       return result;
     408             :     }
     409             : //print_chosen_node(v[0], table);
     410           0 :     return v[0];
     411             :   }
     412             : 
     413             :   // resolve RegFrm ambiguities
     414           0 :   if (is_all_of_type(v, n, "RegFrm", table))
     415             :   {
     416             : //print_ambiguous_nodes(v, n, "RegFrm", table);
     417           0 :     for (int i = 0; i < n; i++)
     418             :     {
     419           0 :       core::parse_node node(v[i]);
     420           0 :       if (table.symbol_name(node.child(0)) == "RegFrm" || table.symbol_name(node.child(0)) == "(")
     421             :       {
     422             : //print_chosen_node(v[i], table);
     423           0 :         return v[i];
     424             :       }
     425           0 :     }
     426             :   }
     427             : 
     428             :   // If we reach this point, then the ambiguity is unresolved. We print all
     429             :   // ambiguities on the debug output, then throw an exception.
     430           0 :   for (int i = 0; i < n; ++i)
     431             :   {
     432           0 :     core::parse_node vi(v[i]);
     433           0 :     mCRL2log(log::verbose) << "Ambiguity: " << vi.tree() << std::endl;
     434           0 :     mCRL2log(log::debug) << "Ambiguity: " << table.tree(vi) << std::endl;
     435           0 :   }
     436           0 :   throw mcrl2::runtime_error("Unresolved ambiguity.");
     437             : }
     438             : 
     439           1 : static void log_location(struct D_Parser *ap)
     440             : {
     441             :   // We recover information about the last parsed node by casting D_Parser to Parser, which
     442             :   // is the structure that the dparser library internally uses to keep its administration in.
     443           1 :   std::string after;
     444           1 :   SNode *s = ((Parser*)ap)->snode_hash.last_all;
     445           1 :   ZNode *z = s != nullptr ? s->zns.v[0] : nullptr;
     446           1 :   while (z != nullptr && z->pn->parse_node.start_loc.s == z->pn->parse_node.end)
     447             :   {
     448           0 :     z = (z->sns.v && z->sns.v[0]->zns.v) ? z->sns.v[0]->zns.v[0] : nullptr;
     449             :   }
     450           1 :   if (z && z->pn->parse_node.start_loc.s != z->pn->parse_node.end)
     451             :   {
     452           1 :     after = std::string(z->pn->parse_node.start_loc.s, z->pn->parse_node.end);
     453             :   }
     454             : 
     455           1 :   std::string message = "syntax error";
     456           1 :   if (!after.empty())
     457             :   {
     458           1 :     message = message + " after '" + after + "'";
     459             :   }
     460           1 :   mCRL2log(log::error) << add_context(&ap->loc, message) << std::endl;
     461           1 : }
     462             : 
     463           1 : void syntax_error_fn(struct D_Parser *ap)
     464             : {
     465           1 :   core::detail::increment_dparser_error_message_count();
     466           1 :   if (core::detail::get_dparser_error_message_count() > core::detail::get_dparser_max_error_message_count())
     467             :   {
     468           0 :     return;
     469             :   }
     470           1 :   log_location(ap);
     471           1 :   if (ap->loc.s == nullptr)
     472             :   {
     473           0 :     mCRL2log(log::error) << "Unexpected end of input." << std::endl;
     474             :   }
     475             :   else
     476             :   {
     477             :     // Dive into the internals of dparser to recover some extra diagnostics.
     478           1 :     Parser* p = (Parser*)ap;
     479           1 :     if (p->pnode_hash.all && p->pnode_hash.all->latest)
     480             :     {
     481           1 :       core::parse_node n(&p->pnode_hash.all->latest->parse_node);
     482           1 :       D_Symbol &s = p->t->symbols[n.symbol()];
     483           1 :       if (s.kind == D_SYMBOL_INTERNAL)
     484             :       {
     485             :         /* DParser stores production rules in order: search for the corresponding nonterminal. */
     486           0 :         int parentsym = n.symbol() - 1;
     487           0 :         while (p->t->symbols[parentsym].kind == D_SYMBOL_INTERNAL)
     488           0 :           --parentsym;
     489           0 :         s = p->t->symbols[parentsym];
     490             :       }
     491             : 
     492           1 :       switch (s.kind)
     493             :       {
     494           1 :       case D_SYMBOL_STRING:
     495             :       case D_SYMBOL_TOKEN:
     496             :         {
     497           1 :           std::locale loc;
     498           2 :           mCRL2log(log::error) << "Unexpected "
     499           2 :                                          << (std::isalpha(n.string()[0], loc) ? "keyword " : "")
     500           2 :                                          << "'" << n.string() << "'" << std::endl;
     501           1 :         }
     502           1 :         break;
     503           0 :       case D_SYMBOL_NTERM:
     504           0 :         mCRL2log(log::error) << "Unexpected " << s.name << " '" << n.string() << "'" << std::endl;
     505           0 :         break;
     506           0 :       default:
     507             :         // TODO: check if we can give more sensible output in the remaining cases.
     508           0 :         break;
     509             :       }
     510           1 :     }
     511             :   }
     512             : }
     513             : 
     514             : } // namespace detail
     515             : 
     516           0 : void parser::custom_parse_error(const std::string& message) const
     517             : {
     518           0 :   core::detail::increment_dparser_error_message_count();
     519           0 :   if (core::detail::get_dparser_error_message_count() > core::detail::get_dparser_max_error_message_count())
     520             :   {
     521           0 :     return;
     522             :   }
     523           0 :   detail::log_location(m_parser);
     524           0 :   mCRL2log(log::error) << message << std::endl;
     525             : }
     526             : 
     527             : } // namespace core
     528             : 
     529             : } // namespace mcrl2
     530             :