Left shift, >32 bit constants, fixed zero_extend, fixed (?) SBVREM.

Now left shifts by a variable amount. Previously the shift amount needed to a constant.

The smtlib parser reads bitvector constants into strings rather than into ints. This allows formula to
contain constants greater than the size of the machine's integer.

Fixed zero_extend. I didn't add code for it into the SimplifyTermAux function. SBVREM was sometimes failing
because it also wasn't included in the same function. Added it in. Not sure what the function does though..

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@51 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/AST/AST.cpp b/AST/AST.cpp
index 1a3db0bc2698ca4758007adafd4e5a84ab7e9b24..2ecff2f19c3b219cb1251216be04b50d4ccf53a8 100644 (file)
--- a/AST/AST.cpp
+++ b/AST/AST.cpp
@@ -786,7 +786,7 @@ namespace BEEV {
     
 
     CBV bv = CONSTANTBV::BitVector_Create(width, true);
-    unsigned long c_val = (0x00000000ffffffffLL) & bvconst;
+    unsigned long c_val = (~((unsigned long)0)) & bvconst;
     unsigned int copied = 0;
 
     // sizeof(unsigned long) returns the number of bytes in unsigned
@@ -801,13 +801,43 @@ namespace BEEV {
     while(copied + (sizeof(unsigned long)<<3) < width){
       CONSTANTBV::BitVector_Chunk_Store(bv, sizeof(unsigned long)<<3,copied,c_val);
       bvconst = bvconst >> (sizeof(unsigned long) << 3);
-      c_val = (0x00000000ffffffffLL) & bvconst;
+      c_val = (~((unsigned long)0)) & bvconst;
       copied += sizeof(unsigned long) << 3;
     }
     CONSTANTBV::BitVector_Chunk_Store(bv,width - copied,copied,c_val);
     return CreateBVConst(bv,width);
   }
 
+ ASTNode BeevMgr::CreateBVConst(string*& strval, unsigned int base,  size_t bit_width) {
+
+   if(!(2 == base || 10 == base || 16 == base))
+     {
+      FatalError("CreateBVConst: unsupported base: ",ASTUndefined,base);
+     }
+
+    //checking if the input is in the correct format
+    CBV bv = CONSTANTBV::BitVector_Create(bit_width,true);
+    CONSTANTBV::ErrCode e;
+    if(2 == base){
+      e = CONSTANTBV::BitVector_from_Bin(bv, (unsigned char*) strval->c_str());
+    }else if(10 == base){
+      e = CONSTANTBV::BitVector_from_Dec(bv, (unsigned char*) strval->c_str());
+    }else if(16 == base){
+      e = CONSTANTBV::BitVector_from_Hex(bv, (unsigned char*) strval->c_str());
+    }else{
+      e = CONSTANTBV::ErrCode_Pars;
+    }
+
+    if(0 != e) {
+      cerr << "CreateBVConst: " << BitVector_Error(e);
+      FatalError("",ASTUndefined);
+    }
+
+    return CreateBVConst(bv, bit_width);
+  }
+
+
+
   //Create a ASTBVConst node from std::string
   ASTNode BeevMgr::CreateBVConst(const char* const strval, int base) {
     size_t width = strlen((const char *)strval);    

diff --git a/AST/AST.h b/AST/AST.h
index 04f3528912a1e1fece868f4154e39e2d14249f4b..27d090e0778793e57cfa6408d1cce987a85edbde 100644 (file)
--- a/AST/AST.h
+++ b/AST/AST.h
@@ -687,12 +687,23 @@ namespace BEEV {
     CBV GetBVConst() const {return _bvconst;}
   }; //End of ASTBVConst
 
-  //FIXME This function is DEPRICATED
+
+  //FIXME This function is DEPRECATED
   //Do not use in the future
-  inline unsigned int GetUnsignedConst(const ASTNode n) {
-    if(32 < n.GetValueWidth())
-      FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int:");
-        
+ inline unsigned int GetUnsignedConst(const ASTNode n) 
+  {
+    if(sizeof(unsigned int) * 8  <= n.GetValueWidth())  
+      {
+       // It may only contain a small value in a bit type, which fits nicely into an unsigned int.
+       // This is common for functions like: bvshl(bv1[128], bv1[128])
+       // where both operands have the same type.
+       unsigned long maxBit = (unsigned) CONSTANTBV::Set_Max(n.GetBVConst());
+       if (maxBit >= sizeof(unsigned int) * 8 )
+         {
+           n.LispPrint(cerr); //print the node so they can find it.
+           FatalError("GetUnsignedConst: cannot convert bvconst of length greater than 32 to unsigned int");
+         }
+      }
     return (unsigned int) *((unsigned int *)n.GetBVConst());
   }
 #else
@@ -1216,6 +1227,9 @@ namespace BEEV {
     void BBLShift(ASTVec& x);
     void BBRShift(ASTVec& x);
 
+    void BBLShift(ASTVec& x, unsigned int shift);
+    void BBRShift(ASTVec& x, unsigned int shift);
+
   public:
     // Simplifying create functions
     ASTNode CreateSimpForm(Kind kind, ASTVec &children);
@@ -1350,12 +1364,14 @@ namespace BEEV {
 
     // Create and return an ASTNode for a symbol
     // Width is number of bits.
+    ASTNode CreateBVConst(string*& strval, unsigned int base,  size_t bit_width);
     ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst);
     ASTNode CreateZeroConst(unsigned int width);
     ASTNode CreateOneConst(unsigned int width);
     ASTNode CreateTwoConst(unsigned int width);
     ASTNode CreateMaxConst(unsigned int width);
 
+
     // Create and return an ASTNode for a symbol
     // Optional base was a problem because 0 could be an int or char *,
     // so CreateBVConst was ambiguous.

diff --git a/AST/BitBlast.cpp b/AST/BitBlast.cpp
index 7ebf2de2fecbe565e12f9497c85877649dc72818..7ead02caf1601e6c4ffd7a0fae55899a174c4f72 100644 (file)
--- a/AST/BitBlast.cpp
+++ b/AST/BitBlast.cpp
@@ -69,6 +69,78 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
     result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren()));
     break;
   }
+
+  case BVLEFTSHIFT:
+   {
+     if (BVCONST == term[1].GetKind())
+       {
+        // Constant shifts should be removed during simplification.
+        unsigned int shift = GetUnsignedConst(term[1]);
+
+        ASTNode term0 = BBTerm(term[0]);
+        ASTVec children(term0.GetChildren()); // mutable copy of the children.
+        BBLShift(children, shift);
+        
+        result = CreateNode(BOOLVEC, children);
+      }
+     else
+     {
+     // Barrel shifter
+       const ASTVec& bbarg1 = BBTerm(term[0]).GetChildren();
+       const ASTVec& bbarg2 = BBTerm(term[1]).GetChildren();  
+       
+       ASTVec temp_result(bbarg1);
+       
+       for (unsigned int i =0; i < bbarg2.size(); i++)
+               {
+                       if (bbarg2[i] == ASTFalse) 
+                               continue;  // Not shifting by anything.
+                       
+                       unsigned int shift_amount = 1 << i;
+                       
+                       bool done = false;
+                       
+                       for (unsigned int j=temp_result.size()-1; !done; j--)
+                       {
+                               if (j < shift_amount)
+                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i],ASTFalse,temp_result[j]);
+                               else
+                                       temp_result[j] = CreateSimpForm(ITE, bbarg2[i],temp_result[j-shift_amount],temp_result[j]);
+                               
+                               // want it to stop after doing 0, but subtracting 1 from j makes it very big. 
+                               if (j ==0)
+                                       done = true;
+                       }
+               }
+
+       result =  CreateNode(BOOLVEC, temp_result);
+  }
+       break;
+   }
+   
+   case BVRIGHTSHIFT:
+   {
+    if (BVCONST == term[1].GetKind())
+      {
+               // Constant shifts should be removed during simplification.
+               
+           unsigned int shift = GetUnsignedConst(term[1]);
+
+       ASTNode term0 = BBTerm(term[0]);
+       ASTVec children(term0.GetChildren()); // mutable copy of the children.
+       BBRShift(children, shift);
+
+       result = CreateNode(BOOLVEC, children);
+      }
+     else
+       {
+               FatalError("Not implemented shift right by unk. value.");
+               }
+   }
+       break;
+   
+
+
   case BVSRSHIFT:
   case BVVARSHIFT: 
     FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term);
