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("domain");
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,
113  const goto_programt &goto_program,
114  const irep_idt &identifier,
115  std::ostream &out) const
116 {
117  forall_goto_program_instructions(i_it, goto_program)
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,
161  const goto_programt &goto_program,
162  const irep_idt &identifier) const
163 {
164  json_arrayt contents;
165 
166  forall_goto_program_instructions(i_it, goto_program)
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["domain"]=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,
219  const goto_programt &goto_program,
220  const irep_idt &identifier) const
221 {
222  xmlt function_body;
223 
224  forall_goto_program_instructions(i_it, goto_program)
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 
258 void ai_baset::entry_state(const goto_programt &goto_program)
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 
269 void ai_baset::initialize(const goto_programt &goto_program)
270 {
271  // we mark everything as unreachable as starting point
272 
273  forall_goto_program_instructions(i_it, goto_program)
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  working_sett &working_set)
285 {
286  assert(!working_set.empty());
287 
288  working_sett::iterator i=working_set.begin();
289  locationt l=i->second;
290  working_set.erase(i);
291 
292  return l;
293 }
294 
296  const goto_programt &goto_program,
297  const goto_functionst &goto_functions,
298  const namespacet &ns)
299 {
300  working_sett working_set;
301 
302  // Put the first location in the working set
303  if(!goto_program.empty())
305  working_set,
306  goto_program.instructions.begin());
307 
308  bool new_data=false;
309 
310  while(!working_set.empty())
311  {
312  locationt l=get_next(working_set);
313 
314  if(visit(l, working_set, goto_program, goto_functions, ns))
315  new_data=true;
316  }
317 
318  return new_data;
319 }
320 
322  locationt l,
323  working_sett &working_set,
324  const goto_programt &goto_program,
325  const goto_functionst &goto_functions,
326  const namespacet &ns)
327 {
328  bool new_data=false;
329 
330  statet &current=get_state(l);
331 
332  for(const auto &to_l : goto_program.get_successors(l))
333  {
334  if(to_l==goto_program.instructions.end())
335  continue;
336 
337  std::unique_ptr<statet> tmp_state(
338  make_temporary_state(current));
339 
340  statet &new_values=*tmp_state;
341 
342  bool have_new_values=false;
343 
344  if(l->is_function_call() &&
345  !goto_functions.function_map.empty())
346  {
347  // this is a big special case
348  const code_function_callt &code=
349  to_code_function_call(l->code);
350 
352  l, to_l,
353  code.function(),
354  code.arguments(),
355  goto_functions, ns))
356  have_new_values=true;
357  }
358  else
359  {
360  // initialize state, if necessary
361  get_state(to_l);
362 
363  new_values.transform(l, to_l, *this, ns);
364 
365  if(merge(new_values, l, to_l))
366  have_new_values=true;
367  }
368 
369  if(have_new_values)
370  {
371  new_data=true;
372  put_in_working_set(working_set, to_l);
373  }
374  }
375 
376  return new_data;
377 }
378 
380  locationt l_call, locationt l_return,
381  const goto_functionst &goto_functions,
382  const goto_functionst::function_mapt::const_iterator f_it,
383  const exprt::operandst &arguments,
384  const namespacet &ns)
385 {
386  // initialize state, if necessary
387  get_state(l_return);
388 
389  const goto_functionst::goto_functiont &goto_function=
390  f_it->second;
391 
392  if(!goto_function.body_available())
393  {
394  // if we don't have a body, we just do an edige call -> return
395  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
396  tmp_state->transform(l_call, l_return, *this, ns);
397 
398  return merge(*tmp_state, l_call, l_return);
399  }
400 
401  assert(!goto_function.body.instructions.empty());
402 
403  // This is the edge from call site to function head.
404 
405  {
406  // get the state at the beginning of the function
407  locationt l_begin=goto_function.body.instructions.begin();
408  // initialize state, if necessary
409  get_state(l_begin);
410 
411  // do the edge from the call site to the beginning of the function
412  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
413  tmp_state->transform(l_call, l_begin, *this, ns);
414 
415  bool new_data=false;
416 
417  // merge the new stuff
418  if(merge(*tmp_state, l_call, l_begin))
419  new_data=true;
420 
421  // do we need to do/re-do the fixedpoint of the body?
422  if(new_data)
423  fixedpoint(goto_function.body, goto_functions, ns);
424  }
425 
426  // This is the edge from function end to return site.
427 
428  {
429  // get location at end of the procedure we have called
430  locationt l_end=--goto_function.body.instructions.end();
431  assert(l_end->is_end_function());
432 
433  // do edge from end of function to instruction after call
434  std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_end)));
435  tmp_state->transform(l_end, l_return, *this, ns);
436 
437  // Propagate those
438  return merge(*tmp_state, l_end, l_return);
439  }
440 }
441 
443  locationt l_call, locationt l_return,
444  const exprt &function,
445  const exprt::operandst &arguments,
446  const goto_functionst &goto_functions,
447  const namespacet &ns)
448 {
449  assert(!goto_functions.function_map.empty());
450 
451  bool new_data=false;
452 
453  if(function.id()==ID_symbol)
454  {
455  const irep_idt &identifier=function.get(ID_identifier);
456 
457  if(recursion_set.find(identifier)!=recursion_set.end())
458  {
459  // recursion detected!
460  return new_data;
461  }
462  else
463  recursion_set.insert(identifier);
464 
465  goto_functionst::function_mapt::const_iterator it=
466  goto_functions.function_map.find(identifier);
467 
468  if(it==goto_functions.function_map.end())
469  throw "failed to find function "+id2string(identifier);
470 
471  new_data=do_function_call(
472  l_call, l_return,
473  goto_functions,
474  it,
475  arguments,
476  ns);
477 
478  recursion_set.erase(identifier);
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()=="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
targett add_instruction()
Adds an instruction at the end.
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:275
goto_programt::const_targett locationt
Definition: ai.h:112
exprt simplify_expr(const exprt &src, const namespacet &ns)
instructionst instructions
The list of instructions in the goto program.
Definition: json.h:21
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
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
bool empty() const
Is the program empty?
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
std::list< Target > get_successors(Target target) const
Extract member of struct or union.
Definition: std_expr.h:3214
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast a generic exprt to a dereference_exprt.
Definition: std_expr.h:2748
std::map< unsigned, locationt > working_sett
Definition: ai.h:271
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
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:157
const exprt & compound() const
Definition: std_expr.h:3281
const irep_idt & id() const
Definition: irep.h:189
instructionst::const_iterator const_targett
argumentst & arguments()
Definition: std_code.h:689
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:442
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:379
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
Definition: ai.h:93
Operator to dereference a pointer.
Definition: std_expr.h:2701
API to expression classes.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void entry_state(const goto_programt &)
Definition: ai.cpp:258
Definition: xml.h:18
virtual const statet & find_state(locationt l) const =0
A function call.
Definition: std_code.h:657
virtual bool merge_shared(const statet &src, locationt from, locationt to, const namespacet &ns)=0
std::string data
Definition: xml.h:30
goto_function_templatet< goto_programt > goto_functiont
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:49
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
bool fixedpoint(const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:295
bool visit(locationt l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:321
exprt & index()
Definition: std_expr.h:1208
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:677
Definition: ai.h:108
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai.cpp:34
Base class for all expressions.
Definition: expr.h:46
exprt & pointer()
Definition: std_expr.h:2727
virtual void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: ai.h:56
locationt get_next(working_sett &working_set)
Definition: ai.cpp:283
virtual statet * make_temporary_state(const statet &s)=0
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
void concurrent_fixedpoint(const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:537
recursion_sett recursion_set
Definition: ai.h:309
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)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
array index operator
Definition: std_expr.h:1170