cprover
flow_insensitive_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Flow Insensitive Static Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
14 
15 #include <cassert>
16 
17 #include <util/expr_util.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 
22  locationt from,
23  locationt to) const
24 {
25  if(!from->is_goto())
26  return true_exprt();
27  else if(std::next(from) == to)
28  return boolean_negate(from->get_condition());
29  else
30  return from->get_condition();
31 }
32 
34 {
35  // get predecessor of "to"
36  to--;
37 
38  if(to->is_end_function())
39  return static_cast<const exprt &>(get_nil_irep());
40 
41  // must be the function call
42  return to_code_function_call(to->code).lhs();
43 }
44 
46  const goto_functionst &goto_functions)
47 {
48  initialize(goto_functions);
49  fixedpoint(goto_functions);
50 }
51 
53 operator()(const irep_idt &function_id, const goto_programt &goto_program)
54 {
55  initialize(goto_program);
56  goto_functionst goto_functions;
57  fixedpoint(function_id, goto_program, goto_functions);
58 }
59 
61  const goto_functionst &goto_functions,
62  std::ostream &out)
63 {
64  forall_goto_functions(f_it, goto_functions)
65  {
66  out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
67 
68  output(f_it->first, f_it->second.body, out);
69  }
70 }
71 
73  const irep_idt &,
74  const goto_programt &,
75  std::ostream &out)
76 {
77  get_state().output(ns, out);
78 }
79 
82  working_sett &working_set)
83 {
84  assert(!working_set.empty());
85 
86 // working_sett::iterator i=working_set.begin();
87 // locationt l=i->second;
88 // working_set.erase(i);
89 
90 // pop_heap(working_set.begin(), working_set.end());
91  locationt l=working_set.top();
92  working_set.pop();
93 
94  return l;
95 }
96 
98  const irep_idt &function_id,
99  const goto_programt &goto_program,
100  const goto_functionst &goto_functions)
101 {
102  if(goto_program.instructions.empty())
103  return false;
104 
105  working_sett working_set;
106 
107 // make_heap(working_set.begin(), working_set.end());
108 
110  working_set,
111  goto_program.instructions.begin());
112 
113  bool new_data=false;
114 
115  while(!working_set.empty())
116  {
117  locationt l=get_next(working_set);
118 
119  if(visit(function_id, l, working_set, goto_program, goto_functions))
120  new_data=true;
121  }
122 
123  return new_data;
124 }
125 
127  const irep_idt &function_id,
128  locationt l,
129  working_sett &working_set,
130  const goto_programt &goto_program,
131  const goto_functionst &goto_functions)
132 {
133  bool new_data=false;
134 
135  #if 0
136  std::cout << "Visiting: " << l->function << " " <<
137  l->location_number << '\n';
138  #endif
139 
140  seen_locations.insert(l);
141  if(statistics.find(l)==statistics.end())
142  statistics[l]=1;
143  else
144  statistics[l]++;
145 
146  for(const auto &to_l : goto_program.get_successors(l))
147  {
148  if(to_l==goto_program.instructions.end())
149  continue;
150 
151  bool changed=false;
152 
153  if(l->is_function_call())
154  {
155  // this is a big special case
156  const code_function_callt &code = to_code_function_call(l->code);
157 
158  changed = do_function_call_rec(
159  function_id,
160  l,
161  code.function(),
162  code.arguments(),
163  get_state(),
164  goto_functions);
165  }
166  else
167  changed = get_state().transform(ns, function_id, l, function_id, to_l);
168 
169  if(changed || !seen(to_l))
170  {
171  new_data=true;
172  put_in_working_set(working_set, to_l);
173  }
174  }
175 
176 // if (id2string(l->function).find("debug")!=std::string::npos)
177 // std::cout << l->function << '\n'; //=="messages::debug")
178 
179 // {
180 // static unsigned state_cntr=0;
181 // std::string s("pastate"); s += std::to_string(state_cntr);
182 // std::ofstream f(s.c_str());
183 // goto_program.output_instruction(ns, "", f, l);
184 // f << '\n';
185 // get_state().output(ns, f);
186 // f.close();
187 // state_cntr++;
188 // }
189 
190  return new_data;
191 }
192 
194  const irep_idt &calling_function,
195  locationt l_call,
196  const goto_functionst &goto_functions,
197  const goto_functionst::function_mapt::const_iterator f_it,
198  const exprt::operandst &,
199  statet &state)
200 {
201  const goto_functionst::goto_functiont &goto_function=f_it->second;
202 
203  if(!goto_function.body_available())
204  {
205  const code_function_callt &code = to_code_function_call(l_call->code);
206 
207  goto_programt temp;
208 
210  side_effect_expr_nondett(code.lhs().type(), l_call->source_location))));
211  r->location_number=0;
212 
214  t->location_number=1;
215 
216  locationt l_next=l_call; l_next++;
217  // do the edge from the call site to the simulated function (the artificial
218  // return statement that we just generated)
219  bool new_data =
220  state.transform(ns, calling_function, l_call, f_it->first, r);
221  // do the edge from the return to the artificial end-of-function
222  new_data = state.transform(ns, f_it->first, r, f_it->first, t) || new_data;
223  // do edge from (artificial) end of function to instruction after call
224  new_data =
225  state.transform(ns, f_it->first, t, calling_function, l_next) || new_data;
226 
227  return new_data;
228  }
229 
230  assert(!goto_function.body.instructions.empty());
231 
232  bool new_data=false;
233 
234  {
235  // get the state at the beginning of the function
236  locationt l_begin=goto_function.body.instructions.begin();
237 
238  // do the edge from the call site to the beginning of the function
239  new_data =
240  state.transform(ns, calling_function, l_call, f_it->first, l_begin);
241 
242  // do each function at least once
243  if(functions_done.find(f_it->first)==
244  functions_done.end())
245  {
246  new_data=true;
247  functions_done.insert(f_it->first);
248  }
249 
250  // do we need to do the fixedpoint of the body?
251  if(new_data)
252  {
253  // recursive call
254  fixedpoint(f_it->first, goto_function.body, goto_functions);
255  new_data=true; // could be reset by fixedpoint
256  }
257  }
258 
259  {
260  // get location at end of procedure
261  locationt l_end=--goto_function.body.instructions.end();
262 
263  assert(l_end->is_end_function());
264 
265  // do edge from end of function to instruction after call
266  locationt l_next=l_call;
267  l_next++;
268  new_data =
269  state.transform(ns, f_it->first, l_end, calling_function, l_next) ||
270  new_data;
271  }
272 
273  return new_data;
274 }
275 
277  const irep_idt &calling_function,
278  locationt l_call,
279  const exprt &function,
280  const exprt::operandst &arguments,
281  statet &state,
282  const goto_functionst &goto_functions)
283 {
284  bool new_data = false;
285 
286  if(function.id()==ID_symbol)
287  {
288  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
289 
290  if(recursion_set.find(identifier)!=recursion_set.end())
291  {
292  // recursion detected!
293  return false;
294  }
295  else
296  recursion_set.insert(identifier);
297 
298  goto_functionst::function_mapt::const_iterator it=
299  goto_functions.function_map.find(identifier);
300 
301  if(it==goto_functions.function_map.end())
302  throw "failed to find function "+id2string(identifier);
303 
304  new_data = do_function_call(
305  calling_function, l_call, goto_functions, it, arguments, state);
306 
307  recursion_set.erase(identifier);
308  }
309  else if(function.id()==ID_if)
310  {
311  const auto &if_expr = to_if_expr(function);
312 
313  new_data = do_function_call_rec(
314  calling_function,
315  l_call,
316  if_expr.true_case(),
317  arguments,
318  state,
319  goto_functions);
320 
321  new_data = do_function_call_rec(
322  calling_function,
323  l_call,
324  if_expr.false_case(),
325  arguments,
326  state,
327  goto_functions) ||
328  new_data;
329  }
330  else if(function.id()==ID_dereference)
331  {
332  // get value set
333  expr_sett values;
334 
335  get_reference_set(function, values);
336 
337  // now call all of these
338  for(const auto &v : values)
339  {
340  if(v.id()==ID_object_descriptor)
341  {
343 
344  // ... but only if they are actually functions.
345  goto_functionst::function_mapt::const_iterator it=
346  goto_functions.function_map.find(o.object().get(ID_identifier));
347 
348  if(it!=goto_functions.function_map.end())
349  {
350  new_data = do_function_call_rec(
351  calling_function,
352  l_call,
353  o.object(),
354  arguments,
355  state,
356  goto_functions) ||
357  new_data;
358  }
359  }
360  }
361  }
362  else if(function.id() == ID_null_object)
363  {
364  // ignore, can't be a function
365  }
366  else if(function.id()==ID_member || function.id()==ID_index)
367  {
368  // ignore, can't be a function
369  }
370  else if(function.id()=="builtin-function")
371  {
372  // ignore
373  }
374  else
375  {
376  throw "unexpected function_call argument: "+
377  function.id_string();
378  }
379  return new_data;
380 }
381 
383  const goto_functionst &goto_functions)
384 {
385  // do each function at least once
386 
387  forall_goto_functions(it, goto_functions)
388  if(functions_done.find(it->first)==
389  functions_done.end())
390  {
391  fixedpoint(it, goto_functions);
392  }
393 }
394 
396  const goto_functionst::function_mapt::const_iterator it,
397  const goto_functionst &goto_functions)
398 {
399  functions_done.insert(it->first);
400  return fixedpoint(it->first, it->second.body, goto_functions);
401 }
402 
404 {
405  // no need to copy value sets around
406 }
407 
409 {
410  // no need to copy value sets around
411 }
flow_insensitive_analysis_baset::update
virtual void update(const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:408
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
flow_insensitive_analysis_baset::get_state
virtual statet & get_state()=0
flow_insensitive_analysis_baset::visit
bool visit(const irep_idt &function_id, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:126
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
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
exprt
Base class for all expressions.
Definition: expr.h:53
flow_insensitive_analysis_baset::recursion_set
recursion_sett recursion_set
Definition: flow_insensitive_analysis.h:200
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
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
flow_insensitive_analysis_baset::working_sett
std::priority_queue< locationt > working_sett
Definition: flow_insensitive_analysis.h:158
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition: flow_insensitive_analysis.cpp:33
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
flow_insensitive_analysis_baset::initialize
virtual void initialize(const goto_programt &)
Definition: flow_insensitive_analysis.h:111
flow_insensitive_analysis_baset::seen_locations
std::set< locationt > seen_locations
Definition: flow_insensitive_analysis.h:96
flow_insensitive_abstract_domain_baset::output
virtual void output(const namespacet &, std::ostream &) const
Definition: flow_insensitive_analysis.h:59
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
flow_insensitive_analysis_baset::do_function_call_rec
bool do_function_call_rec(const irep_idt &calling_function, locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:276
flow_insensitive_analysis_baset::fixedpoint
bool fixedpoint(const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:97
flow_insensitive_analysis_baset::operator()
virtual void operator()(const irep_idt &function_id, const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:53
flow_insensitive_analysis_baset::get_reference_set
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
flow_insensitive_abstract_domain_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:44
flow_insensitive_analysis_baset::functions_done
functions_donet functions_done
Definition: flow_insensitive_analysis.h:197
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
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
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
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
flow_insensitive_analysis_baset::put_in_working_set
void put_in_working_set(working_sett &working_set, locationt l)
Definition: flow_insensitive_analysis.h:162
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
flow_insensitive_analysis.h
Flow Insensitive Static Analysis.
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:838
flow_insensitive_analysis_baset::output
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
Definition: flow_insensitive_analysis.cpp:60
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
flow_insensitive_analysis_baset::do_function_call
bool do_function_call(const irep_idt &calling_function, locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
Definition: flow_insensitive_analysis.cpp:193
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
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.
flow_insensitive_analysis_baset::statistics
std::map< locationt, unsigned > statistics
Definition: flow_insensitive_analysis.h:98
flow_insensitive_abstract_domain_baset::get_guard
exprt get_guard(locationt from, locationt to) const
Definition: flow_insensitive_analysis.cpp:21
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:94
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1310
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
flow_insensitive_abstract_domain_baset::transform
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to)=0
flow_insensitive_analysis_baset::expr_sett
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
Definition: flow_insensitive_analysis.h:226
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
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
flow_insensitive_abstract_domain_baset
Definition: flow_insensitive_analysis.h:37
r
static int8_t r
Definition: irep_hash.h:59
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:1858
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
flow_insensitive_analysis_baset::seen
bool seen(const locationt &l)
Definition: flow_insensitive_analysis.h:100
flow_insensitive_analysis_baset::get_next
locationt get_next(working_sett &working_set)
Definition: flow_insensitive_analysis.cpp:81
std_expr.h
API to expression classes.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
code_function_callt::function
exprt & function()
Definition: std_code.h:1218