From d454241c653d3d25514ae0ffe4b954b2b1affa5a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 27 Jul 2009 11:59:44 +0000 Subject: [PATCH] Partial fix of bvsmod, bvsrem. Both operations still report spurious division by zero errors. They work much better than they used to. But not perfectly. See the test cases in misc-tests for examples they currently fail on. Also, updated BVTypeCheck to return a boolean (so it is easy to use in asserts()). A trivial recursive typecheck function. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@90 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 32 +++++- AST/AST.h | 12 +- AST/ToSAT.cpp | 3 +- AST/Transform.cpp | 231 +++++++++++++++----------------------- AST/genkinds.pl | 2 +- bitvec/consteval.cpp | 155 ++++++++++++++++++++++++- simplifier/simplifier.cpp | 1 + 7 files changed, 281 insertions(+), 155 deletions(-) diff --git a/AST/AST.cpp b/AST/AST.cpp index a032833..9c97d6d 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -59,7 +59,7 @@ bool smtlib_parser_enable = false; //print the input back bool print_STPinput_back = false; -enum BEEV::inputStatus input_status = NOT_DECLARED; +enum inputStatus input_status = NOT_DECLARED; // Used only in smtlib lexer/parser ASTNode SingleBitOne; @@ -1247,15 +1247,36 @@ ASTNode::ASTNode(const ASTNode &n) : #endif } +// If there is a lot of sharing in the graph, this will take a long time. +// it doesn't mark subgraphs as already having been typechecked. +bool BeevMgr::BVTypeCheckRecursive(const ASTNode& n) +{ + const ASTVec& c = n.GetChildren(); + + BVTypeCheck(n); + + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + BVTypeCheckRecursive(*it); + + return true; +} + + + /* FUNCTION: Typechecker for terms and formulas * * TypeChecker: Assumes that the immediate Children of the input * ASTNode have been typechecked. This function is suitable in * scenarios like where you are building the ASTNode Tree, and you * typecheck as you go along. It is not suitable as a general - * typechecker + * typechecker. + * + * This ALWAYS returns true. If there is an error it will call + * FatalError() and abort. */ -void BeevMgr::BVTypeCheck(const ASTNode& n) + + +bool BeevMgr::BVTypeCheck(const ASTNode& n) { Kind k = n.GetKind(); //The children of bitvector terms are in turn bitvectors. @@ -1269,7 +1290,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n) FatalError("BVTypeCheck: The term t does not typecheck, where t = \n", n); break; case SYMBOL: - return; + return true; case ITE: if (BOOLEAN_TYPE != n[0].GetType() || (n[1].GetType() != n[2].GetType())) FatalError("BVTypeCheck: The term t does not typecheck, where t = \n", n); @@ -1392,7 +1413,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n) case TRUE: case FALSE: case SYMBOL: - return; + return true; case EQ: case NEQ: if (!(n[0].GetValueWidth() == n[1].GetValueWidth() && n[0].GetIndexWidth() == n[1].GetIndexWidth())) @@ -1445,6 +1466,7 @@ void BeevMgr::BVTypeCheck(const ASTNode& n) break; } } + return true; } //End of TypeCheck function //add an assertion to the current logical context diff --git a/AST/AST.h b/AST/AST.h index 3c487b2..627bd89 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -1724,7 +1724,8 @@ public: ASTNode TransformFormula(const ASTNode& query); ASTNode TransformTerm(const ASTNode& term); ASTNode TransformArray(const ASTNode& term); - ASTNode TranslateSignedDivMod(const ASTNode& term); + ASTNode TranslateSignedDivModRem(const ASTNode& term); + void assertTransformPostConditions(const ASTNode & term); //LET Management private: @@ -1843,7 +1844,14 @@ public: //in scenarios like where you are building the ASTNode Tree, and //you typecheck as you go along. It is not suitable as a general //typechecker - void BVTypeCheck(const ASTNode& n); + + // NB: The boolean value is always true! + bool BVTypeCheck(const ASTNode& n); + + // Checks recursively all the way down. + bool BVTypeCheckRecursive(const ASTNode& n); + + private: //stack of Logical Context. each entry in the stack is a logical diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp index f050524..e8cd101 100644 --- a/AST/ToSAT.cpp +++ b/AST/ToSAT.cpp @@ -1158,6 +1158,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) Begin_RemoveWrites = false; newq = TransformFormula(newq); + assertTransformPostConditions(newq); ASTNodeStats("after transformation: ", newq); TermsAlreadySeenMap.clear(); @@ -1197,7 +1198,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) return res; } - FatalError("TopLevelSAT: reached the end without proper conclusion:" + FatalError("TopLevelSATAux: reached the end without proper conclusion:" "either a divide by zero in the input or a bug in STP"); //bogus return to make the compiler shut up return 2; diff --git a/AST/Transform.cpp b/AST/Transform.cpp index ecb5223..8dd760c 100644 --- a/AST/Transform.cpp +++ b/AST/Transform.cpp @@ -7,19 +7,20 @@ ********************************************************************/ // -*- c++ -*- +// Transform: * Converts signed Div/ signed remainder/ signed modulus into unsigned. +// * Removes array selects / stores from formula. + + #include "AST.h" #include #include namespace BEEV { -//Translates signed BVDIV/BVMOD into unsigned variety -ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) +//Translates signed BVDIV,BVMOD and BVREM into unsigned variety +ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) { - if (!(SBVREM == in.GetKind() || SBVDIV == in.GetKind())) - { - FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n", in); - } + assert(in.GetChildren().size() ==2); ASTNode dividend = in[0]; ASTNode divisor = in[1]; @@ -51,10 +52,13 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) //put everything together, simplify, and return ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode); - return SimplifyTerm_TopLevel(n); + return SimplifyTerm(n); } - if (SBVMOD == in.GetKind()) + // This is the modulus of dividing rounding to -infinity. + // Except if the signs are different, and it perfectly divides + // the modulus is the divisor (not zero). + else if (SBVMOD == in.GetKind()) { // (let (?msb_s (extract[|m-1|:|m-1|] s)) // (let (?msb_t (extract[|m-1|:|m-1|] t)) @@ -67,16 +71,16 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) // (bvneg (bvurem (bvneg s) (bvneg t))))))) ASTNode & s = dividend; ASTNode & t = divisor; - ASTNode & msb_s = cond_dividend; - ASTNode & msb_t = cond_divisor; - ASTNode isSPos = CreateNode(EQ, msb_s, zero); // (= ?msb_s bit0) - ASTNode isSNeg = CreateNode(EQ, msb_s, one); // (= ?msb_s bit1) - ASTNode isTPos = CreateNode(EQ, msb_t, zero); // (= ?msb_t bit0) - ASTNode isTNeg = CreateNode(EQ, msb_t, one); // (= ?msb_t bit1) + ASTNode isSNeg = cond_dividend; // (= ?msb_s bit1) + ASTNode isSPos = CreateNode(NOT, isSNeg); // (= ?msb_s bit0) + + ASTNode isTNeg = cond_divisor; // (= ?msb_t bit1) + ASTNode isTPos = CreateNode(NOT, isTNeg); // (= ?msb_t bit0) + ASTNode negS = CreateTerm(BVUMINUS, len, s); // (bvneg s) - ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg s) + ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg t) // (bvneg (bvurem (bvneg s) (bvneg t))) ASTNode branch4 = CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, negT)); @@ -91,133 +95,76 @@ ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) 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(ite1); + } + else if (SBVDIV == in.GetKind()) + { + //now handle the BVDIV case + //if topBit(dividend) is 1 and topBit(divisor) is 0 + // + //then output is -BVDIV(-dividend,divisor) + // + //elseif topBit(dividend) is 0 and topBit(divisor) is 1 + // + //then output is -BVDIV(dividend,-divisor) + // + //elseif topBit(dividend) is 1 and topBit(divisor) is 1 + // + // then output is BVDIV(-dividend,-divisor) + // + //else simply output BVDIV(dividend,divisor) + + ASTNode divnode = CreateTerm(BVDIV, len, dividend, 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 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); + + 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(n); } - //now handle the BVDIV case - //if topBit(dividend) is 1 and topBit(divisor) is 0 - // - //then output is -BVDIV(-dividend,divisor) - // - //elseif topBit(dividend) is 0 and topBit(divisor) is 1 - // - //then output is -BVDIV(dividend,-divisor) - // - //elseif topBit(dividend) is 1 and topBit(divisor) is 1 - // - // then output is BVDIV(-dividend,-divisor) - // - //else simply output BVDIV(dividend,divisor) - ASTNode divnode = CreateTerm(BVDIV, len, dividend, 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 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); - - 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); -}//end of TranslateSignedDivMod() - -/* - //Translates signed BVDIV/BVMOD into unsigned variety - ASTNode BeevMgr::TranslateSignedDivMod(const ASTNode& in) { - if(!(SBVREM == in.GetKind() || SBVDIV == in.GetKind())) { - FatalError("TranslateSignedDivMod: input must be signed DIV/MOD\n",in); - } - - ASTNode dividend = in[0]; - ASTNode divisor = in[1]; - unsigned len = in.GetValueWidth(); - if(SBVMOD == in.GetKind()) { - //if(TopBit(dividend)==1) - // - //then -BVMOD(-dividend,abs(divisor)) - // - //else BVMOD(dividend,abs(divisor)) - - //create the condition for the dividend - ASTNode hi1 = CreateBVConst(32,len-1); - ASTNode one = CreateOneConst(1); - ASTNode cond = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,dividend,hi1,hi1)); - - //create the condition and conditional for the divisor - ASTNode cond_divisor = CreateNode(EQ,one,CreateTerm(BVEXTRACT,1,divisor,hi1,hi1)); - ASTNode pos_divisor = CreateTerm(ITE,len,cond_divisor,CreateTerm(BVUMINUS,len,divisor),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); - - //put everything together, simplify, and return - ASTNode n = CreateTerm(ITE,len,cond,minus_modnode,modnode); - return SimplifyTerm_TopLevel(n); - } - - //now handle the BVDIV case - //if topBit(dividend) is 1 and topBit(divisor) is 0 - // - //then output is -BVDIV(-dividend,divisor) - // - //elseif topBit(dividend) is 0 and topBit(divisor) is 1 - // - //then output is -BVDIV(dividend,-divisor) - // - //elseif topBit(dividend) is 1 and topBit(divisor) is 1 - // - // then output is BVDIV(-dividend,-divisor) - // - //else simply output BVDIV(dividend,divisor) - ASTNode hi1 = CreateBVConst(32,len-1); - ASTNode zero = CreateZeroConst(1); - ASTNode one = CreateOneConst(1); - ASTNode divnode = CreateTerm(BVDIV, len, dividend, 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 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); - - 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); - }//end of TranslateSignedDivMod() - */ + FatalError("TranslateSignedDivModRem: input must be signed DIV/MOD/REM", in); + return ASTUndefined; + +}//end of TranslateSignedDivModRem() + +// Check that the transformations have occurred. +void BeevMgr::assertTransformPostConditions(const ASTNode & term) +{ + const Kind k = term.GetKind(); + + // Check the signed operations have been removed. + assert( SBVDIV != k); + assert( SBVMOD != k); + assert( SBVREM !=k); + + // Check the array reads / writes have been removed + assert( READ !=k ); + assert( WRITE !=k); + + // There should be no nodes left of type array. + assert(0 == term.GetIndexWidth()); + + ASTVec c = term.GetChildren(); + ASTVec::iterator it = c.begin(); + ASTVec::iterator itend = c.end(); + ASTVec o; + for (; it != itend; it++) + { + assertTransformPostConditions(*it); + } +} ASTNode BeevMgr::TransformFormula(const ASTNode& form) { @@ -304,7 +251,7 @@ ASTNode BeevMgr::TransformFormula(const ASTNode& form) } break; } - //BVTypeCheck(result); + assert(BVTypeCheckRecursive(result)); TransformMap[simpleForm] = result; return result; } //End of TransformFormula @@ -371,7 +318,7 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) if (SBVDIV == result.GetKind() || SBVREM == result.GetKind() || SBVMOD == result.GetKind()) { - result = TranslateSignedDivMod(result); + result = TranslateSignedDivModRem(result); } break; } diff --git a/AST/genkinds.pl b/AST/genkinds.pl index 7944832..1eaa407 100755 --- a/AST/genkinds.pl +++ b/AST/genkinds.pl @@ -81,7 +81,7 @@ sub gen_h_file { print HFILE "extern const char *_kind_names[];\n\n", "/** Prints symbolic name of kind */\n", - "inline ostream& operator<<(ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n", + "inline std::ostream& operator<<(std::ostream &os, const Kind &kind) { os << _kind_names[kind]; return os; }\n", "\n\n", "}; // end namespace\n", "\n\n#endif\n"; diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp index e6ca42a..6ccb97d 100644 --- a/bitvec/consteval.cpp +++ b/bitvec/consteval.cpp @@ -236,13 +236,153 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) OutputNode = CreateBVConst(output, outputwidth); break; } - //FIXME ANOTHER SPECIAL CASE + + // SBVREM : Result of rounding the quotient towards zero. i.e. (-10)/3, has a remainder of -1 + // SBVMOD : Result of rounding the quotient towards -infinity. i.e. (-10)/3, has a modulus of 2. + // EXCEPT THAT if it divides exactly and the signs are different, then it's equal to the dividend. case SBVDIV: case SBVREM: { - OutputNode = BVConstEvaluator(TranslateSignedDivMod(t)); + CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true); + CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); + + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder); + + if (e != 0) + { + cerr << "WARNING" << endl; + FatalError((const char*) CONSTANTBV::BitVector_Error(e)); + } + + if (SBVDIV == k) + { + OutputNode = CreateBVConst(quotient, outputwidth); + CONSTANTBV::BitVector_Destroy(remainder); + } + else + { + OutputNode = CreateBVConst(remainder, outputwidth); + CONSTANTBV::BitVector_Destroy(quotient); + + } + break; } + + case SBVMOD: + { + /* Definition taken from the SMTLIB website + (bvsmod s t) abbreviates + (let (?msb_s (extract[|m-1|:|m-1|] s)) + (let (?msb_t (extract[|m-1|:|m-1|] t)) + (ite (and (= ?msb_s bit0) (= ?msb_t bit0)) + (bvurem s t) + (ite (and (= ?msb_s bit1) (= ?msb_t bit0)) + (bvadd (bvneg (bvurem (bvneg s) t)) t) + (ite (and (= ?msb_s bit0) (= ?msb_t bit1)) + (bvadd (bvurem s (bvneg t)) t) + (bvneg (bvurem (bvneg s) (bvneg t))))))) + */ + + assert(t[0].GetValueWidth() == t[1].GetValueWidth()); + + bool isNegativeS = CONSTANTBV::BitVector_msb_(tmp0); + bool isNegativeT = CONSTANTBV::BitVector_msb_(tmp1); + + CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true); + CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); + tmp0 = CONSTANTBV::BitVector_Clone(tmp0); + tmp1 = CONSTANTBV::BitVector_Clone(tmp1); + + if (CONSTANTBV::BitVector_is_empty(tmp1)) + { + // If t is zero + FatalError("Dividing by zero"); + } + + if (!isNegativeS && !isNegativeT) + { + // Signs are both positive + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder); + if(e != CONSTANTBV::ErrCode_Ok) + { + cerr << "Error code was:" << e << endl; + assert(e == CONSTANTBV::ErrCode_Ok); + } + OutputNode = CreateBVConst(remainder, outputwidth); + } + else if (isNegativeS && !isNegativeT) + { + // S negative, T positive. + CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_Negate(tmp0b, tmp0); + + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder); + + assert(e == CONSTANTBV::ErrCode_Ok); + + CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_Negate(remb, remainder); + + bool carry = false; + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_add(res, remb, tmp1, &carry); + + OutputNode = CreateBVConst(res, outputwidth); + + CONSTANTBV::BitVector_Destroy(tmp0b); + CONSTANTBV::BitVector_Destroy(remb); + CONSTANTBV::BitVector_Destroy(remainder); + } + else if (!isNegativeS && isNegativeT) + { + // If s is positive and t is negative + CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_Negate(tmp1b, tmp1); + + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder); + + assert(e == CONSTANTBV::ErrCode_Ok); + + bool carry = false; + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry); + + OutputNode = CreateBVConst(res, outputwidth); + + CONSTANTBV::BitVector_Destroy(tmp1b); + CONSTANTBV::BitVector_Destroy(remainder); + } + else if (isNegativeS && isNegativeT) + { + // Signs are both negative + CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true); + CBV tmp1b = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_Negate(tmp0b, tmp0); + CONSTANTBV::BitVector_Negate(tmp1b, tmp1); + + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1b, remainder); + assert(e == CONSTANTBV::ErrCode_Ok); + + CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_Negate(remb, remainder); + + OutputNode = CreateBVConst(remb, outputwidth); + CONSTANTBV::BitVector_Destroy(tmp0b); + CONSTANTBV::BitVector_Destroy(tmp1b); + CONSTANTBV::BitVector_Destroy(remainder); + } + else + { + FatalError("never get called"); + } + + CONSTANTBV::BitVector_Destroy(tmp0); + CONSTANTBV::BitVector_Destroy(tmp1); + CONSTANTBV::BitVector_Destroy(quotient); + } + break; + case BVDIV: case BVMOD: { @@ -291,12 +431,19 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) break; } case ITE: - if (ASTTrue == t[0]) + { + ASTNode tmp0 = t[0]; // Should this run BVConstEvaluator?? + + if (ASTTrue == tmp0) OutputNode = BVConstEvaluator(t[1]); - else if (ASTFalse == t[0]) + else if (ASTFalse == tmp0) OutputNode = BVConstEvaluator(t[2]); else + { + cerr << tmp0; FatalError("BVConstEvaluator: ITE condiional must be either TRUE or FALSE:", t); + } + } break; case EQ: if (CONSTANTBV::BitVector_equal(tmp0, tmp1)) diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index 77c374f..d94af9b 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -1896,6 +1896,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm) } case SBVREM: case SBVDIV: + case SBVMOD: { ASTVec c = inputterm.GetChildren(); ASTVec o; -- 2.47.3