diff options
Diffstat (limited to 'stp/parser')
| -rw-r--r-- | stp/parser/Makefile | 27 | ||||
| -rw-r--r-- | stp/parser/PL.lex | 128 | ||||
| -rw-r--r-- | stp/parser/PL.y | 1006 | ||||
| -rw-r--r-- | stp/parser/let-funcs.cpp | 85 | ||||
| -rw-r--r-- | stp/parser/main.cpp | 181 | ||||
| -rw-r--r-- | stp/parser/smtlib.lex | 232 | ||||
| -rw-r--r-- | stp/parser/smtlib.y | 1036 |
7 files changed, 2695 insertions, 0 deletions
diff --git a/stp/parser/Makefile b/stp/parser/Makefile new file mode 100644 index 00000000..8211c825 --- /dev/null +++ b/stp/parser/Makefile @@ -0,0 +1,27 @@ +include ../Makefile.common + +SRCS = lexPL.cpp parsePL.cpp let-funcs.cpp main.cpp +OBJS = $(SRCS:.cpp=.o) +LIBS = -L../AST -last -L../sat -lsatsolver -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv + +all: parser + +parser: lexPL.o parsePL.o let-funcs.o main.o + $(CXX) $(CFLAGS) $(LDFLAGS) lexPL.o parsePL.o main.o let-funcs.o $(LIBS) -o parser + +main.o: parsePL_defs.h + +lexPL.cpp: PL.lex parsePL_defs.h ../AST/AST.h + $(LEX) -o lexPL.cpp PL.lex + +parsePL_defs.h: y.tab.h + @cp y.tab.h parsePL_defs.h +parsePL.cpp: y.tab.c + @cp y.tab.c parsePL.cpp + +y.tab.c y.tab.h: PL.y + $(YACC) PL.y + + +clean: + rm -rf *.o parsePL_defs.h *~ lexPL.cpp parsePL.cpp *.output parser y.tab.* lex.yy.c .#* diff --git a/stp/parser/PL.lex b/stp/parser/PL.lex new file mode 100644 index 00000000..e9358a0e --- /dev/null +++ b/stp/parser/PL.lex @@ -0,0 +1,128 @@ +%{ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +#include <iostream> +#include "../AST/AST.h" +#include "parsePL_defs.h" + +extern char *yytext; +extern int yyerror (const char *msg); +%} + +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno +%x COMMENT +%x STRING_LITERAL +LETTER ([a-zA-Z]) +HEX ([0-9a-fA-F]) +BITS ([0-1]) +DIGIT ([0-9]) +OPCHAR (['?\_$]) +ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) +%% + +[()[\]{},.;:'!#?_=] { return yytext[0];} + +[\n] { /*Skip new line */ } +[ \t\r\f] { /* skip whitespace */ } +0b{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} +0bin{BITS}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} +0h{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} +0hex{HEX}+ { yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} +{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} + +"%" { BEGIN COMMENT;} +<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */} +<COMMENT>. { /* stay in comment mode */} + +"ARRAY" { return ARRAY_TOK; } +"OF" { return OF_TOK; } +"WITH" { return WITH_TOK; } +"AND" { return AND_TOK;} +"NAND" { return NAND_TOK;} +"NOR" { return NOR_TOK;} +"NOT" { return NOT_TOK; } +"OR" { return OR_TOK; } +"/=" { return NEQ_TOK; } + ":=" { return ASSIGN_TOK;} +"=>" { return IMPLIES_TOK; } +"<=>" { return IFF_TOK; } +"XOR" { return XOR_TOK; } +"IF" { return IF_TOK; } +"THEN" { return THEN_TOK; } +"ELSE" { return ELSE_TOK; } +"ELSIF" { return ELSIF_TOK; } +"END" { return END_TOK; } +"ENDIF" { return ENDIF_TOK; } +"BV" { return BV_TOK;} +"BITVECTOR" { return BV_TOK;} +"BOOLEAN" { return BOOLEAN_TOK;} +"<<" { return BVLEFTSHIFT_TOK;} +">>" { return BVRIGHTSHIFT_TOK;} +"BVPLUS" { return BVPLUS_TOK;} +"BVSUB" { return BVSUB_TOK;} +"BVUMINUS" { return BVUMINUS_TOK;} +"BVMULT" { return BVMULT_TOK;} +"BVDIV" { return BVDIV_TOK;} +"BVMOD" { return BVMOD_TOK;} +"SBVDIV" { return SBVDIV_TOK;} +"SBVMOD" { return SBVMOD_TOK;} +"~" { return BVNEG_TOK;} +"&" { return BVAND_TOK;} +"|" { return BVOR_TOK;} +"BVXOR" { return BVXOR_TOK;} +"BVNAND" { return BVNAND_TOK;} +"BVNOR" { return BVNOR_TOK;} +"BVXNOR" { return BVXNOR_TOK;} +"@" { return BVCONCAT_TOK;} +"BVLT" { return BVLT_TOK;} +"BVGT" { return BVGT_TOK;} +"BVLE" { return BVLE_TOK;} +"BVGE" { return BVGE_TOK;} +"BVSLT" { return BVSLT_TOK;} +"BVSGT" { return BVSGT_TOK;} +"BVSLE" { return BVSLE_TOK;} +"BVSGE" { return BVSGE_TOK;} +"BVSX" { return BVSX_TOK;} +"SBVLT" { return BVSLT_TOK;} +"SBVGT" { return BVSGT_TOK;} +"SBVLE" { return BVSLE_TOK;} +"SBVGE" { return BVSGE_TOK;} +"SX" { return BVSX_TOK;} +"BOOLEXTRACT" { return BOOLEXTRACT_TOK;} +"BOOLBV" { return BOOL_TO_BV_TOK;} +"ASSERT" { return ASSERT_TOK; } +"QUERY" { return QUERY_TOK; } +"FALSE" { return FALSELIT_TOK;} +"TRUE" { return TRUELIT_TOK;} +"IN" { return IN_TOK;} +"LET" { return LET_TOK;} +"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK;} +"COUNTERMODEL" { return COUNTEREXAMPLE_TOK;} + "PUSH" { return PUSH_TOK;} + "POP" { return POP_TOK;} + +(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { + BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); + + // 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. + yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + //yylval.node = new BEEV::ASTNode(nptr); + if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; +} + +. { yyerror("Illegal input character."); } +%% diff --git a/stp/parser/PL.y b/stp/parser/PL.y new file mode 100644 index 00000000..aa58aa4c --- /dev/null +++ b/stp/parser/PL.y @@ -0,0 +1,1006 @@ +%{ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "../AST/AST.h" +using namespace std; + + // Suppress the bogus warning suppression in bison (it generates + // compile error) +#undef __GNUC_MINOR__ + + extern int yylex(void); + extern char* yytext; + extern int yylineno; + int yyerror(const char *s) { + cout << "syntax error: line " << yylineno << "\n" << s << endl; + BEEV::FatalError(""); + return 1; /* Dill: don't know what it should return */ + }; + +#define YYLTYPE_IS_TRIVIAL 1 +#define YYMAXDEPTH 10485760 +#define YYERROR_VERBOSE 1 +#define YY_EXIT_FAILURE -1 +%} + +%union { + + unsigned int uintval; /* for numerals in types. */ + struct { + //stores the indexwidth and valuewidth + //indexwidth is 0 iff type is bitvector. positive iff type is + //array, and stores the width of the indexing bitvector + unsigned int indexwidth; + //width of the bitvector type + unsigned int valuewidth; + } indexvaluewidth; + + //ASTNode,ASTVec + BEEV::ASTNode *node; + BEEV::ASTVec *vec; + + //Hash_Map to hold Array Updates during parse A map from array index + //to array values. To support the WITH construct + BEEV::ASTNodeMap * Index_To_UpdateValue; +}; + +%start cmd + +%token AND_TOK "AND" +%token OR_TOK "OR" +%token NOT_TOK "NOT" +%token XOR_TOK "XOR" +%token NAND_TOK "NAND" +%token NOR_TOK "NOR" +%token IMPLIES_TOK "=>" +%token IFF_TOK "<=>" + +%token IF_TOK "IF" +%token THEN_TOK "THEN" +%token ELSE_TOK "ELSE" +%token ELSIF_TOK "ELSIF" +%token END_TOK "END" +%token ENDIF_TOK "ENDIF" +%token NEQ_TOK "/=" +%token ASSIGN_TOK ":=" + +%token BV_TOK "BV" +%token BVLEFTSHIFT_TOK "<<" +%token BVRIGHTSHIFT_TOK ">>" +%token BVPLUS_TOK "BVPLUS" +%token BVSUB_TOK "BVSUB" +%token BVUMINUS_TOK "BVUMINUS" +%token BVMULT_TOK "BVMULT" + +%token BVDIV_TOK "BVDIV" +%token BVMOD_TOK "BVMOD" +%token SBVDIV_TOK "SBVDIV" +%token SBVMOD_TOK "SBVMOD" + + +%token BVNEG_TOK "~" +%token BVAND_TOK "&" +%token BVOR_TOK "|" +%token BVXOR_TOK "BVXOR" +%token BVNAND_TOK "BVNAND" +%token BVNOR_TOK "BVNOR" +%token BVXNOR_TOK "BVXNOR" +%token BVCONCAT_TOK "@" + +%token BVLT_TOK "BVLT" +%token BVGT_TOK "BVGT" +%token BVLE_TOK "BVLE" +%token BVGE_TOK "BVGE" + +%token BVSLT_TOK "BVSLT" +%token BVSGT_TOK "BVSGT" +%token BVSLE_TOK "BVSLE" +%token BVSGE_TOK "BVSGE" +%token BOOL_TO_BV_TOK "BOOLBV" +%token BVSX_TOK "BVSX" +%token BOOLEXTRACT_TOK "BOOLEXTRACT" +%token ASSERT_TOK "ASSERT" +%token QUERY_TOK "QUERY" + +%token BOOLEAN_TOK "BOOLEAN" +%token ARRAY_TOK "ARRAY" +%token OF_TOK "OF" +%token WITH_TOK "WITH" + +%token TRUELIT_TOK "TRUE" +%token FALSELIT_TOK "FALSE" + +%token IN_TOK "IN" +%token LET_TOK "LET" +//%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE" +%token PUSH_TOK "PUSH" +%token POP_TOK "POP" + +%left IN_TOK +%left XOR_TOK +%left IFF_TOK +%right IMPLIES_TOK +%left OR_TOK +%left AND_TOK +%left NAND_TOK +%left NOR_TOK +%left NOT_TOK +%left BVCONCAT_TOK +%left BVOR_TOK +%left BVAND_TOK +%left BVXOR_TOK +%left BVNAND_TOK +%left BVNOR_TOK +%left BVXNOR_TOK +%left BVNEG_TOK +%left BVLEFTSHIFT_TOK BVRIGHTSHIFT_TOK +%left WITH_TOK + +%nonassoc '=' NEQ_TOK ASSIGN_TOK +%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK +%nonassoc BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK BVSX_TOK +%nonassoc '[' +%nonassoc '{' '.' '(' +%nonassoc BV_TOK + +%type <vec> Exprs FORM_IDs reverseFORM_IDs +%type <vec> Asserts +%type <node> Expr Formula IfExpr ElseRestExpr IfForm ElseRestForm Assert Query ArrayUpdateExpr +%type <Index_To_UpdateValue> Updates + +%type <indexvaluewidth> BvType BoolType ArrayType Type + +%token <node> BVCONST_TOK +%token <node> TERMID_TOK FORMID_TOK COUNTEREXAMPLE_TOK +%token <uintval> NUMERAL_TOK + +%% + +cmd : other_cmd + | other_cmd counterexample + ; + +counterexample : COUNTEREXAMPLE_TOK ';' + { + BEEV::print_counterexample = true; + BEEV::globalBeevMgr_for_parser->PrintCounterExample(true); + } + ; + +other_cmd : other_cmd1 + | Query + { + BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$1); + delete $1; + } + | VarDecls Query + { + BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE),*$2); + delete $2; + } + | other_cmd1 Query + { + BEEV::ASTVec aaa = BEEV::globalBeevMgr_for_parser->GetAsserts(); + if(aaa.size() == 0) + yyerror("Fatal Error: parsing: GetAsserts() call: no assertions: "); + if(aaa.size() == 1) + BEEV::globalBeevMgr_for_parser->TopLevelSAT(aaa[0],*$2); + else + BEEV::globalBeevMgr_for_parser->TopLevelSAT(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,aaa),*$2); + delete $2; + } + ; + +other_cmd1 : VarDecls Asserts + { + delete $2; + } + | Asserts + { + delete $1; + } + | other_cmd1 VarDecls Asserts + { + delete $3; + } + ; + +/* push : PUSH_TOK */ +/* { */ +/* BEEV::globalBeevMgr_for_parser->Push(); */ +/* } */ +/* | */ +/* ; */ + +/* pop : POP_TOK */ +/* { */ +/* BEEV::globalBeevMgr_for_parser->Pop(); */ +/* } */ +/* | */ +/* ; */ + +Asserts : Assert + { + $$ = new BEEV::ASTVec; + $$->push_back(*$1); + BEEV::globalBeevMgr_for_parser->AddAssert(*$1); + delete $1; + } + | Asserts Assert + { + $1->push_back(*$2); + BEEV::globalBeevMgr_for_parser->AddAssert(*$2); + $$ = $1; + delete $2; + } + ; + +Assert : ASSERT_TOK Formula ';' { $$ = $2; } + ; + +Query : QUERY_TOK Formula ';' { BEEV::globalBeevMgr_for_parser->AddQuery(*$2); $$ = $2;} + ; + + +/* Grammar for Variable Declaration */ +VarDecls : VarDecl ';' + { + } + | VarDecls VarDecl ';' + { + } + ; + +VarDecl : FORM_IDs ':' Type + { + for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + BEEV::_parser_symbol_table.insert(*i); + i->SetIndexWidth($3.indexwidth); + i->SetValueWidth($3.valuewidth); + + //FIXME: HACK_ATTACK. this vector was hacked into the code to + //support a special request by Dawson' group. They want the + //counterexample to be printed in the order of variables declared. + BEEV::globalBeevMgr_for_parser->_special_print_set.push_back(*i); + } + delete $1; + } + | FORM_IDs ':' Type '=' Expr + { + //do type checking. if doesn't pass then abort + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + //set the valuewidth of the identifier + i->SetValueWidth($5->GetValueWidth()); + i->SetIndexWidth($5->GetIndexWidth()); + + BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5); + delete $5; + } + } + | FORM_IDs ':' Type '=' Formula + { + //do type checking. if doesn't pass then abort + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + for(BEEV::ASTVec::iterator i=$1->begin(),iend=$1->end();i!=iend;i++) { + //set the valuewidth of the identifier + i->SetValueWidth($5->GetValueWidth()); + i->SetIndexWidth($5->GetIndexWidth()); + + BEEV::globalBeevMgr_for_parser->LetExprMgr(*i,*$5); + delete $5; + } + } + ; + +reverseFORM_IDs : FORMID_TOK + { + $$ = new BEEV::ASTVec; + $$->push_back(*$1); + delete $1; + } + | FORMID_TOK ',' reverseFORM_IDs + { + $3->push_back(*$1); + $$ = $3; + delete $1; + } + ; + +FORM_IDs : reverseFORM_IDs + { + $$ = new BEEV::ASTVec($1->rbegin(),$1->rend()); + delete $1; + } + ; + +/* Grammar for Types */ +Type : BvType { $$ = $1; } + | BoolType { $$ = $1; } + | ArrayType { $$ = $1; } + ; + +BvType : BV_TOK '(' NUMERAL_TOK ')' + { + /*((indexwidth is 0) && (valuewidth>0)) iff type is BV*/ + $$.indexwidth = 0; + unsigned int length = $3; + if(length > 0) { + $$.valuewidth = length; + } + else + BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } + ; +BoolType : BOOLEAN_TOK + { + $$.indexwidth = 0; + $$.valuewidth = 0; + } + ; +ArrayType : ARRAY_TOK BvType OF_TOK BvType + { + $$.indexwidth = $2.valuewidth; + $$.valuewidth = $4.valuewidth; + } + ; + +/*Grammar for ITEs which are a type of Term*/ +IfExpr : IF_TOK Formula THEN_TOK Expr ElseRestExpr + { + unsigned int width = $4->GetValueWidth(); + if (width != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + if($4->GetIndexWidth() != $5->GetIndexWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5)); + $$->SetIndexWidth($5->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + delete $2; + delete $4; + delete $5; + } + ; + +ElseRestExpr : ELSE_TOK Expr ENDIF_TOK { $$ = $2; } + | ELSIF_TOK Expr THEN_TOK Expr ElseRestExpr + { + unsigned int width = $2->GetValueWidth(); + if (width != $4->GetValueWidth() || width != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + if ($2->GetIndexWidth() != $4->GetValueWidth() || $2->GetIndexWidth() != $5->GetValueWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE, width, *$2, *$4, *$5)); + $$->SetIndexWidth($5->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + delete $2; + delete $4; + delete $5; + } + ; + +/* Grammar for formulas */ +Formula : '(' Formula ')' { $$ = $2; } + | FORMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;} + | BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')' + { + unsigned int width = $3->GetValueWidth(); + if(0 > (unsigned)$5 || width <= (unsigned)$5) + yyerror("Fatal Error: BOOLEXTRACT: trying to boolextract a bit which beyond range"); + + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,1,*$3,hi,low)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0); + BEEV::ASTNode * out = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ,*n,zero)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*out); + + $$ = out; + delete $3; + } + | Expr '=' Expr + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::EQ, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; + } + | Expr NEQ_TOK Expr + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NEQ, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; + } + | NOT_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$2)); + delete $2; + } + | Formula OR_TOK Formula %prec OR_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$1, *$3)); + delete $1; + delete $3; + } + | Formula NOR_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOR, *$1, *$3)); + delete $1; + delete $3; + } + | Formula AND_TOK Formula %prec AND_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$1, *$3)); + delete $1; + delete $3; + } + | Formula NAND_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NAND, *$1, *$3)); + delete $1; + delete $3; + } + | Formula IMPLIES_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$1, *$3)); + delete $1; + delete $3; + } + | Formula IFF_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$1, *$3)); + delete $1; + delete $3; + } + | Formula XOR_TOK Formula + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$1, *$3)); + delete $1; + delete $3; + } + | BVLT_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVGT_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVLE_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVGE_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVSLT_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVSGT_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVSLE_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVSGE_TOK '(' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | IfForm + | TRUELIT_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); + } + | FALSELIT_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); + } + + | LET_TOK LetDecls IN_TOK Formula + { + $$ = $4; + //Cleanup the LetIDToExprMap + BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + } + ; + +/*Grammar for ITEs which are Formulas */ +IfForm : IF_TOK Formula THEN_TOK Formula ElseRestForm + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5)); + delete $2; + delete $4; + delete $5; + } + ; + +ElseRestForm : ELSE_TOK Formula ENDIF_TOK { $$ = $2; } + | ELSIF_TOK Formula THEN_TOK Formula ElseRestForm + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$2, *$4, *$5)); + delete $2; + delete $4; + delete $5; + } + ; + +/*Grammar for a list of expressions*/ +Exprs : Expr + { + $$ = new BEEV::ASTVec; + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$1); + $$->push_back(*$1); + delete $1; + } + | Exprs ',' Expr + { + $1->push_back(*$3); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + $$ = $1; + delete $3; + } + ; + +/* Grammar for Expr */ +Expr : TERMID_TOK { $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); delete $1;} + | '(' Expr ')' { $$ = $2; } + | BVCONST_TOK { $$ = $1; } + | BOOL_TO_BV_TOK '(' Formula ')' + { + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + BEEV::ASTNode one = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,1); + BEEV::ASTNode zero = BEEV::globalBeevMgr_for_parser->CreateBVConst(1,0); + + //return ITE(*$3, length(1), 0bin1, 0bin0) + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,1,*$3,one,zero)); + delete $3; + } + | Expr '[' Expr ']' + { + // valuewidth is same as array, indexwidth is 0. + unsigned int width = $1->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; + } + | Expr '(' Expr ')' //array read but in the form of a uninterpreted function application + { + // valuewidth is same as array, indexwidth is 0. + unsigned int width = $1->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; + } + | Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']' + { + int width = $3 - $5 + 1; + if (width < 0) + yyerror("Negative width in extract"); + + if((unsigned)$3 >= $1->GetValueWidth() || (unsigned)$5 < 0) + yyerror("Parsing: Wrong width in BVEXTRACT\n"); + + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$1,hi,low)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + } + | BVNEG_TOK Expr + { + unsigned int width = $2->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNEG, width, *$2)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + } + | Expr BVAND_TOK Expr + { + unsigned int width = $1->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in AND"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; + } + | Expr BVOR_TOK Expr + { + unsigned int width = $1->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in OR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + delete $3; + } + | BVXOR_TOK '(' Expr ',' Expr ')' + { + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in XOR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $5; + } + | BVNAND_TOK '(' Expr ',' Expr ')' + { + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NAND"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; + } + | BVNOR_TOK '(' Expr ',' Expr ')' + { + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NOR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; + } + | BVXNOR_TOK '(' Expr ',' Expr ')' + { + unsigned int width = $3->GetValueWidth(); + if (width != $5->GetValueWidth()) { + yyerror("Width mismatch in NOR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXNOR, width, *$3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $3; + delete $5; + } + | BVSX_TOK '(' Expr ',' NUMERAL_TOK ')' + { + //width of the expr which is being sign + //extended. $5 is the resulting length of the + //signextended expr + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + if($3->GetValueWidth() == $5) { + $$ = $3; + } + else { + BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$5); + BEEV::ASTNode *n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX, $5,*$3,width)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + } + } + | Expr BVCONCAT_TOK Expr + { + unsigned int width = $1->GetValueWidth() + $3->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$1, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $1; + delete $3; + } + | Expr BVLEFTSHIFT_TOK NUMERAL_TOK + { + BEEV::ASTNode zero_bits = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, + $1->GetValueWidth() + $3, *$1, zero_bits)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $1; + } + | Expr BVRIGHTSHIFT_TOK NUMERAL_TOK + { + BEEV::ASTNode len = BEEV::globalBeevMgr_for_parser->CreateZeroConst($3); + unsigned int w = $1->GetValueWidth(); + + //the amount by which you are rightshifting + //is less-than/equal-to the length of input + //bitvector + if((unsigned)$3 < w) { + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$3); + BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$1,hi,low); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,len, extract)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + } + else + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateZeroConst(w)); + + delete $1; + } + | BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, $3, *$5)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + } + | BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; + } + | BVUMINUS_TOK '(' Expr ')' + { + unsigned width = $3->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + } + | BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; + } + | BVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVDIV, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; + } + | BVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMOD, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; + } + | SBVDIV_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVDIV, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $5; + delete $7; + } + | SBVMOD_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')' + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::SBVMOD, $3, *$5, *$7)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $5; + delete $7; + } + | IfExpr { $$ = $1; } + | ArrayUpdateExpr + | LET_TOK LetDecls IN_TOK Expr + { + $$ = $4; + //Cleanup the LetIDToExprMap + //BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + } + ; + +/*Grammar for Array Update Expr*/ +ArrayUpdateExpr : Expr WITH_TOK Updates + { + BEEV::ASTNode * result; + unsigned int width = $1->GetValueWidth(); + + BEEV::ASTNodeMap::iterator it = $3->begin(); + BEEV::ASTNodeMap::iterator itend = $3->end(); + result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE, + width, + *$1, + (*it).first, + (*it).second)); + result->SetIndexWidth($1->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + for(it++;it!=itend;it++) { + result = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE, + width, + *result, + (*it).first, + (*it).second)); + result->SetIndexWidth($1->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + } + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*result); + $$ = result; + delete $3; + } + ; + +Updates : '[' Expr ']' ASSIGN_TOK Expr + { + $$ = new BEEV::ASTNodeMap(); + (*$$)[*$2] = *$5; + } + | Updates WITH_TOK '[' Expr ']' ASSIGN_TOK Expr + { + (*$1)[*$4] = *$7; + } + ; + +/*Grammar for LET Expr*/ +LetDecls : LetDecl + | LetDecls ',' LetDecl + ; + +LetDecl : FORMID_TOK '=' Expr + { + //Expr must typecheck + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + + //set the valuewidth of the identifier + $1->SetValueWidth($3->GetValueWidth()); + $1->SetIndexWidth($3->GetIndexWidth()); + + //populate the hashtable from LET-var --> + //LET-exprs and then process them: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3); + delete $1; + delete $3; + } + | FORMID_TOK ':' Type '=' Expr + { + //do type checking. if doesn't pass then abort + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + //set the valuewidth of the identifier + $1->SetValueWidth($5->GetValueWidth()); + $1->SetIndexWidth($5->GetIndexWidth()); + + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5); + delete $1; + delete $5; + } + | FORMID_TOK '=' Formula + { + //Expr must typecheck + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + + //set the valuewidth of the identifier + $1->SetValueWidth($3->GetValueWidth()); + $1->SetIndexWidth($3->GetIndexWidth()); + + //Do LET-expr management + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$3); + delete $1; + delete $3; + } + | FORMID_TOK ':' Type '=' Formula + { + //do type checking. if doesn't pass then abort + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + + if($3.indexwidth != $5->GetIndexWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + if($3.valuewidth != $5->GetValueWidth()) + yyerror("Fatal Error: parsing: LET Expr: Type check fail: "); + + //set the valuewidth of the identifier + $1->SetValueWidth($5->GetValueWidth()); + $1->SetIndexWidth($5->GetIndexWidth()); + + //Do LET-expr management + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$1,*$5); + delete $1; + delete $5; + } + ; + +%% diff --git a/stp/parser/let-funcs.cpp b/stp/parser/let-funcs.cpp new file mode 100644 index 00000000..1de10492 --- /dev/null +++ b/stp/parser/let-funcs.cpp @@ -0,0 +1,85 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "../AST/AST.h" +#include <stdlib.h> + +namespace BEEV { + //external parser table for declared symbols. Only symbols which are + //declared are stored here. + ASTNodeSet _parser_symbol_table; + + // FUNC: This function maintains a map between LET-var names and + // LET-expressions + // + //1. if the Let-var is already defined in the LET scope, then the + //1. function returns an error. + // + //2. if the Let-var is already declared variable in the input, then + //2. the function returns an error + // + //3. otherwise add the <var,letExpr> pair to the _letid_expr table. + void BeevMgr::LetExprMgr(const ASTNode& var, const ASTNode& letExpr) { + ASTNodeMap::iterator it; + if(((it = _letid_expr_map.find(var)) != _letid_expr_map.end()) && + it->second != ASTUndefined) { + FatalError("LetExprMgr:The LET-var v has already been defined in this LET scope: v =", var); + } + + if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) { + FatalError("LetExprMgr:This var is already declared. cannot redeclare as a letvar: v =", var); + } + + _letid_expr_map[var] = letExpr; + } + + //this function looksup the "var to letexpr map" and returns the + //corresponding letexpr. if there is no letexpr, then it simply + //returns the var. + ASTNode BeevMgr::ResolveID(const ASTNode& v) { + if(v.GetKind() != SYMBOL) { + return v; + } + + if(_parser_symbol_table.find(v) != _parser_symbol_table.end()) { + return v; + } + + ASTNodeMap::iterator it; + if((it =_letid_expr_map.find(v)) != _letid_expr_map.end()) { + if(it->second == ASTUndefined) + FatalError("Unresolved Identifier: ",v); + else + return it->second; + } + + //this is to mark the let-var as undefined. the let var is defined + //only after the LetExprMgr has completed its work, and until then + //'v' is undefined. + // + //declared variables also get stored in this map, but there value + //is ASTUndefined. This is really a hack. I don't know how to get + //rid of this hack. + _letid_expr_map[v] = ASTUndefined; + return v; + } + + // This function simply cleans up the LetID -> LetExpr Map. + void BeevMgr::CleanupLetIDMap(void) { + ASTNodeMap::iterator it = _letid_expr_map.begin(); + ASTNodeMap::iterator itend = _letid_expr_map.end(); + for(;it!=itend;it++) { + if(it->second != ASTUndefined) { + it->first.SetValueWidth(0); + it->first.SetIndexWidth(0); + } + } + _letid_expr_map.clear(); + } +}; diff --git a/stp/parser/main.cpp b/stp/parser/main.cpp new file mode 100644 index 00000000..ed251ed3 --- /dev/null +++ b/stp/parser/main.cpp @@ -0,0 +1,181 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include <iostream> +#include <sstream> +#include <string> +#include <algorithm> +#include <ctime> +#include <unistd.h> +#include <signal.h> +//#include <zlib.h> +#include <stdio.h> +#include "../AST/AST.h" +#include "parsePL_defs.h" +#include "../sat/Solver.h" +#include "../sat/SolverTypes.h" +#include "../sat/VarOrder.h" + +#include <unistd.h> + +#ifdef EXT_HASH_MAP + using namespace __gnu_cxx; +#endif + +/* GLOBAL FUNCTION: parser + */ +extern int yyparse(); +//extern int smtlibparse(); + +/* GLOBAL VARS: Some global vars for the Main function. + * + */ +const char * prog = "stp"; +int linenum = 1; +const char * usage = "Usage: %s [-option] [infile]\n"; +std::string helpstring = "\n\n"; + +// Amount of memory to ask for at beginning of main. +static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; + +// Used only in smtlib lexer/parser +BEEV::ASTNode SingleBitOne; +BEEV::ASTNode SingleBitZero; + +/****************************************************************************** + * MAIN FUNCTION: + * + * step 0. Parse the input into an ASTVec. + * step 1. Do BV Rewrites + * step 2. Bitblasts the ASTNode. + * step 3. Convert to CNF + * step 4. Convert to SAT + * step 5. Call SAT to determine if input is SAT or UNSAT + ******************************************************************************/ +int main(int argc, char ** argv) { + char * infile; + extern FILE *yyin; + + // Grab some memory from the OS upfront to reduce system time when individual + // hash tables are being allocated + + if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) { + // FIXME: figure out how to get and print the real error message. + BEEV::FatalError("Initial allocation of memory failed."); + } + + //populate the help string + helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; + helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; + helpstring += "-a : switch optimizations off (optimizations are ON by default)\n"; + helpstring += "-s : print function statistics\n"; + helpstring += "-v : print nodes \n"; + helpstring += "-c : construct counterexample\n"; + helpstring += "-d : check counterexample\n"; + helpstring += "-p : print counterexample\n"; + helpstring += "-x : flatten nested XORs\n"; + helpstring += "-h : help\n"; + + for(int i=1; i < argc;i++) { + if(argv[i][0] == '-') + switch(argv[i][1]) { + case 'a' : + BEEV::optimize = false; + BEEV::wordlevel_solve = false; + break; + case 'b': + BEEV::print_STPinput_back = true; + break; + case 'c': + BEEV::construct_counterexample = true; + break; + case 'd': + BEEV::construct_counterexample = true; + BEEV::check_counterexample = true; + break; + case 'e': + BEEV::variable_activity_optimize = true; + break; + case 'f': + BEEV::smtlib_parser_enable = true; + break; + case 'h': + fprintf(stderr,usage,prog); + cout << helpstring; + //BEEV::FatalError(""); + return -1; + break; + case 'l' : + BEEV::linear_search = true; + break; + case 'n': + BEEV::print_output = true; + break; + case 'p': + BEEV::print_counterexample = true; + break; + case 'q': + BEEV::print_arrayval_declaredorder = true; + break; + case 'r': + BEEV::arrayread_refinement = false; + break; + case 's' : + BEEV::stats = true; + break; + case 'u': + BEEV::arraywrite_refinement = false; + break; + case 'v' : + BEEV::print_nodes = true; + break; + case 'w': + BEEV::wordlevel_solve = false; + break; + case 'x': + BEEV::xor_flatten = true; + break; + case 'z': + BEEV::print_sat_varorder = true; + break; + default: + fprintf(stderr,usage,prog); + cout << helpstring; + //BEEV::FatalError(""); + return -1; + break; + } + else { + infile = argv[i]; + yyin = fopen(infile,"r"); + if(yyin == NULL) { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + BEEV::FatalError(""); + } + } + } + +#ifdef NATIVE_C_ARITH +#else + CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); + if(0 != c) { + cout << CONSTANTBV::BitVector_Error(c) << endl; + return 0; + } +#endif + + //want to print the output always from the commandline. + BEEV::print_output = true; + BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); + + SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); + SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); + //BEEV::smtlib_parser_enable = true; + yyparse(); +}//end of Main diff --git a/stp/parser/smtlib.lex b/stp/parser/smtlib.lex new file mode 100644 index 00000000..a03ae94e --- /dev/null +++ b/stp/parser/smtlib.lex @@ -0,0 +1,232 @@ +%{ + /******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: July, 2006 + * + * This file is modified version of the CVCL's smtlib.lex file. Please + * see CVCL license below + ********************************************************************/ + + /******************************************************************** + * \file smtlib.lex + * + * Author: Sergey Berezin, Clark Barrett + * + * Created: Apr 30 2005 + * + * <hr> + * Copyright (C) 2004 by the Board of Trustees of Leland Stanford + * Junior University and by New York University. + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. In particular: + * + * - The above copyright notice and this permission notice must appear + * in all copies of the software and related documentation. + * + * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, + * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. + * + * <hr> + ********************************************************************/ + // -*- c++ -*- +#include <iostream> +#include "../AST/AST.h" +#include "parsePL_defs.h" + + extern char *yytext; + extern int yyerror (char *msg); + + // File-static (local to this file) variables and functions + static std::string _string_lit; + + static char escapeChar(char c) { + switch(c) { + case 'n': return '\n'; + case 't': return '\t'; + default: return c; + } + } + + extern BEEV::ASTNode SingleBitOne; + extern BEEV::ASTNode SingleBitZero; + +/* Changed for smtlib speedup */ +/* bv{DIGIT}+ { yylval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(yytext+2, 10)); return BVCONST_TOK;} */ + +%} + +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno + +%x COMMENT +%x STRING_LITERAL +%x USER_VALUE + +LETTER ([a-zA-Z]) +DIGIT ([0-9]) +OPCHAR (['\.\_]) +ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) + +%% +[ \n\t\r\f] { /* sk'ip whitespace */ } +{DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; } + + +bv{DIGIT}+ { yylval.ullval = strtoull(yytext+2, NULL, 10); return BVCONST_TOK; } + +bit{DIGIT}+ { + char c = yytext[3]; + if (c == '1') { + yylval.node = new BEEV::ASTNode(SingleBitOne); + } + else { + yylval.node = new BEEV::ASTNode(SingleBitZero); + } + return BITCONST_TOK; + }; + + +";" { BEGIN COMMENT; } +<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */} +<COMMENT>. { /* stay in comment mode */ } + +<INITIAL>"\"" { BEGIN STRING_LITERAL; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */ + _string_lit.insert(_string_lit.end(), + escapeChar(yytext[1])); } +<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */ + yylval.str = new std::string(_string_lit); + return STRING_TOK; } +<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*yytext); } + + +<INITIAL>"{" { BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +<USER_VALUE>"\\"[{}] { /* escape characters */ + _string_lit.insert(_string_lit.end(),yytext[1]); } + +<USER_VALUE>"}" { BEGIN INITIAL; /* return to normal mode */ + yylval.str = new std::string(_string_lit); + return USER_VAL_TOK; } +<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');} +<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*yytext); } + +"BitVec" { return BITVEC_TOK;} +"Array" { return ARRAY_TOK;} +"true" { return TRUE_TOK; } +"false" { return FALSE_TOK; } +"not" { return NOT_TOK; } +"implies" { return IMPLIES_TOK; } +"ite" { return ITE_TOK;} +"if_then_else" { return IF_THEN_ELSE_TOK; } +"and" { return AND_TOK; } +"or" { return OR_TOK; } +"xor" { return XOR_TOK; } +"iff" { return IFF_TOK; } +"let" { return LET_TOK; } +"flet" { return FLET_TOK; } +"notes" { return NOTES_TOK; } +"cvc_command" { return CVC_COMMAND_TOK; } +"sorts" { return SORTS_TOK; } +"funs" { return FUNS_TOK; } +"preds" { return PREDS_TOK; } +"extensions" { return EXTENSIONS_TOK; } +"definition" { return DEFINITION_TOK; } +"axioms" { return AXIOMS_TOK; } +"logic" { return LOGIC_TOK; } +"sat" { return SAT_TOK; } +"unsat" { return UNSAT_TOK; } +"unknown" { return UNKNOWN_TOK; } +"assumption" { return ASSUMPTION_TOK; } +"formula" { return FORMULA_TOK; } +"status" { return STATUS_TOK; } +"difficulty" { return DIFFICULTY_TOK; } +"benchmark" { return BENCHMARK_TOK; } +"source" { return SOURCE_TOK;} +"category" { return CATEGORY_TOK;} +"extrasorts" { return EXTRASORTS_TOK; } +"extrafuns" { return EXTRAFUNS_TOK; } +"extrapreds" { return EXTRAPREDS_TOK; } +"language" { return LANGUAGE_TOK; } +"distinct" { return DISTINCT_TOK; } +"select" { return SELECT_TOK; } +"store" { return STORE_TOK; } +":" { return COLON_TOK; } +"\[" { return LBRACKET_TOK; } +"\]" { return RBRACKET_TOK; } +"(" { return LPAREN_TOK; } +")" { return RPAREN_TOK; } +"$" { return DOLLAR_TOK; } +"?" { return QUESTION_TOK; } +"=" {return EQ_TOK;} + +"nand" { return NAND_TOK;} +"nor" { return NOR_TOK;} +"/=" { return NEQ_TOK; } + ":=" { return ASSIGN_TOK;} +"shift_left0" { return BVLEFTSHIFT_TOK;} +"bvshl" { return BVLEFTSHIFT_1_TOK;} +"shift_right0" { return BVRIGHTSHIFT_TOK;} +"bvlshr" { return BVRIGHTSHIFT_1_TOK;} +"bvadd" { return BVPLUS_TOK;} +"bvsub" { return BVSUB_TOK;} +"bvnot" { return BVNOT_TOK;} +"bvmul" { return BVMULT_TOK;} +"bvdiv" { return BVDIV_TOK;} +"bvmod" { return BVMOD_TOK;} +"bvneg" { return BVNEG_TOK;} +"bvand" { return BVAND_TOK;} +"bvor" { return BVOR_TOK;} +"bvxor" { return BVXOR_TOK;} +"bvnand" { return BVNAND_TOK;} +"bvnor" { return BVNOR_TOK;} +"bvxnor" { return BVXNOR_TOK;} +"concat" { return BVCONCAT_TOK;} +"extract" { return BVEXTRACT_TOK;} +"bvlt" { return BVLT_TOK;} +"bvgt" { return BVGT_TOK;} +"bvleq" { return BVLE_TOK;} +"bvgeq" { return BVGE_TOK;} +"bvult" { return BVLT_TOK;} +"bvugt" { return BVGT_TOK;} +"bvuleq" { return BVLE_TOK;} +"bvugeq" { return BVGE_TOK;} +"bvule" { return BVLE_TOK;} +"bvuge" { return BVGE_TOK;} + +"bvslt" { return BVSLT_TOK;} +"bvsgt" { return BVSGT_TOK;} +"bvsleq" { return BVSLE_TOK;} +"bvsgeq" { return BVSGE_TOK;} +"bvsle" { return BVSLE_TOK;} +"bvsge" { return BVSGE_TOK;} + +"sign_extend" { return BVSX_TOK;} +"boolextract" { return BOOLEXTRACT_TOK;} +"boolbv" { return BOOL_TO_BV_TOK;} + +(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { + BEEV::ASTNode nptr = BEEV::globalBeevMgr_for_parser->CreateSymbol(yytext); + + // 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. + yylval.node = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(nptr)); + //yylval.node = new BEEV::ASTNode(nptr); + if ((yylval.node)->GetType() == BEEV::BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; +} +. { yyerror("Illegal input character."); } +%% diff --git a/stp/parser/smtlib.y b/stp/parser/smtlib.y new file mode 100644 index 00000000..0aa22dee --- /dev/null +++ b/stp/parser/smtlib.y @@ -0,0 +1,1036 @@ +%{ + /******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: July, 2006 + * + * This file is modified version of the CVCL's smtlib.y file. Please + * see CVCL license below + ********************************************************************/ + + /******************************************************************** + * + * \file smtlib.y + * + * Author: Sergey Berezin, Clark Barrett + * + * Created: Apr 30 2005 + * + * <hr> + * Copyright (C) 2004 by the Board of Trustees of Leland Stanford + * Junior University and by New York University. + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. In particular: + * + * - The above copyright notice and this permission notice must appear + * in all copies of the software and related documentation. + * + * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, + * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. + * + * <hr> + ********************************************************************/ + // -*- c++ -*- + +#include "../AST/AST.h" + using namespace std; + + // Suppress the bogus warning suppression in bison (it generates + // compile error) +#undef __GNUC_MINOR__ + + extern char* yytext; + extern int yylineno; + + //int yylineno; + + extern int yylex(void); + + int yyerror(char *s) { + //yylineno = 0; + cout << "syntax error: line " << yylineno << "\n" << s << endl; + cout << " token: " << yytext << endl; + BEEV::FatalError(""); + return 1; + } + + BEEV::ASTNode query; +#define YYLTYPE_IS_TRIVIAL 1 +#define YYMAXDEPTH 104857600 +#define YYERROR_VERBOSE 1 +#define YY_EXIT_FAILURE -1 +%} + +%union { + // FIXME: Why is this not an UNSIGNED int? + int uintval; /* for numerals in types. */ + + // for BV32 BVCONST + unsigned long long ullval; + + struct { + //stores the indexwidth and valuewidth + //indexwidth is 0 iff type is bitvector. positive iff type is + //array, and stores the width of the indexing bitvector + unsigned int indexwidth; + //width of the bitvector type + unsigned int valuewidth; + } indexvaluewidth; + + //ASTNode,ASTVec + BEEV::ASTNode *node; + BEEV::ASTVec *vec; + std::string *str; +}; + +%start cmd + +%type <indexvaluewidth> sort_symb sort_symbs +%type <node> status +%type <vec> bench_attributes an_formulas + +%type <node> benchmark bench_name bench_attribute +%type <node> an_term an_nonbvconst_term an_formula + +%type <node> var fvar logic_name +%type <str> user_value + +%token <uintval> NUMERAL_TOK +%token <ullval> BVCONST_TOK +%token <node> BITCONST_TOK +%token <node> FORMID_TOK TERMID_TOK +%token <str> STRING_TOK +%token <str> USER_VAL_TOK +%token SOURCE_TOK +%token CATEGORY_TOK +%token DIFFICULTY_TOK +%token BITVEC_TOK +%token ARRAY_TOK +%token SELECT_TOK +%token STORE_TOK +%token TRUE_TOK +%token FALSE_TOK +%token NOT_TOK +%token IMPLIES_TOK +%token ITE_TOK +%token IF_THEN_ELSE_TOK +%token AND_TOK +%token OR_TOK +%token XOR_TOK +%token IFF_TOK +%token EXISTS_TOK +%token FORALL_TOK +%token LET_TOK +%token FLET_TOK +%token NOTES_TOK +%token CVC_COMMAND_TOK +%token SORTS_TOK +%token FUNS_TOK +%token PREDS_TOK +%token EXTENSIONS_TOK +%token DEFINITION_TOK +%token AXIOMS_TOK +%token LOGIC_TOK +%token COLON_TOK +%token LBRACKET_TOK +%token RBRACKET_TOK +%token LPAREN_TOK +%token RPAREN_TOK +%token SAT_TOK +%token UNSAT_TOK +%token UNKNOWN_TOK +%token ASSUMPTION_TOK +%token FORMULA_TOK +%token STATUS_TOK +%token BENCHMARK_TOK +%token EXTRASORTS_TOK +%token EXTRAFUNS_TOK +%token EXTRAPREDS_TOK +%token LANGUAGE_TOK +%token DOLLAR_TOK +%token QUESTION_TOK +%token DISTINCT_TOK +%token SEMICOLON_TOK +%token EOF_TOK +%token EQ_TOK +/*BV SPECIFIC TOKENS*/ +%token NAND_TOK +%token NOR_TOK +%token NEQ_TOK +%token ASSIGN_TOK +%token BV_TOK +%token BOOLEAN_TOK +%token BVLEFTSHIFT_TOK +%token BVLEFTSHIFT_1_TOK +%token BVRIGHTSHIFT_TOK +%token BVRIGHTSHIFT_1_TOK +%token BVPLUS_TOK +%token BVSUB_TOK +%token BVNOT_TOK //bvneg in CVCL +%token BVMULT_TOK +%token BVDIV_TOK +%token BVMOD_TOK +%token BVNEG_TOK //bvuminus in CVCL +%token BVAND_TOK +%token BVOR_TOK +%token BVXOR_TOK +%token BVNAND_TOK +%token BVNOR_TOK +%token BVXNOR_TOK +%token BVCONCAT_TOK +%token BVLT_TOK +%token BVGT_TOK +%token BVLE_TOK +%token BVGE_TOK +%token BVSLT_TOK +%token BVSGT_TOK +%token BVSLE_TOK +%token BVSGE_TOK +%token BVSX_TOK +%token BOOLEXTRACT_TOK +%token BOOL_TO_BV_TOK +%token BVEXTRACT_TOK + +%left LBRACKET_TOK RBRACKET_TOK + +%% + +cmd: + benchmark + { + if($1 != NULL) { + BEEV::globalBeevMgr_for_parser->TopLevelSAT(*$1,query); + delete $1; + } + YYACCEPT; + } +; + +benchmark: + LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK + { + if($4 != NULL){ + if($4->size() > 1) + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND,*$4)); + else + $$ = new BEEV::ASTNode((*$4)[0]); + delete $4; + } + else { + $$ = NULL; + } + } +/* | EOF_TOK */ +/* { */ +/* } */ +; + +bench_name: + FORMID_TOK + { + } +; + +bench_attributes: + bench_attribute + { + $$ = new BEEV::ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + BEEV::globalBeevMgr_for_parser->AddAssert(*$1); + delete $1; + } + } + | bench_attributes bench_attribute + { + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + BEEV::globalBeevMgr_for_parser->AddAssert(*$2); + $$ = $1; + delete $2; + } + } +; + +bench_attribute: + COLON_TOK ASSUMPTION_TOK an_formula + { + //assumptions are like asserts + $$ = $3; + } + | COLON_TOK FORMULA_TOK an_formula + { + //the query + query = BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT,*$3); + BEEV::globalBeevMgr_for_parser->AddQuery(query); + //dummy true + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); + + + } + | COLON_TOK STATUS_TOK status + { + $$ = NULL; + } + | COLON_TOK LOGIC_TOK logic_name + { + if (!(0 == strcmp($3->GetName(),"QF_UFBV") || + 0 == strcmp($3->GetName(),"QF_AUFBV"))) { + yyerror("Wrong input logic:"); + } + $$ = NULL; + } + | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK var_decls RPAREN_TOK + { + $$ = NULL; + } + | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK + { + $$ = NULL; + } + | annotation + { + $$ = NULL; + } +; + +logic_name: + FORMID_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + $$ = $1; + } + | FORMID_TOK + { + $$ = $1; + } +; + +status: + SAT_TOK { $$ = NULL; } + | UNSAT_TOK { $$ = NULL; } + | UNKNOWN_TOK { $$ = NULL; } +; + + +/* annotations: */ +/* annotation */ +/* { */ +/* } */ +/* | annotations annotation */ +/* { */ +/* } */ +/* ; */ + +annotation: + attribute + { + } + | attribute user_value + { + } +; + +user_value: + USER_VAL_TOK + { + //cerr << "Printing user_value: " << *$1 << endl; + } +; + +attribute: + COLON_TOK SOURCE_TOK + { + } + | COLON_TOK CATEGORY_TOK + { + } + | COLON_TOK DIFFICULTY_TOK +; + +sort_symbs: + sort_symb + { + //a single sort symbol here means either a BitVec or a Boolean + $$.indexwidth = $1.indexwidth; + $$.valuewidth = $1.valuewidth; + } + | sort_symb sort_symb + { + //two sort symbols mean f: type --> type + $$.indexwidth = $1.valuewidth; + $$.valuewidth = $2.valuewidth; + } +; + +var_decls: + var_decl + { + } +// | LPAREN_TOK var_decl RPAREN_TOK + | + var_decls var_decl + { + } +; + +var_decl: + LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK + { + BEEV::_parser_symbol_table.insert(*$2); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $2->SetIndexWidth($3.indexwidth); + $2->SetValueWidth($3.valuewidth); + } + | LPAREN_TOK FORMID_TOK RPAREN_TOK + { + BEEV::_parser_symbol_table.insert(*$2); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $2->SetIndexWidth(0); + $2->SetValueWidth(0); + } +; + +an_formulas: + an_formula + { + $$ = new BEEV::ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + delete $1; + } + } + | + an_formulas an_formula + { + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + $$ = $1; + delete $2; + } + } +; + +an_formula: + TRUE_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::TRUE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); + } + | FALSE_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::FALSE)); + $$->SetIndexWidth(0); + $$->SetValueWidth(0); + } + | fvar + { + $$ = $1; + } + | LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedEQ(*$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVSLT_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLT, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVSLE_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSLE, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGT, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVSGE_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVSGE, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVLT_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLT, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVLE_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVLE, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVGT_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGT, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVGE_TOK an_term an_term annotations RPAREN_TOK + { + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::BVGE, *$3, *$4)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $3; + delete $4; + } + | LPAREN_TOK an_formula RPAREN_TOK + { + $$ = $2; + } + | LPAREN_TOK NOT_TOK an_formula RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::NOT, *$3)); + delete $3; + } + | LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IMPLIES, *$3, *$4)); + delete $3; + delete $4; + } + | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::ITE, *$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; + } + | LPAREN_TOK AND_TOK an_formulas RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::AND, *$3)); + delete $3; + } + | LPAREN_TOK OR_TOK an_formulas RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::OR, *$3)); + delete $3; + } + | LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::XOR, *$3, *$4)); + delete $3; + delete $4; + } + | LPAREN_TOK IFF_TOK an_formula an_formula RPAREN_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateNode(BEEV::IFF, *$3, *$4)); + delete $3; + delete $4; + } + | letexpr_mgmt an_formula RPAREN_TOK + //| letexpr_mgmt an_formula annotations RPAREN_TOK + { + $$ = $2; + //Cleanup the LetIDToExprMap + BEEV::globalBeevMgr_for_parser->CleanupLetIDMap(); + } +; + +letexpr_mgmt: + LPAREN_TOK LET_TOK LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK + { + //Expr must typecheck + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6); + + //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: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6); + delete $5; + delete $6; + } + | LPAREN_TOK FLET_TOK LPAREN_TOK DOLLAR_TOK FORMID_TOK an_formula RPAREN_TOK + { + //Expr must typecheck + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$6); + + //set the valuewidth of the identifier + $5->SetValueWidth($6->GetValueWidth()); + $5->SetIndexWidth($6->GetIndexWidth()); + + //Do LET-expr management + BEEV::globalBeevMgr_for_parser->LetExprMgr(*$5,*$6); + delete $5; + delete $6; + } + +/* an_terms: */ +/* an_term */ +/* { */ +/* } */ +/* | an_terms an_term */ +/* { */ +/* } */ +/* ; */ + +an_term: + BVCONST_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(64, $1)); + } + | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($3, $1)); + } + | an_nonbvconst_term + ; + +an_nonbvconst_term: + BITCONST_TOK { $$ = $1; } + | var + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + delete $1; + } + | LPAREN_TOK an_term RPAREN_TOK + //| LPAREN_TOK an_term annotations RPAREN_TOK + { + $$ = $2; + //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(*$2)); + //delete $2; + } + | LPAREN_TOK TERMID_TOK an_term RPAREN_TOK + { + //ARRAY READ + // valuewidth is same as array, indexwidth is 0. + BEEV::ASTNode in = *$2; + BEEV::ASTNode m = *$3; + unsigned int width = in.GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, in, m)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | SELECT_TOK an_term an_term + { + //ARRAY READ + // valuewidth is same as array, indexwidth is 0. + BEEV::ASTNode array = *$2; + BEEV::ASTNode index = *$3; + unsigned int width = array.GetValueWidth(); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::READ, width, array, index)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | STORE_TOK an_term an_term an_term + { + //ARRAY WRITE + unsigned int width = $4->GetValueWidth(); + BEEV::ASTNode array = *$2; + BEEV::ASTNode index = *$3; + BEEV::ASTNode writeval = *$4; + BEEV::ASTNode write_term = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::WRITE,width,array,index,writeval); + write_term.SetIndexWidth($2->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(write_term); + BEEV::ASTNode * n = new BEEV::ASTNode(write_term); + $$ = n; + delete $2; + delete $3; + delete $4; + } +/* | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK BVCONST_TOK */ +/* { */ +/* // This special case is when we have an extract on top of a constant bv, which happens */ +/* // almost all the time in the smt syntax. */ + +/* // $3 is high, $5 is low. They are ints (why not unsigned? See uintval) */ +/* int hi = $3; */ +/* int low = $5; */ +/* int width = hi - low + 1; */ + +/* if (width < 0) */ +/* yyerror("Negative width in extract"); */ + +/* unsigned long long int val = $7; */ + +/* // cut and past from BV32 const evaluator */ + +/* unsigned long long int mask1 = 0xffffffffffffffffLL; */ + +/* mask1 >>= 64-(hi+1); */ + +/* //extract val[hi:0] */ +/* val &= mask1; */ +/* //extract val[hi:low] */ +/* val >>= low; */ + +/* // val is the desired BV32. */ +/* BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(width, val)); */ +/* $$ = n; */ +/* } */ + | BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term + { + int width = $3 - $5 + 1; + if (width < 0) + yyerror("Negative width in extract"); + + if((unsigned)$3 >= $7->GetValueWidth() || (unsigned)$5 < 0) + yyerror("Parsing: Wrong width in BVEXTRACT\n"); + + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $3); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, $5); + BEEV::ASTNode output = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT, width, *$7,hi,low); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->SimplifyTerm(output)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $7; + } + | ITE_TOK an_formula an_term an_term + { + unsigned int width = $3->GetValueWidth(); + if (width != $4->GetValueWidth()) { + cerr << *$3; + cerr << *$4; + yyerror("Width mismatch in IF-THEN-ELSE"); + } + if($3->GetIndexWidth() != $4->GetIndexWidth()) + yyerror("Width mismatch in IF-THEN-ELSE"); + + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$2); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$3); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$4); + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateSimplifiedTermITE(*$2, *$3, *$4)); + //$$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::ITE,width,*$2, *$3, *$4)); + $$->SetIndexWidth($4->GetIndexWidth()); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$$); + delete $2; + delete $3; + delete $4; + } + | BVCONCAT_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth() + $3->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + + delete $2; + delete $3; + } + | BVNOT_TOK an_term + { + //this is the BVNEG (term) in the CVCL language + unsigned int width = $2->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNEG, width, *$2)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + } + | BVNEG_TOK an_term + { + //this is the BVUMINUS term in CVCL langauge + unsigned width = $2->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVUMINUS,width,*$2)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + } + | BVAND_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in AND"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVAND, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVOR_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in OR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVOR, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVXOR_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in XOR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVXOR, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVSUB_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVSUB"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSUB, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVPLUS_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVPLUS"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVPLUS, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + + } + | BVMULT_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVMULT"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVMULT, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVNAND_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVNAND"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNAND, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVNOR_TOK an_term an_term + { + unsigned int width = $2->GetValueWidth(); + if (width != $3->GetValueWidth()) { + yyerror("Width mismatch in BVNOR"); + } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVNOR, width, *$2, *$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + delete $3; + } + | BVLEFTSHIFT_TOK an_term NUMERAL_TOK + { + unsigned int w = $2->GetValueWidth(); + if((unsigned)$3 < w) { + BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0); + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-$3-1); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); + BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + } + else + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + delete $2; + } + | BVLEFTSHIFT_1_TOK an_term an_term + { + unsigned int w = $2->GetValueWidth(); + unsigned int shift_amt = GetUnsignedConst(*$3); + if((unsigned)shift_amt < w) { + BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0); + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-shift_amt-1); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0); + BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + } + else { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + } + delete $2; + //delete $3; + } + | BVRIGHTSHIFT_TOK an_term NUMERAL_TOK + { + BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst($3, 0); + unsigned int w = $2->GetValueWidth(); + + //the amount by which you are rightshifting + //is less-than/equal-to the length of input + //bitvector + if((unsigned)$3 < w) { + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,$3); + BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-$3,*$2,hi,low); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + } + else { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + } + delete $2; + } + | BVRIGHTSHIFT_1_TOK an_term an_term + { + unsigned int shift_amt = GetUnsignedConst(*$3); + BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0); + unsigned int w = $2->GetValueWidth(); + + //the amount by which you are rightshifting + //is less-than/equal-to the length of input + //bitvector + if((unsigned)shift_amt < w) { + BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1); + BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,shift_amt); + BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low); + BEEV::ASTNode * n = + new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + } + else { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0)); + } + delete $2; + } + | BVSX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term + { + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + unsigned w = $5->GetValueWidth() + $3; + BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w); + BEEV::ASTNode *n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVSX,w,*$5,width)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $5; + } +; + +sort_symb: + BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + // Just return BV width. If sort is BOOL, width is 0. + // Otherwise, BITVEC[w] returns w. + // + //((indexwidth is 0) && (valuewidth>0)) iff type is BV + $$.indexwidth = 0; + unsigned int length = $3; + if(length > 0) { + $$.valuewidth = length; + } + else { + BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } + } + | ARRAY_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK + { + unsigned int index_len = $3; + unsigned int value_len = $5; + if(index_len > 0) { + $$.indexwidth = $3; + } + else { + BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } + + if(value_len > 0) { + $$.valuewidth = $5; + } + else { + BEEV::FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } + } +; + +var: + FORMID_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + delete $1; + } + | TERMID_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + delete $1; + } + | QUESTION_TOK TERMID_TOK + { + $$ = $2; + } +; + +fvar: + DOLLAR_TOK FORMID_TOK + { + $$ = $2; + } + | FORMID_TOK + { + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->ResolveID(*$1)); + delete $1; + } +; +%% |