cprover
flow_insensitive_analysis.cpp
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 
14 
15 #include <cassert>
16 
17 #include <util/std_expr.h>
18 #include <util/std_code.h>
19 
21  locationt from,
22  locationt to) const
23 {
24  if(!from->is_goto())
25  return true_exprt();
26 
27  locationt next=from;
28  next++;
29 
30  if(next==to)
31  {
32  exprt tmp(from->guard);
33  tmp.make_not();
34  return tmp;
35  }
36 
37  return from->guard;
38 }
39 
41 {
42  // get predecessor of "to"
43  to--;
44 
45  if(to->is_end_function())
46  return static_cast<const exprt &>(get_nil_irep());
47 
48  // must be the function call
49  return to_code_function_call(to->code).lhs();
50 }
51 
53  const goto_functionst &goto_functions)
54 {
55  initialize(goto_functions);
56  fixedpoint(goto_functions);
57 }
58 
61 {
63  goto_functionst goto_functions;
64  fixedpoint(goto_program, goto_functions);
65 }
66 
68  const goto_functionst &goto_functions,
69  std::ostream &out)
70 {
71  forall_goto_functions(f_it, goto_functions)
72  {
73  out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
74 
75  output(f_it->second.body, f_it->first, out);
76  }
77 }
78 
80  const goto_programt &,
81  const irep_idt &,
82  std::ostream &out) const
83 {
84  get_state().output(ns, out);
85 }
86 
89  working_sett &working_set)
90 {
91  assert(!working_set.empty());
92 
93 // working_sett::iterator i=working_set.begin();
94 // locationt l=i->second;
95 // working_set.erase(i);
96 
97 // pop_heap(working_set.begin(), working_set.end());
98  locationt l=working_set.top();
99  working_set.pop();
100 
101  return l;
102 }
103 
106  const goto_functionst &goto_functions)
107 {
108  if(goto_program.instructions.empty())
109  return false;
110 
111  working_sett working_set;
112 
113 // make_heap(working_set.begin(), working_set.end());
114 
116  working_set,
117  goto_program.instructions.begin());
118 
119  bool new_data=false;
120 
121  while(!working_set.empty())
122  {
123  locationt l=get_next(working_set);
124 
125  if(visit(l, working_set, goto_program, goto_functions))
126  new_data=true;
127  }
128 
129  return new_data;
130 }
131 
133  locationt l,
134  working_sett &working_set,
136  const goto_functionst &goto_functions)
137 {
138  bool new_data=false;
139 
140  #if 0
141  std::cout << "Visiting: " << l->function << " " <<
142  l->location_number << '\n';
143  #endif
144 
145  seen_locations.insert(l);
146  if(statistics.find(l)==statistics.end())
147  statistics[l]=1;
148  else
149  statistics[l]++;
150 
151  for(const auto &to_l : goto_program.get_successors(l))
152  {
153  if(to_l==goto_program.instructions.end())
154  continue;
155 
156  bool changed=false;
157 
158  if(l->is_function_call())
159  {
160  // this is a big special case
161  const code_function_callt &code = to_code_function_call(l->code);
162 
163  changed=
165  l,
166  code.function(),
167  code.arguments(),
168  get_state(),
169  goto_functions);
170  }
171  else
172  changed = get_state().transform(ns, l, to_l);
173 
174  if(changed || !seen(to_l))
175  {
176  new_data=true;
177  put_in_working_set(working_set, to_l);
178  }
179  }
180 
181 // if (id2string(l->function).find("debug")!=std::string::npos)
182 // std::cout << l->function << '\n'; //=="messages::debug")
183 
184 // {
185 // static unsigned state_cntr=0;
186 // std::string s("pastate"); s += std::to_string(state_cntr);
187 // std::ofstream f(s.c_str());
188 // goto_program.output_instruction(ns, "", f, l);
189 // f << '\n';
190 // get_state().output(ns, f);
191 // f.close();
192 // state_cntr++;
193 // }
194 
195  return new_data;
196 }
197 
199  locationt l_call,
200  const goto_functionst &goto_functions,
201  const goto_functionst::function_mapt::const_iterator f_it,
202  const exprt::operandst &,
203  statet &state)
204 {
205  const goto_functionst::goto_functiont &goto_function=f_it->second;
206 
207  if(!goto_function.body_available())
208  {
209  const code_function_callt &code = to_code_function_call(l_call->code);
210 
211  goto_programt temp;
212 
213  exprt rhs =
215 
217  r->make_return();
218  r->code=code_returnt(rhs);
219  r->function=f_it->first;
220  r->location_number=0;
221 
223  t->code.set(ID_identifier, code.function());
224  t->function=f_it->first;
225  t->location_number=1;
226 
227  locationt l_next=l_call; l_next++;
228  bool new_data=state.transform(ns, l_call, r);
229  new_data = state.transform(ns, r, t) || new_data;
230  new_data = state.transform(ns, t, l_next) || new_data;
231 
232  return new_data;
233  }
234 
235  assert(!goto_function.body.instructions.empty());
236 
237  bool new_data=false;
238 
239  {
240  // get the state at the beginning of the function
241  locationt l_begin=goto_function.body.instructions.begin();
242 
243  // do the edge from the call site to the beginning of the function
244  new_data=state.transform(ns, l_call, l_begin);
245 
246  // do each function at least once
247  if(functions_done.find(f_it->first)==
248  functions_done.end())
249  {
250  new_data=true;
251  functions_done.insert(f_it->first);
252  }
253 
254  // do we need to do the fixedpoint of the body?
255  if(new_data)
256  {
257  // recursive call
258  fixedpoint(goto_function.body, goto_functions);
259  new_data=true; // could be reset by fixedpoint
260  }
261  }
262 
263  {
264  // get location at end of procedure
265  locationt l_end=--goto_function.body.instructions.end();
266 
267  assert(l_end->is_end_function());
268 
269  // do edge from end of function to instruction after call
270  locationt l_next=l_call;
271  l_next++;
272  new_data = state.transform(ns, l_end, l_next) || new_data;
273  }
274 
275  return new_data;
276 }
277 
279  locationt l_call,
280  const exprt &function,
281  const exprt::operandst &arguments,
282  statet &state,
283  const goto_functionst &goto_functions)
284 {
285  bool new_data = false;
286 
287  if(function.id()==ID_symbol)
288  {
289  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
290 
291  if(recursion_set.find(identifier)!=recursion_set.end())
292  {
293  // recursion detected!
294  return false;
295  }
296  else
297  recursion_set.insert(identifier);
298 
299  goto_functionst::function_mapt::const_iterator it=
300  goto_functions.function_map.find(identifier);
301 
302  if(it==goto_functions.function_map.end())
303  throw "failed to find function "+id2string(identifier);
304 
305  new_data =
307  l_call,
308  goto_functions,
309  it,
310  arguments,
311  state);
312 
313  recursion_set.erase(identifier);
314  }
315  else if(function.id()==ID_if)
316  {
317  if(function.operands().size()!=3)
318  throw "if takes three arguments";
319 
320  new_data =
322  l_call,
323  function.op1(),
324  arguments,
325  state,
326  goto_functions);
327 
328  new_data =
330  l_call,
331  function.op2(),
332  arguments,
333  state,
334  goto_functions) || new_data;
335  }
336  else if(function.id()==ID_dereference)
337  {
338  // get value set
339  expr_sett values;
340 
341  get_reference_set(function, values);
342 
343  // now call all of these
344  for(const auto &v : values)
345  {
346  if(v.id()==ID_object_descriptor)
347  {
349 
350  // ... but only if they are actually functions.
351  goto_functionst::function_mapt::const_iterator it=
352  goto_functions.function_map.find(o.object().get(ID_identifier));
353 
354  if(it!=goto_functions.function_map.end())
355  {
356  new_data =
358  l_call,
359  o.object(),
360  arguments,
361  state,
362  goto_functions) || new_data;
363  }
364  }
365  }
366  }
367  else if(function.id() == ID_null_object)
368  {
369  // ignore, can't be a function
370  }
371  else if(function.id()==ID_member || function.id()==ID_index)
372  {
373  // ignore, can't be a function
374  }
375  else if(function.id()=="builtin-function")
376  {
377  // ignore
378  }
379  else
380  {
381  throw "unexpected function_call argument: "+
382  function.id_string();
383  }
384  return new_data;
385 }
386 
388  const goto_functionst &goto_functions)
389 {
390  // do each function at least once
391 
392  forall_goto_functions(it, goto_functions)
393  if(functions_done.find(it->first)==
394  functions_done.end())
395  {
396  fixedpoint(it, goto_functions);
397  }
398 }
399 
401  const goto_functionst::function_mapt::const_iterator it,
402  const goto_functionst &goto_functions)
403 {
404  functions_done.insert(it->first);
405  return fixedpoint(it->second.body, goto_functions);
406 }
407 
409 {
410  // no need to copy value sets around
411 }
412 
414 {
415  // no need to copy value sets around
416 }
const irept & get_nil_irep()
Definition: irep.cpp:56
static int8_t r
Definition: irep_hash.h:59
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
const irep_idt & get_identifier() const
Definition: std_expr.h:128
virtual void operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
Definition: std_expr.h:2000
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
function_mapt function_map
typet & type()
Definition: expr.h:56
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 statet & get_state()=0
goto_programt::const_targett locationt
The boolean constant true.
Definition: std_expr.h:4486
argumentst & arguments()
Definition: std_code.h:890
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
instructionst::iterator targett
Definition: goto_program.h:397
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)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
::goto_functiont goto_functiont
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
std::vector< exprt > operandst
Definition: expr.h:45
const source_locationt & source_location() const
Definition: type.h:97
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Flow Insensitive Static Analysis.
void make_not()
Definition: expr.cpp:91
exprt & function()
Definition: std_code.h:878
virtual void initialize(const goto_programt &)
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
goto_programt & goto_program
Definition: cover.cpp:63
Return from a function.
Definition: std_code.h:923
#define forall_goto_functions(it, functions)
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
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
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