Added support for bitvector constants to the SMTLIB parser. Only

variable and array support left.



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

4 files changed, 45 insertions, 61 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 32e453f0..6e40978a 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -77,6 +77,15 @@ int SMTParser::StringToInt(const std::string& s) {
 }
 
 
+ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
+  cerr << "In GetConstExpr(): val=" << val << ", base=" << (unsigned)base << ", width=" << w << "\n";
+  assert(base == 2 || base == 10 || base == 16);
+  llvm::APInt ap(w, val.c_str(), val.length(), base);
+  
+  return klee::ConstantExpr::alloc(ap);
+}
+
+
 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 780100b0..1e24122f 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -56,6 +56,7 @@ class SMTParser : public klee::expr::Parser {
   int Error(const std::string& s);
   
   int StringToInt(const std::string& s);
+  ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
 
 
   typedef std::map<const std::string, ExprHandle> VarEnv;
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index be909773..f5633716 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -247,6 +247,11 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "rotate_right"  { return ROR_TOK; }
 
 
+"bv"[0-9]+              { smtliblval.str = new std::string(smtlibtext); return BV_TOK; }
+"bvbin"[0-1]+	        { smtliblval.str = new std::string(smtlibtext); return BVBIN_TOK; }
+"bvhex"[0-9,A-F,a-f]+	{ smtliblval.str = new std::string(smtlibtext); return BVHEX_TOK; }
+
+
 ({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 6469a9c3..febf76cd 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -98,7 +98,7 @@ int smtliberror(const char *s)
 */
 
 %type <node> an_formula an_logical_formula an_atom prop_atom
-%type <node> an_term basic_term 
+%type <node> an_term basic_term constant
 %type <node> an_fun an_arithmetic_fun an_bitwise_fun
 %type <node> an_pred
 %type <str> logic_name status attribute user_value annotation annotations 
@@ -109,6 +109,11 @@ int smtliberror(const char *s)
 %token <str> STRING_TOK
 %token <str> AR_SYMB
 %token <str> USER_VAL_TOK
+
+%token <str> BV_TOK
+%token <str> BVBIN_TOK
+%token <str> BVHEX_TOK
+
 %token TRUE_TOK
 %token FALSE_TOK
 %token ITE_TOK
@@ -770,69 +775,38 @@ an_fun:
     }
 
 /*
-
       else if (ARRAYSENABLED && *$1 == "select") {
         $$->push_back(VC->idExpr("_READ"));
       }
       else if (ARRAYSENABLED && *$1 == "store") {
         $$->push_back(VC->idExpr("_WRITE"));
       }
-
-      // Bitvector constants
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        bool done = false;
-        if ((*$1)[2] >= '0' && (*$1)[2] <= '9') {
-          int i = 3;
-          while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-          if ((*$1)[i] == '\0') {
-            $$->push_back(VC->idExpr("_BVCONST"));
-            $$->push_back(VC->ratExpr($1->substr(2), 10));
-            $$->push_back(VC->ratExpr(32));
-            done = true;
-          }
-        }
-        else if ($1->size() > 5) {
-          std::string s = $1->substr(0,5);
-          if (s == "bvbin") {
-            int i = 5;
-            while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i;
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 2));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-          else if (s == "bvhex") {
-            int i = 5;
-            char c = (*$1)[i];
-            while ((c >= '0' && c <= '9') ||
-                   (c >= 'a' && c <= 'f') ||
-                   (c >= 'A' && c <= 'F')) {
-              ++i;
-              c =(*$1)[i];
-            }
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 16));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-        }
-        if (!done) $$->push_back(VC->idExpr(*$1));
-      }
-      else {
-        $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
 */
+;
 
+constant:
+    BIT0_TOK
+    {
+      $$ = PARSER->GetConstExpr("0", 2, 1);
+    }
 
+  | BIT1_TOK
+    {
+      $$ = PARSER->GetConstExpr("1", 2, 1);
+    }
 
+  | BVBIN_TOK
+    {
+      $$ = PARSER->GetConstExpr($1->substr(5), 2, $1->length()-5);
+    }
+  | BVHEX_TOK
+    {
+      $$ = PARSER->GetConstExpr($1->substr(5), 16, ($1->length()-5)*4);
+    }
+  | BV_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
+    {
+      $$ = PARSER->GetConstExpr($1->substr(2), 10, PARSER->StringToInt(*$3));
+    }
 ;
 
 
@@ -860,14 +834,9 @@ an_term:
 
 
 basic_term:
-    BIT1_TOK
+    constant 
     {
-      $$ = ConstantExpr::create(1, 1);
-    }
-
-  | BIT0_TOK
-    { 
-      $$ = ConstantExpr::create(0, 1);;
+      $$ = $1;
     }
 
   | var