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