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 <memory>
15 #include <sstream>
16 #include <type_traits>
17 
18 #include <util/invariant.h>
19 #include <util/std_code.h>
20 
22  const namespacet &ns,
23  const goto_functionst &goto_functions,
24  std::ostream &out) const
25 {
26  for(const auto &gf_entry : goto_functions.function_map)
27  {
28  if(gf_entry.second.body_available())
29  {
30  out << "////\n";
31  out << "//// Function: " << gf_entry.first << "\n";
32  out << "////\n";
33  out << "\n";
34 
35  output(ns, gf_entry.first, gf_entry.second.body, out);
36  }
37  }
38 }
39 
41  const namespacet &ns,
42  const irep_idt &function_id,
43  const goto_programt &goto_program,
44  std::ostream &out) const
45 {
46  forall_goto_program_instructions(i_it, goto_program)
47  {
48  out << "**** " << i_it->location_number << " " << i_it->source_location()
49  << "\n";
50 
51  abstract_state_before(i_it)->output(out, *this, ns);
52  out << "\n";
53  #if 1
54  goto_program.output_instruction(ns, function_id, out, *i_it);
55  out << "\n";
56  #endif
57  }
58 }
59 
61  const namespacet &ns,
62  const goto_functionst &goto_functions) const
63 {
64  json_objectt result;
65 
66  for(const auto &gf_entry : goto_functions.function_map)
67  {
68  if(gf_entry.second.body_available())
69  {
70  result[id2string(gf_entry.first)] =
71  output_json(ns, gf_entry.first, gf_entry.second.body);
72  }
73  else
74  {
75  result[id2string(gf_entry.first)] = json_arrayt();
76  }
77  }
78 
79  return std::move(result);
80 }
81 
83  const namespacet &ns,
84  const irep_idt &function_id,
85  const goto_programt &goto_program) const
86 {
87  json_arrayt contents;
88 
89  forall_goto_program_instructions(i_it, goto_program)
90  {
91  // Ideally we need output_instruction_json
92  std::ostringstream out;
93  goto_program.output_instruction(ns, function_id, out, *i_it);
94 
95  json_objectt location{
96  {"locationNumber", json_numbert(std::to_string(i_it->location_number))},
97  {"sourceLocation", json_stringt(i_it->source_location().as_string())},
98  {"abstractState", abstract_state_before(i_it)->output_json(*this, ns)},
99  {"instruction", json_stringt(out.str())}};
100 
101  contents.push_back(std::move(location));
102  }
103 
104  return std::move(contents);
105 }
106 
108  const namespacet &ns,
109  const goto_functionst &goto_functions) const
110 {
111  xmlt program("program");
112 
113  for(const auto &gf_entry : goto_functions.function_map)
114  {
115  xmlt function(
116  "function",
117  {{"name", id2string(gf_entry.first)},
118  {"body_available", gf_entry.second.body_available() ? "true" : "false"}},
119  {});
120 
121  if(gf_entry.second.body_available())
122  {
123  function.new_element(
124  output_xml(ns, gf_entry.first, gf_entry.second.body));
125  }
126 
127  program.new_element(function);
128  }
129 
130  return program;
131 }
132 
134  const namespacet &ns,
135  const irep_idt &function_id,
136  const goto_programt &goto_program) const
137 {
138  xmlt function_body;
139 
140  forall_goto_program_instructions(i_it, goto_program)
141  {
142  xmlt location(
143  "",
144  {{"location_number", std::to_string(i_it->location_number)},
145  {"source_location", i_it->source_location().as_string()}},
146  {abstract_state_before(i_it)->output_xml(*this, ns)});
147 
148  // Ideally we need output_instruction_xml
149  std::ostringstream out;
150  goto_program.output_instruction(ns, function_id, out, *i_it);
151  location.set_attribute("instruction", out.str());
152 
153  function_body.new_element(location);
154  }
155 
156  return function_body;
157 }
158 
161 {
162  // find the 'entry function'
163 
164  goto_functionst::function_mapt::const_iterator
165  f_it=goto_functions.function_map.find(goto_functions.entry_point());
166 
167  if(f_it!=goto_functions.function_map.end())
168  return entry_state(f_it->second.body);
169 
170  // It is not clear if this is even a well-structured goto_functionst object
171  return nullptr;
172 }
173 
175 {
176  // The first instruction of 'goto_program' is the entry point
177  trace_ptrt p = history_factory->epoch(goto_program.instructions.begin());
178  get_state(p).make_entry();
179  return p;
180 }
181 
183  const irep_idt &function_id,
184  const goto_functionst::goto_functiont &goto_function)
185 {
186  initialize(function_id, goto_function.body);
187 }
188 
189 void ai_baset::initialize(const irep_idt &, const goto_programt &goto_program)
190 {
191  // Domains are created and set to bottom on access.
192  // So we do not need to set them to be bottom before hand.
193 }
194 
195 void ai_baset::initialize(const goto_functionst &goto_functions)
196 {
197  for(const auto &gf_entry : goto_functions.function_map)
198  initialize(gf_entry.first, gf_entry.second);
199 }
200 
202 {
203  // Nothing to do per default
204 }
205 
207 {
208  PRECONDITION(!working_set.empty());
209 
210  static_assert(
211  std::is_same<
212  working_sett,
213  std::set<trace_ptrt, ai_history_baset::compare_historyt>>::value,
214  "begin must return the minimal entry");
215  auto first = working_set.begin();
216 
217  trace_ptrt t = *first;
218 
219  working_set.erase(first);
220 
221  return t;
222 }
223 
225  trace_ptrt start_trace,
226  const irep_idt &function_id,
227  const goto_programt &goto_program,
228  const goto_functionst &goto_functions,
229  const namespacet &ns)
230 {
231  PRECONDITION(start_trace != nullptr);
232 
233  working_sett working_set;
234  put_in_working_set(working_set, start_trace);
235 
236  bool new_data=false;
237 
238  while(!working_set.empty())
239  {
240  trace_ptrt p = get_next(working_set);
241 
242  // goto_program is really only needed for iterator manipulation
243  if(visit(function_id, p, working_set, goto_program, goto_functions, ns))
244  new_data=true;
245  }
246 
247  return new_data;
248 }
249 
251  trace_ptrt start_trace,
252  const goto_functionst &goto_functions,
253  const namespacet &ns)
254 {
255  goto_functionst::function_mapt::const_iterator f_it =
256  goto_functions.function_map.find(goto_functions.entry_point());
257 
258  if(f_it != goto_functions.function_map.end())
259  fixedpoint(start_trace, f_it->first, f_it->second.body, goto_functions, ns);
260 }
261 
263  const irep_idt &function_id,
264  trace_ptrt p,
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  locationt l = p->current_location();
273 
274  log.progress() << "ai_baset::visit " << l->location_number << " in "
275  << function_id << messaget::eom;
276 
277  // Function call and end are special cases
278  if(l->is_function_call())
279  {
281  goto_program.get_successors(l).size() == 1,
282  "function calls only have one successor");
283 
285  *(goto_program.get_successors(l).begin()) == std::next(l),
286  "function call successor / return location must be the next instruction");
287 
288  new_data = visit_function_call(
289  function_id, p, working_set, goto_program, goto_functions, ns);
290  }
291  else if(l->is_end_function())
292  {
294  goto_program.get_successors(l).empty(),
295  "The end function instruction should have no successors.");
296 
297  new_data = visit_end_function(
298  function_id, p, working_set, goto_program, goto_functions, ns);
299  }
300  else
301  {
302  // Successors can be empty, for example assume(0).
303  // Successors can contain duplicates, for example GOTO next;
304  for(const auto &to_l : goto_program.get_successors(l))
305  {
306  if(to_l == goto_program.instructions.end())
307  continue;
308 
309  new_data |= visit_edge(
310  function_id,
311  p,
312  function_id,
313  to_l,
315  ns,
316  working_set); // Local steps so no caller history needed
317  }
318  }
319 
320  return new_data;
321 }
322 
324  const irep_idt &function_id,
325  trace_ptrt p,
326  const irep_idt &to_function_id,
327  locationt to_l,
328  trace_ptrt caller_history,
329  const namespacet &ns,
330  working_sett &working_set)
331 {
333  log.progress() << "ai_baset::visit_edge from "
334  << p->current_location()->location_number << " to "
335  << to_l->location_number << "... ";
336 
337  // Has history taught us not to step here...
338  auto next =
339  p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);
341  {
342  log.progress() << "blocked by history" << messaget::eom;
343  return false;
344  }
345  else if(next.first == ai_history_baset::step_statust::NEW)
346  {
347  log.progress() << "gives a new history... ";
348  }
349  else
350  {
351  log.progress() << "merges with existing history... ";
352  }
353  trace_ptrt to_p = next.second;
354 
355  // Abstract domains are mutable so we must copy before we transform
356  statet &current = get_state(p);
357 
358  std::unique_ptr<statet> tmp_state(make_temporary_state(current));
359  statet &new_values = *tmp_state;
360 
361  // Apply transformer
362  log.progress() << "applying transformer... ";
363  new_values.transform(function_id, p, to_function_id, to_p, *this, ns);
364 
365  // Expanding a domain means that it has to be analysed again
366  // Likewise if the history insists that it is a new trace
367  // (assuming it is actually reachable).
368  log.progress() << "merging... ";
369  bool return_value = false;
370  if(
371  merge(new_values, p, to_p) ||
372  (next.first == ai_history_baset::step_statust::NEW &&
373  !new_values.is_bottom()))
374  {
375  put_in_working_set(working_set, to_p);
376  log.progress() << "result queued." << messaget::eom;
377  return_value = true;
378  }
379  else
380  {
381  log.progress() << "domain unchanged." << messaget::eom;
382  }
383 
384  // Branch because printing some histories and domains can be expensive
385  // esp. if the output is then just discarded and this is a critical path.
386  if(message_handler.get_verbosity() >= messaget::message_levelt::M_DEBUG)
387  {
388  log.debug() << "p = ";
389  p->output(log.debug());
390  log.debug() << messaget::eom;
391 
392  log.debug() << "current = ";
393  current.output(log.debug(), *this, ns);
394  log.debug() << messaget::eom;
395 
396  log.debug() << "to_p = ";
397  to_p->output(log.debug());
398  log.debug() << messaget::eom;
399 
400  log.debug() << "new_values = ";
401  new_values.output(log.debug(), *this, ns);
402  log.debug() << messaget::eom;
403  }
404 
405  return return_value;
406 }
407 
409  const irep_idt &calling_function_id,
410  trace_ptrt p_call,
411  locationt l_return,
412  const irep_idt &,
413  working_sett &working_set,
414  const goto_programt &,
415  const goto_functionst &,
416  const namespacet &ns)
417 {
419  log.progress() << "ai_baset::visit_edge_function_call from "
420  << p_call->current_location()->location_number << " to "
421  << l_return->location_number << messaget::eom;
422 
423  // The default implementation is not interprocedural
424  // so the effects of the call are approximated but nothing else
425  return visit_edge(
426  calling_function_id,
427  p_call,
428  calling_function_id,
429  l_return,
431  no_caller_history, // Not needed as we are skipping the function call
432  ns,
433  working_set);
434 }
435 
437  const irep_idt &calling_function_id,
438  trace_ptrt p_call,
439  working_sett &working_set,
440  const goto_programt &caller,
441  const goto_functionst &goto_functions,
442  const namespacet &ns)
443 {
444  locationt l_call = p_call->current_location();
445 
446  PRECONDITION(l_call->is_function_call());
447 
449  log.progress() << "ai_baset::visit_function_call at "
450  << l_call->location_number << messaget::eom;
451 
452  locationt l_return = std::next(l_call);
453 
454  // operator() allows analysis of a single goto_program independently
455  // it generates a synthetic goto_functions object for this
456  if(!goto_functions.function_map.empty())
457  {
458  const exprt &callee_expression = l_call->call_function();
459 
460  if(callee_expression.id() == ID_symbol)
461  {
462  const irep_idt &callee_function_id =
463  to_symbol_expr(callee_expression).get_identifier();
464 
465  log.progress() << "Calling " << callee_function_id << messaget::eom;
466 
467  goto_functionst::function_mapt::const_iterator it =
468  goto_functions.function_map.find(callee_function_id);
469 
471  it != goto_functions.function_map.end(),
472  "Function " + id2string(callee_function_id) + "not in function map");
473 
474  const goto_functionst::goto_functiont &callee_fun = it->second;
475 
476  if(callee_fun.body_available())
477  {
479  calling_function_id,
480  p_call,
481  l_return,
482  callee_function_id,
483  working_set,
484  callee_fun.body,
485  goto_functions,
486  ns);
487  }
488  else
489  {
490  // Fall through to the default, body not available, case
491  }
492  }
493  else
494  {
495  // Function pointers are not currently supported and must be removed
497  callee_expression.id() == ID_symbol,
498  "Function pointers and indirect calls must be removed before "
499  "analysis.");
500  }
501  }
502 
503  // If the body is not available then we just do the edge from call to return
504  // in the caller. Domains should over-approximate what the function might do.
505  return visit_edge(
506  calling_function_id,
507  p_call,
508  calling_function_id,
509  l_return,
510  ai_history_baset::no_caller_history, // Would be the same as p_call...
511  ns,
512  working_set);
513 }
514 
516  const irep_idt &function_id,
517  trace_ptrt p,
518  working_sett &working_set,
519  const goto_programt &goto_program,
520  const goto_functionst &goto_functions,
521  const namespacet &ns)
522 {
523  locationt l = p->current_location();
524  PRECONDITION(l->is_end_function());
525 
527  log.progress() << "ai_baset::visit_end_function " << function_id
528  << messaget::eom;
529 
530  // Do nothing
531  return false;
532 }
533 
535  const irep_idt &calling_function_id,
536  trace_ptrt p_call,
537  locationt l_return,
538  const irep_idt &callee_function_id,
539  working_sett &working_set,
540  const goto_programt &callee,
541  const goto_functionst &goto_functions,
542  const namespacet &ns)
543 {
545  log.progress() << "ai_recursive_interproceduralt::visit_edge_function_call"
546  << " from " << p_call->current_location()->location_number
547  << " to " << l_return->location_number << messaget::eom;
548 
549  // This is the edge from call site to function head.
550  {
551  locationt l_begin = callee.instructions.begin();
552 
553  working_sett catch_working_set; // The trace from the next fixpoint
554 
555  // Do the edge from the call site to the beginning of the function
556  bool new_data = visit_edge(
557  calling_function_id,
558  p_call,
559  callee_function_id,
560  l_begin,
562  no_caller_history, // Not needed as p_call already has the info
563  ns,
564  catch_working_set);
565 
566  log.progress() << "Handle " << callee_function_id << " recursively"
567  << messaget::eom;
568 
569  // do we need to do/re-do the fixedpoint of the body?
570  if(new_data)
571  fixedpoint(
572  get_next(catch_working_set),
573  callee_function_id,
574  callee,
575  goto_functions,
576  ns);
577  }
578 
579  // This is the edge from function end to return site.
580  {
581  log.progress() << "Handle return edges" << messaget::eom;
582 
583  // get location at end of the procedure we have called
584  locationt l_end = --callee.instructions.end();
586  l_end->is_end_function(),
587  "The last instruction of a goto_program must be END_FUNCTION");
588 
589  // Find the histories for a location
590  auto traces = storage->abstract_traces_before(l_end);
591 
592  bool new_data = false;
593 
594  // The history used may mean there are multiple histories at the end of the
595  // function. Some of these can be progressed (for example, if the history
596  // tracks paths within functions), some can't be (for example, not all
597  // calling contexts will be appropriate). We rely on the history's step,
598  // called from visit_edge to prune as applicable.
599  for(auto p_end : *traces)
600  {
601  // do edge from end of function to instruction after call
602  const statet &end_state = get_state(p_end);
603 
604  if(!end_state.is_bottom())
605  {
606  // function exit point reachable in that history
607 
608  new_data |= visit_edge(
609  callee_function_id,
610  p_end,
611  calling_function_id,
612  l_return,
613  p_call, // To allow function-local history
614  ns,
615  working_set);
616  }
617  }
618 
619  return new_data;
620  }
621 }
Abstract Interpretation.
goto_programt::const_targett locationt
Definition: ai.h:126
virtual bool visit(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Perform one step of abstract interpretation from trace t Depending on the instruction type it may com...
Definition: ai.cpp:262
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:60
std::unique_ptr< ai_storage_baset > storage
Definition: ai.h:513
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:107
bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, trace_ptrt caller_history, const namespacet &ns, working_sett &working_set)
Definition: ai.cpp:323
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition: ai.cpp:40
message_handlert & message_handler
Definition: ai.h:523
virtual bool visit_end_function(const irep_idt &function_id, trace_ptrt p, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:515
virtual bool visit_function_call(const irep_idt &function_id, trace_ptrt p_call, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:436
trace_ptrt 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:174
virtual bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns)
Definition: ai.cpp:408
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:189
virtual std::unique_ptr< statet > make_temporary_state(const statet &s)
Make a copy of a state.
Definition: ai.h:507
virtual bool fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, 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:224
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai.h:123
void put_in_working_set(working_sett &working_set, trace_ptrt t)
Definition: ai.h:421
trace_ptrt get_next(working_sett &working_set)
Get the next location from the work queue.
Definition: ai.cpp:206
trace_sett working_sett
The work queue, sorted using the history's ordering operator.
Definition: ai.h:416
virtual bool merge(const statet &src, trace_ptrt from, trace_ptrt to)
Merge the state src, flowing from tracet from to tracet to, into the state currently stored for trace...
Definition: ai.h:500
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:223
std::unique_ptr< ai_history_factory_baset > history_factory
For creating history objects.
Definition: ai.h:493
virtual void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: ai.cpp:201
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition: ai.h:517
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
virtual bool is_bottom() const =0
virtual void transform(const irep_idt &function_from, trace_ptrt from, const irep_idt &function_to, trace_ptrt 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...
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition: ai_domain.h:105
virtual void make_entry()=0
Make this domain a reasonable entry-point state.
A history object is an abstraction / representation of the control-flow part of a set of traces.
Definition: ai_history.h:37
static const trace_ptrt no_caller_history
Definition: ai_history.h:121
bool visit_edge_function_call(const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, const irep_idt &callee_function_id, working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, const namespacet &ns) override
Definition: ai.cpp:534
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
const irep_idt & id() const
Definition: irep.h:396
jsont & push_back(const jsont &json)
Definition: json.h:212
Definition: json.h:27
unsigned get_verbosity() const
Definition: message.h:54
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & progress() const
Definition: message.h:424
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
const irep_idt & get_identifier() const
Definition: std_expr.h:109
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.