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-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 : : * 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 : 66 : 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 : 66 : Command cmd;
74 : 66 : 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 : : }
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 : : ParserException);
138 : : }
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 : : }
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 : : , ParserException);
185 : : }
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 : 2 : 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 : 2 : 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 : 2 : 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 : 2 : 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
|
