ROSE  0.9.12.19
BinaryFeasiblePath.h
1 #ifndef ROSE_BinaryAnalysis_FeasiblePath_H
2 #define ROSE_BinaryAnalysis_FeasiblePath_H
3 
4 #include <BaseSemantics2.h>
5 #include <BinarySmtSolver.h>
6 #include <BinarySymbolicExprParser.h>
7 #include <Partitioner2/CfgPath.h>
8 #include <RoseException.h>
9 #include <Sawyer/CommandLine.h>
10 #include <Sawyer/Message.h>
11 #include <boost/filesystem/path.hpp>
12 
13 namespace Rose {
14 namespace BinaryAnalysis {
15 
19 class FeasiblePath {
21  // Types and public data members
23 public:
25  class Exception: public Rose::Exception {
26  public:
27  Exception(const std::string &what)
28  : Rose::Exception(what) {}
29  ~Exception() throw () {}
30  };
31 
33  enum SearchMode {
37  };
38 
43  };
44 
50  };
51 
53  enum IoMode { READ, WRITE };
54 
56  enum MayOrMust { MAY, MUST };
57 
59  typedef std::set<rose_addr_t> AddressSet;
60 
67  struct Expression {
69  std::string parsable;
72  Expression() {}
73  /*implicit*/ Expression(const std::string &parsable): parsable(parsable) {}
74  /*implicit*/ Expression(const SymbolicExpr::Ptr &expr): expr(expr) {}
75 
76  void print(std::ostream&) const;
77  };
78 
80  struct Settings {
81  // Path feasibility
84  size_t maxVertexVisit;
85  size_t maxPathLength;
86  size_t maxCallDepth;
88  std::vector<Expression> assertions;
89  std::vector<std::string> assertionLocations;
90  std::vector<rose_addr_t> summarizeFunctions;
92  std::string solverName;
99  std::vector<rose_addr_t> ipRewrite;
101  // Null dereferences
102  struct NullDeref {
103  bool check;
105  bool constOnly;
107  NullDeref()
108  : check(false), mode(MUST), constOnly(false) {}
109  } nullDeref;
111  std::string exprParserDoc;
115  : searchMode(SEARCH_SINGLE_DFS), maxVertexVisit((size_t)-1), maxPathLength(200), maxCallDepth((size_t)-1),
116  maxRecursionDepth((size_t)-1), nonAddressIsFeasible(true), solverName("best"),
117  memoryParadigm(LIST_BASED_MEMORY), processFinalVertex(false), ignoreSemanticFailure(false),
118  kCycleCoefficient(0.0), edgeVisitOrder(VISIT_NATURAL), trackingCodeCoverage(true) {}
119  };
120 
122  static Sawyer::Message::Facility mlog;
123 
132 
134  struct VarDetail {
135  std::string registerName;
136  std::string firstAccessMode;
140  size_t memSize;
141  size_t memByteNumber;
144  VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
145  std::string toString() const;
146  };
147 
150 
155  public:
156  enum Action {
159  };
160 
161  virtual ~PathProcessor() {}
162 
177  virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
179  const SmtSolverPtr &solver) { return CONTINUE; }
180 
192  virtual void nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
193  const SmtSolverPtr &solver, IoMode ioMode,
195 
200  virtual void memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
201  const SmtSolverPtr &solver, IoMode ioMode,
205  };
206 
211  rose_addr_t address;
212  int64_t stackDelta;
213  std::string name;
216  FunctionSummary(): stackDelta(SgAsmInstruction::INVALID_STACK_DELTA) {}
217 
219  FunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
220  };
221 
224 
229  public:
232  protected:
233  FunctionSummarizer() {}
234  public:
236  virtual void init(const FeasiblePath &analysis, FunctionSummary &summary /*in,out*/,
237  const Partitioner2::Function::Ptr &function,
238  Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;
239 
244  virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary,
246 
252  returnValue(const FeasiblePath &analysis, const FunctionSummary &summary,
254  };
255 
257  // Private data members
259 private:
260  const Partitioner2::Partitioner *partitioner_; // binary analysis context
261  RegisterDictionary *registers_; // registers augmented with "path" pseudo-register
262  RegisterDescriptor REG_RETURN_; // FIXME[Robb P Matzke 2016-10-11]: see source
263  Settings settings_;
264  FunctionSummaries functionSummaries_;
265  Partitioner2::CfgVertexMap vmap_; // relates CFG vertices to path vertices
266  Partitioner2::ControlFlowGraph paths_; // all possible paths, feasible or otherwise
267  Partitioner2::CfgConstVertexSet pathsBeginVertices_;// vertices of paths_ where searching starts
268  Partitioner2::CfgConstVertexSet pathsEndVertices_; // vertices of paths_ where searching stops
269  Partitioner2::CfgConstEdgeSet cfgAvoidEdges_; // CFG edges to avoid
270  Partitioner2::CfgConstVertexSet cfgEndAvoidVertices_;// CFG end-of-path and other avoidance vertices
271  FunctionSummarizer::Ptr functionSummarizer_; // user-defined function for handling function summaries
272  AddressSet reachedBlockVas_; // basic block addresses reached during analysis
273  static Sawyer::Attribute::Id POST_STATE; // stores semantic state after executing the insns for a vertex
274  static Sawyer::Attribute::Id POST_INSN_LENGTH; // path length in instructions at end of vertex
275  static Sawyer::Attribute::Id EFFECTIVE_K; // (double) effective maximimum path length
276 
277 
279  // Construction, destruction
281 public:
284  : registers_(NULL) {}
285 
286  virtual ~FeasiblePath() {}
287 
289  void reset() {
290  partitioner_ = NULL;
291  registers_ = NULL;
292  REG_PATH = REG_RETURN_ = RegisterDescriptor();
293  functionSummaries_.clear();
294  vmap_.clear();
295  paths_.clear();
296  pathsBeginVertices_.clear();
297  pathsEndVertices_.clear();
298  cfgAvoidEdges_.clear();
299  cfgEndAvoidVertices_.clear();
300  reachedBlockVas_.clear();
301  }
302 
304  static void initDiagnostics();
305 
306 
308  // Settings affecting behavior
310 public:
314  const Settings& settings() const { return settings_; }
315  Settings& settings() { return settings_; }
316  void settings(const Settings &s) { settings_ = s; }
324 
326  static std::string expressionDocumentation();
327 
328 
330  // Overridable processing functions
332 public:
339  buildVirtualCpu(const Partitioner2::Partitioner&, const Partitioner2::CfgPath*, PathProcessor*, const SmtSolver::Ptr&);
340 
347  virtual void
349  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);
350 
355  virtual void
357  const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex);
358 
362  virtual void
363  processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex,
365  size_t pathInsnIndex);
366 
370  virtual void
371  processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
373  size_t pathInsnIndex);
374 
378  virtual void
380  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
381  size_t &pathInsnIndex /*in,out*/);
382 
384  virtual bool
385  shouldSummarizeCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex,
387  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
388 
390  virtual bool
391  shouldInline(const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);
392 
401  FunctionSummarizer::Ptr functionSummarizer() const { return functionSummarizer_; }
402  void functionSummarizer(const FunctionSummarizer::Ptr &f) { functionSummarizer_ = f; }
405  // Utilities
408 public:
410  Partitioner2::ControlFlowGraph::ConstVertexIterator
411  pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const;
412 
416 
419 
421  bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator&) const;
422 
424  void printPathVertex(std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
425  size_t &insnIdx /*in,out*/) const;
426 
430  void printPath(std::ostream &out, const Partitioner2::CfgPath&) const;
431 
436  const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
437  const Partitioner2::CfgConstVertexSet &endVertices);
438 
440  // Functions for describing the search space
442 public:
443 
450  void
452  const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
453  const Partitioner2::CfgConstVertexSet &cfgEndVertices,
456  void
457  setSearchBoundary(const Partitioner2::Partitioner &partitioner,
458  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
459  const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
465  // Functions for searching for paths
468 public:
473  void depthFirstSearch(PathProcessor &pathProcessor);
474 
475 
477  // Functions for getting the results
479 public:
484  const Partitioner2::Partitioner& partitioner() const;
485 
489  const FunctionSummaries& functionSummaries() const {
490  return functionSummaries_;
491  }
492 
497  const FunctionSummary& functionSummary(rose_addr_t entryVa) const;
498 
500  const VarDetail& varDetail(const InstructionSemantics2::BaseSemantics::StatePtr&, const std::string &varName) const;
501 
503  const VarDetails& varDetails(const InstructionSemantics2::BaseSemantics::StatePtr&) const;
504 
507 
513  double pathEffectiveK(const Partitioner2::CfgPath&) const;
514 
521  static size_t pathLength(const Partitioner2::CfgPath&);
522 
524  // Functions for code coverage
526 public:
531  const AddressSet& reachedBlockVas() const;
532 
534  // Private supporting functions
536 private:
537  // Check that analysis settings are valid, or throw an exception.
538  void checkSettings() const;
539 
540  static rose_addr_t virtualAddress(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);
541 
542  void insertCallSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
544  const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);
545 
546  boost::filesystem::path emitPathGraph(size_t callId, size_t graphId); // emit paths graph to "rose-debug" directory
547 
548  // Pop an edge (or more) from the path and follow some other edge. Also, adjust the SMT solver's stack in a similar
549  // way. The SMT solver will have an initial state, plus one pushed state per edge of the path.
550  void backtrack(Partitioner2::CfgPath &path /*in,out*/, const SmtSolver::Ptr&);
551 
552  // Process one edge of a path to find any path constraints. When called, the cpu's current state should be the virtual
553  // machine state at it exists just prior to executing the target vertex of the specified edge.
554  //
555  // Returns a null pointer if the edge's assertion is trivially unsatisfiable, such as when the edge points to a basic block
556  // whose address doesn't match the contents of the instruction pointer register after executing the edge's source
557  // block. Otherwise, returns a symbolic expression which must be tree if the edge is feasible. For trivially feasible
558  // edges, the return value is the constant 1 (one bit wide; i.e., true).
559  SymbolicExpr::Ptr pathEdgeConstraint(const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
561 
562  // Parse the expression if it's a parsable string, otherwise return the expression as is. */
563  Expression parseExpression(Expression, const std::string &where, SymbolicExprParser&) const;
564 
565  SymbolicExpr::Ptr expandExpression(const Expression&, SymbolicExprParser&);
566 
567  // Based on the last vertex of the path, insert user-specified assertions into the SMT solver.
568  void insertAssertions(const SmtSolver::Ptr&, const Partitioner2::CfgPath&,
569  const std::vector<Expression> &assertions, bool atEndOfPath, SymbolicExprParser&);
570 
571  // Size of vertex. How much of "k" does this vertex consume?
572  static size_t vertexSize(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
573 
574  // Insert the edge assertion and any applicable user assertions (after delayed expansion of the expressions' register
575  // and memory references), and run the solver, returning its result.
577  solvePathConstraints(SmtSolver::Ptr&, const Partitioner2::CfgPath&, const SymbolicExpr::Ptr &edgeAssertion,
578  const std::vector<Expression> &userAssertions, bool atEndOfPath, SymbolicExprParser&);
579 
580  // Mark vertex as being reached
581  void markAsReached(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);
582 };
583 
584 } // namespace
585 } // namespace
586 
587 std::ostream& operator<<(std::ostream&, const Rose::BinaryAnalysis::FeasiblePath::Expression&);
588 
589 // Convert string to feasible path expression during command-line parsing
590 namespace Sawyer {
591  namespace CommandLine {
592  template<>
593  struct LexicalCast<Rose::BinaryAnalysis::FeasiblePath::Expression> {
594  static Rose::BinaryAnalysis::FeasiblePath::Expression convert(const std::string &src) {
596  }
597  };
598  }
599 }
600 
601 #endif
std::string firstAccessMode
How was variable first accessed ("read" or "write").
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.
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.
static bool isAnyEndpointReachable(const Partitioner2::ControlFlowGraph &cfg, const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex, const Partitioner2::CfgConstVertexSet &endVertices)
Determine whether any ending vertex is reachable.
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.
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.
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.
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.
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.
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.
virtual void nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, SgAsmInstruction *insn)
Function invoked whenever a null pointer dereference is detected.
std::vector< std::string > assertionLocations
Locations at which "constraints" are checked.
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.
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.
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.
virtual void memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, const SmtSolverPtr &solver, IoMode ioMode, const InstructionSemantics2::BaseSemantics::SValuePtr &addr, const InstructionSemantics2::BaseSemantics::SValuePtr &value, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops)
Function invoked every time a memory reference occurs.
void reset()
Reset to initial state without changing settings.
A path through a control flow graph.
Definition: CfgPath.h:15
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.
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.
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.
virtual void processVertex(const InstructionSemantics2::BaseSemantics::DispatcherPtr &cpu, const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex, size_t &pathInsnIndex)
Process one vertex.
const VarDetails & varDetails(const InstructionSemantics2::BaseSemantics::StatePtr &) const
Details about all variables by name.
void clear()
Remove all edges or vertices from this set.
static size_t pathLength(const Partitioner2::CfgPath &)
Total length of path.
Partitioner2::ControlFlowGraph::ConstVertexIterator pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const
Convert path vertex to a CFG 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.
Defines registers available for a particular architecture.
Definition: Registers.h:35
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.
SymbolicExpr::Ptr memAddress
Address where variable is located.
Partitions instructions into basic blocks and functions.
Definition: Partitioner.h:316
Base class for all ROSE exceptions.
Definition: RoseException.h:9
const AddressSet & reachedBlockVas() const
Property: Addresses reached during analysis.
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.
Container associating values with keys.
Definition: Sawyer/Map.h:66
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.