@@ -86,6 +158,8 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
        CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren()));
     break;
   }
+
+
   case BVSX: {
     // Replicate high-order bit as many times as necessary.
     // Arg 0 is expression to be sign extended.
@@ -139,7 +213,7 @@ const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
        *res_it = *bb_it;
       }
       // repeat MSB to fill up rest of result.
-      for( ; res_it < res_end; (res_it++, bb_it++)) {
+      for( ; res_it < res_end; (res_it++)) {
        *res_it = msb;
       }
       
@@ -841,6 +915,40 @@ void BeevMgr::BBLShift(ASTVec& x)
   // lpvec(x);
 }
 
+// Left shift  within fixed field inserting zeros at LSB.
+// Writes result into first argument.
+  void BeevMgr::BBLShift(ASTVec& x, unsigned int shift)
+{
+  // left shift x (destructively) within width.
+  // loop backwards so that copy to self works correctly. (DON'T use STL insert!)
+  ASTVec::iterator xbeg = x.begin();
+  ASTVec::iterator xit = x.end()-1;
+  for(; xit >= xbeg; xit--) {
+    if (xit-shift >= xbeg)
+      *xit = *(xit-shift);
+    else
+      *xit= ASTFalse; // new LSB is zero.
+  }
+}
+
+// Right shift within fixed field inserting zeros at MSB.
+// Writes result into first argument.
+  void BeevMgr::BBRShift(ASTVec& x, unsigned int shift)
+{
+  // right shift x (destructively) within width.
+  ASTVec::iterator xend = x.end();
+  ASTVec::iterator xit = x.begin();
+  for(; xit < xend; xit++) {
+    if (xit+shift < xend)
+      *xit = *(xit+shift);
+    else
+      *xit= ASTFalse; // new MSB is zero.
+  }
+}
+
+
+
+
 // Right shift by 1 within fixed field, inserting new zeros at MSB.
 // Writes result into first argument.
 // Fixme: generalize to n bits.
