Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Base class lexer
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "parser/lexer.h"
      17                 :            : 
      18                 :            : #include <cassert>
      19                 :            : #include <iostream>
      20                 :            : #include <sstream>
      21                 :            : 
      22                 :            : #include "base/output.h"
      23                 :            : #include <cvc5/cvc5_parser.h>
      24                 :            : 
      25                 :            : namespace cvc5 {
      26                 :            : namespace parser {
      27                 :            : 
      28                 :          0 : std::ostream& operator<<(std::ostream& o, const Location& l)
      29                 :            : {
      30                 :          0 :   return o << l.d_line << ":" << l.d_column;
      31                 :            : }
      32                 :          0 : std::ostream& operator<<(std::ostream& o, const Span& l)
      33                 :            : {
      34                 :          0 :   return o << l.d_start << "-" << l.d_end;
      35                 :            : }
      36                 :            : 
      37                 :      23024 : Lexer::Lexer()
      38                 :      23024 :     : d_bufferPos(0), d_bufferEnd(0), d_peekedChar(false), d_chPeeked(0)
      39                 :            : {
      40                 :      23024 : }
      41                 :            : 
      42                 :        239 : void Lexer::warning(const std::string& msg)
      43                 :            : {
      44         [ +  + ]:        239 :   Warning() << d_inputName << ':' << d_span.d_start.d_line << '.'
      45                 :        239 :             << d_span.d_start.d_column << ": " << msg << std::endl;
      46                 :        239 : }
      47                 :            : 
      48                 :         85 : void Lexer::parseError(const std::string& msg, bool eofException)
      49                 :            : {
      50         [ +  + ]:         85 :   if (eofException)
      51                 :            :   {
      52                 :            :     throw ParserEndOfFileException(
      53                 :          1 :         msg, d_inputName, d_span.d_start.d_line, d_span.d_start.d_column);
      54                 :            :   }
      55                 :            :   else
      56                 :            :   {
      57                 :            :     throw ParserException(
      58                 :         84 :         msg, d_inputName, d_span.d_start.d_line, d_span.d_start.d_column);
      59                 :            :   }
      60                 :            : }
      61                 :            : 
      62                 :      23030 : void Lexer::initSpan()
      63                 :            : {
      64                 :      23030 :   d_span.d_start.d_line = 1;
      65                 :      23030 :   d_span.d_start.d_column = 0;
      66                 :      23030 :   d_span.d_end.d_line = 1;
      67                 :      23030 :   d_span.d_end.d_column = 0;
      68                 :      23030 : }
      69                 :            : 
      70                 :      23030 : void Lexer::initialize(Input* input, const std::string& inputName)
      71                 :            : {
      72 [ -  + ][ -  + ]:      23030 :   Assert(input != nullptr);
                 [ -  - ]
      73                 :      23030 :   d_istream = input->getStream();
      74                 :      23030 :   d_isInteractive = input->isInteractive();
      75                 :      23030 :   d_inputName = inputName;
      76                 :      23030 :   initSpan();
      77                 :      23030 :   d_peeked.clear();
      78                 :      23030 :   d_bufferPos = 0;
      79                 :      23030 :   d_bufferEnd = 0;
      80                 :      23030 :   d_peekedChar = false;
      81                 :      23030 :   d_chPeeked = 0;
      82                 :      23030 : }
      83                 :            : 
      84                 :   35918500 : Token Lexer::nextToken()
      85                 :            : {
      86         [ +  + ]:   35918500 :   if (d_peeked.empty())
      87                 :            :   {
      88                 :            :     // Call the derived yylex() and convert it to a token
      89                 :   35737300 :     return nextTokenInternal();
      90                 :            :   }
      91                 :     181157 :   Token t = d_peeked.back();
      92                 :     181157 :   d_peeked.pop_back();
      93                 :     181157 :   return t;
      94                 :            : }
      95                 :            : 
      96                 :      37714 : Token Lexer::peekToken()
      97                 :            : {
      98                 :            :   // since d_peeked is first in, last out, we should not peek more than once
      99                 :            :   // or the order is swapped.
     100 [ -  + ][ -  + ]:      37714 :   Assert(d_peeked.empty());
                 [ -  - ]
     101                 :            :   // parse next token
     102                 :      37714 :   Token t = nextTokenInternal();
     103                 :            :   // reinsert it immediately
     104                 :      37709 :   reinsertToken(t);
     105                 :            :   // return it
     106                 :      37709 :   return t;
     107                 :            : }
     108                 :            : 
     109                 :     181200 : void Lexer::reinsertToken(Token t) { d_peeked.push_back(t); }
     110                 :            : 
     111                 :         10 : void Lexer::unexpectedTokenError(Token t, const std::string& info)
     112                 :            : {
     113 [ -  + ][ -  + ]:         10 :   Assert(d_peeked.empty());
                 [ -  - ]
     114                 :         20 :   std::ostringstream o{};
     115                 :         10 :   o << info << ", got `" << tokenStr() << "` (" << t << ").";
     116                 :            :   // Note that we treat this as an EOF exception if the token is EOF_TOK.
     117                 :            :   // This is important for exception handling in interactive mode.
     118                 :         20 :   parseError(o.str(), t == Token::EOF_TOK);
     119                 :          0 : }
     120                 :            : 
     121                 :    2194790 : void Lexer::eatToken(Token t)
     122                 :            : {
     123                 :    2194790 :   Token tt = nextToken();
     124         [ +  + ]:    2194790 :   if (t != tt)
     125                 :            :   {
     126                 :          8 :     std::ostringstream o{};
     127                 :          4 :     o << "Expected a " << t;
     128                 :          8 :     unexpectedTokenError(tt, o.str());
     129                 :            :   }
     130                 :    2194790 : }
     131                 :            : 
     132                 :    1589560 : bool Lexer::eatTokenChoice(Token t, Token f)
     133                 :            : {
     134                 :    1589560 :   Token tt = nextToken();
     135         [ +  + ]:    1589560 :   if (tt == t)
     136                 :            :   {
     137                 :     520617 :     return true;
     138                 :            :   }
     139         [ +  + ]:    1068940 :   else if (tt != f)
     140                 :            :   {
     141                 :          4 :     std::ostringstream o{};
     142                 :          2 :     o << "Expected " << t << " or " << f;
     143                 :          4 :     unexpectedTokenError(tt, o.str());
     144                 :            :   }
     145                 :    1068940 :   return false;
     146                 :            : }
     147                 :            : 
     148                 :            : }  // namespace parser
     149                 :            : }  // namespace cvc5