From: trevor_hansen Date: Sun, 30 Aug 2009 10:44:51 +0000 (+0000) Subject: When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keepin... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=22dd6033ea0dbd09600d4e2fe8353137f0506539;p=francis%2Fstp.git When using the SMT parser (x % 0) and (x /0) both evaluate to 1. This isn't in keeping with the semantics of the SMTLIB language which says that the formula should only be satisfiable for all interpretations of division by zero (rather than just (x/0 ==1)). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@162 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index fa975c9..04651b1 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -55,6 +55,9 @@ bool smtlib_parser_flag = false; //print the input back bool print_STPinput_back_flag = false; +// If enabled. division, mod and remainder by zero will evaluate to 1. +bool division_by_zero_returns_one = false; + enum inputStatus input_status = NOT_DECLARED; // Used only in smtlib lexer/parser diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h index 8e0cf13..e0c8827 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -25,7 +25,7 @@ #include -using namespace std; +using namespace std; namespace BEEV { #ifdef EXT_HASH_MAP using namespace __gnu_cxx; @@ -61,7 +61,7 @@ namespace BEEV { extern bool print_output_flag; //print the variable order chosen by the sat solver while it is //solving. - extern bool print_sat_varorder_flag; + extern bool print_sat_varorder_flag; //turn on word level bitvector solver extern bool wordlevel_solve_flag; //XOR flattening optimizations. @@ -73,6 +73,8 @@ namespace BEEV { //Flag to switch on the smtlib parser extern bool smtlib_parser_flag; + extern bool division_by_zero_returns_one; + enum inputStatus { NOT_DECLARED =0, // Not included in the input file / stream @@ -107,10 +109,10 @@ namespace BEEV { // Table for storing function count stats. #ifdef TR1_UNORDERED_MAP - typedef tr1::unordered_map,eqstr> function_counters; #else - typedef hash_map,eqstr> function_counters; #endif @@ -118,7 +120,7 @@ namespace BEEV { //global function which accepts an integer and looks up the //corresponding ASTNode and prints a char* of that ASTNode - void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, + void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision, int polarity=0); }; // end namespace. #endif diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index e8f6acc..52a1c8b 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -40,7 +40,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) //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 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); @@ -69,12 +69,12 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) //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 pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); 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 rev_node = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node); // if It's XOR <0 then add t (not its absolute value). ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor); @@ -101,7 +101,7 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in) //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 pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor); ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor); @@ -305,14 +305,16 @@ ASTNode BeevMgr::TransformTerm(const ASTNode& inputterm) result = TranslateSignedDivModRem(result); } - ////// Temporary hack so we don't get killed on the Spear benchmarks in SMTCOMP-2009 - // This is a difficult rule to introduce in other places because it's recursive. i.e. - // result is imbedded unchanged inside the result. It's not + if (division_by_zero_returns_one) + { + // This is a difficult rule to introduce in other places because it's recursive. i.e. + // result is embedded unchanged inside the result. - unsigned inputValueWidth = result.GetValueWidth(); - ASTNode zero = CreateZeroConst(inputValueWidth); - ASTNode one = CreateOneConst(inputValueWidth); - result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result); + unsigned inputValueWidth = result.GetValueWidth(); + ASTNode zero = CreateZeroConst(inputValueWidth); + ASTNode one = CreateOneConst(inputValueWidth); + result = CreateTerm(ITE, inputValueWidth, CreateNode(EQ, zero, bottom), one, result); + } } } //////////////////////////////////////////////////////////////////////////////////// diff --git a/src/bitvec/consteval.cpp b/src/bitvec/consteval.cpp index daa4272..12860c9 100644 --- a/src/bitvec/consteval.cpp +++ b/src/bitvec/consteval.cpp @@ -143,9 +143,9 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) { // signed shift, and the number was originally negative. // Shift may be larger than the inputwidth. - for (unsigned int i =0; i < min(shift,inputwidth);i++) + for (unsigned int i = 0; i < min(shift, inputwidth); i++) { - CONSTANTBV::BitVector_Bit_On(output,(inputwidth-1 -i)); + CONSTANTBV::BitVector_Bit_On(output, (inputwidth - 1 - i)); } assert(CONSTANTBV::BitVector_Sign(output) == -1); //must be negative. } @@ -261,26 +261,33 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& 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) + if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) { - OutputNode = CreateBVConst(quotient, outputwidth); - CONSTANTBV::BitVector_Destroy(remainder); + // Expecting a division by zero. Just return one. + OutputNode = CreateOneConst(outputwidth); } else { - OutputNode = CreateBVConst(remainder, outputwidth); - CONSTANTBV::BitVector_Destroy(quotient); + 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; } @@ -309,87 +316,90 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) tmp0 = CONSTANTBV::BitVector_Clone(tmp0); tmp1 = CONSTANTBV::BitVector_Clone(tmp1); - if (CONSTANTBV::BitVector_is_empty(tmp1)) + if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) { - // If t is zero - FatalError("Dividing by zero"); - } + // Expecting a division by zero. Just return one. + OutputNode = CreateOneConst(outputwidth); - if (!isNegativeS && !isNegativeT) + } + else { - // Signs are both positive - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder); - if (e != CONSTANTBV::ErrCode_Ok) + if (!isNegativeS && !isNegativeT) { - cerr << "Error code was:" << e << endl; - assert(e == CONSTANTBV::ErrCode_Ok); + // 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); } - OutputNode = CreateBVConst(remainder, outputwidth); - } - else if (isNegativeS && !isNegativeT) - { - // S negative, T positive. - CBV tmp0b = CONSTANTBV::BitVector_Create(inputwidth, true); - CONSTANTBV::BitVector_Negate(tmp0b, tmp0); + 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); + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0b, tmp1, remainder); - assert(e == CONSTANTBV::ErrCode_Ok); + assert(e == CONSTANTBV::ErrCode_Ok); - CBV remb = CONSTANTBV::BitVector_Create(inputwidth, true); - CONSTANTBV::BitVector_Negate(remb, remainder); + 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); + bool carry = false; + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_add(res, remb, tmp1, &carry); - OutputNode = CreateBVConst(res, outputwidth); + 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::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); + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1b, remainder); - assert(e == CONSTANTBV::ErrCode_Ok); + assert(e == CONSTANTBV::ErrCode_Ok); - bool carry = false; - CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); - CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry); + bool carry = false; + CBV res = CONSTANTBV::BitVector_Create(inputwidth, true); + CONSTANTBV::BitVector_add(res, remainder, tmp1, &carry); - OutputNode = CreateBVConst(res, outputwidth); + 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(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); @@ -404,45 +414,53 @@ ASTNode BeevMgr::BVConstEvaluator(const ASTNode& t) CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true); CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true); - // tmp0 is dividend, tmp1 is the divisor - //All parameters to BitVector_Div_Pos must be distinct unlike BitVector_Divide - //FIXME the contents of the second parameter to Div_Pos is destroyed - //As tmp0 is currently the same as the copy belonging to an ASTNode t[0] - //this must be copied. - tmp0 = CONSTANTBV::BitVector_Clone(tmp0); - CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder); - CONSTANTBV::BitVector_Destroy(tmp0); - - if (0 != e) + if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1)) + { + // Expecting a division by zero. Just return one. + OutputNode = CreateOneConst(outputwidth); + } + else { - //error printing - if (counterexample_checking_during_refinement) - { - output = CONSTANTBV::BitVector_Create(inputwidth, true); - OutputNode = CreateBVConst(output, outputwidth); - bvdiv_exception_occured = true; - // CONSTANTBV::BitVector_Destroy(output); - break; + // tmp0 is dividend, tmp1 is the divisor + //All parameters to BitVector_Div_Pos must be distinct unlike BitVector_Divide + //FIXME the contents of the second parameter to Div_Pos is destroyed + //As tmp0 is currently the same as the copy belonging to an ASTNode t[0] + //this must be copied. + tmp0 = CONSTANTBV::BitVector_Clone(tmp0); + CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Div_Pos(quotient, tmp0, tmp1, remainder); + CONSTANTBV::BitVector_Destroy(tmp0); + + if (0 != e) + { + //error printing + if (counterexample_checking_during_refinement) + { + output = CONSTANTBV::BitVector_Create(inputwidth, true); + OutputNode = CreateBVConst(output, outputwidth); + bvdiv_exception_occured = true; + + // CONSTANTBV::BitVector_Destroy(output); + break; + } + else + { + BVConstEvaluatorError(e, t); + } + } //end of error printing + + //FIXME Not very standard in the current scheme + if (BVDIV == k) + { + OutputNode = CreateBVConst(quotient, outputwidth); + CONSTANTBV::BitVector_Destroy(remainder); } else { - BVConstEvaluatorError(e, t); + OutputNode = CreateBVConst(remainder, outputwidth); + CONSTANTBV::BitVector_Destroy(quotient); } - } //end of error printing - - //FIXME Not very standard in the current scheme - if (BVDIV == k) - { - OutputNode = CreateBVConst(quotient, outputwidth); - CONSTANTBV::BitVector_Destroy(remainder); } - else - { - OutputNode = CreateBVConst(remainder, outputwidth); - CONSTANTBV::BitVector_Destroy(quotient); - } - break; } case ITE: diff --git a/src/parser/main.cpp b/src/parser/main.cpp index 9b2b656..e385850 100644 --- a/src/parser/main.cpp +++ b/src/parser/main.cpp @@ -53,7 +53,7 @@ std::string helpstring = "\n\n"; static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; /****************************************************************************** - * MAIN FUNCTION: + * MAIN FUNCTION: * * step 0. Parse the input into an ASTVec. * step 1. Do BV Rewrites @@ -76,7 +76,7 @@ int main(int argc, char ** argv) { // FIXME: figure out how to get and print the real error message. BEEV::FatalError("Initial allocation of memory failed."); } - + //populate the help string helpstring += "-r : switch refinement off (optimizations are ON by default)\n"; helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n"; @@ -116,9 +116,10 @@ int main(int argc, char ** argv) { break; case 'n': BEEV::print_output_flag = true; - break; + break; case 'm': BEEV::smtlib_parser_flag=true; + BEEV::division_by_zero_returns_one = true; break; case 'p': BEEV::print_counterexample_flag = true; @@ -170,7 +171,7 @@ int main(int argc, char ** argv) { if (BEEV::smtlib_parser_flag) { smtin = fopen(infile,"r"); - if(smtin == NULL) + if(smtin == NULL) { fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); BEEV::FatalError(""); @@ -179,7 +180,7 @@ int main(int argc, char ** argv) { else { cvcin = fopen(infile,"r"); - if(cvcin == NULL) + if(cvcin == NULL) { fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); BEEV::FatalError(""); @@ -188,19 +189,19 @@ int main(int argc, char ** argv) { } } - CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); + CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot(); if(0 != c) { cout << CONSTANTBV::BitVector_Error(c) << endl; return 0; } - //want to print the output always from the commandline. + //want to print the output always from the commandline. BEEV::print_output_flag = true; - BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); + BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); - + if (BEEV::smtlib_parser_flag) smtparse(); else