ROSE  0.11.23.0
BinaryFeasiblePath.h
1 #ifndef ROSE_BinaryAnalysis_FeasiblePath_H
2 #define ROSE_BinaryAnalysis_FeasiblePath_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
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>
15 
16 namespace Rose {
17 namespace BinaryAnalysis {
18 
22 class FeasiblePath {
24  // Types and public data members
26 public:
28  class Exception: public Rose::Exception {
29  public:
30  Exception(const std::string &what)
31  : Rose::Exception(what) {}
32  ~Exception() throw () {}
33  };
34 
36  enum SearchMode {
40  };
41 
46  };
47 
53  };
54 
56  enum IoMode { READ, WRITE };
57 
59  enum MayOrMust { MAY, MUST };
60 
62  typedef std::set<rose_addr_t> AddressSet;
63 
70  struct Expression {
72  std::string parsable;
75  Expression() {}
76  /*implicit*/ Expression(const std::string &parsable): parsable(parsable) {}
77  /*implicit*/ Expression(const SymbolicExpr::Ptr &expr): expr(expr) {}
78 
79  void print(std::ostream&) const;
80  };
81 
83  struct Settings {
84  // Path feasibility
87  size_t maxVertexVisit;
88  size_t maxPathLength;
89  size_t maxCallDepth;
91  std::vector<Expression> assertions;
92  std::vector<std::string> assertionLocations;
93  std::vector<rose_addr_t> summarizeFunctions;
95  std::string solverName;
102  std::vector<rose_addr_t> ipRewrite;
104  size_t maxExprSize;
107  // Null dereferences
108  struct NullDeref {
109  bool check;
111  bool constOnly;
112  rose_addr_t minValid;
114  NullDeref()
115  : check(false), mode(MUST), constOnly(false), minValid(1024) {}
116  } nullDeref;
118  std::string exprParserDoc;
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) {}
127  };
128 
130  struct Statistics {
137  Statistics()
138  : maxVertexVisitHits(0), maxPathLengthHits(0), maxCallDepthHits(0), maxRecursionDepthHits(0) {}
139 
140  Statistics& operator+=(const Statistics&);
141  };
142 
145 
154 
156  struct VarDetail {
157  std::string registerName;
158  std::string firstAccessMode;
162  size_t memSize;
163  size_t memByteNumber;
166  VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
167  std::string toString() const;
168  };
169 
172 
177  public:
178  enum Action {
181  };
182 
183  virtual ~PathProcessor() {}
184 
201  virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
203  const SmtSolverPtr &solver) {
204  return CONTINUE;
205  }
206 
240  virtual Action nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
243  return CONTINUE;
244  }
245 
285  virtual Action memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
289  return CONTINUE;
290  }
291  };
292 
297  rose_addr_t address;
298  int64_t stackDelta;
299  std::string name;
302  FunctionSummary(): stackDelta(SgAsmInstruction::INVALID_STACK_DELTA) {}
303 
305  FunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
306  };
307 
310 
315  public:
318  protected:
319  FunctionSummarizer() {}
320  public:
322  virtual void init(const FeasiblePath &analysis, FunctionSummary &summary /*in,out*/,
323  const Partitioner2::Function::Ptr &function,
324  Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;
325 
330  virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary,
332 
338  returnValue(const FeasiblePath &analysis, const FunctionSummary &summary,
340  };
341 
343  // Private data members
345 private:
346  const Partitioner2::Partitioner *partitioner_; // binary analysis context
347  RegisterDictionary *registers_; // registers augmented with "path" pseudo-register
348  RegisterDescriptor REG_RETURN_; // FIXME[Robb P Matzke 2016-10-11]: see source
349  Settings settings_;
350  FunctionSummaries functionSummaries_;
351  Partitioner2::CfgVertexMap vmap_; // relates CFG vertices to path vertices
352  Partitioner2::ControlFlowGraph paths_; // all possible paths, feasible or otherwise
353  Partitioner2::CfgConstVertexSet pathsBeginVertices_;// vertices of paths_ where searching starts
354  Partitioner2::CfgConstVertexSet pathsEndVertices_; // vertices of paths_ where searching stops
355  bool isDirectedSearch_; // use pathsEndVertices_?
356  Partitioner2::CfgConstEdgeSet cfgAvoidEdges_; // CFG edges to avoid
357  Partitioner2::CfgConstVertexSet cfgEndAvoidVertices_;// CFG end-of-path and other avoidance vertices
358  FunctionSummarizer::Ptr functionSummarizer_; // user-defined function for handling function summaries
359  InstructionSemantics2::BaseSemantics::StatePtr initialState_; // set by setInitialState.
360  Statistics stats_; // statistical results of the analysis
361  static Sawyer::Attribute::Id POST_STATE; // stores semantic state after executing the insns for a vertex
362  static Sawyer::Attribute::Id POST_INSN_LENGTH; // path length in instructions at end of vertex
363  static Sawyer::Attribute::Id EFFECTIVE_K; // (double) effective maximimum path length
364 
365 
367  // Construction, destruction
369 public:
372  : registers_(NULL), isDirectedSearch_(true) {}
373 
374  virtual ~FeasiblePath() {}
375 
377  void reset() {
378  partitioner_ = NULL;
379  registers_ = NULL;
380  REG_PATH = REG_RETURN_ = RegisterDescriptor();
381  functionSummaries_.clear();
382  vmap_.clear();
383  paths_.clear();
384  pathsBeginVertices_.clear();
385  pathsEndVertices_.clear();
386  isDirectedSearch_ = true;
387  cfgAvoidEdges_.clear();
388  cfgEndAvoidVertices_.clear();
389  resetStatistics();
390  }
391 
394  stats_ = Statistics();
395  }
396 
398  static void initDiagnostics();
399 
400 
402  // Settings affecting behavior
404 public:
408  const Settings& settings() const { return settings_; }
409  Settings& settings() { return settings_; }
410  void settings(const Settings &s) { settings_ = s; }
418 
420  static std::string expressionDocumentation();
421 
422 
424  // Overridable processing functions
426 public:
433  buildVirtualCpu(const Partitioner2::Partitioner&, const Partitioner2::CfgPath*, PathProcessor*, const SmtSolver::Ptr&);
434 
441  virtual void
443  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);
444 
449  virtual void
451  const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex);
452 
456  virtual void
457  processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex,
459  size_t pathInsnIndex);
460 
464  virtual void
465  processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
467  size_t pathInsnIndex);
468 
472  virtual void
474  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
475  size_t pathInsnIndex);
476 
478  virtual bool
479  shouldSummarizeCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex,
481  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
482 
484  virtual bool
485  shouldInline(const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
486 
495  FunctionSummarizer::Ptr functionSummarizer() const { return functionSummarizer_; }
496  void functionSummarizer(const FunctionSummarizer::Ptr &f) { functionSummarizer_ = f; }
499  // Utilities
502 public:
504  Partitioner2::ControlFlowGraph::ConstVertexIterator
505  pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const;
506 
510 
516 
519 
521  bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator&) const;
522 
524  void printPathVertex(std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
525  size_t &insnIdx /*in,out*/) const;
526 
530  void printPath(std::ostream &out, const Partitioner2::CfgPath&) const;
531 
537  const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
538  const Partitioner2::CfgConstVertexSet &endVertices);
539 
541  // Functions for describing the search space
543 public:
544 
553  void
555  const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
556  const Partitioner2::CfgConstVertexSet &cfgEndVertices,
559  void
560  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
561  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
562  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
565  void
566  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
567  const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
570  void
571  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
572  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
582  bool isDirectedSearch() const {
583  return isDirectedSearch_;
584  }
585 
587  // Functions for searching for paths
589 public:
594  void depthFirstSearch(PathProcessor &pathProcessor);
595 
596 
598  // Functions for getting the results
600 public:
605  const Partitioner2::Partitioner& partitioner() const;
606 
610  const FunctionSummaries& functionSummaries() const {
611  return functionSummaries_;
612  }
613 
618  const FunctionSummary& functionSummary(rose_addr_t entryVa) const;
619 
621  const VarDetail& varDetail(const InstructionSemantics2::BaseSemantics::StatePtr&, const std::string &varName) const;
622 
624  const VarDetails& varDetails(const InstructionSemantics2::BaseSemantics::StatePtr&) const;
625 
628 
631 
637  double pathEffectiveK(const Partitioner2::CfgPath&) const;
638 
645  static size_t pathLength(const Partitioner2::CfgPath&, int position = -1);
646 
651  return stats_;
652  }
653 
655  // Private supporting functions
657 private:
658  // Check that analysis settings are valid, or throw an exception.
659  void checkSettings() const;
660 
661  static rose_addr_t virtualAddress(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);
662 
663  void insertCallSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
665  const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);
666 
667  boost::filesystem::path emitPathGraph(size_t callId, size_t graphId); // emit paths graph to "rose-debug" directory
668 
669  // Pop an edge (or more) from the path and follow some other edge. Also, adjust the SMT solver's stack in a similar
670  // way. The SMT solver will have an initial state, plus one pushed state per edge of the path.
671  void backtrack(Partitioner2::CfgPath &path /*in,out*/, const SmtSolver::Ptr&);
672 
673  // Process one edge of a path to find any path constraints. When called, the cpu's current state should be the virtual
674  // machine state at it exists just prior to executing the target vertex of the specified edge.
675  //
676  // Returns a null pointer if the edge's assertion is trivially unsatisfiable, such as when the edge points to a basic block
677  // whose address doesn't match the contents of the instruction pointer register after executing the edge's source
678  // block. Otherwise, returns a symbolic expression which must be tree if the edge is feasible. For trivially feasible
679  // edges, the return value is the constant 1 (one bit wide; i.e., true).
680  SymbolicExpr::Ptr pathEdgeConstraint(const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
682 
683  // Parse the expression if it's a parsable string, otherwise return the expression as is. */
684  Expression parseExpression(Expression, const std::string &where, SymbolicExprParser&) const;
685 
686  SymbolicExpr::Ptr expandExpression(const Expression&, const SymbolicExprParser&);
687 
688  // Based on the last vertex of the path, insert user-specified assertions into the SMT solver.
689  void insertAssertions(const SmtSolver::Ptr&, const Partitioner2::CfgPath&,
690  const std::vector<Expression> &assertions, bool atEndOfPath, const SymbolicExprParser&);
691 
692  // Size of vertex. How much of "k" does this vertex consume?
693  static size_t vertexSize(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
694 
695  // Information needed for adding user-supplied assertions to the solver.
696  struct Substitutions {
697  SymbolicExprParser exprParser;
698  std::vector<Expression> assertions;
701  };
702 
703  // Insert the edge assertion and any applicable user assertions (after delayed expansion of the expressions' register
704  // and memory references), and run the solver, returning its result.
706  solvePathConstraints(const SmtSolver::Ptr&, const Partitioner2::CfgPath&, const SymbolicExpr::Ptr &edgeAssertion,
707  const Substitutions&, bool atEndOfPath);
708 
709  // Mark vertex as being reached
710  void markAsReached(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
711 
712  // Top-level info for debugging
713  void dfsDebugHeader(Sawyer::Message::Stream &trace, Sawyer::Message::Stream &debug, size_t callId, size_t graphId);
714 
715  // Top-level info for debugging a path.
716  void dfsDebugCurrentPath(Sawyer::Message::Stream&, const Partitioner2::CfgPath&, const SmtSolverPtr&, size_t effectiveK);
717 
718  // Prepare substitutions for registers and memory based on user-supplied symbolic expressions.
719  Substitutions parseSubstitutions();
720 
721  // Substitute registers and memory values into user-supplied symbolic expressions.
722  void makeSubstitutions(const Substitutions&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);
723 
724  // Create an SMT solver. It will have an initial state plus, eventually, a transaction for each path edge.
725  SmtSolverPtr createSmtSolver();
726 
727  // The parts of the instruction semantics framework
728  struct Semantics {
732  };
733 
734  // Create the parts of the instruction semantics framework.
735  Semantics createSemantics(const Partitioner2::CfgPath&, PathProcessor&, const SmtSolverPtr&);
736 
737  // Convert a position to an index. Negative positions measure from the end of the sequence so that -1 refers to the last
738  // element, -2 to the second-to-last element, etc. Non-negative positions are the same thing as an index. Returns nothing
739  // if the position is out of range.
740  static Sawyer::Optional<size_t> positionToIndex(int position, size_t nElmts);
741 
742  // Obtain the incoming state for the specified path vertex. This is a pointer to the state, so copy it if you make changes.
743  // The incoming state for the first vertex is the specified initial state.
745  incomingState(const Partitioner2::CfgPath&, int position, const InstructionSemantics2::BaseSemantics::StatePtr &initialState);
746 
747  // Number of steps (e.g., instructions) up to but not including the specified path vertex.
748  size_t incomingStepCount(const Partitioner2::CfgPath&, int position);
749 
750  // Number of steps (e.g., instructions) up to and including the specified path vertex.
751  size_t outgoingStepCount(const Partitioner2::CfgPath&, int position);
752 
753  // Evaluate semantics up to and including the specified path vertex, returning the outgoing state for that vertex. If
754  // semantics fails, then returns a null state pointer.
755  InstructionSemantics2::BaseSemantics::StatePtr evaluate(Partitioner2::CfgPath&, int position, const Semantics&);
756 
757  // Check whether the last vertex of the path is feasible. Returns true if provably feasible, false if provably infeasible,
758  // or indeterminate if not provable one way or the other.
759  boost::logic::tribool isFeasible(Partitioner2::CfgPath&, const Substitutions&, const Semantics&, const SmtSolverPtr&);
760 
761  // Safely call the path processor's "found" action for the path's final vertex and return its value.
762  PathProcessor::Action callPathProcessorFound(PathProcessor&, Partitioner2::CfgPath&, const Semantics&, const SmtSolverPtr&);
763 
764  // Given an effective K value, adjust it based on how often the last vertex of the path has been visited. Returns a new
765  // effective K. As a special case, the new K is zero if the last vertex has been visited too often.
766  double adjustEffectiveK(Partitioner2::CfgPath&, double oldK);
767 
768  // Given a path that ends with a function call, inline the function or a summary of the function, adjusting the paths_
769  // control flow graph.
770  void summarizeOrInline(Partitioner2::CfgPath&, const Semantics&);
771 };
772 
773 } // namespace
774 } // namespace
775 
776 std::ostream& operator<<(std::ostream&, const Rose::BinaryAnalysis::FeasiblePath::Expression&);
777 
778 // Convert string to feasible path expression during command-line parsing
779 namespace Sawyer {
780  namespace CommandLine {
781  template<>
782  struct LexicalCast<Rose::BinaryAnalysis::FeasiblePath::Expression> {
783  static Rose::BinaryAnalysis::FeasiblePath::Expression convert(const std::string &src) {
785  }
786  };
787  }
788 }
789 
790 #endif
791 #endif
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.
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.
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.
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.
Collection of streams.
Definition: Message.h:1599
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.
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.
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.
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.
Definition: CfgPath.h:18
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.
Definition: Attribute.h:140
void clear()
Remove all vertices and edges.
Definition: Graph.h:1978
bool pathEndsWithFunctionCall(const Partitioner2::CfgPath &) const
True if path ends with a function call.
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.
Definition: SharedObject.h:64
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.
Definition: Message.h:1396
Sawyer::SharedPointer< SmtSolver > Ptr
Reference counting pointer for SMT solvers.
Defines registers available for a particular architecture.
Definition: Registers.h:38
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.
SymbolicExpr::Ptr memAddress
Address where variable is located.
Partitions instructions into basic blocks and functions.
Definition: Partitioner.h:322
Base class for all ROSE exceptions.
Definition: RoseException.h:9
std::string solverName
Type of SMT solver.
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.
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.