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