Use a builder in the SMT parser instead of constructing expressions

directly.



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

4 files changed, 89 insertions, 54 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 5edff9d0..b6ac5480 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -8,6 +8,8 @@
 //===----------------------------------------------------------------------===//
 
 #include "SMTParser.h"
+
+#include "klee/ExprBuilder.h"
 #include "expr/Parser.h"
 
 #include <iostream>
@@ -32,13 +34,15 @@ extern void smtlib_setInteractive(bool);
 
 SMTParser* SMTParser::parserTemp = NULL;
 
-SMTParser::SMTParser(const std::string filename) : fileName(filename), 
-						   lineNum(1),
-						   done(false),
-						   query(NULL),
-						   bvSize(0),
-						   queryParsed(false) {
-  is = new ifstream(filename.c_str());
+SMTParser::SMTParser(const std::string _filename, 
+		     ExprBuilder* _builder) : fileName(_filename),
+					      lineNum(1),
+					      done(false),
+					      query(NULL),
+					      bvSize(0),
+					      queryParsed(false),
+					      builder(_builder) {
+  is = new ifstream(fileName.c_str());
   
   // Initial empty environments
   varEnvs.push(VarEnv());
@@ -87,9 +91,9 @@ ExprHandle SMTParser::CreateAnd(std::vector<ExprHandle> kids) {
   if (n_kids == 1)
     return kids[0];
 
-  ExprHandle r = AndExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  ExprHandle r = builder->And(kids[n_kids-2], kids[n_kids-1]);
   for (int i=n_kids-3; i>=0; i--)
-    r = AndExpr::create(kids[i], r);
+    r = builder->And(kids[i], r);
   return r;
 }
 
@@ -99,9 +103,9 @@ ExprHandle SMTParser::CreateOr(std::vector<ExprHandle> kids) {
   if (n_kids == 1)
     return kids[0];
 
-  ExprHandle r = OrExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  ExprHandle r = builder->Or(kids[n_kids-2], kids[n_kids-1]);
   for (int i=n_kids-3; i>=0; i--)
-    r = OrExpr::create(kids[i], r);
+    r = builder->Or(kids[i], r);
   return r;
 }
 
@@ -111,9 +115,9 @@ ExprHandle SMTParser::CreateXor(std::vector<ExprHandle> kids) {
   if (n_kids == 1)
     return kids[0];
 
-  ExprHandle r = XorExpr::create(kids[n_kids-2], kids[n_kids-1]);
+  ExprHandle r = builder->Xor(kids[n_kids-2], kids[n_kids-1]);
   for (int i=n_kids-3; i>=0; i--)
-    r = XorExpr::create(kids[i], r);
+    r = builder->Xor(kids[i], r);
   return r;
 }
 
@@ -133,9 +137,9 @@ void SMTParser::DeclareExpr(std::string name, Expr::Width w) {
   
   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);
+    kids[i] = builder->Read(UpdateList(arr, NULL), 
+			    builder->Constant(i, 32));
+  ref<Expr> var = ConcatExpr::createN(w/8, kids); // XXX: move to builder?
   delete [] kids;
   
   AddVar(name, var);
diff --git a/lib/SMT/SMTParser.h b/lib/SMT/SMTParser.h
index 3d64a9b2..798e70b3 100644
--- a/lib/SMT/SMTParser.h
+++ b/lib/SMT/SMTParser.h
@@ -20,12 +20,14 @@
 #include <string>
 
 namespace klee {
+  class ExprBuilder;
+  
 namespace expr {
 
 class SMTParser : public klee::expr::Parser {
   private:
     void *buf;
-
+    
  public:
   /* For interacting w/ the actual parser, should make this nicer */
   static SMTParser* parserTemp;
@@ -40,8 +42,10 @@ class SMTParser : public klee::expr::Parser {
 
   int bvSize;
   bool queryParsed;
+
+  klee::ExprBuilder *builder;
     
-  SMTParser(const std::string filename);
+  SMTParser(const std::string filename, ExprBuilder *builder);
   
   virtual klee::expr::Decl *ParseTopLevelDecl();
   
diff --git a/lib/SMT/main.cpp b/lib/SMT/main.cpp
index 38bfac86..934f0702 100644
--- a/lib/SMT/main.cpp
+++ b/lib/SMT/main.cpp
@@ -1,8 +1,11 @@
 #include "SMTParser.h"
 
+#include "klee/ExprBuilder.h"
+
 #include <iostream>
 
 using namespace std;
+using namespace klee;
 
 int main(int argc, char** argv) {
   if (argc != 2) {
@@ -10,7 +13,29 @@ int main(int argc, char** argv) {
     return 1;
   }
   
-  klee::expr::SMTParser smtParser(argv[1]);
+  enum BuilderKinds {
+    DefaultBuilder,
+    ConstantFoldingBuilder,
+    SimplifyingBuilder
+  } BuilderKind = SimplifyingBuilder;
+
+  ExprBuilder *Builder = 0;
+  switch (BuilderKind) {
+  case DefaultBuilder:
+    Builder = createDefaultExprBuilder();
+    break;
+  case ConstantFoldingBuilder:
+    Builder = createDefaultExprBuilder();
+    Builder = createConstantFoldingExprBuilder(Builder);
+    break;
+  case SimplifyingBuilder:
+    Builder = createDefaultExprBuilder();
+    Builder = createConstantFoldingExprBuilder(Builder);
+    Builder = createSimplifyingExprBuilder(Builder);
+    break;
+  }
+  
+  klee::expr::SMTParser smtParser(argv[1], Builder);
 
   smtParser.Init();
   
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
index 0efc5703..28a434c9 100644
--- a/lib/SMT/smtlib.y
+++ b/lib/SMT/smtlib.y
@@ -25,6 +25,7 @@
 
 #include "SMTParser.h"
 #include "klee/Expr.h"
+#include "klee/ExprBuilder.h"
 
 #include <sstream>
 
@@ -33,6 +34,7 @@ using namespace klee::expr;
 
 // Define shortcuts for various things
 #define PARSER SMTParser::parserTemp
+#define BUILDER SMTParser::parserTemp->builder
 #define DONE SMTParser::parserTemp->done
 #define EXPR SMTParser::parserTemp->query
 #define ASSUMPTIONS SMTParser::parserTemp->assumptions
@@ -434,17 +436,17 @@ an_logical_formula:
 
     LPAREN_TOK NOT_TOK an_formula annotations
     {
-      $$ = NotExpr::create($3);
+      $$ = BUILDER->Not($3);
     }
 
   | LPAREN_TOK IMPLIES_TOK an_formula an_formula annotations
     {
-      $$ = Expr::createImplies($3, $4);
+      $$ = Expr::createImplies($3, $4);  // XXX: move to builder?
     }
 
   | LPAREN_TOK IF_THEN_ELSE_TOK an_formula an_formula an_formula annotations
     {
-      $$ = SelectExpr::create($3, $4, $5);
+      $$ = BUILDER->Select($3, $4, $5);
     }
 
   | LPAREN_TOK AND_TOK an_formulas annotations
@@ -464,7 +466,7 @@ an_logical_formula:
 
   | LPAREN_TOK IFF_TOK an_formula an_formula annotations
     {
-      $$ = EqExpr::create($3, $4);
+      $$ = BUILDER->Eq($3, $4);
     }
 ;
 
@@ -557,12 +559,12 @@ an_atom:
 prop_atom:
     TRUE_TOK
     {
-      $$ = ConstantExpr::create(1, 1);
+      $$ = BUILDER->Constant(1, 1);
     }
 
   | FALSE_TOK
     { 
-      $$ = ConstantExpr::create(0, 1);;
+      $$ = BUILDER->Constant(0, 1);;
     }
 
   | fvar
@@ -575,47 +577,47 @@ prop_atom:
 an_pred:
     LPAREN_TOK EQ_TOK an_term an_term annotations
     {
-      $$ = EqExpr::create($3, $4);
+      $$ = BUILDER->Eq($3, $4);
     }
 
   | LPAREN_TOK BVULT_TOK an_term an_term annotations
     {
-      $$ = UltExpr::create($3, $4);
+      $$ = BUILDER->Ult($3, $4);
     }
 
   | LPAREN_TOK BVULE_TOK an_term an_term annotations
     {
-      $$ = UleExpr::create($3, $4);
+      $$ = BUILDER->Ule($3, $4);
     }
 
   | LPAREN_TOK BVUGT_TOK an_term an_term annotations
     {
-      $$ = UgtExpr::create($3, $4);
+      $$ = BUILDER->Ugt($3, $4);
     }
 
   | LPAREN_TOK BVUGE_TOK an_term an_term annotations
     {
-      $$ = UgeExpr::create($3, $4);
+      $$ = BUILDER->Uge($3, $4);
     }
 
   | LPAREN_TOK BVSLT_TOK an_term an_term annotations
     {
-      $$ = SltExpr::create($3, $4);
+      $$ = BUILDER->Slt($3, $4);
     }
 
   | LPAREN_TOK BVSLE_TOK an_term an_term annotations
     {
-      $$ = SleExpr::create($3, $4);
+      $$ = BUILDER->Sle($3, $4);
     }
 
   | LPAREN_TOK BVSGT_TOK an_term an_term annotations
     {
-      $$ = SgtExpr::create($3, $4);
+      $$ = BUILDER->Sgt($3, $4);
     }
 
   | LPAREN_TOK BVSGE_TOK an_term an_term annotations
     {
-      $$ = SgeExpr::create($3, $4);
+      $$ = BUILDER->Sge($3, $4);
     }
 ;
 
@@ -630,37 +632,37 @@ an_arithmetic_fun:
 
   | LPAREN_TOK BVADD_TOK an_term an_term annotations
     {
-      $$ = AddExpr::create($3, $4);
+      $$ = BUILDER->Add($3, $4);
     }
 
   | LPAREN_TOK BVSUB_TOK an_term an_term annotations
     {
-      $$ = SubExpr::create($3, $4);
+      $$ = BUILDER->Sub($3, $4);
     }
 
   | LPAREN_TOK BVMUL_TOK an_term an_term annotations
     {
-      $$ = MulExpr::create($3, $4);
+      $$ = BUILDER->Mul($3, $4);
     }
 
   | LPAREN_TOK BVUDIV_TOK an_term an_term annotations
     {
-      $$ = UDivExpr::create($3, $4);
+      $$ = BUILDER->UDiv($3, $4);
     }
 
   | LPAREN_TOK BVUREM_TOK an_term an_term annotations
     {
-      $$ = URemExpr::create($3, $4);
+      $$ = BUILDER->URem($3, $4);
     }
 
   | LPAREN_TOK BVSDIV_TOK an_term an_term annotations
     {
-      $$ = SDivExpr::create($3, $4);
+      $$ = BUILDER->SDiv($3, $4);
     }
 
   | LPAREN_TOK BVSREM_TOK an_term an_term annotations
     {
-      $$ = SRemExpr::create($3, $4);
+      $$ = BUILDER->SRem($3, $4);
     }
 
   | LPAREN_TOK BVSMOD_TOK an_term an_term annotations
@@ -674,22 +676,22 @@ an_arithmetic_fun:
 an_bitwise_fun:
     LPAREN_TOK BVNOT_TOK an_term annotations
     {
-      $$ = NotExpr::create($3);
+      $$ = BUILDER->Not($3);
     }
 
   | LPAREN_TOK BVAND_TOK an_term an_term annotations
     {
-      $$ = AndExpr::create($3, $4);
+      $$ = BUILDER->And($3, $4);
     }
 
   | LPAREN_TOK BVOR_TOK an_term an_term annotations
     {
-      $$ = OrExpr::create($3, $4);
+      $$ = BUILDER->Or($3, $4);
     }
 
   | LPAREN_TOK BVXOR_TOK an_term an_term annotations
     {
-      $$ = XorExpr::create($3, $4);
+      $$ = BUILDER->Xor($3, $4);
     }
 
   | LPAREN_TOK BVXNOR_TOK an_term an_term annotations
@@ -700,17 +702,17 @@ an_bitwise_fun:
 
   | LPAREN_TOK BVSHL_TOK an_term an_term annotations
     {
-      $$ = ShlExpr::create($3, $4);
+      $$ = BUILDER->Shl($3, $4);
     }
 
   | LPAREN_TOK BVLSHR_TOK an_term an_term annotations
     {
-      $$ = LShrExpr::create($3, $4);
+      $$ = BUILDER->LShr($3, $4);
     }
 
   | LPAREN_TOK BVASHR_TOK an_term an_term annotations
     {
-      $$ = AShrExpr::create($3, $4);
+      $$ = BUILDER->AShr($3, $4);
     }
 
   | LPAREN_TOK ROL_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
@@ -727,17 +729,17 @@ an_bitwise_fun:
  
   | LPAREN_TOK ZEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
     {
-      $$ = ZExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
+      $$ = BUILDER->ZExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
     }
 
   | LPAREN_TOK SEXT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
     {
-      $$ = SExtExpr::create($6, $6->getWidth() + PARSER->StringToInt(*$4));
+      $$ = BUILDER->SExt($6, $6->getWidth() + PARSER->StringToInt(*$4));
     }
 
   | LPAREN_TOK BVCONCAT_TOK an_term an_term annotations
     {
-      $$ = ConcatExpr::create($3, $4);
+      $$ = BUILDER->Concat($3, $4);
     }
 
   | LPAREN_TOK REPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
@@ -749,7 +751,7 @@ an_bitwise_fun:
   | LPAREN_TOK BVEXTRACT_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK an_term annotations
     {
       int off = PARSER->StringToInt(*$6);
-      $$ = ExtractExpr::create($8, off, PARSER->StringToInt(*$4) - off + 1);
+      $$ = BUILDER->Extract($8, off, PARSER->StringToInt(*$4) - off + 1);
     }
 ;
 
@@ -767,7 +769,7 @@ an_fun:
 
   | LPAREN_TOK BVCOMP_TOK an_term an_term annotations
     {
-      $$ = EqExpr::create($3, $4);
+      $$ = BUILDER->Eq($3, $4);
     }
  
   | an_arithmetic_fun
@@ -834,7 +836,7 @@ an_term:
 
   | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations
     {
-      $$ = SelectExpr::create($3, $4, $5);
+      $$ = BUILDER->Select($3, $4, $5);
     }
 ;