aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Expr/ExprPPrinter.cpp37
-rw-r--r--lib/Expr/Parser.cpp121
-rw-r--r--lib/Solver/PCLoggingSolver.cpp28
3 files changed, 162 insertions, 24 deletions
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);
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-24 08:22:31 +0000