klee
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

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: