1 #ifndef ROSE_BinaryAnalysis_FeasiblePath_H
2 #define ROSE_BinaryAnalysis_FeasiblePath_H
3 #include <featureTests.h>
6 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics.h>
7 #include <Rose/BinaryAnalysis/SmtSolver.h>
8 #include <Rose/BinaryAnalysis/SymbolicExprParser.h>
9 #include <Rose/BinaryAnalysis/Partitioner2/CfgPath.h>
10 #include <Rose/Exception.h>
11 #include <Sawyer/CommandLine.h>
12 #include <Sawyer/Message.h>
13 #include <boost/filesystem/path.hpp>
14 #include <boost/logic/tribool.hpp>
16 namespace Rose {
17 namespace BinaryAnalysis {
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  };
36  enum SearchMode {
40  };
46  };
53  };
56  enum IoMode { READ, WRITE };
59  enum MayOrMust { MAY, MUST };
62  typedef std::set<rose_addr_t> AddressSet;
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) {}
79  void print(std::ostream&) const;
80  };
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  };
130  struct Statistics {
131  size_t nPathsExplored;
138  Statistics()
139  : nPathsExplored(0), maxVertexVisitHits(0), maxPathLengthHits(0), maxCallDepthHits(0), maxRecursionDepthHits(0) {}
141  Statistics& operator+=(const Statistics&);
142  };
157  struct VarDetail {
158  std::string registerName;
159  std::string firstAccessMode;
163  size_t memSize;
164  size_t memByteNumber;
167  VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
168  std::string toString() const;
169  };
178  public:
179  enum Action {
182  };
184  virtual ~PathProcessor() {}
202  virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
204  const SmtSolverPtr &solver) {
205  return CONTINUE;
206  }
241  virtual Action nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
244  return CONTINUE;
245  }
286  virtual Action memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
290  return CONTINUE;
291  }
292  };
298  rose_addr_t address;
299  int64_t stackDelta;
300  std::string name;
303  FunctionSummary(): stackDelta(SgAsmInstruction::INVALID_STACK_DELTA) {}
306  FunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
307  };
316  public:
319  protected:
320  FunctionSummarizer() {}
321  public:
323  virtual void init(const FeasiblePath &analysis, FunctionSummary &summary /*in,out*/,
324  const Partitioner2::Function::Ptr &function,
325  Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;
331  virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary,
339  returnValue(const FeasiblePath &analysis, const FunctionSummary &summary,
341  };
344  // Private data members
346 private:
347  const Partitioner2::Partitioner *partitioner_; // binary analysis context
348  RegisterDictionary *registers_; // registers augmented with "path" pseudo-register
349  RegisterDescriptor REG_RETURN_; // FIXME[Robb P Matzke 2016-10-11]: see source
350  Settings settings_;
351  FunctionSummaries functionSummaries_;
352  Partitioner2::CfgVertexMap vmap_; // relates CFG vertices to path vertices
353  Partitioner2::ControlFlowGraph paths_; // all possible paths, feasible or otherwise
354  Partitioner2::CfgConstVertexSet pathsBeginVertices_;// vertices of paths_ where searching starts
355  Partitioner2::CfgConstVertexSet pathsEndVertices_; // vertices of paths_ where searching stops
356  bool isDirectedSearch_; // use pathsEndVertices_?
357  Partitioner2::CfgConstEdgeSet cfgAvoidEdges_; // CFG edges to avoid
358  Partitioner2::CfgConstVertexSet cfgEndAvoidVertices_;// CFG end-of-path and other avoidance vertices
359  FunctionSummarizer::Ptr functionSummarizer_; // user-defined function for handling function summaries
360  InstructionSemantics2::BaseSemantics::StatePtr initialState_; // set by setInitialState.
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
365  mutable SAWYER_THREAD_TRAITS::Mutex statsMutex_; // protects the following data member
366  Statistics stats_; // statistical results of the analysis
369  // Construction, destruction
371 public:
374  : registers_(NULL), isDirectedSearch_(true) {}
376  virtual ~FeasiblePath() {}
379  void reset() {
380  partitioner_ = NULL;
381  registers_ = NULL;
382  REG_PATH = REG_RETURN_ = RegisterDescriptor();
383  functionSummaries_.clear();
384  vmap_.clear();
385  paths_.clear();
386  pathsBeginVertices_.clear();
387  pathsEndVertices_.clear();
388  isDirectedSearch_ = true;
389  cfgAvoidEdges_.clear();
390  cfgEndAvoidVertices_.clear();
391  resetStatistics();
392  }
398  SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
399  stats_ = Statistics();
400  }
403  static void initDiagnostics();
407  // Settings affecting behavior
409 public:
413  const Settings& settings() const { return settings_; }
414  Settings& settings() { return settings_; }
415  void settings(const Settings &s) { settings_ = s; }
425  static std::string expressionDocumentation();
429  // Overridable processing functions
431 public:
438  buildVirtualCpu(const Partitioner2::Partitioner&, const Partitioner2::CfgPath*, PathProcessor*, const SmtSolver::Ptr&);
446  virtual void
448  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);
454  virtual void
455  processBasicBlock(const Partitioner2::BasicBlock::Ptr &bblock,
456  const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex);
461  virtual void
462  processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex,
464  size_t pathInsnIndex);
469  virtual void
470  processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
472  size_t pathInsnIndex);
477  virtual void
479  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
480  size_t pathInsnIndex);
483  virtual bool
484  shouldSummarizeCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex,
485  const Partitioner2::ControlFlowGraph &cfg,
486  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
489  virtual bool
490  shouldInline(const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
500  FunctionSummarizer::Ptr functionSummarizer() const { return functionSummarizer_; }
501  void functionSummarizer(const FunctionSummarizer::Ptr &f) { functionSummarizer_ = f; }
504  // Utilities
507 public:
509  Partitioner2::ControlFlowGraph::ConstVertexIterator
510  pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const;
513  Partitioner2::CfgConstVertexSet
514  cfgToPaths(const Partitioner2::CfgConstVertexSet&) const;
519  Partitioner2::CfgConstEdgeSet
520  cfgToPaths(const Partitioner2::CfgConstEdgeSet&) const;
523  bool pathEndsWithFunctionCall(const Partitioner2::CfgPath&) const;
526  bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator&) const;
529  void printPathVertex(std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
530  size_t &insnIdx /*in,out*/) const;
535  void printPath(std::ostream &out, const Partitioner2::CfgPath&) const;
541  bool isAnyEndpointReachable(const Partitioner2::ControlFlowGraph &cfg,
542  const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
543  const Partitioner2::CfgConstVertexSet &endVertices);
546  // Functions for describing the search space
548 public:
558  void
559  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
560  const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
561  const Partitioner2::CfgConstVertexSet &cfgEndVertices,
562  const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
563  const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
564  void
565  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
566  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
567  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
568  const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
569  const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
570  void
571  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
572  const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
573  const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
574  const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
575  void
576  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
577  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
578  const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
579  const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
587  bool isDirectedSearch() const {
588  return isDirectedSearch_;
589  }
592  // Functions for searching for paths
594 public:
599  void depthFirstSearch(PathProcessor &pathProcessor);
603  // Functions for getting the results
605 public:
610  const Partitioner2::Partitioner& partitioner() const;
615  const FunctionSummaries& functionSummaries() const {
616  return functionSummaries_;
617  }
623  const FunctionSummary& functionSummary(rose_addr_t entryVa) const;
626  const VarDetail& varDetail(const InstructionSemantics2::BaseSemantics::StatePtr&, const std::string &varName) const;
629  const VarDetails& varDetails(const InstructionSemantics2::BaseSemantics::StatePtr&) const;
635  static InstructionSemantics2::BaseSemantics::StatePtr pathPostState(const Partitioner2::CfgPath&, size_t vertexIdx);
642  double pathEffectiveK(const Partitioner2::CfgPath&) const;
650  static size_t pathLength(const Partitioner2::CfgPath&, int position = -1);
658  SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
659  return stats_;
660  }
663  // Private supporting functions
665 private:
666  // Check that analysis settings are valid, or throw an exception.
667  void checkSettings() const;
669  static rose_addr_t virtualAddress(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);
671  void insertCallSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
672  const Partitioner2::ControlFlowGraph &cfg,
673  const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);
675  boost::filesystem::path emitPathGraph(size_t callId, size_t graphId); // emit paths graph to "rose-debug" directory
677  // Pop an edge (or more) from the path and follow some other edge. Also, adjust the SMT solver's stack in a similar
678  // way. The SMT solver will have an initial state, plus one pushed state per edge of the path.
679  void backtrack(Partitioner2::CfgPath &path /*in,out*/, const SmtSolver::Ptr&);
681  // Process one edge of a path to find any path constraints. When called, the cpu's current state should be the virtual
682  // machine state at it exists just prior to executing the target vertex of the specified edge.
683  //
684  // Returns a null pointer if the edge's assertion is trivially unsatisfiable, such as when the edge points to a basic block
685  // whose address doesn't match the contents of the instruction pointer register after executing the edge's source
686  // block. Otherwise, returns a symbolic expression which must be tree if the edge is feasible. For trivially feasible
687  // edges, the return value is the constant 1 (one bit wide; i.e., true).
688  SymbolicExpr::Ptr pathEdgeConstraint(const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
691  // Parse the expression if it's a parsable string, otherwise return the expression as is. */
692  Expression parseExpression(Expression, const std::string &where, SymbolicExprParser&) const;
694  SymbolicExpr::Ptr expandExpression(const Expression&, const SymbolicExprParser&);
696  // Based on the last vertex of the path, insert user-specified assertions into the SMT solver.
697  void insertAssertions(const SmtSolver::Ptr&, const Partitioner2::CfgPath&,
698  const std::vector<Expression> &assertions, bool atEndOfPath, const SymbolicExprParser&);
700  // Size of vertex. How much of "k" does this vertex consume?
701  static size_t vertexSize(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
703  // Information needed for adding user-supplied assertions to the solver.
704  struct Substitutions {
705  SymbolicExprParser exprParser;
706  std::vector<Expression> assertions;
709  };
711  // Insert the edge assertion and any applicable user assertions (after delayed expansion of the expressions' register
712  // and memory references), and run the solver, returning its result.
714  solvePathConstraints(const SmtSolver::Ptr&, const Partitioner2::CfgPath&, const SymbolicExpr::Ptr &edgeAssertion,
715  const Substitutions&, bool atEndOfPath);
717  // Mark vertex as being reached
718  void markAsReached(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
720  // Top-level info for debugging
721  void dfsDebugHeader(Sawyer::Message::Stream &trace, Sawyer::Message::Stream &debug, size_t callId, size_t graphId);
723  // Top-level info for debugging a path.
724  void dfsDebugCurrentPath(Sawyer::Message::Stream&, const Partitioner2::CfgPath&, const SmtSolverPtr&, size_t effectiveK);
726  // Prepare substitutions for registers and memory based on user-supplied symbolic expressions.
727  Substitutions parseSubstitutions();
729  // Substitute registers and memory values into user-supplied symbolic expressions.
730  void makeSubstitutions(const Substitutions&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);
732  // Create an SMT solver. It will have an initial state plus, eventually, a transaction for each path edge.
733  SmtSolverPtr createSmtSolver();
735  // The parts of the instruction semantics framework
736  struct Semantics {
740  };
742  // Create the parts of the instruction semantics framework.
743  Semantics createSemantics(const Partitioner2::CfgPath&, PathProcessor&, const SmtSolverPtr&);
745  // Convert a position to an index. Negative positions measure from the end of the sequence so that -1 refers to the last
746  // element, -2 to the second-to-last element, etc. Non-negative positions are the same thing as an index. Returns nothing
747  // if the position is out of range.
748  static Sawyer::Optional<size_t> positionToIndex(int position, size_t nElmts);
750  // Obtain the incoming state for the specified path vertex. This is a pointer to the state, so copy it if you make changes.
751  // The incoming state for the first vertex is the specified initial state.
753  incomingState(const Partitioner2::CfgPath&, int position, const InstructionSemantics2::BaseSemantics::StatePtr &initialState);
755  // Number of steps (e.g., instructions) up to but not including the specified path vertex.
756  size_t incomingStepCount(const Partitioner2::CfgPath&, int position);
758  // Number of steps (e.g., instructions) up to and including the specified path vertex.
759  size_t outgoingStepCount(const Partitioner2::CfgPath&, int position);
761  // Evaluate semantics up to and including the specified path vertex, returning the outgoing state for that vertex. If
762  // semantics fails, then returns a null state pointer.
763  InstructionSemantics2::BaseSemantics::StatePtr evaluate(Partitioner2::CfgPath&, int position, const Semantics&);
765  // Check whether the last vertex of the path is feasible. Returns true if provably feasible, false if provably infeasible,
766  // or indeterminate if not provable one way or the other.
767  boost::logic::tribool isFeasible(Partitioner2::CfgPath&, const Substitutions&, const Semantics&, const SmtSolverPtr&);
769  // Safely call the path processor's "found" action for the path's final vertex and return its value.
770  PathProcessor::Action callPathProcessorFound(PathProcessor&, Partitioner2::CfgPath&, const Semantics&, const SmtSolverPtr&);
772  // Given an effective K value, adjust it based on how often the last vertex of the path has been visited. Returns a new
773  // effective K. As a special case, the new K is zero if the last vertex has been visited too often.
774  double adjustEffectiveK(Partitioner2::CfgPath&, double oldK);
776  // Given a path that ends with a function call, inline the function or a summary of the function, adjusting the paths_
777  // control flow graph.
778  void summarizeOrInline(Partitioner2::CfgPath&, const Semantics&);
779 };
781 } // namespace
782 } // namespace
784 std::ostream& operator<<(std::ostream&, const Rose::BinaryAnalysis::FeasiblePath::Expression&);
786 // Convert string to feasible path expression during command-line parsing
787 namespace Sawyer {
788  namespace CommandLine {
789  template<>
790  struct LexicalCast<Rose::BinaryAnalysis::FeasiblePath::Expression> {
791  static Rose::BinaryAnalysis::FeasiblePath::Expression convert(const std::string &src) {
793  }
794  };
795  }
796 }
798 #endif
799 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
std::string firstAccessMode
How was variable first accessed ("read" or "write").
Definition: FeasiblePath.h:159
bool traceSemantics
Trace all instruction semantics operations.
Definition: FeasiblePath.h:105
size_t maxPathLengthHits
Number of times settings.maxPathLength was hit (effective K).
Definition: FeasiblePath.h:133
std::vector< rose_addr_t > summarizeFunctions
Functions to always summarize.
Definition: FeasiblePath.h:93
Sawyer::Container::Map< rose_addr_t, FunctionSummary > FunctionSummaries
Summaries for multiple functions.
Definition: FeasiblePath.h:310
MayOrMust mode
Check for addrs that may or must be null.
Definition: FeasiblePath.h:110
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.
Definition: SymbolicExpr.h:156
EdgeVisitOrder edgeVisitOrder
Order in which to visit edges.
Definition: FeasiblePath.h:100
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.
Definition: FeasiblePath.h:134
size_t nPathsExplored
Number of paths explored.
Definition: FeasiblePath.h:131
rose_addr_t address
Address of summarized function.
Definition: FeasiblePath.h:298
SemanticMemoryParadigm memoryParadigm
Type of memory state when there's a choice to be made.
Definition: FeasiblePath.h:96
bool trackingCodeCoverage
If set, track which block addresses are reached.
Definition: FeasiblePath.h:101
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.
Definition: FeasiblePath.h:72
Information stored per V_USER_DEFINED path vertex.
Definition: FeasiblePath.h:297
Sawyer::Container::Map< std::string, FeasiblePath::VarDetail > VarDetails
Variable detail by name.
Definition: FeasiblePath.h:172
Types of comparisons.
Definition: FeasiblePath.h:59
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.
Definition: FeasiblePath.h:165
Collection of streams.
Definition: Message.h:1606
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to symbolic RISC operations.
Constructs a new feasible path analyzer.
Definition: FeasiblePath.h:373
How to search for paths.
Definition: FeasiblePath.h:36
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.
Definition: FeasiblePath.h:154
size_t maxRecursionDepthHits
Number of times settings.maxRecursionDepth was hit.
Definition: FeasiblePath.h:135
std::string name
Name of summarized function.
Definition: FeasiblePath.h:300
Sawyer::Optional< size_t > firstAccessIdx
Instruction position in path where this var was first read.
Definition: FeasiblePath.h:161
A collection of related switch declarations.
Sawyer::Container::Map< rose_addr_t, size_t > reachedBlockVas
Number of times each basic block was reached.
Definition: FeasiblePath.h:136
Sawyer::Optional< boost::chrono::duration< double > > smtTimeout
Max seconds allowed per SMT solve call.
Definition: FeasiblePath.h:103
Main namespace for the ROSE library.
Parses symbolic expressions from text.
Satisfiability constants.
Definition: SmtSolver.h:81
size_t maxCallDepth
Max length of path in terms of function calls.
Definition: FeasiblePath.h:89
size_t maxExprSize
Maximum symbolic expression size before replacement.
Definition: FeasiblePath.h:104
struct Rose::BinaryAnalysis::FeasiblePath::Settings::NullDeref nullDeref
Settings for null-dereference analysis.
Blast everything at once to the SMT solver.
Definition: FeasiblePath.h:39
Feasible path analysis.
Definition: FeasiblePath.h:22
Name space for the entire library.
Definition: FeasiblePath.h:787
std::vector< std::string > assertionLocations
Locations at which "constraints" are checked.
Definition: FeasiblePath.h:92
size_t maxVertexVisitHits
Number of times settings.maxVertexVisit was hit.
Definition: FeasiblePath.h:132
const FunctionSummaries & functionSummaries() const
Function summary information.
Definition: FeasiblePath.h:615
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.
Definition: FeasiblePath.h:102
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.
Definition: FeasiblePath.h:415
size_t maxPathLength
Limit path length in terms of number of instructions.
Definition: FeasiblePath.h:88
bool constOnly
If true, check only constants or sets of constants.
Definition: FeasiblePath.h:111
Base class for callbacks for function summaries.
Definition: FeasiblePath.h:315
AddressIntervalSet location
Location where constraint applies.
Definition: FeasiblePath.h:71
Visit edges in reverse of the natural order.
Definition: FeasiblePath.h:51
bool isDirectedSearch() const
Property: Whether search is directed or not.
Definition: FeasiblePath.h:587
static InstructionSemantics2::BaseSemantics::StatePtr pathPostState(const Partitioner2::CfgPath &, size_t vertexIdx)
Get the state at the end of the specified vertex.
Construct empty function summary.
Definition: FeasiblePath.h:303
bool nonAddressIsFeasible
Indeterminate/undiscovered vertices are feasible?
Definition: FeasiblePath.h:94
size_t maxVertexVisit
Max times to visit a particular vertex in one path.
Definition: FeasiblePath.h:87
Describes (part of) a physical CPU register.
size_t maxRecursionDepth
Max path length in terms of recursive function calls.
Definition: FeasiblePath.h:90
void reset()
Reset to initial state without changing settings.
Definition: FeasiblePath.h:379
rose_addr_t minValid
Minnimum address that is not treated as a null dereference.
Definition: FeasiblePath.h:112
Information about a variable seen on a path.
Definition: FeasiblePath.h:157
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.
Definition: FeasiblePath.h:202
FunctionSummarizer::Ptr functionSummarizer() const
Property: Function summary handling.
Definition: FeasiblePath.h:500
Exception for errors specific to feasible path analysis.
Definition: FeasiblePath.h:28
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.
Definition: FeasiblePath.h:73
bool ignoreSemanticFailure
Whether to ignore instructions with no semantic info.
Definition: FeasiblePath.h:98
SearchMode searchMode
Method to use when searching for feasible paths.
Definition: FeasiblePath.h:85
size_t Id
Attribute identification.
Definition: Attribute.h:140
bool pathEndsWithFunctionCall(const Partitioner2::CfgPath &) const
True if path ends with a function call.
Read or write operation.
Definition: FeasiblePath.h:56
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.
Definition: FeasiblePath.h:657
void resetStatistics()
Reset only statistics.
Definition: FeasiblePath.h:397
std::set< rose_addr_t > AddressSet
Set of basic block addresses.
Definition: FeasiblePath.h:62
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.
Definition: FeasiblePath.h:413
size_t memByteNumber
Byte number for memory access.
Definition: FeasiblePath.h:164
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.
Definition: FeasiblePath.h:286
int64_t stackDelta
Stack delta for summarized function.
Definition: FeasiblePath.h:299
Base class for reference counted objects.
Definition: SharedObject.h:64
double kCycleCoefficient
Coefficient for adjusting maxPathLengh during CFG cycles.
Definition: FeasiblePath.h:99
static Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &settings)
Describe command-line switches.
Sawyer::SharedPointer< FunctionSummarizer > Ptr
Reference counting pointer.
Definition: FeasiblePath.h:318
static Sawyer::Message::Facility mlog
Diagnostic output.
Definition: FeasiblePath.h:145
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.
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.
Definition: FeasiblePath.h:50
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
Defines registers available for a particular architecture.
Definition: Registers.h:37
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.
Definition: FeasiblePath.h:241
Statistics from path searching.
Definition: FeasiblePath.h:130
SymbolicExpr::Ptr memAddress
Address where variable is located.
Definition: FeasiblePath.h:162
Base class for all ROSE exceptions.
Definition: Rose/Exception.h:9
std::string solverName
Type of SMT solver.
Definition: FeasiblePath.h:95
Edge visitation order.
Definition: FeasiblePath.h:49
void functionSummarizer(const FunctionSummarizer::Ptr &f)
Property: Function summary handling.
Definition: FeasiblePath.h:501
Settings & settings()
Property: Settings used by this analysis.
Definition: FeasiblePath.h:414
size_t memSize
Size of total memory access in bytes.
Definition: FeasiblePath.h:163
std::string exprParserDoc
String documenting how expressions are parsed, empty for default.
Definition: FeasiblePath.h:118
bool processFinalVertex
Whether to process the last vertex of the path.
Definition: FeasiblePath.h:97
SgAsmInstruction * firstAccessInsn
Instruction address where this var was first read.
Definition: FeasiblePath.h:160
Settings that control this analysis.
Definition: FeasiblePath.h:83
static void initDiagnostics()
Initialize diagnostic output.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:25
bool check
If true, look for null dereferences along the paths.
Definition: FeasiblePath.h:109
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.
Definition: FeasiblePath.h:86
Organization of semantic memory.
Definition: FeasiblePath.h:43
std::vector< Expression > assertions
Constraints to be satisfied at some point along the path.
Definition: FeasiblePath.h:91
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.