ROSE  0.9.9.109
BinaryTaintedFlow.h
1 #ifndef ROSE_BinaryAnalysis_TaintedFlow_H
2 #define ROSE_BinaryAnalysis_TaintedFlow_H
3 
4 #include "BinaryDataFlow.h"
5 #include "Diagnostics.h"
6 
7 #include <boost/foreach.hpp>
8 #include <boost/shared_ptr.hpp>
9 #include <stdexcept>
10 
11 namespace Rose {
12 namespace BinaryAnalysis {
13 
17 class TaintedFlow {
18 public:
23  enum Taintedness { BOTTOM, NOT_TAINTED, TAINTED, TOP };
24 
30  enum Approximation { UNDER_APPROXIMATE, OVER_APPROXIMATE };
31 
36 
38  typedef std::pair<DataFlow::Variable, Taintedness> VariableTaint;
39 
41  // State
43 public:
48  class State {
49  typedef std::list<VariableTaint> VarTaintList;
50  VarTaintList taints_;
51 
52  public:
54  typedef boost::shared_ptr<State> Ptr;
55 
56  protected:
57  // Initialize taintedness for all variables; this is protected because this is a reference-counted object
59  BOOST_FOREACH (const DataFlow::Variable &variable, variables)
60  taints_.push_back(std::make_pair(variable, taint));
61  }
62 
63  public:
69  return State::Ptr(new State(variables, taint));
70  }
71 
75  virtual State::Ptr copy() const {
76  return State::Ptr(new State(*this));
77  }
78 
79  virtual ~State() {}
80 
86 
91 
95  bool merge(const State::Ptr&);
96 
102  const VarTaintList& variables() const { return taints_; }
103  VarTaintList& variables() { return taints_; }
107  void print(std::ostream&) const;
108  };
109 
114 
116  // Transfer function
118 protected:
120  const DataFlow::VertexFlowGraphs &index_; // maps CFG vertex to data flow graph
121  Approximation approximation_;
122  SMTSolver *smtSolver_;
124  public:
127  : index_(index), approximation_(approx), smtSolver_(solver), mlog(mlog) {}
128 
129  template<class CFG>
130  StatePtr operator()(const CFG &cfg, size_t cfgVertex, const StatePtr &in) {
131  return (*this)(cfgVertex, in);
132  }
133 
134  StatePtr operator()(size_t cfgVertex, const StatePtr &in);
135 
136  std::string printState(const StatePtr &in);
137  };
138 
140  // Merge function
142 protected:
144  public:
145  bool operator()(StatePtr &dst /*in,out*/, const StatePtr &src) const {
146  ASSERT_not_null(src);
147  if (!dst) {
148  dst = src->copy();
149  return true; // destination changed
150  }
151  return dst->merge(src);
152  }
153  };
154 
156  // Data members
158 private:
159  static Sawyer::Message::Facility mlog;
160  Approximation approximation_;
161  DataFlow dataFlow_;
162  DataFlow::VertexFlowGraphs vertexFlowGraphs_;
163  DataFlow::VariableList variableList_;
164  bool vlistInitialized_;
165  std::vector<StatePtr> results_;
166  SMTSolver *smtSolver_;
167 
168 public:
176  : approximation_(UNDER_APPROXIMATE), dataFlow_(userDispatcher), vlistInitialized_(false), smtSolver_(NULL) {}
177 
181  static void initDiagnostics();
182 
191  Approximation approximation() const { return approximation_; }
192  void approximation(Approximation a) { approximation_ = a; }
201  SMTSolver *smtSolver() const { return smtSolver_; }
202  void smtSolver(SMTSolver *solver) { smtSolver_ = solver; }
210  template<class CFG>
211  void computeFlowGraphs(const CFG &cfg, size_t cfgStartVertex) {
212  using namespace Diagnostics;
213  ASSERT_this();
214  ASSERT_require(cfgStartVertex < cfg.nVertices());
215  Stream mesg(mlog[WHERE] <<"computeFlowGraphs starting at CFG vertex " <<cfgStartVertex);
216  vertexFlowGraphs_ = dataFlow_.buildGraphPerVertex(cfg, cfgStartVertex);
217  variableList_ = dataFlow_.getUniqueVariables(vertexFlowGraphs_);
218  results_.clear();
219  vlistInitialized_ = true;
220  mesg <<"; found " <<StringUtility::plural(variableList_.size(), "variables") <<"\n";
221  if (mlog[DEBUG]) {
222  BOOST_FOREACH (const DataFlow::Variable &variable, variableList_)
223  mlog[DEBUG] <<" found variable: " <<variable <<"\n";
224  }
225  }
226 
235  ASSERT_this();
236  return vertexFlowGraphs_;
237  }
239  using namespace Diagnostics;
240  ASSERT_this();
241  vertexFlowGraphs_ = graphMap;
242  variableList_ = dataFlow_.getUniqueVariables(vertexFlowGraphs_);
243  vlistInitialized_ = true;
244  results_.clear();
245  mlog[WHERE] <<"vertexFlowGraphs set by user with " <<StringUtility::plural(variableList_.size(), "variables") <<"\n";
246  }
254  ASSERT_this();
255  ASSERT_require2(vlistInitialized_, "TaintedFlow::computeFlowGraphs must be called before TaintedFlow::variables");
256  return variableList_;
257  }
258 
263  StatePtr stateInstance(Taintedness taint) const {
264  ASSERT_this();
265  ASSERT_require2(vlistInitialized_, "TaintedFlow::computeFlowGraphs must be called before TaintedFlow::stateInstance");
266  return State::instance(variableList_, taint);
267  }
268 
272  template<class CFG>
273  void runToFixedPoint(const CFG &cfg, size_t cfgStartVertex, const StatePtr &initialState) {
274  using namespace Diagnostics;
275  ASSERT_this();
276  ASSERT_require(cfgStartVertex < cfg.nVertices());
277  ASSERT_not_null(initialState);
278  Stream mesg(mlog[WHERE] <<"runToFixedPoint starting at CFG vertex " <<cfgStartVertex);
279  results_.clear();
280  TransferFunction xfer(vertexFlowGraphs_, approximation_, smtSolver_, mlog);
283  dfEngine.runToFixedPoint(cfgStartVertex, initialState);
284  results_ = dfEngine.getFinalStates();
285  mesg <<"; results for " <<StringUtility::plural(results_.size(), "vertices", "vertex") <<"\n";
286  }
287 
292  StatePtr getFinalState(size_t cfgVertexId) const {
293  ASSERT_this();
294  ASSERT_require(cfgVertexId < results_.size());
295  return results_[cfgVertexId];
296  }
297 };
298 
299 std::ostream& operator<<(std::ostream &out, const TaintedFlow::State &state);
300 
301 } // namespace
302 } // namespace
303 
304 #endif
SMTSolver * smtSolver() const
Property: SMT solver.
StatePtr getFinalState(size_t cfgVertexId) const
Query results.
static State::Ptr instance(const DataFlow::VariableList &variables, Taintedness taint=BOTTOM)
Allocating constructor.
const VarTaintList & variables() const
List of all variables and their taintedness.
Collection of streams.
Definition: Message.h:1579
Various tools for performing tainted flow analysis.
void runToFixedPoint(const CFG &cfg, size_t cfgStartVertex, const StatePtr &initialState)
Run data flow.
void smtSolver(SMTSolver *solver)
Property: SMT solver.
std::list< Variable > VariableList
List of variables.
TaintedFlow(const InstructionSemantics2::BaseSemantics::DispatcherPtr &userDispatcher)
Constructs a tainted flow analysis.
const VertexStates & getFinalStates() const
All outgoing states.
void print(std::ostream &) const
Print this state.
boost::shared_ptr< State > Ptr
Shared-ownership pointer to taint states.
Main namespace for the ROSE library.
bool merge(const State::Ptr &)
Merge other state into this state.
void runToFixedPoint()
Run data-flow until it reaches a fixed point.
bool setIfExists(const DataFlow::Variable &, Taintedness)
Set taintedness if the variable exists.
VariableList getUniqueVariables(const VertexFlowGraphs &)
Get list of unique variables.
State::Ptr StatePtr
Reference counting pointer to State.
VarTaintList & variables()
List of all variables and their taintedness.
boost::shared_ptr< class Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
void vertexFlowGraphs(const DataFlow::VertexFlowGraphs &graphMap)
Property: data flow graphs.
std::pair< DataFlow::Variable, Taintedness > VariableTaint
Variable-Taintedness pair.
static Taintedness merge(Taintedness, Taintedness)
Merges two taint values.
const DataFlow::VertexFlowGraphs & vertexFlowGraphs() const
Property: data flow graphs.
const DataFlow::VariableList & variables() const
List of variables.
static void initDiagnostics()
Initialize diagnostics.
Various tools for data-flow analysis.
void approximation(Approximation a)
Property: approximation.
std::string plural(T n, const std::string &plural_word, const std::string &singular_word="")
Helpful way to print singular or plural words.
Taintedness & lookup(const DataFlow::Variable &)
Find the taintedness for some variable.
Approximation approximation() const
Property: approximation.
VertexFlowGraphs buildGraphPerVertex(const CFG &cfg, size_t startVertex, VertexUnpacker vertexUnpacker)
Compute data-flow per CFG vertex.
virtual State::Ptr copy() const
Virtual copy constructor.
Interface to Satisfiability Modulo Theory (SMT) solvers.
Definition: SMTSolver.h:19
StatePtr stateInstance(Taintedness taint) const
Creates a new state.
void computeFlowGraphs(const CFG &cfg, size_t cfgStartVertex)
Compute data flow graphs.