cprover
ai.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ai.h"
13 
14 #include <cassert>
15 #include <memory>
16 #include <sstream>
17 
18 #include <util/invariant.h>
19 #include <util/std_code.h>
20 #include <util/std_expr.h>
21 
22 #include "is_threaded.h"
23 
25  const namespacet &ns,
26  const goto_functionst &goto_functions,
27  std::ostream &out) const
28 {
29  forall_goto_functions(f_it, goto_functions)
30  {
31  if(f_it->second.body_available())
32  {
33  out << "////\n";
34  out << "//// Function: " << f_it->first << "\n";
35  out << "////\n";
36  out << "\n";
37 
38  output(ns, f_it->second.body, f_it->first, out);
39  }
40  }
41 }
42 
44  const namespacet &ns,
46  const irep_idt &identifier,
47  std::ostream &out) const
48 {
50  {
51  out << "**** " << i_it->location_number << " "
52  << i_it->source_location << "\n";
53 
54  abstract_state_before(i_it)->output(out, *this, ns);
55  out << "\n";
56  #if 1
57  goto_program.output_instruction(ns, identifier, out, *i_it);
58  out << "\n";
59  #endif
60  }
61 }
62 
67  const namespacet &ns,
68  const goto_functionst &goto_functions) const
69 {
70  json_objectt result;
71 
72  forall_goto_functions(f_it, goto_functions)
73  {
74  if(f_it->second.body_available())
75  {
76  result[id2string(f_it->first)]=
77  output_json(ns, f_it->second.body, f_it->first);
78  }
79  else
80  {
81  result[id2string(f_it->first)]=json_arrayt();
82  }
83  }
84 
85  return result;
86 }
87 
92  const namespacet &ns,
94  const irep_idt &identifier) const
95 {
96  json_arrayt contents;
97 
99  {
100  json_objectt location;
101  location["locationNumber"]=
102  json_numbert(std::to_string(i_it->location_number));
103  location["sourceLocation"]=
104  json_stringt(i_it->source_location.as_string());
105  location["abstractState"] =
106  abstract_state_before(i_it)->output_json(*this, ns);
107 
108  // Ideally we need output_instruction_json
109  std::ostringstream out;
110  goto_program.output_instruction(ns, identifier, out, *i_it);
111  location["instruction"]=json_stringt(out.str());
112 
113  contents.push_back(location);
114  }
115 
116  return contents;
117 }
118 
123  const namespacet &ns,
124  const goto_functionst &goto_functions) const
125 {
126  xmlt program("program");
127 
128  forall_goto_functions(f_it, goto_functions)
129  {
130  xmlt function("function");
131  function.set_attribute("name", id2string(f_it->first));
132  function.set_attribute(
133  "body_available",
134  f_it->second.body_available() ? "true" : "false");
135 
136  if(f_it->second.body_available())
137  {
138  function.new_element(output_xml(ns, f_it->second.body, f_it->first));
139  }
140 
141  program.new_element(function);
142  }
143 
144  return program;
145 }
146 
151  const namespacet &ns,
153  const irep_idt &identifier) const
154 {
155  xmlt function_body;
156 
158  {
159  xmlt location;
160  location.set_attribute(
161  "location_number",
162  std::to_string(i_it->location_number));
163  location.set_attribute(
164  "source_location",
165  i_it->source_location.as_string());
166 
167  location.new_element(abstract_state_before(i_it)->output_xml(*this, ns));
168 
169  // Ideally we need output_instruction_xml
170  std::ostringstream out;
171  goto_program.output_instruction(ns, identifier, out, *i_it);
172  location.set_attribute("instruction", out.str());
173 
174  function_body.new_element(location);
175  }
176 
177  return function_body;
178 }
179 
180 void ai_baset::entry_state(const goto_functionst &goto_functions)
181 {
182  // find the 'entry function'
183 
184  goto_functionst::function_mapt::const_iterator
185  f_it=goto_functions.function_map.find(goto_functions.entry_point());
186 
187  if(f_it!=goto_functions.function_map.end())
188  entry_state(f_it->second.body);
189 }
190 
192 {
193  // The first instruction of 'goto_program' is the entry point
194  get_state(goto_program.instructions.begin()).make_entry();
195 }
196 
198 {
199  initialize(goto_function.body);
200 }
201 
203 {
204  // we mark everything as unreachable as starting point
205 
207  get_state(i_it).make_bottom();
208 }
209 
210 void ai_baset::initialize(const goto_functionst &goto_functions)
211 {
212  forall_goto_functions(it, goto_functions)
213  initialize(it->second);
214 }
215 
217 {
218  // Nothing to do per default
219 }
220 
222  working_sett &working_set)
223 {
224  PRECONDITION(!working_set.empty());
225 
226  working_sett::iterator i=working_set.begin();
227  locationt l=i->second;
228  working_set.erase(i);
229 
230  return l;
231 }
232 
235  const goto_functionst &goto_functions,
236  const namespacet &ns)
237 {
238  working_sett working_set;
239 
240  // Put the first location in the working set
241  if(!goto_program.empty())
243  working_set,
244  goto_program.instructions.begin());
245 
246  bool new_data=false;
247 
248  while(!working_set.empty())
249  {
250  locationt l=get_next(working_set);
251 
252  // goto_program is really only needed for iterator manipulation
253  if(visit(l, working_set, goto_program, goto_functions, ns))
254  new_data=true;
255  }
256 
257  return new_data;
258 }
259 
261  locationt l,
262  working_sett &working_set,
264  const goto_functionst &goto_functions,
265  const namespacet &ns)
266 {
267  bool new_data=false;
268 
269  statet &current=get_state(l);
270 
271  for(const auto &to_l : goto_program.get_successors(l))
272  {
273  if(to_l==goto_program.instructions.end())
274  continue;
275 
276  std::unique_ptr<statet> tmp_state(
277  make_temporary_state(current));
278 
279  statet &new_values=*tmp_state;
280 
281  bool have_new_values=false;
282 
283  if(l->is_function_call() &&
284  !goto_functions.function_map.empty())
285  {
286  // this is a big special case
287  const code_function_callt &code=
288  to_code_function_call(l->code);
289 
291  l, to_l,
292  code.function(),
293  code.arguments(),
294  goto_functions, ns))
295  have_new_values=true;
296  }
297  else
298  {
299  // initialize state, if necessary
300  get_state(to_l);
301 
302  new_values.transform(l, to_l, *this, ns);
303 
304  if(merge(new_values, l, to_l))
305  have_new_values=true;
306  }
307 
308  if(have_new_values)
309  {
310  new_data=true;
311  put_in_working_set(working_set, to_l);
312  }
313  }
314 
315  return new_data;
316 }
317 
319  locationt l_call, locationt l_return,
320  const goto_functionst &goto_functions,
321  const goto_functionst::function_mapt::const_iterator f_it,
322  const exprt::operandst &,
323  const namespacet &ns)
324 {
325  // initialize state, if necessary
326  get_state(l_return);
327 
328  PRECONDITION(l_call->is_function_call());
329 
330  const goto_functionst::goto_functiont &goto_function=
331  f_it->second;
332 
333  if(!goto_function.body_available())
334  {
335  // if we don't have a body, we just do an edige call -> return
336  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
337  tmp_state->transform(l_call, l_return, *this, ns);
338 
339  return merge(*tmp_state, l_call, l_return);
340  }
341 
342  assert(!goto_function.body.instructions.empty());
343 
344  // This is the edge from call site to function head.
345 
346  {
347  // get the state at the beginning of the function
348  locationt l_begin=goto_function.body.instructions.begin();
349  // initialize state, if necessary
350  get_state(l_begin);
351 
352  // do the edge from the call site to the beginning of the function
353  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
354  tmp_state->transform(l_call, l_begin, *this, ns);
355 
356  bool new_data=false;
357 
358  // merge the new stuff
359  if(merge(*tmp_state, l_call, l_begin))
360  new_data=true;
361 
362  // do we need to do/re-do the fixedpoint of the body?
363  if(new_data)
364  fixedpoint(goto_function.body, goto_functions, ns);
365  }
366 
367  // This is the edge from function end to return site.
368 
369  {
370  // get location at end of the procedure we have called
371  locationt l_end=--goto_function.body.instructions.end();
372  assert(l_end->is_end_function());
373 
374  // do edge from end of function to instruction after call
375  const statet &end_state=get_state(l_end);
376 
377  if(end_state.is_bottom())
378  return false; // function exit point not reachable
379 
380  std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
381  tmp_state->transform(l_end, l_return, *this, ns);
382 
383  // Propagate those
384  return merge(*tmp_state, l_end, l_return);
385  }
386 }
387 
389  locationt l_call, locationt l_return,
390  const exprt &function,
391  const exprt::operandst &arguments,
392  const goto_functionst &goto_functions,
393  const namespacet &ns)
394 {
395  PRECONDITION(!goto_functions.function_map.empty());
396 
397  // This is quite a strong assumption on the well-formedness of the program.
398  // It means function pointers must be removed before use.
400  function.id() == ID_symbol,
401  "Function pointers and indirect calls must be removed before analysis.");
402 
403  bool new_data=false;
404 
405  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
406 
407  goto_functionst::function_mapt::const_iterator it =
408  goto_functions.function_map.find(identifier);
409 
411  it != goto_functions.function_map.end(),
412  "Function " + id2string(identifier) + "not in function map");
413 
414  new_data =
415  do_function_call(l_call, l_return, goto_functions, it, arguments, ns);
416 
417  return new_data;
418 }
419 
421  const goto_functionst &goto_functions,
422  const namespacet &ns)
423 {
424  goto_functionst::function_mapt::const_iterator
425  f_it=goto_functions.function_map.find(goto_functions.entry_point());
426 
427  if(f_it!=goto_functions.function_map.end())
428  fixedpoint(f_it->second.body, goto_functions, ns);
429 }
430 
432  const goto_functionst &goto_functions,
433  const namespacet &ns)
434 {
435  sequential_fixedpoint(goto_functions, ns);
436 
437  is_threadedt is_threaded(goto_functions);
438 
439  // construct an initial shared state collecting the results of all
440  // functions
441  goto_programt tmp;
442  tmp.add_instruction();
443  goto_programt::const_targett sh_target=tmp.instructions.begin();
444  statet &shared_state=get_state(sh_target);
445 
446  typedef std::list<std::pair<goto_programt const*,
447  goto_programt::const_targett> > thread_wlt;
448  thread_wlt thread_wl;
449 
450  forall_goto_functions(it, goto_functions)
451  forall_goto_program_instructions(t_it, it->second.body)
452  {
453  if(is_threaded(t_it))
454  {
455  thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
456 
458  it->second.body.instructions.end();
459  --l_end;
460 
461  merge_shared(shared_state, l_end, sh_target, ns);
462  }
463  }
464 
465  // now feed in the shared state into all concurrently executing
466  // functions, and iterate until the shared state stabilizes
467  bool new_shared=true;
468  while(new_shared)
469  {
470  new_shared=false;
471 
472  for(const auto &wl_pair : thread_wl)
473  {
474  working_sett working_set;
475  put_in_working_set(working_set, wl_pair.second);
476 
477  statet &begin_state=get_state(wl_pair.second);
478  merge(begin_state, sh_target, wl_pair.second);
479 
480  while(!working_set.empty())
481  {
482  goto_programt::const_targett l=get_next(working_set);
483 
484  visit(l, working_set, *(wl_pair.first), goto_functions, ns);
485 
486  // the underlying domain must make sure that the final state
487  // carries all possible values; otherwise we would need to
488  // merge over each and every state
489  if(l->is_end_function())
490  new_shared|=merge_shared(shared_state, l, sh_target, ns);
491  }
492  }
493  }
494 }
virtual statet & get_state(locationt l)=0
Over-approximate Concurrency for Threaded Goto Programs.
virtual void make_bottom()=0
no states
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void put_in_working_set(working_sett &working_set, locationt l)
Definition: ai.h:227
goto_programt::const_targett locationt
Definition: ai.h:36
const irep_idt & get_identifier() const
Definition: std_expr.h:128
Definition: json.h:23
virtual bool merge(const statet &src, locationt from, locationt to)=0
function_mapt function_map
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as JSON.
Definition: ai.cpp:66
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
how function calls are treated: a) there is an edge from each call site to the function head b) there...
std::map< unsigned, locationt > working_sett
Definition: ai.h:223
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:24
jsont & push_back(const jsont &json)
Definition: json.h:163
argumentst & arguments()
Definition: std_code.h:890
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
bool do_function_call_rec(locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:388
bool do_function_call(locationt l_call, locationt l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, const namespacet &ns)
Definition: ai.cpp:318
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
instructionst::const_iterator const_targett
Definition: goto_program.h:398
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
void entry_state(const goto_programt &)
Definition: ai.cpp:191
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
Definition: xml.h:18
A function call.
Definition: std_code.h:858
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
virtual void finalize()
Definition: ai.cpp:216
xmlt & new_element(const std::string &name)
Definition: xml.h:86
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:420
std::vector< exprt > operandst
Definition: expr.h:45
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:233
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:260
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
static irep_idt entry_point()
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Abstract Interpretation.
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
locationt get_next(working_sett &working_set)
Definition: ai.cpp:221
std::string to_string(const string_constraintt &expr)
Used for debug printing.
bool empty() const
Is the program empty?
Definition: goto_program.h:590
virtual void initialize(const goto_programt &)
Definition: ai.cpp:202
goto_programt & goto_program
Definition: cover.cpp:63
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:431
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the domains for the whole program as XML.
Definition: ai.cpp:122
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909