Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Base class lexer
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5parser_public.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__PARSER__LEXER_H
      16                 :            : #define CVC5__PARSER__LEXER_H
      17                 :            : 
      18                 :            : #include <fstream>
      19                 :            : #include <iosfwd>
      20                 :            : #include <string>
      21                 :            : #include <vector>
      22                 :            : 
      23                 :            : #include "base/check.h"
      24                 :            : #include "parser/input.h"
      25                 :            : #include "parser/tokens.h"
      26                 :            : 
      27                 :            : namespace cvc5 {
      28                 :            : namespace parser {
      29                 :            : 
      30                 :            : /** A location for tracking parse errors */
      31                 :            : struct Location
      32                 :            : {
      33                 :      48764 :   Location() : d_line(1), d_column(1) {}
      34                 :            :   uint32_t d_line;
      35                 :            :   uint32_t d_column;
      36                 :            : };
      37                 :            : std::ostream& operator<<(std::ostream& o, const Location& l);
      38                 :            : 
      39                 :            : /** A span for tracking parse errors */
      40                 :            : struct Span
      41                 :            : {
      42                 :            :   Location d_start;
      43                 :            :   Location d_end;
      44                 :            : };
      45                 :            : std::ostream& operator<<(std::ostream& o, const Span& l);
      46                 :            : 
      47                 :            : #define INPUT_BUFFER_SIZE 32768
      48                 :            : 
      49                 :            : /**
      50                 :            :  * The base lexer class. The main methods to override are initialize and
      51                 :            :  * nextTokenInternal.
      52                 :            :  */
      53                 :            : class Lexer
      54                 :            : {
      55                 :            :  public:
      56                 :            :   Lexer();
      57                 :      24361 :   virtual ~Lexer() {}
      58                 :            :   /**
      59                 :            :    * Initialize the lexer to generate tokens from stream input.
      60                 :            :    * @param input The input stream
      61                 :            :    * @param inputName The name for debugging
      62                 :            :    */
      63                 :            :   virtual void initialize(Input* input, const std::string& inputName);
      64                 :            :   /**
      65                 :            :    * String corresponding to the last token (old top of stack). This is only
      66                 :            :    * valid if no tokens are currently peeked.
      67                 :            :    */
      68                 :            :   virtual const char* tokenStr() const = 0;
      69                 :            :   /** Advance to the next token (pop from stack) */
      70                 :            :   Token nextToken();
      71                 :            :   /** Add a token back into the stream (push to stack) */
      72                 :            :   Token peekToken();
      73                 :            :   /** Expect a token `t` as the next one. Error o.w. */
      74                 :            :   void eatToken(Token t);
      75                 :            :   /**
      76                 :            :    * Expect a token `t` or `f` as the next one, or throw a parse error
      77                 :            :    * otherwise. Return true if `t`.
      78                 :            :    */
      79                 :            :   bool eatTokenChoice(Token t, Token f);
      80                 :            :   /** reinsert token, read back first in, last out */
      81                 :            :   void reinsertToken(Token t);
      82                 :            :   /** Used to report warnings, with the current source location attached. */
      83                 :            :   void warning(const std::string&);
      84                 :            :   /** Used to report errors, with the current source location attached. */
      85                 :            :   void parseError(const std::string&, bool eofException = false);
      86                 :            :   /** Error. Got `t`, expected `info`. */
      87                 :            :   void unexpectedTokenError(Token t, const std::string& info);
      88                 :            : 
      89                 :            :  protected:
      90                 :            :   // -----------------
      91                 :            :   /** Compute the next token by reading from the stream */
      92                 :            :   virtual Token nextTokenInternal() = 0;
      93                 :            :   /** Get the next character */
      94                 :  106224897 :   int32_t readNextChar()
      95                 :            :   {
      96         [ +  + ]:  106224897 :     if (d_bufferPos < d_bufferEnd)
      97                 :            :     {
      98                 :  106162463 :       d_ch = d_buffer[d_bufferPos];
      99                 :  106162463 :       d_bufferPos++;
     100                 :            :     }
     101         [ +  + ]:      62434 :     else if (d_isInteractive)
     102                 :            :     {
     103                 :      15189 :       d_ch = d_istream->get();
     104                 :            :     }
     105                 :            :     else
     106                 :            :     {
     107                 :      47245 :       d_istream->read(d_buffer, INPUT_BUFFER_SIZE);
     108                 :      47245 :       d_bufferEnd = static_cast<size_t>(d_istream->gcount());
     109         [ +  + ]:      47245 :       if (d_bufferEnd == 0)
     110                 :            :       {
     111                 :      20904 :         d_ch = EOF;
     112                 :      20904 :         d_bufferPos = 0;
     113                 :            :       }
     114                 :            :       else
     115                 :            :       {
     116                 :      26341 :         d_ch = d_buffer[0];
     117                 :      26341 :         d_bufferPos = 1;
     118                 :            :       }
     119                 :            :     }
     120                 :  106224897 :     return d_ch;
     121                 :            :   }
     122                 :            :   /** Get the next character */
     123                 :  123714872 :   int32_t nextChar()
     124                 :            :   {
     125                 :            :     int32_t res;
     126         [ +  + ]:  123714872 :     if (d_peekedChar)
     127                 :            :     {
     128                 :   17489975 :       res = d_chPeeked;
     129                 :   17489975 :       d_peekedChar = false;
     130                 :            :     }
     131                 :            :     else
     132                 :            :     {
     133                 :  106224897 :       res = readNextChar();
     134         [ +  + ]:  106224897 :       if (res == '\n')
     135                 :            :       {
     136                 :     843710 :         d_span.d_end.d_line++;
     137                 :     843710 :         d_span.d_end.d_column = 0;
     138                 :            :       }
     139                 :            :       else
     140                 :            :       {
     141                 :  105381187 :         d_span.d_end.d_column++;
     142                 :            :       }
     143                 :            :     }
     144                 :  123714872 :     return res;
     145                 :            :   }
     146                 :            :   /** Save character */
     147                 :   17490017 :   void saveChar(int32_t ch)
     148                 :            :   {
     149 [ -  + ][ -  + ]:   17490017 :     Assert(!d_peekedChar);
                 [ -  - ]
     150                 :   17490017 :     d_peekedChar = true;
     151                 :   17490017 :     d_chPeeked = ch;
     152                 :   17490017 :   }
     153                 :            :   // -----------------
     154                 :            :   /** Used to initialize d_span. */
     155                 :            :   void initSpan();
     156                 :            :   /** Sets the spans start to its current end. */
     157                 :   66878886 :   void bumpSpan()
     158                 :            :   {
     159                 :   66878886 :     d_span.d_start.d_line = d_span.d_end.d_line;
     160                 :   66878886 :     d_span.d_start.d_column = d_span.d_end.d_column;
     161                 :   66878886 :   }
     162                 :            :   /** Add columns or lines to the end location of the span. */
     163                 :            :   void addColumns(uint32_t columns) { d_span.d_end.d_column += columns; }
     164                 :            :   void addLines(uint32_t lines)
     165                 :            :   {
     166                 :            :     d_span.d_end.d_line += lines;
     167                 :            :     d_span.d_end.d_column = 0;
     168                 :            :   }
     169                 :            :   /** Span of last token pulled from underlying lexer (old top of stack) */
     170                 :            :   Span d_span;
     171                 :            :   /** Name of current input, for debugging */
     172                 :            :   std::string d_inputName;
     173                 :            :   /**
     174                 :            :    * The peeked stack. When we peek at the next token, it is added to this
     175                 :            :    * vector. When we read a token, if this vector is non-empty, we return the
     176                 :            :    * back of it and pop.
     177                 :            :    */
     178                 :            :   std::vector<Token> d_peeked;
     179                 :            : 
     180                 :            :  private:
     181                 :            :   /** The input */
     182                 :            :   std::istream* d_istream;
     183                 :            :   /** True if the input stream is interactive */
     184                 :            :   bool d_isInteractive;
     185                 :            :   /** The current buffer */
     186                 :            :   char d_buffer[INPUT_BUFFER_SIZE];
     187                 :            :   /** The position in the current buffer we are reading from */
     188                 :            :   size_t d_bufferPos;
     189                 :            :   /** The size of characters in the current buffer */
     190                 :            :   size_t d_bufferEnd;
     191                 :            :   /** The current character we read. */
     192                 :            :   int32_t d_ch;
     193                 :            :   /** True if we have a saved character that has not been consumed yet. */
     194                 :            :   bool d_peekedChar;
     195                 :            :   /** The saved character. */
     196                 :            :   int32_t d_chPeeked;
     197                 :            : };
     198                 :            : 
     199                 :            : }  // namespace parser
     200                 :            : }  // namespace cvc5
     201                 :            : 
     202                 :            : #endif