From 0784ff823bdf8cf52eb08ecae2987d9a79b7f45b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 7 Jan 2016 09:31:56 +0000 Subject: [NFC] Refactor ValidatingSolver out of Solver.cpp into its own file ``ValidatingSolver.cpp``. Whilst I'm here also clang-format the modified code. --- lib/Solver/Solver.cpp | 134 ------------------------------------- lib/Solver/ValidatingSolver.cpp | 142 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 142 insertions(+), 134 deletions(-) create mode 100644 lib/Solver/ValidatingSolver.cpp diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 30424526..e596d37d 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -276,140 +276,6 @@ std::pair< ref, ref > Solver::getRange(const Query& query) { ConstantExpr::create(max, width)); } -/***/ - -class ValidatingSolver : public SolverImpl { -private: - Solver *solver, *oracle; - -public: - ValidatingSolver(Solver *_solver, Solver *_oracle) - : solver(_solver), oracle(_oracle) {} - ~ValidatingSolver() { delete solver; } - - bool computeValidity(const Query&, Solver::Validity &result); - bool computeTruth(const Query&, bool &isValid); - bool computeValue(const Query&, ref &result); - bool computeInitialValues(const Query&, - const std::vector &objects, - std::vector< std::vector > &values, - bool &hasSolution); - SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); -}; - -bool ValidatingSolver::computeTruth(const Query& query, - bool &isValid) { - bool answer; - - if (!solver->impl->computeTruth(query, isValid)) - return false; - if (!oracle->impl->computeTruth(query, answer)) - return false; - - if (isValid != answer) - assert(0 && "invalid solver result (computeTruth)"); - - return true; -} - -bool ValidatingSolver::computeValidity(const Query& query, - Solver::Validity &result) { - Solver::Validity answer; - - if (!solver->impl->computeValidity(query, result)) - return false; - if (!oracle->impl->computeValidity(query, answer)) - return false; - - if (result != answer) - assert(0 && "invalid solver result (computeValidity)"); - - return true; -} - -bool ValidatingSolver::computeValue(const Query& query, - ref &result) { - bool answer; - - if (!solver->impl->computeValue(query, result)) - return false; - // We don't want to compare, but just make sure this is a legal - // solution. - if (!oracle->impl->computeTruth(query.withExpr(NeExpr::create(query.expr, - result)), - answer)) - return false; - - if (answer) - assert(0 && "invalid solver result (computeValue)"); - - return true; -} - -bool -ValidatingSolver::computeInitialValues(const Query& query, - const std::vector - &objects, - std::vector< std::vector > - &values, - bool &hasSolution) { - bool answer; - - if (!solver->impl->computeInitialValues(query, objects, values, - hasSolution)) - return false; - - if (hasSolution) { - // Assert the bindings as constraints, and verify that the - // conjunction of the actual constraints is satisfiable. - std::vector< ref > bindings; - for (unsigned i = 0; i != values.size(); ++i) { - const Array *array = objects[i]; - assert(array); - for (unsigned j=0; jsize; j++) { - unsigned char value = values[i][j]; - bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(j, array->getDomain())), - ConstantExpr::alloc(value, array->getRange()))); - } - } - ConstraintManager tmp(bindings); - ref constraints = Expr::createIsZero(query.expr); - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) - constraints = AndExpr::create(constraints, *it); - - if (!oracle->impl->computeTruth(Query(tmp, constraints), answer)) - return false; - if (!answer) - assert(0 && "invalid solver result (computeInitialValues)"); - } else { - if (!oracle->impl->computeTruth(query, answer)) - return false; - if (!answer) - assert(0 && "invalid solver result (computeInitialValues)"); - } - - return true; -} - -SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() { - return solver->impl->getOperationStatusCode(); -} - -char *ValidatingSolver::getConstraintLog(const Query& query) { - return solver->impl->getConstraintLog(query); -} - -void ValidatingSolver::setCoreSolverTimeout(double timeout) { - solver->impl->setCoreSolverTimeout(timeout); -} - -Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) { - return new Solver(new ValidatingSolver(s, oracle)); -} /***/ diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp new file mode 100644 index 00000000..ef79b563 --- /dev/null +++ b/lib/Solver/ValidatingSolver.cpp @@ -0,0 +1,142 @@ +//===-- ValidatingSolver.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/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include + +namespace klee { + +class ValidatingSolver : public SolverImpl { +private: + Solver *solver, *oracle; + +public: + ValidatingSolver(Solver *_solver, Solver *_oracle) + : solver(_solver), oracle(_oracle) {} + ~ValidatingSolver() { delete solver; } + + bool computeValidity(const Query &, Solver::Validity &result); + bool computeTruth(const Query &, bool &isValid); + bool computeValue(const Query &, ref &result); + bool computeInitialValues(const Query &, + const std::vector &objects, + std::vector > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; + +bool ValidatingSolver::computeTruth(const Query &query, bool &isValid) { + bool answer; + + if (!solver->impl->computeTruth(query, isValid)) + return false; + if (!oracle->impl->computeTruth(query, answer)) + return false; + + if (isValid != answer) + assert(0 && "invalid solver result (computeTruth)"); + + return true; +} + +bool ValidatingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + Solver::Validity answer; + + if (!solver->impl->computeValidity(query, result)) + return false; + if (!oracle->impl->computeValidity(query, answer)) + return false; + + if (result != answer) + assert(0 && "invalid solver result (computeValidity)"); + + return true; +} + +bool ValidatingSolver::computeValue(const Query &query, ref &result) { + bool answer; + + if (!solver->impl->computeValue(query, result)) + return false; + // We don't want to compare, but just make sure this is a legal + // solution. + if (!oracle->impl->computeTruth( + query.withExpr(NeExpr::create(query.expr, result)), answer)) + return false; + + if (answer) + assert(0 && "invalid solver result (computeValue)"); + + return true; +} + +bool ValidatingSolver::computeInitialValues( + const Query &query, const std::vector &objects, + std::vector > &values, bool &hasSolution) { + bool answer; + + if (!solver->impl->computeInitialValues(query, objects, values, hasSolution)) + return false; + + if (hasSolution) { + // Assert the bindings as constraints, and verify that the + // conjunction of the actual constraints is satisfiable. + std::vector > bindings; + for (unsigned i = 0; i != values.size(); ++i) { + const Array *array = objects[i]; + assert(array); + for (unsigned j = 0; j < array->size; j++) { + unsigned char value = values[i][j]; + bindings.push_back(EqExpr::create( + ReadExpr::create(UpdateList(array, 0), + ConstantExpr::alloc(j, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); + } + } + ConstraintManager tmp(bindings); + ref constraints = Expr::createIsZero(query.expr); + for (ConstraintManager::const_iterator it = query.constraints.begin(), + ie = query.constraints.end(); + it != ie; ++it) + constraints = AndExpr::create(constraints, *it); + + if (!oracle->impl->computeTruth(Query(tmp, constraints), answer)) + return false; + if (!answer) + assert(0 && "invalid solver result (computeInitialValues)"); + } else { + if (!oracle->impl->computeTruth(query, answer)) + return false; + if (!answer) + assert(0 && "invalid solver result (computeInitialValues)"); + } + + return true; +} + +SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + +char *ValidatingSolver::getConstraintLog(const Query &query) { + return solver->impl->getConstraintLog(query); +} + +void ValidatingSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} + +Solver *createValidatingSolver(Solver *s, Solver *oracle) { + return new Solver(new ValidatingSolver(s, oracle)); +} +} -- cgit 1.4.1