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 &ns,
48  std::ostream &out) const
49  {
50  }
51 
52  typedef std::unordered_set<exprt, irep_hash> expr_sett;
53 
54  virtual void get_reference_set(
55  const namespacet &ns,
56  const exprt &expr,
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(
100  {
101  if(!initialized)
102  {
103  initialized=true;
104  }
105  }
106 
107  virtual void initialize(
108  const goto_functionst &goto_functions)
109  {
110  if(!initialized)
111  {
112  initialized=true;
113  }
114  }
115 
116  virtual void update(const goto_programt &goto_program);
117 
118  virtual void update(const goto_functionst &goto_functions);
119 
120  virtual void operator()(
121  const goto_programt &goto_program);
122 
123  virtual void operator()(
124  const goto_functionst &goto_functions);
125 
127  {
128  }
129 
130  virtual void clear()
131  {
132  initialized=false;
133  }
134 
135  virtual void output(
136  const goto_functionst &goto_functions,
137  std::ostream &out);
138 
139  virtual void output(
141  std::ostream &out)
142  {
143  output(goto_program, "", out);
144  }
145 
146 protected:
147  const namespacet &ns;
148 
149  virtual void output(
151  const irep_idt &identifier,
152  std::ostream &out) const;
153 
154  typedef std::priority_queue<locationt> working_sett;
155 
156  locationt get_next(working_sett &working_set);
157 
159  working_sett &working_set,
160  locationt l)
161  {
162  working_set.push(l);
163  }
164 
165  // true = found something new
166  bool fixedpoint(
168  const goto_functionst &goto_functions);
169 
170  bool fixedpoint(
171  goto_functionst::function_mapt::const_iterator it,
172  const goto_functionst &goto_functions);
173 
174  void fixedpoint(
175  const goto_functionst &goto_functions);
176 
177  // true = found something new
178  bool visit(
179  locationt l,
180  working_sett &working_set,
182  const goto_functionst &goto_functions);
183 
185  {
186  l++;
187  return l;
188  }
189 
190  typedef std::set<irep_idt> functions_donet;
192 
193  typedef std::set<irep_idt> recursion_sett;
195 
197 
198  // function calls
200  locationt l_call,
201  const exprt &function,
202  const exprt::operandst &arguments,
203  statet &new_state,
204  const goto_functionst &goto_functions);
205 
206  bool do_function_call(
207  locationt l_call,
208  const goto_functionst &goto_functions,
209  const goto_functionst::function_mapt::const_iterator f_it,
210  const exprt::operandst &arguments,
211  statet &new_state);
212 
213  // abstract methods
214 
215  virtual statet &get_state()=0;
216  virtual const statet &get_state() const=0;
217 
219 
220  virtual void get_reference_set(
221  const exprt &expr,
222  expr_sett &expr_set)=0;
223 };
224 
225 
226 template<typename T>
228 {
229 public:
230  // constructor
233  {
234  }
235 
237 
238  virtual void clear()
239  {
240  state.clear();
242  }
243 
244  T &get_data() { return state; }
245  const T &get_data() const { return state; }
246 
247 protected:
248  T state; // one global state
249 
250  virtual statet &get_state() { return state; }
251 
252  virtual const statet &get_state() const { return state; }
253 
255  const exprt &expr,
256  expr_sett &expr_set)
257  {
258  state.get_reference_set(ns, expr, expr_set);
259  }
260 
261 private:
262  // to enforce that T is derived from abstract_domain_baset
263  void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
264 };
265 
266 #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 operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
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)
virtual void output(const namespacet &ns, std::ostream &out) const
flow_insensitive_analysis_baset(const namespacet &_ns)
virtual statet & get_state()=0
goto_programt::const_targett locationt
virtual void initialize(const goto_functionst &goto_functions)
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
virtual void initialize(const goto_programt &goto_program)
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
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 get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)