klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
PPrinter Class Reference
Inheritance diagram for PPrinter:
Collaboration diagram for PPrinter:

Public Member Functions

 PPrinter (llvm::raw_ostream &_os)
 
void setNewline (const std::string &_newline)
 
void setForceNoLineBreaks (bool _forceNoLineBreaks)
 
void reset ()
 
void scan (const ref< Expr > &e)
 
void print (const ref< Expr > &e, unsigned level=0)
 
void printConst (const ref< ConstantExpr > &e, PrintContext &PC, bool printWidth)
 
void print (const ref< Expr > &e, PrintContext &PC, bool printConstWidth=false)
 
void printSeparator (PrintContext &PC, bool simple, unsigned indent)
 
- Public Member Functions inherited from klee::ExprPPrinter
virtual ~ExprPPrinter ()
 
template<class Container >
void scan (Container c)
 
template<class InputIterator >
void scan (InputIterator it, InputIterator end)
 

Public Attributes

std::set< const Array * > usedArrays
 

Private Member Functions

bool shouldPrintWidth (ref< Expr > e)
 
bool isVerySimple (const ref< Expr > &e)
 
bool isVerySimpleUpdate (const UpdateNode *un)
 
bool isSimple (const ref< Expr > &e)
 
bool hasSimpleKids (const Expr *ep)
 
void scanUpdate (const UpdateNode *un)
 
void scan1 (const ref< Expr > &e)
 
void printUpdateList (const UpdateList &updates, PrintContext &PC)
 
void printWidth (PrintContext &PC, ref< Expr > e)
 
bool isReadExprAtOffset (ref< Expr > e, const ReadExpr *base, ref< Expr > offset)
 
const ReadExprhasOrderedReads (ref< Expr > e, int stride)
 
void printRead (const ReadExpr *re, PrintContext &PC, unsigned indent)
 
void printExtract (const ExtractExpr *ee, PrintContext &PC, unsigned indent)
 
void printExpr (const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false)
 

Private Attributes

std::map< ref< Expr >, unsigned > bindings
 
std::map< const UpdateNode
*, unsigned > 
updateBindings
 
std::set< ref< Expr > > couldPrint
 
std::set< ref< Expr > > shouldPrint
 
std::set< const UpdateNode * > couldPrintUpdates
 
std::set< const UpdateNode * > shouldPrintUpdates
 
llvm::raw_ostream & os
 
unsigned counter
 
unsigned updateCounter
 
bool hasScan
 
bool forceNoLineBreaks
 
std::string newline
 

Additional Inherited Members

- Static Public Member Functions inherited from klee::ExprPPrinter
static ExprPPrintercreate (llvm::raw_ostream &os)
 
static void printOne (llvm::raw_ostream &os, const char *message, const ref< Expr > &e)
 
static void printSingleExpr (llvm::raw_ostream &os, const ref< Expr > &e)
 
static void printConstraints (llvm::raw_ostream &os, const ConstraintManager &constraints)
 
static void printQuery (llvm::raw_ostream &os, const ConstraintManager &constraints, const ref< Expr > &q, const ref< Expr > *evalExprsBegin=0, const ref< Expr > *evalExprsEnd=0, const Array *const *evalArraysBegin=0, const Array *const *evalArraysEnd=0, bool printArrayDecls=true)
 
- Protected Member Functions inherited from klee::ExprPPrinter
 ExprPPrinter ()
 

Detailed Description

Definition at line 40 of file ExprPPrinter.cpp.

Constructor & Destructor Documentation

PPrinter::PPrinter ( llvm::raw_ostream &  _os)
inline

Definition at line 301 of file ExprPPrinter.cpp.

Member Function Documentation

const ReadExpr* PPrinter::hasOrderedReads ( ref< Expr e,
int  stride 
)
inlineprivate

hasOrderedReads:

  • e must be a ConcatExpr,
  • stride must be 1 or -1.

If all children of this Concat are reads or concats of reads with consecutive offsets according to the given

  • stride, it returns the base ReadExpr according to
  • stride: first Read for 1 (MSB), last Read for -1 (LSB). Otherwise, it returns null.

Definition at line 222 of file ExprPPrinter.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Concat, klee::ConstantExpr::create(), klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getWidth(), klee::ReadExpr::getWidth(), klee::ReadExpr::index, and klee::Expr::Int8.

Here is the call graph for this function:

bool PPrinter::hasSimpleKids ( const Expr ep)
inlineprivate

Definition at line 87 of file ExprPPrinter.cpp.

References klee::Expr::getKid(), and klee::Expr::getNumKids().

Here is the call graph for this function:

bool PPrinter::isReadExprAtOffset ( ref< Expr e,
const ReadExpr base,
ref< Expr offset 
)
inlineprivate

Definition at line 197 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::ReadExpr::getWidth(), klee::ReadExpr::index, and klee::Expr::Int8.

Here is the call graph for this function:

bool PPrinter::isSimple ( const ref< Expr > &  e)
inlineprivate

Definition at line 73 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::Expr::getKid(), and klee::Expr::getNumKids().

Here is the call graph for this function:

bool PPrinter::isVerySimple ( const ref< Expr > &  e)
inlineprivate

Definition at line 63 of file ExprPPrinter.cpp.

bool PPrinter::isVerySimpleUpdate ( const UpdateNode un)
inlineprivate

Definition at line 67 of file ExprPPrinter.cpp.