@@ -854,7 +962,6 @@ void BeevMgr::BBRShift(ASTVec& x)
   *xit = ASTFalse;             // new MSB is zero.
 }
 
-
 // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. 
 ASTNode BeevMgr::BBcompare(const ASTNode& form) {
   const ASTNode lnode = BBTerm(form[0]);

diff --git a/bitvec/consteval.cpp b/bitvec/consteval.cpp
index b2700eeeed78c323541c5bba6935a3a41f3a82bb..86837633dfb129d40e178f3d7bd9b7e2071e0271 100644 (file)
--- a/bitvec/consteval.cpp
+++ b/bitvec/consteval.cpp
@@ -96,6 +96,36 @@ namespace BEEV {
     }
 
 
+   case BVLEFTSHIFT: 
+     {
+      output = CONSTANTBV::BitVector_Create(inputwidth,true);
+
+      // the shift is destructive, get a copy.
+      CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
+
+      // get the number of bits to shift it.
+      unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1]));
+
+      CONSTANTBV::BitVector_Move_Left(output,shift);
+      OutputNode = CreateBVConst(output,outputwidth);
+      break;
+    }
+    case BVRIGHTSHIFT: 
+      {
+       output = CONSTANTBV::BitVector_Create(inputwidth,true);
+
+      // the shift is destructive, get a copy.
+      CONSTANTBV::BitVector_Interval_Copy(output, tmp0, 0, 0, inputwidth);
+
+      // get the number of bits to shift it.
+      unsigned int shift = GetUnsignedConst(BVConstEvaluator(t[1]));
+
+      CONSTANTBV::BitVector_Move_Right(output,shift);
+      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 7070686e5cba2951723a7817e6cc8d6cfcd227fd..5d5f1a63cd06b7ff4af2b0e648b2d411facbdab8 100644 (file)
--- a/parser/smtlib.lex
+++ b/parser/smtlib.lex
@@ -79,7 +79,7 @@ ANYTHING  ({LETTER}|{DIGIT}|{OPCHAR})
 {DIGIT}+       { yylval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK; }
 
 
-bv{DIGIT}+     { yylval.ullval = strtoull(yytext+2, NULL, 10); return BVCONST_TOK; }
+        bv{DIGIT}+     { yylval.str = new std::string(yytext+2); return BVCONST_TOK; }
 
 bit{DIGIT}+     {
                   char c = yytext[3];

diff --git a/parser/smtlib.y b/parser/smtlib.y
index 52215ecf5f7360c14cc037444d01e803739e8596..3da40906db3ba223ef1c7523b0686272496cd181 100644 (file)
--- a/parser/smtlib.y
+++ b/parser/smtlib.y
@@ -99,7 +99,7 @@
 %type <str> user_value
 
 %token <uintval> NUMERAL_TOK
-%token <ullval> BVCONST_TOK
+%token <str> BVCONST_TOK
 %token <node> BITCONST_TOK
 %token <node> FORMID_TOK TERMID_TOK 
 %token <str> STRING_TOK
@@ -671,11 +671,12 @@ an_terms:
 an_term:
     BVCONST_TOK
     {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(64, $1));
+      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1, 10, 32));
     }
   | BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
     {
-      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($3, $1));
+      $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst($1,10,$3));
+      delete $1;
     }
   | an_nonbvconst_term
   ;
