1 #ifndef ROSE_BinaryAnalysis_FeasiblePath_H
2 #define ROSE_BinaryAnalysis_FeasiblePath_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/BasicTypes.h>
7 #include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
8 #include <Rose/BinaryAnalysis/SmtSolver.h>
9 #include <Rose/BinaryAnalysis/SymbolicExpressionParser.h>
10 #include <Rose/BinaryAnalysis/Partitioner2/CfgPath.h>
11 #include <Rose/Exception.h>
12 #include <Sawyer/CommandLine.h>
13 #include <Sawyer/Message.h>
14 #include <boost/filesystem/path.hpp>
15 #include <boost/logic/tribool.hpp>
18 namespace BinaryAnalysis {
77 Expression(
const std::string &parsable): parsable(parsable) {}
80 void print(std::ostream&)
const;
116 : check(false), mode(MUST), constOnly(false), minValid(1024) {}
123 : searchMode(
SEARCH_SINGLE_DFS), maxVertexVisit((size_t)-1), maxPathLength(200), maxCallDepth((size_t)-1),
124 maxRecursionDepth((size_t)-1), nonAddressIsFeasible(true), solverName(
"best"),
125 memoryParadigm(
LIST_BASED_MEMORY), processFinalVertex(false), ignoreSemanticFailure(false),
126 kCycleCoefficient(0.0), edgeVisitOrder(
VISIT_NATURAL), trackingCodeCoverage(true), maxExprSize(
UNLIMITED),
127 traceSemantics(false) {}
140 : nPathsExplored(0), maxVertexVisitHits(0), maxPathLengthHits(0), maxCallDepthHits(0), maxRecursionDepthHits(0) {}
159 std::string registerName;
168 VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
169 std::string toString()
const;
301 FunctionSummary(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
320 Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;
346 FunctionSummaries functionSummaries_;
351 bool isDirectedSearch_ =
true;
360 mutable SAWYER_THREAD_TRAITS::Mutex statsMutex_;
378 SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
428 const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);
444 size_t pathInsnIndex);
452 size_t pathInsnIndex);
459 const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
460 size_t pathInsnIndex);
466 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
489 Partitioner2::ControlFlowGraph::ConstVertexIterator
490 pathToCfg(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex)
const;
506 bool isFunctionCall(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&)
const;
509 void printPathVertex(std::ostream &out,
const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
510 size_t &insnIdx )
const;
522 const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
546 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
547 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
557 const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
568 return isDirectedSearch_;
596 return functionSummaries_;
638 SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
647 void checkSettings()
const;
649 static rose_addr_t virtualAddress(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);
651 void insertCallSummary(
const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
653 const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);
655 boost::filesystem::path emitPathGraph(
size_t callId,
size_t graphId);
668 SymbolicExpressionPtr pathEdgeConstraint(
const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
681 static size_t vertexSize(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
684 struct Substitutions {
686 std::vector<Expression> assertions;
694 solvePathConstraints(
const SmtSolverPtr&,
const Partitioner2::CfgPath&,
const SymbolicExpressionPtr &edgeAssertion,
695 const Substitutions&,
bool atEndOfPath);
698 void markAsReached(
const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
707 Substitutions parseSubstitutions();
723 Semantics createSemantics(
const Partitioner2::CfgPath&, PathProcessor&,
const SmtSolverPtr&);
736 size_t incomingStepCount(
const Partitioner2::CfgPath&,
int position);
739 size_t outgoingStepCount(
const Partitioner2::CfgPath&,
int position);
747 boost::logic::tribool isFeasible(Partitioner2::CfgPath&,
const Substitutions&,
const Semantics&,
const SmtSolverPtr&);
754 double adjustEffectiveK(Partitioner2::CfgPath&,
double oldK);
758 void summarizeOrInline(Partitioner2::CfgPath&,
const Semantics&);
768 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.
EdgeVisitOrder edgeVisitOrder
Order in which to visit edges.
size_t maxCallDepthHits
Number of times settings.maxCallDepth was hit.
size_t nPathsExplored
Number of paths explored.
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.
virtual void setInitialState(const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex)
Initialize state for first vertex of path.
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.
InstructionSemantics::BaseSemantics::StatePtr initialState() const
Get the initial state before the first path vertex.
SymbolicExpressionPtr expr
Symbolic expression.
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.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
void depthFirstSearch(PathProcessor &pathProcessor)
Find all feasible paths.
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.
static InstructionSemantics::BaseSemantics::StatePtr pathPostState(const Partitioner2::CfgPath &, size_t vertexIdx)
Get the state at the end of the specified vertex.
virtual void processVertex(const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, size_t pathInsnIndex)
Process one vertex.
Continue along this path.
const VarDetails & varDetails(const InstructionSemantics::BaseSemantics::StatePtr &) const
Details about all variables by name.
RegisterDescriptor REG_PATH
Descriptor of path pseudo-registers.
virtual Action nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics::BaseSemantics::SValuePtr &addr)
Function invoked whenever a null pointer dereference is detected.
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.
SymbolicExpressionPtr memAddress
Address where variable is located.
Main namespace for the ROSE library.
const size_t UNLIMITED(static_cast< size_t >(-1))
Effictively unlimited size.
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.
virtual void processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process a function summary vertex.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
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.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
static const int64_t INVALID_STACK_DELTA
Represents an invalid stack delta.
const FunctionSummaries & functionSummaries() const
Function summary information.
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.
virtual InstructionSemantics::BaseSemantics::DispatcherPtr buildVirtualCpu(const Partitioner2::PartitionerConstPtr &, const Partitioner2::CfgPath *, PathProcessor *, const SmtSolverPtr &)
Create the virtual CPU.
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.
void setSearchBoundary(const Partitioner2::PartitionerConstPtr &partitioner, const Partitioner2::CfgConstVertexSet &cfgBeginVertices, const Partitioner2::CfgConstVertexSet &cfgEndVertices, const Partitioner2::CfgConstVertexSet &cfgAvoidVertices=Partitioner2::CfgConstVertexSet(), const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges=Partitioner2::CfgConstEdgeSet())
Specify search boundary.
AddressIntervalSet location
Location where constraint applies.
virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, const SmtSolverPtr &solver)
Function invoked whenever a complete path is found.
Visit edges in reverse of the natural order.
bool isDirectedSearch() const
Property: Whether search is directed or not.
virtual Action memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics::BaseSemantics::SValuePtr &addr, const InstructionSemantics::BaseSemantics::SValuePtr &value)
Function invoked every time a memory reference occurs.
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.
virtual void processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process an indeterminate block.
rose_addr_t minValid
Minnimum address that is not treated as a null dereference.
Information about a variable seen on a path.
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.
Partitioner2::PartitionerConstPtr partitioner() const
Property: Partitioner currently in use.
bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &) const
True if vertex is a function call.
bool ignoreSemanticFailure
Whether to ignore instructions with no semantic info.
const VarDetail & varDetail(const InstructionSemantics::BaseSemantics::StatePtr &, const std::string &varName) const
Details about a variable.
SearchMode searchMode
Method to use when searching for feasible paths.
size_t Id
Attribute identification.
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.
Parses symbolic expressions from text.
const Settings & settings() const
Property: Settings used by this analysis.
size_t memByteNumber
Byte number for memory access.
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.
virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary, const InstructionSemantics::SymbolicSemantics::RiscOperatorsPtr &ops)=0
Invoked when the analysis traverses the summary.
bool isAnyEndpointReachable(const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex, const Partitioner2::CfgConstVertexSet &endVertices)
Determine whether any ending vertex is reachable.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Partitioner2::ControlFlowGraph::ConstVertexIterator pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const
Convert path vertex to a CFG vertex.
Visit edges in their natural, forward order.
virtual InstructionSemantics::SymbolicSemantics::SValuePtr returnValue(const FeasiblePath &analysis, const FunctionSummary &summary, const InstructionSemantics::SymbolicSemantics::RiscOperatorsPtr &ops)=0
Return value for function.
const FunctionSummary & functionSummary(rose_addr_t entryVa) const
Function summary information.
Converts text to messages.
virtual void init(const FeasiblePath &analysis, FunctionSummary &summary, const Partitioner2::FunctionPtr &function, Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget)=0
Invoked when a new summary is created.
Statistics from path searching.
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.
virtual void processBasicBlock(const Partitioner2::BasicBlockPtr &bblock, const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex)
Process instructions for one basic block on the specified virtual CPU.
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.
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.