Added support for bitvector variables to the SMTLIB parser (currently

widths have to be multiples of 8).



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

4 files changed, 43 insertions, 15 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 6e40978a..619d7ff6 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -77,6 +77,28 @@ int SMTParser::StringToInt(const std::string& s) {
 }
 
 
+void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
+  // for now, only allow variables which are multiples of 8
+  if (w % 8 != 0) {
+    cout << "BitVec not multiple of 8 (" << w << ").  Need to update code.\n";
+    exit(1);
+  }
+  
+  std::cout << "Declaring " << name << " of width " << w << "\n";
+  
+  Array *arr = new Array(name, w / 8);
+  
+  ref<Expr> *kids = new ref<Expr>[w/8];
+  for (unsigned i=0; i < w/8; i++)
+    kids[i] = ReadExpr::create(UpdateList(arr, NULL), 
+			       ConstantExpr::create(i, 32));
+  ref<Expr> var = ConcatExpr::createN(w/8, kids);
+  delete [] kids;
+  
+  AddVar(name, var);
+}
+
+
 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);
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index 1e24122f..bae4a23f 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -58,6 +58,8 @@ class SMTParser : public klee::expr::Parser {
   int StringToInt(const std::string& s);
   ExprHandle GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w);
 
+  void DeclareExpr(std::string name, Expr::Width w);
+
 
   typedef std::map<const std::string, ExprHandle> VarEnv;
   typedef std::map<const std::string, ExprHandle> FVarEnv;
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index f5633716..c614c683 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -154,6 +154,8 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
                           SMTParser::parserTemp->lineNum++; }
 <USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }
 
+"BitVec"        { return BITVEC_TOK; }
+
 "true"          { return TRUE_TOK; }
 "false"         { return FALSE_TOK; }
 "ite"           { return ITE_TOK; }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index febf76cd..3fef3e64 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -102,7 +102,7 @@ int smtliberror(const char *s)
 %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
+%type <str> var fvar symb
 
 %token <str> NUMERAL_TOK
 %token <str> SYM_TOK
@@ -114,6 +114,8 @@ int smtliberror(const char *s)
 %token <str> BVBIN_TOK
 %token <str> BVHEX_TOK
 
+%token BITVEC_TOK
+
 %token TRUE_TOK
 %token FALSE_TOK
 %token ITE_TOK
@@ -264,12 +266,13 @@ bench_attribute:
     { 
       // XXX?
     }
+*/
 
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK
+  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK LPAREN_TOK SYM_TOK BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK RPAREN_TOK RPAREN_TOK
     {
-      //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
-      //delete $4;
+      PARSER->DeclareExpr(*$5, atoi($8->c_str()));
     }
+/*
   | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
     {
       //$$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
@@ -435,7 +438,8 @@ an_logical_formula:
 
     LPAREN_TOK NOT_TOK an_formula annotations
     {
-      $$ = Expr::createNot($3);
+      //$$ = Expr::createNot($3);
+      $$ = NULL;
     }
 
   | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
@@ -843,18 +847,11 @@ basic_term:
     {
       $$ = PARSER->GetVar(*$1);
     }
-/*
-  | fun_symb 
+  | symb
     {
-      if ($1->size() == 1) {
-        $$ = new CVC3::Expr(((*$1)[0]));
-      }
-      else {
-        $$ = new CVC3::Expr(VC->listExpr(*$1));
-      }
-      delete $1;
+      std::cout << "SYMBOL " << *$1 << "\n";
+      $$ = PARSER->GetVar(*$1);
     }
-*/
 ;
 
 
@@ -966,5 +963,10 @@ fvar:
     }
 ;
 
+symb:
+    SYM_TOK
+    {
+      $$ = $1;
+    }
 
 %%