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                 :            :  * The lexer for smt2
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "parser/smt2/smt2_lexer.h"
      17                 :            : 
      18                 :            : #include <cstdio>
      19                 :            : 
      20                 :            : #include "base/output.h"
      21                 :            : #include "parser/lexer.h"
      22                 :            : 
      23                 :            : namespace cvc5 {
      24                 :            : namespace parser {
      25                 :            : 
      26                 :      23713 : Smt2Lexer::Smt2Lexer(bool isStrict, bool isSygus)
      27                 :            :     : Lexer(),
      28                 :            :       d_isStrict(isStrict),
      29                 :      23713 :       d_isSygus(isSygus)
      30                 :            : {
      31         [ +  + ]:     640251 :   for (int32_t ch = 'a'; ch <= 'z'; ++ch)
      32                 :            :   {
      33                 :     616538 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      34                 :     616538 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      35                 :            :   }
      36         [ +  + ]:     165991 :   for (int32_t ch = 'a'; ch <= 'f'; ++ch)
      37                 :            :   {
      38                 :     142278 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      39                 :            :   }
      40         [ +  + ]:     640251 :   for (int32_t ch = 'A'; ch <= 'Z'; ++ch)
      41                 :            :   {
      42                 :     616538 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      43                 :     616538 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      44                 :            :   }
      45         [ +  + ]:     165991 :   for (int32_t ch = 'A'; ch <= 'F'; ++ch)
      46                 :            :   {
      47                 :     142278 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      48                 :            :   }
      49         [ +  + ]:     260843 :   for (int32_t ch = '0'; ch <= '9'; ++ch)
      50                 :            :   {
      51                 :     237130 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::HEXADECIMAL_DIGIT);
      52                 :     237130 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::DECIMAL_DIGIT);
      53                 :     237130 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      54                 :            :   }
      55                 :      23713 :   d_charClass['0'] |= static_cast<uint32_t>(CharacterClass::BIT);
      56                 :      23713 :   d_charClass['1'] |= static_cast<uint32_t>(CharacterClass::BIT);
      57                 :            :   // ~!@$%^&*_-+|=<>.?/
      58         [ +  + ]:     426834 :   for (int32_t ch : s_extraSymbolChars)
      59                 :            :   {
      60                 :     403121 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL_START);
      61                 :     403121 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::SYMBOL);
      62                 :            :   }
      63         [ +  + ]:    2347590 :   for (int32_t ch : s_printableAsciiChars)
      64                 :            :   {
      65                 :    2323870 :     d_charClass[ch] |= static_cast<uint32_t>(CharacterClass::PRINTABLE);
      66                 :            :   }
      67                 :            :   // whitespace
      68                 :      23713 :   d_charClass[' '] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      69                 :      23713 :   d_charClass['\t'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      70                 :      23713 :   d_charClass['\r'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      71                 :      23713 :   d_charClass['\n'] |= static_cast<uint32_t>(CharacterClass::WHITESPACE);
      72                 :      23713 : }
      73                 :            : 
      74                 :   16717600 : const char* Smt2Lexer::tokenStr() const
      75                 :            : {
      76 [ +  - ][ +  - ]:   33435100 :   Assert(!d_token.empty() && d_token.back() == 0);
         [ -  + ][ -  - ]
      77                 :   16717600 :   return d_token.data();
      78                 :            : }
      79                 :     451352 : bool Smt2Lexer::isStrict() const { return d_isStrict; }
      80                 :      23713 : bool Smt2Lexer::isSygus() const { return d_isSygus; }
      81                 :            : 
      82                 :   36018300 : Token Smt2Lexer::nextTokenInternal()
      83                 :            : {
      84         [ +  - ]:   36018300 :   Trace("lexer-debug") << "Call nextToken" << std::endl;
      85                 :   36018300 :   d_token.clear();
      86                 :   36018300 :   Token ret = computeNextToken();
      87                 :            :   // null terminate?
      88                 :   36018300 :   d_token.push_back(0);
      89         [ +  - ]:   72036500 :   Trace("lexer-debug") << "Return nextToken " << ret << " / " << tokenStr()
      90                 :   36018300 :                        << std::endl;
      91                 :   36018300 :   return ret;
      92                 :            : }
      93                 :            : 
      94                 :   36018300 : Token Smt2Lexer::computeNextToken()
      95                 :            : {
      96                 :   36018300 :   bumpSpan();
      97                 :            :   int32_t ch;
      98                 :            :   // skip whitespace and comments
      99                 :            :   for (;;)
     100                 :            :   {
     101                 :   18927600 :     do
     102                 :            :     {
     103         [ +  + ]:   54945900 :       if ((ch = nextChar()) == EOF)
     104                 :            :       {
     105                 :      20134 :         return Token::EOF_TOK;
     106                 :            :       }
     107         [ +  + ]:   54925800 :     } while (isCharacterClass(ch, CharacterClass::WHITESPACE));
     108                 :            : 
     109         [ +  + ]:   36041300 :     if (ch != ';')
     110                 :            :     {
     111                 :   35998100 :       break;
     112                 :            :     }
     113         [ +  + ]:    1118180 :     while ((ch = nextChar()) != '\n')
     114                 :            :     {
     115         [ +  + ]:    1075020 :       if (ch == EOF)
     116                 :            :       {
     117                 :          4 :         return Token::EOF_TOK;
     118                 :            :       }
     119                 :            :     }
     120                 :            :   }
     121                 :   35998100 :   bumpSpan();
     122                 :   35998100 :   pushToToken(ch);
     123 [ +  + ][ +  + ]:   35998100 :   switch (ch)
            [ +  + ][ + ]
     124                 :            :   {
     125                 :    9303140 :     case '(': return Token::LPAREN_TOK;
     126                 :    9303010 :     case ')': return Token::RPAREN_TOK;
     127                 :     273108 :     case '|':
     128                 :     258971 :       do
     129                 :            :       {
     130                 :     273108 :         ch = nextChar();
     131         [ -  + ]:     273108 :         if (ch == EOF)
     132                 :            :         {
     133                 :          0 :           return Token::UNTERMINATED_QUOTED_SYMBOL;
     134                 :            :         }
     135                 :     273108 :         pushToToken(ch);
     136         [ +  + ]:     273108 :       } while (ch != '|');
     137                 :      14137 :       return Token::QUOTED_SYMBOL;
     138                 :      19216 :     case '#':
     139 [ +  + ][ +  - ]:      19216 :       ch = nextChar();
     140                 :            :       switch (ch)
     141                 :            :       {
     142                 :      13550 :         case 'b':
     143                 :      13550 :           pushToToken(ch);
     144                 :            :           // parse [01]+
     145         [ +  + ]:      13550 :           if (!parseNonEmptyCharList(CharacterClass::BIT))
     146                 :            :           {
     147                 :          6 :             parseError("Error expected bit string");
     148                 :            :           }
     149                 :      13548 :           return Token::BINARY_LITERAL;
     150                 :       3658 :         case 'x':
     151                 :       3658 :           pushToToken(ch);
     152                 :            :           // parse [0-9a-fA-F]+
     153         [ +  + ]:       3658 :           if (!parseNonEmptyCharList(CharacterClass::HEXADECIMAL_DIGIT))
     154                 :            :           {
     155                 :          6 :             parseError("Error expected hexadecimal string");
     156                 :            :           }
     157                 :       3656 :           return Token::HEX_LITERAL;
     158                 :       2008 :         case 'f':
     159                 :       2008 :           pushToToken(ch);
     160                 :            :           // parse [0-9]+m[0-9]+
     161         [ -  + ]:       2008 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     162                 :            :           {
     163                 :          0 :             parseError("Error expected decimal for finite field value");
     164                 :            :           }
     165         [ -  + ]:       2008 :           if (!parseLiteralChar('m'))
     166                 :            :           {
     167                 :          0 :             parseError("Error bad syntax for finite field value");
     168                 :            :           }
     169         [ -  + ]:       2008 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     170                 :            :           {
     171                 :          0 :             parseError("Error expected decimal for finite field size");
     172                 :            :           }
     173                 :       2008 :           return Token::FIELD_LITERAL;
     174                 :          0 :         default:
     175                 :            :           // otherwise error
     176                 :          0 :           parseError("Error finding token following #");
     177                 :          0 :           break;
     178                 :            :       }
     179                 :          0 :       break;
     180                 :     212393 :     case '"':
     181                 :            :       for (;;)
     182                 :            :       {
     183                 :     212393 :         ch = nextChar();
     184         [ -  + ]:     212393 :         if (ch == EOF)
     185                 :            :         {
     186                 :          0 :           return Token::UNTERMINATED_STRING_LITERAL;
     187                 :            :         }
     188         [ +  + ]:     212393 :         else if (!isCharacterClass(ch, CharacterClass::PRINTABLE))
     189                 :            :         {
     190                 :          3 :           parseError("Non-printable character in string literal");
     191                 :            :         }
     192         [ +  + ]:     212392 :         else if (ch == '"')
     193                 :            :         {
     194                 :      29100 :           pushToToken(ch);
     195                 :      29100 :           ch = nextChar();
     196                 :            :           // "" denotes the escape sequence for "
     197         [ +  + ]:      29100 :           if (ch != '"')
     198                 :            :           {
     199                 :      29046 :             saveChar(ch);
     200                 :      29046 :             return Token::STRING_LITERAL;
     201                 :            :           }
     202                 :            :         }
     203                 :     183346 :         pushToToken(ch);
     204                 :            :       }
     205                 :            :       break;
     206                 :      53525 :     case ':':
     207                 :            :       // parse a simple symbol
     208         [ -  + ]:      53525 :       if (!parseChar(CharacterClass::SYMBOL_START))
     209                 :            :       {
     210                 :          0 :         parseError("Error expected symbol following :");
     211                 :            :       }
     212                 :      53525 :       parseNonEmptyCharList(CharacterClass::SYMBOL);
     213                 :      53525 :       return Token::KEYWORD;
     214                 :   17276100 :     default:
     215         [ +  + ]:   17276100 :       if (isCharacterClass(ch, CharacterClass::DECIMAL_DIGIT))
     216                 :            :       {
     217                 :    1474690 :         Token res = Token::INTEGER_LITERAL;
     218                 :            :         // parse [0-9]*
     219                 :    1474690 :         parseCharList(CharacterClass::DECIMAL_DIGIT);
     220                 :            :         // maybe .[0-9]+
     221                 :    1474690 :         ch = nextChar();
     222         [ +  + ]:    1474690 :         if (ch == '.')
     223                 :            :         {
     224                 :      73627 :           pushToToken(ch);
     225                 :      73627 :           res = Token::DECIMAL_LITERAL;
     226                 :            :           // parse [0-9]+
     227         [ +  + ]:      73627 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     228                 :            :           {
     229                 :          3 :             parseError("Error expected decimal string following .");
     230                 :            :           }
     231                 :            :         }
     232         [ +  + ]:    1401070 :         else if (ch == '/')
     233                 :            :         {
     234                 :          9 :           pushToToken(ch);
     235                 :          9 :           res = Token::RATIONAL_LITERAL;
     236                 :            :           // parse [0-9]+
     237         [ -  + ]:          9 :           if (!parseNonEmptyCharList(CharacterClass::DECIMAL_DIGIT))
     238                 :            :           {
     239                 :          0 :             parseError("Error expected decimal string following .");
     240                 :            :           }
     241                 :            :         }
     242                 :            :         else
     243                 :            :         {
     244                 :            :           // otherwise, undo
     245                 :    1401060 :           saveChar(ch);
     246                 :            :         }
     247                 :    1474690 :         return res;
     248                 :            :       }
     249         [ +  - ]:   15801400 :       else if (isCharacterClass(ch, CharacterClass::SYMBOL_START))
     250                 :            :       {
     251                 :            :         // otherwise, we are a simple symbol or standard alphanumeric token
     252                 :            :         // note that we group the case when `:` is here.
     253                 :   15801400 :         parseCharList(CharacterClass::SYMBOL);
     254                 :            :         // tokenize the current symbol, which may be a special case
     255                 :   15801400 :         return tokenizeCurrentSymbol();
     256                 :            :       }
     257                 :            :       // otherwise error
     258                 :          0 :       break;
     259                 :            :   }
     260                 :          0 :   parseError("Error finding token");
     261                 :          0 :   return Token::NONE;
     262                 :            : }
     263                 :            : 
     264                 :       2008 : bool Smt2Lexer::parseLiteralChar(int32_t chc)
     265                 :            : {
     266                 :       2008 :   int32_t ch = nextChar();
     267         [ -  + ]:       2008 :   if (ch != chc)
     268                 :            :   {
     269                 :            :     // will be an error
     270                 :          0 :     return false;
     271                 :            :   }
     272                 :       2008 :   pushToToken(ch);
     273                 :       2008 :   return true;
     274                 :            : }
     275                 :            : 
     276                 :      53525 : bool Smt2Lexer::parseChar(CharacterClass cc)
     277                 :            : {
     278                 :      53525 :   int32_t ch = nextChar();
     279         [ -  + ]:      53525 :   if (!isCharacterClass(ch, cc))
     280                 :            :   {
     281                 :            :     // will be an error
     282                 :          0 :     return false;
     283                 :            :   }
     284                 :      53525 :   pushToToken(ch);
     285                 :      53525 :   return true;
     286                 :            : }
     287                 :            : 
     288                 :     148385 : bool Smt2Lexer::parseNonEmptyCharList(CharacterClass cc)
     289                 :            : {
     290                 :            :   // must contain at least one character
     291                 :     148385 :   int32_t ch = nextChar();
     292         [ +  + ]:     148385 :   if (!isCharacterClass(ch, cc))
     293                 :            :   {
     294                 :            :     // will be an error
     295                 :          5 :     return false;
     296                 :            :   }
     297                 :     148380 :   pushToToken(ch);
     298                 :     148380 :   parseCharList(cc);
     299                 :     148380 :   return true;
     300                 :            : }
     301                 :            : 
     302                 :   74716900 : void Smt2Lexer::parseCharList(CharacterClass cc)
     303                 :            : {
     304                 :            :   int32_t ch;
     305                 :            :   for (;;)
     306                 :            :   {
     307                 :   74716900 :     ch = nextChar();
     308         [ +  + ]:   74716900 :     if (!isCharacterClass(ch, cc))
     309                 :            :     {
     310                 :            :       // failed, we are done, put the character back
     311                 :   17424500 :       saveChar(ch);
     312                 :   17424500 :       return;
     313                 :            :     }
     314                 :   57292400 :     pushToToken(ch);
     315                 :            :   }
     316                 :            : }
     317                 :            : 
     318                 :   15801400 : Token Smt2Lexer::tokenizeCurrentSymbol() const
     319                 :            : {
     320 [ -  + ][ -  + ]:   15801400 :   Assert(!d_token.empty());
                 [ -  - ]
     321 [ +  + ][ +  + ]:   15801400 :   switch (d_token[0])
         [ +  + ][ +  + ]
     322                 :            :   {
     323                 :      23522 :     case '!':
     324         [ +  + ]:      23522 :       if (d_token.size() == 1)
     325                 :            :       {
     326                 :      23495 :         return Token::ATTRIBUTE_TOK;
     327                 :            :       }
     328                 :         27 :       break;
     329                 :     857598 :     case 'a':
     330 [ +  + ][ +  + ]:     857598 :       if (d_token.size() == 2 && d_token[1] == 's')
                 [ +  + ]
     331                 :            :       {
     332                 :       2045 :         return Token::AS_TOK;
     333                 :            :       }
     334                 :     855553 :       break;
     335                 :     265960 :     case 'p':
     336 [ +  + ][ +  + ]:     265960 :       if (d_token.size() == 3 && d_token[1] == 'a' && d_token[2] == 'r')
         [ +  - ][ +  + ]
     337                 :            :       {
     338                 :        178 :         return Token::PAR_TOK;
     339                 :            :       }
     340                 :     265782 :       break;
     341                 :     285801 :     case 'l':
     342 [ +  + ][ +  + ]:     285801 :       if (d_token.size() == 3 && d_token[1] == 'e' && d_token[2] == 't')
         [ +  + ][ +  + ]
     343                 :            :       {
     344                 :     234158 :         return Token::LET_TOK;
     345                 :            :       }
     346                 :      51643 :       break;
     347                 :      18139 :     case 'm':
     348 [ +  + ][ +  + ]:      20041 :       if (d_token.size() == 5 && d_token[1] == 'a' && d_token[2] == 't'
     349 [ +  + ][ +  - ]:      20041 :           && d_token[3] == 'c' && d_token[4] == 'h')
         [ +  - ][ +  + ]
     350                 :            :       {
     351                 :         55 :         return Token::MATCH_TOK;
     352                 :            :       }
     353                 :      18084 :       break;
     354                 :    2793700 :     case '_':
     355         [ +  + ]:    2793700 :       if (d_token.size() == 1)
     356                 :            :       {
     357                 :     419031 :         return Token::INDEX_TOK;
     358                 :            :       }
     359                 :    2374670 :       break;
     360                 :     408390 :     case '-':
     361                 :            :     {
     362                 :            :       // note that `-4`, `-4.0`, `-4/5` are SMT-LIB symbols, hence we only
     363                 :            :       // convert these to literals if we are not strict parsing.
     364 [ +  + ][ +  + ]:     408390 :       if (!d_isStrict && d_token.size() >= 2)
                 [ +  + ]
     365                 :            :       {
     366                 :            :         // reparse as a negative numeral, rational or decimal
     367                 :      22156 :         Token ret = Token::INTEGER_LITERAL;
     368         [ +  + ]:      22197 :         for (size_t i = 1, tsize = d_token.size(); i < tsize; i++)
     369                 :            :         {
     370         [ +  + ]:      22174 :           if (isCharacterClass(d_token[i], CharacterClass::DECIMAL_DIGIT))
     371                 :            :           {
     372                 :         35 :             continue;
     373                 :            :           }
     374 [ +  + ][ +  - ]:      22139 :           else if (i + 1 < tsize && ret == Token::INTEGER_LITERAL)
     375                 :            :           {
     376         [ +  + ]:         61 :             if (d_token[i] == '.')
     377                 :            :             {
     378                 :          3 :               ret = Token::DECIMAL_LITERAL;
     379                 :          3 :               continue;
     380                 :            :             }
     381         [ +  + ]:         58 :             else if (d_token[i] == '/')
     382                 :            :             {
     383                 :          3 :               ret = Token::RATIONAL_LITERAL;
     384                 :          3 :               continue;
     385                 :            :             }
     386                 :            :           }
     387                 :      22133 :           return Token::SYMBOL;
     388                 :            :         }
     389                 :         23 :         return ret;
     390                 :            :       }
     391                 :            :     }
     392                 :     386234 :     break;
     393                 :   11148300 :     default: break;
     394                 :            :   }
     395                 :            :   // otherwise not a special symbol
     396                 :   15100300 :   return Token::SYMBOL;
     397                 :            : }
     398                 :            : 
     399                 :            : }  // namespace parser
     400                 :            : }  // namespace cvc5