diff options
Diffstat (limited to 'stp/AST/BitBlast.cpp')
| -rw-r--r-- | stp/AST/BitBlast.cpp | 812 |
1 files changed, 812 insertions, 0 deletions
diff --git a/stp/AST/BitBlast.cpp b/stp/AST/BitBlast.cpp new file mode 100644 index 00000000..de78ec74 --- /dev/null +++ b/stp/AST/BitBlast.cpp @@ -0,0 +1,812 @@ +/******************************************************************** + * 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 |