From d01f547e43a0e1a383ff61fbd58b023eebd3db34 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 15 Sep 2009 12:49:45 +0000 Subject: [PATCH] * Add signed & unsigned shifts to a test generator * Speed up the shifting circuit, by treating specially bits beyond log2 of the bitwidth. * During simplification if the shift amount is known, then remove the shift replacing it with a concat and extract. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@230 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 4 - src/simplifier/simplifier.cpp | 64 ++++++- src/to-sat/BitBlast.cpp | 240 +++++++++----------------- tests/generated_tests/Makefile | 2 + tests/generated_tests/mulDivRem.cpp | 43 +++-- tests/generated_tests/runMulDivRem.sh | 12 ++ 6 files changed, 185 insertions(+), 180 deletions(-) create mode 100644 tests/generated_tests/Makefile create mode 100755 tests/generated_tests/runMulDivRem.sh diff --git a/src/AST/AST.h b/src/AST/AST.h index 6385f8d..41190cf 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -941,10 +941,6 @@ namespace BEEV // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. ASTNode BBcompare(const ASTNode& form); - // Left and right shift one. Writes into x. - void BBLShift(ASTVec& x); - void BBRShift(ASTVec& x); - void BBRSignedShift(ASTVec& x, unsigned int shift); void BBLShift(ASTVec& x, unsigned int shift); void BBRShift(ASTVec& x, unsigned int shift); diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 8fb9aea..7513942 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -10,6 +10,7 @@ #include "../AST/AST.h" #include "../AST/ASTUtil.h" #include +#include namespace BEEV { @@ -2115,12 +2116,71 @@ ASTNode Flatten(const ASTNode& a) } break; } + + + case BVLEFTSHIFT: + case BVRIGHTSHIFT: + + { // If the shift amount is known. Then replace it by an extract. + ASTNode a = SimplifyTerm(inputterm[0], VarConstMap); + ASTNode b = SimplifyTerm(inputterm[1], VarConstMap); + const unsigned int width = a.GetValueWidth(); + if (BVCONST == b.GetKind()) // known shift amount. + { + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) + { + // Intended to remove shifts by very large amounts that don't fit into the unsigned. + // at thhe start of the "else" branch. + output = CreateZeroConst(width); + } + else + { + const unsigned int shift = GetUnsignedConst(b); + if (shift > width) + { + output = CreateZeroConst(width); + } + else if (shift == 0) + { + output = a; // unchanged. + } + else + { + if (k == BVLEFTSHIFT) + { + ASTNode zero = CreateZeroConst(shift); + ASTNode hi = CreateBVConst(32, width - shift -1); + ASTNode low = CreateBVConst(32, 0); + ASTNode extract = CreateTerm(BVEXTRACT, width - shift, a, hi, low); + BVTypeCheck(extract); + output = CreateTerm(BVCONCAT, width, extract, zero); + BVTypeCheck(output); + } + else if (k == BVRIGHTSHIFT) + { + ASTNode zero = CreateZeroConst(shift); + ASTNode hi = CreateBVConst(32, width ); + ASTNode low = CreateBVConst(32, shift+1); + ASTNode extract = CreateTerm(BVEXTRACT, width - shift, a, hi, low); + BVTypeCheck(extract); + output = CreateTerm(BVCONCAT, width, zero, extract); + BVTypeCheck(output); + } + else + FatalError("herasdf"); + } + } + } + else + output = CreateTerm(k, width, a, b); + } + break; + + case BVXOR: case BVXNOR: case BVNAND: case BVNOR: - case BVLEFTSHIFT: - case BVRIGHTSHIFT: case BVVARSHIFT: case BVSRSHIFT: case BVDIV: diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 88becd6..fd537c1 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -19,6 +19,8 @@ // The 0th element of the vector corresponds to bit 0 -- the low-order bit. #include "../AST/AST.h" +#include + namespace BEEV { // extern void lpvec(ASTVec &vec); @@ -45,17 +47,9 @@ namespace BEEV return it->second; } - // ASTNode& result = ASTJunk; ASTNode result; - /* - bool weregood = false; - if(term.GetNodeNum() == 17408){ - weregood = true; - } - */ - - Kind k = term.GetKind(); + const Kind k = term.GetKind(); if (!is_Term_kind(k)) FatalError("BBTerm: Illegal kind to BBTerm", term); @@ -73,121 +67,78 @@ namespace BEEV 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 the loop to finish after j=0, but when j=0, j-1 == MAX_INT. Hence this weird idiom. - if (j == 0) - done = true; - } - } - - result = CreateNode(BOOLVEC, temp_result); - } - break; - } - - case BVRIGHTSHIFT: - case BVSRSHIFT: - { - 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. - - if (BVRIGHTSHIFT == k) - BBRShift(children, shift); - else - BBRSignedShift(children, shift); - - result = CreateNode(BOOLVEC, children); - } - else - { - // Barrel shifter - const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); - const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); - - - // Signed right shift, need to copy the sign bit. - ASTNode toFill; - if (BVRIGHTSHIFT == k) - toFill = ASTFalse; - else - toFill = bbarg1.back(); - - 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 = 0; j < temp_result.size(); j++) - { - if (j + shift_amount >= temp_result.size()) - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); - else - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); - - if (j == 0) - done = true; - } - } - - result = CreateNode(BOOLVEC, temp_result); - - /* cerr << result << endl; - cerr << term[0] << endl; - cerr << term[1] << endl; - cerr << "right shift. Node size is:" << NodeSize(result) << endl; - cerr << "input size: " << NodeSize(term[0]) << " " << NodeSize(term[1]) << endl; - */ - } - } - break; + case BVRIGHTSHIFT: + case BVSRSHIFT: + case BVLEFTSHIFT: + { + // Barrel shifter + const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren(); + const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren(); + + // Signed right shift, need to copy the sign bit. + ASTNode toFill; + if (BVSRSHIFT == k) + toFill = bbarg1.back(); + else + toFill = ASTFalse; + + ASTVec temp_result(bbarg1); + // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero. + // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about + // 8.2 so round up to 9. + + const unsigned width = bbarg1.size(); + unsigned log2Width = log2(width) + 1; + + + if (k == BVSRSHIFT || k == BVRIGHTSHIFT) + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + unsigned int shift_amount = 1 << i; + + for (unsigned int j = 0; j < width; j++) + { + if (j + shift_amount >= width) + temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + else + temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); + } + } + else + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + int shift_amount = 1 << i; + + for (signed int j = width - 1; j > 0; j--) + { + if (j < shift_amount) + temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + else + temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]); + } + } + + // If any of the remainder are true. Then the whole thing gets the fill value. + ASTNode remainder = ASTFalse; + for (unsigned int i = log2Width; i < width; i++) + { + remainder = CreateNode(OR, remainder, bbarg2[i]); + } + + for (unsigned int i = 0; i < width; i++) + { + temp_result[i] = CreateSimpForm(ITE, remainder, toFill, temp_result[i]); + } + + result = CreateNode(BOOLVEC, temp_result); + } + break; case BVVARSHIFT: FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term); break; @@ -552,7 +503,7 @@ namespace BEEV CBV bv = term.GetBVConst(); for (unsigned int i = 0; i < num_bits; i++) { - tmp_res[i] = + tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv, i) ? ASTTrue : ASTFalse; } result = CreateNode(BOOLVEC, tmp_res); @@ -835,7 +786,7 @@ namespace BEEV for (xit++; xit < xend; xit++) { // shift first - BBLShift(ycopy); + BBLShift(ycopy,1); if (ASTFalse == *xit) { @@ -867,16 +818,16 @@ namespace BEEV { ASTVec q1, r1; ASTVec yrshift1(y); - BBRShift(yrshift1); + BBRShift(yrshift1,1); // recursively divide y/2 by x. BBDivMod(yrshift1, x, q1, r1, rwidth - 1); ASTVec q1lshift1(q1); - BBLShift(q1lshift1); + BBLShift(q1lshift1,1); ASTVec r1lshift1(r1); - BBLShift(r1lshift1); + BBLShift(r1lshift1,1); ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]); ASTVec rminusx(r1lshift1plusyodd); @@ -987,23 +938,6 @@ namespace BEEV 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); - } - // Left shift within fixed field inserting zeros at LSB. // Writes result into first argument. void BeevMgr::BBLShift(ASTVec& x, unsigned int shift) @@ -1054,20 +988,6 @@ namespace BEEV } } - // 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) { diff --git a/tests/generated_tests/Makefile b/tests/generated_tests/Makefile new file mode 100644 index 0000000..a9cee77 --- /dev/null +++ b/tests/generated_tests/Makefile @@ -0,0 +1,2 @@ +mudivrem: + g++ mulDivRem.cpp -m32 -Wno-deprecated -DTR1_UNORDERED_MAP -o muldiv -L../../lib -lstp \ No newline at end of file diff --git a/tests/generated_tests/mulDivRem.cpp b/tests/generated_tests/mulDivRem.cpp index 13b204e..7ab8e50 100644 --- a/tests/generated_tests/mulDivRem.cpp +++ b/tests/generated_tests/mulDivRem.cpp @@ -1,10 +1,10 @@ -#include +//#include #include #include #include #include -#include "../constantbv/constantbv.h" -#include "../AST/AST.h" +#include "../../src/AST/AST.h" +#include "../../src/extlib-constbv/constantbv.h" /* * Generates random (a op b = c) triples to check that solver. @@ -17,9 +17,9 @@ using std::cerr; using namespace BEEV; using namespace CONSTANTBV; -int width = 16; -typedef uint16_t uns; -typedef int16_t sig; +int width = 64; +typedef uint64_t uns; +typedef int64_t sig; const bool debug = false; @@ -38,7 +38,14 @@ uns getUnsignedResult(uns a, Kind k, uns b) else if (BVDIV == k) { return a / b; + }else if (BVLEFTSHIFT == k) + { + return (b > (sizeof(a) * 8) ? 0 : a << b); } + else if (BVRIGHTSHIFT == k) + { + return (b > (sizeof(a) * 8) ? 0 : a << b); + } cerr << "not implemetned" << endl; exit(2); @@ -68,6 +75,10 @@ sig getSignedResult(sig a, Kind k, sig b) { gold = a / b; } + else if (BVSRSHIFT == k) + { + return (b > (sizeof(a) * 8) ? 0 : a >> b); + } else { cerr << "not implemetned" << endl; @@ -77,7 +88,7 @@ sig getSignedResult(sig a, Kind k, sig b) } -void go(int count, uns a, uns b, uns result, char* name) +void go(int count, uns a, uns b, uns result, const char* name) { cout << ":extrafuns ((a" << count << " BitVec[" << width << "])) " << endl; cout << ":extrafuns ((b" << count << " BitVec[" << width << "])) " << endl; @@ -123,7 +134,7 @@ void testSolver(void) bS = rand(); } while (bS == 0 || b == 0); - switch (rand() % 6) + switch (rand() % 9) { case 0: go(0, a, b, getUnsignedResult(a, BVMULT, b), "bvmul"); @@ -143,6 +154,16 @@ void testSolver(void) case 5: go(5, aS, bS, getSignedResult(aS, SBVMOD, bS), "bvsmod"); break; + case 6: + go(5, aS, bS, getUnsignedResult(aS, BVLEFTSHIFT, bS), "bvshl"); + break; + case 7: + go(5, aS, bS, getUnsignedResult(aS, BVRIGHTSHIFT, bS), "bvshl"); + break; + case 8: + go(5, aS, bS, getSignedResult(aS, BVSRSHIFT, bS), "bvshl"); + break; + } cout << ")" << endl; @@ -164,12 +185,6 @@ int main(int argc, char**argv) BitVector_Boot(); - if (false) - { - testConstEval(SBVMOD); - testConstEval(SBVREM); - testConstEval(SBVDIV); - } testSolver(); return 0; diff --git a/tests/generated_tests/runMulDivRem.sh b/tests/generated_tests/runMulDivRem.sh new file mode 100755 index 0000000..486bf1d --- /dev/null +++ b/tests/generated_tests/runMulDivRem.sh @@ -0,0 +1,12 @@ +#!/bin/bash + +for i in {1..5000} +do + ./muldiv > file + result=`stp -d -m file` + if [ $result != "sat" ]; then + echo "failed" + exit + fi + echo $result +done -- 2.47.3