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 
23 
24 #ifndef CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
25 #define CPROVER_ANALYSES_FLOW_INSENSITIVE_ANALYSIS_H
26 
27 #include <queue>
28 #include <map>
29 #include <iosfwd>
30 #include <unordered_set>
31 
33 
34 // don't use me -- I am just a base class
35 // please derive from me
37 {
38 public:
40  changed(false)
41  {
42  }
43 
45 
46  virtual void initialize(const namespacet &ns)=0;
47 
48  virtual bool transform(
49  const namespacet &ns,
50  locationt from,
51  locationt to)=0;
52 
54  {
55  }
56 
57  virtual void output(
58  const namespacet &,
59  std::ostream &) const
60  {
61  }
62 
63  typedef std::unordered_set<exprt, irep_hash> expr_sett;
64 
65  virtual void get_reference_set(
66  const namespacet &,
67  const exprt &,
68  expr_sett &expr_set)
69  {
70  // dummy, overload me!
71  expr_set.clear();
72  }
73 
74  virtual void clear(void)=0;
75 
76 protected:
77  bool changed;
78  // utilities
79 
80  // get guard of a conditional edge
81  exprt get_guard(locationt from, locationt to) const;
82 
83  // get lhs that return value is assigned to
84  // for an edge that returns from a function
85  exprt get_return_lhs(locationt to) const;
86 };
87 
89 {
90 public:
93 
94  std::set<locationt> seen_locations;
95 
96  std::map<locationt, unsigned> statistics;
97 
98  bool seen(const locationt &l)
99  {
100  return (seen_locations.find(l)!=seen_locations.end());
101  }
102 
104  ns(_ns),
105  initialized(false)
106  {
107  }
108 
109  virtual void initialize(const goto_programt &)
110  {
111  if(!initialized)
112  {
113  initialized=true;
114  }
115  }
116 
117  virtual void initialize(const goto_functionst &)
118  {
119  if(!initialized)
120  {
121  initialized=true;
122  }
123  }
124 
125  virtual void update(const goto_programt &goto_program);
126 
127  virtual void update(const goto_functionst &goto_functions);
128 
129  virtual void operator()(
130  const goto_programt &goto_program);
131 
132  virtual void operator()(
133  const goto_functionst &goto_functions);
134 
136  {
137  }
138 
139  virtual void clear()
140  {
141  initialized=false;
142  }
143 
144  virtual void output(
145  const goto_functionst &goto_functions,
146  std::ostream &out);
147 
148  virtual void output(
149  const goto_programt &goto_program,
150  std::ostream &out)
151  {
152  output(goto_program, "", out);
153  }
154 
155 protected:
156  const namespacet &ns;
157 
158  virtual void output(
159  const goto_programt &goto_program,
160  const irep_idt &identifier,
161  std::ostream &out) const;
162 
163  typedef std::priority_queue<locationt> working_sett;
164 
165  locationt get_next(working_sett &working_set);
166 
168  working_sett &working_set,
169  locationt l)
170  {
171  working_set.push(l);
172  }
173 
174  // true = found something new
175  bool fixedpoint(
176  const goto_programt &goto_program,
177  const goto_functionst &goto_functions);
178 
179  bool fixedpoint(
180  goto_functionst::function_mapt::const_iterator it,
181  const goto_functionst &goto_functions);
182 
183  void fixedpoint(
184  const goto_functionst &goto_functions);
185 
186  // true = found something new
187  bool visit(
188  locationt l,
189  working_sett &working_set,
190  const goto_programt &goto_program,
191  const goto_functionst &goto_functions);
192 
194  {
195  l++;
196  return l;
197  }
198 
199  typedef std::set<irep_idt> functions_donet;
201 
202  typedef std::set<irep_idt> recursion_sett;
204 
206 
207  // function calls
209  locationt l_call,
210  const exprt &function,
211  const exprt::operandst &arguments,
212  statet &new_state,
213  const goto_functionst &goto_functions);
214 
215  bool do_function_call(
216  locationt l_call,
217  const goto_functionst &goto_functions,
218  const goto_functionst::function_mapt::const_iterator f_it,
219  const exprt::operandst &arguments,
220  statet &new_state);
221 
222  // abstract methods
223 
224  virtual statet &get_state()=0;
225  virtual const statet &get_state() const=0;
226 
228 
229  virtual void get_reference_set(
230  const exprt &expr,
231  expr_sett &expr_set)=0;
232 };
233 
234 
235 template<typename T>
237 {
238 public:
239  // constructor
242  {
243  }
244 
246 
247  virtual void clear()
248  {
249  state.clear();
251  }
252 
253  T &get_data() { return state; }
254  const T &get_data() const { return state; }
255 
256 protected:
257  T state; // one global state
258 
259  virtual statet &get_state() { return state; }
260 
261  virtual const statet &get_state() const { return state; }
262 
264  const exprt &expr,
265  expr_sett &expr_set)
266  {
267  state.get_reference_set(ns, expr, expr_set);
268  }
269 
270 private:
271  // to enforce that T is derived from abstract_domain_baset
272  void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
273 };
274 
275 #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:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
A collection of goto functions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
static locationt successor(locationt l)
std::vector< exprt > operandst
Definition: expr.h:57
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
Base class for all expressions.
Definition: expr.h:54
void get_reference_set(const exprt &expr, expr_sett &expr_set)
virtual void initialize(const namespacet &ns)=0
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