1 #ifndef ROSE_BinaryAnalysis_FeasiblePath_H
2 #define ROSE_BinaryAnalysis_FeasiblePath_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <BaseSemantics2.h>
7 #include <BinarySmtSolver.h>
8 #include <BinarySymbolicExprParser.h>
9 #include <Partitioner2/CfgPath.h>
10 #include <RoseException.h>
11 #include <Sawyer/CommandLine.h>
12 #include <Sawyer/Message.h>
13 #include <boost/filesystem/path.hpp>
14 #include <boost/logic/tribool.hpp>
76 Expression(
const std::string &parsable): parsable(parsable) {}
79 void print(std::ostream&)
const;
115 : check(false), mode(MUST), constOnly(false), minValid(1024) {}
122 : searchMode(
SEARCH_SINGLE_DFS), maxVertexVisit((size_t)-1), maxPathLength(200), maxCallDepth((size_t)-1),
123 maxRecursionDepth((size_t)-1), nonAddressIsFeasible(true), solverName(
"best"),
124 memoryParadigm(
LIST_BASED_MEMORY), processFinalVertex(false), ignoreSemanticFailure(false),
125 kCycleCoefficient(0.0), edgeVisitOrder(
VISIT_NATURAL), trackingCodeCoverage(true), maxExprSize(
UNLIMITED),
126 traceSemantics(false) {}
138 : maxVertexVisitHits(0), maxPathLengthHits(0), maxCallDepthHits(0), maxRecursionDepthHits(0) {}
157 std::string registerName;
166 VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
167 std::string toString()
const;
305 FunctionSummary(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
324 Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;
350 FunctionSummaries functionSummaries_;
355 bool isDirectedSearch_;
372 : registers_(NULL), isDirectedSearch_(true) {}
381 functionSummaries_.clear();
384 pathsBeginVertices_.
clear();
385 pathsEndVertices_.
clear();
386 isDirectedSearch_ =
true;
387 cfgAvoidEdges_.
clear();
388 cfgEndAvoidVertices_.
clear();
443 const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);
459 size_t pathInsnIndex);
467 size_t pathInsnIndex);
474 const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
475 size_t pathInsnIndex);
481 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
504 Partitioner2::ControlFlowGraph::ConstVertexIterator
505 pathToCfg(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex)
const;
521 bool isFunctionCall(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&)
const;
524 void printPathVertex(std::ostream &out,
const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
525 size_t &insnIdx )
const;
537 const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
561 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
562 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
572 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
583 return isDirectedSearch_;
611 return functionSummaries_;
659 void checkSettings()
const;
661 static rose_addr_t virtualAddress(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);
663 void insertCallSummary(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
665 const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);
667 boost::filesystem::path emitPathGraph(
size_t callId,
size_t graphId);
680 SymbolicExpr::Ptr pathEdgeConstraint(
const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
684 Expression parseExpression(Expression,
const std::string &where,
SymbolicExprParser&)
const;
690 const std::vector<Expression> &assertions,
bool atEndOfPath,
const SymbolicExprParser&);
693 static size_t vertexSize(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
696 struct Substitutions {
698 std::vector<Expression> assertions;
707 const Substitutions&,
bool atEndOfPath);
710 void markAsReached(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
719 Substitutions parseSubstitutions();
735 Semantics createSemantics(
const Partitioner2::CfgPath&, PathProcessor&,
const SmtSolverPtr&);
748 size_t incomingStepCount(
const Partitioner2::CfgPath&,
int position);
751 size_t outgoingStepCount(
const Partitioner2::CfgPath&,
int position);
759 boost::logic::tribool isFeasible(Partitioner2::CfgPath&,
const Substitutions&,
const Semantics&,
const SmtSolverPtr&);
766 double adjustEffectiveK(Partitioner2::CfgPath&,
double oldK);
770 void summarizeOrInline(Partitioner2::CfgPath&,
const Semantics&);
780 namespace CommandLine {
std::string firstAccessMode
How was variable first accessed ("read" or "write").
bool traceSemantics
Trace all instruction semantics operations.
size_t maxPathLengthHits
Number of times settings.maxPathLength was hit (effective K).
std::vector< rose_addr_t > summarizeFunctions
Functions to always summarize.
Sawyer::Container::Map< rose_addr_t, FunctionSummary > FunctionSummaries
Summaries for multiple functions.
Perform a breadth first search.
MayOrMust mode
Check for addrs that may or must be null.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
InstructionSemantics2::BaseSemantics::StatePtr initialState() const
Get the initial state before the first path vertex.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
EdgeVisitOrder edgeVisitOrder
Order in which to visit edges.
virtual InstructionSemantics2::SymbolicSemantics::SValuePtr returnValue(const FeasiblePath &analysis, const FunctionSummary &summary, const InstructionSemantics2::SymbolicSemantics::RiscOperatorsPtr &ops)=0
Return value for function.
size_t maxCallDepthHits
Number of times settings.maxCallDepth was hit.
rose_addr_t address
Address of summarized function.
SemanticMemoryParadigm memoryParadigm
Type of memory state when there's a choice to be made.
Perform a depth first search.
bool trackingCodeCoverage
If set, track which block addresses are reached.
static size_t pathLength(const Partitioner2::CfgPath &, int position=-1)
Total length of path up to and including the specified vertex.
const size_t UNLIMITED(-1)
Effictively unlimited size.
double pathEffectiveK(const Partitioner2::CfgPath &) const
Effective maximum path length.
void printPathVertex(std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex, size_t &insnIdx) const
Print one vertex of a path for debugging.
std::string parsable
String to be parsed as an expression.
Information stored per V_USER_DEFINED path vertex.
Sawyer::Container::Map< std::string, FeasiblePath::VarDetail > VarDetails
Variable detail by name.
MayOrMust
Types of comparisons.
void setSearchBoundary(const Partitioner2::Partitioner &partitioner, const Partitioner2::CfgConstVertexSet &cfgBeginVertices, const Partitioner2::CfgConstVertexSet &cfgEndVertices, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
Specify search boundary.
void depthFirstSearch(PathProcessor &pathProcessor)
Find all feasible paths.
virtual void processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex, const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process an indeterminate block.
Base class for machine instructions.
Sawyer::Optional< rose_addr_t > returnFrom
This variable is the return value from the specified function.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
FeasiblePath()
Constructs a new feasible path analyzer.
SearchMode
How to search for paths.
virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary, const InstructionSemantics2::SymbolicSemantics::RiscOperatorsPtr &ops)=0
Invoked when the analysis traverses the summary.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
virtual void processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process a function summary vertex.
Continue along this path.
RegisterDescriptor REG_PATH
Descriptor of path pseudo-registers.
size_t maxRecursionDepthHits
Number of times settings.maxRecursionDepth was hit.
std::string name
Name of summarized function.
Sawyer::Optional< size_t > firstAccessIdx
Instruction position in path where this var was first read.
Settings()
Default settings.
A collection of related switch declarations.
Sawyer::Container::Map< rose_addr_t, size_t > reachedBlockVas
Number of times each basic block was reached.
Sawyer::Optional< boost::chrono::duration< double > > smtTimeout
Max seconds allowed per SMT solve call.
Main namespace for the ROSE library.
Parses symbolic expressions from text.
Satisfiable
Satisfiability constants.
size_t maxCallDepth
Max length of path in terms of function calls.
size_t maxExprSize
Maximum symbolic expression size before replacement.
struct Rose::BinaryAnalysis::FeasiblePath::Settings::NullDeref nullDeref
Settings for null-dereference analysis.
Visit edges in random order.
Blast everything at once to the SMT solver.
Name space for the entire library.
std::vector< std::string > assertionLocations
Locations at which "constraints" are checked.
size_t maxVertexVisitHits
Number of times settings.maxVertexVisit was hit.
const FunctionSummaries & functionSummaries() const
Function summary information.
Sawyer::SharedPointer< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Partitioner2::CfgConstVertexSet cfgToPaths(const Partitioner2::CfgConstVertexSet &) const
Convert CFG vertices to path vertices.
virtual bool shouldInline(const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget)
Determines whether a function call should be inlined.
std::vector< rose_addr_t > ipRewrite
An even number of from,to pairs for rewriting the insn ptr reg.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
static std::string expressionDocumentation()
Documentation for the symbolic expression parser.
void settings(const Settings &s)
Property: Settings used by this analysis.
size_t maxPathLength
Limit path length in terms of number of instructions.
bool constOnly
If true, check only constants or sets of constants.
Base class for callbacks for function summaries.
AddressIntervalSet location
Location where constraint applies.
void clear()
Remove all entries from this container.
Visit edges in reverse of the natural order.
bool isDirectedSearch() const
Property: Whether search is directed or not.
static InstructionSemantics2::BaseSemantics::StatePtr pathPostState(const Partitioner2::CfgPath &, size_t vertexIdx)
Get the state at the end of the specified vertex.
FunctionSummary()
Construct empty function summary.
bool nonAddressIsFeasible
Indeterminate/undiscovered vertices are feasible?
size_t maxVertexVisit
Max times to visit a particular vertex in one path.
Describes (part of) a physical CPU register.
size_t maxRecursionDepth
Max path length in terms of recursive function calls.
void reset()
Reset to initial state without changing settings.
A path through a control flow graph.
rose_addr_t minValid
Minnimum address that is not treated as a null dereference.
Information about a variable seen on a path.
virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, const SmtSolverPtr &solver)
Function invoked whenever a complete path is found.
FunctionSummarizer::Ptr functionSummarizer() const
Property: Function summary handling.
Exception for errors specific to feasible path analysis.
virtual bool shouldSummarizeCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex, const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget)
Determines whether a function call should be summarized instead of inlined.
bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &) const
True if vertex is a function call.
SymbolicExpr::Ptr expr
Symbolic expression.
bool ignoreSemanticFailure
Whether to ignore instructions with no semantic info.
SearchMode searchMode
Method to use when searching for feasible paths.
size_t Id
Attribute identification.
void clear()
Remove all vertices and edges.
bool pathEndsWithFunctionCall(const Partitioner2::CfgPath &) const
True if path ends with a function call.
IoMode
Read or write operation.
void printPath(std::ostream &out, const Partitioner2::CfgPath &) const
Print the path to the specified output stream.
Statistics statistics() const
Cumulative statistics about prior analyses.
void resetStatistics()
Reset only statistics.
std::set< rose_addr_t > AddressSet
Set of basic block addresses.
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr buildVirtualCpu(const Partitioner2::Partitioner &, const Partitioner2::CfgPath *, PathProcessor *, const SmtSolver::Ptr &)
Create the virtual CPU.
const Settings & settings() const
Property: Settings used by this analysis.
size_t memByteNumber
Byte number for memory access.
virtual Action memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &value)
Function invoked every time a memory reference occurs.
int64_t stackDelta
Stack delta for summarized function.
Base class for reference counted objects.
double kCycleCoefficient
Coefficient for adjusting maxPathLengh during CFG cycles.
static Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &settings)
Describe command-line switches.
Sawyer::SharedPointer< FunctionSummarizer > Ptr
Reference counting pointer.
static Sawyer::Message::Facility mlog
Diagnostic output.
bool isAnyEndpointReachable(const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex, const Partitioner2::CfgConstVertexSet &endVertices)
Determine whether any ending vertex is reachable.
const VarDetails & varDetails(const InstructionSemantics2::BaseSemantics::StatePtr &) const
Details about all variables by name.
void clear()
Remove all edges or vertices from this set.
Partitioner2::ControlFlowGraph::ConstVertexIterator pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const
Convert path vertex to a CFG vertex.
virtual void processVertex(const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, size_t pathInsnIndex)
Process one vertex.
Visit edges in their natural, forward order.
const FunctionSummary & functionSummary(rose_addr_t entryVa) const
Function summary information.
const Partitioner2::Partitioner & partitioner() const
Property: Partitioner currently in use.
Converts text to messages.
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for SMT solvers.
Defines registers available for a particular architecture.
const VarDetail & varDetail(const InstructionSemantics2::BaseSemantics::StatePtr &, const std::string &varName) const
Details about a variable.
virtual void processBasicBlock(const Partitioner2::BasicBlock::Ptr &bblock, const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process instructions for one basic block on the specified virtual CPU.
virtual Action nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics2::BaseSemantics::SValuePtr &addr)
Function invoked whenever a null pointer dereference is detected.
Statistics from path searching.
SymbolicExpr::Ptr memAddress
Address where variable is located.
Partitions instructions into basic blocks and functions.
Base class for all ROSE exceptions.
std::string solverName
Type of SMT solver.
Do not continue along this path.
EdgeVisitOrder
Edge visitation order.
void functionSummarizer(const FunctionSummarizer::Ptr &f)
Property: Function summary handling.
Settings & settings()
Property: Settings used by this analysis.
size_t memSize
Size of total memory access in bytes.
std::string exprParserDoc
String documenting how expressions are parsed, empty for default.
bool processFinalVertex
Whether to process the last vertex of the path.
SgAsmInstruction * firstAccessInsn
Instruction address where this var was first read.
Expression to be evaluated.
Settings that control this analysis.
static void initDiagnostics()
Initialize diagnostic output.
bool check
If true, look for null dereferences along the paths.
virtual void setInitialState(const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex)
Initialize state for first vertex of path.
Sawyer::Optional< rose_addr_t > initialStackPtr
Concrete value to use for stack pointer register initial value.
SemanticMemoryParadigm
Organization of semantic memory.
std::vector< Expression > assertions
Constraints to be satisfied at some point along the path.
virtual void init(const FeasiblePath &analysis, FunctionSummary &summary, const Partitioner2::Function::Ptr &function, Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget)=0
Invoked when a new summary is created.