void PPrinter::print ( const ref< Expr > &  e,
unsigned  level = 0 
)
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 331 of file ExprPPrinter.cpp.

References PrintContext::pos.

Referenced by klee::ExprPPrinter::printOne(), klee::ExprPPrinter::printQuery(), and klee::ExprPPrinter::printSingleExpr().

Here is the caller graph for this function:

void PPrinter::print ( const ref< Expr > &  e,
PrintContext PC,
bool  printConstWidth = false 
)
inline

Definition at line 361 of file ExprPPrinter.cpp.

References klee::Expr::Concat, klee::ref< T >::get(), klee::Expr::getKind(), PrintContext::pos, and klee::Expr::SExt.

Here is the call graph for this function:

void PPrinter::printConst ( const ref< ConstantExpr > &  e,
PrintContext PC,
bool  printWidth 
)
inline
void PPrinter::printExpr ( const Expr ep,
PrintContext PC,
unsigned  indent,
bool  printConstWidth = false 
)
inlineprivate

Definition at line 290 of file ExprPPrinter.cpp.

References klee::Expr::getKid(), and klee::Expr::getNumKids().

Here is the call graph for this function:

void PPrinter::printExtract ( const ExtractExpr ee,
PrintContext PC,
unsigned  indent 
)
inlineprivate

Definition at line 285 of file ExprPPrinter.cpp.

References klee::ExtractExpr::expr, and klee::ExtractExpr::offset.

void PPrinter::printRead ( const ReadExpr re,
PrintContext PC,
unsigned  indent 
)
inlineprivate

Definition at line 279 of file ExprPPrinter.cpp.

References klee::ReadExpr::index, and klee::ReadExpr::updates.

void PPrinter::printSeparator ( PrintContext PC,
bool  simple,
unsigned  indent 
)
inline

Definition at line 418 of file ExprPPrinter.cpp.

References PrintContext::breakLine().

Referenced by klee::ExprPPrinter::printQuery().

Here is the call graph for this function:

Here is the caller graph for this function:

void PPrinter::printUpdateList ( const UpdateList updates,
PrintContext PC 
)
inlineprivate

Definition at line 123 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), klee::UpdateList::head, klee::Array::name, klee::UpdateNode::next, PrintContext::pos, and klee::UpdateList::root.

Here is the call graph for this function:

void PPrinter::printWidth ( PrintContext PC,
ref< Expr e 
)
inlineprivate

Definition at line 183 of file ExprPPrinter.cpp.

References klee::Expr::getWidth().

Here is the call graph for this function:

void PPrinter::reset ( )
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 313 of file ExprPPrinter.cpp.

void PPrinter::scan ( const ref< Expr > &  e)
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 326 of file ExprPPrinter.cpp.

Referenced by klee::ExprPPrinter::printOne(), klee::ExprPPrinter::printQuery(), and klee::ExprPPrinter::printSingleExpr().

Here is the caller graph for this function:

void PPrinter::scan1 ( const ref< Expr > &  e)
inlineprivate

Definition at line 107 of file ExprPPrinter.cpp.

References klee::ref< T >::get(), klee::Expr::getKid(), and klee::Expr::getNumKids().

Here is the call graph for this function:

void PPrinter::scanUpdate ( const UpdateNode un)
inlineprivate
void PPrinter::setForceNoLineBreaks ( bool  _forceNoLineBreaks)
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 309 of file ExprPPrinter.cpp.

void PPrinter::setNewline ( const std::string &  _newline)
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 305 of file ExprPPrinter.cpp.

bool PPrinter::shouldPrintWidth ( ref< Expr e)
inlineprivate

shouldPrintWidth - Predicate for whether this expression should be printed with its width.

Definition at line 57 of file ExprPPrinter.cpp.

References klee::Expr::Bool, and klee::Expr::getWidth().

Here is the call graph for this function:

Member Data Documentation

std::map<ref<Expr>, unsigned> PPrinter::bindings
private

Definition at line 44 of file ExprPPrinter.cpp.

std::set< ref<Expr> > PPrinter::couldPrint
private

Definition at line 46 of file ExprPPrinter.cpp.

std::set<const UpdateNode*> PPrinter::couldPrintUpdates
private

Definition at line 47 of file ExprPPrinter.cpp.

unsigned PPrinter::counter
private

Definition at line 49 of file ExprPPrinter.cpp.

bool PPrinter::forceNoLineBreaks
private

Definition at line 52 of file ExprPPrinter.cpp.

bool PPrinter::hasScan
private

Definition at line 51 of file ExprPPrinter.cpp.

std::string PPrinter::newline
private

Definition at line 53 of file ExprPPrinter.cpp.

llvm::raw_ostream& PPrinter::os
private

Definition at line 48 of file ExprPPrinter.cpp.

std::set< ref<Expr> > PPrinter::shouldPrint
private

Definition at line 46 of file ExprPPrinter.cpp.

std::set<const UpdateNode*> PPrinter::shouldPrintUpdates
private

Definition at line 47 of file ExprPPrinter.cpp.

std::map<const UpdateNode*, unsigned> PPrinter::updateBindings
private

Definition at line 45 of file ExprPPrinter.cpp.

unsigned PPrinter::updateCounter
private

Definition at line 50 of file ExprPPrinter.cpp.

std::set<const Array*> PPrinter::usedArrays

Definition at line 42 of file ExprPPrinter.cpp.

Referenced by klee::ExprPPrinter::printQuery().


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