From a8abaa43873b8ee49320035817fcdd70a9879bda Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 15 Aug 2019 22:57:36 +0100 Subject: Moved solver-related header files into a separate klee/Solver/ directory. --- include/klee/Common.h | 3 +- include/klee/Expr/ArrayExprHash.h | 3 +- include/klee/Expr/ExprSMTLIBPrinter.h | 2 +- include/klee/IncompleteSolver.h | 111 ------------ include/klee/Solver.h | 273 ------------------------------ include/klee/Solver/IncompleteSolver.h | 111 ++++++++++++ include/klee/Solver/Solver.h | 273 ++++++++++++++++++++++++++++++ include/klee/Solver/SolverCmdLine.h | 93 ++++++++++ include/klee/Solver/SolverImpl.h | 114 +++++++++++++ include/klee/Solver/SolverStats.h | 38 +++++ include/klee/SolverCmdLine.h | 93 ---------- include/klee/SolverImpl.h | 114 ------------- include/klee/SolverStats.h | 38 ----- lib/Core/Executor.cpp | 4 +- lib/Core/ExecutorUtil.cpp | 2 +- lib/Core/ImpliedValue.cpp | 2 +- lib/Core/Memory.cpp | 2 +- lib/Core/SpecialFunctionHandler.cpp | 4 +- lib/Core/StatsTracker.cpp | 2 +- lib/Core/TimingSolver.cpp | 2 +- lib/Core/TimingSolver.h | 2 +- lib/Core/UserSearcher.cpp | 3 +- lib/Expr/ArrayExprVisitor.h | 2 +- lib/Expr/Parser.cpp | 2 +- lib/Solver/AssignmentValidatingSolver.cpp | 4 +- lib/Solver/CachingSolver.cpp | 9 +- lib/Solver/CexCachingSolver.cpp | 6 +- lib/Solver/ConstructSolverChain.cpp | 4 +- lib/Solver/CoreSolver.cpp | 7 +- lib/Solver/DummySolver.cpp | 6 +- lib/Solver/FastCexSolver.cpp | 4 +- lib/Solver/IncompleteSolver.cpp | 2 +- lib/Solver/IndependentSolver.cpp | 4 +- lib/Solver/MetaSMTSolver.cpp | 4 +- lib/Solver/MetaSMTSolver.h | 2 +- lib/Solver/QueryLoggingSolver.h | 4 +- lib/Solver/STPBuilder.cpp | 4 +- lib/Solver/STPSolver.cpp | 2 +- lib/Solver/STPSolver.h | 2 +- lib/Solver/Solver.cpp | 4 +- lib/Solver/SolverCmdLine.cpp | 3 +- lib/Solver/SolverImpl.cpp | 4 +- lib/Solver/SolverStats.cpp | 2 +- lib/Solver/ValidatingSolver.cpp | 4 +- lib/Solver/Z3Builder.cpp | 4 +- lib/Solver/Z3Solver.cpp | 4 +- lib/Solver/Z3Solver.h | 2 +- tools/kleaver/main.cpp | 6 +- tools/klee/main.cpp | 2 +- unittests/Solver/SolverTest.cpp | 4 +- 50 files changed, 700 insertions(+), 696 deletions(-) delete mode 100644 include/klee/IncompleteSolver.h delete mode 100644 include/klee/Solver.h create mode 100644 include/klee/Solver/IncompleteSolver.h create mode 100644 include/klee/Solver/Solver.h create mode 100644 include/klee/Solver/SolverCmdLine.h create mode 100644 include/klee/Solver/SolverImpl.h create mode 100644 include/klee/Solver/SolverStats.h delete mode 100644 include/klee/SolverCmdLine.h delete mode 100644 include/klee/SolverImpl.h delete mode 100644 include/klee/SolverStats.h diff --git a/include/klee/Common.h b/include/klee/Common.h index 611b137c..7b244158 100644 --- a/include/klee/Common.h +++ b/include/klee/Common.h @@ -14,7 +14,8 @@ #ifndef KLEE_COMMON_H #define KLEE_COMMON_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" + #include namespace klee { diff --git a/include/klee/Expr/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h index 04660fe0..f8bef491 100644 --- a/include/klee/Expr/ArrayExprHash.h +++ b/include/klee/Expr/ArrayExprHash.h @@ -11,11 +11,10 @@ #define KLEE_ARRAYEXPRHASH_H #include "klee/Expr/Expr.h" +#include "klee/Solver/SolverStats.h" #include "klee/TimerStatIncrementer.h" -#include "klee/SolverStats.h" #include - #include namespace klee { diff --git a/include/klee/Expr/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h index a7a604e1..38ae2fa1 100644 --- a/include/klee/Expr/ExprSMTLIBPrinter.h +++ b/include/klee/Expr/ExprSMTLIBPrinter.h @@ -13,7 +13,7 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/util/PrintContext.h" #include diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h deleted file mode 100644 index 6511584e..00000000 --- a/include/klee/IncompleteSolver.h +++ /dev/null @@ -1,111 +0,0 @@ -//===-- IncompleteSolver.h --------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_INCOMPLETESOLVER_H -#define KLEE_INCOMPLETESOLVER_H - -#include "klee/Solver.h" -#include "klee/SolverImpl.h" - -namespace klee { - -/// IncompleteSolver - Base class for incomplete solver -/// implementations. -/// -/// Incomplete solvers are useful for implementing optimizations which -/// may quickly compute an answer, but cannot always compute the -/// correct answer. They can be used with the StagedSolver to provide -/// a complete Solver implementation. -class IncompleteSolver { -public: - /// PartialValidity - Represent a possibility incomplete query - /// validity. - enum PartialValidity { - /// The query is provably true. - MustBeTrue = 1, - - /// The query is provably false. - MustBeFalse = -1, - - /// The query is not provably false (a true assignment is known to - /// exist). - MayBeTrue = 2, - - /// The query is not provably true (a false assignment is known to - /// exist). - MayBeFalse = -2, - - /// The query is known to have both true and false assignments. - TrueOrFalse = 0, - - /// The validity of the query is unknown. - None = 3 - }; - - static PartialValidity negatePartialValidity(PartialValidity pv); - -public: - IncompleteSolver() {} - virtual ~IncompleteSolver() {} - - /// computeValidity - Compute a partial validity for the given query. - /// - /// The passed expression is non-constant with bool type. - /// - /// The IncompleteSolver class provides an implementation of - /// computeValidity using computeTruth. Sub-classes may override - /// this if a more efficient implementation is available. - virtual IncompleteSolver::PartialValidity computeValidity(const Query&); - - /// computeValidity - Compute a partial validity for the given query. - /// - /// The passed expression is non-constant with bool type. - virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0; - - /// computeValue - Attempt to compute a value for the given expression. - virtual bool computeValue(const Query&, ref &result) = 0; - - /// computeInitialValues - Attempt to compute the constant values - /// for the initial state of each given object. If a correct result - /// is not found, then the values array must be unmodified. - virtual bool computeInitialValues(const Query&, - const std::vector - &objects, - std::vector< std::vector > - &values, - bool &hasSolution) = 0; -}; - -/// StagedSolver - Adapter class for staging an incomplete solver with -/// a complete secondary solver, to form an (optimized) complete -/// solver. -class StagedSolverImpl : public SolverImpl { -private: - IncompleteSolver *primary; - Solver *secondary; - -public: - StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary); - ~StagedSolverImpl(); - - bool computeTruth(const Query&, bool &isValid); - bool computeValidity(const Query&, Solver::Validity &result); - 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(time::Span timeout); -}; - -} - -#endif /* KLEE_INCOMPLETESOLVER_H */ diff --git a/include/klee/Solver.h b/include/klee/Solver.h deleted file mode 100644 index f320a5b6..00000000 --- a/include/klee/Solver.h +++ /dev/null @@ -1,273 +0,0 @@ -//===-- Solver.h ------------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_SOLVER_H -#define KLEE_SOLVER_H - -#include "klee/Expr/Expr.h" -#include "klee/SolverCmdLine.h" -#include "klee/Internal/System/Time.h" - -#include - -namespace klee { - class ConstraintManager; - class Expr; - class SolverImpl; - - struct Query { - public: - const ConstraintManager &constraints; - ref expr; - - Query(const ConstraintManager& _constraints, ref _expr) - : constraints(_constraints), expr(_expr) { - } - - /// withExpr - Return a copy of the query with the given expression. - Query withExpr(ref _expr) const { - return Query(constraints, _expr); - } - - /// withFalse - Return a copy of the query with a false expression. - Query withFalse() const { - return Query(constraints, ConstantExpr::alloc(0, Expr::Bool)); - } - - /// negateExpr - Return a copy of the query with the expression negated. - Query negateExpr() const { - return withExpr(Expr::createIsZero(expr)); - } - - /// Dump query - void dump() const ; - }; - - class Solver { - // DO NOT IMPLEMENT. - Solver(const Solver&); - void operator=(const Solver&); - - public: - enum Validity { - True = 1, - False = -1, - Unknown = 0 - }; - - public: - /// validity_to_str - Return the name of given Validity enum value. - static const char *validity_to_str(Validity v); - - public: - SolverImpl *impl; - - public: - Solver(SolverImpl *_impl) : impl(_impl) {} - virtual ~Solver(); - - /// evaluate - Determine for a particular state if the query - /// expression is provably true, provably false or neither. - /// - /// \param [out] result - if - /// \f[ \forall X constraints(X) \to query(X) \f] - /// then Solver::True, - /// else if - /// \f[ \forall X constraints(X) \to \lnot query(X) \f] - /// then Solver::False, - /// else - /// Solver::Unknown - /// - /// \return True on success. - bool evaluate(const Query&, Validity &result); - - /// mustBeTrue - Determine if the expression is provably true. - /// - /// This evaluates the following logical formula: - /// - /// \f[ \forall X constraints(X) \to query(X) \f] - /// - /// which is equivalent to - /// - /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// - /// \param [out] result - On success, true iff the logical formula is true - /// - /// \return True on success. - bool mustBeTrue(const Query&, bool &result); - - /// mustBeFalse - Determine if the expression is provably false. - /// - /// This evaluates the following logical formula: - /// - /// \f[ \lnot \exists X constraints(X) \land query(X) \f] - /// - /// which is equivalent to - /// - /// \f[ \forall X constraints(X) \to \lnot query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// - /// \param [out] result - On success, true iff the logical formula is false - /// - /// \return True on success. - bool mustBeFalse(const Query&, bool &result); - - /// mayBeTrue - Determine if there is a valid assignment for the given state - /// in which the expression evaluates to true. - /// - /// This evaluates the following logical formula: - /// - /// \f[ \exists X constraints(X) \land query(X) \f] - /// - /// which is equivalent to - /// - /// \f[ \lnot \forall X constraints(X) \to \lnot query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// - /// \param [out] result - On success, true iff the logical formula may be true - /// - /// \return True on success. - bool mayBeTrue(const Query&, bool &result); - - /// mayBeFalse - Determine if there is a valid assignment for the given - /// state in which the expression evaluates to false. - /// - /// This evaluates the following logical formula: - /// - /// \f[ \exists X constraints(X) \land \lnot query(X) \f] - /// - /// which is equivalent to - /// - /// \f[ \lnot \forall X constraints(X) \to query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// - /// \param [out] result - On success, true iff the logical formula may be false - /// - /// \return True on success. - bool mayBeFalse(const Query&, bool &result); - - /// getValue - Compute one possible value for the given expression. - /// - /// \param [out] result - On success, a value for the expression in some - /// satisfying assignment. - /// - /// \return True on success. - bool getValue(const Query&, ref &result); - - /// getInitialValues - Compute the initial values for a list of objects. - /// - /// \param [out] result - On success, this vector will be filled in with an - /// array of bytes for each given object (with length matching the object - /// size). The bytes correspond to the initial values for the objects for - /// some satisfying assignment. - /// - /// \return True on success. - /// - /// NOTE: This function returns failure if there is no satisfying - /// assignment. - // - // FIXME: This API is lame. We should probably just provide an API which - // returns an Assignment object, then clients can get out whatever values - // they want. This also allows us to optimize the representation. - bool getInitialValues(const Query&, - const std::vector &objects, - std::vector< std::vector > &result); - - /// getRange - Compute a tight range of possible values for a given - /// expression. - /// - /// \return - A pair with (min, max) values for the expression. - /// - /// \post(mustBeTrue(min <= e <= max) && - /// mayBeTrue(min == e) && - /// mayBeTrue(max == e)) - // - // FIXME: This should go into a helper class, and should handle failure. - virtual std::pair< ref, ref > getRange(const Query&); - - virtual char *getConstraintLog(const Query& query); - virtual void setCoreSolverTimeout(time::Span timeout); - }; - - /* *** */ - - /// createValidatingSolver - Create a solver which will validate all query - /// results against an oracle, used for testing that an optimized solver has - /// the same results as an unoptimized one. This solver will assert on any - /// mismatches. - /// - /// \param s - The primary underlying solver to use. - /// \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). - /// - /// \param s - The underlying solver to use. - Solver *createCachingSolver(Solver *s); - - /// createCexCachingSolver - Create a counterexample caching solver. This is a - /// more sophisticated cache which records counterexamples for a constraint - /// set and uses subset/superset relations among constraints to try and - /// quickly find satisfying assignments. - /// - /// \param s - The underlying solver to use. - Solver *createCexCachingSolver(Solver *s); - - /// createFastCexSolver - Create a "fast counterexample solver", which tries - /// to quickly compute a satisfying assignment for a constraint set using - /// value propogation and range analysis. - /// - /// \param s - The underlying solver to use. - Solver *createFastCexSolver(Solver *s); - - /// createIndependentSolver - Create a solver which will eliminate any - /// unnecessary constraints before propogating the query to the underlying - /// solver. - /// - /// \param s - The underlying solver to use. - Solver *createIndependentSolver(Solver *s); - - /// createKQueryLoggingSolver - Create a solver which will forward all queries - /// after writing them to the given path in .kquery format. - Solver *createKQueryLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); - - /// createSMTLIBLoggingSolver - Create a solver which will forward all queries - /// after writing them to the given path in .smt2 format. - Solver *createSMTLIBLoggingSolver(Solver *s, std::string path, - time::Span minQueryTimeToLog, - bool logTimedOut); - - - /// createDummySolver - Create a dummy solver implementation which always - /// fails. - Solver *createDummySolver(); - - // Create a solver based on the supplied ``CoreSolverType``. - Solver *createCoreSolver(CoreSolverType cst); -} - -#endif /* KLEE_SOLVER_H */ diff --git a/include/klee/Solver/IncompleteSolver.h b/include/klee/Solver/IncompleteSolver.h new file mode 100644 index 00000000..3841c38b --- /dev/null +++ b/include/klee/Solver/IncompleteSolver.h @@ -0,0 +1,111 @@ +//===-- IncompleteSolver.h --------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_INCOMPLETESOLVER_H +#define KLEE_INCOMPLETESOLVER_H + +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" + +namespace klee { + +/// IncompleteSolver - Base class for incomplete solver +/// implementations. +/// +/// Incomplete solvers are useful for implementing optimizations which +/// may quickly compute an answer, but cannot always compute the +/// correct answer. They can be used with the StagedSolver to provide +/// a complete Solver implementation. +class IncompleteSolver { +public: + /// PartialValidity - Represent a possibility incomplete query + /// validity. + enum PartialValidity { + /// The query is provably true. + MustBeTrue = 1, + + /// The query is provably false. + MustBeFalse = -1, + + /// The query is not provably false (a true assignment is known to + /// exist). + MayBeTrue = 2, + + /// The query is not provably true (a false assignment is known to + /// exist). + MayBeFalse = -2, + + /// The query is known to have both true and false assignments. + TrueOrFalse = 0, + + /// The validity of the query is unknown. + None = 3 + }; + + static PartialValidity negatePartialValidity(PartialValidity pv); + +public: + IncompleteSolver() {} + virtual ~IncompleteSolver() {} + + /// computeValidity - Compute a partial validity for the given query. + /// + /// The passed expression is non-constant with bool type. + /// + /// The IncompleteSolver class provides an implementation of + /// computeValidity using computeTruth. Sub-classes may override + /// this if a more efficient implementation is available. + virtual IncompleteSolver::PartialValidity computeValidity(const Query&); + + /// computeValidity - Compute a partial validity for the given query. + /// + /// The passed expression is non-constant with bool type. + virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0; + + /// computeValue - Attempt to compute a value for the given expression. + virtual bool computeValue(const Query&, ref &result) = 0; + + /// computeInitialValues - Attempt to compute the constant values + /// for the initial state of each given object. If a correct result + /// is not found, then the values array must be unmodified. + virtual bool computeInitialValues(const Query&, + const std::vector + &objects, + std::vector< std::vector > + &values, + bool &hasSolution) = 0; +}; + +/// StagedSolver - Adapter class for staging an incomplete solver with +/// a complete secondary solver, to form an (optimized) complete +/// solver. +class StagedSolverImpl : public SolverImpl { +private: + IncompleteSolver *primary; + Solver *secondary; + +public: + StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary); + ~StagedSolverImpl(); + + bool computeTruth(const Query&, bool &isValid); + bool computeValidity(const Query&, Solver::Validity &result); + 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(time::Span timeout); +}; + +} + +#endif /* KLEE_INCOMPLETESOLVER_H */ diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h new file mode 100644 index 00000000..fe4d7e88 --- /dev/null +++ b/include/klee/Solver/Solver.h @@ -0,0 +1,273 @@ +//===-- Solver.h ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_SOLVER_H +#define KLEE_SOLVER_H + +#include "klee/Expr/Expr.h" +#include "klee/Internal/System/Time.h" +#include "klee/Solver/SolverCmdLine.h" + +#include + +namespace klee { + class ConstraintManager; + class Expr; + class SolverImpl; + + struct Query { + public: + const ConstraintManager &constraints; + ref expr; + + Query(const ConstraintManager& _constraints, ref _expr) + : constraints(_constraints), expr(_expr) { + } + + /// withExpr - Return a copy of the query with the given expression. + Query withExpr(ref _expr) const { + return Query(constraints, _expr); + } + + /// withFalse - Return a copy of the query with a false expression. + Query withFalse() const { + return Query(constraints, ConstantExpr::alloc(0, Expr::Bool)); + } + + /// negateExpr - Return a copy of the query with the expression negated. + Query negateExpr() const { + return withExpr(Expr::createIsZero(expr)); + } + + /// Dump query + void dump() const ; + }; + + class Solver { + // DO NOT IMPLEMENT. + Solver(const Solver&); + void operator=(const Solver&); + + public: + enum Validity { + True = 1, + False = -1, + Unknown = 0 + }; + + public: + /// validity_to_str - Return the name of given Validity enum value. + static const char *validity_to_str(Validity v); + + public: + SolverImpl *impl; + + public: + Solver(SolverImpl *_impl) : impl(_impl) {} + virtual ~Solver(); + + /// evaluate - Determine for a particular state if the query + /// expression is provably true, provably false or neither. + /// + /// \param [out] result - if + /// \f[ \forall X constraints(X) \to query(X) \f] + /// then Solver::True, + /// else if + /// \f[ \forall X constraints(X) \to \lnot query(X) \f] + /// then Solver::False, + /// else + /// Solver::Unknown + /// + /// \return True on success. + bool evaluate(const Query&, Validity &result); + + /// mustBeTrue - Determine if the expression is provably true. + /// + /// This evaluates the following logical formula: + /// + /// \f[ \forall X constraints(X) \to query(X) \f] + /// + /// which is equivalent to + /// + /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ is the query expression. + /// + /// \param [out] result - On success, true iff the logical formula is true + /// + /// \return True on success. + bool mustBeTrue(const Query&, bool &result); + + /// mustBeFalse - Determine if the expression is provably false. + /// + /// This evaluates the following logical formula: + /// + /// \f[ \lnot \exists X constraints(X) \land query(X) \f] + /// + /// which is equivalent to + /// + /// \f[ \forall X constraints(X) \to \lnot query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ is the query expression. + /// + /// \param [out] result - On success, true iff the logical formula is false + /// + /// \return True on success. + bool mustBeFalse(const Query&, bool &result); + + /// mayBeTrue - Determine if there is a valid assignment for the given state + /// in which the expression evaluates to true. + /// + /// This evaluates the following logical formula: + /// + /// \f[ \exists X constraints(X) \land query(X) \f] + /// + /// which is equivalent to + /// + /// \f[ \lnot \forall X constraints(X) \to \lnot query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ is the query expression. + /// + /// \param [out] result - On success, true iff the logical formula may be true + /// + /// \return True on success. + bool mayBeTrue(const Query&, bool &result); + + /// mayBeFalse - Determine if there is a valid assignment for the given + /// state in which the expression evaluates to false. + /// + /// This evaluates the following logical formula: + /// + /// \f[ \exists X constraints(X) \land \lnot query(X) \f] + /// + /// which is equivalent to + /// + /// \f[ \lnot \forall X constraints(X) \to query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ is the query expression. + /// + /// \param [out] result - On success, true iff the logical formula may be false + /// + /// \return True on success. + bool mayBeFalse(const Query&, bool &result); + + /// getValue - Compute one possible value for the given expression. + /// + /// \param [out] result - On success, a value for the expression in some + /// satisfying assignment. + /// + /// \return True on success. + bool getValue(const Query&, ref &result); + + /// getInitialValues - Compute the initial values for a list of objects. + /// + /// \param [out] result - On success, this vector will be filled in with an + /// array of bytes for each given object (with length matching the object + /// size). The bytes correspond to the initial values for the objects for + /// some satisfying assignment. + /// + /// \return True on success. + /// + /// NOTE: This function returns failure if there is no satisfying + /// assignment. + // + // FIXME: This API is lame. We should probably just provide an API which + // returns an Assignment object, then clients can get out whatever values + // they want. This also allows us to optimize the representation. + bool getInitialValues(const Query&, + const std::vector &objects, + std::vector< std::vector > &result); + + /// getRange - Compute a tight range of possible values for a given + /// expression. + /// + /// \return - A pair with (min, max) values for the expression. + /// + /// \post(mustBeTrue(min <= e <= max) && + /// mayBeTrue(min == e) && + /// mayBeTrue(max == e)) + // + // FIXME: This should go into a helper class, and should handle failure. + virtual std::pair< ref, ref > getRange(const Query&); + + virtual char *getConstraintLog(const Query& query); + virtual void setCoreSolverTimeout(time::Span timeout); + }; + + /* *** */ + + /// createValidatingSolver - Create a solver which will validate all query + /// results against an oracle, used for testing that an optimized solver has + /// the same results as an unoptimized one. This solver will assert on any + /// mismatches. + /// + /// \param s - The primary underlying solver to use. + /// \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). + /// + /// \param s - The underlying solver to use. + Solver *createCachingSolver(Solver *s); + + /// createCexCachingSolver - Create a counterexample caching solver. This is a + /// more sophisticated cache which records counterexamples for a constraint + /// set and uses subset/superset relations among constraints to try and + /// quickly find satisfying assignments. + /// + /// \param s - The underlying solver to use. + Solver *createCexCachingSolver(Solver *s); + + /// createFastCexSolver - Create a "fast counterexample solver", which tries + /// to quickly compute a satisfying assignment for a constraint set using + /// value propogation and range analysis. + /// + /// \param s - The underlying solver to use. + Solver *createFastCexSolver(Solver *s); + + /// createIndependentSolver - Create a solver which will eliminate any + /// unnecessary constraints before propogating the query to the underlying + /// solver. + /// + /// \param s - The underlying solver to use. + Solver *createIndependentSolver(Solver *s); + + /// createKQueryLoggingSolver - Create a solver which will forward all queries + /// after writing them to the given path in .kquery format. + Solver *createKQueryLoggingSolver(Solver *s, std::string path, + time::Span minQueryTimeToLog, + bool logTimedOut); + + /// createSMTLIBLoggingSolver - Create a solver which will forward all queries + /// after writing them to the given path in .smt2 format. + Solver *createSMTLIBLoggingSolver(Solver *s, std::string path, + time::Span minQueryTimeToLog, + bool logTimedOut); + + + /// createDummySolver - Create a dummy solver implementation which always + /// fails. + Solver *createDummySolver(); + + // Create a solver based on the supplied ``CoreSolverType``. + Solver *createCoreSolver(CoreSolverType cst); +} + +#endif /* KLEE_SOLVER_H */ diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h new file mode 100644 index 00000000..b453d058 --- /dev/null +++ b/include/klee/Solver/SolverCmdLine.h @@ -0,0 +1,93 @@ +//===-- SolverCmdLine.h -----------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +/* + * This header groups command-line options and associated declarations + * that are common to both KLEE and Kleaver. + */ + +#ifndef KLEE_SOLVERCMDLINE_H +#define KLEE_SOLVERCMDLINE_H + +#include "klee/Config/config.h" + +#include "llvm/ADT/ArrayRef.h" +#include "llvm/Support/CommandLine.h" + +namespace klee { + +extern llvm::cl::opt UseFastCexSolver; + +extern llvm::cl::opt UseCexCache; + +extern llvm::cl::opt UseBranchCache; + +extern llvm::cl::opt UseIndependentSolver; + +extern llvm::cl::opt DebugValidateSolver; + +extern llvm::cl::opt MinQueryTimeToLog; + +extern llvm::cl::opt LogTimedOutQueries; + +extern llvm::cl::opt MaxCoreSolverTime; + +extern llvm::cl::opt UseForkedCoreSolver; + +extern llvm::cl::opt CoreSolverOptimizeDivides; + +extern llvm::cl::opt UseAssignmentValidatingSolver; + +/// The different query logging solvers that can be switched on/off +enum QueryLoggingSolverType { + ALL_KQUERY, ///< Log all queries in .kquery (KQuery) format + ALL_SMTLIB, ///< Log all queries .smt2 (SMT-LIBv2) format + SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format + SOLVER_SMTLIB ///< Log queries passed to solver in .smt2 (SMT-LIBv2) format +}; + +extern llvm::cl::bits QueryLoggingOptions; + +enum CoreSolverType { + STP_SOLVER, + METASMT_SOLVER, + DUMMY_SOLVER, + Z3_SOLVER, + NO_SOLVER +}; + +extern llvm::cl::opt CoreSolverToUse; + +extern llvm::cl::opt DebugCrossCheckCoreSolverWith; + +#ifdef ENABLE_METASMT + +enum MetaSMTBackendType { + METASMT_BACKEND_STP, + METASMT_BACKEND_Z3, + METASMT_BACKEND_BOOLECTOR, + METASMT_BACKEND_CVC4, + METASMT_BACKEND_YICES2 +}; + +extern llvm::cl::opt MetaSMTBackend; + +#endif /* ENABLE_METASMT */ + +class KCommandLine { +public: + /// Hide all options in the specified category + static void HideOptions(llvm::cl::OptionCategory &Category); + + /// Hide all options except the ones in the specified category + static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category); +}; +} // namespace klee + +#endif /* KLEE_SOLVERCMDLINE_H */ diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h new file mode 100644 index 00000000..90d5af24 --- /dev/null +++ b/include/klee/Solver/SolverImpl.h @@ -0,0 +1,114 @@ +//===-- SolverImpl.h --------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_SOLVERIMPL_H +#define KLEE_SOLVERIMPL_H + +#include "klee/Internal/System/Time.h" +#include "Solver.h" + +#include + +namespace klee { + class Array; + class ExecutionState; + class Expr; + struct Query; + + /// SolverImpl - Abstract base clase for solver implementations. + class SolverImpl { + // DO NOT IMPLEMENT. + SolverImpl(const SolverImpl&); + void operator=(const SolverImpl&); + + public: + SolverImpl() {} + virtual ~SolverImpl(); + + enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, + SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, + SOLVER_RUN_STATUS_FAILURE, + SOLVER_RUN_STATUS_TIMEOUT, + SOLVER_RUN_STATUS_FORK_FAILED, + SOLVER_RUN_STATUS_INTERRUPTED, + SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, + SOLVER_RUN_STATUS_WAITPID_FAILED }; + + /// computeValidity - Compute a full validity result for the + /// query. + /// + /// The query expression is guaranteed to be non-constant and have + /// bool type. + /// + /// SolverImpl provides a default implementation which uses + /// computeTruth. Clients should override this if a more efficient + /// implementation is available. + /// + /// \param [out] result - if + /// \f[ \forall X constraints(X) \to query(X) \f] + /// then Solver::True, + /// else if + /// \f[ \forall X constraints(X) \to \lnot query(X) \f] + /// then Solver::False, + /// else + /// Solver::Unknown + /// + /// \return True on success + virtual bool computeValidity(const Query& query, Solver::Validity &result); + + /// computeTruth - Determine whether the given query expression is provably true + /// given the constraints. + /// + /// The query expression is guaranteed to be non-constant and have + /// bool type. + /// + /// This method should evaluate the logical formula: + /// + /// \f[ \forall X constraints(X) \to query(X) \f] + /// + /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints + /// in the query and \f$query(X)\f$ is the query expression. + /// + /// \param [out] isValid - On success, true iff the logical formula is true. + /// \return True on success + virtual bool computeTruth(const Query& query, bool &isValid) = 0; + + /// computeValue - Compute a feasible value for the expression. + /// + /// The query expression is guaranteed to be non-constant. + /// + /// \return True on success + virtual bool computeValue(const Query& query, ref &result) = 0; + + /// \sa Solver::getInitialValues() + virtual bool computeInitialValues(const Query& query, + const std::vector + &objects, + std::vector< std::vector > + &values, + bool &hasSolution) = 0; + + /// getOperationStatusCode - get the status of the last solver operation + virtual SolverRunStatus getOperationStatusCode() = 0; + + /// getOperationStatusString - get string representation of the operation + /// status code + static const char* getOperationStatusString(SolverRunStatus statusCode); + + virtual char *getConstraintLog(const Query& query) { + // dummy + return nullptr; + } + + virtual void setCoreSolverTimeout(time::Span timeout) {}; +}; + +} + +#endif /* KLEE_SOLVERIMPL_H */ diff --git a/include/klee/Solver/SolverStats.h b/include/klee/Solver/SolverStats.h new file mode 100644 index 00000000..dd39043a --- /dev/null +++ b/include/klee/Solver/SolverStats.h @@ -0,0 +1,38 @@ +//===-- SolverStats.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_SOLVERSTATS_H +#define KLEE_SOLVERSTATS_H + +#include "klee/Statistic.h" + +namespace klee { +namespace stats { + + extern Statistic cexCacheTime; + extern Statistic queries; + extern Statistic queriesInvalid; + extern Statistic queriesValid; + extern Statistic queryCacheHits; + extern Statistic queryCacheMisses; + extern Statistic queryCexCacheHits; + extern Statistic queryCexCacheMisses; + extern Statistic queryConstructTime; + extern Statistic queryConstructs; + extern Statistic queryCounterexamples; + extern Statistic queryTime; + +#ifdef KLEE_ARRAY_DEBUG + extern Statistic arrayHashTime; +#endif + +} +} + +#endif /* KLEE_SOLVERSTATS_H */ diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h deleted file mode 100644 index b453d058..00000000 --- a/include/klee/SolverCmdLine.h +++ /dev/null @@ -1,93 +0,0 @@ -//===-- SolverCmdLine.h -----------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -/* - * This header groups command-line options and associated declarations - * that are common to both KLEE and Kleaver. - */ - -#ifndef KLEE_SOLVERCMDLINE_H -#define KLEE_SOLVERCMDLINE_H - -#include "klee/Config/config.h" - -#include "llvm/ADT/ArrayRef.h" -#include "llvm/Support/CommandLine.h" - -namespace klee { - -extern llvm::cl::opt UseFastCexSolver; - -extern llvm::cl::opt UseCexCache; - -extern llvm::cl::opt UseBranchCache; - -extern llvm::cl::opt UseIndependentSolver; - -extern llvm::cl::opt DebugValidateSolver; - -extern llvm::cl::opt MinQueryTimeToLog; - -extern llvm::cl::opt LogTimedOutQueries; - -extern llvm::cl::opt MaxCoreSolverTime; - -extern llvm::cl::opt UseForkedCoreSolver; - -extern llvm::cl::opt CoreSolverOptimizeDivides; - -extern llvm::cl::opt UseAssignmentValidatingSolver; - -/// The different query logging solvers that can be switched on/off -enum QueryLoggingSolverType { - ALL_KQUERY, ///< Log all queries in .kquery (KQuery) format - ALL_SMTLIB, ///< Log all queries .smt2 (SMT-LIBv2) format - SOLVER_KQUERY, ///< Log queries passed to solver in .kquery (KQuery) format - SOLVER_SMTLIB ///< Log queries passed to solver in .smt2 (SMT-LIBv2) format -}; - -extern llvm::cl::bits QueryLoggingOptions; - -enum CoreSolverType { - STP_SOLVER, - METASMT_SOLVER, - DUMMY_SOLVER, - Z3_SOLVER, - NO_SOLVER -}; - -extern llvm::cl::opt CoreSolverToUse; - -extern llvm::cl::opt DebugCrossCheckCoreSolverWith; - -#ifdef ENABLE_METASMT - -enum MetaSMTBackendType { - METASMT_BACKEND_STP, - METASMT_BACKEND_Z3, - METASMT_BACKEND_BOOLECTOR, - METASMT_BACKEND_CVC4, - METASMT_BACKEND_YICES2 -}; - -extern llvm::cl::opt MetaSMTBackend; - -#endif /* ENABLE_METASMT */ - -class KCommandLine { -public: - /// Hide all options in the specified category - static void HideOptions(llvm::cl::OptionCategory &Category); - - /// Hide all options except the ones in the specified category - static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category); -}; -} // namespace klee - -#endif /* KLEE_SOLVERCMDLINE_H */ diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h deleted file mode 100644 index 90d5af24..00000000 --- a/include/klee/SolverImpl.h +++ /dev/null @@ -1,114 +0,0 @@ -//===-- SolverImpl.h --------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_SOLVERIMPL_H -#define KLEE_SOLVERIMPL_H - -#include "klee/Internal/System/Time.h" -#include "Solver.h" - -#include - -namespace klee { - class Array; - class ExecutionState; - class Expr; - struct Query; - - /// SolverImpl - Abstract base clase for solver implementations. - class SolverImpl { - // DO NOT IMPLEMENT. - SolverImpl(const SolverImpl&); - void operator=(const SolverImpl&); - - public: - SolverImpl() {} - virtual ~SolverImpl(); - - enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, - SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, - SOLVER_RUN_STATUS_FAILURE, - SOLVER_RUN_STATUS_TIMEOUT, - SOLVER_RUN_STATUS_FORK_FAILED, - SOLVER_RUN_STATUS_INTERRUPTED, - SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, - SOLVER_RUN_STATUS_WAITPID_FAILED }; - - /// computeValidity - Compute a full validity result for the - /// query. - /// - /// The query expression is guaranteed to be non-constant and have - /// bool type. - /// - /// SolverImpl provides a default implementation which uses - /// computeTruth. Clients should override this if a more efficient - /// implementation is available. - /// - /// \param [out] result - if - /// \f[ \forall X constraints(X) \to query(X) \f] - /// then Solver::True, - /// else if - /// \f[ \forall X constraints(X) \to \lnot query(X) \f] - /// then Solver::False, - /// else - /// Solver::Unknown - /// - /// \return True on success - virtual bool computeValidity(const Query& query, Solver::Validity &result); - - /// computeTruth - Determine whether the given query expression is provably true - /// given the constraints. - /// - /// The query expression is guaranteed to be non-constant and have - /// bool type. - /// - /// This method should evaluate the logical formula: - /// - /// \f[ \forall X constraints(X) \to query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// - /// \param [out] isValid - On success, true iff the logical formula is true. - /// \return True on success - virtual bool computeTruth(const Query& query, bool &isValid) = 0; - - /// computeValue - Compute a feasible value for the expression. - /// - /// The query expression is guaranteed to be non-constant. - /// - /// \return True on success - virtual bool computeValue(const Query& query, ref &result) = 0; - - /// \sa Solver::getInitialValues() - virtual bool computeInitialValues(const Query& query, - const std::vector - &objects, - std::vector< std::vector > - &values, - bool &hasSolution) = 0; - - /// getOperationStatusCode - get the status of the last solver operation - virtual SolverRunStatus getOperationStatusCode() = 0; - - /// getOperationStatusString - get string representation of the operation - /// status code - static const char* getOperationStatusString(SolverRunStatus statusCode); - - virtual char *getConstraintLog(const Query& query) { - // dummy - return nullptr; - } - - virtual void setCoreSolverTimeout(time::Span timeout) {}; -}; - -} - -#endif /* KLEE_SOLVERIMPL_H */ diff --git a/include/klee/SolverStats.h b/include/klee/SolverStats.h deleted file mode 100644 index dd39043a..00000000 --- a/include/klee/SolverStats.h +++ /dev/null @@ -1,38 +0,0 @@ -//===-- SolverStats.h -------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_SOLVERSTATS_H -#define KLEE_SOLVERSTATS_H - -#include "klee/Statistic.h" - -namespace klee { -namespace stats { - - extern Statistic cexCacheTime; - extern Statistic queries; - extern Statistic queriesInvalid; - extern Statistic queriesValid; - extern Statistic queryCacheHits; - extern Statistic queryCacheMisses; - extern Statistic queryCexCacheHits; - extern Statistic queryCexCacheMisses; - extern Statistic queryConstructTime; - extern Statistic queryConstructs; - extern Statistic queryCounterexamples; - extern Statistic queryTime; - -#ifdef KLEE_ARRAY_DEBUG - extern Statistic arrayHashTime; -#endif - -} -} - -#endif /* KLEE_SOLVERSTATS_H */ diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 85cb8e8d..56753bb1 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -47,8 +47,8 @@ #include "klee/Internal/System/Time.h" #include "klee/Interpreter.h" #include "klee/OptionCategories.h" -#include "klee/SolverCmdLine.h" -#include "klee/SolverStats.h" +#include "klee/Solver/SolverCmdLine.h" +#include "klee/Solver/SolverStats.h" #include "klee/TimerStatIncrementer.h" #include "klee/util/GetElementPtrTypeIterator.h" diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 15125fe1..9cd74355 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -16,7 +16,7 @@ #include "klee/Internal/Module/KModule.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Interpreter.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index cc001660..6a17c870 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -15,7 +15,7 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 93be1f44..c7e7a928 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -17,7 +17,7 @@ #include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/util/BitArray.h" #include "llvm/IR/Function.h" diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 231bd88d..4acf2e36 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -13,15 +13,15 @@ #include "Memory.h" #include "MemoryManager.h" #include "TimingSolver.h" -#include "klee/MergeHandler.h" #include "klee/ExecutionState.h" #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/KModule.h" #include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/MergeHandler.h" #include "klee/OptionCategories.h" -#include "klee/SolverCmdLine.h" +#include "klee/Solver/SolverCmdLine.h" #include "llvm/ADT/Twine.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index 408e4d6d..259a8d98 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -18,7 +18,7 @@ #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/MemoryUsage.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/SolverStats.h" +#include "klee/Solver/SolverStats.h" #include "CallPathManager.h" #include "CoreStats.h" diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 0f69509a..81ebf098 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -11,7 +11,7 @@ #include "klee/Config/Version.h" #include "klee/ExecutionState.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Statistics.h" #include "klee/TimerStatIncrementer.h" diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index b08073ab..d74572b8 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -11,7 +11,7 @@ #define KLEE_TIMINGSOLVER_H #include "klee/Expr/Expr.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Internal/System/Time.h" #include diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 7efdb30d..c02c349e 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -13,9 +13,8 @@ #include "Executor.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/SolverCmdLine.h" #include "klee/MergeHandler.h" - +#include "klee/Solver/SolverCmdLine.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h index a6d9ae46..c5a4691e 100644 --- a/lib/Expr/ArrayExprVisitor.h +++ b/lib/Expr/ArrayExprVisitor.h @@ -12,7 +12,7 @@ #include "klee/Expr/ExprBuilder.h" #include "klee/Expr/ExprVisitor.h" -#include "klee/SolverCmdLine.h" +#include "klee/Solver/SolverCmdLine.h" #include #include diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index c365002d..6b29ac3e 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -14,7 +14,7 @@ #include "klee/Expr/ExprPPrinter.h" #include "klee/Expr/Parser/Lexer.h" #include "klee/Expr/Parser/Parser.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "llvm/ADT/APInt.h" #include "llvm/Support/MemoryBuffer.h" diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index b75f982a..7e1ccd38 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -9,8 +9,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Assignment.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 2eedc616..2c7371d0 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -8,14 +8,13 @@ //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" -#include "klee/IncompleteSolver.h" -#include "klee/SolverImpl.h" - -#include "klee/SolverStats.h" +#include "klee/Solver/IncompleteSolver.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" #include #ifdef _LIBCPP_VERSION diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 5c181dc3..27a165e1 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" @@ -17,8 +17,8 @@ #include "klee/Internal/ADT/MapOfSets.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/SolverImpl.h" -#include "klee/SolverStats.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" #include "klee/TimerStatIncrementer.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index 39e0e824..ed6a77dd 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -10,10 +10,12 @@ /* * This file groups declarations that are common to both KLEE and Kleaver. */ + #include "klee/Common.h" -#include "klee/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/System/Time.h" +#include "klee/Solver/SolverCmdLine.h" + #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index 774f52a7..e22f0471 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -10,11 +10,14 @@ #include "STPSolver.h" #include "Z3Solver.h" #include "MetaSMTSolver.h" -#include "klee/SolverCmdLine.h" + +#include "klee/Solver/SolverCmdLine.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" + #include "llvm/Support/ErrorHandling.h" #include "llvm/Support/raw_ostream.h" + #include namespace klee { diff --git a/lib/Solver/DummySolver.cpp b/lib/Solver/DummySolver.cpp index 39328653..60a4fb51 100644 --- a/lib/Solver/DummySolver.cpp +++ b/lib/Solver/DummySolver.cpp @@ -7,9 +7,9 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" -#include "klee/SolverImpl.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" +#include "klee/Solver/SolverStats.h" namespace klee { diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 9f493cd1..3e1162fd 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -8,14 +8,14 @@ //===----------------------------------------------------------------------===// #define DEBUG_TYPE "cex-solver" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprEvaluator.h" #include "klee/Expr/ExprRangeEvaluator.h" #include "klee/Expr/ExprVisitor.h" -#include "klee/IncompleteSolver.h" +#include "klee/Solver/IncompleteSolver.h" #include "klee/Internal/Support/Debug.h" #include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index e19a71e1..9b57bc6c 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/IncompleteSolver.h" +#include "klee/Solver/IncompleteSolver.h" #include "klee/Expr/Constraints.h" diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 12017e5c..7beb1a7c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -8,14 +8,14 @@ //===----------------------------------------------------------------------===// #define DEBUG_TYPE "independent-solver" -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/Debug.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c4ff1f13..6817c47a 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -16,8 +16,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/ErrorHandling.h" diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h index 9fa93719..89cb7143 100644 --- a/lib/Solver/MetaSMTSolver.h +++ b/lib/Solver/MetaSMTSolver.h @@ -11,7 +11,7 @@ #ifndef KLEE_METASMTSOLVER_H #define KLEE_METASMTSOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 75faf3a3..3c012cc2 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -11,8 +11,8 @@ #ifndef KLEE_QUERYLOGGINGSOLVER_H #define KLEE_QUERYLOGGINGSOLVER_H -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "klee/Internal/System/Time.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 645c8989..ef6697ef 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -11,8 +11,8 @@ #include "STPBuilder.h" #include "klee/Expr/Expr.h" -#include "klee/Solver.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "klee/util/Bits.h" #include "ConstantDivision.h" diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index eb46b6db..ebb67254 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -18,7 +18,7 @@ #include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h index 70b9aa12..494a30db 100644 --- a/lib/Solver/STPSolver.h +++ b/lib/Solver/STPSolver.h @@ -11,7 +11,7 @@ #ifndef KLEE_STPSOLVER_H #define KLEE_STPSOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { /// STPSolver - A complete solver based on STP. diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 6c7361dc..855f7102 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -7,10 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" #include "klee/Expr/Constraints.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/SolverImpl.h" using namespace klee; diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp index 9e190840..87b66317 100644 --- a/lib/Solver/SolverCmdLine.cpp +++ b/lib/Solver/SolverCmdLine.cpp @@ -12,8 +12,9 @@ * data that are common to both KLEE and Kleaver. */ +#include "klee/Solver/SolverCmdLine.h" + #include "klee/Config/Version.h" -#include "klee/SolverCmdLine.h" #include "klee/OptionCategories.h" #include "llvm/ADT/ArrayRef.h" diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp index e8f30c9e..ad5388e5 100644 --- a/lib/Solver/SolverImpl.cpp +++ b/lib/Solver/SolverImpl.cpp @@ -7,8 +7,8 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" using namespace klee; diff --git a/lib/Solver/SolverStats.cpp b/lib/Solver/SolverStats.cpp index efdfe6ed..841bfc60 100644 --- a/lib/Solver/SolverStats.cpp +++ b/lib/Solver/SolverStats.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/SolverStats.h" +#include "klee/Solver/SolverStats.h" using namespace klee; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 71e6834e..93d743db 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -8,8 +8,8 @@ //===----------------------------------------------------------------------===// #include "klee/Expr/Constraints.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 07a7b681..43440fa7 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -12,8 +12,8 @@ #include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/Solver.h" -#include "klee/SolverStats.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverStats.h" #include "klee/util/Bits.h" #include "llvm/ADT/StringExtras.h" diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index cfcb77e7..00777a78 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -20,8 +20,8 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/ExprUtil.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverImpl.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h index bed74b88..9688ccff 100644 --- a/lib/Solver/Z3Solver.h +++ b/lib/Solver/Z3Solver.h @@ -11,7 +11,7 @@ #ifndef KLEE_Z3SOLVER_H #define KLEE_Z3SOLVER_H -#include "klee/Solver.h" +#include "klee/Solver/Solver.h" namespace klee { /// Z3Solver - A complete solver based on Z3 diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index cc292d10..70b51208 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -19,9 +19,9 @@ #include "klee/Expr/Parser/Parser.h" #include "klee/Internal/Support/PrintVersion.h" #include "klee/OptionCategories.h" -#include "klee/Solver.h" -#include "klee/SolverCmdLine.h" -#include "klee/SolverImpl.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverCmdLine.h" +#include "klee/Solver/SolverImpl.h" #include "klee/Statistics.h" #include "llvm/ADT/StringExtras.h" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 09b3dea5..de2989f6 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -22,7 +22,7 @@ #include "klee/Internal/System/Time.h" #include "klee/Interpreter.h" #include "klee/OptionCategories.h" -#include "klee/SolverCmdLine.h" +#include "klee/Solver/SolverCmdLine.h" #include "klee/Statistics.h" #include "llvm/IR/Constants.h" diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index b15fd64b..9c1089e0 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -12,8 +12,8 @@ #include "klee/Expr/ArrayCache.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" -#include "klee/Solver.h" -#include "klee/SolverCmdLine.h" +#include "klee/Solver/Solver.h" +#include "klee/Solver/SolverCmdLine.h" #include "llvm/ADT/StringExtras.h" -- cgit 1.4.1