From: trevor_hansen Date: Thu, 16 Jun 2011 03:54:40 +0000 (+0000) Subject: Bugfix. Fix the semantics of BVSMOD to always give the remainder rounding towards... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=40c0e75371799d9db4b4353f7f0d8dce73eadfb2;p=francis%2Fstp.git Bugfix. Fix the semantics of BVSMOD to always give the remainder rounding towards zero. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1343 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index 5f71254..af1853c 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -51,7 +51,7 @@ namespace BEEV runTimes->stop(RunTimes::Transforming); - return result; + return result; } //Translates signed BVDIV,BVMOD and BVREM into unsigned variety @@ -106,19 +106,26 @@ namespace BEEV } // 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)) - // (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))))))) + + /* + (bvsmod s t) abbreviates + (let ((?msb_s ((_ extract |m-1| |m-1|) s)) + (?msb_t ((_ extract |m-1| |m-1|) t))) + (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s))) + (abs_t (ite (= ?msb_t #b0) t (bvneg t)))) + (let ((u (bvurem abs_s abs_t))) + (ite (= u (_ bv0 m)) + u + (ite (and (= ?msb_s #b0) (= ?msb_t #b0)) + u + (ite (and (= ?msb_s #b1) (= ?msb_t #b0)) + (bvadd (bvneg u) t) + (ite (and (= ?msb_s #b0) (= ?msb_t #b1)) + (bvadd u t) + (bvneg u)))))))) + */ //Take absolute value. ASTNode pos_dividend = @@ -143,12 +150,14 @@ namespace BEEV nf->CreateTerm(BVUMINUS, len, urem_node), urem_node); - // if It's XOR <0 then add t (not its absolute value). + // if It's XOR <0, and it doesn't perfectly divide, then add t (not its absolute value). ASTNode xor_node = nf->CreateNode(XOR, cond_dividend, cond_divisor); + ASTNode neZ = nf->CreateNode(NOT, nf->CreateNode(EQ, rev_node, bm->CreateZeroConst(divisor.GetValueWidth()))); + ASTNode cond = nf->CreateNode(AND,xor_node ,neZ); ASTNode n = nf->CreateTerm(ITE, len, - xor_node, + cond, nf->CreateTerm(BVPLUS, len, rev_node, divisor), rev_node); diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp index e9acd55..412f100 100644 --- a/src/simplifier/consteval.cpp +++ b/src/simplifier/consteval.cpp @@ -346,18 +346,23 @@ namespace BEEV case SBVMOD: { assert(2==number_of_children); - /* 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))))))) - */ +/* + (bvsmod s t) abbreviates + (let ((?msb_s ((_ extract |m-1| |m-1|) s)) + (?msb_t ((_ extract |m-1| |m-1|) t))) + (let ((abs_s (ite (= ?msb_s #b0) s (bvneg s))) + (abs_t (ite (= ?msb_t #b0) t (bvneg t)))) + (let ((u (bvurem abs_s abs_t))) + (ite (= u (_ bv0 m)) + u + (ite (and (= ?msb_s #b0) (= ?msb_t #b0)) + u + (ite (and (= ?msb_s #b1) (= ?msb_t #b0)) + (bvadd (bvneg u) t) + (ite (and (= ?msb_s #b0) (= ?msb_t #b1)) + (bvadd u t) + (bvneg u)))))))) +*/ assert(input_children[0].GetValueWidth() == input_children[1].GetValueWidth()); @@ -396,20 +401,25 @@ namespace BEEV 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 = _bm->CreateBVConst(res, outputwidth); + if (CONSTANTBV::BitVector_is_empty(remb)) + { + OutputNode = _bm->CreateZeroConst(outputwidth); + } + else + { + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + bool carry = false; + CONSTANTBV::BitVector_add(res, remb, tmp1, &carry); + OutputNode = _bm->CreateBVConst(res, outputwidth); + } - CONSTANTBV::BitVector_Destroy(tmp0b); CONSTANTBV::BitVector_Destroy(remb); + CONSTANTBV::BitVector_Destroy(tmp0b); CONSTANTBV::BitVector_Destroy(remainder); } else if (!isNegativeS && isNegativeT) @@ -422,11 +432,17 @@ namespace BEEV assert(e == CONSTANTBV::ErrCode_Ok); - bool carry = false; - CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); - CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry); - - OutputNode = _bm->CreateBVConst(res, outputwidth); + if (CONSTANTBV::BitVector_is_empty(remainder)) + { + OutputNode = _bm->CreateZeroConst(outputwidth); + } + else + { + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + bool carry = false; + CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry); + OutputNode = _bm->CreateBVConst(res, outputwidth); + } CONSTANTBV::BitVector_Destroy(tmp1b); CONSTANTBV::BitVector_Destroy(remainder);