GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/parser/parser_black.cpp Lines: 206 206 100.0 %
Date: 2021-03-23 Branches: 342 786 43.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file parser_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Christopher L. Conway, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::parser::Parser for CVC and SMT-LIBv2
13
 ** inputs.
14
 **
15
 ** Black box testing of CVC4::parser::Parser for CVC and SMT-LIbv2 inputs.
16
 **/
17
18
#include <sstream>
19
20
#include "api/cvc4cpp.h"
21
#include "base/output.h"
22
#include "expr/symbol_manager.h"
23
#include "options/base_options.h"
24
#include "options/language.h"
25
#include "options/options.h"
26
#include "parser/parser.h"
27
#include "parser/parser_builder.h"
28
#include "parser/smt2/smt2.h"
29
#include "smt/command.h"
30
#include "test.h"
31
32
namespace CVC4 {
33
34
using namespace parser;
35
using namespace language::input;
36
37
namespace test {
38
39
class TestParserBlackParser : public TestInternal
40
{
41
 protected:
42
16
  TestParserBlackParser(InputLanguage lang) : d_lang(lang) {}
43
44
16
  virtual ~TestParserBlackParser() {}
45
46
16
  void SetUp() override
47
  {
48
16
    TestInternal::SetUp();
49
32
    d_options.set(options::parseOnly, true);
50
16
    d_symman.reset(nullptr);
51
16
    d_solver.reset(new CVC4::api::Solver(&d_options));
52
16
  }
53
54
16
  void TearDown() override
55
  {
56
16
    d_symman.reset(nullptr);
57
16
    d_solver.reset(nullptr);
58
16
  }
59
60
  void setUp()
61
  {
62
    /* ensure the old symbol manager is deleted */
63
    d_symman.reset(nullptr);
64
    d_solver.reset(new api::Solver(&d_options));
65
  }
66
67
  /* Set up declaration context for expr inputs */
68
76
  void setupContext(Parser& parser)
69
  {
70
    /* a, b, c: BOOLEAN */
71
76
    parser.bindVar("a", d_solver.get()->getBooleanSort());
72
76
    parser.bindVar("b", d_solver.get()->getBooleanSort());
73
76
    parser.bindVar("c", d_solver.get()->getBooleanSort());
74
    /* t, u, v: TYPE */
75
152
    api::Sort t = parser.mkSort("t");
76
152
    api::Sort u = parser.mkSort("u");
77
152
    api::Sort v = parser.mkSort("v");
78
    /* f : t->u; g: u->v; h: v->t; */
79
76
    parser.bindVar("f", d_solver.get()->mkFunctionSort(t, u));
80
76
    parser.bindVar("g", d_solver.get()->mkFunctionSort(u, v));
81
76
    parser.bindVar("h", d_solver.get()->mkFunctionSort(v, t));
82
    /* x:t; y:u; z:v; */
83
76
    parser.bindVar("x", t);
84
76
    parser.bindVar("y", u);
85
76
    parser.bindVar("z", v);
86
76
  }
87
88
72
  void tryGoodInput(const std::string goodInput)
89
  {
90
72
    d_symman.reset(new SymbolManager(d_solver.get()));
91
144
    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
92
72
                         .withStringInput(goodInput)
93
72
                         .withOptions(d_options)
94
72
                         .withInputLanguage(d_lang)
95
72
                         .build();
96
72
    ASSERT_FALSE(parser->done());
97
    Command* cmd;
98
356
    while ((cmd = parser->nextCommand()) != NULL)
99
    {
100
142
      Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
101
142
      delete cmd;
102
    }
103
104
72
    ASSERT_TRUE(parser->done());
105
72
    delete parser;
106
  }
107
108
60
  void tryBadInput(const std::string badInput, bool strictMode = false)
109
  {
110
60
    d_symman.reset(new SymbolManager(d_solver.get()));
111
120
    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
112
60
                         .withStringInput(badInput)
113
60
                         .withOptions(d_options)
114
60
                         .withInputLanguage(d_lang)
115
60
                         .withStrictMode(strictMode)
116
60
                         .build();
117
60
    ASSERT_THROW(
118
        {
119
          Command* cmd;
120
          while ((cmd = parser->nextCommand()) != NULL)
121
          {
122
            Debug("parser") << "Parsed command: " << (*cmd) << std::endl;
123
            delete cmd;
124
          }
125
          std::cout << "\nBad input succeeded:\n" << badInput << std::endl;
126
        },
127
60
        ParserException);
128
60
    delete parser;
129
  }
130
131
34
  void tryGoodExpr(const std::string goodExpr)
132
  {
133
34
    d_symman.reset(new SymbolManager(d_solver.get()));
134
68
    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
135
34
                         .withStringInput(goodExpr)
136
34
                         .withOptions(d_options)
137
34
                         .withInputLanguage(d_lang)
138
34
                         .build();
139
140
34
    if (d_lang == LANG_SMTLIB_V2)
141
    {
142
      /* Use QF_LIA to make multiplication ("*") available */
143
      std::unique_ptr<Command> cmd(
144
24
          static_cast<Smt2*>(parser)->setLogic("QF_LIA"));
145
    }
146
147
34
    ASSERT_FALSE(parser->done());
148
34
    setupContext(*parser);
149
34
    ASSERT_FALSE(parser->done());
150
68
    api::Term e = parser->nextExpression();
151
34
    ASSERT_FALSE(e.isNull());
152
34
    e = parser->nextExpression();
153
34
    ASSERT_TRUE(parser->done());
154
34
    ASSERT_TRUE(e.isNull());
155
34
    delete parser;
156
  }
157
158
  /**
159
   * NOTE: The check implemented here may fail if a bad expression
160
   * expression string has a prefix that is parseable as a good
161
   * expression. E.g., the bad SMT v2 expression "#b10@@@@@@" will
162
   * actually return the bit-vector 10 and ignore the tail of the
163
   * input. It's more trouble than it's worth to check that the whole
164
   * input was consumed here, so just be careful to avoid valid
165
   * prefixes in tests.
166
   */
167
42
  void tryBadExpr(const std::string badExpr, bool strictMode = false)
168
  {
169
42
    d_symman.reset(new SymbolManager(d_solver.get()));
170
84
    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
171
42
                         .withStringInput(badExpr)
172
42
                         .withOptions(d_options)
173
42
                         .withInputLanguage(d_lang)
174
42
                         .withStrictMode(strictMode)
175
42
                         .build();
176
42
    setupContext(*parser);
177
42
    ASSERT_FALSE(parser->done());
178
42
    ASSERT_THROW(api::Term e = parser->nextExpression();
179
                 std::cout << std::endl
180
                           << "Bad expr succeeded." << std::endl
181
                           << "Input: <<" << badExpr << ">>" << std::endl
182
                           << "Output: <<" << e << ">>" << std::endl;
183
42
                 , ParserException);
184
42
    delete parser;
185
  }
186
187
  Options d_options;
188
  InputLanguage d_lang;
189
  std::unique_ptr<CVC4::api::Solver> d_solver;
190
  std::unique_ptr<SymbolManager> d_symman;
191
};
192
193
/* -------------------------------------------------------------------------- */
194
195
8
class TestParserBlackCvCParser : public TestParserBlackParser
196
{
197
 protected:
198
8
  TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC4) {}
199
};
200
201
17
TEST_F(TestParserBlackCvCParser, good_inputs)
202
{
203
2
  tryGoodInput("");   // empty string is OK
204
2
  tryGoodInput(";");  // no command is OK
205
2
  tryGoodInput("ASSERT TRUE;");
206
2
  tryGoodInput("QUERY TRUE;");
207
2
  tryGoodInput("CHECKSAT FALSE;");
208
2
  tryGoodInput("a, b : BOOLEAN;");
209
2
  tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;");
210
2
  tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;");
211
2
  tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
212
2
  tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];");
213
2
  tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;");
214
2
  tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;");
215
2
  tryGoodInput(
216
      "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;");
217
2
  tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;");
218
2
  tryGoodInput("%% nothing but a comment");
219
2
  tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
220
2
  tryGoodInput("a : BOOLEAN; a: BOOLEAN;");  // double decl, but compatible
221
2
  tryGoodInput("a : INT = 5; a: INT;");      // decl after define, compatible
222
2
  tryGoodInput(
223
      "a : TYPE; a : INT;");  // ok, sort and variable symbol spaces distinct
224
2
  tryGoodInput(
225
      "a : TYPE; a : INT; b : a;");  // ok except a is both INT and sort `a'
226
2
  tryGoodInput(
227
      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null "
228
      "END;");
229
2
  tryGoodInput(
230
      "DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil "
231
      "END;");
232
2
  tryGoodInput(
233
      "DATATYPE trex = Foo | Bar END; DATATYPE tree = "
234
      "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list "
235
      "OF tree,cdr:BITVECTOR(32)) END;");
236
2
}
237
238
17
TEST_F(TestParserBlackCvCParser, bad_inputs)
239
{
240
// competition builds don't do any checking
241
#ifndef CVC4_COMPETITION_MODE
242
2
  tryBadInput("ASSERT;");  // no args
243
2
  tryBadInput("QUERY");
244
2
  tryBadInput("CHECKSAT");
245
2
  tryBadInput("a, b : boolean;");  // lowercase boolean isn't a type
246
2
  tryBadInput("0x : INT;");        // 0x isn't an identifier
247
2
  tryBadInput(
248
      "a, b : BOOLEAN\nQUERY (a => b) AND a => b;");  // no semicolon after decl
249
2
  tryBadInput("ASSERT 0bin012 /= 0hex0;");            // bad binary literal
250
2
  tryBadInput("a, b: BOOLEAN; QUERY a(b);");  // non-function used as function
251
2
  tryBadInput("a : BOOLEAN; a: INT;");        // double decl, incompatible
252
2
  tryBadInput("A : TYPE; A: TYPE;");          // types can't be double-declared
253
2
  tryBadInput("a : INT; a: INT = 5;");        // can't define after decl
254
2
  tryBadInput("a : INT = 5; a: BOOLEAN;");    // decl w/ incompatible type
255
2
  tryBadInput(
256
      "a : TYPE; a : INT; a : a;");  // ok except a is both INT and sort `a'
257
2
  tryBadInput(
258
      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | "
259
      "cons(car:INT,cdr:list) END;");
260
2
  tryBadInput(
261
      "DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil "
262
      "END;");
263
2
  tryBadInput(
264
      "DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = "
265
      "cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
266
#endif
267
2
}
268
269
17
TEST_F(TestParserBlackCvCParser, good_exprs)
270
{
271
2
  tryGoodExpr("a AND b");
272
2
  tryGoodExpr("a AND b OR c");
273
2
  tryGoodExpr("(a => b) AND a => b");
274
2
  tryGoodExpr("(a <=> b) AND (NOT a)");
275
2
  tryGoodExpr("(a XOR b) <=> (a OR b) AND (NOT (a AND b))");
276
2
}
277
278
17
TEST_F(TestParserBlackCvCParser, bad_exprs)
279
{
280
// competition builds don't do any checking
281
#ifndef CVC4_COMPETITION_MODE
282
2
  tryBadInput("a AND");             // wrong arity
283
2
  tryBadInput("AND(a,b)");          // not infix
284
2
  tryBadInput("(OR (AND a b) c)");  // not infix
285
2
  tryBadInput("a IMPLIES b");       // should be =>
286
2
  tryBadInput("a NOT b");           // wrong arity, not infix
287
2
  tryBadInput("a and b");           // wrong case
288
#endif
289
2
}
290
291
/* -------------------------------------------------------------------------- */
292
293
8
class TestParserBlackSmt2Parser : public TestParserBlackParser
294
{
295
 protected:
296
8
  TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {}
297
};
298
299
17
TEST_F(TestParserBlackSmt2Parser, good_inputs)
300
{
301
2
  tryGoodInput("");  // empty string is OK
302
2
  tryGoodInput("(set-logic QF_UF)");
303
2
  tryGoodInput("(set-info :notes |This is a note, take note!|)");
304
2
  tryGoodInput("(set-logic QF_UF) (assert true)");
305
2
  tryGoodInput("(check-sat)");
306
2
  tryGoodInput("(exit)");
307
2
  tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
308
2
  tryGoodInput(
309
      "(set-logic QF_UF) (declare-fun a () Bool) "
310
      "(declare-fun b () Bool)");
311
2
  tryGoodInput(
312
      "(set-logic QF_UF) (declare-fun a () Bool) "
313
      "(declare-fun b () Bool) (assert (=> (and (=> a b) a) b))");
314
2
  tryGoodInput(
315
      "(set-logic QF_UF) (declare-sort a 0) "
316
      "(declare-fun f (a) a) (declare-fun x () a) "
317
      "(assert (= (f x) x))");
318
2
  tryGoodInput(
319
      "(set-logic QF_UF) (declare-sort a 0) "
320
      "(declare-fun x () a) (declare-fun y () a) "
321
      "(assert (= (ite true x y) x))");
322
2
  tryGoodInput(";; nothing but a comment");
323
2
  tryGoodInput("; a comment\n(check-sat ; goodbye\n)");
324
2
}
325
326
17
TEST_F(TestParserBlackSmt2Parser, bad_inputs)
327
{
328
  // competition builds don't do any checking
329
#ifndef CVC4_COMPETITION_MODE
330
  // no arguments
331
2
  tryBadInput("(assert)");
332
  // illegal character in symbol
333
2
  tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
334
  // check-sat should not have an argument
335
2
  tryBadInput("(set-logic QF_UF) (check-sat true)", true);
336
  // no argument
337
2
  tryBadInput("(declare-sort a)");
338
  // double declaration
339
2
  tryBadInput("(declare-sort a 0) (declare-sort a 0)");
340
  // should be "(declare-fun p () Bool)"
341
2
  tryBadInput("(set-logic QF_UF) (declare-fun p Bool)");
342
  // strict mode
343
  // no set-logic, core theory symbol "true" undefined
344
2
  tryBadInput("(assert true)", true);
345
  // core theory symbol "Bool" undefined
346
2
  tryBadInput("(declare-fun p Bool)", true);
347
#endif
348
2
}
349
350
17
TEST_F(TestParserBlackSmt2Parser, good_exprs)
351
{
352
2
  tryGoodExpr("(and a b)");
353
2
  tryGoodExpr("(or (and a b) c)");
354
2
  tryGoodExpr("(=> (and (=> a b) a) b)");
355
2
  tryGoodExpr("(and (= a b) (not a))");
356
2
  tryGoodExpr("(= (xor a b) (and (or a b) (not (and a b))))");
357
2
  tryGoodExpr("(ite a (f x) y)");
358
2
  tryGoodExpr("1");
359
2
  tryGoodExpr("0");
360
2
  tryGoodExpr("1.5");
361
2
  tryGoodExpr("#xfab09c7");
362
2
  tryGoodExpr("#b0001011");
363
2
  tryGoodExpr("(* 5 1)");
364
2
}
365
366
17
TEST_F(TestParserBlackSmt2Parser, bad_exprs)
367
{
368
// competition builds don't do any checking
369
#ifndef CVC4_COMPETITION_MODE
370
2
  tryBadExpr("(and)");                     // wrong arity
371
2
  tryBadExpr("(and a b");                  // no closing paren
372
2
  tryBadExpr("(a and b)");                 // infix
373
2
  tryBadExpr("(implies a b)");             // no implies in v2
374
2
  tryBadExpr("(iff a b)");                 // no iff in v2
375
2
  tryBadExpr("(OR (AND a b) c)");          // wrong case
376
2
  tryBadExpr("(a IMPLIES b)");             // infix AND wrong case
377
2
  tryBadExpr("(not a b)");                 // wrong arity
378
2
  tryBadExpr("not a");                     // needs parens
379
2
  tryBadExpr("(ite a x)");                 // wrong arity
380
2
  tryBadExpr("(if_then_else a (f x) y)");  // no if_then_else in v2
381
2
  tryBadExpr("(a b)");                     // using non-function as function
382
2
  tryBadExpr(".5");  // rational constants must have integer prefix
383
2
  tryBadExpr("1.");  // rational constants must have fractional suffix
384
2
  tryBadExpr("#x");  // hex constants must have at least one digit
385
2
  tryBadExpr("#b");  // ditto binary constants
386
2
  tryBadExpr("#xg0f");
387
2
  tryBadExpr("#b9");
388
  // Bad strict exprs
389
2
  tryBadExpr("(and a)", true);   // no unary and's
390
2
  tryBadExpr("(or a)", true);    // no unary or's
391
2
  tryBadExpr("(* 5 01)", true);  // '01' is not a valid integer constant
392
#endif
393
2
}
394
}  // namespace test
395
43
}  // namespace CVC4