From 69bdf082f698ab304de8806bc1c50366ce7fedff Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 23 Mar 2011 05:45:36 +0000 Subject: [PATCH] Fix the SMTLIB1 to not accept badly formed input. Previously if a variable wasn't defined it'd be implicitly defined as a boolean. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1229 e59a4935-1847-0410-ae03-e826735625c1 --- src/parser/LetMgr.cpp | 7 +++++ src/parser/LetMgr.h | 8 +++++ src/parser/smt.lex | 39 ++++++++++++++++------- src/parser/smt.y | 72 +++++++++++++++++++------------------------ 4 files changed, 75 insertions(+), 51 deletions(-) diff --git a/src/parser/LetMgr.cpp b/src/parser/LetMgr.cpp index b75ef2b..ffb5054 100644 --- a/src/parser/LetMgr.cpp +++ b/src/parser/LetMgr.cpp @@ -37,9 +37,16 @@ namespace BEEV { "cannot redeclare as a letvar: v =", var); } + LetExprMgr(var.GetName(),letExpr); + }//end of LetExprMgr() + + void LETMgr::LetExprMgr(string name, const ASTNode& letExpr) + { + assert (_letid_expr_map->find(name) == _letid_expr_map->end()); (*_letid_expr_map)[name] = letExpr; }//end of LetExprMgr() + //this function looks up the "var to letexpr map" and returns the //corresponding letexpr. if there is no letexpr, then it simply //returns the var. diff --git a/src/parser/LetMgr.h b/src/parser/LetMgr.h index 51e3148..6455fba 100644 --- a/src/parser/LetMgr.h +++ b/src/parser/LetMgr.h @@ -70,10 +70,18 @@ namespace BEEV delete _letid_expr_map; } + // We know for sure that it's a let. + ASTNode resolveLet(const string s) + { + assert(isLetDeclared(s)); + return _letid_expr_map->find(s)->second; + } + ASTNode ResolveID(const ASTNode& var); //Functions that are used to manage LET expressions void LetExprMgr(const ASTNode& var, const ASTNode& letExpr); + void LetExprMgr(string name, const ASTNode& letExpr); //Delete Letid Map. Called when we move onto the expression after (let ... ) void CleanupLetIDMap(void); diff --git a/src/parser/smt.lex b/src/parser/smt.lex index 4fa24b7..c223332 100644 --- a/src/parser/smt.lex +++ b/src/parser/smt.lex @@ -220,17 +220,34 @@ bit{DIGIT}+ { "boolbv" { return BOOL_TO_BV_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(smttext); - - // Check valuesize to see if it's a prop var. I don't like doing - // type determination in the lexer, but it's easier than rewriting - // the whole grammar to eliminate the term/formula distinction. - smtlval.node = new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr)); - //smtlval.node = new BEEV::ASTNode(nptr); - if ((smtlval.node)->GetType() == BOOLEAN_TYPE) - return FORMID_TOK; - else - return TERMID_TOK; + string str(smttext); + bool found = false; + ASTNode nptr; + + if (BEEV::parserInterface->isSymbolAlreadyDeclared(str)) // it's a symbol. + { + nptr= BEEV::parserInterface->LookupOrCreateSymbol(str); + found = true; + } + else if (BEEV::parserInterface->letMgr.isLetDeclared(str)) // a let. + { + nptr= BEEV::parserInterface->letMgr.resolveLet(str); + found = true; + } + + if (found) + { + smtlval.node = BEEV::parserInterface->newNode(nptr); + if ((smtlval.node)->GetType() == BEEV::BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; + } + + // It hasn't been found. So it's not already declared. + // it has not been seen before. + smtlval.str = new std::string(str); + return STRING_TOK; } . { smterror("Illegal input character."); } %% diff --git a/src/parser/smt.y b/src/parser/smt.y index 37e38b5..ed37d52 100644 --- a/src/parser/smt.y +++ b/src/parser/smt.y @@ -91,11 +91,11 @@ %type status %type bench_attributes an_formulas an_terms -%type benchmark bench_name bench_attribute +%type benchmark bench_attribute %type an_term an_nonbvconst_term an_formula -%type var fvar logic_name -%type user_value +%type var fvar +%type user_value logic_name bench_name %token NUMERAL_TOK %token BVCONST_TOK @@ -254,7 +254,7 @@ LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK ; bench_name: -FORMID_TOK +STRING_TOK { } ; @@ -303,10 +303,10 @@ COLON_TOK ASSUMPTION_TOK an_formula } | COLON_TOK LOGIC_TOK logic_name { - if (!(0 == strcmp($3->GetName(),"QF_UFBV") || - 0 == strcmp($3->GetName(),"QF_BV") || - //0 == strcmp($3->GetName(),"QF_UF") || - 0 == strcmp($3->GetName(),"QF_AUFBV"))) { + if (!(0 == strcmp($3->c_str(),"QF_UFBV") || + 0 == strcmp($3->c_str(),"QF_BV") || + //0 == strcmp($3->c_str(),"QF_UF") || + 0 == strcmp($3->c_str(),"QF_AUFBV"))) { yyerror("Wrong input logic:"); } delete $3; @@ -327,11 +327,11 @@ COLON_TOK ASSUMPTION_TOK an_formula ; logic_name: -FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +STRING_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK { $$ = $1; } -| FORMID_TOK +| STRING_TOK { $$ = $1; } @@ -405,34 +405,37 @@ sort_symb } ; +// There are some gulwani benchmarks that create multiple variables in the same header. +// Maybe you shouldn'.t.. var_decls: var_decl -{ -} -// | LPAREN_TOK var_decl RPAREN_TOK +{} | var_decls var_decl -{ -} +{} ; + + var_decl: -LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK +LPAREN_TOK STRING_TOK sort_symbs RPAREN_TOK { - parserInterface->letMgr._parser_symbol_table.insert(*$2); + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str()); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var - $2->SetIndexWidth($3.indexwidth); - $2->SetValueWidth($3.valuewidth); + s.SetIndexWidth($3.indexwidth); + s.SetValueWidth($3.valuewidth); + parserInterface->letMgr._parser_symbol_table.insert(s); delete $2; } -| LPAREN_TOK FORMID_TOK RPAREN_TOK +| LPAREN_TOK STRING_TOK RPAREN_TOK { - parserInterface->letMgr._parser_symbol_table.insert(*$2); + ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($2->c_str()); + s.SetIndexWidth(0); + s.SetValueWidth(0); + parserInterface->letMgr._parser_symbol_table.insert(s); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var - $2->SetIndexWidth(0); - $2->SetValueWidth(0); delete $2; } ; @@ -627,13 +630,8 @@ TRUE_TOK ; letexpr_mgmt: -LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK +LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK STRING_TOK an_term RPAREN_TOK { - - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); - //populate the hashtable from LET-var --> //LET-exprs and then process them: // @@ -647,14 +645,8 @@ LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK delete $5; delete $6; } -| LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK +| LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK STRING_TOK an_formula RPAREN_TOK { - //Expr must typecheck - - //set the valuewidth of the identifier - $5->SetValueWidth($6->GetValueWidth()); - $5->SetIndexWidth($6->GetIndexWidth()); - //Do LET-expr management parserInterface->letMgr.LetExprMgr(*$5,*$6); delete $5; @@ -702,7 +694,7 @@ an_nonbvconst_term: BITCONST_TOK { $$ = $1; } | var { - $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + $$ = new ASTNode((*$1)); delete $1; } | LPAREN_TOK an_term RPAREN_TOK @@ -1096,12 +1088,12 @@ BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK var: FORMID_TOK { - $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + $$ = new ASTNode((*$1)); delete $1; } | TERMID_TOK { - $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + $$ = new ASTNode((*$1)); delete $1; } | QUESTION_TOK TERMID_TOK @@ -1117,7 +1109,7 @@ DOLLAR_TOK FORMID_TOK } | FORMID_TOK { - $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + $$ = new ASTNode((*$1)); delete $1; } ; -- 2.47.3