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  {
30  }
31 
33 
34  virtual void initialize(const namespacet &ns)=0;
35 
36  virtual bool transform(
37  const namespacet &ns,
38  locationt from,
39  locationt to)=0;
40 
42  {
43  }
44 
45  virtual void output(
46  const namespacet &ns,
47  std::ostream &out) const
48  {
49  }
50 
51  typedef std::unordered_set<exprt, irep_hash> expr_sett;
52 
53  virtual void get_reference_set(
54  const namespacet &ns,
55  const exprt &expr,
56  expr_sett &expr_set)
57  {
58  // dummy, overload me!
59  expr_set.clear();
60  }
61 
62  virtual void clear(void)=0;
63 
64 protected:
65  bool changed;
66  // utilities
67 
68  // get guard of a conditional edge
69  exprt get_guard(locationt from, locationt to) const;
70 
71  // get lhs that return value is assigned to
72  // for an edge that returns from a function
73  exprt get_return_lhs(locationt to) const;
74 };
75 
77 {
78 public:
81 
82  std::set<locationt> seen_locations;
83 
84  std::map<locationt, unsigned> statistics;
85 
86  bool seen(const locationt &l)
87  {
88  return (seen_locations.find(l)!=seen_locations.end());
89  }
90 
92  ns(_ns),
93  initialized(false)
94  {
95  }
96 
97  virtual void initialize(
98  const goto_programt &goto_program)
99  {
100  if(!initialized)
101  {
102  initialized=true;
103  }
104  }
105 
106  virtual void initialize(
107  const goto_functionst &goto_functions)
108  {
109  if(!initialized)
110  {
111  initialized=true;
112  }
113  }
114 
115  virtual void update(const goto_programt &goto_program);
116 
117  virtual void update(const goto_functionst &goto_functions);
118 
119  virtual void operator()(
120  const goto_programt &goto_program);
121 
122  virtual void operator()(
123  const goto_functionst &goto_functions);
124 
126  {
127  }
128 
129  virtual void clear()
130  {
131  initialized=false;
132  }
133 
134  virtual void output(
135  const goto_functionst &goto_functions,
136  std::ostream &out);
137 
138  virtual void output(
139  const goto_programt &goto_program,
140  std::ostream &out)
141  {
142  output(goto_program, "", out);
143  }
144 
145 protected:
146  const namespacet &ns;
147 
148  virtual void output(
149  const goto_programt &goto_program,
150  const irep_idt &identifier,
151  std::ostream &out) const;
152 
153  typedef std::priority_queue<locationt> working_sett;
154 
155  locationt get_next(working_sett &working_set);
156 
158  working_sett &working_set,
159  locationt l)
160  {
161  working_set.push(l);
162  }
163 
164  // true = found something new
165  bool fixedpoint(
166  const goto_programt &goto_program,
167  const goto_functionst &goto_functions);
168 
169  bool fixedpoint(
170  goto_functionst::function_mapt::const_iterator it,
171  const goto_functionst &goto_functions);
172 
173  void fixedpoint(
174  const goto_functionst &goto_functions);
175 
176  // true = found something new
177  bool visit(
178  locationt l,
179  working_sett &working_set,
180  const goto_programt &goto_program,
181  const goto_functionst &goto_functions);
182 
184  {
185  l++;
186  return l;
187  }
188 
189  typedef std::set<irep_idt> functions_donet;
191 
192  typedef std::set<irep_idt> recursion_sett;
194 
196 
197  // function calls
199  locationt l_call,
200  const exprt &function,
201  const exprt::operandst &arguments,
202  statet &new_state,
203  const goto_functionst &goto_functions);
204 
205  bool do_function_call(
206  locationt l_call,
207  const goto_functionst &goto_functions,
208  const goto_functionst::function_mapt::const_iterator f_it,
209  const exprt::operandst &arguments,
210  statet &new_state);
211 
212  // abstract methods
213 
214  virtual statet &get_state()=0;
215  virtual const statet &get_state() const=0;
216 
218 
219  virtual void get_reference_set(
220  const exprt &expr,
221  expr_sett &expr_set)=0;
222 };
223 
224 
225 template<typename T>
227 {
228 public:
229  // constructor
232  {
233  }
234 
236 
237  virtual void clear()
238  {
239  state.clear();
241  }
242 
243  T &get_data() { return state; }
244  const T &get_data() const { return state; }
245 
246 protected:
247  T state; // one global state
248 
249  virtual statet &get_state() { return state; }
250 
251  virtual const statet &get_state() const { return state; }
252 
254  const exprt &expr,
255  expr_sett &expr_set)
256  {
257  state.get_reference_set(ns, expr, expr_set);
258  }
259 
260 private:
261  // to enforce that T is derived from abstract_domain_baset
262  void dummy(const T &s) { const statet &x=dummy1(s); (void)x; }
263 };
264 
265 #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)
instructionst::const_iterator const_targett
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
TO_BE_DOCUMENTED.
Definition: namespace.h:62
virtual void initialize(const goto_programt &goto_program)
static locationt successor(locationt l)
std::vector< exprt > operandst
Definition: expr.h:49
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
goto_programt::const_targett locationt
Base class for all expressions.
Definition: expr.h:46
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 get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)