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