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/simplify_expr.h>
19 #include <util/std_expr.h>
20 #include <util/std_code.h>
21 
22 #include "is_threaded.h"
23 
25  const ai_baset &ai,
26  const namespacet &ns) const
27 {
28  std::ostringstream out;
29  output(out, ai, ns);
30  json_stringt json(out.str());
31  return json;
32 }
33 
35  const ai_baset &ai,
36  const namespacet &ns) const
37 {
38  std::ostringstream out;
39  output(out, ai, ns);
40  xmlt xml("abstract_state");
41  xml.data=out.str();
42  return xml;
43 }
44 
54  exprt &condition, const namespacet &ns) const
55 {
56  // Care must be taken here to give something that is still writable
57  if(condition.id()==ID_index)
58  {
59  index_exprt ie=to_index_expr(condition);
60  bool no_simplification=ai_simplify(ie.index(), ns);
61  if(!no_simplification)
62  condition=simplify_expr(ie, ns);
63 
64  return no_simplification;
65  }
66  else if(condition.id()==ID_dereference)
67  {
69  bool no_simplification=ai_simplify(de.pointer(), ns);
70  if(!no_simplification)
71  condition=simplify_expr(de, ns); // So *(&x) -> x
72 
73  return no_simplification;
74  }
75  else if(condition.id()==ID_member)
76  {
77  member_exprt me=to_member_expr(condition);
78  // Since simplify_ai_lhs is required to return an addressable object
79  // (so remains a valid left hand side), to simplify
80  // `(something_simplifiable).b` we require that `something_simplifiable`
81  // must also be addressable
82  bool no_simplification=ai_simplify_lhs(me.compound(), ns);
83  if(!no_simplification)
84  condition=simplify_expr(me, ns);
85 
86  return no_simplification;
87  }
88  else
89  return true;
90 }
91 
93  const namespacet &ns,
94  const goto_functionst &goto_functions,
95  std::ostream &out) const
96 {
97  forall_goto_functions(f_it, goto_functions)
98  {
99  if(f_it->second.body_available())
100  {
101  out << "////\n";
102  out << "//// Function: " << f_it->first << "\n";
103  out << "////\n";
104  out << "\n";
105 
106  output(ns, f_it->second.body, f_it->first, out);
107  }
108  }
109 }
110 
112  const namespacet &ns,
114  const irep_idt &identifier,
115  std::ostream &out) const
116 {
118  {
119  out << "**** " << i_it->location_number << " "
120  << i_it->source_location << "\n";
121 
122  find_state(i_it).output(out, *this, ns);
123  out << "\n";
124  #if 1
125  goto_program.output_instruction(ns, identifier, out, *i_it);
126  out << "\n";
127  #endif
128  }
129 }
130 
135  const namespacet &ns,
136  const goto_functionst &goto_functions) const
137 {
138  json_objectt result;
139 
140  forall_goto_functions(f_it, goto_functions)
141  {
142  if(f_it->second.body_available())
143  {
144  result[id2string(f_it->first)]=
145  output_json(ns, f_it->second.body, f_it->first);
146  }
147  else
148  {
149  result[id2string(f_it->first)]=json_arrayt();
150  }
151  }
152 
153  return result;
154 }
155 
160  const namespacet &ns,
162  const irep_idt &identifier) const
163 {
164  json_arrayt contents;
165 
167  {
168  json_objectt location;
169  location["locationNumber"]=
170  json_numbert(std::to_string(i_it->location_number));
171  location["sourceLocation"]=
172  json_stringt(i_it->source_location.as_string());
173  location["abstractState"]=find_state(i_it).output_json(*this, ns);
174 
175  // Ideally we need output_instruction_json
176  std::ostringstream out;
177  goto_program.output_instruction(ns, identifier, out, *i_it);
178  location["instruction"]=json_stringt(out.str());
179 
180  contents.push_back(location);
181  }
182 
183  return contents;
184 }
185 
190  const namespacet &ns,
191  const goto_functionst &goto_functions) const
192 {
193  xmlt program("program");
194 
195  forall_goto_functions(f_it, goto_functions)
196  {
197  xmlt function("function");
198  function.set_attribute("name", id2string(f_it->first));
199  function.set_attribute(
200  "body_available",
201  f_it->second.body_available() ? "true" : "false");
202 
203  if(f_it->second.body_available())
204  {
205  function.new_element(output_xml(ns, f_it->second.body, f_it->first));
206  }
207 
208  program.new_element(function);
209  }
210 
211  return program;
212 }
213 
218  const namespacet &ns,
220  const irep_idt &identifier) const
221 {
222  xmlt function_body;
223 
225  {
226  xmlt location;
227  location.set_attribute(
228  "location_number",
229  std::to_string(i_it->location_number));
230  location.set_attribute(
231  "source_location",
232  i_it->source_location.as_string());
233 
234  location.new_element(find_state(i_it).output_xml(*this, ns));
235 
236  // Ideally we need output_instruction_xml
237  std::ostringstream out;
238  goto_program.output_instruction(ns, identifier, out, *i_it);
239  location.set_attribute("instruction", out.str());
240 
241  function_body.new_element(location);
242  }
243 
244  return function_body;
245 }
246 
247 void ai_baset::entry_state(const goto_functionst &goto_functions)
248 {
249  // find the 'entry function'
250 
251  goto_functionst::function_mapt::const_iterator
252  f_it=goto_functions.function_map.find(goto_functions.entry_point());
253 
254  if(f_it!=goto_functions.function_map.end())
255  entry_state(f_it->second.body);
256 }
257 
259 {
260  // The first instruction of 'goto_program' is the entry point
261  get_state(goto_program.instructions.begin()).make_entry();
262 }
263 
265 {
266  initialize(goto_function.body);
267 }
268 
270 {
271  // we mark everything as unreachable as starting point
272 
274  get_state(i_it).make_bottom();
275 }
276 
277 void ai_baset::initialize(const goto_functionst &goto_functions)
278 {
279  forall_goto_functions(it, goto_functions)
280  initialize(it->second);
281 }
282 
284 {
285  // Nothing to do per default
286 }
287 
289  working_sett &working_set)
290 {
291  assert(!working_set.empty());
292 
293  working_sett::iterator i=working_set.begin();
294  locationt l=i->second;
295  working_set.erase(i);
296 
297  return l;
298 }
299 
302  const goto_functionst &goto_functions,
303  const namespacet &ns)
304 {
305  working_sett working_set;
306 
307  // Put the first location in the working set
308  if(!goto_program.empty())
310  working_set,
311  goto_program.instructions.begin());
312 
313  bool new_data=false;
314 
315  while(!working_set.empty())
316  {
317  locationt l=get_next(working_set);
318 
319  if(visit(l, working_set, goto_program, goto_functions, ns))
320  new_data=true;
321  }
322 
323  return new_data;
324 }
325 
327  locationt l,
328  working_sett &working_set,
330  const goto_functionst &goto_functions,
331  const namespacet &ns)
332 {
333  bool new_data=false;
334 
335  statet &current=get_state(l);
336 
337  for(const auto &to_l : goto_program.get_successors(l))
338  {
339  if(to_l==goto_program.instructions.end())
340  continue;
341 
342  std::unique_ptr<statet> tmp_state(
343  make_temporary_state(current));
344 
345  statet &new_values=*tmp_state;
346 
347  bool have_new_values=false;
348 
349  if(l->is_function_call() &&
350  !goto_functions.function_map.empty())
351  {
352  // this is a big special case
353  const code_function_callt &code=
354  to_code_function_call(l->code);
355 
357  l, to_l,
358  code.function(),
359  code.arguments(),
360  goto_functions, ns))
361  have_new_values=true;
362  }
363  else
364  {
365  // initialize state, if necessary
366  get_state(to_l);
367 
368  new_values.transform(l, to_l, *this, ns);
369 
370  if(merge(new_values, l, to_l))
371  have_new_values=true;
372  }
373 
374  if(have_new_values)
375  {
376  new_data=true;
377  put_in_working_set(working_set, to_l);
378  }
379  }
380 
381  return new_data;
382 }
383 
385  locationt l_call, locationt l_return,
386  const goto_functionst &goto_functions,
387  const goto_functionst::function_mapt::const_iterator f_it,
388  const exprt::operandst &arguments,
389  const namespacet &ns)
390 {
391  // initialize state, if necessary
392  get_state(l_return);
393 
394  const goto_functionst::goto_functiont &goto_function=
395  f_it->second;
396 
397  if(!goto_function.body_available())
398  {
399  // if we don't have a body, we just do an edige call -> return
400  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
401  tmp_state->transform(l_call, l_return, *this, ns);
402 
403  return merge(*tmp_state, l_call, l_return);
404  }
405 
406  assert(!goto_function.body.instructions.empty());
407 
408  // This is the edge from call site to function head.
409 
410  {
411  // get the state at the beginning of the function
412  locationt l_begin=goto_function.body.instructions.begin();
413  // initialize state, if necessary
414  get_state(l_begin);
415 
416  // do the edge from the call site to the beginning of the function
417  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
418  tmp_state->transform(l_call, l_begin, *this, ns);
419 
420  bool new_data=false;
421 
422  // merge the new stuff
423  if(merge(*tmp_state, l_call, l_begin))
424  new_data=true;
425 
426  // do we need to do/re-do the fixedpoint of the body?
427  if(new_data)
428  fixedpoint(goto_function.body, goto_functions, ns);
429  }
430 
431  // This is the edge from function end to return site.
432 
433  {
434  // get location at end of the procedure we have called
435  locationt l_end=--goto_function.body.instructions.end();
436  assert(l_end->is_end_function());
437 
438  // do edge from end of function to instruction after call
439  const statet &end_state=get_state(l_end);
440 
441  if(end_state.is_bottom())
442  return false; // function exit point not reachable
443 
444  std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
445  tmp_state->transform(l_end, l_return, *this, ns);
446 
447  // Propagate those
448  return merge(*tmp_state, l_end, l_return);
449  }
450 }
451 
453  locationt l_call, locationt l_return,
454  const exprt &function,
455  const exprt::operandst &arguments,
456  const goto_functionst &goto_functions,
457  const namespacet &ns)
458 {
459  assert(!goto_functions.function_map.empty());
460 
461  bool new_data=false;
462 
463  if(function.id()==ID_symbol)
464  {
465  const irep_idt &identifier = to_symbol_expr(function).get_identifier();
466 
467  goto_functionst::function_mapt::const_iterator it=
468  goto_functions.function_map.find(identifier);
469 
470  if(it==goto_functions.function_map.end())
471  throw "failed to find function "+id2string(identifier);
472 
473  new_data=do_function_call(
474  l_call, l_return,
475  goto_functions,
476  it,
477  arguments,
478  ns);
479  }
480  else if(function.id()==ID_if)
481  {
482  if(function.operands().size()!=3)
483  throw "if has three operands";
484 
485  bool new_data1=
487  l_call, l_return,
488  function.op1(),
489  arguments,
490  goto_functions,
491  ns);
492 
493  bool new_data2=
495  l_call, l_return,
496  function.op2(),
497  arguments,
498  goto_functions,
499  ns);
500 
501  if(new_data1 || new_data2)
502  new_data=true;
503  }
504  else if(function.id()==ID_dereference)
505  {
506  // We can't really do this here -- we rely on
507  // these being removed by some previous analysis.
508  }
509  else if(function.id() == ID_null_object)
510  {
511  // ignore, can't be a function
512  }
513  else if(function.id()==ID_member || function.id()==ID_index)
514  {
515  // ignore, can't be a function
516  }
517  else
518  {
519  throw "unexpected function_call argument: "+
520  function.id_string();
521  }
522 
523  return new_data;
524 }
525 
527  const goto_functionst &goto_functions,
528  const namespacet &ns)
529 {
530  goto_functionst::function_mapt::const_iterator
531  f_it=goto_functions.function_map.find(goto_functions.entry_point());
532 
533  if(f_it!=goto_functions.function_map.end())
534  fixedpoint(f_it->second.body, goto_functions, ns);
535 }
536 
538  const goto_functionst &goto_functions,
539  const namespacet &ns)
540 {
541  sequential_fixedpoint(goto_functions, ns);
542 
543  is_threadedt is_threaded(goto_functions);
544 
545  // construct an initial shared state collecting the results of all
546  // functions
547  goto_programt tmp;
548  tmp.add_instruction();
549  goto_programt::const_targett sh_target=tmp.instructions.begin();
550  statet &shared_state=get_state(sh_target);
551 
552  typedef std::list<std::pair<goto_programt const*,
553  goto_programt::const_targett> > thread_wlt;
554  thread_wlt thread_wl;
555 
556  forall_goto_functions(it, goto_functions)
557  forall_goto_program_instructions(t_it, it->second.body)
558  {
559  if(is_threaded(t_it))
560  {
561  thread_wl.push_back(std::make_pair(&(it->second.body), t_it));
562 
564  it->second.body.instructions.end();
565  --l_end;
566 
567  merge_shared(shared_state, l_end, sh_target, ns);
568  }
569  }
570 
571  // now feed in the shared state into all concurrently executing
572  // functions, and iterate until the shared state stabilizes
573  bool new_shared=true;
574  while(new_shared)
575  {
576  new_shared=false;
577 
578  for(const auto &wl_pair : thread_wl)
579  {
580  working_sett working_set;
581  put_in_working_set(working_set, wl_pair.second);
582 
583  statet &begin_state=get_state(wl_pair.second);
584  merge(begin_state, sh_target, wl_pair.second);
585 
586  while(!working_set.empty())
587  {
588  goto_programt::const_targett l=get_next(working_set);
589 
590  visit(l, working_set, *(wl_pair.first), goto_functions, ns);
591 
592  // the underlying domain must make sure that the final state
593  // carries all possible values; otherwise we would need to
594  // merge over each and every state
595  if(l->is_end_function())
596  new_shared|=merge_shared(shared_state, l, sh_target, ns);
597  }
598  }
599  }
600 }
virtual statet & get_state(locationt l)=0
Over-approximate Concurrency for Threaded Goto Programs.
virtual void make_bottom()=0
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void put_in_working_set(working_sett &working_set, locationt l)
Definition: ai.h:313
goto_programt::const_targett locationt
Definition: ai.h:132
exprt simplify_expr(const exprt &src, const namespacet &ns)
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
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai.cpp:24
function_mapt function_map
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:134
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
virtual void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:3328
Extract member of struct or union.
Definition: std_expr.h:3871
std::map< unsigned, locationt > working_sett
Definition: ai.h:309
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
jsont & push_back(const jsont &json)
Definition: json.h:163
const exprt & compound() const
Definition: std_expr.h:3922
const irep_idt & id() const
Definition: irep.h:189
argumentst & arguments()
Definition: std_code.h:860
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:452
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:384
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
Definition: ai.h:113
Operator to dereference a pointer.
Definition: std_expr.h:3284
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:258
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
Definition: xml.h:18
virtual const statet & find_state(locationt l) const =0
A function call.
Definition: std_code.h:828
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
std::string data
Definition: xml.h:30
virtual void finalize()
Definition: ai.cpp:283
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:526
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:300
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:326
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.
exprt & index()
Definition: std_expr.h:1496
Abstract Interpretation.
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Use the information in the domain to simplify the expression on the LHS of an assignment.
Definition: ai.cpp:53
exprt & function()
Definition: std_code.h:848
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Definition: ai.h:128
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai.cpp:34
Base class for all expressions.
Definition: expr.h:42
exprt & pointer()
Definition: std_expr.h:3307
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: ai.h:67
locationt get_next(working_sett &working_set)
Definition: ai.cpp:288
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:269
goto_programt & goto_program
Definition: cover.cpp:63
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:537
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:189
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879
array index operator
Definition: std_expr.h:1462