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/std_expr.h>
19 #include <util/std_code.h>
20 
21 #include "is_threaded.h"
22 
24  locationt from,
25  locationt to)
26 {
27  if(!from->is_goto())
28  return true_exprt();
29 
30  locationt next=from;
31  next++;
32 
33  if(next==to)
34  {
35  exprt tmp(from->guard);
36  tmp.make_not();
37  return tmp;
38  }
39 
40  return from->guard;
41 }
42 
44 {
45  // get predecessor of "to"
46 
47  to--;
48 
49  if(to->is_end_function())
50  return static_cast<const exprt &>(get_nil_irep());
51 
52  // must be the function call
53  assert(to->is_function_call());
54 
55  const code_function_callt &code=
56  to_code_function_call(to->code);
57 
58  return code.lhs();
59 }
60 
62  const goto_functionst &goto_functions)
63 {
64  initialize(goto_functions);
65  fixedpoint(goto_functions);
66 }
67 
70 {
72  goto_functionst goto_functions;
73  fixedpoint(goto_program, goto_functions);
74 }
75 
77  const goto_functionst &goto_functions,
78  std::ostream &out) const
79 {
80  forall_goto_functions(f_it, goto_functions)
81  {
82  if(f_it->second.body_available())
83  {
84  out << "////\n";
85  out << "//// Function: " << f_it->first << "\n";
86  out << "////\n";
87  out << "\n";
88 
89  output(f_it->second.body, f_it->first, out);
90  }
91  }
92 }
93 
96  const irep_idt &,
97  std::ostream &out) const
98 {
100  {
101  out << "**** " << i_it->location_number << " "
102  << i_it->source_location << "\n";
103 
104  get_state(i_it).output(ns, out);
105  out << "\n";
106  #if 0
107  goto_program.output_instruction(ns, identifier, out, i_it);
108  out << "\n";
109  #endif
110  }
111 }
112 
114  const goto_functionst &goto_functions)
115 {
116  forall_goto_functions(f_it, goto_functions)
117  generate_states(f_it->second.body);
118 }
119 
122 {
124  generate_state(i_it);
125 }
126 
128  const goto_functionst &goto_functions)
129 {
130  forall_goto_functions(f_it, goto_functions)
131  update(f_it->second.body);
132 }
133 
136 {
137  locationt previous;
138  bool first=true;
139 
141  {
142  // do we have it already?
143  if(!has_location(i_it))
144  {
145  generate_state(i_it);
146 
147  if(!first)
148  merge(get_state(i_it), get_state(previous), i_it);
149  }
150 
151  first=false;
152  previous=i_it;
153  }
154 }
155 
157  working_sett &working_set)
158 {
159  assert(!working_set.empty());
160 
161  working_sett::iterator i=working_set.begin();
162  locationt l=i->second;
163  working_set.erase(i);
164 
165  return l;
166 }
167 
170  const goto_functionst &goto_functions)
171 {
172  if(goto_program.instructions.empty())
173  return false;
174 
175  working_sett working_set;
176 
178  working_set,
179  goto_program.instructions.begin());
180 
181  bool new_data=false;
182 
183  while(!working_set.empty())
184  {
185  locationt l=get_next(working_set);
186 
187  if(visit(l, working_set, goto_program, goto_functions))
188  new_data=true;
189  }
190 
191  return new_data;
192 }
193 
195  locationt l,
196  working_sett &working_set,
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  l, to_l,
224  code.function(),
225  code.arguments(),
226  new_values,
227  goto_functions);
228  }
229  else
230  new_values.transform(ns, l, to_l);
231 
232  statet &other=get_state(to_l);
233 
234  bool have_new_values=
235  merge(other, new_values, to_l);
236 
237  if(have_new_values)
238  new_data=true;
239 
240  if(have_new_values || !other.seen)
241  put_in_working_set(working_set, to_l);
242  }
243 
244  return new_data;
245 }
246 
248  locationt l_call, locationt l_return,
249  const goto_functionst &goto_functions,
250  const goto_functionst::function_mapt::const_iterator f_it,
251  const exprt::operandst &,
252  statet &new_state)
253 {
254  const goto_functionst::goto_functiont &goto_function=f_it->second;
255 
256  if(!goto_function.body_available())
257  return; // do nothing
258 
259  assert(!goto_function.body.instructions.empty());
260 
261  {
262  // get the state at the beginning of the function
263  locationt l_begin=goto_function.body.instructions.begin();
264 
265  // do the edge from the call site to the beginning of the function
266  std::unique_ptr<statet> tmp_state(make_temporary_state(new_state));
267  tmp_state->transform(ns, l_call, l_begin);
268 
269  statet &begin_state=get_state(l_begin);
270 
271  bool new_data=false;
272 
273  // merge the new stuff
274  if(merge(begin_state, *tmp_state, l_begin))
275  new_data=true;
276 
277  // do each function at least once
278  if(functions_done.find(f_it->first)==
279  functions_done.end())
280  {
281  new_data=true;
282  functions_done.insert(f_it->first);
283  }
284 
285  // do we need to do the fixedpoint of the body?
286  if(new_data)
287  {
288  // recursive call
289  fixedpoint(goto_function.body, goto_functions);
290  }
291  }
292 
293  {
294  // get location at end of procedure
295  locationt l_end=--goto_function.body.instructions.end();
296 
297  assert(l_end->is_end_function());
298 
299  statet &end_of_function=get_state(l_end);
300 
301  // do edge from end of function to instruction after call
302  std::unique_ptr<statet> tmp_state(
303  make_temporary_state(end_of_function));
304  tmp_state->transform(ns, l_end, l_return);
305 
306  // propagate those -- not exceedingly precise, this is,
307  // as still it contains all the state from the
308  // call site
309  merge(new_state, *tmp_state, l_return);
310  }
311 
312  {
313  // effect on current procedure (if any)
314  new_state.transform(ns, l_call, l_return);
315  }
316 }
317 
319  locationt l_call, locationt l_return,
320  const exprt &function,
321  const exprt::operandst &arguments,
322  statet &new_state,
323  const goto_functionst &goto_functions)
324 {
325  // see if we have the functions at all
326  if(goto_functions.function_map.empty())
327  return;
328 
329  if(function.id()==ID_symbol)
330  {
331  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
332 
333  if(recursion_set.find(identifier)!=recursion_set.end())
334  {
335  // recursion detected!
336  return;
337  }
338  else
339  recursion_set.insert(identifier);
340 
341  goto_functionst::function_mapt::const_iterator it=
342  goto_functions.function_map.find(identifier);
343 
344  if(it==goto_functions.function_map.end())
345  throw "failed to find function "+id2string(identifier);
346 
348  l_call, l_return,
349  goto_functions,
350  it,
351  arguments,
352  new_state);
353 
354  recursion_set.erase(identifier);
355  }
356  else if(function.id()==ID_if)
357  {
358  if(function.operands().size()!=3)
359  throw "if takes three arguments";
360 
361  std::unique_ptr<statet> n2(make_temporary_state(new_state));
362 
364  l_call, l_return,
365  function.op1(),
366  arguments,
367  new_state,
368  goto_functions);
369 
371  l_call, l_return,
372  function.op2(),
373  arguments,
374  *n2,
375  goto_functions);
376 
377  merge(new_state, *n2, l_return);
378  }
379  else if(function.id()==ID_dereference)
380  {
381  // get value set
382  std::list<exprt> values;
383  get_reference_set(l_call, function, values);
384 
385  std::unique_ptr<statet> state_from(make_temporary_state(new_state));
386 
387  // now call all of these
388  for(const auto &value : values)
389  {
390  if(value.id()==ID_object_descriptor)
391  {
393  std::unique_ptr<statet> n2(make_temporary_state(new_state));
395  l_call, l_return, o.object(), arguments, *n2, goto_functions);
396  merge(new_state, *n2, l_return);
397  }
398  }
399  }
400  else if(function.id() == ID_null_object ||
401  function.id() == ID_integer_address)
402  {
403  // ignore, can't be a function
404  }
405  else if(function.id()==ID_member || function.id()==ID_index)
406  {
407  // ignore, can't be a function
408  }
409  else if(function.id()=="builtin-function")
410  {
411  // ignore, someone else needs to worry about this
412  }
413  else
414  {
415  throw "unexpected function_call argument: "+
416  function.id_string();
417  }
418 }
419 
421  const goto_functionst &goto_functions)
422 {
423  // do each function at least once
424 
425  forall_goto_functions(it, goto_functions)
426  if(functions_done.insert(it->first).second)
427  fixedpoint(it->second.body, goto_functions);
428 }
429 
431  const goto_functionst &goto_functions)
432 {
433  sequential_fixedpoint(goto_functions);
434 
435  is_threadedt is_threaded(goto_functions);
436 
437  // construct an initial shared state collecting the results of all
438  // functions
439  goto_programt tmp;
440  tmp.add_instruction();
441  goto_programt::const_targett sh_target=tmp.instructions.begin();
442  generate_state(sh_target);
443  statet &shared_state=get_state(sh_target);
444 
445  typedef std::list<std::pair<goto_programt const*,
446  goto_programt::const_targett> > thread_wlt;
447  thread_wlt thread_wl;
448 
449  forall_goto_functions(it, goto_functions)
450  forall_goto_program_instructions(t_it, it->second.body)
451  {
452  if(is_threaded(t_it))
453  {
454  thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
455 
457  it->second.body.instructions.end();
458  --l_end;
459 
460  const statet &end_state=get_state(l_end);
461  merge_shared(shared_state, end_state, sh_target);
462  }
463  }
464 
465  // new feed in the shared state into all concurrently executing
466  // functions, and iterate until the shared state stabilizes
467  bool new_shared=true;
468  while(new_shared)
469  {
470  new_shared=false;
471 
472  for(const auto &thread : thread_wl)
473  {
474  working_sett working_set;
475  put_in_working_set(working_set, thread.second);
476 
477  statet &begin_state=get_state(thread.second);
478  merge(begin_state, shared_state, thread.second);
479 
480  while(!working_set.empty())
481  {
482  goto_programt::const_targett l=get_next(working_set);
483 
484  visit(l, working_set, *thread.first, goto_functions);
485 
486  // the underlying domain must make sure that the final state
487  // carries all possible values; otherwise we would need to
488  // merge over each and every state
489  if(l->is_end_function())
490  {
491  statet &end_state=get_state(l);
492  new_shared|=merge_shared(shared_state, end_state, sh_target);
493  }
494  }
495  }
496  }
497 }
const irept & get_nil_irep()
Definition: irep.cpp:56
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
void sequential_fixedpoint(const goto_functionst &goto_functions)
virtual void transform(const namespacet &ns, locationt from, locationt to)=0
const irep_idt & get_identifier() const
Definition: std_expr.h:128
virtual void output(const goto_functionst &goto_functions, std::ostream &out) const
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 merge_shared(statet &a, const statet &b, locationt to)=0
function_mapt function_map
static exprt get_return_lhs(locationt to)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual bool has_location(locationt l) const =0
virtual void generate_state(locationt l)=0
functions_donet functions_done
virtual void output(const namespacet &, std::ostream &) const
void do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
void put_in_working_set(working_sett &working_set, locationt l)
The boolean constant true.
Definition: std_expr.h:4486
argumentst & arguments()
Definition: std_code.h:890
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:403
API to expression classes.
instructionst::const_iterator const_targett
Definition: goto_program.h:398
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
::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: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
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:33
Static Analysis.
std::vector< exprt > operandst
Definition: expr.h:45
void generate_states(const goto_functionst &goto_functions)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
void make_not()
Definition: expr.cpp:91
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
virtual void operator()(const goto_programt &goto_program)
virtual void update(const goto_programt &goto_program)
goto_programt & goto_program
Definition: cover.cpp:63
locationt get_next(working_sett &working_set)
void do_function_call(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 void initialize(const goto_programt &goto_program)
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909