From: trevor_hansen Date: Tue, 6 Jan 2009 03:41:16 +0000 (+0000) Subject: Added zero_extend function. Renamed bvdiv to bvudiv as per specification. Fixed off... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=20d383e9356f0cf3de6f39f6a517a4f8318d4e8a;p=francis%2Fstp.git Added zero_extend function. Renamed bvdiv to bvudiv as per specification. Fixed off-by-one check in BV_SX. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@50 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/AST/AST.cpp b/AST/AST.cpp index bfb350c..1a3db0b 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -666,6 +666,7 @@ namespace BEEV { os << endl; break; case BVSX: + case BVZX: os << kind << "("; c[0].PL_Print1(os,indentation,letize); os << ","; @@ -1197,10 +1198,19 @@ namespace BEEV { case BVSX: //in BVSX(n[0],len), the length of the BVSX term must be //greater than the length of n[0] - if(n[0].GetValueWidth() >= n.GetValueWidth()) { + if(n[0].GetValueWidth() > n.GetValueWidth()) { FatalError("BVTypeCheck: BVSX(t,bvsx_len) : length of 't' must be <= bvsx_len\n",n); } break; + + case BVZX: + //in BVZX(n[0],len), the length of the BVZX term must be + //greater than the length of n[0] + if(n[0].GetValueWidth() > n.GetValueWidth()) { + FatalError("BVTypeCheck: BVZX(t,bvzx_len) : length of 't' must be <= bvzx_len\n",n); + } + break; + default: for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++) if(BITVECTOR_TYPE != it->GetType()) { diff --git a/AST/ASTKind.kinds b/AST/ASTKind.kinds index b649de1..985ee62 100644 --- a/AST/ASTKind.kinds +++ b/AST/ASTKind.kinds @@ -32,6 +32,7 @@ SBVDIV 2 2 Term SBVREM 2 2 Term SBVMOD 2 2 Term BVSX 1 1 Term +BVZX 1 1 Term BOOLVEC 0 - Term # Formula OR term, depending on context diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp index f87fa46..7ebf2de 100644 --- a/AST/BitBlast.cpp +++ b/AST/BitBlast.cpp @@ -156,6 +156,48 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) { break; } } + + case BVZX: { + // Fill the high-order bits with as many zeroes as needed. + // Arg 0 is expression to be sign extended. + const ASTNode& arg = term[0]; + unsigned long result_width = term.GetValueWidth(); + unsigned long arg_width = arg.GetValueWidth(); + + //FIXME Uses a temporary const ASTNode reference + const ASTNode& bbarg = BBTerm(arg); + ASTVec tmp_res(result_width); + + //FIXME Should these be gotten from result? + ASTVec::const_iterator bb_it = bbarg.begin(); + ASTVec::iterator res_it = tmp_res.begin(); + ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part + ASTVec::iterator res_end = tmp_res.end(); + // copy LSBs directly from bbvec + for( ; res_it < res_ext; (res_it++, bb_it++)) { + *res_it = *bb_it; + } + // repeat zero to fill up rest of result. + for( ; res_it < res_end; (res_it++)) { + *res_it = ASTFalse; + } + + // Temporary debugging code + // cout << "Zero extending:" << endl + // << " Vec "; + // lpvec( bbarg.GetChildren() ); + // cout << " Extended to "; + // cout << result; + // cout << endl; + + result = CreateNode(BOOLVEC, tmp_res); + + break; + } + + + + case BVEXTRACT: { // bitblast the child, then extract the relevant bits. // Note: This could be optimized by not bitblasting the bits diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp index 77ba5b7..b2700ee 100644 --- a/bitvec/consteval.cpp +++ b/bitvec/consteval.cpp @@ -80,6 +80,22 @@ namespace BEEV { } break; } + + case BVZX: { + output = CONSTANTBV::BitVector_Create(inputwidth,true); + unsigned t0_width = t[0].GetValueWidth(); + if(inputwidth == t0_width) { + CONSTANTBV::BitVector_Copy(output, tmp0); + OutputNode = CreateBVConst(output, outputwidth); + } + else { + CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, t0_width); + OutputNode = CreateBVConst(output, outputwidth); + } + break; + } + + case BVAND: { output = CONSTANTBV::BitVector_Create(inputwidth,true); CONSTANTBV::Set_Intersection(output,tmp0,tmp1); diff --git a/parser/smtlib.lex b/parser/smtlib.lex index e39bc47..7070686 100644 --- a/parser/smtlib.lex +++ b/parser/smtlib.lex @@ -183,7 +183,7 @@ bit{DIGIT}+ { "bvsub" { return BVSUB_TOK;} "bvnot" { return BVNOT_TOK;} "bvmul" { return BVMULT_TOK;} -"bvdiv" { return BVDIV_TOK;} +"bvudiv" { return BVDIV_TOK;} "bvsdiv" { return SBVDIV_TOK;} "bvurem" { return BVMOD_TOK;} "bvsrem" { return SBVREM_TOK;} @@ -215,6 +215,7 @@ bit{DIGIT}+ { "bvsle" { return BVSLE_TOK;} "bvsge" { return BVSGE_TOK;} +"zero_extend" { return BVZX_TOK;} "sign_extend" { return BVSX_TOK;} "boolextract" { return BOOLEXTRACT_TOK;} "boolbv" { return BOOL_TO_BV_TOK;} diff --git a/parser/smtlib.y b/parser/smtlib.y index d462299..52215ec 100644 --- a/parser/smtlib.y +++ b/parser/smtlib.y @@ -194,6 +194,7 @@ %token BVSLE_TOK %token BVSGE_TOK %token BVSX_TOK +%token BVZX_TOK %token BOOLEXTRACT_TOK %token BOOL_TO_BV_TOK %token BVEXTRACT_TOK @@ -1108,6 +1109,17 @@ an_nonbvconst_term: $$ = n; delete $5; } +| BVZX_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term + { + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*$5); + unsigned w = $5->GetValueWidth() + $3; + BEEV::ASTNode width = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w); + BEEV::ASTNode *n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVZX,w,*$5,width)); + BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n); + $$ = n; + delete $5; + } + ; sort_symb: diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index 72c8700..fc715f6 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -1403,6 +1403,14 @@ namespace BEEV { } break; } + + case BVZX: + { + output = CreateTerm(BVZX,inputValueWidth,SimplifyTerm(inputterm[0]),inputterm[1]); + } + break; + + case BVSX:{ //a0 is the expr which is being sign extended ASTNode a0 = SimplifyTerm(inputterm[0]);