diff options
Diffstat (limited to 'stp/parser/PL.y')
| -rw-r--r-- | stp/parser/PL.y | 1006 |
1 files changed, 0 insertions, 1006 deletions
diff --git a/stp/parser/PL.y b/stp/parser/PL.y deleted file mode 100644 index aa58aa4c..00000000 --- a/stp/parser/PL.y +++ /dev/null @@ -1,1006 +0,0 @@ -%{ -/******************************************************************** - * 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; - } - ; - -%% |