klee
Public Member Functions | Private Member Functions | Private Attributes | List of all members
klee::ExprOptimizer Class Reference

#include <ArrayExprOptimizer.h>

Collaboration diagram for klee::ExprOptimizer:
Collaboration graph
[legend]

Public Member Functions

ref< Expr > optimizeExpr (const ref< Expr > &e, bool valueOnly)
 

Private Member Functions

bool computeIndexes (array2idx_ty &arrays, const ref< Expr > &e, mapIndexOptimizedExpr_ty &idx_valIdx) const
 
ref< Expr > getSelectOptExpr (const ref< Expr > &e, std::vector< const ReadExpr * > &reads, std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > &readInfo, bool isSymbolic)
 
ref< Expr > buildConstantSelectExpr (const ref< Expr > &index, std::vector< uint64_t > &arrayValues, Expr::Width width, unsigned elementsInArray) const
 
ref< Expr > buildMixedSelectExpr (const ReadExpr *re, std::vector< std::pair< uint64_t, bool > > &arrayValues, Expr::Width width, unsigned elementsInArray) const
 

Private Attributes

ExprHashMap< ref< Expr > > cacheExprOptimized
 
ExprHashSet cacheExprUnapplicable
 
ExprHashMap< ref< Expr > > cacheReadExprOptimized
 

Detailed Description

Definition at line 31 of file ArrayExprOptimizer.h.

Member Function Documentation

◆ buildConstantSelectExpr()

ref< Expr > ExprOptimizer::buildConstantSelectExpr ( const ref< Expr > &  index,
std::vector< uint64_t > &  arrayValues,
Expr::Width  width,
unsigned  elementsInArray 
) const
private

Definition at line 432 of file ArrayExprOptimizer.cpp.

References klee::ExtractExpr::alloc(), klee::ArrayValueRatio(), klee::ExprBuilder::Constant(), klee::SelectExpr::create(), klee::createDefaultExprBuilder(), klee::Expr::getWidth(), and klee::Expr::Int32.

Referenced by getSelectOptExpr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ buildMixedSelectExpr()

ref< Expr > ExprOptimizer::buildMixedSelectExpr ( const ReadExpr *  re,
std::vector< std::pair< uint64_t, bool > > &  arrayValues,
Expr::Width  width,
unsigned  elementsInArray 
) const
private

Definition at line 573 of file ArrayExprOptimizer.cpp.

References klee::ArrayValueRatio(), klee::ExprBuilder::Constant(), klee::SelectExpr::create(), klee::ConstantExpr::create(), klee::createDefaultExprBuilder(), extendRead(), klee::Expr::getWidth(), klee::ReadExpr::index, and klee::ReadExpr::updates.

Referenced by getSelectOptExpr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ computeIndexes()

bool ExprOptimizer::computeIndexes ( array2idx_ty &  arrays,
const ref< Expr > &  e,
mapIndexOptimizedExpr_ty &  idx_valIdx 
) const
private

Definition at line 191 of file ArrayExprOptimizer.cpp.

References klee::ConstantExpr::alloc(), klee::Array::constantValues, klee::AssignmentGenerator::generatePartialAssignment(), klee::Array::getDomain(), klee::IndexTransformationExprVisitor::getMul(), klee::IndexTransformationExprVisitor::getWidth(), klee::Array::isConstantArray(), klee::Expr::isTrue(), klee::Array::range, and klee::ExprVisitor::visit().

Referenced by optimizeExpr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getSelectOptExpr()

ref< Expr > ExprOptimizer::getSelectOptExpr ( const ref< Expr > &  e,
std::vector< const ReadExpr * > &  reads,
std::map< const ReadExpr *, std::pair< ref< Expr >, Expr::Width > > &  readInfo,
bool  isSymbolic 
)
private

Definition at line 251 of file ArrayExprOptimizer.cpp.

References klee::ArrayValueSymbRatio(), buildConstantSelectExpr(), buildMixedSelectExpr(), cacheReadExprOptimized, klee::ConstantExpr::create(), klee::BitArray::get(), klee::UpdateNode::index, klee::Expr::Int8, klee::UpdateNode::next, klee::BitArray::set(), klee::BitArray::unset(), klee::UpdateNode::value, and klee::ExprVisitor::visit().

Referenced by optimizeExpr().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ optimizeExpr()

ref< Expr > ExprOptimizer::optimizeExpr ( const ref< Expr > &  e,
bool  valueOnly 
)

Returns the optimised version of e.

Parameters
eexpression to optimise
valueOnlyXXX document
Returns
optimised expression

Definition at line 103 of file ArrayExprOptimizer.cpp.

References klee::ALL, klee::Expr::Bool, cacheExprOptimized, cacheExprUnapplicable, computeIndexes(), klee::ArrayReadExprVisitor::containsSymbolic(), klee::ConstantExpr::create(), klee::ExprRewriter::createOptExpr(), getSelectOptExpr(), klee::INDEX, klee::ConstantArrayExprVisitor::isIncompatible(), klee::ArrayReadExprVisitor::isIncompatible(), klee::klee_warning(), klee::NONE, klee::OptimizeArray(), klee::VALUE, and klee::ExprVisitor::visit().

Referenced by klee::Executor::callExternalFunction(), klee::Executor::executeAlloc(), klee::Executor::executeFree(), klee::Executor::executeGetValue(), klee::Executor::executeInstruction(), klee::Executor::executeMemoryOperation(), klee::Executor::resolveExact(), and klee::Executor::toUnique().

Here is the call graph for this function:
Here is the caller graph for this function:

Member Data Documentation

◆ cacheExprOptimized

ExprHashMap<ref<Expr> > klee::ExprOptimizer::cacheExprOptimized
private

Definition at line 33 of file ArrayExprOptimizer.h.

Referenced by optimizeExpr().

◆ cacheExprUnapplicable

ExprHashSet klee::ExprOptimizer::cacheExprUnapplicable
private

Definition at line 34 of file ArrayExprOptimizer.h.

Referenced by optimizeExpr().

◆ cacheReadExprOptimized

ExprHashMap<ref<Expr> > klee::ExprOptimizer::cacheReadExprOptimized
private

Definition at line 35 of file ArrayExprOptimizer.h.

Referenced by getSelectOptExpr().

The documentation for this class was generated from the following files: