diff options
Diffstat (limited to 'stp/AST/BitBlast.cpp')
| -rw-r--r-- | stp/AST/BitBlast.cpp | 812 |
1 files changed, 0 insertions, 812 deletions
diff --git a/stp/AST/BitBlast.cpp b/stp/AST/BitBlast.cpp deleted file mode 100644 index de78ec74..00000000 --- a/stp/AST/BitBlast.cpp +++ /dev/null @@ -1,812 +0,0 @@ -/******************************************************************** - * AUTHORS: David L. Dill, Vijay Ganesh - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -// BitBlast -- convert bitvector terms and formulas to boolean -// formulas. A term is something that can represent a multi-bit -// bitvector, such as BVPLUS or BVXOR (or a BV variable or constant). -// A formula (form) represents a boolean value, such as EQ or BVLE. -// Bit blasting a term representing an n-bit bitvector with BBTerm -// yields a vector of n boolean formulas (returning ASTVec). -// Bit blasting a formula returns a single boolean formula (type ASTNode). - -// A bitblasted term is a vector of ASTNodes for formulas. -// The 0th element of the vector corresponds to bit 0 -- the low-order bit. - -#include "AST.h" -namespace BEEV { - // extern void lpvec(ASTVec &vec); - -// FIXME: Assert no zero-length bit vectors!!! -// FIXME: Need top-level functions that create and destroy the memo tables. -// FIXME: Check resource limits and generate an exception when exceeded. -// FIXME: THis does a lot of unnecessary copying of vectors. -// Had to be careful not to modify memoized vectors! -// FIXME: Might be some redundant variables. - -// accepts a term, and returns a vector of bitblasted bits(ASTVec) - -ASTNode ASTJunk; -const ASTNode BeevMgr::BBTerm(const ASTNode& term) { - //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo - ASTNodeMap::iterator it = BBTermMemo.find(term); - if (it != BBTermMemo.end()) { - // already there. Just return it. - return it->second; - } - -// ASTNode& result = ASTJunk; - ASTNode result; - - Kind k = term.GetKind(); - if (!is_Term_kind(k)) - FatalError("BBTerm: Illegal kind to BBTerm",term); - - ASTVec::const_iterator kids_end = term.end(); - unsigned int num_bits = term.GetValueWidth(); - switch (k) { - case BVNEG: { - // bitwise complement - // bitblast the child. - //FIXME Uses a tempory const ASTNode - const ASTNode& bbkids = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren())); - break; - } - case BVSRSHIFT: - case BVVARSHIFT: - FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); - break; - case ITE: { - // Term version of ITE. - - // Blast the args - // FIXME Uses temporary const ASTNodes and an ASTVec& - const ASTNode& cond = BBForm(term[0]); - const ASTNode& thn = BBTerm(term[1]); - const ASTNode& els = BBTerm(term[2]); - result = - 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. - const ASTNode& arg = term[0]; - unsigned long result_width = term.GetValueWidth(); - unsigned long arg_width = arg.GetValueWidth(); - //FIXME Uses a temporary const ASTNode reference - const ASTNode& bbarg = BBTerm(arg); - - if (result_width == arg_width) { - //nothing to sign extend - break; - } - else { - //we need to sign extend - const ASTNode& msbX = bbarg.back(); - //const ASTNode& msb1 = msbX; - - ASTVec ccc = msbX.GetChildren(); - const ASTNode& msb = CreateSimpForm(msbX.GetKind(),ccc); - - // Old version - // ASTNode msb = bbarg.back(); - // const ASTNode msb1 = msb; - - // ASTVec ccc = msb.GetChildren(); - // msb = CreateSimpForm(msb.GetKind(),ccc); - - // DD 1/14/07 Simplify silently drops all but first two args of XOR. - // I expanded XOR to N args with flattening optimization. - // This bug took 2 days to track down! - - // msb = SimplifyFormula(msb,false); - - // cout << "!!!!!!!!!!!!!!!!" << endl - // << "Simplify msb:" << msb2 << endl - // << "Simplify result:" << msb << endl; - - //FIXME Dynamically allocate the result vector? - //Is this doing multiple copies? - //ASTVec& tmp_res = *(new ASTVec(result_width)); - ASTVec tmp_res(result_width); - - //FIXME Should these be gotten from result? - ASTVec::const_iterator bb_it = bbarg.begin(); - ASTVec::iterator res_it = tmp_res.begin(); - ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part - ASTVec::iterator res_end = tmp_res.end(); - // copy LSBs directly from bbvec - for( ; res_it < res_ext; (res_it++, bb_it++)) { - *res_it = *bb_it; - } - // repeat MSB to fill up rest of result. - for( ; res_it < res_end; (res_it++, bb_it++)) { - *res_it = msb; - } - - //Temporary debugging code - // cout << "Sign extending:" << endl - // << " Vec "; - // lpvec( bbarg.GetChildren() ); - // cout << " Extended to "; - // lp(result); - // cout << endl; - - result = CreateNode(BOOLVEC, tmp_res); - - break; - } - } - case BVEXTRACT: { - // bitblast the child, then extract the relevant bits. - // Note: This could be optimized by not bitblasting the bits - // that aren't fetched. But that would be tricky, especially - // with memo-ization. - - //FIXME Using const ASTNode w/out reference - const ASTNode& bbkids = BBTerm(term[0]); - unsigned int high = GetUnsignedConst(term[1]); - unsigned int low = GetUnsignedConst(term[2]); - - ASTVec::const_iterator bbkfit = bbkids.begin(); - // I should have used pointers to ASTVec, to avoid this crock - - //FIXME Creates a new local ASTVec and does the CreateNode from that - result = CreateNode(BOOLVEC, ASTVec(bbkfit+low, bbkfit+high+1)); - break; - } - case BVCONCAT: { - //FIXME Using temporary const ASTNodes - const ASTNode& vec1 = BBTerm(term[0]); - const ASTNode& vec2 = BBTerm(term[1]); - - //FIXME This has to be an unnessecary copy and a memory leak - //Leaking ASTVec tmp_res = *(new ASTVec(vec2.GetChildren())); - ASTVec tmp_res(vec2.GetChildren()); - tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end()); - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVPLUS: { - // ASSERT: at least one child. - // ASSERT: all children and result are the same size. - // Previous phase must make sure this is true. - // Add children pairwise and accumulate in BBsum - - // FIXME: Unnecessary array copies. - ASTVec::const_iterator it = term.begin(); - ASTVec tmp_res = BBTerm(*it).GetChildren(); - for (++it; it < kids_end; it++) { - const ASTVec& tmp = BBTerm(*it).GetChildren(); - BBPlus2(tmp_res, tmp, ASTFalse); - } - - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVUMINUS: { - //FIXME Using const ASTNode reference - const ASTNode& bbkid = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren())); - break; - } - case BVSUB: { - // complement of subtrahend - // copy, since BBSub writes into it. - - //FIXME: Unnecessary array copies? - ASTVec tmp_res = BBTerm(term[0]).GetChildren(); - - const ASTVec& bbkid1 = BBTerm(term[1]).GetChildren(); - BBSub(tmp_res, bbkid1); - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BVMULT: { - // ASSERT 2 arguments, same length, result is same length. - - const ASTNode& t0 = term[0]; - const ASTNode& t1 = term[1]; - - const ASTNode& mpcd1 = BBTerm(t0); - const ASTNode& mpcd2 = BBTerm(t1); - //Reverese the order of the nodes w/out the need for temporaries - //This is needed because t0 an t1 must be const - if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { - result = CreateNode(BOOLVEC, - BBMult(mpcd2.GetChildren(), mpcd1.GetChildren()) ); - }else{ - result = CreateNode(BOOLVEC, - BBMult(mpcd1.GetChildren(), mpcd2.GetChildren()) ); - } - break; - } - case BVDIV: - case BVMOD: { - const ASTNode& dvdd = BBTerm(term[0]); - const ASTNode& dvsr = BBTerm(term[1]); - unsigned int width = dvdd.Degree(); - ASTVec q(width); - ASTVec r(width); - BBDivMod(dvdd.GetChildren(), dvsr.GetChildren(), q, r, width); - if (k == BVDIV) - result = CreateNode(BOOLVEC, q); - else - result = CreateNode(BOOLVEC, r); - break; - } - // n-ary bitwise operators. - case BVXOR: - case BVXNOR: - case BVAND: - case BVOR: - case BVNOR: - case BVNAND: { - // Add children pairwise and accumulate in BBsum - ASTVec::const_iterator it = term.begin(); - Kind bk = UNDEFINED; // Kind of individual bit op. - switch (k) { - case BVXOR: bk = XOR; break; - case BVXNOR: bk = IFF; break; - case BVAND: bk = AND; break; - case BVOR: bk = OR; break; - case BVNOR: bk = NOR; break; - case BVNAND: bk = NAND; break; - default: - FatalError("BBTerm: Illegal kind to BBTerm",term); - break; - } - - // Sum is destructively modified in the loop, so make a copy of value - // returned by BBTerm. - ASTNode temp = BBTerm(*it); - ASTVec sum(temp.GetChildren()); // First operand. - - // Iterate over remaining bitvector term operands - for (++it; it < kids_end; it++) { - //FIXME FIXME FIXME: Why does using a temp. var change the behavior? - temp = BBTerm(*it); - const ASTVec& y = temp.GetChildren(); - - // Iterate over bits - // FIXME: Why is this not using an iterator??? - int n = y.size(); - for (int i = 0; i < n; i++) { - sum[i] = CreateSimpForm(bk, sum[i], y[i]); - } - } - result = CreateNode(BOOLVEC, sum); - break; - } - case SYMBOL: { - // ASSERT: IndexWidth = 0? Semantic analysis should check. - //Leaking ASTVec& bbvec = *(new ASTVec); - - //FIXME Why is isn't this ASTVEC bbvec(num_bits) ? - ASTVec bbvec; - for (unsigned int i = 0; i < num_bits; i++) { - ASTNode bit_node = - CreateNode(BVGETBIT, term, CreateBVConst(32,i)); - bbvec.push_back(bit_node); - } - result = CreateNode(BOOLVEC, bbvec); - break; - } - case BVCONST: { - ASTVec tmp_res(num_bits); -#ifndef NATIVE_C_ARITH - CBV bv = term.GetBVConst(); - for(unsigned int i = 0; i < num_bits; i++){ - tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv,i) ? ASTTrue : ASTFalse; - } -#else - const unsigned long long int c = term.GetBVConst(); - unsigned long long int bitmask = 0x00000000000000001LL; - for (unsigned int i = 0; i < num_bits; i++, bitmask <<= 1) - tmp_res[i] = ((c & (bitmask)) ? ASTTrue : ASTFalse); -#endif - result = CreateNode(BOOLVEC, tmp_res); - break; - } - case BOOLVEC: { - cerr << "Hit a boolvec! what to do?" << endl; - break; - } - default: - FatalError("BBTerm: Illegal kind to BBTerm",term); - } - - //if(result == ASTJunk) - // cout<<"result does not change"<<endl; - // cout << "================" << endl << "BBTerm:" << term << endl; - // cout << "----------------" << endl << "BBTerm result:"; - // lpvec(result); - // cout << endl; - - return (BBTermMemo[term] = result); - -} - -// bit blast a formula (boolean term). Result is one bit wide, -// so it returns a single ASTNode. -// FIXME: Add IsNegated flag. -const ASTNode BeevMgr::BBForm(const ASTNode& form) -{ - - ASTNodeMap::iterator it = BBFormMemo.find(form); - if (it != BBFormMemo.end()) { - // already there. Just return it. - return it->second; - } - - ASTNode result = ASTUndefined; - - Kind k = form.GetKind(); - if (!is_Form_kind(k)) { - FatalError("BBForm: Illegal kind: ",form); - } - - // Not returning until end, and memoizing everything, makes it easier - // to trace coherently. - - // Various special cases - switch (k) { - case TRUE: - case FALSE: { - result = form; - break; - } - - case SYMBOL: - if (form.GetType() != BOOLEAN_TYPE) { - FatalError("BBForm: Symbol represents more than one bit", form); - } - - result = form; - break; - - case BVGETBIT: { - // exactly two children - const ASTNode bbchild = BBTerm(form[0]); - unsigned int index = GetUnsignedConst(form[1]); - result = bbchild[index]; - break; - } - - case NOT: - result = CreateSimpNot(BBForm(form[0])); - break; - - case ITE: - // FIXME: SHould this be CreateSimpITE? - result = CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2])); - break; - - case AND: - case OR: - case NAND: - case NOR: - case IFF: - case XOR: - case IMPLIES: { - ASTVec bbkids; // bit-blasted children (formulas) - - // FIXME: Put in fast exits for AND/OR/NAND/NOR/IMPLIES - ASTVec::const_iterator kids_end = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) { - bbkids.push_back(BBForm(*it)); - } - result = CreateSimpForm(k, bbkids); - break; - } - - case NEQ: { - ASTNode bbkid = BBForm(CreateNode(EQ, form.GetChildren())); - result = CreateSimpNot(bbkid); - break; - } - - case EQ: { - // Common code for binary operations - // FIXME: This ought to be in a semantic analysis phase. - const ASTNode left = BBTerm(form[0]); - const ASTNode right = BBTerm(form[1]); - if (left.Degree() != right.Degree()) { - cerr << "BBForm: Size mismatch" << endl << form[0] << endl << form[1] << endl; - FatalError("",ASTUndefined); - } - result = BBEQ(left.GetChildren(), right.GetChildren()); - break; - } - - case BVLE: - case BVGE: - case BVGT: - case BVLT: - case BVSLE: - case BVSGE: - case BVSGT: - case BVSLT: { - result = BBcompare(form); - break; - } - default: - FatalError("BBForm: Illegal kind: ", form); - break; - } - - // cout << "================" << endl - // << "BBForm: " << form << endl - // << "----------------" << endl - // << "BBForm Result: " << result << endl; - - return (BBFormMemo[form] = result); -} - -// Bit blast a sum of two equal length BVs. -// Update sum vector destructively with new sum. -void BeevMgr::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin) -{ -// cout << "Bitblasting plus. Operand 1: " << endl; -// lpvec(sum); -// cout << endl << " operand 2: " << endl; -// lpvec(y); -// cout << endl << "carry: " << endl << cin << endl; - - - int n = sum.size(); - // ASSERT: y.size() == x.size() - // FIXME: Don't bother computing i+1 carry, which is discarded. - for (int i = 0; i < n; i++) { - ASTNode nextcin = Majority(sum[i], y[i], cin); - sum[i] = CreateSimpForm(XOR, CreateSimpForm(XOR, sum[i], y[i]), cin); - cin = nextcin; - } - -// cout << "----------------" << endl << "Result: " << endl; -// lpvec(sum); -// cout << endl; - -} - -// Stores result - x in result, destructively -void BeevMgr::BBSub(ASTVec& result, const ASTVec& y) -{ - ASTVec compsubtrahend = BBNeg(y); - BBPlus2(result, compsubtrahend, ASTTrue); -} - -// Add one bit -ASTVec BeevMgr::BBAddOneBit(ASTVec& x, ASTNode cin) -{ - ASTVec result = ASTVec(0); - ASTVec::const_iterator itend = x.end(); - for (ASTVec::const_iterator it = x.begin(); it < itend; it++) { - ASTNode nextcin = CreateSimpForm(AND, *it, cin); - result.push_back(CreateSimpForm(XOR, *it, cin)); - cin = nextcin; - } - // FIXME: unnecessary array copy on return? - return result; -} - -// Increment bit-blasted vector and return result. -ASTVec BeevMgr::BBInc(ASTVec& x) -{ - return BBAddOneBit(x, ASTTrue); -} - -// Return formula for majority function of three bits. -// Pass arguments by reference to reduce refcounting. -ASTNode BeevMgr::Majority(const ASTNode& a, const ASTNode& b,const ASTNode& c) -{ - // Checking explicitly for constant a, b and c could - // be more efficient, because they are repeated in the logic. - if (ASTTrue == a) { - return CreateSimpForm(OR, b, c); - } - else if (ASTFalse == a) { - return CreateSimpForm(AND, b, c); - } - else if (ASTTrue == b) { - return CreateSimpForm(OR, a, c); - } - else if (ASTFalse == b) { - return CreateSimpForm(AND, a, c); - } - else if (ASTTrue == c) { - return CreateSimpForm(OR, a, b); - } - else if (ASTFalse == c) { - return CreateSimpForm(AND, a, b); - } - // there are lots more simplifications, but I'm not sure they're - // worth doing explicitly (e.g., a = b, a = ~b, etc.) - else { - return - CreateSimpForm(OR, - CreateSimpForm(AND, a, b), - CreateSimpForm(AND, b, c), - CreateSimpForm(AND, a, c)); - } -} - - -// Bitwise complement -ASTVec BeevMgr::BBNeg(const ASTVec& x) -{ - ASTVec result = ASTVec(0); // FIXME: faster to preallocate n entries? - // Negate each bit. - ASTVec::const_iterator xend = x.end(); - for (ASTVec::const_iterator it = x.begin(); it < xend; it++) { - result.push_back(CreateSimpNot(*it)); - } - // FIXME: unecessary array copy when it returns? - return result; -} - -// Compute unary minus -ASTVec BeevMgr::BBUminus(const ASTVec& x) -{ - ASTVec xneg = BBNeg(x); - return BBInc(xneg); -} - -// Multiply two bitblasted numbers -ASTVec BeevMgr::BBMult(const ASTVec& x, const ASTVec& y) -{ - ASTVec ycopy(y); - ASTVec::const_iterator xend = x.end(); - ASTVec::const_iterator xit = x.begin(); - // start prod with first partial product. - // FIXME: This is unnecessary. Clean it up. - ASTVec prod = ASTVec(BBAndBit(y, *xit)); - // start loop at next bit. - for(xit++; xit < xend; xit++) { - // shift first - BBLShift(ycopy); - - if (ASTFalse == *xit) { - // If this bit is zero, the partial product will - // be zero. No reason to add that in. - continue; - } - - ASTVec pprod = BBAndBit(ycopy, *xit); - // accumulate in the product. - BBPlus2(prod, pprod, ASTFalse); - } - return prod; -} - -// This implements a variant of binary long division. -// q and r are "out" parameters. rwidth puts a bound on the -// recursion depth. -void BeevMgr::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth) -{ - unsigned int width = y.size(); - if (rwidth == 0) { - // When we have shifted the entire width, y is guaranteed to be 0. - q = BBfill(width, ASTFalse); - r = BBfill(width, ASTFalse); - } - else { - ASTVec q1, r1; - ASTVec yrshift1(y); - BBRShift(yrshift1); - - // recursively divide y/2 by x. - BBDivMod(yrshift1, x, q1, r1, rwidth-1); - - ASTVec q1lshift1(q1); - BBLShift(q1lshift1); - - ASTVec r1lshift1(r1); - BBLShift(r1lshift1); - - ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]); - ASTVec rminusx(r1lshift1plusyodd); - BBSub(rminusx, x); - - // Adjusted q, r values when when r is too large. - ASTNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false); - ASTVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1); - ASTVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd); - - // q & r values when y >= x - ASTNode yeqx = BBEQ(y, x); - // *** Problem: the bbfill for qval is wrong. Should be 1, not -1. - ASTVec one = BBfill(width, ASTFalse); - one[0] = ASTTrue; - ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval); - ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval); - // y < x <=> not x >= y. - ASTNode ylessx = CreateSimpNot(BBBVLE(x, y, false)); - // final values of q and r - q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval); - r = BBITE(ylessx, y, notylessxrval); - } -} - -// build ITE's (ITE cond then[i] else[i]) for each i. -ASTVec BeevMgr::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els) -{ - // Fast exits. - if (ASTTrue == cond) { - return thn; - } - else if (ASTFalse == cond) { - return els; - } - - ASTVec result(0); - ASTVec::const_iterator th_it_end = thn.end(); - ASTVec::const_iterator el_it = els.begin(); - for (ASTVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { - result.push_back(CreateSimpForm(ITE, cond, *th_it, *el_it)); - } - return result; -} -// AND each bit of vector y with single bit b and return the result. -ASTVec BeevMgr::BBAndBit(const ASTVec& y, ASTNode b) -{ - ASTVec result(0); - - if (ASTTrue == b) { - return y; - } - // FIXME: put in fast exits when b is constant 0. - - ASTVec::const_iterator yend = y.end(); - for(ASTVec::const_iterator yit = y.begin(); yit < yend; yit++) { - result.push_back(CreateSimpForm(AND, *yit, b)); - } - return result; -} - - -// Workhorse for comparison routines. This does a signed BVLE if is_signed -// is true, else it's unsigned. All other comparison operators can be reduced -// to this by swapping args or complementing the result bit. -// FIXME: If this were done MSB first, it would enable a fast exit sometimes -// when the MSB is constant, deciding the result without looking at the rest -// of the bits. -ASTNode BeevMgr::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed) -{ - // "thisbit" represents BVLE of the suffixes of the BVs - // from that position . if R < L, return TRUE, else if L < R - // return FALSE, else return BVLE of lower-order bits. MSB is - // treated separately, because signed comparison is done by - // complementing the MSB of each BV, then doing an unsigned - // comparison. - ASTVec::const_iterator lit = left.begin(); - ASTVec::const_iterator litend = left.end(); - ASTVec::const_iterator rit = right.begin(); - ASTNode prevbit = ASTTrue; - for ( ; lit < litend-1; lit++, rit++) { - ASTNode neglit = CreateSimpNot(*lit); - ASTNode thisbit = - CreateSimpForm(OR, - CreateSimpForm(AND,neglit,*rit), // TRUE if l < r - CreateSimpForm(AND, - CreateSimpForm(OR, neglit, *rit), // false if not equal - prevbit)); // else prevbit - prevbit = thisbit; - } - - // Handle MSB -- negate MSBs if signed comparison - // FIXME: make into refs after it's debugged. - ASTNode lmsb = *lit; - ASTNode rmsb = *rit; - if (is_signed) { - lmsb = CreateSimpNot(*lit); - rmsb = CreateSimpNot(*rit); - } - - ASTNode neglmsb = CreateSimpNot(lmsb); - ASTNode msb = - CreateSimpForm(OR, - CreateSimpForm(AND,neglmsb, rmsb), // TRUE if l < r - CreateSimpForm(AND, - CreateSimpForm(OR, neglmsb, rmsb), // false if not equal - prevbit)); // else prevbit - return msb; -} - -// Left shift by 1 within fixed field inserting zeros at LSB. -// Writes result into first argument. -// Fixme: generalize to n bits -void BeevMgr::BBLShift(ASTVec& x) -{ - // 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(); - for(ASTVec::iterator xit = x.end()-1; xit > xbeg; xit--) { - *xit = *(xit-1); - } - *xbeg = ASTFalse; // new LSB is zero. - // cout << "Shifted result" << endl; - // lpvec(x); -} - -// Right shift by 1 within fixed field, inserting new zeros at MSB. -// Writes result into first argument. -// Fixme: generalize to n bits. -void BeevMgr::BBRShift(ASTVec& x) -{ - ASTVec::iterator xend = x.end() - 1; - ASTVec::iterator xit = x.begin(); - for( ; xit < xend; xit++) { - *xit = *(xit+1); - } - *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]); - const ASTNode rnode = BBTerm(form[1]); - const ASTVec& left = lnode.GetChildren(); - const ASTVec& right = rnode.GetChildren(); - - //const ASTVec& left = BBTerm(form[0]).GetChildren(); - //const ASTVec& right = BBTerm(form[1]).GetChildren(); - - Kind k = form.GetKind(); - switch(k) { - case BVLE: { return BBBVLE(left, right, false); break; } - case BVGE: { return BBBVLE(right, left, false); break; } - case BVGT: { return CreateSimpNot(BBBVLE(left, right, false)); break; } - case BVLT: { return CreateSimpNot(BBBVLE(right, left, false)); break; } - case BVSLE: { return BBBVLE(left, right, true); break; } - case BVSGE: { return BBBVLE(right, left, true); break; } - case BVSGT: { return CreateSimpNot(BBBVLE(left, right, true)); break; } - case BVSLT: { return CreateSimpNot(BBBVLE(right, left, true)); break; } - default: - cerr << "BBCompare: Illegal kind" << form << endl; - FatalError("",ASTUndefined); - } - return ASTUndefined; -} - - -// return a vector with n copies of fillval -ASTVec BeevMgr::BBfill(unsigned int width, ASTNode fillval) -{ - ASTVec zvec(width, fillval); - return zvec; -} - -ASTNode BeevMgr::BBEQ(const ASTVec& left, const ASTVec& right) -{ - ASTVec andvec; - ASTVec::const_iterator lit = left.begin(); - ASTVec::const_iterator litend = left.end(); - ASTVec::const_iterator rit = right.begin(); - - if(left.size() > 1) { - for(; lit != litend; lit++, rit++) { - ASTNode biteq = CreateSimpForm(IFF, *lit, *rit); - // fast path exit - if (biteq == ASTFalse) { - return ASTFalse; - } - else { - andvec.push_back(biteq); - } - } - ASTNode n = CreateSimpForm(AND, andvec); - return n; - } - else - return CreateSimpForm(IFF,*lit,*rit); -} -} // BEEV namespace |