From 6da5197fcbea405edebbefad553d8ea2f4fb8303 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 6 Jan 2009 12:38:33 +0000 Subject: [PATCH] Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM. Now left shifts by a variable amount. Previously the shift amount needed to a constant. The smtlib parser reads bitvector constants into strings rather than into ints. This allows formula to contain constants greater than the size of the machine's integer. Fixed zero_extend. I didn't add code for it into the SimplifyTermAux function. SBVREM was sometimes failing because it also wasn't included in the same function. Added it in. Not sure what the function does though.. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@51 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 34 +++++++++++- AST/AST.h | 26 +++++++-- AST/BitBlast.cpp | 111 +++++++++++++++++++++++++++++++++++++- bitvec/consteval.cpp | 30 +++++++++++ parser/smtlib.lex | 2 +- parser/smtlib.y | 58 ++++++-------------- simplifier/simplifier.cpp | 17 +++++- 7 files changed, 226 insertions(+), 52 deletions(-) diff --git a/AST/AST.cpp b/AST/AST.cpp index 1a3db0b..2ecff2f 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -786,7 +786,7 @@ namespace BEEV { CBV bv = CONSTANTBV::BitVector_Create(width, true); - unsigned long c_val = (0x00000000ffffffffLL) & bvconst; + unsigned long c_val = (~((unsigned long)0)) & bvconst; unsigned int copied = 0; // sizeof(unsigned long) returns the number of bytes in unsigned @@ -801,13 +801,43 @@ namespace BEEV { while(copied + (sizeof(unsigned long)<<3) < width){ CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val); bvconst = bvconst >> (sizeof(unsigned long) << 3); - c_val = (0x00000000ffffffffLL) & bvconst; + c_val = (~((unsigned long)0)) & bvconst; copied += sizeof(unsigned long) << 3; } CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val); return CreateBVConst(bv,width); } + ASTNode BeevMgr::CreateBVConst(string*& strval, unsigned int base, size_t bit_width) { + + if(!(2 == base || 10 == base || 16 == base)) + { + FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base); + } + + //checking if the input is in the correct format + CBV bv = CONSTANTBV::BitVector_Create(bit_width,true); + CONSTANTBV::ErrCode e; + if(2 == base){ + e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*) strval->c_str()); + }else if(10 == base){ + e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*) strval->c_str()); + }else if(16 == base){ + e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*) strval->c_str()); + }else{ + e = CONSTANTBV::ErrCode_Pars; + } + + if(0 != e) { + cerr << "CreateBVConst: " << BitVector_Error(e); + FatalError("",ASTUndefined); + } + + return CreateBVConst(bv, bit_width); + } + + + //Create a ASTBVConst node from std::string ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) { size_t width = strlen((const char *)strval); diff --git a/AST/AST.h b/AST/AST.h index 04f3528..27d090e 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -687,12 +687,23 @@ namespace BEEV { CBV GetBVConst() const {return _bvconst;} }; //End of ASTBVConst - //FIXME This function is DEPRICATED + + //FIXME This function is DEPRECATED //Do not use in the future - inline unsigned int GetUnsignedConst(const ASTNode n) { - if(32 < n.GetValueWidth()) - FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:"); - + inline unsigned int GetUnsignedConst(const ASTNode n) + { + if(sizeof(unsigned int) * 8 <= n.GetValueWidth()) + { + // It may only contain a small value in a bit type, which fits nicely into an unsigned int. + // This is common for functions like: bvshl(bv1[128], bv1[128]) + // where both operands have the same type. + unsigned long maxBit = (unsigned) CONSTANTBV::Set_Max(n.GetBVConst()); + if (maxBit >= sizeof(unsigned int) * 8 ) + { + n.LispPrint(cerr); //print the node so they can find it. + FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int"); + } + } return (unsigned int) *((unsigned int *)n.GetBVConst()); } #else @@ -1216,6 +1227,9 @@ namespace BEEV { void BBLShift(ASTVec& x); void BBRShift(ASTVec& x); + void BBLShift(ASTVec& x, unsigned int shift); + void BBRShift(ASTVec& x, unsigned int shift); + public: // Simplifying create functions ASTNode CreateSimpForm(Kind kind, ASTVec &children); @@ -1350,12 +1364,14 @@ namespace BEEV { // Create and return an ASTNode for a symbol // Width is number of bits. + ASTNode CreateBVConst(string*& strval, unsigned int base, size_t bit_width); ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); ASTNode CreateZeroConst(unsigned int width); ASTNode CreateOneConst(unsigned int width); ASTNode CreateTwoConst(unsigned int width); ASTNode CreateMaxConst(unsigned int width); + // Create and return an ASTNode for a symbol // Optional base was a problem because 0 could be an int or char *, // so CreateBVConst was ambiguous. diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp index 7ebf2de..7ead02c 100644 --- a/AST/BitBlast.cpp +++ b/AST/BitBlast.cpp @@ -69,6 +69,78 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) { result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren())); break; } + + case BVLEFTSHIFT: + { + if (BVCONST == term[1].GetKind()) + { + // Constant shifts should be removed during simplification. + unsigned int shift = GetUnsignedConst(term[1]); + + ASTNode term0 = BBTerm(term[0]); + ASTVec children(term0.GetChildren()); // mutable copy of the children. + BBLShift(children, shift); + + result = CreateNode(BOOLVEC, children); + } + else + { + // Barrel shifter + const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); + const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); + + ASTVec temp_result(bbarg1); + + for (unsigned int i =0; i < bbarg2.size(); i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + unsigned int shift_amount = 1 << i; + + bool done = false; + + for (unsigned int j=temp_result.size()-1; !done; j--) + { + if (j < shift_amount) + temp_result[j] = CreateSimpForm(ITE, bbarg2[i],ASTFalse,temp_result[j]); + else + temp_result[j] = CreateSimpForm(ITE, bbarg2[i],temp_result[j-shift_amount],temp_result[j]); + + // want it to stop after doing 0, but subtracting 1 from j makes it very big. + if (j ==0) + done = true; + } + } + + result = CreateNode(BOOLVEC, temp_result); + } + break; + } + + case BVRIGHTSHIFT: + { + if (BVCONST == term[1].GetKind()) + { + // Constant shifts should be removed during simplification. + + unsigned int shift = GetUnsignedConst(term[1]); + + ASTNode term0 = BBTerm(term[0]); + ASTVec children(term0.GetChildren()); // mutable copy of the children. + BBRShift(children, shift); + + result = CreateNode(BOOLVEC, children); + } + else + { + FatalError("Not implemented shift right by unk. value."); + } + } + break; + + + case BVSRSHIFT: case BVVARSHIFT: FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); @@ -86,6 +158,8 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) { CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren())); break; } + + case BVSX: { // Replicate high-order bit as many times as necessary. // Arg 0 is expression to be sign extended. @@ -139,7 +213,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) { *res_it = *bb_it; } // repeat MSB to fill up rest of result. - for( ; res_it < res_end; (res_it++, bb_it++)) { + for( ; res_it < res_end; (res_it++)) { *res_it = msb; } @@ -841,6 +915,40 @@ void BeevMgr::BBLShift(ASTVec& x) // lpvec(x); } +// Left shift within fixed field inserting zeros at LSB. +// Writes result into first argument. + void BeevMgr::BBLShift(ASTVec& x, unsigned int shift) +{ + // left shift x (destructively) within width. + // loop backwards so that copy to self works correctly. (DON'T use STL insert!) + ASTVec::iterator xbeg = x.begin(); + ASTVec::iterator xit = x.end()-1; + for(; xit >= xbeg; xit--) { + if (xit-shift >= xbeg) + *xit = *(xit-shift); + else + *xit= ASTFalse; // new LSB is zero. + } +} + +// Right shift within fixed field inserting zeros at MSB. +// Writes result into first argument. + void BeevMgr::BBRShift(ASTVec& x, unsigned int shift) +{ + // right shift x (destructively) within width. + ASTVec::iterator xend = x.end(); + ASTVec::iterator xit = x.begin(); + for(; xit < xend; xit++) { + if (xit+shift < xend) + *xit = *(xit+shift); + else + *xit= ASTFalse; // new MSB is zero. + } +} + + + + // Right shift by 1 within fixed field, inserting new zeros at MSB. // Writes result into first argument. // Fixme: generalize to n bits. @@ -854,7 +962,6 @@ void BeevMgr::BBRShift(ASTVec& x) *xit = ASTFalse; // new MSB is zero. } - // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. ASTNode BeevMgr::BBcompare(const ASTNode& form) { const ASTNode lnode = BBTerm(form[0]); diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp index b2700ee..8683763 100644 --- a/bitvec/consteval.cpp +++ b/bitvec/consteval.cpp @@ -96,6 +96,36 @@ namespace BEEV { } + case BVLEFTSHIFT: + { + output = CONSTANTBV::BitVector_Create(inputwidth,true); + + // the shift is destructive, get a copy. + CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth); + + // get the number of bits to shift it. + unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1])); + + CONSTANTBV::BitVector_Move_Left(output,shift); + OutputNode = CreateBVConst(output,outputwidth); + break; + } + case BVRIGHTSHIFT: + { + output = CONSTANTBV::BitVector_Create(inputwidth,true); + + // the shift is destructive, get a copy. + CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth); + + // get the number of bits to shift it. + unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1])); + + CONSTANTBV::BitVector_Move_Right(output,shift); + OutputNode = CreateBVConst(output,outputwidth); + break; + } + + case BVAND: { output = CONSTANTBV::BitVector_Create(inputwidth,true); CONSTANTBV::Set_Intersection(output,tmp0,tmp1); diff --git a/parser/smtlib.lex b/parser/smtlib.lex index 7070686..5d5f1a6 100644 --- a/parser/smtlib.lex +++ b/parser/smtlib.lex @@ -79,7 +79,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) {DIGIT}+ { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; } -bv{DIGIT}+ { yylval.ullval = strtoull(yytext+2, NULL, 10); return BVCONST_TOK; } + bv{DIGIT}+ { yylval.str = new std::string(yytext+2); return BVCONST_TOK; } bit{DIGIT}+ { char c = yytext[3]; diff --git a/parser/smtlib.y b/parser/smtlib.y index 52215ec..3da4090 100644 --- a/parser/smtlib.y +++ b/parser/smtlib.y @@ -99,7 +99,7 @@ %type user_value %token NUMERAL_TOK -%token BVCONST_TOK +%token BVCONST_TOK %token BITCONST_TOK %token FORMID_TOK TERMID_TOK %token STRING_TOK @@ -671,11 +671,12 @@ an_terms: an_term: BVCONST_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(64, $1)); + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1, 10, 32)); } | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK { - $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($3, $1)); + $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1,10,$3)); + delete $1; } | an_nonbvconst_term ; @@ -1018,24 +1019,22 @@ an_nonbvconst_term: delete $2; } | BVLEFTSHIFT_1_TOK an_term an_term +{ + // shifting left by who know how much? + unsigned int w = $2->GetValueWidth(); + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVLEFTSHIFT,w,*$2,*$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $2; + } + | BVRIGHTSHIFT_1_TOK an_term an_term { + // shifting right by who know how much? 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)); - } + BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVRIGHTSHIFT,w,*$2,*$3)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; delete $2; - //delete $3; } | BVRIGHTSHIFT_TOK an_term NUMERAL_TOK { @@ -1059,29 +1058,6 @@ an_nonbvconst_term: } 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; - } | BVARITHRIGHTSHIFT_TOK an_term an_term { unsigned int shift_amt = GetUnsignedConst(*$3); diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index fc715f6..6e49414 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -2020,6 +2020,20 @@ namespace BEEV { } break; } + case BVZX: + { + //a0 is the expr which is being zero extended + ASTNode a0 = SimplifyTerm(inputterm[0]); + //a1 represents the length of the term BVZX(a0) + ASTNode a1 = inputterm[1]; + //output length of the BVSX term + unsigned len = inputValueWidth; + + output = CreateTerm(BVZX,len,a0,a1); + break; + } + break; + case BVSX:{ //a0 is the expr which is being sign extended ASTNode a0 = SimplifyTerm(inputterm[0]); @@ -2232,6 +2246,7 @@ namespace BEEV { output = CreateSimplifiedTermITE(t0,t1,t2); break; } + case SBVREM: case SBVMOD: case SBVDIV: { ASTVec c = inputterm.GetChildren(); @@ -2245,7 +2260,7 @@ namespace BEEV { } case WRITE: default: - FatalError("SimplifyTerm: Control should never reach here:", inputterm, k); + FatalError("SimplifyTermAux: Control should never reach here:", inputterm, k); return inputterm; break; } -- 2.47.3