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,
45  const goto_programt &goto_program,
46  const irep_idt &identifier,
47  std::ostream &out) const
48 {
49  forall_goto_program_instructions(i_it, goto_program)
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 
64  const namespacet &ns,
65  const goto_functionst &goto_functions) const
66 {
67  json_objectt result;
68 
69  forall_goto_functions(f_it, goto_functions)
70  {
71  if(f_it->second.body_available())
72  {
73  result[id2string(f_it->first)]=
74  output_json(ns, f_it->second.body, f_it->first);
75  }
76  else
77  {
78  result[id2string(f_it->first)]=json_arrayt();
79  }
80  }
81 
82  return std::move(result);
83 }
84 
92  const namespacet &ns,
93  const goto_programt &goto_program,
94  const irep_idt &identifier) const
95 {
96  json_arrayt contents;
97 
98  forall_goto_program_instructions(i_it, goto_program)
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 std::move(contents);
117 }
118 
120  const namespacet &ns,
121  const goto_functionst &goto_functions) const
122 {
123  xmlt program("program");
124 
125  forall_goto_functions(f_it, goto_functions)
126  {
127  xmlt function("function");
128  function.set_attribute("name", id2string(f_it->first));
129  function.set_attribute(
130  "body_available",
131  f_it->second.body_available() ? "true" : "false");
132 
133  if(f_it->second.body_available())
134  {
135  function.new_element(output_xml(ns, f_it->second.body, f_it->first));
136  }
137 
138  program.new_element(function);
139  }
140 
141  return program;
142 }
143 
151  const namespacet &ns,
152  const goto_programt &goto_program,
153  const irep_idt &identifier) const
154 {
155  xmlt function_body;
156 
157  forall_goto_program_instructions(i_it, goto_program)
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 
191 void ai_baset::entry_state(const goto_programt &goto_program)
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 
202 void ai_baset::initialize(const goto_programt &goto_program)
203 {
204  // we mark everything as unreachable as starting point
205 
206  forall_goto_program_instructions(i_it, goto_program)
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 
234  const irep_idt &function_identifier,
235  const goto_programt &goto_program,
236  const goto_functionst &goto_functions,
237  const namespacet &ns)
238 {
239  working_sett working_set;
240 
241  // Put the first location in the working set
242  if(!goto_program.empty())
244  working_set,
245  goto_program.instructions.begin());
246 
247  bool new_data=false;
248 
249  while(!working_set.empty())
250  {
251  locationt l=get_next(working_set);
252 
253  // goto_program is really only needed for iterator manipulation
254  if(visit(
255  function_identifier, l, working_set, goto_program, goto_functions, ns))
256  new_data=true;
257  }
258 
259  return new_data;
260 }
261 
263  const irep_idt &function_identifier,
264  locationt l,
265  working_sett &working_set,
266  const goto_programt &goto_program,
267  const goto_functionst &goto_functions,
268  const namespacet &ns)
269 {
270  bool new_data=false;
271 
272  statet &current=get_state(l);
273 
274  for(const auto &to_l : goto_program.get_successors(l))
275  {
276  if(to_l==goto_program.instructions.end())
277  continue;
278 
279  std::unique_ptr<statet> tmp_state(
280  make_temporary_state(current));
281 
282  statet &new_values=*tmp_state;
283 
284  bool have_new_values=false;
285 
286  if(l->is_function_call() &&
287  !goto_functions.function_map.empty())
288  {
289  // this is a big special case
290  const code_function_callt &code=
291  to_code_function_call(l->code);
292 
294  function_identifier,
295  l,
296  to_l,
297  code.function(),
298  code.arguments(),
299  goto_functions,
300  ns))
301  have_new_values=true;
302  }
303  else
304  {
305  // initialize state, if necessary
306  get_state(to_l);
307 
308  new_values.transform(
309  function_identifier, l, function_identifier, to_l, *this, ns);
310 
311  if(merge(new_values, l, to_l))
312  have_new_values=true;
313  }
314 
315  if(have_new_values)
316  {
317  new_data=true;
318  put_in_working_set(working_set, to_l);
319  }
320  }
321 
322  return new_data;
323 }
324 
326  const irep_idt &calling_function_identifier,
327  locationt l_call,
328  locationt l_return,
329  const goto_functionst &goto_functions,
330  const goto_functionst::function_mapt::const_iterator f_it,
331  const exprt::operandst &,
332  const namespacet &ns)
333 {
334  // initialize state, if necessary
335  get_state(l_return);
336 
337  PRECONDITION(l_call->is_function_call());
338 
339  const goto_functionst::goto_functiont &goto_function=
340  f_it->second;
341 
342  if(!goto_function.body_available())
343  {
344  // If we don't have a body, we just do an edge call -> return
345  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
346  tmp_state->transform(
347  calling_function_identifier,
348  l_call,
349  calling_function_identifier,
350  l_return,
351  *this,
352  ns);
353 
354  return merge(*tmp_state, l_call, l_return);
355  }
356 
357  assert(!goto_function.body.instructions.empty());
358 
359  // This is the edge from call site to function head.
360 
361  {
362  // get the state at the beginning of the function
363  locationt l_begin=goto_function.body.instructions.begin();
364  // initialize state, if necessary
365  get_state(l_begin);
366 
367  // do the edge from the call site to the beginning of the function
368  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
369  tmp_state->transform(
370  calling_function_identifier, l_call, f_it->first, l_begin, *this, ns);
371 
372  bool new_data=false;
373 
374  // merge the new stuff
375  if(merge(*tmp_state, l_call, l_begin))
376  new_data=true;
377 
378  // do we need to do/re-do the fixedpoint of the body?
379  if(new_data)
380  fixedpoint(f_it->first, goto_function.body, goto_functions, ns);
381  }
382 
383  // This is the edge from function end to return site.
384 
385  {
386  // get location at end of the procedure we have called
387  locationt l_end=--goto_function.body.instructions.end();
388  assert(l_end->is_end_function());
389 
390  // do edge from end of function to instruction after call
391  const statet &end_state=get_state(l_end);
392 
393  if(end_state.is_bottom())
394  return false; // function exit point not reachable
395 
396  std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
397  tmp_state->transform(
398  f_it->first, l_end, calling_function_identifier, l_return, *this, ns);
399 
400  // Propagate those
401  return merge(*tmp_state, l_end, l_return);
402  }
403 }
404 
406  const irep_idt &calling_function_identifier,
407  locationt l_call,
408  locationt l_return,
409  const exprt &function,
410  const exprt::operandst &arguments,
411  const goto_functionst &goto_functions,
412  const namespacet &ns)
413 {
414  PRECONDITION(!goto_functions.function_map.empty());
415 
416  // This is quite a strong assumption on the well-formedness of the program.
417  // It means function pointers must be removed before use.
419  function.id() == ID_symbol,
420  "Function pointers and indirect calls must be removed before analysis.");
421 
422  bool new_data=false;
423 
424  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
425 
426  goto_functionst::function_mapt::const_iterator it =
427  goto_functions.function_map.find(identifier);
428 
430  it != goto_functions.function_map.end(),
431  "Function " + id2string(identifier) + "not in function map");
432 
433  new_data = do_function_call(
434  calling_function_identifier,
435  l_call,
436  l_return,
437  goto_functions,
438  it,
439  arguments,
440  ns);
441 
442  return new_data;
443 }
444 
446  const goto_functionst &goto_functions,
447  const namespacet &ns)
448 {
449  goto_functionst::function_mapt::const_iterator
450  f_it=goto_functions.function_map.find(goto_functions.entry_point());
451 
452  if(f_it!=goto_functions.function_map.end())
453  fixedpoint(f_it->first, f_it->second.body, goto_functions, ns);
454 }
455 
457  const goto_functionst &goto_functions,
458  const namespacet &ns)
459 {
460  sequential_fixedpoint(goto_functions, ns);
461 
462  is_threadedt is_threaded(goto_functions);
463 
464  // construct an initial shared state collecting the results of all
465  // functions
466  goto_programt tmp;
467  tmp.add_instruction();
468  goto_programt::const_targett sh_target=tmp.instructions.begin();
469  statet &shared_state=get_state(sh_target);
470 
471  struct wl_entryt
472  {
473  wl_entryt(
474  const irep_idt &_function_identifier,
475  const goto_programt &_goto_program,
476  locationt _location)
477  : function_identifier(_function_identifier),
478  goto_program(&_goto_program),
479  location(_location)
480  {
481  }
482 
483  irep_idt function_identifier;
484  const goto_programt *goto_program;
485  locationt location;
486  };
487 
488  typedef std::list<wl_entryt> thread_wlt;
489  thread_wlt thread_wl;
490 
491  forall_goto_functions(it, goto_functions)
492  forall_goto_program_instructions(t_it, it->second.body)
493  {
494  if(is_threaded(t_it))
495  {
496  thread_wl.push_back(wl_entryt(it->first, it->second.body, t_it));
497 
499  it->second.body.instructions.end();
500  --l_end;
501 
502  merge_shared(shared_state, l_end, sh_target, ns);
503  }
504  }
505 
506  // now feed in the shared state into all concurrently executing
507  // functions, and iterate until the shared state stabilizes
508  bool new_shared=true;
509  while(new_shared)
510  {
511  new_shared=false;
512 
513  for(const auto &wl_entry : thread_wl)
514  {
515  working_sett working_set;
516  put_in_working_set(working_set, wl_entry.location);
517 
518  statet &begin_state = get_state(wl_entry.location);
519  merge(begin_state, sh_target, wl_entry.location);
520 
521  while(!working_set.empty())
522  {
523  goto_programt::const_targett l=get_next(working_set);
524 
525  visit(
526  wl_entry.function_identifier,
527  l,
528  working_set,
529  *(wl_entry.goto_program),
530  goto_functions,
531  ns);
532 
533  // the underlying domain must make sure that the final state
534  // carries all possible values; otherwise we would need to
535  // merge over each and every state
536  if(l->is_end_function())
537  new_shared|=merge_shared(shared_state, l, sh_target, ns);
538  }
539  }
540  }
541 }
virtual statet & get_state(locationt l)=0
Get the state for the given location, creating it in a default way if it doesn&#39;t exist.
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:282
goto_programt::const_targett locationt
Definition: ai.h:36
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const irep_idt & get_identifier() const
Definition: std_expr.h:176
virtual void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
Definition: json.h:23
virtual bool merge(const statet &src, locationt from, locationt to)=0
function_mapt function_map
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
virtual jsont output_json(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as JSON.
Definition: ai.cpp:63
std::map< unsigned, locationt > working_sett
The work queue, sorted by location number.
Definition: ai.h:277
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Output the abstract states for a whole program.
Definition: ai.cpp:24
jsont & push_back(const jsont &json)
Definition: json.h:163
bool do_function_call_rec(const irep_idt &calling_function_identifier, locationt l_call, locationt l_return, const exprt &function, const exprt::operandst &arguments, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:405
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
argumentst & arguments()
Definition: std_code.h:1109
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
instructionst::const_iterator const_targett
Definition: goto_program.h:415
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
Definition: xml.h:18
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
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:35
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: ai.cpp:216
void sequential_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:445
std::vector< exprt > operandst
Definition: expr.h:57
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
bool fixedpoint(const irep_idt &function_identifier, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
Definition: ai.cpp:233
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)=0
Make a copy of a state.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool visit(const irep_idt &function_identifier, locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from location l Depending on the instruction type it may ...
Definition: ai.cpp:262
xmlt & new_element(const std::string &key)
Definition: xml.h:86
Abstract Interpretation.
exprt & function()
Definition: std_code.h:1099
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
locationt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:221
bool empty() const
Is the program empty?
Definition: goto_program.h:626
bool do_function_call(const irep_idt &calling_function_identifier, 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:325
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:456
virtual xmlt output_xml(const namespacet &ns, const goto_functionst &goto_functions) const
Output the abstract states for the whole program as XML.
Definition: ai.cpp:119
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
#define forall_goto_functions(it, functions)
void entry_state(const goto_programt &goto_program)
Set the abstract state of the entry location of a single function to the entry state required by the ...
Definition: ai.cpp:191
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173