diff options
| -rw-r--r-- | include/expr/Lexer.h | 9 | ||||
| -rw-r--r-- | include/expr/Parser.h | 4 | ||||
| -rw-r--r-- | include/klee/util/ExprPPrinter.h | 3 | ||||
| -rw-r--r-- | lib/Core/ExecutorUtil.cpp | 8 | ||||
| -rw-r--r-- | lib/Expr/ExprPPrinter.cpp | 26 | ||||
| -rw-r--r-- | lib/Expr/Lexer.cpp | 9 | ||||
| -rw-r--r-- | lib/Expr/Parser.cpp | 260 | ||||
| -rw-r--r-- | test/Expr/Evaluate.pc | 5 | ||||
| -rw-r--r-- | test/Expr/Lexer/Numbers.pc | 2 | ||||
| -rw-r--r-- | test/Expr/Parser/Concat64.pc | 1 | ||||
| -rw-r--r-- | test/Expr/Parser/Exprs.pc | 106 | ||||
| -rw-r--r-- | test/Expr/Parser/MultiByteReads.pc | 3 | ||||
| -rw-r--r-- | test/Expr/Parser/TypeChecking.pc | 10 | ||||
| -rw-r--r-- | www/KQuery.html | 9 |
14 files changed, 368 insertions, 87 deletions
diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h index 4ae760a0..a8719b4d 100644 --- a/include/expr/Lexer.h +++ b/include/expr/Lexer.h @@ -28,9 +28,11 @@ namespace expr { EndOfFile, /// <end of file> Equals, /// ' = ' Identifier, /// [a-zA-Z_][a-zA-Z0-9._]* + KWArray, /// 'array' KWFalse, /// 'false' KWQuery, /// 'query' KWReserved, /// fp[0-9]+([.].*)?, i[0-9]+ + KWSymbolic, /// 'symbolic' KWTrue, /// 'true' KWWidth, /// w[0-9]+ LBrace, /// '{' @@ -41,7 +43,10 @@ namespace expr { RParen, /// ')' RSquare, /// ']' Semicolon, /// ';' - Unknown /// <other> + Unknown, /// <other> + + KWKindFirst=KWArray, + KWKindLast=KWWidth }; Kind kind; /// The token kind. @@ -60,7 +65,7 @@ namespace expr { /// isKeyword - True if this token is a keyword. bool isKeyword() const { - return kind >= KWFalse && kind <= KWTrue; + return kind >= KWKindFirst && kind <= KWKindLast; } // dump - Dump the token to stderr. diff --git a/include/expr/Parser.h b/include/expr/Parser.h index 5caf0027..65105f12 100644 --- a/include/expr/Parser.h +++ b/include/expr/Parser.h @@ -79,7 +79,7 @@ namespace expr { /// Size - The maximum array size (or 0 if unspecified). Concrete /// arrays always are specified with a size. - const unsigned Size; + const uint64_t Size; /// Domain - The width of indices. const unsigned Domain; @@ -96,7 +96,7 @@ namespace expr { const std::vector<ExprHandle> Contents; public: - ArrayDecl(const Identifier *_Name, unsigned _Size, + ArrayDecl(const Identifier *_Name, uint64_t _Size, unsigned _Domain, unsigned _Range, const Array *_Root) : Decl(ArrayDeclKind), Name(_Name), diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h index 50ccd203..4d1930d8 100644 --- a/include/klee/util/ExprPPrinter.h +++ b/include/klee/util/ExprPPrinter.h @@ -65,7 +65,8 @@ namespace klee { const ref<Expr> *evalExprsBegin = 0, const ref<Expr> *evalExprsEnd = 0, const Array * const* evalArraysBegin = 0, - const Array * const* evalArraysEnd = 0); + const Array * const* evalArraysEnd = 0, + bool printArrayDecls = true); }; } diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 1e346e89..a1e030a5 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -46,7 +46,10 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) { switch (ce->getOpcode()) { default : - assert(0 && "unknown ConstantExpr type"); + ce->dump(); + llvm::cerr << "error: unknown ConstantExpr type\n" + << "opcode: " << ce->getOpcode() << "\n"; + abort(); case Instruction::Trunc: return ExtractExpr::createByteOff(op1, 0, @@ -128,6 +131,9 @@ Executor::evalConstantExpr(llvm::ConstantExpr *ce) { return SelectExpr::create(op1, op2, op3); } + case Instruction::FAdd: + case Instruction::FSub: + case Instruction::FMul: case Instruction::FDiv: case Instruction::FRem: case Instruction::FPTrunc: diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index affde4ad..7bfb6567 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -81,6 +81,9 @@ public: }; class PPrinter : public ExprPPrinter { +public: + std::set<const Array*> usedArrays; +private: std::map<ref<Expr>, unsigned> bindings; std::map<const UpdateNode*, unsigned> updateBindings; std::set< ref<Expr> > couldPrint, shouldPrint; @@ -131,6 +134,7 @@ class PPrinter : public ExprPPrinter { } void scanUpdate(const UpdateNode *un) { + // FIXME: This needs to be non-recursive. if (un) { if (couldPrintUpdates.insert(un).second) { scanUpdate(un->next); @@ -148,8 +152,10 @@ class PPrinter : public ExprPPrinter { Expr *ep = e.get(); for (unsigned i=0; i<ep->getNumKids(); i++) scan1(ep->getKid(i)); - if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) + if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) { + usedArrays.insert(re->updates.root); scanUpdate(re->updates.head); + } } else { shouldPrint.insert(e); } @@ -507,7 +513,8 @@ void ExprPPrinter::printQuery(std::ostream &os, const ref<Expr> *evalExprsBegin, const ref<Expr> *evalExprsEnd, const Array * const *evalArraysBegin, - const Array * const *evalArraysEnd) { + const Array * const *evalArraysEnd, + bool printArrayDecls) { PPrinter p(os); for (ConstraintManager::const_iterator it = constraints.begin(), @@ -519,6 +526,21 @@ void ExprPPrinter::printQuery(std::ostream &os, p.scan(*it); PrintContext PC(os); + + // Print array declarations. + if (printArrayDecls) { + for (std::set<const Array*>::iterator it = p.usedArrays.begin(), + ie = p.usedArrays.end(); it != ie; ++it) { + const Array *A = *it; + // FIXME: Print correct name, domain, and range. + PC << "array " << "arr" << A->id + << "[" << A->size << "]" + << " : " << "w32" << " -> " << "w8" + << " = symbolic"; + PC.breakLine(); + } + } + PC << "(query ["; // Ident at constraint list; diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index 77e25f62..d8809a53 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -34,9 +34,11 @@ const char *Token::getKindName() const { case EndOfFile: return "EndOfFile"; case Equals: return "Equals"; case Identifier: return "Identifier"; + case KWArray: return "KWArray"; case KWFalse: return "KWFalse"; case KWQuery: return "KWQuery"; case KWReserved: return "KWReserved"; + case KWSymbolic: return "KWSymbolic"; case KWTrue: return "KWTrue"; case KWWidth: return "KWWidth"; case LBrace: return "LBrace"; @@ -153,7 +155,7 @@ Token &Lexer::SetIdentifierTokenKind(Token &Result) { case 5: if (memcmp("array", Result.start, 5) == 0) - return SetTokenKind(Result, Token::KWReserved); + return SetTokenKind(Result, Token::KWArray); if (memcmp("false", Result.start, 5) == 0) return SetTokenKind(Result, Token::KWFalse); if (memcmp("query", Result.start, 5) == 0) @@ -169,6 +171,11 @@ Token &Lexer::SetIdentifierTokenKind(Token &Result) { if (memcmp("declare", Result.start, 7) == 0) return SetTokenKind(Result, Token::KWReserved); break; + + case 8: + if (memcmp("symbolic", Result.start, 8) == 0) + return SetTokenKind(Result, Token::KWSymbolic); + break; } if (isReservedKW(Result.start, Length)) diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index dedbaa3a..f6487674 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -36,7 +36,7 @@ namespace { T Value; public: - ParseResult() : IsValid(false) {} + ParseResult() : IsValid(false), Value() {} ParseResult(T _Value) : IsValid(true), Value(_Value) {} ParseResult(bool _IsValid, T _Value) : IsValid(_IsValid), Value(_Value) {} @@ -71,6 +71,7 @@ namespace { typedef ParseResult<Decl*> DeclResult; typedef ParseResult<Expr::Width> TypeResult; typedef ParseResult<VersionHandle> VersionResult; + typedef ParseResult<uint64_t> IntegerResult; /// NumberOrExprResult - Represent a number or expression. This is used to /// wrap an expression production which may be a number, but for @@ -137,37 +138,43 @@ namespace { /// ConsumeToken - Consume the current 'peek token' and lex the next one. void ConsumeToken() { - assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen); + assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen && + Tok.kind != Token::LSquare && Tok.kind != Token::RSquare); GetNextNonCommentToken(); } /// ConsumeExpectedToken - Check that the current token is of the /// expected kind and consume it. void ConsumeExpectedToken(Token::Kind k) { + assert(Tok.kind != Token::LParen && Tok.kind != Token::RParen && + Tok.kind != Token::LSquare && Tok.kind != Token::RSquare); + _ConsumeExpectedToken(k); + } + void _ConsumeExpectedToken(Token::Kind k) { assert(Tok.kind == k && "Unexpected token!"); GetNextNonCommentToken(); } void ConsumeLParen() { ++ParenLevel; - ConsumeExpectedToken(Token::LParen); + _ConsumeExpectedToken(Token::LParen); } void ConsumeRParen() { if (ParenLevel) // Cannot go below zero. --ParenLevel; - ConsumeExpectedToken(Token::RParen); + _ConsumeExpectedToken(Token::RParen); } void ConsumeLSquare() { ++SquareLevel; - ConsumeExpectedToken(Token::LSquare); + _ConsumeExpectedToken(Token::LSquare); } void ConsumeRSquare() { if (SquareLevel) // Cannot go below zero. --SquareLevel; - ConsumeExpectedToken(Token::RSquare); + _ConsumeExpectedToken(Token::RSquare); } void ConsumeAnyToken() { @@ -277,6 +284,7 @@ namespace { /* Etc. */ NumberOrExprResult ParseNumberOrExpr(); + IntegerResult ParseIntegerConstant(Expr::Width Type); ExprResult ParseExpr(TypeResult ExpectedType); ExprResult ParseParenExpr(TypeResult ExpectedType); @@ -355,13 +363,23 @@ const Identifier *ParserImpl::GetOrCreateIdentifier(const Token &Tok) { Decl *ParserImpl::ParseTopLevelDecl() { // Repeat until success or EOF. while (Tok.kind != Token::EndOfFile) { - // Only handle commands for now. - if (Tok.kind == Token::LParen) { + switch (Tok.kind) { + case Token::KWArray: { + DeclResult Res = ParseArrayDecl(); + if (Res.isValid()) + return Res.get(); + break; + } + + case Token::LParen: { DeclResult Res = ParseCommandDecl(); if (Res.isValid()) return Res.get(); - } else { - Error("expected '(' token."); + break; + } + + default: + Error("expected 'array' or '(' token."); ConsumeAnyToken(); } } @@ -369,6 +387,153 @@ Decl *ParserImpl::ParseTopLevelDecl() { return 0; } +/// ParseArrayDecl - Parse an array declaration. The lexer should be positioned +/// at the opening 'array'. +/// +/// array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range +/// "=" array-initializer +/// array-initializer = "symbolic" | "{" { numeric-literal } "}" +DeclResult ParserImpl::ParseArrayDecl() { + // FIXME: Recovery here is horrible, we need to scan to next decl start or + // something. + ConsumeExpectedToken(Token::KWArray); + + if (Tok.kind != Token::Identifier) { + Error("expected identifier token."); + return DeclResult(); + } + + Token Name = Tok; + IntegerResult Size; + TypeResult DomainType; + TypeResult RangeType; + std::vector<ExprHandle> Values; + + ConsumeToken(); + + if (Tok.kind != Token::LSquare) { + Error("expected '['."); + goto exit; + } + ConsumeLSquare(); + + if (Tok.kind != Token::RSquare) { + Size = ParseIntegerConstant(64); + } + if (Tok.kind != Token::RSquare) { + Error("expected ']'."); + goto exit; + } + ConsumeRSquare(); + + if (Tok.kind != Token::Colon) { + Error("expected ':'."); + goto exit; + } + ConsumeExpectedToken(Token::Colon); + + DomainType = ParseTypeSpecifier(); + if (Tok.kind != Token::Arrow) { + Error("expected '->'."); + goto exit; + } + ConsumeExpectedToken(Token::Arrow); + + RangeType = ParseTypeSpecifier(); + if (Tok.kind != Token::Equals) { + Error("expected '='."); + goto exit; + } + ConsumeExpectedToken(Token::Equals); + + if (Tok.kind == Token::KWSymbolic) { + ConsumeExpectedToken(Token::KWSymbolic); + } else if (Tok.kind == Token::LSquare) { + ConsumeLSquare(); + while (Tok.kind != Token::RSquare) { + if (Tok.kind == Token::EndOfFile) { + Error("unexpected end of file."); + goto exit; + } + + ExprResult Res = ParseNumber(RangeType.get()); + if (Res.isValid()) + Values.push_back(Res.get()); + } + ConsumeRSquare(); + } else { + Error("expected 'symbolic' or '['."); + goto exit; + } + + // Type check size. + if (!Size.isValid()) { + if (Values.empty()) { + Error("unsized arrays are not yet supported."); + Size = 1; + } else { + Size = Values.size(); + } + } + + if (!Values.empty()) { + if (Size.get() != Values.size()) { + // FIXME: Lame message. + Error("constant arrays must be completely specified."); + Values.clear(); + } + + for (unsigned i = 0; i != Size.get(); ++i) { + // FIXME: Must be constant expression. + } + } + + // FIXME: Validate that size makes sense for domain type. + + if (DomainType.get() != Expr::Int32) { + Error("array domain must currently be w32."); + DomainType = Expr::Int32; + Values.clear(); + } + + if (RangeType.get() != Expr::Int8) { + Error("array domain must currently be w8."); + RangeType = Expr::Int8; + Values.clear(); + } + + if (!Values.empty()) { + Error("constant arrays are not yet supported."); + Values.clear(); + } + + // FIXME: Validate that this array is undeclared. + + exit: + if (!Size.isValid()) + Size = 1; + if (!DomainType.isValid()) + DomainType = 32; + if (!RangeType.isValid()) + RangeType = 8; + + // FIXME: Array should take name, not id. + // FIXME: Array should take domain and range. + const Identifier *Label = GetOrCreateIdentifier(Name); + static int counter = 0; + Array *Root = new Array(0, ++counter, Size.get()); + ArrayDecl *AD = new ArrayDecl(Label, Size.get(), + DomainType.get(), RangeType.get(), Root); + + ArraySymTab.insert(std::make_pair(Label, AD)); + + // Create the initial version reference. + VersionSymTab.insert(std::make_pair(Label, + UpdateList(Root, true, NULL))); + + return AD; +} + /// ParseCommandDecl - Parse a command declaration. The lexer should /// be positioned at the opening '('. /// @@ -407,6 +572,16 @@ DeclResult ParserImpl::ParseQueryCommand() { ExprSymTab.clear(); VersionSymTab.clear(); + // Reinsert initial array versions. + // FIXME: Remove this! + for (std::map<const Identifier*, const ArrayDecl*>::iterator + it = ArraySymTab.begin(), ie = ArraySymTab.end(); it != ie; ++it) { + VersionSymTab.insert(std::make_pair(it->second->Name, + UpdateList(it->second->Root, + true, NULL))); + } + + ConsumeExpectedToken(Token::KWQuery); if (Tok.kind != Token::LSquare) { Error("malformed query, expected constraint list."); @@ -414,7 +589,7 @@ DeclResult ParserImpl::ParseQueryCommand() { return DeclResult(); } - ConsumeExpectedToken(Token::LSquare); + ConsumeLSquare(); // FIXME: Should avoid reading past unbalanced parens here. while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { @@ -437,7 +612,7 @@ DeclResult ParserImpl::ParseQueryCommand() { if (Tok.kind == Token::RParen) goto exit; - ConsumeExpectedToken(Token::LSquare); + ConsumeLSquare(); // FIXME: Should avoid reading past unbalanced parens here. while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { @@ -455,7 +630,7 @@ DeclResult ParserImpl::ParseQueryCommand() { if (Tok.kind == Token::RParen) goto exit; - ConsumeExpectedToken(Token::LSquare); + ConsumeLSquare(); // FIXME: Should avoid reading past unbalanced parens here. while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { @@ -474,15 +649,15 @@ DeclResult ParserImpl::ParseQueryCommand() { 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)); + // Lookup array. + std::map<const Identifier*, const ArrayDecl*>::iterator + it = ArraySymTab.find(Label); + + if (it == ArraySymTab.end()) { + Error("unknown array", LTok); + } else { + Objects.push_back(it->second->Root); } - - Objects.push_back(AD->Root); } ConsumeRSquare(); @@ -995,10 +1170,18 @@ ExprResult ParserImpl::ParseConcatParenExpr(const Token &Name, return ConcatExpr::createN(Kids.size(), &Kids[0]); } +IntegerResult ParserImpl::ParseIntegerConstant(Expr::Width Type) { + ExprResult Res = ParseNumber(Type); + + if (!Res.isValid()) + return IntegerResult(); + + return cast<ConstantExpr>(Res.get())->getConstantValue(); +} + ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name, Expr::Width ResTy) { - // FIXME: Pull out parse constant integer expression. - ExprResult OffsetExpr = ParseNumber(Expr::Int32); + IntegerResult OffsetExpr = ParseIntegerConstant(Expr::Int32); ExprResult Child = ParseExpr(TypeResult()); ExpectRParen("unexpected argument to expression."); @@ -1006,9 +1189,7 @@ ExprResult ParserImpl::ParseExtractParenExpr(const Token &Name, if (!OffsetExpr.isValid() || !Child.isValid()) return ConstantExpr::alloc(0, ResTy); - unsigned Offset = - (unsigned) cast<ConstantExpr>(OffsetExpr.get())->getConstantValue(); - + 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); @@ -1086,26 +1267,11 @@ VersionResult ParserImpl::ParseVersionSpecifier() { Label = GetOrCreateIdentifier(Tok); ConsumeToken(); - // FIXME: hack: add array declarations and ditch this. - if (memcmp(Label->Name.c_str(), "arr", 3) == 0) { - // Declare or create array. - const ArrayDecl *&A = ArraySymTab[Label]; - if (!A) { - 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)); - } - } - if (Tok.kind != Token::Colon) { VersionSymTabTy::iterator it = VersionSymTab.find(Label); if (it == VersionSymTab.end()) { - Error("invalid update list label reference.", LTok); + Error("invalid version reference.", LTok); return VersionResult(false, UpdateList(0, true, NULL)); } @@ -1381,9 +1547,10 @@ 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 << " = "; + // FIXME: For now, print using the Array* "name". + std::cout << "array " << "arr" << Root->id + << "[" << Size << "]" + << " : " << 'w' << Domain << " -> " << 'w' << Range << " = "; if (Contents.empty()) { std::cout << "symbolic\n"; @@ -1412,7 +1579,8 @@ void QueryCommand::dump() { } ExprPPrinter::printQuery(std::cout, ConstraintManager(Constraints), Query, ValuesBegin, ValuesEnd, - ObjectsBegin, ObjectsEnd); + ObjectsBegin, ObjectsEnd, + false); } // Public parser API diff --git a/test/Expr/Evaluate.pc b/test/Expr/Evaluate.pc index 354b0489..0dac0cc8 100644 --- a/test/Expr/Evaluate.pc +++ b/test/Expr/Evaluate.pc @@ -1,8 +1,11 @@ # RUN: %kleaver -evaluate %s > %t.log +array arr0[4] : w32 -> w8 = symbolic +array arr1[8] : w32 -> w8 = symbolic + # RUN: grep "Query 0: INVALID" %t.log # Query 0 -(query [] (Not (Ult (ReadLSB w32 0 arr65) +(query [] (Not (Ult (ReadLSB w32 0 arr0) 16))) # RUN: grep "Query 1: VALID" %t.log diff --git a/test/Expr/Lexer/Numbers.pc b/test/Expr/Lexer/Numbers.pc index 6af40133..6b8e2e37 100644 --- a/test/Expr/Lexer/Numbers.pc +++ b/test/Expr/Lexer/Numbers.pc @@ -17,7 +17,7 @@ # RUN: grep "(Token .LBrace. .{. 1 56 0)" %t1 # RUN: grep "(Token .RBrace. .}. 1 56 2)" %t1 # RUN: grep "(Token .Identifier. ._hello_world. 12 58 0)" %t1 -# RUN: grep "(Token .KWReserved. .array. 5 62 0)" %t1 +# RUN: grep "(Token .KWArray. .array. 5 62 0)" %t1 # RUN: grep "(Token .KWReserved. .declare. 7 63 0)" %t1 # RUN: grep "(Token .KWReserved. .def. 3 64 0)" %t1 # RUN: grep "(Token .KWReserved. .define. 6 65 0)" %t1 diff --git a/test/Expr/Parser/Concat64.pc b/test/Expr/Parser/Concat64.pc index e57e9760..0b1479d4 100644 --- a/test/Expr/Parser/Concat64.pc +++ b/test/Expr/Parser/Concat64.pc @@ -1,5 +1,6 @@ # RUN: kleaver --print-ast %s +array arr1[8] : w32 -> w8 = symbolic (query [(Eq 0 (Concat w64 (Read w8 7 arr1) (Concat w56 (Read w8 6 arr1) diff --git a/test/Expr/Parser/Exprs.pc b/test/Expr/Parser/Exprs.pc index 742a0185..4a6adf7e 100644 --- a/test/Expr/Parser/Exprs.pc +++ b/test/Expr/Parser/Exprs.pc @@ -6,64 +6,79 @@ # RUN: %kleaver -print-ast %s # Query 0 -- Type: Truth, Instructions: 31 +array arr53[4] : w32 -> w8 = symbolic (query [] (Not (Ult (ReadLSB w32 0 arr53) 16))) -# OK -- Elapsed: 0.00128889 +# OK -- Elapsed: 0.00137401 # Is Valid: false # Query 1 -- Type: Value, Instructions: 39 +array arr53[4] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 arr53) 16)] false - [(Add w32 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000106812 -# Result: 31543472 + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000108004 +# Result: 31543488 # Query 2 -- Type: Truth, Instructions: 39 +array arr53[4] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 arr53) 16)] (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.0014112 +# OK -- Elapsed: 0.00140095 # Is Valid: true # Query 3 -- Type: Truth, Instructions: 55 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16)] (Not (Ult (ReadLSB w32 0 arr60) 16))) -# OK -- Elapsed: 0.00128603 +# OK -- Elapsed: 0.00106597 # Is Valid: false # Query 4 -- Type: Value, Instructions: 60 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult N0:(ReadLSB w32 0 arr60) 16)] false - [(Add w32 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000141144 -# Result: 31543472 + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000138998 +# Result: 31543488 # Query 5 -- Type: Truth, Instructions: 60 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult N0:(ReadLSB w32 0 arr60) 16)] (Ult (Mul w32 4 N0) 61)) -# OK -- Elapsed: 0.00145102 +# OK -- Elapsed: 0.00137782 # Is Valid: true # Query 6 -- Type: Truth, Instructions: 77 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) 16)] (Not (Ult (ReadLSB w32 0 arr67) 16))) -# OK -- Elapsed: 0.00127888 +# OK -- Elapsed: 0.001127 # Is Valid: false # Query 7 -- Type: Value, Instructions: 85 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -71,11 +86,14 @@ (Ult N0:(ReadLSB w32 0 arr67) 16)] false - [(Add w32 31543472 (Mul w32 4 N0))]) -# OK -- Elapsed: 0.000179052 -# Result: 31543472 + [(Add w32 31543488 (Mul w32 4 N0))]) +# OK -- Elapsed: 0.000175953 +# Result: 31543488 # Query 8 -- Type: Truth, Instructions: 85 +array arr53[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -87,6 +105,10 @@ # Is Valid: true # Query 9 -- Type: Truth, Instructions: 101 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -98,10 +120,14 @@ (And (Not (Eq 2 N0)) (And (Not (Eq 1 N0)) (Not (Eq 0 N0)))))) -# OK -- Elapsed: 0.00163794 +# OK -- Elapsed: 0.00157499 # Is Valid: false # Query 10 -- Type: Value, Instructions: 106 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -114,11 +140,15 @@ (And (Not (Eq 1 N0)) (Not (Eq 0 N0))))))] false - [(Add w32 31583216 N0)]) -# OK -- Elapsed: 0.000283003 -# Result: 31583219 + [(Add w32 31583232 N0)]) +# OK -- Elapsed: 0.000259876 +# Result: 31583235 # Query 11 -- Type: Truth, Instructions: 106 +array arr53[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -132,10 +162,15 @@ (Not N4:(Eq 0 N1))))))] (Or N0 (Or N2 (Or N3 N4)))) -# OK -- Elapsed: 0.00217485 +# OK -- Elapsed: 0.00194788 # Is Valid: true # Query 12 -- Type: Truth, Instructions: 112 +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -150,10 +185,15 @@ (Not (Eq 104 (Read w8 0 [N0=0, 1=97] @ arr49)))) -# OK -- Elapsed: 0.00330305 +# OK -- Elapsed: 0.0030148 # Is Valid: false # Query 13 -- Type: Truth, Instructions: 122 +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult (ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -172,10 +212,16 @@ (Concat w32 (Read w8 3 U0) (Concat w24 (Read w8 2 U0) (Concat w16 (Read w8 1 U0) (w8 104))))))) -# OK -- Elapsed: 0.00039506 +# OK -- Elapsed: 0.000394106 # Is Valid: false # Query 14 -- Type: Truth, Instructions: 128 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 arr53) 16) (Ult (ReadLSB w32 0 arr60) @@ -204,10 +250,16 @@ (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] @ arr5) N3))) -# OK -- Elapsed: 0.018568 +# OK -- Elapsed: 0.0180621 # Is Valid: false # Query 15 -- Type: Truth, Instructions: 133 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 arr53) 16) (Ult N1:(ReadLSB w32 0 arr60) @@ -238,10 +290,16 @@ N4)] (Eq 32 (ReadLSB w32 N9:(Mul w32 4 N1) U2))) -# OK -- Elapsed: 0.00105405 +# OK -- Elapsed: 0.00104594 # Is Valid: false # Query 16 -- Type: InitialValues, Instructions: 135 +array arr5[64] : w32 -> w8 = symbolic +array arr53[4] : w32 -> w8 = symbolic +array arr49[4] : w32 -> w8 = symbolic +array arr74[4] : w32 -> w8 = symbolic +array arr60[4] : w32 -> w8 = symbolic +array arr67[4] : w32 -> w8 = symbolic (query [(Ult N0:(ReadLSB w32 0 arr53) 16) (Ult N1:(ReadLSB w32 0 arr60) @@ -278,7 +336,7 @@ arr60 arr67 arr74]) -# OK -- Elapsed: 0.00058198 +# OK -- Elapsed: 0.000574112 # Solvable: true # arr49 = [104,0,0,0] # arr53 = [12,0,0,0] diff --git a/test/Expr/Parser/MultiByteReads.pc b/test/Expr/Parser/MultiByteReads.pc index af94b516..ea2e7a5d 100644 --- a/test/Expr/Parser/MultiByteReads.pc +++ b/test/Expr/Parser/MultiByteReads.pc @@ -2,6 +2,9 @@ # RUN: grep -q "(ReadLSB w32 4 arr1)" log # RUN: grep -q "(ReadMSB w32 2 arr2)" log +array arr1[8] : w32 -> w8 = symbolic +array arr2[8] : w32 -> w8 = symbolic + (query [(Not (Slt 100 (Concat w32 (Read w8 7 arr1) (Concat w24 (Read w8 6 arr1) diff --git a/test/Expr/Parser/TypeChecking.pc b/test/Expr/Parser/TypeChecking.pc index 9e29d0db..66991c20 100644 --- a/test/Expr/Parser/TypeChecking.pc +++ b/test/Expr/Parser/TypeChecking.pc @@ -2,13 +2,15 @@ -# RUN: grep "TypeChecking.pc:6:9: error: type widths do not match in binary expression" %t.log +# RUN: grep "TypeChecking.pc:7:9: error: type widths do not match in binary expression" %t.log +array arr1[8] : w32 -> w8 = symbolic (query [(Eq (ReadLSB w32 0 arr1) true)] false) -# RUN: grep "TypeChecking.pc:12:25: error: invalid write index (doesn't match array domain)" %t.log -# RUN: grep "TypeChecking.pc:12:35: error: invalid write value (doesn't match array range)" %t.log +# RUN: grep "TypeChecking.pc:14:25: error: invalid write index (doesn't match array domain)" %t.log +# RUN: grep "TypeChecking.pc:14:35: error: invalid write value (doesn't match array range)" %t.log # FIXME: Add array declarations -(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr0) 0)] false) +array arr2[8] : w32 -> w8 = symbolic +(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false) # RUN: grep "TypeChecking.pc: parse failure: 3 errors." %t.log diff --git a/www/KQuery.html b/www/KQuery.html index db0d2b59..f0aaffae 100644 --- a/www/KQuery.html +++ b/www/KQuery.html @@ -265,13 +265,18 @@ <p><b>Syntax:</b></p> <div class="syntax"> array-declaration = "array" name "[" [ size ] "]" ":" domain "->" range "=" array-initializer<br> - array-initializer = "symbolic" | "{" { numeric-literal } "}"<br> + array-initializer = "symbolic" | "[" { numeric-literal } "]"<br> </div> + <p>Arrays can be initialized to be either symbolic, or to have a given list of + constant values. For constant arrays, the initializer list must exactly match + the size of the array (if the size was unspecified, it will be the number of + constant values).</p> + <p><b>Examples:</b></p> <div class="example"> array foo[10] : w32 -> w8 = symbolic <font color="Red"># A ten element symbolic array</font><br> - array foo[4] : w8 -> w1 = { true, false, false, true } <font color="Red"># A constant array of four booleans</font><br> + array foo[] : w8 -> w1 = [ true, false, false, true ] <font color="Red"># A constant array of four booleans</font><br> </div> <h3><a name="query_commands">Query Commands</a></h3> |