klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
FastCexSolver.cpp File Reference
#include "klee/Solver.h"
#include "klee/Constraints.h"
#include "klee/Expr.h"
#include "klee/IncompleteSolver.h"
#include "klee/util/ExprEvaluator.h"
#include "klee/util/ExprRangeEvaluator.h"
#include "klee/util/ExprVisitor.h"
#include "klee/Internal/Support/IntEvaluation.h"
#include "llvm/Support/Debug.h"
#include "llvm/Support/raw_ostream.h"
#include <sstream>
#include <cassert>
#include <map>
#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

#define DEBUG_TYPE   "cex-solver"

Definition at line 21 of file FastCexSolver.cpp.

Typedef Documentation

Definition at line 295 of file FastCexSolver.cpp.

Function Documentation

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

Definition at line 81 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryAnd().

Here is the caller graph for this function:

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

Definition at line 50 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryOr().

Here is the caller graph for this function:

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

Definition at line 66 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryAnd().

Here is the caller graph for this function:

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

Definition at line 34 of file FastCexSolver.cpp.

Referenced by ValueRange::binaryOr().

Here is the caller graph for this function:

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

Definition at line 288 of file FastCexSolver.cpp.

References ValueRange::print().

Here is the call graph for this function:

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 999 of file FastCexSolver.cpp.

References klee::ConstraintManager::begin(), klee::Query::constraints, CexData::dump(), klee::ConstraintManager::end(), 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: