FastCexSolver.cpp File Reference

#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/Solver/IncompleteSolver.h"
#include "klee/Support/Debug.h"
#include "klee/Support/IntEvaluation.h"
#include "llvm/Support/raw_ostream.h"
#include <cassert>
#include <map>
#include <sstream>
#include <vector>

Include dependency graph for FastCexSolver.cpp:

Go to the source code of this file.

Classes
class	ValueRange
class	CexObjectData
class	CexRangeEvaluator
class	CexPossibleEvaluator
class	CexExactEvaluator
class	CexData
class	FastCexSolver

Macros
#define	DEBUG_TYPE   "cex-solver"

Typedefs
typedef ValueRange	CexValueData

Functions
static uint64_t	minOR (uint64_t a, uint64_t b, uint64_t c, uint64_t d)
static uint64_t	maxOR (uint64_t a, uint64_t b, uint64_t c, uint64_t d)
static uint64_t	minAND (uint64_t a, uint64_t b, uint64_t c, uint64_t d)
static uint64_t	maxAND (uint64_t a, uint64_t b, uint64_t c, uint64_t d)
llvm::raw_ostream &	operator<< (llvm::raw_ostream &os, const ValueRange &vr)
static bool	propogateValues (const Query &query, CexData &cd, bool checkExpr, bool &isValid)

Macro Definition Documentation

DEBUG_TYPE

#define DEBUG_TYPE   "cex-solver"

Definition at line 10 of file FastCexSolver.cpp.

Typedef Documentation

CexValueData

typedef ValueRange CexValueData

Definition at line 303 of file FastCexSolver.cpp.

Function Documentation

maxAND()

static uint64_t maxAND ( uint64_t  a, uint64_t  b, uint64_t  c, uint64_t  d  )

static

Definition at line 79 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryAnd().

Here is the caller graph for this function:

maxOR()

static uint64_t maxOR ( uint64_t  a, uint64_t  b, uint64_t  c, uint64_t  d  )

static

Definition at line 48 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryOr().

Here is the caller graph for this function:

minAND()

static uint64_t minAND ( uint64_t  a, uint64_t  b, uint64_t  c, uint64_t  d  )

static

Definition at line 64 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryAnd().

Here is the caller graph for this function:

minOR()

static uint64_t minOR ( uint64_t  a, uint64_t  b, uint64_t  c, uint64_t  d  )

static

Definition at line 32 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryOr().

Here is the caller graph for this function:

operator<<()

llvm::raw_ostream & operator<< ( llvm::raw_ostream &  os, const ValueRange &  vr  )

inline

Definition at line 296 of file FastCexSolver.cpp.

References ValueRange::print().

Here is the call graph for this function:

propogateValues()

static bool propogateValues ( const Query &  query, CexData &  cd, bool  checkExpr, bool &  isValid  )

static

propogateValues - Propogate value ranges for the given query and return the propogation results.

Parameters

query	- The query to propogate values for.
cd	- The initial object values resulting from the propogation.
checkExpr	- Include the query expression in the constraints to propogate.
isValid	- If the propogation succeeds (returns true), whether the constraints were proven valid or invalid.

Returns

- True if the propogation was able to prove validity or invalidity.

Definition at line 1008 of file FastCexSolver.cpp.

References klee::Query::constraints, CexData::dump(), CexData::evaluateExact(), CexData::evaluatePossible(), klee::Query::expr, klee::Expr::isFalse(), klee::Expr::isTrue(), CexData::propogateExactValue(), and CexData::propogatePossibleValue().

Referenced by FastCexSolver::computeInitialValues(), FastCexSolver::computeTruth(), and FastCexSolver::computeValue().

Here is the call graph for this function:

Here is the caller graph for this function: