cprover
static_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #define USE_DEPRECATED_STATIC_ANALYSIS_H
13 #include "static_analysis.h"
14 
15 #include <cassert>
16 #include <memory>
17 
18 #include <util/expr_util.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
22 #include "is_threaded.h"
23 
25  locationt from,
26  locationt to)
27 {
28  if(!from->is_goto())
29  return true_exprt();
30 
31  locationt next=from;
32  next++;
33 
34  if(next==to)
35  return boolean_negate(from->guard);
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);
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 irep_idt &function_identifier,
67  const goto_programt &goto_program)
68 {
69  initialize(goto_program);
70  goto_functionst goto_functions;
71  fixedpoint(function_identifier, goto_program, goto_functions);
72 }
73 
75  const goto_functionst &goto_functions,
76  std::ostream &out) const
77 {
78  forall_goto_functions(f_it, goto_functions)
79  {
80  if(f_it->second.body_available())
81  {
82  out << "////\n";
83  out << "//// Function: " << f_it->first << "\n";
84  out << "////\n";
85  out << "\n";
86 
87  output(f_it->second.body, f_it->first, out);
88  }
89  }
90 }
91 
93  const goto_programt &goto_program,
94  const irep_idt &,
95  std::ostream &out) const
96 {
97  forall_goto_program_instructions(i_it, goto_program)
98  {
99  out << "**** " << i_it->location_number << " "
100  << i_it->source_location << "\n";
101 
102  get_state(i_it).output(ns, out);
103  out << "\n";
104  #if 0
105  goto_program.output_instruction(ns, identifier, out, i_it);
106  out << "\n";
107  #endif
108  }
109 }
110 
112  const goto_functionst &goto_functions)
113 {
114  forall_goto_functions(f_it, goto_functions)
115  generate_states(f_it->second.body);
116 }
117 
119  const goto_programt &goto_program)
120 {
121  forall_goto_program_instructions(i_it, goto_program)
122  generate_state(i_it);
123 }
124 
126  const goto_functionst &goto_functions)
127 {
128  forall_goto_functions(f_it, goto_functions)
129  update(f_it->second.body);
130 }
131 
133  const goto_programt &goto_program)
134 {
135  locationt previous;
136  bool first=true;
137 
138  forall_goto_program_instructions(i_it, goto_program)
139  {
140  // do we have it already?
141  if(!has_location(i_it))
142  {
143  generate_state(i_it);
144 
145  if(!first)
146  merge(get_state(i_it), get_state(previous), i_it);
147  }
148 
149  first=false;
150  previous=i_it;
151  }
152 }
153 
155  working_sett &working_set)
156 {
157  assert(!working_set.empty());
158 
159  working_sett::iterator i=working_set.begin();
160  locationt l=i->second;
161  working_set.erase(i);
162 
163  return l;
164 }
165 
167  const irep_idt &function_identifier,
168  const goto_programt &goto_program,
169  const goto_functionst &goto_functions)
170 {
171  if(goto_program.instructions.empty())
172  return false;
173 
174  working_sett working_set;
175 
177  working_set,
178  goto_program.instructions.begin());
179 
180  bool new_data=false;
181 
182  while(!working_set.empty())
183  {
184  locationt l=get_next(working_set);
185 
186  if(visit(function_identifier, l, working_set, goto_program, goto_functions))
187  new_data=true;
188  }
189 
190  return new_data;
191 }
192 
194  const irep_idt &function_identifier,
195  locationt l,
196  working_sett &working_set,
197  const goto_programt &goto_program,
198  const goto_functionst &goto_functions)
199 {
200  bool new_data=false;
201 
202  statet &current=get_state(l);
203 
204  current.seen=true;
205 
206  for(const auto &to_l : goto_program.get_successors(l))
207  {
208  if(to_l==goto_program.instructions.end())
209  continue;
210 
211  std::unique_ptr<statet> tmp_state(
212  make_temporary_state(current));
213 
214  statet &new_values=*tmp_state;
215 
216  if(l->is_function_call())
217  {
218  // this is a big special case
219  const code_function_callt &code=
220  to_code_function_call(l->code);
221 
223  function_identifier,
224  l,
225  to_l,
226  code.function(),
227  code.arguments(),
228  new_values,
229  goto_functions);
230  }
231  else
232  new_values.transform(
233  ns, function_identifier, l, function_identifier, to_l);
234 
235  statet &other=get_state(to_l);
236 
237  bool have_new_values=
238  merge(other, new_values, to_l);
239 
240  if(have_new_values)
241  new_data=true;
242 
243  if(have_new_values || !other.seen)
244  put_in_working_set(working_set, to_l);
245  }
246 
247  return new_data;
248 }
249 
251  const irep_idt &calling_function,
252  locationt l_call,
253  locationt l_return,
254  const goto_functionst &goto_functions,
255  const goto_functionst::function_mapt::const_iterator f_it,
256  const exprt::operandst &,
257  statet &new_state)
258 {
259  const goto_functionst::goto_functiont &goto_function=f_it->second;
260 
261  if(!goto_function.body_available())
262  return; // do nothing
263 
264  assert(!goto_function.body.instructions.empty());
265 
266  {
267  // get the state at the beginning of the function
268  locationt l_begin=goto_function.body.instructions.begin();
269 
270  // do the edge from the call site to the beginning of the function
271  std::unique_ptr<statet> tmp_state(make_temporary_state(new_state));
272  tmp_state->transform(ns, calling_function, l_call, f_it->first, l_begin);
273 
274  statet &begin_state=get_state(l_begin);
275 
276  bool new_data=false;
277 
278  // merge the new stuff
279  if(merge(begin_state, *tmp_state, l_begin))
280  new_data=true;
281 
282  // do each function at least once
283  if(functions_done.find(f_it->first)==
284  functions_done.end())
285  {
286  new_data=true;
287  functions_done.insert(f_it->first);
288  }
289 
290  // do we need to do the fixedpoint of the body?
291  if(new_data)
292  {
293  // recursive call
294  fixedpoint(f_it->first, goto_function.body, goto_functions);
295  }
296  }
297 
298  {
299  // get location at end of procedure
300  locationt l_end=--goto_function.body.instructions.end();
301 
302  assert(l_end->is_end_function());
303 
304  statet &end_of_function=get_state(l_end);
305 
306  // do edge from end of function to instruction after call
307  std::unique_ptr<statet> tmp_state(
308  make_temporary_state(end_of_function));
309  tmp_state->transform(ns, f_it->first, l_end, calling_function, l_return);
310 
311  // propagate those -- not exceedingly precise, this is,
312  // as still it contains all the state from the
313  // call site
314  merge(new_state, *tmp_state, l_return);
315  }
316 
317  {
318  // effect on current procedure (if any)
319  new_state.transform(
320  ns, calling_function, l_call, calling_function, l_return);
321  }
322 }
323 
325  const irep_idt &calling_function,
326  locationt l_call,
327  locationt l_return,
328  const exprt &function,
329  const exprt::operandst &arguments,
330  statet &new_state,
331  const goto_functionst &goto_functions)
332 {
333  // see if we have the functions at all
334  if(goto_functions.function_map.empty())
335  return;
336 
337  if(function.id()==ID_symbol)
338  {
339  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
340 
341  if(recursion_set.find(identifier)!=recursion_set.end())
342  {
343  // recursion detected!
344  return;
345  }
346  else
347  recursion_set.insert(identifier);
348 
349  goto_functionst::function_mapt::const_iterator it=
350  goto_functions.function_map.find(identifier);
351 
352  if(it==goto_functions.function_map.end())
353  throw "failed to find function "+id2string(identifier);
354 
356  calling_function,
357  l_call,
358  l_return,
359  goto_functions,
360  it,
361  arguments,
362  new_state);
363 
364  recursion_set.erase(identifier);
365  }
366  else if(function.id()==ID_if)
367  {
368  if(function.operands().size()!=3)
369  throw "if takes three arguments";
370 
371  std::unique_ptr<statet> n2(make_temporary_state(new_state));
372 
374  calling_function,
375  l_call,
376  l_return,
377  function.op1(),
378  arguments,
379  new_state,
380  goto_functions);
381 
383  calling_function,
384  l_call,
385  l_return,
386  function.op2(),
387  arguments,
388  *n2,
389  goto_functions);
390 
391  merge(new_state, *n2, l_return);
392  }
393  else if(function.id()==ID_dereference)
394  {
395  // get value set
396  std::list<exprt> values;
397  get_reference_set(l_call, function, values);
398 
399  std::unique_ptr<statet> state_from(make_temporary_state(new_state));
400 
401  // now call all of these
402  for(const auto &value : values)
403  {
404  if(value.id()==ID_object_descriptor)
405  {
407  std::unique_ptr<statet> n2(make_temporary_state(new_state));
409  calling_function,
410  l_call,
411  l_return,
412  o.object(),
413  arguments,
414  *n2,
415  goto_functions);
416  merge(new_state, *n2, l_return);
417  }
418  }
419  }
420  else if(function.id() == ID_null_object ||
421  function.id() == ID_integer_address)
422  {
423  // ignore, can't be a function
424  }
425  else if(function.id()==ID_member || function.id()==ID_index)
426  {
427  // ignore, can't be a function
428  }
429  else if(function.id()=="builtin-function")
430  {
431  // ignore, someone else needs to worry about this
432  }
433  else
434  {
435  throw "unexpected function_call argument: "+
436  function.id_string();
437  }
438 }
439 
441  const goto_functionst &goto_functions)
442 {
443  // do each function at least once
444 
445  forall_goto_functions(it, goto_functions)
446  if(functions_done.insert(it->first).second)
447  fixedpoint(it->first, it->second.body, goto_functions);
448 }
449 
451  const goto_functionst &goto_functions)
452 {
453  sequential_fixedpoint(goto_functions);
454 
455  is_threadedt is_threaded(goto_functions);
456 
457  // construct an initial shared state collecting the results of all
458  // functions
459  goto_programt tmp;
460  tmp.add_instruction();
461  goto_programt::const_targett sh_target=tmp.instructions.begin();
462  generate_state(sh_target);
463  statet &shared_state=get_state(sh_target);
464 
465  struct wl_entryt
466  {
467  wl_entryt(
468  const irep_idt &_function_identifier,
469  const goto_programt &_goto_program,
470  locationt _location)
471  : function_identifier(_function_identifier),
472  goto_program(&_goto_program),
473  location(_location)
474  {
475  }
476 
477  irep_idt function_identifier;
478  const goto_programt *goto_program;
479  locationt location;
480  };
481 
482  typedef std::list<wl_entryt> thread_wlt;
483  thread_wlt thread_wl;
484 
485  forall_goto_functions(it, goto_functions)
486  forall_goto_program_instructions(t_it, it->second.body)
487  {
488  if(is_threaded(t_it))
489  {
490  thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
491 
493  it->second.body.instructions.end();
494  --l_end;
495 
496  const statet &end_state=get_state(l_end);
497  merge_shared(shared_state, end_state, sh_target);
498  }
499  }
500 
501  // new feed in the shared state into all concurrently executing
502  // functions, and iterate until the shared state stabilizes
503  bool new_shared=true;
504  while(new_shared)
505  {
506  new_shared=false;
507 
508  for(const auto &thread : thread_wl)
509  {
510  working_sett working_set;
511  put_in_working_set(working_set, thread.location);
512 
513  statet &begin_state = get_state(thread.location);
514  merge(begin_state, shared_state, thread.location);
515 
516  while(!working_set.empty())
517  {
518  goto_programt::const_targett l=get_next(working_set);
519 
520  visit(
521  thread.function_identifier,
522  l,
523  working_set,
524  *thread.goto_program,
525  goto_functions);
526 
527  // the underlying domain must make sure that the final state
528  // carries all possible values; otherwise we would need to
529  // merge over each and every state
530  if(l->is_end_function())
531  {
532  statet &end_state=get_state(l);
533  new_shared|=merge_shared(shared_state, end_state, sh_target);
534  }
535  }
536  }
537  }
538 }
const irept & get_nil_irep()
Definition: irep.cpp:55
static exprt get_guard(locationt from, locationt to)
const namespacet & ns
virtual std::unique_ptr< statet > make_temporary_state(statet &s)=0
Over-approximate Concurrency for Threaded Goto Programs.
std::map< unsigned, locationt > working_sett
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual statet & get_state(locationt l)=0
recursion_sett recursion_set
Deprecated expression utility functions.
void sequential_fixedpoint(const goto_functionst &goto_functions)
const irep_idt & get_identifier() const
Definition: std_expr.h:176
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2176
void do_function_call_rec(const irep_idt &calling_function, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
virtual bool merge_shared(statet &a, const statet &b, locationt to)=0
function_mapt function_map
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static exprt get_return_lhs(locationt to)
void do_function_call(const irep_idt &calling_function, locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
virtual bool has_location(locationt l) const =0
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void generate_state(locationt l)=0
functions_donet functions_done
virtual void output(const namespacet &, std::ostream &) const
void put_in_working_set(working_sett &working_set, locationt l)
The Boolean constant true.
Definition: std_expr.h:4443
argumentst & arguments()
Definition: std_code.h:1109
virtual bool merge(statet &a, const statet &b, locationt to)=0
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:415
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
::goto_functiont goto_functiont
void concurrent_fixedpoint(const goto_functionst &goto_functions)
goto_programt::const_targett locationt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
virtual void get_reference_set(locationt l, const exprt &expr, std::list< exprt > &dest)=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Static Analysis.
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
std::vector< exprt > operandst
Definition: expr.h:57
void generate_states(const goto_functionst &goto_functions)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
exprt & function()
Definition: std_code.h:1099
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
virtual void update(const goto_programt &goto_program)
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions)
locationt get_next(working_sett &working_set)
virtual void initialize(const goto_programt &goto_program)
virtual void transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:127
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173