From 627628cd06fc5b19fe59c95b3cb4073d85a8dfab Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 3 Oct 2014 18:05:31 -0400 Subject: [PATCH] Fix native language parsing of chained-store expressions (resolves bug 585). Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic. --- src/parser/cvc/Cvc.g | 87 +++++++++---------- test/regress/regress0/Makefile.am | 5 +- test/regress/regress0/arrays/Makefile.am | 3 +- .../regress0/arrays/parsing_ringer.cvc | 59 +++++++++++++ test/regress/regress0/bug585.cvc | 9 ++ 5 files changed, 116 insertions(+), 47 deletions(-) create mode 100644 test/regress/regress0/arrays/parsing_ringer.cvc create mode 100644 test/regress/regress0/bug585.cvc diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 347759c9a..79db2b629 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1454,18 +1454,6 @@ comparisonBinop[unsigned& op] | MEMBER_TOK ; -term[CVC4::Expr& f] -@init { - std::vector expressions; - std::vector operators; - unsigned op; - Type t; -} - : storeTerm[f] { expressions.push_back(f); } - ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } - ; - arithmeticBinop[unsigned& op] @init { op = LT(1)->getType(LT(1)); @@ -1479,14 +1467,26 @@ arithmeticBinop[unsigned& op] | EXP_TOK ; +moreArrayStores[CVC4::Expr& f] + : COMMA arrayStore[f] + ; + /** Parses an array/tuple/record assignment term. */ -storeTerm[CVC4::Expr& f] +term[CVC4::Expr& f] +@init { + std::vector expressions; + std::vector operators; + unsigned op; + Type t; +} : uminusTerm[f] ( WITH_TOK ( arrayStore[f] ( COMMA arrayStore[f] )* | DOT ( tupleStore[f] ( COMMA DOT tupleStore[f] )* | recordStore[f] ( COMMA DOT recordStore[f] )* ) ) - | /* nothing */ + | { expressions.push_back(f); } + ( arithmeticBinop[op] uminusTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ) ; @@ -1496,28 +1496,15 @@ storeTerm[CVC4::Expr& f] */ arrayStore[CVC4::Expr& f] @init { - Expr f2, f3; - std::vector dims; + Expr f2, k; } - : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ - ASSIGN_TOK uminusTerm[f3] - { assert(dims.size() >= 1); - // these loops are a bit complicated; they're only used for the - // multidimensional ...WITH [a][b] :=... syntax - for(unsigned i = 0; i < dims.size() - 1; ++i) { - f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]); - } - // a[i][j][k] := v turns into - // store(a, i, store(a[i], j, store(a[i][j], k, v))) - for(unsigned i = dims.size() - 1; i > 0; --i) { - f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3); - // strip off one layer of the select - f = f[0]; - } - - // outermost wrapping - f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3); - } + : LBRACKET formula[k] RBRACKET + { f2 = MK_EXPR(CVC4::kind::SELECT, f, k); } + ( ( arrayStore[f2] + | DOT ( tupleStore[f2] + | recordStore[f2] ) ) + | ASSIGN_TOK term[f2] ) + { f = MK_EXPR(CVC4::kind::STORE, f, k, f2); } ; /** @@ -1528,9 +1515,8 @@ tupleStore[CVC4::Expr& f] @init { Expr f2; } - : k=numeral ASSIGN_TOK uminusTerm[f2] - { - Type t = f.getType(); + : k=numeral + { Type t = f.getType(); if(! t.isTuple()) { PARSER_STATE->parseError("tuple-update applied to non-tuple"); } @@ -1540,8 +1526,13 @@ tupleStore[CVC4::Expr& f] ss << "tuple is of length " << length << "; cannot update index " << k; PARSER_STATE->parseError(ss.str()); } - f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2); + f2 = MK_EXPR(MK_CONST(TupleSelect(k)), f); } + ( ( arrayStore[f2] + | DOT ( tupleStore[f2] + | recordStore[f2] ) ) + | ASSIGN_TOK term[f2] ) + { f = MK_EXPR(MK_CONST(TupleUpdate(k)), f, f2); } ; /** @@ -1553,19 +1544,27 @@ recordStore[CVC4::Expr& f] std::string id; Expr f2; } - : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2] - { - Type t = f.getType(); + : identifier[id,CHECK_NONE,SYM_VARIABLE] + { Type t = f.getType(); if(! t.isRecord()) { - PARSER_STATE->parseError("record-update applied to non-record"); + std::stringstream ss; + ss << "record-update applied to non-record term" << std::endl + << "the term: " << f << std::endl + << "its type: " << t; + PARSER_STATE->parseError(ss.str()); } const Record& rec = RecordType(t).getRecord(); Record::const_iterator fld = rec.find(id); if(fld == rec.end()) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2); + f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f); } + ( ( arrayStore[f2] + | DOT ( tupleStore[f2] + | recordStore[f2] ) ) + | ASSIGN_TOK term[f2] ) + { f = MK_EXPR(MK_CONST(RecordUpdate(id)), f, f2); } ; /** Parses a unary minus term. */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5e57e9b67..128783388 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -163,9 +163,10 @@ BUG_TESTS = \ bug567.smt2 \ bug576.smt2 \ bug576a.smt2 \ - bug578.smt2 + bug578.smt2 \ + bug585.cvc -TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) +TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # bug512 -- taking too long, --time-per not working perhaps? in any case, # we have a minimized version still getting tested diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 345856d85..c11d68780 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -39,7 +39,8 @@ TESTS = \ incorrect11.smt \ swap_t1_np_nf_ai_00005_007.cvc.smt \ x2.smt \ - x3.smt + x3.smt \ + parsing_ringer.cvc EXTRA_DIST = $(TESTS) \ bug272.smt \ diff --git a/test/regress/regress0/arrays/parsing_ringer.cvc b/test/regress/regress0/arrays/parsing_ringer.cvc new file mode 100644 index 000000000..c9f8c9e22 --- /dev/null +++ b/test/regress/regress0/arrays/parsing_ringer.cvc @@ -0,0 +1,59 @@ +% Test for presentiation language parsing, some edge cases with cascading +% store terms. Intended to put this part of the parser "through the ringer," +% hence the name. + +% COMMAND-LINE: --incremental +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat +% EXPECT: sat + +PUSH; + +x, y : ARRAY INT OF ARRAY INT OF ARRAY INT OF INT; + +% multidimensional arrays +ASSERT x[0][0][0] = 0; %% select +ASSERT y = x WITH [0][0][1] := 1; %% partial store + +CHECKSAT; + +% mixed stores: records of arrays of tuples, oh my +z : [# x:ARRAY INT OF [# x:INT #], y:[ARRAY INT OF INT, ARRAY INT OF INT] #]; + +arr1 : ARRAY INT OF [# x:INT #]; +arr2 : [ ARRAY INT OF INT, ARRAY INT OF INT ]; + +ASSERT arr1[0].x = 0; +ASSERT arr2.0[0] = 1; +ASSERT arr2.1[0] = 5; + +ASSERT z.y.1[1] /= 1; +ASSERT (# x:=arr1, y:=arr2 #) = z; + +CHECKSAT; + +ASSERT z.x[0].x /= z.y.0[5]; + +CHECKSAT; + +ASSERT z.y.0[1] = z.x[5].x; + +CHECKSAT; + +ASSERT z.y.0[5] = z.x[-2].x; + +CHECKSAT; + +POP; + +a : ARRAY INT OF ARRAY INT OF INT; +b : ARRAY INT OF INT; + +% ambiguity in presentation language, comma needs to bind to innermost WITH +% causes type error if the [2]:=2 at the end is attached to the wrong WITH +ASSERT a = a WITH [0]:=b WITH [1]:=1,[2]:=2; + +CHECKSAT; diff --git a/test/regress/regress0/bug585.cvc b/test/regress/regress0/bug585.cvc new file mode 100644 index 000000000..825cb0003 --- /dev/null +++ b/test/regress/regress0/bug585.cvc @@ -0,0 +1,9 @@ +% EXPECT: sat + +Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #]; +State: TYPE = [# pc: INT, cache: Cache #]; + +s0: State; +s1: State = s0 WITH .cache[10].data := 2/3; + +CHECKSAT; -- 2.30.2