cprover
flow_insensitive_analysis.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Flow Insensitive Static Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
14 #define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
15 
16 #include <queue>
17 #include <map>
18 #include <iosfwd>
19 #include <unordered_set>
20 
22 
23 // don't use me -- I am just a base class
24 // please derive from me
26 {
27 public:
29  changed(false)
30  {
31  }
32 
34 
35  virtual void initialize(const namespacet &ns)=0;
36 
37  virtual bool transform(
38  const namespacet &ns,
39  locationt from,
40  locationt to)=0;
41 
43  {
44  }
45 
46  virtual void output(
47  const namespacet &,
48  std::ostream &) const
49  {
50  }
51 
52  typedef std::unordered_set<exprt, irep_hash> expr_sett;
53 
54  virtual void get_reference_set(
55  const namespacet &,
56  const exprt &,
57  expr_sett &expr_set)
58  {
59  // dummy, overload me!
60  expr_set.clear();
61  }
62 
63  virtual void clear(void)=0;
64 
65 protected:
66  bool changed;
67  // utilities
68 
69  // get guard of a conditional edge
70  exprt get_guard(locationt from, locationt to) const;
71 
72  // get lhs that return value is assigned to
73  // for an edge that returns from a function
74  exprt get_return_lhs(locationt to) const;
75 };
76 
78 {
79 public:
82 
83  std::set<locationt> seen_locations;
84 
85  std::map<locationt, unsigned> statistics;
86 
87  bool seen(const locationt &l)
88  {
89  return (seen_locations.find(l)!=seen_locations.end());
90  }
91 
93  ns(_ns),
94  initialized(false)
95  {
96  }
97 
98  virtual void initialize(const goto_programt &)
99  {
100  if(!initialized)
101  {
102  initialized=true;
103  }
104  }
105 
106  virtual void initialize(const goto_functionst &)
107  {
108  if(!initialized)
109  {
110  initialized=true;
111  }
112  }
113 
114  virtual void update(const goto_programt &goto_program);
115 
116  virtual void update(const goto_functionst &goto_functions);
117 
118  virtual void operator()(
119  const goto_programt &goto_program);
120 
121  virtual void operator()(
122  const goto_functionst &goto_functions);
123 
125  {
126  }
127 
128  virtual void clear()
129  {
130  initialized=false;
131  }
132 
133  virtual void output(
134  const goto_functionst &goto_functions,
135  std::ostream &out);
136 
137  virtual void output(
139  std::ostream &out)
140  {
141  output(goto_program, "", out);
142  }
143 
144 protected:
145  const namespacet &ns;
146 
147  virtual void output(
149  const irep_idt &identifier,
150  std::ostream &out) const;
151 
152  typedef std::priority_queue<locationt> working_sett;
153 
154  locationt get_next(working_sett &working_set);
155 
157  working_sett &working_set,
158  locationt l)
159  {
160  working_set.push(l);
161  }
162 
163  // true = found something new
164  bool fixedpoint(
166  const goto_functionst &goto_functions);
167 
168  bool fixedpoint(
169  goto_functionst::function_mapt::const_iterator it,
170  const goto_functionst &goto_functions);
171 
172  void fixedpoint(
173  const goto_functionst &goto_functions);
174 
175  // true = found something new
176  bool visit(
177  locationt l,
178  working_sett &working_set,
180  const goto_functionst &goto_functions);
181 
183  {
184  l++;
185  return l;
186  }
187 
188  typedef std::set<irep_idt> functions_donet;
190 
191  typedef std::set<irep_idt> recursion_sett;
193 
195 
196  // function calls
198  locationt l_call,
199  const exprt &function,
200  const exprt::operandst &arguments,
201  statet &new_state,
202  const goto_functionst &goto_functions);
203 
204  bool do_function_call(
205  locationt l_call,
206  const goto_functionst &goto_functions,
207  const goto_functionst::function_mapt::const_iterator f_it,
208  const exprt::operandst &arguments,
209  statet &new_state);
210 
211  // abstract methods
212 
213  virtual statet &get_state()=0;
214  virtual const statet &get_state() const=0;
215 
217 
218  virtual void get_reference_set(
219  const exprt &expr,
220  expr_sett &expr_set)=0;
221 };
222 
223 
224 template<typename T>
226 {
227 public:
228  // constructor
231  {
232  }
233 
235 
236  virtual void clear()
237  {
238  state.clear();
240  }
241 
242  T &get_data() { return state; }
243  const T &get_data() const { return state; }
244 
245 protected:
246  T state; // one global state
247 
248  virtual statet &get_state() { return state; }
249 
250  virtual const statet &get_state() const { return state; }
251 
253  const exprt &expr,
254  expr_sett &expr_set)
255  {
256  state.get_reference_set(ns, expr, expr_set);
257  }
258 
259 private:
260  // to enforce that T is derived from abstract_domain_baset
261  void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
262 };
263 
264 #endif // CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
Goto Programs with Functions.
virtual void get_reference_set(const namespacet &, const exprt &, expr_sett &expr_set)
virtual void operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
virtual void initialize(const goto_functionst &)
std::unordered_set< exprt, irep_hash > expr_sett
virtual void output(const goto_programt &goto_program, std::ostream &out)
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
flow_insensitive_analysis_baset(const namespacet &_ns)
virtual statet & get_state()=0
goto_programt::const_targett locationt
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
bool do_function_call(locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
flow_insensitive_abstract_domain_baset statet
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
static locationt successor(locationt l)
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
Base class for all expressions.
Definition: expr.h:42
void get_reference_set(const exprt &expr, expr_sett &expr_set)
virtual void initialize(const namespacet &ns)=0
goto_programt & goto_program
Definition: cover.cpp:63
flow_insensitive_analysist(const namespacet &_ns)
virtual const statet & get_state() const
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
void put_in_working_set(working_sett &working_set, locationt l)
std::priority_queue< locationt > working_sett
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
virtual void output(const namespacet &, std::ostream &) const