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 
44  to--;
45 
46  if(to->is_end_function())
47  return static_cast<const exprt &>(get_nil_irep());
48 
49  // must be the function call
50  assert(to->is_function_call());
51 
52  const code_function_callt &code=
53  to_code_function_call(to_code(to->code));
54 
55  return code.lhs();
56 }
57 
59  const goto_functionst &goto_functions)
60 {
61  initialize(goto_functions);
62  fixedpoint(goto_functions);
63 }
64 
66  const goto_programt &goto_program)
67 {
68  initialize(goto_program);
69  goto_functionst goto_functions;
70  fixedpoint(goto_program, goto_functions);
71 }
72 
74  const goto_functionst &goto_functions,
75  std::ostream &out)
76 {
77  forall_goto_functions(f_it, goto_functions)
78  {
79  out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
80 
81  output(f_it->second.body, f_it->first, out);
82  }
83 }
84 
86  const goto_programt &goto_program,
87  const irep_idt &identifier,
88  std::ostream &out) const
89 {
90  get_state().output(ns, out);
91 }
92 
95  working_sett &working_set)
96 {
97  assert(!working_set.empty());
98 
99 // working_sett::iterator i=working_set.begin();
100 // locationt l=i->second;
101 // working_set.erase(i);
102 
103 // pop_heap(working_set.begin(), working_set.end());
104  locationt l=working_set.top();
105  working_set.pop();
106 
107  return l;
108 }
109 
111  const goto_programt &goto_program,
112  const goto_functionst &goto_functions)
113 {
114  if(goto_program.instructions.empty())
115  return false;
116 
117  working_sett working_set;
118 
119 // make_heap(working_set.begin(), working_set.end());
120 
122  working_set,
123  goto_program.instructions.begin());
124 
125  bool new_data=false;
126 
127  while(!working_set.empty())
128  {
129  locationt l=get_next(working_set);
130 
131  if(visit(l, working_set, goto_program, goto_functions))
132  new_data=true;
133  }
134 
135  return new_data;
136 }
137 
139  locationt l,
140  working_sett &working_set,
141  const goto_programt &goto_program,
142  const goto_functionst &goto_functions)
143 {
144  bool new_data=false;
145 
146  #if 0
147  std::cout << "Visiting: " << l->function << " " <<
148  l->location_number << '\n';
149  #endif
150 
151  seen_locations.insert(l);
152  if(statistics.find(l)==statistics.end())
153  statistics[l]=1;
154  else
155  statistics[l]++;
156 
157  for(const auto &to_l : goto_program.get_successors(l))
158  {
159  if(to_l==goto_program.instructions.end())
160  continue;
161 
162  bool changed=false;
163 
164  if(l->is_function_call())
165  {
166  // this is a big special case
167  const code_function_callt &code=
168  to_code_function_call(to_code(l->code));
169 
170  changed=
172  l,
173  code.function(),
174  code.arguments(),
175  get_state(),
176  goto_functions);
177  }
178  else
179  changed = get_state().transform(ns, l, to_l);
180 
181  if(changed || !seen(to_l))
182  {
183  new_data=true;
184  put_in_working_set(working_set, to_l);
185  }
186  }
187 
188 // if (id2string(l->function).find("debug")!=std::string::npos)
189 // std::cout << l->function << '\n'; //=="messages::debug")
190 
191 // {
192 // static unsigned state_cntr=0;
193 // std::string s("pastate"); s += std::to_string(state_cntr);
194 // std::ofstream f(s.c_str());
195 // goto_program.output_instruction(ns, "", f, l);
196 // f << '\n';
197 // get_state().output(ns, f);
198 // f.close();
199 // state_cntr++;
200 // }
201 
202  return new_data;
203 }
204 
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 &state)
211 {
212  const goto_functionst::goto_functiont &goto_function=f_it->second;
213 
214  if(!goto_function.body_available())
215  {
216  const code_function_callt &code =
217  to_code_function_call(to_code(l_call->code));
218 
219  goto_programt temp;
220 
221  exprt rhs=side_effect_expr_nondett(code.lhs().type());
222 
224  r->make_return();
225  r->code=code_returnt(rhs);
226  r->function=f_it->first;
227  r->location_number=0;
228 
230  t->code.set(ID_identifier, code.function());
231  t->function=f_it->first;
232  t->location_number=1;
233 
234  locationt l_next=l_call; l_next++;
235  bool new_data=state.transform(ns, l_call, r);
236  new_data = state.transform(ns, r, t) || new_data;
237  new_data = state.transform(ns, t, l_next) || new_data;
238 
239  return new_data;
240  }
241 
242  assert(!goto_function.body.instructions.empty());
243 
244  bool new_data=false;
245 
246  {
247  // get the state at the beginning of the function
248  locationt l_begin=goto_function.body.instructions.begin();
249 
250  // do the edge from the call site to the beginning of the function
251  new_data=state.transform(ns, l_call, l_begin);
252 
253  // do each function at least once
254  if(functions_done.find(f_it->first)==
255  functions_done.end())
256  {
257  new_data=true;
258  functions_done.insert(f_it->first);
259  }
260 
261  // do we need to do the fixedpoint of the body?
262  if(new_data)
263  {
264  // recursive call
265  fixedpoint(goto_function.body, goto_functions);
266  new_data=true; // could be reset by fixedpoint
267  }
268  }
269 
270  {
271  // get location at end of procedure
272  locationt l_end=--goto_function.body.instructions.end();
273 
274  assert(l_end->is_end_function());
275 
276  // do edge from end of function to instruction after call
277  locationt l_next=l_call;
278  l_next++;
279  new_data = state.transform(ns, l_end, l_next) || new_data;
280  }
281 
282  return new_data;
283 }
284 
286  locationt l_call,
287  const exprt &function,
288  const exprt::operandst &arguments,
289  statet &state,
290  const goto_functionst &goto_functions)
291 {
292  bool new_data = false;
293 
294  if(function.id()==ID_symbol)
295  {
296  const irep_idt &identifier=function.get(ID_identifier);
297 
298  if(recursion_set.find(identifier)!=recursion_set.end())
299  {
300  // recursion detected!
301  return false;
302  }
303  else
304  recursion_set.insert(identifier);
305 
306  goto_functionst::function_mapt::const_iterator it=
307  goto_functions.function_map.find(identifier);
308 
309  if(it==goto_functions.function_map.end())
310  throw "failed to find function "+id2string(identifier);
311 
312  new_data =
314  l_call,
315  goto_functions,
316  it,
317  arguments,
318  state);
319 
320  recursion_set.erase(identifier);
321  }
322  else if(function.id()==ID_if)
323  {
324  if(function.operands().size()!=3)
325  throw "if takes three arguments";
326 
327  new_data =
329  l_call,
330  function.op1(),
331  arguments,
332  state,
333  goto_functions);
334 
335  new_data =
337  l_call,
338  function.op2(),
339  arguments,
340  state,
341  goto_functions) || new_data;
342  }
343  else if(function.id()==ID_dereference)
344  {
345  // get value set
346  expr_sett values;
347 
348  get_reference_set(function, values);
349 
350  // now call all of these
351  for(const auto &v : values)
352  {
353  if(v.id()==ID_object_descriptor)
354  {
356 
357  // ... but only if they are actually functions.
358  goto_functionst::function_mapt::const_iterator it=
359  goto_functions.function_map.find(o.object().get(ID_identifier));
360 
361  if(it!=goto_functions.function_map.end())
362  {
363  new_data =
365  l_call,
366  o.object(),
367  arguments,
368  state,
369  goto_functions) || new_data;
370  }
371  }
372  }
373  }
374  else if(function.id()=="NULL-object")
375  {
376  // ignore, can't be a function
377  }
378  else if(function.id()==ID_member || function.id()==ID_index)
379  {
380  // ignore, can't be a function
381  }
382  else if(function.id()=="builtin-function")
383  {
384  // ignore
385  }
386  else
387  {
388  throw "unexpected function_call argument: "+
389  function.id_string();
390  }
391  return new_data;
392 }
393 
395  const goto_functionst &goto_functions)
396 {
397  // do each function at least once
398 
399  forall_goto_functions(it, goto_functions)
400  if(functions_done.find(it->first)==
401  functions_done.end())
402  {
403  fixedpoint(it, goto_functions);
404  }
405 }
406 
408  const goto_functionst::function_mapt::const_iterator it,
409  const goto_functionst &goto_functions)
410 {
411  functions_done.insert(it->first);
412  return fixedpoint(it->second.body, goto_functions);
413 }
414 
416  const goto_functionst &goto_functions)
417 {
418  // no need to copy value sets around
419 }
420 
422  const goto_programt &goto_program)
423 {
424  // no need to copy value sets around
425 }
const irept & get_nil_irep()
Definition: irep.cpp:56
static int8_t r
Definition: irep_hash.h:59
std::map< locationt, unsigned > statistics
targett add_instruction()
Adds an instruction at the end.
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
instructionst instructions
The list of instructions in the goto program.
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
typet & type()
Definition: expr.h:60
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
virtual statet & get_state()=0
std::list< Target > get_successors(Target target) const
goto_programt::const_targett locationt
The boolean constant true.
Definition: std_expr.h:3742
argumentst & arguments()
Definition: std_code.h:689
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)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1578
A function call.
Definition: std_code.h:657
virtual void initialize(const goto_programt &goto_program)
std::vector< exprt > operandst
Definition: expr.h:49
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast a generic exprt to an object_descriptor_exprt.
Definition: std_expr.h:1634
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Flow Insensitive Static Analysis.
void make_not()
Definition: expr.cpp:100
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Return from a function.
Definition: std_code.h:714
#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:700
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)