aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/SMT/SMTParser.cpp36
-rw-r--r--lib/SMT/SMTParser.h8
-rw-r--r--lib/SMT/main.cpp27
-rw-r--r--lib/SMT/smtlib.y72
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);
}
;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-16 04:03:45 +0000