Branch data     Line data    Source code

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