diff options
Diffstat (limited to 'stp/parser/PL.y')
| -rw-r--r-- | stp/parser/PL.y | 1006 |
1 files changed, 1006 insertions, 0 deletions
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; + } + ; + +%% |