diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-09-15 12:09:23 +0100 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-03-23 21:46:41 +0000 |
commit | 4530447c21353b5596b66a9fbb642409cda56f73 (patch) | |
tree | 094a516168e39166898887984cdb2cbed6762965 | |
parent | a40818cab8e1b2315ac40d2c2cb125fc422e8ed7 (diff) | |
download | klee-4530447c21353b5596b66a9fbb642409cda56f73.tar.gz |
Add `AssignmentValidatingSolver`. It's purpose is to check any computed
assignments against the corresponding `Query` object and check the assignment evaluates correctly. This can be switched on using `-debug-assignment-validating-solver` on the command line.
-rw-r--r-- | include/klee/CommandLine.h | 2 | ||||
-rw-r--r-- | include/klee/Solver.h | 6 | ||||
-rw-r--r-- | include/klee/util/Assignment.h | 1 | ||||
-rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 4 | ||||
-rw-r--r-- | lib/Basic/ConstructSolverChain.cpp | 3 | ||||
-rw-r--r-- | lib/Expr/Assigment.cpp | 17 | ||||
-rw-r--r-- | lib/Solver/AssignmentValidatingSolver.cpp | 158 |
7 files changed, 191 insertions, 0 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index cc186db7..6a72692d 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -29,6 +29,8 @@ extern llvm::cl::opt<bool> UseForkedCoreSolver; extern llvm::cl::opt<bool> CoreSolverOptimizeDivides; +extern llvm::cl::opt<bool> UseAssignmentValidatingSolver; + ///The different query logging solvers that can switched on/off enum QueryLoggingSolverType { diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 2f613992..32c8cf9e 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -268,6 +268,12 @@ namespace klee { /// \param oracle - The solver to check query results against. Solver *createValidatingSolver(Solver *s, Solver *oracle); + /// createAssignmentValidatingSolver - Create a solver that when requested + /// for an assignment will check that the computed assignment satisfies + /// the Query. + /// \param s - The underlying solver to use. + Solver *createAssignmentValidatingSolver(Solver *s); + /// createCachingSolver - Create a solver which will cache the queries in /// memory (without eviction). /// diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 5d8aa1ab..55e681de 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -46,6 +46,7 @@ namespace klee { ref<Expr> evaluate(const Array *mo, unsigned index) const; ref<Expr> evaluate(ref<Expr> e); + void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const; template<typename InputIterator> bool satisfies(InputIterator begin, InputIterator end); diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index e55c4550..82cb01b2 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -82,6 +82,10 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions( llvm::cl::CommaSeparated ); +llvm::cl::opt<bool> + UseAssignmentValidatingSolver("debug-assignment-validating-solver", + llvm::cl::init(false)); + #ifdef ENABLE_METASMT #ifdef METASMT_DEFAULT_BACKEND_IS_BTOR diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 68e1b08b..d00fcec1 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -37,6 +37,9 @@ Solver *constructSolverChain(Solver *coreSolver, baseSolverQuerySMT2LogPath.c_str()); } + if (UseAssignmentValidatingSolver) + solver = createAssignmentValidatingSolver(solver); + if (UseFastCexSolver) solver = createFastCexSolver(solver); diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index 635362d4..d788785a 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -22,4 +22,21 @@ void Assignment::dump() { llvm::errs() << "]\n"; } } + +void Assignment::createConstraintsFromAssignment( + std::vector<ref<Expr> > &out) const { + assert(out.size() == 0 && "out should be empty"); + for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end(); + it != ie; ++it) { + const Array *array = it->first; + const std::vector<unsigned char> &values = it->second; + for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) { + unsigned char value = values[arrayIndex]; + out.push_back(EqExpr::create( + ReadExpr::create(UpdateList(array, 0), + ConstantExpr::alloc(arrayIndex, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); + } + } +} } diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp new file mode 100644 index 00000000..a4d97f54 --- /dev/null +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -0,0 +1,158 @@ +//===-- AssignmentValidatingSolver.cpp ------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/util/Assignment.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include <vector> + +namespace klee { + +class AssignmentValidatingSolver : public SolverImpl { +private: + Solver *solver; + void dumpAssignmentQuery(const Query &query, const Assignment &assignment); + +public: + AssignmentValidatingSolver(Solver *_solver) : solver(_solver) {} + ~AssignmentValidatingSolver() { delete solver; } + + bool computeValidity(const Query &, Solver::Validity &result); + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref<Expr> &result); + bool computeInitialValues(const Query &, + const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; + +// TODO: use computeInitialValues for all queries for more stress testing +bool AssignmentValidatingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + return solver->impl->computeValidity(query, result); +} +bool AssignmentValidatingSolver::computeTruth(const Query &query, + bool &isValid) { + return solver->impl->computeTruth(query, isValid); +} +bool AssignmentValidatingSolver::computeValue(const Query &query, + ref<Expr> &result) { + return solver->impl->computeValue(query, result); +} + +bool AssignmentValidatingSolver::computeInitialValues( + const Query &query, const std::vector<const Array *> &objects, + std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + if (!hasSolution) + return success; + + // Use `_allowFreeValues` so that if we are missing an assignment + // we can't compute a constant and flag this as a problem. + Assignment assignment(objects, values, /*_allowFreeValues=*/true); + // Check computed assignment satisfies query + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + ref<Expr> constraint = *it; + ref<Expr> constraintEvaluated = assignment.evaluate(constraint); + ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated); + if (CE == NULL) { + llvm::errs() << "Constraint did not evalaute to a constant:\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Evaluated Constraint:\n" << constraintEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + if (CE->isFalse()) { + llvm::errs() << "Constraint evaluated to false when using assignment\n"; + llvm::errs() << "Constraint:\n" << constraint << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + } + + ref<Expr> queryExprEvaluated = assignment.evaluate(query.expr); + ConstantExpr *CE = dyn_cast<ConstantExpr>(queryExprEvaluated); + if (CE == NULL) { + llvm::errs() << "Query expression did not evalaute to a constant:\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Evaluated expression:\n" << queryExprEvaluated << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + // KLEE queries are validity queries. A counter example to + // ∀ x constraints(x) → query(x) + // exists therefore + // ¬∀ x constraints(x) → query(x) + // Which is equivalent to + // ∃ x constraints(x) ∧ ¬ query(x) + // This means for the assignment we get back query expression should evaluate + // to false. + if (CE->isTrue()) { + llvm::errs() + << "Query Expression evaluated to true when using assignment\n"; + llvm::errs() << "Expression:\n" << query.expr << "\n"; + llvm::errs() << "Assignment:\n"; + assignment.dump(); + dumpAssignmentQuery(query, assignment); + abort(); + } + + return success; +} + +void AssignmentValidatingSolver::dumpAssignmentQuery( + const Query &query, const Assignment &assignment) { + // Create a Query that is augmented with constraints that + // enforce the given assignment. + std::vector<ref<Expr> > constraints; + assignment.createConstraintsFromAssignment(constraints); + // Add Constraints from `query` + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) { + constraints.push_back(*it); + } + ConstraintManager augmentedConstraints(constraints); + Query augmentedQuery(augmentedConstraints, query.expr); + + // Ask the solver for the log for this query. + char *logText = solver->getConstraintLog(augmentedQuery); + llvm::errs() << "Query with assignment as constraints:\n" << logText << "\n"; + free(logText); +} + +SolverImpl::SolverRunStatus +AssignmentValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + +char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { + return solver->impl->getConstraintLog(query); +} + +void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) { + return solver->impl->setCoreSolverTimeout(timeout); +} + +Solver *createAssignmentValidatingSolver(Solver *s) { + return new Solver(new AssignmentValidatingSolver(s)); +} +} |