klee
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 ()
 
virtual void setNewline (const std::string &newline)=0
 
virtual void setForceNoLineBreaks (bool forceNoLineBreaks)=0
 
virtual void reset ()=0
 
virtual void scan (const ref< Expr > &e)=0
 
virtual void print (const ref< Expr > &e, unsigned indent=0)=0
 
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 ConstraintSet &constraints)
 
static void printQuery (llvm::raw_ostream &os, const ConstraintSet &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 58 of file ExprPPrinter.cpp.

Constructor & Destructor Documentation

◆ PPrinter()

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

Definition at line 320 of file ExprPPrinter.cpp.

References reset().

Here is the call graph for this function:

Member Function Documentation

◆ hasOrderedReads()

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 241 of file ExprPPrinter.cpp.

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

Referenced by print().

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

◆ hasSimpleKids()

bool PPrinter::hasSimpleKids ( const Expr ep)
inlineprivate

Definition at line 106 of file ExprPPrinter.cpp.

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

Referenced by printExpr().

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

◆ isReadExprAtOffset()

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

Definition at line 216 of file ExprPPrinter.cpp.

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

Referenced by hasOrderedReads().

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

◆ isSimple()

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

Definition at line 91 of file ExprPPrinter.cpp.

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

Referenced by hasSimpleKids().

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

◆ isVerySimple()

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

Definition at line 81 of file ExprPPrinter.cpp.

References bindings.

Referenced by isSimple(), and printRead().

Here is the caller graph for this function:

◆ isVerySimpleUpdate()

bool PPrinter::isVerySimpleUpdate ( const UpdateNode un)
inlineprivate

Definition at line 85 of file ExprPPrinter.cpp.

References updateBindings.

Referenced by isSimple().

Here is the caller graph for this function:

◆ print() [1/2]

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

◆ print() [2/2]

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

Implements klee::ExprPPrinter.

Definition at line 350 of file ExprPPrinter.cpp.

References os, PrintContext::pos, and print().

Referenced by print(), printExpr(), printExtract(), klee::ExprPPrinter::printOne(), klee::ExprPPrinter::printQuery(), printRead(), klee::ExprPPrinter::printSingleExpr(), and printUpdateList().

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

◆ printConst()

void PPrinter::printConst ( const ref< ConstantExpr > &  e,
PrintContext PC,
bool  printWidth 
)
inline

Definition at line 356 of file ExprPPrinter.cpp.

References printWidth().

Referenced by print().

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

◆ printExpr()

void PPrinter::printExpr ( const Expr ep,
PrintContext PC,
unsigned  indent,
bool  printConstWidth = false 
)
inlineprivate

Definition at line 309 of file ExprPPrinter.cpp.

References klee::Expr::getKid(), klee::Expr::getNumKids(), hasSimpleKids(), print(), and printSeparator().

Referenced by print().

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

◆ printExtract()

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

Definition at line 304 of file ExprPPrinter.cpp.

References klee::ExtractExpr::expr, klee::ExtractExpr::offset, and print().

Referenced by print().

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

◆ printRead()

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

Definition at line 298 of file ExprPPrinter.cpp.

References klee::ReadExpr::index, isVerySimple(), print(), printSeparator(), printUpdateList(), and klee::ReadExpr::updates.

Referenced by print().

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

◆ printSeparator()

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

Definition at line 437 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), and forceNoLineBreaks.

Referenced by printExpr(), klee::ExprPPrinter::printQuery(), printRead(), and printUpdateList().

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

◆ printUpdateList()

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

Definition at line 142 of file ExprPPrinter.cpp.

References PrintContext::breakLine(), hasScan, klee::UpdateList::head, klee::Array::name, PrintContext::pos, print(), printSeparator(), klee::UpdateList::root, shouldPrintUpdates, updateBindings, and updateCounter.

Referenced by printRead().

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

◆ printWidth()

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

Definition at line 202 of file ExprPPrinter.cpp.

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

