diff options
Diffstat (limited to 'lib/SMT')
| -rw-r--r-- | lib/SMT/SMTParser.cpp | 36 | ||||
| -rw-r--r-- | lib/SMT/SMTParser.h | 8 | ||||
| -rw-r--r-- | lib/SMT/main.cpp | 27 | ||||
| -rw-r--r-- | lib/SMT/smtlib.y | 72 |
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); } ; |