Recognizing more SMTLIB expressions (bitwise, etc.). Some of them

still need to actually be constructed.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74169 91177308-0d34-0410-b5e6-96231b3b80d8

4 files changed, 109 insertions, 200 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index dee3801c..32e453f0 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -12,7 +12,8 @@
 
 #include <iostream>
 #include <fstream>
-#include <cstring>
+#include <string>
+#include <sstream>
 #include <cassert>
 #include <stack>
 
@@ -66,6 +67,16 @@ int SMTParser::Error(const string& s) {
   return 0;
 }
 
+
+int SMTParser::StringToInt(const std::string& s) {
+  std::stringstream str(s);
+  int x;
+  str >> x;
+  assert(str);
+  return x;
+}
+
+
 void SMTParser::PushVarEnv() {
   cout << "Pushing new var env\n";
   varEnvs.push(VarEnv(varEnvs.top()));
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index ea5c34e5..780100b0 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -54,6 +54,8 @@ class SMTParser : public klee::expr::Parser {
   void Init(void);
 
   int Error(const std::string& s);
+  
+  int StringToInt(const std::string& s);
 
 
   typedef std::map<const std::string, ExprHandle> VarEnv;
@@ -61,7 +63,6 @@ class SMTParser : public klee::expr::Parser {
 
   std::stack<VarEnv> varEnvs;
   std::stack<FVarEnv> fvarEnvs;
- 
 
   void PushVarEnv(void);
   void PopVarEnv(void);
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index fb59316d..be909773 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -118,9 +118,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 [\n]            { SMTParser::parserTemp->lineNum++; }
 [ \t\r\f]	{ /* skip whitespace */ }
 
-{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
-{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; 
-		}
+{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
 
 ";"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
@@ -249,7 +247,6 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "rotate_right"  { return ROR_TOK; }
 
 
-[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
 ({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
 
 <<EOF>>         { return EOF_TOK; }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 38e58170..6469a9c3 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -98,7 +98,9 @@ int smtliberror(const char *s)
 */
 
 %type <node> an_formula an_logical_formula an_atom prop_atom
-%type <node> an_term basic_term an_fun an_arithmetic_fun an_pred
+%type <node> an_term basic_term 
+%type <node> an_fun an_arithmetic_fun an_bitwise_fun
+%type <node> an_pred
 %type <str> logic_name status attribute user_value annotation annotations 
 %type <str> var fvar
 
@@ -614,7 +616,13 @@ an_pred:
 
 
 an_arithmetic_fun:
-    LPAREN_TOK BVADD_TOK an_term an_term annotations
+
+    LPAREN_TOK BVNEG_TOK an_term an_term annotations
+    {
+      $$ = NULL;  // XXX: not supported yet
+    }
+
+  | LPAREN_TOK BVADD_TOK an_term an_term annotations
     {
       $$ = AddExpr::create($3, $4);
     }
@@ -651,11 +659,89 @@ an_arithmetic_fun:
 
   | LPAREN_TOK BVSMOD_TOK an_term an_term annotations
     {
-      $$ = NULL; // XXX: unsupported
+      $$ = NULL; // XXX: not supported yet
     }
 ;
 
 
+an_bitwise_fun:
+    LPAREN_TOK BVNOT_TOK an_term an_term annotations
+    {
+      $$ = NULL; // XXX: not supported yet
+    }
+
+  | LPAREN_TOK BVAND_TOK an_term an_term annotations
+    {
+      $$ = AndExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVOR_TOK an_term an_term annotations
+    {
+      $$ = OrExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVXOR_TOK an_term an_term annotations
+    {
+      $$ = XorExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+
+  | LPAREN_TOK BVSHL_TOK an_term an_term annotations
+    {
+      $$ = ShlExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVLSHR_TOK an_term an_term annotations
+    {
+      $$ = LShrExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVASHR_TOK an_term an_term annotations
+    {
+      $$ = AShrExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+
+  | LPAREN_TOK ROR_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+ 
+  | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+
+  | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+
+  | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations
+    {
+      $$ = ConcatExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      $$ = NULL; // TODO
+    }
+
+  | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
+    {
+      int off = PARSER->StringToInt(*$4);
+      $$ = ExtractExpr::create($8, off, PARSER->StringToInt(*$6) - off + 1);
+    }
+;
+
 
 an_fun:
     an_logical_formula
@@ -678,6 +764,11 @@ an_fun:
       $$ = $1;
     }
 
+  | an_bitwise_fun
+    {
+      $$ = $1;
+    }
+
 /*
 
       else if (ARRAYSENABLED && *$1 == "select") {
@@ -686,77 +777,6 @@ an_fun:
       else if (ARRAYSENABLED && *$1 == "store") {
         $$->push_back(VC->idExpr("_WRITE"));
       }
-      else if (BVENABLED && *$1 == "concat") {
-        $$->push_back(VC->idExpr("_CONCAT"));
-      }
-      else if (BVENABLED && *$1 == "bvnot") {
-        $$->push_back(VC->idExpr("_BVNEG"));
-      }
-      else if (BVENABLED && *$1 == "bvand") {
-        $$->push_back(VC->idExpr("_BVAND"));
-      }
-      else if (BVENABLED && *$1 == "bvor") {
-        $$->push_back(VC->idExpr("_BVOR"));
-      }
-      else if (BVENABLED && *$1 == "bvneg") {
-        $$->push_back(VC->idExpr("_BVUMINUS"));
-      }
-      else if (BVENABLED && *$1 == "bvadd") {
-        $$->push_back(VC->idExpr("_BVPLUS"));
-      }
-      else if (BVENABLED && *$1 == "bvmul") {
-        $$->push_back(VC->idExpr("_BVMULT"));
-      }
-      else if (BVENABLED && *$1 == "bvudiv") {
-        $$->push_back(VC->idExpr("_BVUDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvurem") {
-        $$->push_back(VC->idExpr("_BVUREM"));
-      }
-      else if (BVENABLED && *$1 == "bvshl") {
-        $$->push_back(VC->idExpr("_BVSHL"));
-      }
-      else if (BVENABLED && *$1 == "bvlshr") {
-        $$->push_back(VC->idExpr("_BVLSHR"));
-      }
-
-      else if (BVENABLED && *$1 == "bvxor") {
-        $$->push_back(VC->idExpr("_BVXOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxnor") {
-        $$->push_back(VC->idExpr("_BVXNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvcomp") {
-        $$->push_back(VC->idExpr("_BVCOMP"));
-      }
-
-      else if (BVENABLED && *$1 == "bvsub") {
-        $$->push_back(VC->idExpr("_BVSUB"));
-      }
-      else if (BVENABLED && *$1 == "bvsdiv") {
-        $$->push_back(VC->idExpr("_BVSDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvsrem") {
-        $$->push_back(VC->idExpr("_BVSREM"));
-      }
-      else if (BVENABLED && *$1 == "bvsmod") {
-        $$->push_back(VC->idExpr("_BVSMOD"));
-      }
-      else if (BVENABLED && *$1 == "bvashr") {
-        $$->push_back(VC->idExpr("_BVASHR"));
-      }
-
-      // For backwards compatibility:
-      else if (BVENABLED && *$1 == "shift_left0") {
-        $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "shift_right0") {
-        $$->push_back(VC->idExpr("_RIGHTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
 
       // Bitvector constants
       else if (BVENABLED &&
@@ -928,82 +948,12 @@ sort_symb:
     }
 ;
 
-pred_symb:
-    SYM_TOK
-    {
-      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVGE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVGT"));
-      }
-      else if (BVENABLED && *$1 == "bvslt") {
-        $$ = new CVC3::Expr(VC->idExpr("_BVSLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVSLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
-        $$ = new CVC3::Expr(VC->idExpr("_BVSGE"));
-      }
-      else if (BVENABLED && *$1 == "bvsgt") {
-        $$ = new CVC3::Expr(VC->idExpr("_BVSGT"));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | AR_SYMB 
-    { 
-      if ($1->length() == 1) {
-	switch ((*$1)[0]) {
-	  case '=': $$ = new CVC3::Expr(VC->idExpr("_EQ")); break;
-	  case '<': $$ = new CVC3::Expr(VC->idExpr("_LT")); break;
-	  case '>': $$ = new CVC3::Expr(VC->idExpr("_GT")); break;
-	  default: $$ = new CVC3::Expr(VC->idExpr(*$1)); break;
-	}
-      }
-      else {
-	if (*$1 == "<=") {
-	  $$ = new CVC3::Expr(VC->idExpr("_LE"));
-	} else if (*$1 == ">=") {
-	  $$ = new CVC3::Expr(VC->idExpr("_GE"));
-	}
-	else $$ = new CVC3::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-;
 */
 
 /*
 fun_symb:
     SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
     {
-      $$ = new std::vector<CVC3::Expr>;
-      if (BVENABLED && *$1 == "repeat") {
-        $$->push_back(VC->idExpr("_BVREPEAT"));
-      }
-      else if (BVENABLED && *$1 == "zero_extend") {
-        $$->push_back(VC->idExpr("_BVZEROEXTEND"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
-      else if (BVENABLED && *$1 == "rotate_left") {
-        $$->push_back(VC->idExpr("_BVROTL"));
-      }
-      else if (BVENABLED && *$1 == "rotate_right") {
-        $$->push_back(VC->idExpr("_BVROTR"));
-      }
       else if (BVENABLED &&
                $1->size() > 2 &&
                (*$1)[0] == 'b' &&
@@ -1021,56 +971,6 @@ fun_symb:
       delete $1;
       delete $3;
     }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      if (BVENABLED && *$1 == "extract") {
-        $$->push_back(VC->idExpr("_EXTRACT"));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      $$->push_back(VC->ratExpr(*$5));
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK
-    {
-
-    }
-
-  | AR_SYMB 
-    { 
-      $$ = new std::vector<CVC3::Expr>;
-      if ($1->length() == 1) {
-	switch ((*$1)[0]) {
-	case '+': $$->push_back(VC->idExpr("_PLUS")); break;
-	case '-': $$->push_back(VC->idExpr("_MINUS")); break;
-	case '*': $$->push_back(VC->idExpr("_MULT")); break;
-	case '~': $$->push_back(VC->idExpr("_UMINUS")); break;
-	case '/': $$->push_back(VC->idExpr("_DIVIDE")); break;
-        case '=': $$->push_back(VC->idExpr("_EQ")); break;
-        case '<': $$->push_back(VC->idExpr("_LT")); break;
-        case '>': $$->push_back(VC->idExpr("_GT")); break;
-	default: $$->push_back(VC->idExpr(*$1));
-	}
-      }
-      else {
-	if (*$1 == "<=") {
-	  $$->push_back(VC->idExpr("_LE"));
-	} else if (*$1 == ">=") {
-	  $$->push_back(VC->idExpr("_GE"));
-	}
-	else $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | NUMERAL_TOK
-    {
-      $$ = new std::vector<CVC3::Expr>;
-      $$->push_back(VC->ratExpr(*$1));
-      delete $1;
-    }
 ;
 */