From e77ad2f363f66797fac28062b49b73bc0f416829 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 29 Aug 2009 14:26:52 +0000 Subject: [PATCH] * Test file generator for mul, div, rem. * Speed up the signed div, signed mod & signed rem encodings. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@160 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/Transform.cpp | 74 ++++-------- tests/generated_tests/mulDivRem.cpp | 177 ++++++++++++++++++++++++++++ 2 files changed, 203 insertions(+), 48 deletions(-) create mode 100644 tests/generated_tests/mulDivRem.cpp diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 771e25c..e8f6acc 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -36,22 +36,19 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) if (SBVREM == in.GetKind()) { - //if(TopBit(dividend)==1) - // - //then -BVMOD(-dividend,abs(divisor)) - // - //else BVMOD(dividend,abs(divisor)) + //BVMOD is an expensive operation. So have the fewest bvmods possible. Just one. + + //Take absolute value. + ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); - //create the condition and conditional for the divisor - ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); + //create the modulus term + ASTNode modnode = CreateTerm(BVMOD, len, pos_dividend, pos_divisor); - //create the modulus term for each case - ASTNode modnode = CreateTerm(BVMOD, len, dividend, pos_divisor); - ASTNode minus_modnode = CreateTerm(BVMOD, len, CreateTerm(BVUMINUS, len, dividend), pos_divisor); - minus_modnode = CreateTerm(BVUMINUS, len, minus_modnode); + //If the dividend is <0 take the unary minus. + ASTNode n = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, modnode), modnode); //put everything together, simplify, and return - ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode); return SimplifyTerm_TopLevel(n); } @@ -69,33 +66,21 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) // (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) // (bvadd (bvurem s (bvneg t)) t) // (bvneg (bvurem (bvneg s) (bvneg t))))))) - ASTNode & s = dividend; - ASTNode & t = divisor; - ASTNode isSNeg = cond_dividend; // (= ?msb_s bit1) - ASTNode isSPos = CreateNode(NOT, isSNeg); // (= ?msb_s bit0) + //Take absolute value. + ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode isTNeg = cond_divisor; // (= ?msb_t bit1) - ASTNode isTPos = CreateNode(NOT, isTNeg); // (= ?msb_t bit0) + ASTNode urem_node = CreateTerm(BVMOD, len, pos_dividend, pos_divisor); + // If the dividend is <0, then we negate the whole thing. + ASTNode rev_node = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node); - ASTNode negS = CreateTerm(BVUMINUS, len, s); // (bvneg s) - ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg t) + // if It's XOR <0 then add t (not its absolute value). + ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); - // (bvneg (bvurem (bvneg s) (bvneg t))) - ASTNode branch4 = CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, negT)); - // (bvadd (bvurem s (bvneg t)) t) - ASTNode branch3 = CreateTerm(BVPLUS, len, CreateTerm(BVMOD, len, s, negT), t); - // (bvadd (bvneg (bvurem (bvneg s) t)) t) - ASTNode branch2 = CreateTerm(BVPLUS, len, CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, t)), t); - // (bvurem s t) - ASTNode branch1 = CreateTerm(BVMOD, len, s, t); - - ASTNode ite3 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTNeg), branch3, branch4); - ASTNode ite2 = CreateTerm(ITE, len, CreateNode(AND, isSNeg, isTPos), branch2, ite3); - ASTNode ite1 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTPos), branch1, ite2); - - return SimplifyTerm_TopLevel(ite1); + return SimplifyTerm_TopLevel(n); } else if (SBVDIV == in.GetKind()) { @@ -114,23 +99,16 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) // //else simply output BVDIV(dividend,divisor) - ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor); + //Take absolute value. + ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend); + ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); - ASTNode cond1 = CreateNode(AND, CreateNode(EQ, zero, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT, - 1, divisor, hi1, hi1))); - ASTNode minus_divnode1 = CreateTerm(BVDIV, len, dividend, CreateTerm(BVUMINUS, len, divisor)); - minus_divnode1 = CreateTerm(BVUMINUS, len, minus_divnode1); + ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor); - ASTNode cond2 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, zero, CreateTerm(BVEXTRACT, - 1, divisor, hi1, hi1))); - ASTNode minus_divnode2 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), divisor); - minus_divnode2 = CreateTerm(BVUMINUS, len, minus_divnode2); + // A little confusing. Only negate the result if they are XOR <0. + ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVUMINUS, len, divnode), divnode); - ASTNode cond3 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT, - 1, divisor, hi1, hi1))); - ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor)); - ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3, - minus_divnode3, divnode))); return SimplifyTerm_TopLevel(n); } diff --git a/tests/generated_tests/mulDivRem.cpp b/tests/generated_tests/mulDivRem.cpp new file mode 100644 index 0000000..13b204e --- /dev/null +++ b/tests/generated_tests/mulDivRem.cpp @@ -0,0 +1,177 @@ +#include +#include +#include +#include +#include +#include "../constantbv/constantbv.h" +#include "../AST/AST.h" + +/* + * Generates random (a op b = c) triples to check that solver. + * Only for complicated instructions like modulus, remainder and divide. + */ + +using std::endl; +using std::cout; +using std::cerr; +using namespace BEEV; +using namespace CONSTANTBV; + +int width = 16; +typedef uint16_t uns; +typedef int16_t sig; + +const bool debug = false; + +uns getUnsignedResult(uns a, Kind k, uns b) +{ + uns gold; + + if (BVMULT == k) + { + return a * b; + } + else if (BVMOD == k) + { + return a % b; + } + else if (BVDIV == k) + { + return a / b; + } + cerr << "not implemetned" << endl; + exit(2); + +} + +sig getSignedResult(sig a, Kind k, sig b) +{ + sig gold; + + if (SBVMOD == k) + { + sig Q_prime = (sig) (trunc((double) a / (double) b)); + if ((a < 0) != (b < 0)) + { + Q_prime = Q_prime - 1; + } + + gold = a - Q_prime * b; + if (debug) + fprintf(stderr, "a=%d; b=%d; Q_prime=%d\n", a, b, Q_prime); + } + else if (SBVREM == k) + { + gold = a % b; + } + else if (SBVDIV == k) + { + gold = a / b; + } + else + { + cerr << "not implemetned" << endl; + exit(2); + } + return gold; + +} + +void go(int count, uns a, uns b, uns result, char* name) +{ + cout << ":extrafuns ((a" << count << " BitVec[" << width << "])) " << endl; + cout << ":extrafuns ((b" << count << " BitVec[" << width << "])) " << endl; + cout << ":extrafuns ((op" << count << " BitVec[" << width << "])) " << endl; + + cout << ":assumption (= "; + cout << "(" << name << " "; + if ((rand() % 3) == 0) + cout << "a" << count << " "; + else + cout << "bv" << a << "[" << width << "] "; + + if ((rand() % 3) == 0) + cout << "b" << count << " "; + else + cout << "bv" << b << "[" << width << "]"; + cout << " ) "; + + if ((rand() % 3) == 0) + cout << "op" << count << " "; + else + cout << "bv" << result << "[" << width << "]"; + + cout << ")" << endl; +} + +void testSolver(void) +{ + cout << "(" << endl; + cout << "benchmark blah" << endl; + cout << ":logic QF_BV" << endl; + cout << ":source {automatically generated}" << endl; + cout << ":status sat" << endl; + + uns a, b; + sig aS, bS; + + do + { + a = rand(); + b = rand(); + aS = rand(); + bS = rand(); + } while (bS == 0 || b == 0); + + switch (rand() % 6) + { + case 0: + go(0, a, b, getUnsignedResult(a, BVMULT, b), "bvmul"); + break; + case 1: + go(1, a, b, getUnsignedResult(a, BVDIV, b), "bvudiv"); + break; + case 2: + go(2, a, b, getUnsignedResult(a, BVMOD, b), "bvurem"); + break; + case 3: + go(3, aS, bS, getSignedResult(aS, SBVDIV, bS), "bvsdiv"); + break; + case 4: + go(4, aS, bS, getSignedResult(aS, SBVREM, bS), "bvsrem"); + break; + case 5: + go(5, aS, bS, getSignedResult(aS, SBVMOD, bS), "bvsmod"); + break; + + } + cout << ")" << endl; +} + +int main(int argc, char**argv) +{ + int nonce; + if (argc >= 2) + nonce = atoi(argv[1]); + else + nonce = 1; + int seed = time(0) * nonce; + if (debug) + { + cerr << "Seed = " << seed << endl; + } + srand(seed); + + BitVector_Boot(); + + if (false) + { + testConstEval(SBVMOD); + testConstEval(SBVREM); + testConstEval(SBVDIV); + } + testSolver(); + + return 0; +} + -- 2.47.3