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  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  forall_goto_functions(f_it, goto_functions)
75  {
76  if(f_it->second.body_available())
77  {
78  out << "////\n";
79  out << "//// Function: " << f_it->first << "\n";
80  out << "////\n";
81  out << "\n";
82 
83  output(f_it->second.body, f_it->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  forall_goto_functions(f_it, goto_functions)
111  generate_states(f_it->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  forall_goto_functions(f_it, goto_functions)
125  update(f_it->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  forall_goto_functions(it, goto_functions)
442  if(functions_done.insert(it->first).second)
443  fixedpoint(it->first, it->second.body, goto_functions);
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  forall_goto_functions(it, goto_functions)
482  forall_goto_program_instructions(t_it, it->second.body)
483  {
484  if(is_threaded(t_it))
485  {
486  thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
487 
489  it->second.body.instructions.end();
490  --l_end;
491 
492  const statet &end_state=get_state(l_end);
493  merge_shared(shared_state, end_state, sh_target);
494  }
495  }
496 
497  // new feed in the shared state into all concurrently executing
498  // functions, and iterate until the shared state stabilizes
499  bool new_shared=true;
500  while(new_shared)
501  {
502  new_shared=false;
503 
504  for(const auto &thread : thread_wl)
505  {
506  working_sett working_set;
507  put_in_working_set(working_set, thread.location);
508 
509  statet &begin_state = get_state(thread.location);
510  merge(begin_state, shared_state, thread.location);
511 
512  while(!working_set.empty())
513  {
514  goto_programt::const_targett l=get_next(working_set);
515 
516  visit(
517  thread.function_identifier,
518  l,
519  working_set,
520  *thread.goto_program,
521  goto_functions);
522 
523  // the underlying domain must make sure that the final state
524  // carries all possible values; otherwise we would need to
525  // merge over each and every state
526  if(l->is_end_function())
527  {
528  statet &end_state=get_state(l);
529  new_shared|=merge_shared(shared_state, end_state, sh_target);
530  }
531  }
532  }
533  }
534 }
static_analysis_baset::sequential_fixedpoint
void sequential_fixedpoint(const goto_functionst &goto_functions)
Definition: static_analysis.cpp:436
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:70
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:246
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:3029
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
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:53
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:189
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:1084
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:1208
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
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:320
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:694
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:41
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:127
is_threaded.h
Over-approximate Concurrency for Threaded Goto Programs.
static_analysis_baset::operator()
virtual void operator()(const irep_idt &function_identifier, const goto_programt &goto_program)
Definition: static_analysis.cpp:61
domain_baset::seen
bool seen
Definition: static_analysis.h:92
to_object_descriptor_expr
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:1898
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:177
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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:1228
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:107
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
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:73
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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: std_expr.h:1858
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
std_expr.h
API to expression classes.
static_analysis_baset::update
virtual void update(const goto_programt &goto_program)
Definition: static_analysis.cpp:128
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:1218
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
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:162
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:150