Added support for LET expressions. Added simple environment support

to SMTParser.


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

5 files changed, 110 insertions, 28 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 88d0a6c9..395241a0 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -14,6 +14,7 @@
 #include <fstream>
 #include <cstring>
 #include <cassert>
+#include <stack>
 
 using namespace std;
 using namespace klee;
@@ -35,6 +36,10 @@ SMTParser::SMTParser(const std::string filename) : fileName(filename),
 						   bvSize(0),
 						   queryParsed(false) {
   is = new ifstream(filename.c_str());
+  
+  // Initial empty environments
+  varEnvs.push(VarEnv());
+  fvarEnvs.push(FVarEnv());
 }
 
 void SMTParser::Init() {
@@ -60,3 +65,49 @@ int SMTParser::Error(const string& s) {
   exit(1);
   return 0;
 }
+
+void SMTParser::PushVarEnv() {
+  cout << "Pushing new var env\n";
+  varEnvs.push(VarEnv(varEnvs.top()));
+}
+
+void SMTParser::PopVarEnv() {
+  cout << "Popping new var env\n";
+  varEnvs.pop();
+}
+
+void SMTParser::AddVar(std::string name, ExprHandle val) {
+  cout << "Adding (" << name << ", " << val << ") to current var env.\n";
+  varEnvs.top()[name] = val;
+}
+
+ExprHandle SMTParser::GetVar(std::string name) {
+  VarEnv top = varEnvs.top();
+  if (top.find(name) == top.end()) {
+    std::cerr << "Cannot find variable ?" << name << "\n";
+    exit(1);
+  }
+  return top[name];
+}
+
+
+void SMTParser::PushFVarEnv() {
+  fvarEnvs.push(FVarEnv(fvarEnvs.top()));
+}
+
+void SMTParser::PopFVarEnv(void) {
+  fvarEnvs.pop();
+}
+
+void SMTParser::AddFVar(std::string name, ExprHandle val) {
+  fvarEnvs.top()[name] = val;
+}
+
+ExprHandle SMTParser::GetFVar(std::string name) {
+  FVarEnv top = fvarEnvs.top();
+  if (top.find(name) == top.end()) {
+    std::cerr << "Cannot find fvar $" << name << "\n";
+    exit(1);
+  }
+  return top[name];
+}
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index edc1258f..ea5c34e5 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -16,7 +16,8 @@
 #include <cassert>
 #include <iostream>
 #include <map>
-#include <cstring>
+#include <stack>
+#include <string>
 
 namespace klee {
 namespace expr {
@@ -53,6 +54,24 @@ class SMTParser : public klee::expr::Parser {
   void Init(void);
 
   int Error(const std::string& s);
+
+
+  typedef std::map<const std::string, ExprHandle> VarEnv;
+  typedef std::map<const std::string, ExprHandle> FVarEnv;
+
+  std::stack<VarEnv> varEnvs;
+  std::stack<FVarEnv> fvarEnvs;
+ 
+
+  void PushVarEnv(void);
+  void PopVarEnv(void);
+  void AddVar(std::string name, ExprHandle val); // to current var env
+  ExprHandle GetVar(std::string name); // from current var env
+
+  void PushFVarEnv(void);
+  void PopFVarEnv(void);
+  void AddFVar(std::string name, ExprHandle val); // to current fvar env
+  ExprHandle GetFVar(std::string name); // from current fvar env
 };
 
 }
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 4d2b8e0a..d5137782 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -13,4 +13,6 @@ int main(int argc, char** argv) {
   klee::expr::SMTParser smtParser(argv[1]);
 
   smtParser.Init();
+  
+  cout << "Query: " << smtParser.query << "\n"; 
 }
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
index 0d955bf8..fb59316d 100644
--- a/lib/SMT/smtlib.lex
+++ b/lib/SMT/smtlib.lex
@@ -218,6 +218,7 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 "bvxor"         { return BVXOR_TOK; }
 "bvxnor"        { return BVXNOR_TOK; }
 
+"="             { return EQ_TOK; }
 "bvcomp"        { return BVCOMP_TOK; }
 "bvult"         { return BVULT_TOK; }
 "bvule"         { return BVULE_TOK; }
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 12284d89..753b24b3 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -32,6 +32,7 @@ using namespace klee;
 using namespace klee::expr;
 
 // Define shortcuts for various things
+#define PARSER SMTParser::parserTemp
 #define DONE SMTParser::parserTemp->done
 #define EXPR SMTParser::parserTemp->query
 #define ASSUMPTIONS SMTParser::parserTemp->assumptions
@@ -98,8 +99,8 @@ 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 <str> logic_name status attribute user_value annotation annotations
-
+%type <str> logic_name status attribute user_value annotation annotations 
+%type <str> var
 
 %token <str> NUMERAL_TOK
 %token <str> SYM_TOK
@@ -170,6 +171,7 @@ int smtliberror(const char *s)
 %token BVXOR_TOK
 %token BVXNOR_TOK
 
+%token EQ_TOK
 %token BVCOMP_TOK
 %token BVULT_TOK
 %token BVULE_TOK
@@ -499,16 +501,21 @@ an_formula:
     {
       $$ = $1;
     }
-/*
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
+
+
+  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK 
+        { 
+	  PARSER->PushVarEnv();
+	  PARSER->AddVar(*$4, $5); 
+	} 
+    an_formula RPAREN_TOK
     {
-      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
+      $$ = $8;
+      PARSER->PopVarEnv();
     }
+
+
+/*
   | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK
     {
       CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
@@ -517,15 +524,7 @@ an_formula:
       delete $5;
       delete $7;
     }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK
-    {
-      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
+
   | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK
     {
       CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
@@ -610,7 +609,16 @@ prop_atom:
 
 
 an_pred:
-    LPAREN_TOK BVULT_TOK an_term an_term RPAREN_TOK
+    LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+  | LPAREN_TOK EQ_TOK an_term an_term annotations RPAREN_TOK
+    {
+      $$ = EqExpr::create($3, $4);
+    }
+
+  | LPAREN_TOK BVULT_TOK an_term an_term RPAREN_TOK
     {
       $$ = UltExpr::create($3, $4);
     }
@@ -752,7 +760,7 @@ an_arithmetic_fun:
     {
       $$ = NULL; // XXX: unsupported
     }
-  | LPAREN_TOK BVSREM_TOK an_term an_term annotations RPAREN_TOK
+  | LPAREN_TOK BVSMOD_TOK an_term an_term annotations RPAREN_TOK
     {
       $$ = NULL; // XXX: unsupported
     }
@@ -964,10 +972,12 @@ basic_term:
     {
       $$ = $1;
     }
+*/
   | var
     {
-      $$ = $1;
+      $$ = PARSER->GetVar(*$1);
     }
+/*
   | fun_symb 
     {
       if ($1->size() == 1) {
@@ -1194,20 +1204,19 @@ attribute:
     }
 ;
 
-/*
+
 var:
     QUESTION_TOK SYM_TOK
     {
-      $$ = new CVC3::Expr(VC->idExpr(*$2));
-      delete $2;
+      $$ = $2;
     }
 ;
 
+/*
 fvar:
     DOLLAR_TOK SYM_TOK
     {
-      $$ = new CVC3::Expr(VC->idExpr(*$2));
-      delete $2;
+      $$ = $2;
     }
 ;
 */