From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 25 Nov 2009 20:12:47 +0000 (+0000)
Subject: added variable right shift to the CVC parser
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=22ac368ced741c455b19e072847fed2658d2143a;p=francis%2Fstp.git

added variable right shift to the CVC parser

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

diff --git a/src/parser/CVC.y b/src/parser/CVC.y
index 2bf9ad9..aad561c 100644
--- a/src/parser/CVC.y
+++ b/src/parser/CVC.y
@@ -919,7 +919,7 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
   $$ = n;
   delete $1;
 }
-|      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK 
+|      Expr BVRIGHTSHIFT_TOK NUMERAL_TOK
 {
   ASTNode len = ParserBM->CreateZeroConst($3);
   unsigned int w = $1->GetValueWidth();
@@ -934,20 +934,77 @@ Expr            :      TERMID_TOK { $$ = new ASTNode(ParserBM->GetLetMgr()->Reso
     ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVCONCAT, w,len, extract));
     BVTypeCheck(*n);
     $$ = n;
-  } 
+  }
   else
-    $$ = new ASTNode(ParserBM->CreateZeroConst(w));                      
+    $$ = new ASTNode(ParserBM->CreateZeroConst(w));
 
   delete $1;
 }
-/* |      Expr BVRIGHTSHIFT_TOK Expr */
-/* { */
-/*   //$1 is being shifted by variable shift amount $3 */
-/*   // */
+|      Expr BVRIGHTSHIFT_TOK Expr
+{
+  // VARIABLE RIGHT SHIFT
+  //
+  // $1 (THEEXPR) is being shifted
+  //
+  // $3 is the variable shift amount
+  ASTNode inputExpr = *$1;
+  ASTNode varShiftAmt = *$3;
 
-/*   delete $1; */
-/*   delete $3; */
-/* } */
+  unsigned int exprWidth = $1->GetValueWidth();
+  unsigned int shiftAmtWidth = $3->GetValueWidth();
+  ASTNode exprWidthNode = ParserBM->CreateBVConst(shiftAmtWidth, exprWidth);
+  
+  ASTNode cond, thenExpr, elseExpr;
+  unsigned int count = 0;
+  ASTNode hi = ParserBM->CreateBVConst(32,exprWidth-1);
+  while(count < exprWidth)
+    {
+      if(0 == count)
+	{
+	  // if count is zero then the appropriate rightshift expression is
+	  // THEEXPR itself
+	  elseExpr = inputExpr;
+	}
+      else
+	{
+	  // 1 <= count < exprWidth
+	  //
+	  // Construct appropriate conditional
+	  ASTNode countNode = ParserBM->CreateBVConst(shiftAmtWidth, count);
+	  cond = ParserBM->CreateNode(EQ, countNode, varShiftAmt);
+
+	  //Construct the rightshift expression padding @ Expr[hi:low]
+	  ASTNode low =
+	    ParserBM->CreateBVConst(32,count);
+	  ASTNode extract =
+	    ParserBM->CreateTerm(BVEXTRACT,exprWidth-count,inputExpr,hi,low);
+	  ASTNode padding =
+	    ParserBM->CreateZeroConst(count);
+	  thenExpr =
+	    ParserBM->CreateTerm(BVCONCAT, exprWidth, padding, extract);
+	  ASTNode ite =
+	    ParserBM->CreateTerm(ITE, exprWidth, cond, thenExpr, elseExpr);
+	  BVTypeCheck(ite);
+	  elseExpr = ite;
+	}
+      count++;
+    } //End of while loop
+
+  // if shiftamount is greater than or equal to exprwidth, then
+  // output is zero.
+  cond = ParserBM->CreateNode(BVGE, varShiftAmt, exprWidthNode);
+  thenExpr = ParserBM->CreateZeroConst(exprWidth);
+  ASTNode * ret =
+    new ASTNode(ParserBM->CreateTerm(ITE,
+				     exprWidth,
+				     cond, thenExpr, elseExpr));
+  BVTypeCheck(*ret);
+  //cout << *ret;
+
+  $$ = ret;
+  delete $1;
+  delete $3;
+}
 |      BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')' 
 {
   ASTNode * n = new ASTNode(ParserBM->CreateTerm(BVPLUS, $3, *$5));
diff --git a/tests/sample-tests/variable-rightshift-invalid.cvc b/tests/sample-tests/variable-rightshift-invalid.cvc
new file mode 100644
index 0000000..3df311b
--- /dev/null
+++ b/tests/sample-tests/variable-rightshift-invalid.cvc
@@ -0,0 +1,10 @@
+%% Regression level = 3
+%% Result = InValid
+%% Language = presentation
+
+X, Y : BITVECTOR(2);
+
+ASSERT X = 0bin11;
+ASSERT X >> Y = 0bin01;
+
+QUERY FALSE;
\ No newline at end of file
diff --git a/tests/sample-tests/variable-rightshift-valid.cvc b/tests/sample-tests/variable-rightshift-valid.cvc
new file mode 100644
index 0000000..dc90949
--- /dev/null
+++ b/tests/sample-tests/variable-rightshift-valid.cvc
@@ -0,0 +1,10 @@
+%% Regression level = 3
+%% Result = Valid
+%% Language = presentation
+
+X, Y : BITVECTOR(2);
+
+ASSERT X = 0bin11;
+ASSERT X >> Y = 0bin10;
+
+QUERY FALSE;
\ No newline at end of file