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 
28  locationt next=from;
29  next++;
30 
31  if(next==to)
32  return boolean_negate(from->guard);
33 
34  return from->guard;
35 }
36 
38 {
39  // get predecessor of "to"
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  return to_code_function_call(to->code).lhs();
47 }
48 
50  const goto_functionst &goto_functions)
51 {
52  initialize(goto_functions);
53  fixedpoint(goto_functions);
54 }
55 
57  const goto_programt &goto_program)
58 {
59  initialize(goto_program);
60  goto_functionst goto_functions;
61  fixedpoint(goto_program, goto_functions);
62 }
63 
65  const goto_functionst &goto_functions,
66  std::ostream &out)
67 {
68  forall_goto_functions(f_it, goto_functions)
69  {
70  out << "////\n" << "//// Function: " << f_it->first << "\n////\n\n";
71 
72  output(f_it->second.body, f_it->first, out);
73  }
74 }
75 
77  const goto_programt &,
78  const irep_idt &,
79  std::ostream &out) const
80 {
81  get_state().output(ns, out);
82 }
83 
86  working_sett &working_set)
87 {
88  assert(!working_set.empty());
89 
90 // working_sett::iterator i=working_set.begin();
91 // locationt l=i->second;
92 // working_set.erase(i);
93 
94 // pop_heap(working_set.begin(), working_set.end());
95  locationt l=working_set.top();
96  working_set.pop();
97 
98  return l;
99 }
100 
102  const goto_programt &goto_program,
103  const goto_functionst &goto_functions)
104 {
105  if(goto_program.instructions.empty())
106  return false;
107 
108  working_sett working_set;
109 
110 // make_heap(working_set.begin(), working_set.end());
111 
113  working_set,
114  goto_program.instructions.begin());
115 
116  bool new_data=false;
117 
118  while(!working_set.empty())
119  {
120  locationt l=get_next(working_set);
121 
122  if(visit(l, working_set, goto_program, goto_functions))
123  new_data=true;
124  }
125 
126  return new_data;
127 }
128 
130  locationt l,
131  working_sett &working_set,
132  const goto_programt &goto_program,
133  const goto_functionst &goto_functions)
134 {
135  bool new_data=false;
136 
137  #if 0
138  std::cout << "Visiting: " << l->function << " " <<
139  l->location_number << '\n';
140  #endif
141 
142  seen_locations.insert(l);
143  if(statistics.find(l)==statistics.end())
144  statistics[l]=1;
145  else
146  statistics[l]++;
147 
148  for(const auto &to_l : goto_program.get_successors(l))
149  {
150  if(to_l==goto_program.instructions.end())
151  continue;
152 
153  bool changed=false;
154 
155  if(l->is_function_call())
156  {
157  // this is a big special case
158  const code_function_callt &code = to_code_function_call(l->code);
159 
160  changed=
162  l,
163  code.function(),
164  code.arguments(),
165  get_state(),
166  goto_functions);
167  }
168  else
169  changed = get_state().transform(ns, l, to_l);
170 
171  if(changed || !seen(to_l))
172  {
173  new_data=true;
174  put_in_working_set(working_set, to_l);
175  }
176  }
177 
178 // if (id2string(l->function).find("debug")!=std::string::npos)
179 // std::cout << l->function << '\n'; //=="messages::debug")
180 
181 // {
182 // static unsigned state_cntr=0;
183 // std::string s("pastate"); s += std::to_string(state_cntr);
184 // std::ofstream f(s.c_str());
185 // goto_program.output_instruction(ns, "", f, l);
186 // f << '\n';
187 // get_state().output(ns, f);
188 // f.close();
189 // state_cntr++;
190 // }
191 
192  return new_data;
193 }
194 
196  locationt l_call,
197  const goto_functionst &goto_functions,
198  const goto_functionst::function_mapt::const_iterator f_it,
199  const exprt::operandst &,
200  statet &state)
201 {
202  const goto_functionst::goto_functiont &goto_function=f_it->second;
203 
204  if(!goto_function.body_available())
205  {
206  const code_function_callt &code = to_code_function_call(l_call->code);
207 
208  goto_programt temp;
209 
210  exprt rhs =
212 
214  r->make_return();
215  r->code=code_returnt(rhs);
216  r->function=f_it->first;
217  r->location_number=0;
218 
220  t->code.set(ID_identifier, code.function());
221  t->function=f_it->first;
222  t->location_number=1;
223 
224  locationt l_next=l_call; l_next++;
225  bool new_data=state.transform(ns, l_call, r);
226  new_data = state.transform(ns, r, t) || new_data;
227  new_data = state.transform(ns, t, l_next) || new_data;
228 
229  return new_data;
230  }
231 
232  assert(!goto_function.body.instructions.empty());
233 
234  bool new_data=false;
235 
236  {
237  // get the state at the beginning of the function
238  locationt l_begin=goto_function.body.instructions.begin();
239 
241  l_begin->function == f_it->first, "function names have to match");
242 
243  // do the edge from the call site to the beginning of the function
244  new_data=state.transform(ns, l_call, l_begin);
245 
246  // do each function at least once
247  if(functions_done.find(f_it->first)==
248  functions_done.end())
249  {
250  new_data=true;
251  functions_done.insert(f_it->first);
252  }
253 
254  // do we need to do the fixedpoint of the body?
255  if(new_data)
256  {
257  // recursive call
258  fixedpoint(goto_function.body, goto_functions);
259  new_data=true; // could be reset by fixedpoint
260  }
261  }
262 
263  {
264  // get location at end of procedure
265  locationt l_end=--goto_function.body.instructions.end();
266 
267  assert(l_end->is_end_function());
268 
269  // do edge from end of function to instruction after call
270  locationt l_next=l_call;
271  l_next++;
272  new_data = state.transform(ns, l_end, l_next) || new_data;
273  }
274 
275  return new_data;
276 }
277 
279  locationt l_call,
280  const exprt &function,
281  const exprt::operandst &arguments,
282  statet &state,
283  const goto_functionst &goto_functions)
284 {
285  bool new_data = false;
286 
287  if(function.id()==ID_symbol)
288  {
289  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
290 
291  if(recursion_set.find(identifier)!=recursion_set.end())
292  {
293  // recursion detected!
294  return false;
295  }
296  else
297  recursion_set.insert(identifier);
298 
299  goto_functionst::function_mapt::const_iterator it=
300  goto_functions.function_map.find(identifier);
301 
302  if(it==goto_functions.function_map.end())
303  throw "failed to find function "+id2string(identifier);
304 
305  new_data =
307  l_call,
308  goto_functions,
309  it,
310  arguments,
311  state);
312 
313  recursion_set.erase(identifier);
314  }
315  else if(function.id()==ID_if)
316  {
317  const auto &if_expr = to_if_expr(function);
318 
319  new_data = do_function_call_rec(
320  l_call, if_expr.true_case(), arguments, state, goto_functions);
321 
322  new_data =
324  l_call, if_expr.false_case(), arguments, state, goto_functions) ||
325  new_data;
326  }
327  else if(function.id()==ID_dereference)
328  {
329  // get value set
330  expr_sett values;
331 
332  get_reference_set(function, values);
333 
334  // now call all of these
335  for(const auto &v : values)
336  {
337  if(v.id()==ID_object_descriptor)
338  {
340 
341  // ... but only if they are actually functions.
342  goto_functionst::function_mapt::const_iterator it=
343  goto_functions.function_map.find(o.object().get(ID_identifier));
344 
345  if(it!=goto_functions.function_map.end())
346  {
347  new_data =
349  l_call,
350  o.object(),
351  arguments,
352  state,
353  goto_functions) || new_data;
354  }
355  }
356  }
357  }
358  else if(function.id() == ID_null_object)
359  {
360  // ignore, can't be a function
361  }
362  else if(function.id()==ID_member || function.id()==ID_index)
363  {
364  // ignore, can't be a function
365  }
366  else if(function.id()=="builtin-function")
367  {
368  // ignore
369  }
370  else
371  {
372  throw "unexpected function_call argument: "+
373  function.id_string();
374  }
375  return new_data;
376 }
377 
379  const goto_functionst &goto_functions)
380 {
381  // do each function at least once
382 
383  forall_goto_functions(it, goto_functions)
384  if(functions_done.find(it->first)==
385  functions_done.end())
386  {
387  fixedpoint(it, goto_functions);
388  }
389 }
390 
392  const goto_functionst::function_mapt::const_iterator it,
393  const goto_functionst &goto_functions)
394 {
395  functions_done.insert(it->first);
396  return fixedpoint(it->second.body, goto_functions);
397 }
398 
400 {
401  // no need to copy value sets around
402 }
403 
405 {
406  // no need to copy value sets around
407 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
const irept & get_nil_irep()
Definition: irep.cpp:55
static int8_t r
Definition: irep_hash.h:59
std::map< locationt, unsigned > statistics
exprt get_guard(locationt from, locationt to) const
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
virtual void get_reference_set(const exprt &expr, expr_sett &expr_set)=0
Deprecated expression utility functions.
const irep_idt & get_identifier() const
Definition: std_expr.h:176
virtual void operator()(const goto_programt &goto_program)
locationt get_next(working_sett &working_set)
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
Definition: std_expr.h:2176
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
function_mapt function_map
typet & type()
Return the type of the expression.
Definition: expr.h:68
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void update(const goto_programt &goto_program)
virtual statet & get_state()=0
goto_programt::const_targett locationt
The Boolean constant true.
Definition: std_expr.h:4443
argumentst & arguments()
Definition: std_code.h:1109
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
instructionst::iterator targett
Definition: goto_program.h:414
bool do_function_call(locationt l_call, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, statet &new_state)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
::goto_functiont goto_functiont
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
codet representation of a function call statement.
Definition: std_code.h:1036
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
std::vector< exprt > operandst
Definition: expr.h:57
const source_locationt & source_location() const
Definition: type.h:62
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Flow Insensitive Static Analysis.
exprt & function()
Definition: std_code.h:1099
virtual void initialize(const goto_programt &)
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
#define forall_goto_functions(it, functions)
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
void put_in_working_set(working_sett &working_set, locationt l)
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
std::priority_queue< locationt > working_sett
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
virtual void output(const namespacet &, std::ostream &) const