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 ----- 13 files changed, 633 insertions(+), 633 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 (limited to 'include') 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 */ -- cgit 1.4.1