Inheritance diagram for SailfishStateBuilder:
Collaboration diagram for SailfishStateBuilder:
Public Member Functions | |
| SailfishStateBuilder (SMTFactory &Fcty, TSDataLayout &D, ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec) | |
| void | pushState () |
| void | popState () |
| void | resetState () |
| void | recordState (const SEGObject *O) |
| void | recordState (const std::shared_ptr< VulnerabilityTrace > &T) |
| void | recordState (const SMTExpr &E) |
| void | recordState (const SMTExprVec &EV) |
| void | recordState (const SummaryCacheItem &SCI, bool Sym) |
| bool | hasState (const SEGObject *O) const |
| std::vector< SummaryCacheItem >::const_iterator | sym_dep_begin () const |
| std::vector< SummaryCacheItem >::const_iterator | sym_dep_end () const |
| std::vector< SummaryCacheItem >::const_iterator | nonsym_dep_begin () const |
| std::vector< SummaryCacheItem >::const_iterator | nonsym_dep_end () const |
 Public Member Functions inherited from SymbolicExprGraphSolver | |
| SymbolicExprGraphSolver (SMTFactory &Fcty, TSDataLayout &D, ExternalMemorySpec *MemSepc, ExternalIOSpec *IOSpec) | |
| SMTExprVec | getCtrlDeps (const SEGNodeBase *N, void *Args=nullptr) |
| Get the condition of paths reaching node n. | |
| virtual SMTExprVec | getCtrlDeps (WrappedBasicBlock *B, const SymbolicExprGraph *G, void *Args=nullptr) |
| Get the condition of paths reaching the block B. | |
| virtual std::pair< SMTExprVec, SMTExprVec > | getCtrlDepsPair (WrappedBasicBlock *B, const SymbolicExprGraph *G, void *Args=nullptr) |
| virtual SMTExprVec | getDataDeps (const SEGNodeBase *N, void *Args=nullptr) |
| Model node n's data dependence. | |
| virtual SMTExprVec | getPhiGated (const SEGPhiNode *PhiNode, const SEGPhiNode::IncomeNode InNode, void *Args=nullptr) |
| SMTExprVec | getPhiGated (const SEGPhiNode *PhiNode, const SEGNodeBase *Value, WrappedBasicBlock *BB, void *Args=nullptr) |
| SMTExprVec | getPhiGated (const SEGPhiNode *PhiNode, const SEGNodeBase *Value, void *Args=nullptr) |
| virtual SMTExprVec | getDeps (const SEGNodeBase *N, const SEGNodeBase *M) |
| virtual std::pair< SMTExprVec, SMTExprVec > | getDepsPair (const SEGNodeBase *N, const SEGNodeBase *M) |
| virtual void | push () |
| virtual void | pop (unsigned N=1) |
| virtual void | reset () |
| virtual SMTResultType | check () |
| const std::unordered_set< const SEGArgumentNode * > & | getUsedFunctionArguments () |
| std::pair< std::vector< const SEGCallSiteOutputNode * >::iterator, std::vector< const SEGCallSiteOutputNode * >::iterator > | getUsedCallSiteOutputs (bool Restart=false) |
| const SEGNodeBase * | getNodeFromSymbol (std::string Symbol) |
| return the SEG node for the given symbol | |
| SMTExpr | getOrInsertExpr (const SEGNodeBase *N) |
| SMTExpr | encodeOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeBinaryOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeCompareOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeCastOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeGEPOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeExtractElementOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeInsertElementOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeSelectOpcodeNode (const SEGOpcodeNode *N) |
| virtual SMTExpr | encodeConcatOpcodeNode (const SEGOpcodeNode *N) |
Additional Inherited Members | |
| Protected Attributes inherited from SymbolicExprGraphSolver | |
| std::unordered_map< const SEGNodeBase *, SMTExpr > | NodeExprMap |
| each node in seg is a z3 variable | |
| std::unordered_map< std::string, const SEGNodeBase * > | NodeSymbolNameMap |
| map the symbol name used by Z3 in context ctx to the SEG node | |
| TSDataLayout & | DL |
| ExternalMemorySpec * | MemSpec = nullptr |
| ExternalIOSpec * | IOSpec = nullptr |
| PushPopCache< const SEGNodeBase * > | ConstraintCache |
| PushPopCache< WrappedBasicBlock * > | BBCache |
The documentation for this class was generated from the following file:
- /builds/prismers/clearblue/include/Checker/Sailfish/SailfishStateBuilder.h
