diff options
| -rw-r--r-- | include/expr/Parser.h | 38 | ||||
| -rw-r--r-- | include/klee/util/ExprPPrinter.h | 6 | ||||
| -rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 37 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 121 | ||||
| -rw-r--r-- | lib/Solver/PCLoggingSolver.cpp | 28 | ||||
| -rw-r--r-- | test/Expr/Parser/Exprs.pc | 390 | ||||
| -rw-r--r-- | test/Feature/ExprLogging.c | 7 |
7 files changed, 337 insertions, 290 deletions
diff --git a/include/expr/Parser.h b/include/expr/Parser.h index 08ec66aa..5caf0027 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -70,8 +70,8 @@ namespace expr { /// ArrayDecl - Array declarations. /// /// For example: - /// array obj : 32 -> 8 = symbolic - /// array obj[32] : 32 -> 8 = { ... } + /// array obj[] : w32 -> w8 = symbolic + /// array obj[32] : w32 -> w8 = { ... } class ArrayDecl : public Decl { public: /// Name - The name of this array. @@ -86,20 +86,25 @@ namespace expr { /// Range - The width of array contents. const unsigned Range; - + + /// Root - The root array object defined by this decl. + const Array *Root; + /// Contents - The initial contents of the array. The array is /// symbolic if no contents are specified. The contained /// expressions are guaranteed to be constants. const std::vector<ExprHandle> Contents; public: - template<typename InputIterator> ArrayDecl(const Identifier *_Name, unsigned _Size, unsigned _Domain, unsigned _Range, - InputIterator ContentsBegin=InputIterator(), - InputIterator ContentsEnd=InputIterator()) - : Name(_Name), Size(_Size), Domain(_Domain), Range(_Range), - Contents(ContentsBegin, ContentsEnd) {} + const Array *_Root) + : Decl(ArrayDeclKind), Name(_Name), + Size(_Size), Domain(_Domain), Range(_Range), + Root(_Root) { + } + + virtual void dump(); static bool classof(const Decl *D) { return D->getKind() == Decl::ArrayDeclKind; @@ -182,16 +187,19 @@ namespace expr { /// Objects - Symbolic arrays whose initial contents should be /// given if the query is invalid. - const std::vector<ArrayDecl> Objects; + const std::vector<const Array*> Objects; public: - template<typename InputIterator> - QueryCommand(InputIterator ConstraintsBegin, - InputIterator ConstraintsEnd, - ExprHandle _Query) + QueryCommand(const std::vector<ExprHandle> &_Constraints, + ExprHandle _Query, + const std::vector<ExprHandle> &_Values, + const std::vector<const Array*> &_Objects + ) : CommandDecl(QueryCommandDeclKind), - Constraints(ConstraintsBegin, ConstraintsEnd), - Query(_Query) {} + Constraints(_Constraints), + Query(_Query), + Values(_Values), + Objects(_Objects) {} virtual void dump(); diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h index 63e6611d..50ccd203 100644 --- a/include/klee/util/ExprPPrinter.h +++ b/include/klee/util/ExprPPrinter.h @@ -61,7 +61,11 @@ namespace klee { static void printQuery(std::ostream &os, const ConstraintManager &constraints, - const ref<Expr> &q); + const ref<Expr> &q, + const ref<Expr> *evalExprsBegin = 0, + const ref<Expr> *evalExprsEnd = 0, + const Array * const* evalArraysBegin = 0, + const Array * const* evalArraysEnd = 0); }; } diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index c27e265e..f8c6cabc 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -498,9 +498,14 @@ void ExprPPrinter::printConstraints(std::ostream &os, printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool)); } + void ExprPPrinter::printQuery(std::ostream &os, const ConstraintManager &constraints, - const ref<Expr> &q) { + const ref<Expr> &q, + const ref<Expr> *evalExprsBegin, + const ref<Expr> *evalExprsEnd, + const Array * const *evalArraysBegin, + const Array * const *evalArraysEnd) { PPrinter p(os); for (ConstraintManager::const_iterator it = constraints.begin(), @@ -508,6 +513,9 @@ void ExprPPrinter::printQuery(std::ostream &os, p.scan(*it); p.scan(q); + for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) + p.scan(*it); + PrintContext PC(os); PC << "(query ["; @@ -525,6 +533,33 @@ void ExprPPrinter::printQuery(std::ostream &os, p.printSeparator(PC, constraints.empty(), indent-1); p.print(q, PC); + // Print expressions to obtain values for, if any. + if (evalExprsBegin != evalExprsEnd) { + PC.breakLine(indent - 1); + PC << '['; + for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) { + p.print(*it, PC); + if (it + 1 != evalExprsEnd) + PC.breakLine(indent); + } + PC << ']'; + } + + // Print arrays to obtain values for, if any. + if (evalArraysBegin != evalArraysEnd) { + if (evalExprsBegin == evalExprsEnd) + PC << " []"; + + PC.breakLine(indent - 1); + PC << '['; + for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) { + PC << "arr" << (*it)->id; + if (it + 1 != evalArraysEnd) + PC.breakLine(indent); + } + PC << ']'; + } + PC << ')'; PC.breakLine(); } diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index c20c5d66..9b3a2687 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -396,13 +396,17 @@ DeclResult ParserImpl::ParseCommandDecl() { /// ParseQueryCommand - Parse query command. The lexer should be /// positioned at the 'query' keyword. /// -/// 'query' expressions-list expression [expression-list [array-list]] +/// 'query' expressions-list expression [expressions-list [array-list]] DeclResult ParserImpl::ParseQueryCommand() { + std::vector<ExprHandle> Constraints; + std::vector<ExprHandle> Values; + std::vector<const Array*> Objects; + ExprResult Res; + // FIXME: We need a command for this. Or something. ExprSymTab.clear(); VersionSymTab.clear(); - std::vector<ExprHandle> Constraints; ConsumeExpectedToken(Token::KWQuery); if (Tok.kind != Token::LSquare) { Error("malformed query, expected constraint list."); @@ -415,24 +419,77 @@ DeclResult ParserImpl::ParseQueryCommand() { while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { Error("unexpected end of file."); - return new QueryCommand(Constraints.begin(), Constraints.end(), - ConstantExpr::alloc(false, Expr::Bool)); + Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool)); + goto exit; } - ExprResult Res = ParseExpr(TypeResult(Expr::Bool)); - if (Res.isValid()) - Constraints.push_back(Res.get()); + ExprResult Constraint = ParseExpr(TypeResult(Expr::Bool)); + if (Constraint.isValid()) + Constraints.push_back(Constraint.get()); } - ConsumeRSquare(); - ExprResult Res = ParseExpr(TypeResult()); + Res = ParseExpr(TypeResult(Expr::Bool)); if (!Res.isValid()) // Error emitted by ParseExpr. Res = ExprResult(ConstantExpr::alloc(0, Expr::Bool)); - ExpectRParen("unexpected argument to 'query'."); - return new QueryCommand(Constraints.begin(), Constraints.end(), - Res.get()); + // Return if there are no optional lists of things to evaluate. + if (Tok.kind == Token::RParen) + goto exit; + + ConsumeExpectedToken(Token::LSquare); + // FIXME: Should avoid reading past unbalanced parens here. + while (Tok.kind != Token::RSquare) { + if (Tok.kind == Token::EndOfFile) { + Error("unexpected end of file."); + goto exit; + } + + ExprResult Res = ParseExpr(TypeResult()); + if (Res.isValid()) + Values.push_back(Res.get()); + } + ConsumeRSquare(); + + // Return if there are no optional lists of things to evaluate. + if (Tok.kind == Token::RParen) + goto exit; + + ConsumeExpectedToken(Token::LSquare); + // FIXME: Should avoid reading past unbalanced parens here. + while (Tok.kind != Token::RSquare) { + if (Tok.kind == Token::EndOfFile) { + Error("unexpected end of file."); + goto exit; + } + + // FIXME: Factor out. + if (Tok.kind != Token::Identifier) { + Error("unexpected token."); + ConsumeToken(); + continue; + } + + Token LTok = Tok; + const Identifier *Label = GetOrCreateIdentifier(Tok); + ConsumeToken(); + + // Declare or create array. + const ArrayDecl *AD = ArraySymTab[Label]; + if (!AD) { + // FIXME: Don't make up arrays. + unsigned Id = atoi(&Label->Name.c_str()[3]); + AD = new ArrayDecl(Label, 0, 32, 8, new Array(0, Id, 0)); + } + + Objects.push_back(AD->Root); + } + ConsumeRSquare(); + + exit: + if (Tok.kind != Token::EndOfFile) + ExpectRParen("unexpected argument to 'query'."); + return new QueryCommand(Constraints, Res.get(), Values, Objects); } /// ParseNumberOrExpr - Parse an expression whose type cannot be @@ -1035,12 +1092,13 @@ VersionResult ParserImpl::ParseVersionSpecifier() { // Declare or create array. const ArrayDecl *&A = ArraySymTab[Label]; if (!A) { - // Array = new ArrayDecl(Label, 0, 32, 8); unsigned id = atoi(&Label->Name.c_str()[3]); Array *root = new Array(0, id, 0); + ArrayDecl *AD = new ArrayDecl(Label, 0, 32, 8, root); // Create update list mapping of name -> array. VersionSymTab.insert(std::make_pair(Label, UpdateList(root, true, NULL))); + ArraySymTab.insert(std::make_pair(Label, AD)); } } @@ -1312,12 +1370,39 @@ void ParserImpl::Error(const char *Message, const Token &At) { Decl::Decl(DeclKind _Kind) : Kind(_Kind) {} +void ArrayDecl::dump() { + std::cout << "array " << Name->Name << " : " + << 'w' << Domain << " -> " + << 'w' << Range << " = "; + + if (Contents.empty()) { + std::cout << "symbolic\n"; + } else { + std::cout << '{'; + for (std::vector<ExprHandle>::const_iterator it = Contents.begin(), + ie = Contents.end(); it != ie;) { + std::cout << *it; + if (++it != ie) + std::cout << " "; + } + std::cout << "}\n"; + } +} + void QueryCommand::dump() { - // FIXME: This is masking the difference between an actual query and - // a query decl. - ExprPPrinter::printQuery(std::cout, - ConstraintManager(Constraints), - Query); + const ExprHandle *ValuesBegin = 0, *ValuesEnd = 0; + const Array * const* ObjectsBegin = 0, * const* ObjectsEnd = 0; + if (!Values.empty()) { + ValuesBegin = &Values[0]; + ValuesEnd = ValuesBegin + Values.size(); + } + if (!Objects.empty()) { + ObjectsBegin = &Objects[0]; + ObjectsEnd = ObjectsBegin + Objects.size(); + } + ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), + Query, ValuesBegin, ValuesEnd, + ObjectsBegin, ObjectsEnd); } // Public parser API diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp index 4b787acb..81cf7688 100644 --- a/lib/Solver/PCLoggingSolver.cpp +++ b/lib/Solver/PCLoggingSolver.cpp @@ -35,13 +35,19 @@ class PCLoggingSolver : public SolverImpl { unsigned queryCount; double startTime; - void startQuery(const Query& query, const char *typeName) { + void startQuery(const Query& query, const char *typeName, + const ref<Expr> *evalExprsBegin = 0, + const ref<Expr> *evalExprsEnd = 0, + const Array * const* evalArraysBegin = 0, + const Array * const* evalArraysEnd = 0) { Statistic *S = theStatisticManager->getStatisticByName("Instructions"); uint64_t instructions = S ? S->getValue() : 0; os << "# Query " << queryCount++ << " -- " << "Type: " << typeName << ", " << "Instructions: " << instructions << "\n"; - printer->printQuery(os, query.constraints, query.expr); + printer->printQuery(os, query.constraints, query.expr, + evalExprsBegin, evalExprsEnd, + evalArraysBegin, evalArraysEnd); startTime = getWallTime(); } @@ -85,7 +91,8 @@ public: } bool computeValue(const Query& query, ref<Expr> &result) { - startQuery(query, "Value"); + startQuery(query.withFalse(), "Value", + &query.expr, &query.expr + 1); bool success = solver->impl->computeValue(query, result); finishQuery(success); if (success) @@ -98,8 +105,19 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution) { - // FIXME: Add objects to output. - startQuery(query, "InitialValues"); + const ref<Expr> *evalExprBegin = 0, *evalExprEnd = 0; + if (!query.expr->isFalse()) { + evalExprBegin = &query.expr; + evalExprEnd = evalExprBegin + 1; + } + if (objects.empty()) { + startQuery(query.withFalse(), "InitialValues", + evalExprBegin, evalExprEnd); + } else { + startQuery(query.withFalse(), "InitialValues", + evalExprBegin, evalExprEnd, + &objects[0], &objects[0] + objects.size()); + } bool success = solver->impl->computeInitialValues(query, objects, values, hasSolution); finishQuery(success); diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc index 3d37bf9b..9357e0c1 100644 --- a/test/Expr/Parser/Exprs.pc +++ b/test/Expr/Parser/Exprs.pc @@ -1,390 +1,288 @@ +# Taken from Features/ExprLogging.c + # FIXME: Make this test actual check for something (other than # crashing/errors). # RUN: %kleaver -print-ast %s -# Query 0 -- Type: Truth, Instructions: 33 -(query [] (Not (Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 0 -- Type: Truth, Instructions: 36 +(query [] (Not (Ult (ReadLSB w32 0 arr119) 16))) -# OK -- Elapsed: 0.000977993 +# OK -- Elapsed: 0.000962901 # Is Valid: false -# Query 1 -- Type: Value, Instructions: 41 -(query [(Ult N0:(Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 1 -- Type: Value, Instructions: 45 +(query [(Ult N0:(ReadLSB w32 0 arr119) 16)] - (Add w32 174331008 (Mul w32 4 N0))) -# OK -- Elapsed: 3.38554e-05 -# Result: 174331008 + false + [(Add w32 168649296 (Mul w32 4 N0))]) +# OK -- Elapsed: 4.09303e-05 +# Result: 168649296 -# Query 2 -- Type: Truth, Instructions: 41 -(query [(Ult N0:(Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 2 -- Type: Truth, Instructions: 45 +(query [(Ult N0:(ReadLSB w32 0 arr119) 16)] (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00113606 +# OK -- Elapsed: 0.00111999 # Is Valid: true -# Query 3 -- Type: Truth, Instructions: 57 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 3 -- Type: Truth, Instructions: 66 +(query [(Ult (ReadLSB w32 0 arr119) 16)] - (Not (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Not (Ult (ReadLSB w32 0 arr126) 16))) -# OK -- Elapsed: 0.000864983 +# OK -- Elapsed: 0.000853909 # Is Valid: false -# Query 4 -- Type: Value, Instructions: 62 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 4 -- Type: Value, Instructions: 72 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult N0:(Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult N0:(ReadLSB w32 0 arr126) 16)] - (Add w32 174331008 (Mul w32 4 N0))) -# OK -- Elapsed: 3.60012e-05 -# Result: 174331008 + false + [(Add w32 168649296 (Mul w32 4 N0))]) +# OK -- Elapsed: 3.89818e-05 +# Result: 168649296 -# Query 5 -- Type: Truth, Instructions: 62 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 5 -- Type: Truth, Instructions: 72 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult N0:(Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult N0:(ReadLSB w32 0 arr126) 16)] (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00109196 +# OK -- Elapsed: 0.00109102 # Is Valid: true -# Query 6 -- Type: Truth, Instructions: 79 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 6 -- Type: Truth, Instructions: 94 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16)] - (Not (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Not (Ult (ReadLSB w32 0 arr133) 16))) -# OK -- Elapsed: 0.00089097 +# OK -- Elapsed: 0.000877942 # Is Valid: false -# Query 7 -- Type: Value, Instructions: 87 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 7 -- Type: Value, Instructions: 103 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult N0:(Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult N0:(ReadLSB w32 0 arr133) 16)] - (Add w32 174331008 (Mul w32 4 N0))) -# OK -- Elapsed: 4.41074e-05 -# Result: 174331008 + false + [(Add w32 168649296 (Mul w32 4 N0))]) +# OK -- Elapsed: 4.81055e-05 +# Result: 168649296 -# Query 8 -- Type: Truth, Instructions: 87 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 8 -- Type: Truth, Instructions: 103 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult N0:(Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult N0:(ReadLSB w32 0 arr133) 16)] (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00111794 +# OK -- Elapsed: 0.00110997 # Is Valid: true -# Query 9 -- Type: Truth, Instructions: 103 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 9 -- Type: Truth, Instructions: 124 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult (ReadLSB w32 0 arr133) 16)] (And (Not (Eq 3 - N0:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N0:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0)))))) -# OK -- Elapsed: 0.00117898 +# OK -- Elapsed: 0.00117305 # Is Valid: false -# Query 10 -- Type: Value, Instructions: 108 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 10 -- Type: Value, Instructions: 130 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult (ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N0:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N0:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0))))))] - (Add w32 174291904 N0)) -# OK -- Elapsed: 5.91278e-05 -# Result: 174291907 + false + [(Add w32 168742656 N0)]) +# OK -- Elapsed: 6.11061e-05 +# Result: 168742659 -# Query 11 -- Type: Truth, Instructions: 108 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 11 -- Type: Truth, Instructions: 130 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult (ReadLSB w32 0 arr133) 16) (Not (And (Not N0:(Eq 3 - N1:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N1:(ReadLSB w32 0 arr140))) (And (Not N2:(Eq 2 N1)) (And (Not N3:(Eq 1 N1)) (Not N4:(Eq 0 N1))))))] (Or N0 (Or N2 (Or N3 N4)))) -# OK -- Elapsed: 0.00145888 +# OK -- Elapsed: 0.00146289 # Is Valid: true -# Query 12 -- Type: Truth, Instructions: 114 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 12 -- Type: Truth, Instructions: 136 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult (ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N0:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N0:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0))))))] (Not (Eq 104 (Read w8 0 [N0=0, - 1=97] @ arr60)))) -# OK -- Elapsed: 0.00247502 + 1=97] @ arr115)))) +# OK -- Elapsed: 0.00246791 # Is Valid: false -# Query 13 -- Type: Truth, Instructions: 124 -(query [(Ult (Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 13 -- Type: Truth, Instructions: 146 +(query [(Ult (ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult (Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult (ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N0:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N0:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0)))))) (Eq 104 (Read w8 0 U0:[N0=0, - 1=97] @ arr60))] + 1=97] @ arr115))] (Not (Slt 2 (Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104))))))) -# OK -- Elapsed: 0.000127077 +# OK -- Elapsed: 0.000145945 # Is Valid: false -# Query 14 -- Type: Truth, Instructions: 130 -(query [(Ult N0:(Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 14 -- Type: Truth, Instructions: 152 +(query [(Ult N0:(ReadLSB w32 0 arr119) 16) - (Ult (Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult (ReadLSB w32 0 arr126) 16) - (Ult N1:(Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult N1:(ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N2:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N2:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N2)) (And (Not (Eq 1 N2)) (Not (Eq 0 N2)))))) (Eq 104 (Read w8 0 U0:[N2=0, - 1=97] @ arr60)) + 1=97] @ arr115)) (Slt 2 N3:(Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104)))))] - (Not (Eq (Concat w32 (Read w8 51 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr60))), - (Add w32 1 N4)=(Extract w8 8 N5), - (Add w32 2 N4)=(Extract w8 16 N5), - (Add w32 3 N4)=(Extract w8 24 N5), - N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr60))), - (Add w32 1 N6)=(Extract w8 8 N7), - (Add w32 2 N6)=(Extract w8 16 N7), - (Add w32 3 N6)=(Extract w8 24 N7), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) - (Concat w24 (Read w8 50 U1) - (ReadLSB w16 48 U1))) + (Not (Eq (ReadLSB w32 48 U1:[N4:(Mul w32 4 N1)=(Extract w8 0 N5:(SExt w32 (Read w8 3 arr115))), + (Add w32 1 N4)=(Extract w8 8 N5), + (Add w32 2 N4)=(Extract w8 16 N5), + (Add w32 3 N4)=(Extract w8 24 N5), + N6:(Mul w32 4 N0)=(Extract w8 0 N7:(SExt w32 (Read w8 0 arr115))), + (Add w32 1 N6)=(Extract w8 8 N7), + (Add w32 2 N6)=(Extract w8 16 N7), + (Add w32 3 N6)=(Extract w8 24 N7), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) N3))) -# OK -- Elapsed: 0.0158381 +# OK -- Elapsed: 0.016117 # Is Valid: false -# Query 15 -- Type: Truth, Instructions: 135 -(query [(Ult N0:(Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 15 -- Type: Truth, Instructions: 157 +(query [(Ult N0:(ReadLSB w32 0 arr119) 16) - (Ult N1:(Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult N1:(ReadLSB w32 0 arr126) 16) - (Ult N2:(Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult N2:(ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N3:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N3:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N3)) (And (Not (Eq 1 N3)) (Not (Eq 0 N3)))))) (Eq 104 (Read w8 0 U0:[N3=0, - 1=97] @ arr60)) + 1=97] @ arr115)) (Slt 2 N4:(Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104))))) - (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))), - (Add w32 1 N5)=(Extract w8 8 N6), - (Add w32 2 N5)=(Extract w8 16 N6), - (Add w32 3 N5)=(Extract w8 24 N6)] @ - U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr60))), - (Add w32 1 N7)=(Extract w8 8 N8), - (Add w32 2 N7)=(Extract w8 16 N8), - (Add w32 3 N7)=(Extract w8 24 N8), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) - (Concat w24 (Read w8 50 U1) - (ReadLSB w16 48 U1))) + (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr115))), + (Add w32 1 N5)=(Extract w8 8 N6), + (Add w32 2 N5)=(Extract w8 16 N6), + (Add w32 3 N5)=(Extract w8 24 N6)] @ + U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr115))), + (Add w32 1 N7)=(Extract w8 8 N8), + (Add w32 2 N7)=(Extract w8 16 N8), + (Add w32 3 N7)=(Extract w8 24 N8), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) N4)] (Eq 32 - (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1)) - U2) - (Concat w24 (Read w8 (Add w32 2 N9) - U2) - (ReadLSB w16 N9 U2))))) -# OK -- Elapsed: 0.000321865 + (ReadLSB w32 N9:(Mul w32 4 N1) U2))) +# OK -- Elapsed: 0.00037605 # Is Valid: false -# Query 16 -- Type: InitialValues, Instructions: 137 -(query [(Ult N0:(Concat w32 (Read w8 3 arr65) - (Concat w24 (Read w8 2 arr65) - (ReadLSB w16 0 arr65))) +# Query 16 -- Type: InitialValues, Instructions: 159 +(query [(Ult N0:(ReadLSB w32 0 arr119) 16) - (Ult N1:(Concat w32 (Read w8 3 arr72) - (Concat w24 (Read w8 2 arr72) - (ReadLSB w16 0 arr72))) + (Ult N1:(ReadLSB w32 0 arr126) 16) - (Ult N2:(Concat w32 (Read w8 3 arr79) - (Concat w24 (Read w8 2 arr79) - (ReadLSB w16 0 arr79))) + (Ult N2:(ReadLSB w32 0 arr133) 16) (Not (And (Not (Eq 3 - N3:(Concat w32 (Read w8 3 arr86) - (Concat w24 (Read w8 2 arr86) - (ReadLSB w16 0 arr86))))) + N3:(ReadLSB w32 0 arr140))) (And (Not (Eq 2 N3)) (And (Not (Eq 1 N3)) (Not (Eq 0 N3)))))) (Eq 104 (Read w8 0 U0:[N3=0, - 1=97] @ arr60)) + 1=97] @ arr115)) (Slt 2 N4:(Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104))))) - (Eq (Concat w32 (Read w8 51 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr60))), - (Add w32 1 N5)=(Extract w8 8 N6), - (Add w32 2 N5)=(Extract w8 16 N6), - (Add w32 3 N5)=(Extract w8 24 N6)] @ - U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr60))), - (Add w32 1 N7)=(Extract w8 8 N8), - (Add w32 2 N7)=(Extract w8 16 N8), - (Add w32 3 N7)=(Extract w8 24 N8), - 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) - (Concat w24 (Read w8 50 U1) - (ReadLSB w16 48 U1))) + (Eq (ReadLSB w32 48 U1:[N5:(Mul w32 4 N2)=(Extract w8 0 N6:(SExt w32 (Read w8 3 arr115))), + (Add w32 1 N5)=(Extract w8 8 N6), + (Add w32 2 N5)=(Extract w8 16 N6), + (Add w32 3 N5)=(Extract w8 24 N6)] @ + U2:[N7:(Mul w32 4 N0)=(Extract w8 0 N8:(SExt w32 (Read w8 0 arr115))), + (Add w32 1 N7)=(Extract w8 8 N8), + (Add w32 2 N7)=(Extract w8 16 N8), + (Add w32 3 N7)=(Extract w8 24 N8), + 63=0, 62=0, 61=128, 60=0, 59=0, 58=0, 57=64, 56=0, 55=0, 54=0, 53=32, 52=0, 51=0, 50=0, 49=16, 48=0, 47=0, 46=0, 45=8, 44=0, 43=0, 42=0, 41=4, 40=0, 39=0, 38=0, 37=2, 36=0, 35=0, 34=0, 33=1, 32=0, 31=0, 30=0, 29=0, 28=128, 27=0, 26=0, 25=0, 24=64, 23=0, 22=0, 21=0, 20=32, 19=0, 18=0, 17=0, 16=16, 15=0, 14=0, 13=0, 12=8, 11=0, 10=0, 9=0, 8=4, 7=0, 6=0, 5=0, 4=2, 3=0, 2=0, 1=0, 0=1]) N4) (Not (Eq 32 - (Concat w32 (Read w8 (Add w32 3 N9:(Mul w32 4 N1)) - U2) - (Concat w24 (Read w8 (Add w32 2 N9) - U2) - (ReadLSB w16 N9 U2)))))] - false) -# OK -- Elapsed: 0.000178814 + (ReadLSB w32 N9:(Mul w32 4 N1) U2)))] + false [] + [arr115 + arr119 + arr126 + arr133 + arr140]) +# OK -- Elapsed: 0.000240058 # Solvable: true -# arr60 = [104,0,0,0] -# arr65 = [12,0,0,0] -# arr72 = [0,0,0,0] -# arr79 = [0,0,0,0] -# arr86 = [1,0,0,0] +# arr115 = [104,0,0,0] +# arr119 = [12,0,0,0] +# arr126 = [0,0,0,0] +# arr133 = [0,0,0,0] +# arr140 = [1,0,0,0] + diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index 2abf0070..2329279d 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,9 +1,8 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc // RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log -// RUN: %kleaver -print-ast klee-last/test000001.pc - -// FIXME: Ideally we would verify a roundtrip that we parsed the pc -// file and can dump it back out as the same file. +// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log +// RUN: %kleaver -print-ast %t3.log > %t4.log +// RUN: diff %t3.log %t4.log #include <assert.h> |