klee
ValidatingSolver.cpp
Go to the documentation of this file.
1//===-- ValidatingSolver.cpp ----------------------------------------------===//
2//
3// The KLEE Symbolic Virtual Machine
4//
5// This file is distributed under the University of Illinois Open Source
6// License. See LICENSE.TXT for details.
7//
8//===----------------------------------------------------------------------===//
9
11#include "klee/Solver/Solver.h"
13
14#include <vector>
15
16namespace klee {
17
19private:
21
22public:
23 ValidatingSolver(Solver *_solver, Solver *_oracle)
24 : solver(_solver), oracle(_oracle) {}
26
27 bool computeValidity(const Query &, Solver::Validity &result);
28 bool computeTruth(const Query &, bool &isValid);
29 bool computeValue(const Query &, ref<Expr> &result);
30 bool computeInitialValues(const Query &,
31 const std::vector<const Array *> &objects,
32 std::vector<std::vector<unsigned char> > &values,
33 bool &hasSolution);
35 char *getConstraintLog(const Query &);
36 void setCoreSolverTimeout(time::Span timeout);
37};
38
39bool ValidatingSolver::computeTruth(const Query &query, bool &isValid) {
40 bool answer;
41
42 if (!solver->impl->computeTruth(query, isValid))
43 return false;
44 if (!oracle->impl->computeTruth(query, answer))
45 return false;
46
47 if (isValid != answer)
48 assert(0 && "invalid solver result (computeTruth)");
49
50 return true;
51}
52
54 Solver::Validity &result) {
55 Solver::Validity answer;
56
57 if (!solver->impl->computeValidity(query, result))
58 return false;
59 if (!oracle->impl->computeValidity(query, answer))
60 return false;
61
62 if (result != answer)
63 assert(0 && "invalid solver result (computeValidity)");
64
65 return true;
66}
67
68bool ValidatingSolver::computeValue(const Query &query, ref<Expr> &result) {
69 bool answer;
70
71 if (!solver->impl->computeValue(query, result))
72 return false;
73 // We don't want to compare, but just make sure this is a legal
74 // solution.
76 query.withExpr(NeExpr::create(query.expr, result)), answer))
77 return false;
78
79 if (answer)
80 assert(0 && "invalid solver result (computeValue)");
81
82 return true;
83}
84
86 const Query &query, const std::vector<const Array *> &objects,
87 std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
88 bool answer;
89
90 if (!solver->impl->computeInitialValues(query, objects, values, hasSolution))
91 return false;
92
93 if (hasSolution) {
94 // Assert the bindings as constraints, and verify that the
95 // conjunction of the actual constraints is satisfiable.
96 ConstraintSet bindings;
97 for (unsigned i = 0; i != values.size(); ++i) {
98 const Array *array = objects[i];
99 assert(array);
100 for (unsigned j = 0; j < array->size; j++) {
101 unsigned char value = values[i][j];
102 bindings.push_back(EqExpr::create(
104 ConstantExpr::alloc(j, array->getDomain())),
105 ConstantExpr::alloc(value, array->getRange())));
106 }
107 }
108 ConstraintManager tmp(bindings);
109 ref<Expr> constraints = Expr::createIsZero(query.expr);
110 for (auto const &constraint : query.constraints)
111 constraints = AndExpr::create(constraints, constraint);
112
113 if (!oracle->impl->computeTruth(Query(bindings, constraints), answer))
114 return false;
115 if (!answer)
116 assert(0 && "invalid solver result (computeInitialValues)");
117 } else {
118 if (!oracle->impl->computeTruth(query, answer))
119 return false;
120 if (!answer)
121 assert(0 && "invalid solver result (computeInitialValues)");
122 }
123
124 return true;
125}
126
129}
130
132 return solver->impl->getConstraintLog(query);
133}
134
137}
138
140 return new Solver(new ValidatingSolver(s, oracle));
141}
142}
Expr::Width getRange() const
Definition: Expr.h:530
const unsigned size
Definition: Expr.h:489
Expr::Width getDomain() const
Definition: Expr.h:529
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:1065
Manages constraints, e.g. optimisation.
Definition: Constraints.h:50
void push_back(const ref< Expr > &e)
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:322
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:538
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:25
virtual void setCoreSolverTimeout(time::Span timeout)
Definition: SolverImpl.h:109
virtual bool computeTruth(const Query &query, bool &isValid)=0
virtual bool computeInitialValues(const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0
virtual bool computeValue(const Query &query, ref< Expr > &result)=0
virtual char * getConstraintLog(const Query &query)
Definition: SolverImpl.h:104
virtual bool computeValidity(const Query &query, Solver::Validity &result)
Definition: SolverImpl.cpp:17
virtual SolverRunStatus getOperationStatusCode()=0
getOperationStatusCode - get the status of the last solver operation
SolverImpl * impl
Definition: Solver.h:77
Class representing a complete list of updates into an array.
Definition: Expr.h:539
bool computeTruth(const Query &, bool &isValid)
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
ValidatingSolver(Solver *_solver, Solver *_oracle)
bool computeValidity(const Query &, Solver::Validity &result)
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
void setCoreSolverTimeout(time::Span timeout)
bool computeValue(const Query &, ref< Expr > &result)
char * getConstraintLog(const Query &)
Definition: main.cpp:291
Solver * createValidatingSolver(Solver *s, Solver *oracle)
ref< Expr > expr
Definition: Solver.h:35
Query withExpr(ref< Expr > _expr) const
withExpr - Return a copy of the query with the given expression.
Definition: Solver.h:42
const ConstraintSet & constraints
Definition: Solver.h:34