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                 :            :  * Black box testing of cvc5::parser::InputParser for SMT-LIbv2 inputs.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include <cvc5/cvc5.h>
      14                 :            : #include <cvc5/cvc5_parser.h>
      15                 :            : 
      16                 :            : #include <sstream>
      17                 :            : 
      18                 :            : #include "base/output.h"
      19                 :            : #include "options/base_options.h"
      20                 :            : #include "options/language.h"
      21                 :            : #include "options/options.h"
      22                 :            : #include "test.h"
      23                 :            : 
      24                 :            : using namespace cvc5::parser;
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace test {
      28                 :            : 
      29                 :            : class TestParserBlack : public TestInternal
      30                 :            : {
      31                 :            :  protected:
      32                 :          5 :   TestParserBlack(modes::InputLanguage lang) : d_lang(lang) {}
      33                 :            : 
      34                 :          5 :   virtual ~TestParserBlack() {}
      35                 :            : 
      36                 :          5 :   void SetUp() override
      37                 :            :   {
      38                 :          5 :     TestInternal::SetUp();
      39                 :          5 :     d_symman.reset(nullptr);
      40                 :          5 :     d_solver.reset(new cvc5::Solver(d_tm));
      41                 :          5 :     d_solver->setOption("parse-only", "true");
      42                 :          5 :   }
      43                 :            : 
      44                 :          5 :   void TearDown() override
      45                 :            :   {
      46                 :          5 :     d_symman.reset(nullptr);
      47                 :          5 :     d_solver.reset(nullptr);
      48                 :          5 :   }
      49                 :            : 
      50                 :            :   /* Set up declaration context for expr inputs */
      51                 :         33 :   void setupContext(InputParser& parser)
      52                 :            :   {
      53                 :         33 :     std::stringstream ss;
      54                 :         33 :     ss << "(set-logic ALL)" << std::endl;
      55                 :         33 :     ss << "(declare-fun a () Bool)" << std::endl;
      56                 :         33 :     ss << "(declare-fun b () Bool)" << std::endl;
      57                 :         33 :     ss << "(declare-fun c () Bool)" << std::endl;
      58                 :         33 :     ss << "(declare-sort t 0)" << std::endl;
      59                 :         33 :     ss << "(declare-sort u 0)" << std::endl;
      60                 :         33 :     ss << "(declare-sort v 0)" << std::endl;
      61                 :         33 :     ss << "(declare-fun f (t) u)" << std::endl;
      62                 :         33 :     ss << "(declare-fun g (u) v)" << std::endl;
      63                 :         33 :     ss << "(declare-fun h (v) t)" << std::endl;
      64                 :         33 :     ss << "(declare-fun x () t)" << std::endl;
      65                 :         33 :     ss << "(declare-fun y () u)" << std::endl;
      66                 :         33 :     ss << "(declare-fun z () v)" << std::endl;
      67                 :         33 :     parser.setStreamInput(
      68                 :            :         modes::InputLanguage::SMT_LIB_2_6, ss, "parser_black");
      69                 :         33 :     Command cmd;
      70                 :         33 :     std::stringstream tmp;
      71                 :            :     while (true)
      72                 :            :     {
      73                 :        462 :       cmd = parser.nextCommand();
      74         [ +  + ]:        462 :       if (cmd.isNull())
      75                 :            :       {
      76                 :         33 :         break;
      77                 :            :       }
      78                 :        429 :       cmd.invoke(d_solver.get(), d_symman.get(), tmp);
      79                 :            :     }
      80                 :         33 :   }
      81                 :            : 
      82                 :         14 :   void tryGoodInput(const std::string goodInput)
      83                 :            :   {
      84                 :         14 :     d_solver.reset(new cvc5::Solver(d_tm));
      85                 :         14 :     d_symman.reset(new SymbolManager(d_tm));
      86                 :         14 :     InputParser parser(d_solver.get(), d_symman.get());
      87                 :         14 :     std::stringstream ss;
      88                 :         14 :     ss << goodInput;
      89                 :         14 :     parser.setStreamInput(
      90                 :            :         modes::InputLanguage::SMT_LIB_2_6, ss, "parser_black");
      91 [ -  + ][ +  - ]:         14 :     ASSERT_FALSE(parser.done());
      92                 :         14 :     Command cmd;
      93                 :         14 :     std::stringstream tmp;
      94                 :            :     while (true)
      95                 :            :     {
      96                 :         44 :       cmd = parser.nextCommand();
      97         [ +  + ]:         44 :       if (cmd.isNull())
      98                 :            :       {
      99                 :         14 :         break;
     100                 :            :       }
     101         [ +  - ]:         30 :       Trace("parser") << "Parsed command: " << cmd << std::endl;
     102                 :         30 :       cmd.invoke(d_solver.get(), d_symman.get(), tmp);
     103                 :            :     }
     104                 :            : 
     105 [ -  + ][ +  - ]:         14 :     ASSERT_TRUE(parser.done());
     106 [ +  - ][ +  - ]:         14 :   }
     107                 :            : 
     108                 :          8 :   void tryBadInput(const std::string badInput, bool strictMode = false)
     109                 :            :   {
     110                 :          8 :     d_solver.reset(new cvc5::Solver(d_tm));
     111         [ +  + ]:          8 :     d_solver->setOption("strict-parsing", strictMode ? "true" : "false");
     112                 :          8 :     d_symman.reset(new SymbolManager(d_tm));
     113                 :          8 :     InputParser parser(d_solver.get(), d_symman.get());
     114                 :          8 :     std::stringstream ss;
     115                 :          8 :     ss << badInput;
     116                 :          8 :     parser.setStreamInput(d_lang, ss, "parser_black");
     117                 :         27 :     ASSERT_THROW(
     118                 :            :         {
     119                 :            :           Command cmd;
     120                 :            :           std::stringstream tmp;
     121                 :            :           while (true)
     122                 :            :           {
     123                 :            :             cmd = parser.nextCommand();
     124                 :            :             if (cmd.isNull())
     125                 :            :             {
     126                 :            :               break;
     127                 :            :             }
     128                 :            :             Trace("parser") << "Parsed command: " << cmd << std::endl;
     129                 :            :             cmd.invoke(d_solver.get(), d_symman.get(), tmp);
     130                 :            :           }
     131                 :            :           std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
     132                 :            :         },
     133         [ +  - ]:          8 :         ParserException);
     134 [ +  - ][ +  - ]:          8 :   }
     135                 :            : 
     136                 :         12 :   void tryGoodExpr(const std::string goodExpr)
     137                 :            :   {
     138                 :         12 :     d_solver.reset(new cvc5::Solver(d_tm));
     139                 :         12 :     d_symman.reset(new SymbolManager(d_tm));
     140                 :         12 :     InputParser parser(d_solver.get(), d_symman.get());
     141                 :         12 :     setupContext(parser);
     142                 :            : 
     143                 :         12 :     std::stringstream ss;
     144                 :         12 :     ss << goodExpr;
     145                 :         12 :     parser.setStreamInput(d_lang, ss, "parser_black");
     146                 :            : 
     147 [ -  + ][ +  - ]:         12 :     ASSERT_FALSE(parser.done());
     148                 :         12 :     cvc5::Term e = parser.nextTerm();
     149 [ -  + ][ +  - ]:         12 :     ASSERT_FALSE(e.isNull());
     150                 :         12 :     e = parser.nextTerm();
     151 [ -  + ][ +  - ]:         12 :     ASSERT_TRUE(parser.done());
     152 [ -  + ][ +  - ]:         12 :     ASSERT_TRUE(e.isNull());
     153 [ +  - ][ +  - ]:         12 :   }
     154                 :            : 
     155                 :            :   /**
     156                 :            :    * NOTE: The check implemented here may fail if a bad expression
     157                 :            :    * expression string has a prefix that is parseable as a good
     158                 :            :    * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
     159                 :            :    * actually return the bit-vector 10 and ignore the tail of the
     160                 :            :    * input. It's more trouble than it's worth to check that the whole
     161                 :            :    * input was consumed here, so just be careful to avoid valid
     162                 :            :    * prefixes in tests.
     163                 :            :    */
     164                 :         21 :   void tryBadExpr(const std::string badExpr, bool strictMode = false)
     165                 :            :   {
     166                 :         21 :     d_solver.reset(new cvc5::Solver(d_tm));
     167         [ +  + ]:         21 :     d_solver->setOption("strict-parsing", strictMode ? "true" : "false");
     168                 :         21 :     d_symman.reset(new SymbolManager(d_tm));
     169                 :         21 :     InputParser parser(d_solver.get(), d_symman.get());
     170                 :         21 :     setupContext(parser);
     171                 :         21 :     std::stringstream ss;
     172                 :         21 :     ss << badExpr;
     173                 :         21 :     parser.setStreamInput(d_lang, ss, "parser_black");
     174 [ -  + ][ +  - ]:         21 :     ASSERT_FALSE(parser.done());
     175                 :         42 :     ASSERT_THROW(cvc5::Term e = parser.nextTerm();
     176                 :            :                  std::cout << std::endl
     177                 :            :                            << "Bad expr succeeded." << std::endl
     178                 :            :                            << "Input: <<" << badExpr << ">>" << std::endl
     179                 :            :                            << "Output: <<" << e << ">>" << std::endl;
     180         [ +  - ]:         21 :                  , ParserException);
     181 [ +  - ][ +  - ]:         21 :   }
     182                 :            : 
     183                 :            :   modes::InputLanguage d_lang;
     184                 :            :   cvc5::TermManager d_tm;
     185                 :            :   std::unique_ptr<cvc5::Solver> d_solver;
     186                 :            :   std::unique_ptr<SymbolManager> d_symman;
     187                 :            : };
     188                 :            : 
     189                 :            : /* -------------------------------------------------------------------------- */
     190                 :            : 
     191                 :            : class TestParserBlackSmt2InputParser : public TestParserBlack
     192                 :            : {
     193                 :            :  protected:
     194                 :          5 :   TestParserBlackSmt2InputParser()
     195                 :          5 :       : TestParserBlack(modes::InputLanguage::SMT_LIB_2_6)
     196                 :            :   {
     197                 :          5 :   }
     198                 :            : };
     199                 :            : 
     200                 :          4 : TEST_F(TestParserBlackSmt2InputParser, good_inputs)
     201                 :            : {
     202                 :          1 :   tryGoodInput("");  // empty string is OK
     203                 :          1 :   tryGoodInput("(set-logic QF_UF)");
     204                 :          1 :   tryGoodInput("(set-info :notes |This is a note, take note!|)");
     205                 :          1 :   tryGoodInput("(set-logic QF_UF) (assert true)");
     206                 :          1 :   tryGoodInput("(check-sat)");
     207                 :          1 :   tryGoodInput("(exit)");
     208                 :          1 :   tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
     209                 :          1 :   tryGoodInput(
     210                 :            :       "(set-logic QF_UF) (declare-fun a () Bool) "
     211                 :            :       "(declare-fun b () Bool)");
     212                 :          1 :   tryGoodInput(
     213                 :            :       "(set-logic QF_UF) (declare-fun a () Bool) "
     214                 :            :       "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))");
     215                 :          1 :   tryGoodInput(
     216                 :            :       "(set-logic QF_UF) (declare-sort a 0) "
     217                 :            :       "(declare-fun f (a) a) (declare-fun x () a) "
     218                 :            :       "(assert (= (f x) x))");
     219                 :          1 :   tryGoodInput(
     220                 :            :       "(set-logic QF_UF) (declare-sort a 0) "
     221                 :            :       "(declare-fun x () a) (declare-fun y () a) "
     222                 :            :       "(assert (= (ite true x y) x))");
     223                 :          1 :   tryGoodInput(";; nothing but a comment");
     224                 :          1 :   tryGoodInput("; a comment\n(check-sat ; goodbye\n)");
     225                 :          1 : }
     226                 :            : 
     227                 :          4 : TEST_F(TestParserBlackSmt2InputParser, bad_inputs)
     228                 :            : {
     229                 :            :   // competition builds don't do any checking
     230                 :            : #ifndef CVC5_COMPETITION_MODE
     231                 :            :   // no arguments
     232                 :          1 :   tryBadInput("(assert)");
     233                 :            :   // illegal character in symbol
     234                 :          1 :   tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
     235                 :            :   // check-sat should not have an argument
     236                 :          1 :   tryBadInput("(set-logic QF_UF) (check-sat true)", true);
     237                 :            :   // no argument
     238                 :          1 :   tryBadInput("(declare-sort a)");
     239                 :            :   // double declaration
     240                 :          1 :   tryBadInput("(declare-sort a 0) (declare-sort a 0)");
     241                 :            :   // should be "(declare-fun p () Bool)"
     242                 :          1 :   tryBadInput("(set-logic QF_UF) (declare-fun p Bool)");
     243                 :            :   // strict mode
     244                 :            :   // no set-logic, core theory symbol "true" undefined
     245                 :          1 :   tryBadInput("(assert true)", true);
     246                 :            :   // core theory symbol "Bool" undefined
     247                 :          1 :   tryBadInput("(declare-fun p Bool)", true);
     248                 :            : #endif
     249                 :          1 : }
     250                 :            : 
     251                 :          4 : TEST_F(TestParserBlackSmt2InputParser, ff_byte_not_eof)
     252                 :            : {
     253                 :          1 :   std::string ffByte(1, static_cast<char>(0xFF));
     254                 :          1 :   std::string input = "(set-logic QF_UF)\n";
     255                 :          1 :   input += "(set-info :notes |ff";
     256                 :          1 :   input += ffByte;
     257                 :          1 :   input += "name|)\n";
     258                 :          1 :   input += "; comment with ";
     259                 :          1 :   input += ffByte;
     260                 :          1 :   input += " byte here\n";
     261                 :          1 :   input += "(check-sat)\n";
     262                 :          1 :   tryGoodInput(input);
     263                 :          1 : }
     264                 :            : 
     265                 :          4 : TEST_F(TestParserBlackSmt2InputParser, good_exprs)
     266                 :            : {
     267                 :          1 :   tryGoodExpr("(and a b)");
     268                 :          1 :   tryGoodExpr("(or (and a b) c)");
     269                 :          1 :   tryGoodExpr("(=> (and (=> a b) a) b)");
     270                 :          1 :   tryGoodExpr("(and (= a b) (not a))");
     271                 :          1 :   tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))");
     272                 :          1 :   tryGoodExpr("(ite a (f x) y)");
     273                 :          1 :   tryGoodExpr("1");
     274                 :          1 :   tryGoodExpr("0");
     275                 :          1 :   tryGoodExpr("1.5");
     276                 :          1 :   tryGoodExpr("#xfab09c7");
     277                 :          1 :   tryGoodExpr("#b0001011");
     278                 :          1 :   tryGoodExpr("(* 5 1)");
     279                 :          1 : }
     280                 :            : 
     281                 :          4 : TEST_F(TestParserBlackSmt2InputParser, bad_exprs)
     282                 :            : {
     283                 :            : // competition builds don't do any checking
     284                 :            : #ifndef CVC5_COMPETITION_MODE
     285                 :          1 :   tryBadExpr("(and)");                     // wrong arity
     286                 :          1 :   tryBadExpr("(and a b");                  // no closing paren
     287                 :          1 :   tryBadExpr("(a and b)");                 // infix
     288                 :          1 :   tryBadExpr("(implies a b)");             // no implies in v2
     289                 :          1 :   tryBadExpr("(iff a b)");                 // no iff in v2
     290                 :          1 :   tryBadExpr("(OR (AND a b) c)");          // wrong case
     291                 :          1 :   tryBadExpr("(a IMPLIES b)");             // infix AND wrong case
     292                 :          1 :   tryBadExpr("(not a b)");                 // wrong arity
     293                 :          1 :   tryBadExpr("not a");                     // needs parens
     294                 :          1 :   tryBadExpr("(ite a x)");                 // wrong arity
     295                 :          1 :   tryBadExpr("(if_then_else a (f x) y)");  // no if_then_else in v2
     296                 :          1 :   tryBadExpr("(a b)");                     // using non-function as function
     297                 :          1 :   tryBadExpr(".5");  // rational constants must have integer prefix
     298                 :          1 :   tryBadExpr("1.");  // rational constants must have fractional suffix
     299                 :          1 :   tryBadExpr("#x");  // hex constants must have at least one digit
     300                 :          1 :   tryBadExpr("#b");  // ditto binary constants
     301                 :          1 :   tryBadExpr("#xg0f");
     302                 :          1 :   tryBadExpr("#b9");
     303                 :            :   // Bad strict exprs
     304                 :          1 :   tryBadExpr("(and a)", true);   // no unary and's
     305                 :          1 :   tryBadExpr("(or a)", true);    // no unary or's
     306                 :          1 :   tryBadExpr("(* 5 01)", true);  // '01' is not a valid integer constant
     307                 :            : #endif
     308                 :          1 : }
     309                 :            : }  // namespace test
     310                 :            : }  // namespace cvc5::internal