Referenced by print(), and printConst().

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

◆ reset()

void PPrinter::reset ( )
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 332 of file ExprPPrinter.cpp.

References bindings, couldPrint, couldPrintUpdates, counter, forceNoLineBreaks, hasScan, shouldPrint, shouldPrintUpdates, updateBindings, and updateCounter.

Referenced by PPrinter().

Here is the caller graph for this function:

◆ scan()

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

Implements klee::ExprPPrinter.

Definition at line 345 of file ExprPPrinter.cpp.

References hasScan, and scan1().

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

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

◆ scan1()

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

Definition at line 126 of file ExprPPrinter.cpp.

References couldPrint, klee::ref< T >::get(), klee::Expr::getKid(), klee::Expr::getNumKids(), scan1(), scanUpdate(), shouldPrint, and usedArrays.

Referenced by scan(), scan1(), and scanUpdate().

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

◆ scanUpdate()

void PPrinter::scanUpdate ( const UpdateNode un)
inlineprivate

Definition at line 113 of file ExprPPrinter.cpp.

References couldPrintUpdates, klee::UpdateNode::index, klee::UpdateNode::next, scan1(), scanUpdate(), shouldPrintUpdates, and klee::UpdateNode::value.

Referenced by scan1(), and scanUpdate().

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

◆ setForceNoLineBreaks()

void PPrinter::setForceNoLineBreaks ( bool  _forceNoLineBreaks)
inlinevirtual

Implements klee::ExprPPrinter.

Definition at line 328 of file ExprPPrinter.cpp.

References forceNoLineBreaks.

◆ setNewline()

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

Implements klee::ExprPPrinter.

Definition at line 324 of file ExprPPrinter.cpp.

References newline.

◆ shouldPrintWidth()

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

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

Definition at line 75 of file ExprPPrinter.cpp.

References klee::Expr::getWidth().

Referenced by printWidth().

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

Member Data Documentation

◆ bindings

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

Definition at line 62 of file ExprPPrinter.cpp.

Referenced by isVerySimple(), print(), and reset().

◆ couldPrint

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

Definition at line 64 of file ExprPPrinter.cpp.

Referenced by reset(), and scan1().

◆ couldPrintUpdates

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

Definition at line 65 of file ExprPPrinter.cpp.

Referenced by reset(), and scanUpdate().

◆ counter

unsigned PPrinter::counter
private

Definition at line 67 of file ExprPPrinter.cpp.

Referenced by print(), and reset().

◆ forceNoLineBreaks

bool PPrinter::forceNoLineBreaks
private

Definition at line 70 of file ExprPPrinter.cpp.

Referenced by printSeparator(), reset(), and setForceNoLineBreaks().

◆ hasScan

bool PPrinter::hasScan
private

Definition at line 69 of file ExprPPrinter.cpp.

Referenced by print(), printUpdateList(), reset(), and scan().

◆ newline

std::string PPrinter::newline
private

Definition at line 71 of file ExprPPrinter.cpp.

Referenced by setNewline().

◆ os

llvm::raw_ostream& PPrinter::os
private

Definition at line 66 of file ExprPPrinter.cpp.

Referenced by print().

◆ shouldPrint

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

Definition at line 64 of file ExprPPrinter.cpp.

Referenced by print(), reset(), and scan1().

◆ shouldPrintUpdates

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

Definition at line 65 of file ExprPPrinter.cpp.

Referenced by printUpdateList(), reset(), and scanUpdate().

◆ updateBindings

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

Definition at line 63 of file ExprPPrinter.cpp.

Referenced by isVerySimpleUpdate(), printUpdateList(), and reset().

◆ updateCounter

unsigned PPrinter::updateCounter
private

Definition at line 68 of file ExprPPrinter.cpp.

Referenced by printUpdateList(), and reset().

◆ usedArrays

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

Definition at line 60 of file ExprPPrinter.cpp.

Referenced by klee::ExprPPrinter::printQuery(), and scan1().


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