diff options
| -rw-r--r-- | include/expr/Parser.h | 8 | ||||
| -rw-r--r-- | lib/Expr/ExprBuilder.cpp | 6 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 146 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 53 |
4 files changed, 137 insertions, 76 deletions
diff --git a/include/expr/Parser.h b/include/expr/Parser.h index f67e27ab..d2135f12 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -20,6 +20,8 @@ namespace llvm { } namespace klee { + class ExprBuilder; + namespace expr { // These are the language types we manipulate. typedef ref<Expr> ExprHandle; @@ -223,8 +225,12 @@ namespace expr { /// MemoryBuffer. /// /// \arg Name - The name to use in diagnostic messages. + /// \arg MB - The input data. + /// \arg Builder - The expression builder to use for constructing + /// expressions. static Parser *Create(const std::string Name, - const llvm::MemoryBuffer *MB); + const llvm::MemoryBuffer *MB, + ExprBuilder *Builder); }; } } diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp index bc30933b..f373e2b8 100644 --- a/lib/Expr/ExprBuilder.cpp +++ b/lib/Expr/ExprBuilder.cpp @@ -11,6 +11,12 @@ using namespace klee; +ExprBuilder::ExprBuilder() { +} + +ExprBuilder::~ExprBuilder() { +} + namespace { class DefaultExprBuilder : public ExprBuilder { virtual ref<Expr> Constant(uint64_t Value, Expr::Width W) { diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index c9d401e0..c978fe0b 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -12,6 +12,7 @@ #include "expr/Lexer.h" #include "klee/Constraints.h" +#include "klee/ExprBuilder.h" #include "klee/Solver.h" #include "klee/util/ExprPPrinter.h" @@ -107,6 +108,8 @@ namespace { const std::string Filename; const MemoryBuffer *TheMemoryBuffer; + ExprBuilder *Builder; + Lexer TheLexer; unsigned MaxErrors; unsigned NumErrors; @@ -318,11 +321,13 @@ namespace { public: ParserImpl(const std::string _Filename, - const MemoryBuffer *MB) : Filename(_Filename), - TheMemoryBuffer(MB), - TheLexer(MB), - MaxErrors(~0u), - NumErrors(0) {} + const MemoryBuffer *MB, + ExprBuilder *_Builder) : Filename(_Filename), + TheMemoryBuffer(MB), + Builder(_Builder), + TheLexer(MB), + MaxErrors(~0u), + NumErrors(0) {} /// Initialize - Initialize the parsing state. This must be called /// prior to the start of parsing. @@ -591,7 +596,7 @@ DeclResult ParserImpl::ParseQueryCommand() { while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { Error("unexpected end of file."); - Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool)); + Res = ExprResult(Builder->Constant(0, Expr::Bool)); goto exit; } @@ -603,7 +608,7 @@ DeclResult ParserImpl::ParseQueryCommand() { Res = ParseExpr(TypeResult(Expr::Bool)); if (!Res.isValid()) // Error emitted by ParseExpr. - Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool)); + Res = ExprResult(Builder->Constant(0, Expr::Bool)); // Return if there are no optional lists of things to evaluate. if (Tok.kind == Token::RParen) @@ -706,7 +711,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) { if (Tok.kind == Token::KWFalse || Tok.kind == Token::KWTrue) { bool Value = Tok.kind == Token::KWTrue; ConsumeToken(); - return ExprResult(ConstantExpr::alloc(Value, Expr::Bool)); + return ExprResult(Builder->Constant(Value, Expr::Bool)); } if (Tok.kind == Token::Number) { @@ -751,7 +756,7 @@ ExprResult ParserImpl::ParseExpr(TypeResult ExpectedType) { // FIXME: Maybe we should let the symbol table map to invalid // entries? if (Label && ExpectedType.isValid()) { - ref<Expr> Value = ConstantExpr::alloc(0, ExpectedType.get()); + ref<Expr> Value = Builder->Constant(0, ExpectedType.get()); ExprSymTab.insert(std::make_pair(Label, Value)); } return Res; @@ -976,7 +981,7 @@ ExprResult ParserImpl::ParseParenExpr(TypeResult FIXME_UNUSED) { default: Error("internal error, unimplemented special form.", Name); SkipUntilRParen(); - return ExprResult(ConstantExpr::alloc(0, ResTy)); + return ExprResult(Builder->Constant(0, ResTy)); } } @@ -1000,29 +1005,29 @@ ExprResult ParserImpl::ParseUnaryParenExpr(const Token &Name, if (Tok.kind == Token::RParen) { Error("unexpected end of arguments.", Name); ConsumeRParen(); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } ExprResult Arg = ParseExpr(IsFixed ? ResTy : TypeResult()); if (!Arg.isValid()) - Arg = ConstantExpr::alloc(0, ResTy); + Arg = Builder->Constant(0, ResTy); ExpectRParen("unexpected argument in unary expression."); ExprHandle E = Arg.get(); switch (Kind) { case eMacroKind_Not: - return EqExpr::alloc(ConstantExpr::alloc(0, E->getWidth()), E); + return Builder->Eq(Builder->Constant(0, E->getWidth()), E); case eMacroKind_Neg: - return SubExpr::alloc(ConstantExpr::alloc(0, E->getWidth()), E); + return Builder->Sub(Builder->Constant(0, E->getWidth()), E); case Expr::SExt: // FIXME: Type check arguments. - return SExtExpr::alloc(E, ResTy); + return Builder->SExt(E, ResTy); case Expr::ZExt: // FIXME: Type check arguments. - return ZExtExpr::alloc(E, ResTy); + return Builder->ZExt(E, ResTy); default: Error("internal error, unhandled kind.", Name); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } } @@ -1091,44 +1096,44 @@ ExprResult ParserImpl::ParseBinaryParenExpr(const Token &Name, ParseMatchedBinaryArgs(Name, IsFixed ? TypeResult(ResTy) : TypeResult(), LHS, RHS); if (!LHS.isValid() || !RHS.isValid()) - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); ref<Expr> LHS_E = LHS.get(), RHS_E = RHS.get(); if (LHS_E->getWidth() != RHS_E->getWidth()) { Error("type widths do not match in binary expression", Name); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } switch (Kind) { - case Expr::Add: return AddExpr::alloc(LHS_E, RHS_E); - case Expr::Sub: return SubExpr::alloc(LHS_E, RHS_E); - case Expr::Mul: return MulExpr::alloc(LHS_E, RHS_E); - case Expr::UDiv: return UDivExpr::alloc(LHS_E, RHS_E); - case Expr::SDiv: return SDivExpr::alloc(LHS_E, RHS_E); - case Expr::URem: return URemExpr::alloc(LHS_E, RHS_E); - case Expr::SRem: return SRemExpr::alloc(LHS_E, RHS_E); - - case Expr::AShr: return AShrExpr::alloc(LHS_E, RHS_E); - case Expr::LShr: return LShrExpr::alloc(LHS_E, RHS_E); - case Expr::Shl: return AndExpr::alloc(LHS_E, RHS_E); - - case Expr::And: return AndExpr::alloc(LHS_E, RHS_E); - case Expr::Or: return OrExpr::alloc(LHS_E, RHS_E); - case Expr::Xor: return XorExpr::alloc(LHS_E, RHS_E); - - case Expr::Eq: return EqExpr::alloc(LHS_E, RHS_E); - case Expr::Ne: return NeExpr::alloc(LHS_E, RHS_E); - case Expr::Ult: return UltExpr::alloc(LHS_E, RHS_E); - case Expr::Ule: return UleExpr::alloc(LHS_E, RHS_E); - case Expr::Ugt: return UgtExpr::alloc(LHS_E, RHS_E); - case Expr::Uge: return UgeExpr::alloc(LHS_E, RHS_E); - case Expr::Slt: return SltExpr::alloc(LHS_E, RHS_E); - case Expr::Sle: return SleExpr::alloc(LHS_E, RHS_E); - case Expr::Sgt: return SgtExpr::alloc(LHS_E, RHS_E); - case Expr::Sge: return SgeExpr::alloc(LHS_E, RHS_E); + case Expr::Add: return Builder->Add(LHS_E, RHS_E); + case Expr::Sub: return Builder->Sub(LHS_E, RHS_E); + case Expr::Mul: return Builder->Mul(LHS_E, RHS_E); + case Expr::UDiv: return Builder->UDiv(LHS_E, RHS_E); + case Expr::SDiv: return Builder->SDiv(LHS_E, RHS_E); + case Expr::URem: return Builder->URem(LHS_E, RHS_E); + case Expr::SRem: return Builder->SRem(LHS_E, RHS_E); + + case Expr::AShr: return Builder->AShr(LHS_E, RHS_E); + case Expr::LShr: return Builder->LShr(LHS_E, RHS_E); + case Expr::Shl: return Builder->And(LHS_E, RHS_E); + + case Expr::And: return Builder->And(LHS_E, RHS_E); + case Expr::Or: return Builder->Or(LHS_E, RHS_E); + case Expr::Xor: return Builder->Xor(LHS_E, RHS_E); + + case Expr::Eq: return Builder->Eq(LHS_E, RHS_E); + case Expr::Ne: return Builder->Ne(LHS_E, RHS_E); + case Expr::Ult: return Builder->Ult(LHS_E, RHS_E); + case Expr::Ule: return Builder->Ule(LHS_E, RHS_E); + case Expr::Ugt: return Builder->Ugt(LHS_E, RHS_E); + case Expr::Uge: return Builder->Uge(LHS_E, RHS_E); + case Expr::Slt: return Builder->Slt(LHS_E, RHS_E); + case Expr::Sle: return Builder->Sle(LHS_E, RHS_E); + case Expr::Sgt: return Builder->Sgt(LHS_E, RHS_E); + case Expr::Sge: return Builder->Sge(LHS_E, RHS_E); default: Error("FIXME: unhandled kind.", Name); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } } @@ -1138,15 +1143,15 @@ ExprResult ParserImpl::ParseSelectParenExpr(const Token &Name, if (Tok.kind == Token::RParen) { Error("unexpected end of arguments.", Name); ConsumeRParen(); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } ExprResult Cond = ParseExpr(Expr::Bool); ExprResult LHS, RHS; ParseMatchedBinaryArgs(Name, ResTy, LHS, RHS); if (!Cond.isValid() || !LHS.isValid() || !RHS.isValid()) - return ConstantExpr::alloc(0, ResTy); - return SelectExpr::alloc(Cond.get(), LHS.get(), RHS.get()); + return Builder->Constant(0, ResTy); + return Builder->Select(Cond.get(), LHS.get(), RHS.get()); } @@ -1162,7 +1167,7 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name, // Skip to end of expr on error. if (!E.isValid()) { SkipUntilRParen(); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } Kids.push_back(E.get()); @@ -1173,9 +1178,10 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name, if (Width != ResTy) { Error("concat does not match expected result size."); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } + // FIXME: Use builder! return ConcatExpr::createN(Kids.size(), &Kids[0]); } @@ -1196,15 +1202,15 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name, ExpectRParen("unexpected argument to expression."); if (!OffsetExpr.isValid() || !Child.isValid()) - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); unsigned Offset = (unsigned) OffsetExpr.get(); if (Offset + ResTy > Child.get()->getWidth()) { Error("extract out-of-range of child expression.", Name); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } - return ExtractExpr::alloc(Child.get(), Offset, ResTy); + return Builder->Extract(Child.get(), Offset, ResTy); } ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name, @@ -1215,7 +1221,7 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name, ExpectRParen("unexpected argument in read expression."); if (!Array.isValid()) - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); // FIXME: Need generic way to get array width. Needs to work with // anonymous arrays. @@ -1230,10 +1236,10 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name, IndexExpr = Index.getExpr(); if (!IndexExpr.isValid()) - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); else if (IndexExpr.get()->getWidth() != ArrayDomainType) { Error("index width does not match array domain."); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } // FIXME: Check range width. @@ -1241,29 +1247,30 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name, switch (Kind) { default: assert(0 && "Invalid kind."); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); case eMacroKind_ReadLSB: case eMacroKind_ReadMSB: { unsigned NumReads = ResTy / ArrayRangeType; if (ResTy != NumReads*ArrayRangeType) { Error("invalid ordered read (not multiple of range type).", Name); - return ConstantExpr::alloc(0, ResTy); + return Builder->Constant(0, ResTy); } std::vector<ExprHandle> Kids; Kids.reserve(NumReads); ExprHandle Index = IndexExpr.get(); for (unsigned i=0; i<NumReads; ++i) { // FIXME: using folding here - ExprHandle OffsetIndex = AddExpr::create(IndexExpr.get(), - ConstantExpr::alloc(i, ArrayDomainType)); - Kids.push_back(ReadExpr::alloc(Array.get(), OffsetIndex)); + ExprHandle OffsetIndex = Builder->Add(IndexExpr.get(), + Builder->Constant(i, ArrayDomainType)); + Kids.push_back(Builder->Read(Array.get(), OffsetIndex)); } if (Kind == eMacroKind_ReadLSB) std::reverse(Kids.begin(), Kids.end()); + // FIXME: Use builder! return ConcatExpr::createN(NumReads, &Kids[0]); } case Expr::Read: - return ReadExpr::alloc(Array.get(), IndexExpr.get()); + return Builder->Read(Array.get(), IndexExpr.get()); } } @@ -1448,7 +1455,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) { // Diagnose 0[box] with no trailing digits. if (!N) { Error("invalid numeric token (no digits).", Tok); - return ConstantExpr::alloc(0, Type); + return Builder->Constant(0, Type); } } @@ -1470,12 +1477,12 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) { Digit = Char - 'A' + 10; else { Error("invalid character in numeric token.", Tok); - return ConstantExpr::alloc(0, Type); + return Builder->Constant(0, Type); } if (Digit >= Radix) { Error("invalid character in numeric token (out of range).", Tok); - return ConstantExpr::alloc(0, Type); + return Builder->Constant(0, Type); } DigitVal = Digit; @@ -1489,7 +1496,7 @@ ExprResult ParserImpl::ParseNumberToken(Expr::Width Type, const Token &Tok) { if (Type < Val.getBitWidth()) Val = Val.trunc(Type); - return ExprResult(ConstantExpr::alloc(Val.getZExtValue(), Type)); + return ExprResult(Builder->Constant(Val.getZExtValue(), Type)); } /// ParseTypeSpecifier - Parse a type specifier. @@ -1597,8 +1604,9 @@ Parser::~Parser() { } Parser *Parser::Create(const std::string Filename, - const MemoryBuffer *MB) { - ParserImpl *P = new ParserImpl(Filename, MB); + const MemoryBuffer *MB, + ExprBuilder *Builder) { + ParserImpl *P = new ParserImpl(Filename, MB, Builder); P->Initialize(); return P; } diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index fca83905..8762d332 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -3,11 +3,13 @@ #include "klee/Constraints.h" #include "klee/Expr.h" +#include "klee/ExprBuilder.h" #include "klee/Solver.h" #include "klee/Statistics.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" +#include "llvm/ADT/OwningPtr.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/ManagedStatic.h" @@ -41,6 +43,25 @@ namespace { clEnumValN(Evaluate, "evaluate", "Print parsed AST nodes from the input file."), clEnumValEnd)); + + enum BuilderKinds { + DefaultBuilder, + ConstantFoldingBuilder, + FoldingBuilder + }; + + static llvm::cl::opt<BuilderKinds> + BuilderKind("builder", + llvm::cl::desc("Expression builder:"), + llvm::cl::init(DefaultBuilder), + llvm::cl::values( + clEnumValN(DefaultBuilder, "default", + "Default expression construction."), + clEnumValN(ConstantFoldingBuilder, "constant-folding", + "Fold constant expressions."), + clEnumValN(FoldingBuilder, "folding", + "Fold constants and simplify expressions."), + clEnumValEnd)); } static std::string escapedString(const char *start, unsigned length) { @@ -74,9 +95,10 @@ static void PrintInputTokens(const MemoryBuffer *MB) { } static bool PrintInputAST(const char *Filename, - const MemoryBuffer *MB) { + const MemoryBuffer *MB, + ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB); + Parser *P = Parser::Create(Filename, MB, Builder); P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { if (!P->GetNumErrors()) @@ -101,9 +123,10 @@ static bool PrintInputAST(const char *Filename, } static bool EvaluateInputAST(const char *Filename, - const MemoryBuffer *MB) { + const MemoryBuffer *MB, + ExprBuilder *Builder) { std::vector<Decl*> Decls; - Parser *P = Parser::Create(Filename, MB); + Parser *P = Parser::Create(Filename, MB, Builder); P->SetMaxErrors(20); while (Decl *D = P->ParseTopLevelDecl()) { Decls.push_back(D); @@ -229,21 +252,39 @@ int main(int argc, char **argv) { return 1; } + ExprBuilder *Builder = 0; + switch (BuilderKind) { + case DefaultBuilder: + Builder = createDefaultExprBuilder(); + break; + case ConstantFoldingBuilder: + Builder = createDefaultExprBuilder(); + Builder = createConstantFoldingExprBuilder(Builder); + break; + case FoldingBuilder: + Builder = createDefaultExprBuilder(); + Builder = createConstantFoldingExprBuilder(Builder); + Builder = createFoldingExprBuilder(Builder); + break; + } + switch (ToolAction) { case PrintTokens: PrintInputTokens(MB); break; case PrintAST: - success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB); + success = PrintInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), MB, + Builder); break; case Evaluate: success = EvaluateInputAST(InputFile=="-" ? "<stdin>" : InputFile.c_str(), - MB); + MB, Builder); break; default: llvm::cerr << argv[0] << ": error: Unknown program action!\n"; } + delete Builder; delete MB; llvm::llvm_shutdown(); |