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 }
flow_insensitive_analysis_baset::update
virtual void update(const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:404
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
flow_insensitive_analysis_baset::get_state
virtual statet & get_state()=0
flow_insensitive_analysis_baset::do_function_call
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)
Definition: flow_insensitive_analysis.cpp:195
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
exprt
Base class for all expressions.
Definition: expr.h:54
flow_insensitive_analysis_baset::do_function_call_rec
bool do_function_call_rec(locationt l_call, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:278
flow_insensitive_analysis_baset::recursion_set
recursion_sett recursion_set
Definition: flow_insensitive_analysis.h:203
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
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:163
flow_insensitive_abstract_domain_baset::get_return_lhs
exprt get_return_lhs(locationt to) const
Definition: flow_insensitive_analysis.cpp:37
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
flow_insensitive_analysis_baset::initialize
virtual void initialize(const goto_programt &)
Definition: flow_insensitive_analysis.h:109
flow_insensitive_analysis_baset::seen_locations
std::set< locationt > seen_locations
Definition: flow_insensitive_analysis.h:94
flow_insensitive_abstract_domain_baset::output
virtual void output(const namespacet &, std::ostream &) const
Definition: flow_insensitive_analysis.h:57
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
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:200
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:62
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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
flow_insensitive_analysis_baset::operator()
virtual void operator()(const goto_programt &goto_program)
Definition: flow_insensitive_analysis.cpp:56
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:2176
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
flow_insensitive_analysis_baset::put_in_working_set
void put_in_working_set(working_sett &working_set, locationt l)
Definition: flow_insensitive_analysis.h:167
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
END_FUNCTION
Definition: goto_program.h:42
flow_insensitive_analysis.h
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
flow_insensitive_analysis_baset::fixedpoint
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:101
flow_insensitive_analysis_baset::output
virtual void output(const goto_functionst &goto_functions, std::ostream &out)
Definition: flow_insensitive_analysis.cpp:64
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
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:420
expr_util.h
Deprecated expression utility functions.
flow_insensitive_analysis_baset::statistics
std::map< locationt, unsigned > statistics
Definition: flow_insensitive_analysis.h:96
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:22
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:92
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1191
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
flow_insensitive_analysis_baset::expr_sett
flow_insensitive_abstract_domain_baset::expr_sett expr_sett
Definition: flow_insensitive_analysis.h:227
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
flow_insensitive_abstract_domain_baset
Definition: flow_insensitive_analysis.h:36
r
static int8_t r
Definition: irep_hash.h:59
flow_insensitive_analysis_baset::visit
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions)
Definition: flow_insensitive_analysis.cpp:129
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:2147
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
flow_insensitive_analysis_baset::seen
bool seen(const locationt &l)
Definition: flow_insensitive_analysis.h:98
flow_insensitive_analysis_baset::get_next
locationt get_next(working_sett &working_set)
Definition: flow_insensitive_analysis.cpp:85
std_expr.h
flow_insensitive_abstract_domain_baset::transform
virtual bool transform(const namespacet &ns, locationt from, locationt to)=0
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099