@@ -1018,24 +1019,22 @@ an_nonbvconst_term:
       delete $2;
     }
    |  BVLEFTSHIFT_1_TOK an_term an_term 
+{
+       // shifting left by who know how much?
+      unsigned int w = $2->GetValueWidth();
+      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVLEFTSHIFT,w,*$2,*$3));
+         BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+         $$ = n;
+      delete $2;
+    }
+  | BVRIGHTSHIFT_1_TOK an_term an_term 
     {
+    // shifting right by who know how much?
       unsigned int w = $2->GetValueWidth();
-      unsigned int shift_amt = GetUnsignedConst(*$3);
-      if((unsigned)shift_amt < w) {
-       BEEV::ASTNode trailing_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0);
-       BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32, w-shift_amt-1);
-       BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,0);
-       BEEV::ASTNode m = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low);
-       BEEV::ASTNode * n = 
-         new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT,w,m,trailing_zeros));
-       BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-       $$ = n;
-      }
-      else {
-       $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      }
+      BEEV::ASTNode * n = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVRIGHTSHIFT,w,*$2,*$3));
+         BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
+         $$ = n;
       delete $2;
-      //delete $3;
     }
   |  BVRIGHTSHIFT_TOK an_term NUMERAL_TOK 
     {
@@ -1059,29 +1058,6 @@ an_nonbvconst_term:
       }
       delete $2;
     }
-   |  BVRIGHTSHIFT_1_TOK an_term an_term 
-    {
-      unsigned int shift_amt = GetUnsignedConst(*$3);
-      BEEV::ASTNode leading_zeros = BEEV::globalBeevMgr_for_parser->CreateBVConst(shift_amt, 0);
-      unsigned int w = $2->GetValueWidth();
-      
-      //the amount by which you are rightshifting
-      //is less-than/equal-to the length of input
-      //bitvector
-      if((unsigned)shift_amt < w) {
-       BEEV::ASTNode hi = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,w-1);
-       BEEV::ASTNode low = BEEV::globalBeevMgr_for_parser->CreateBVConst(32,shift_amt);
-       BEEV::ASTNode extract = BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVEXTRACT,w-shift_amt,*$2,hi,low);
-       BEEV::ASTNode * n = 
-         new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateTerm(BEEV::BVCONCAT, w,leading_zeros, extract));
-       BEEV::globalBeevMgr_for_parser->BVTypeCheck(*n);
-       $$ = n;
-      }
-      else {
-       $$ = new BEEV::ASTNode(BEEV::globalBeevMgr_for_parser->CreateBVConst(w,0));
-      }
-      delete $2;
-    }
   |  BVARITHRIGHTSHIFT_TOK an_term an_term
     {
       unsigned int shift_amt = GetUnsignedConst(*$3);

diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp
index fc715f6b8b97236003f042968649269d00213c4d..6e4941452105a8eab3e30eaeb25ad2c557f1620a 100644 (file)
--- a/simplifier/simplifier.cpp
+++ b/simplifier/simplifier.cpp
@@ -2020,6 +2020,20 @@ namespace BEEV {
       }
       break;
     }
+    case BVZX:
+      {
+      //a0 is the expr which is being zero extended
+      ASTNode a0 = SimplifyTerm(inputterm[0]);
+      //a1 represents the length of the term BVZX(a0)
+      ASTNode a1 = inputterm[1];
+      //output length of the BVSX term
+      unsigned len = inputValueWidth;
+
+       output = CreateTerm(BVZX,len,a0,a1);
+       break;
+      }
+      break;
+
     case BVSX:{
       //a0 is the expr which is being sign extended
       ASTNode a0 = SimplifyTerm(inputterm[0]);
@@ -2232,6 +2246,7 @@ namespace BEEV {
       output = CreateSimplifiedTermITE(t0,t1,t2);      
       break;
     }
+    case SBVREM:
     case SBVMOD:
     case SBVDIV: {
       ASTVec c = inputterm.GetChildren();
@@ -2245,7 +2260,7 @@ namespace BEEV {
     }
     case WRITE:     
     default:
-      FatalError("SimplifyTerm: Control should never reach here:", inputterm, k);
+      FatalError("SimplifyTermAux: Control should never reach here:", inputterm, k);
       return inputterm;
       break;
     }