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
flow_insensitive_analysis_baset::update
virtual void update(const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:404
flow_insensitive_abstract_domain_baset::~flow_insensitive_abstract_domain_baset
virtual ~flow_insensitive_abstract_domain_baset()
Definition: flow_insensitive_analysis.h:53
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
flow_insensitive_analysist::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:245
flow_insensitive_analysis_baset::get_state
virtual statet & get_state()=0
flow_insensitive_analysis_baset::initialized
bool initialized
Definition: flow_insensitive_analysis.h:205
flow_insensitive_analysis_baset::do_function_call
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)
Definition: flow_insensitive_analysis.cpp:195
flow_insensitive_analysis_baset::clear
virtual void clear()
Definition: flow_insensitive_analysis.h:139
flow_insensitive_analysist::get_data
T & get_data()
Definition: flow_insensitive_analysis.h:253
flow_insensitive_analysist::get_reference_set
void get_reference_set(const exprt &expr, expr_sett &expr_set)
Definition: flow_insensitive_analysis.h:263
flow_insensitive_analysist::flow_insensitive_analysist
flow_insensitive_analysist(const namespacet &_ns)
Definition: flow_insensitive_analysis.h:240
flow_insensitive_abstract_domain_baset::initialize
virtual void initialize(const namespacet &ns)=0
exprt
Base class for all expressions.
Definition: expr.h:54
flow_insensitive_analysis_baset::do_function_call_rec
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:278
flow_insensitive_analysis_baset::recursion_set
recursion_sett recursion_set
Definition: flow_insensitive_analysis.h:203
flow_insensitive_analysist::get_state
virtual const statet & get_state() const
Definition: flow_insensitive_analysis.h:261
flow_insensitive_analysis_baset::working_sett
std::priority_queue< locationt > working_sett
Definition: flow_insensitive_analysis.h:163
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition: flow_insensitive_analysis.cpp:37
flow_insensitive_analysis_baset::initialize
virtual void initialize(const goto_programt &)
Definition: flow_insensitive_analysis.h:109
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
flow_insensitive_analysis_baset::seen_locations
std::set< locationt > seen_locations
Definition: flow_insensitive_analysis.h:94
flow_insensitive_abstract_domain_baset::output
virtual void output(const namespacet &, std::ostream &) const
Definition: flow_insensitive_analysis.h:57
flow_insensitive_analysis_baset::functions_donet
std::set< irep_idt > functions_donet
Definition: flow_insensitive_analysis.h:199
flow_insensitive_analysis_baset::get_reference_set
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:44
flow_insensitive_analysis_baset::functions_done
functions_donet functions_done
Definition: flow_insensitive_analysis.h:200
flow_insensitive_analysis_baset
Definition: flow_insensitive_analysis.h:88
flow_insensitive_analysis_baset::operator()
virtual void operator()(const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:56
flow_insensitive_abstract_domain_baset::get_reference_set
virtual void get_reference_set(const namespacet &, const exprt &, expr_sett &expr_set)
Definition: flow_insensitive_analysis.h:65
flow_insensitive_abstract_domain_baset::expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: flow_insensitive_analysis.h:63
flow_insensitive_analysis_baset::flow_insensitive_analysis_baset
flow_insensitive_analysis_baset(const namespacet &_ns)
Definition: flow_insensitive_analysis.h:103
flow_insensitive_analysis_baset::put_in_working_set
void put_in_working_set(working_sett &working_set, locationt l)
Definition: flow_insensitive_analysis.h:167
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
flow_insensitive_abstract_domain_baset::changed
bool changed
Definition: flow_insensitive_analysis.h:77
flow_insensitive_abstract_domain_baset::flow_insensitive_abstract_domain_baset
flow_insensitive_abstract_domain_baset()
Definition: flow_insensitive_analysis.h:39
flow_insensitive_analysis_baset::~flow_insensitive_analysis_baset
virtual ~flow_insensitive_analysis_baset()
Definition: flow_insensitive_analysis.h:135
flow_insensitive_analysis_baset::fixedpoint
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:101
flow_insensitive_analysis_baset::output
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
Definition: flow_insensitive_analysis.cpp:64
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
flow_insensitive_analysis_baset::statistics
std::map< locationt, unsigned > statistics
Definition: flow_insensitive_analysis.h:96
flow_insensitive_abstract_domain_baset::get_guard
exprt get_guard(locationt from, locationt to) const
Definition: flow_insensitive_analysis.cpp:21
flow_insensitive_analysist::state
T state
Definition: flow_insensitive_analysis.h:257
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:92
flow_insensitive_analysis_baset::recursion_sett
std::set< irep_idt > recursion_sett
Definition: flow_insensitive_analysis.h:202
flow_insensitive_analysis_baset::expr_sett
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
Definition: flow_insensitive_analysis.h:227
flow_insensitive_analysist::dummy
void dummy(const T &s)
Definition: flow_insensitive_analysis.h:272
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
flow_insensitive_analysis_baset::statet
flow_insensitive_abstract_domain_baset statet
Definition: flow_insensitive_analysis.h:91
flow_insensitive_analysist::clear
virtual void clear()
Definition: flow_insensitive_analysis.h:247
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
flow_insensitive_abstract_domain_baset
Definition: flow_insensitive_analysis.h:36
flow_insensitive_analysis_baset::initialize
virtual void initialize(const goto_functionst &)
Definition: flow_insensitive_analysis.h:117
flow_insensitive_analysis_baset::output
virtual void output(const goto_programt &goto_program, std::ostream &out)
Definition: flow_insensitive_analysis.h:148
flow_insensitive_analysist::get_state
virtual statet & get_state()
Definition: flow_insensitive_analysis.h:259
flow_insensitive_analysis_baset::visit
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:129
flow_insensitive_analysis_baset::seen
bool seen(const locationt &l)
Definition: flow_insensitive_analysis.h:98
flow_insensitive_analysis_baset::get_next
locationt get_next(working_sett &working_set)
Definition: flow_insensitive_analysis.cpp:85
flow_insensitive_abstract_domain_baset::transform
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
flow_insensitive_analysist::get_data
const T & get_data() const
Definition: flow_insensitive_analysis.h:254
flow_insensitive_analysist
Definition: flow_insensitive_analysis.h:236
flow_insensitive_abstract_domain_baset::clear
virtual void clear(void)=0
flow_insensitive_analysis_baset::successor
static locationt successor(locationt l)
Definition: flow_insensitive_analysis.h:193