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 |=
307  visit_edge(function_id, p, function_id, to_l, ns, working_set);
308  }
309  }
310 
311  return new_data;
312 }
313 
315  const irep_idt &function_id,
316  trace_ptrt p,
317  const irep_idt &to_function_id,
318  locationt to_l,
319  const namespacet &ns,
320  working_sett &working_set)
321 {
322  // Has history taught us not to step here...
323  auto next = p->step(to_l, *(storage->abstract_traces_before(to_l)));
325  return false;
326  trace_ptrt to_p = next.second;
327 
328  // Abstract domains are mutable so we must copy before we transform
329  statet &current = get_state(p);
330 
331  std::unique_ptr<statet> tmp_state(make_temporary_state(current));
332  statet &new_values = *tmp_state;
333 
334  // Apply transformer
335  new_values.transform(function_id, p, to_function_id, to_p, *this, ns);
336 
337  // Expanding a domain means that it has to be analysed again
338  // Likewise if the history insists that it is a new trace
339  // (assuming it is actually reachable).
340  if(
341  merge(new_values, p, to_p) ||
342  (next.first == ai_history_baset::step_statust::NEW &&
343  !new_values.is_bottom()))
344  {
345  put_in_working_set(working_set, to_p);
346  return true;
347  }
348 
349  return false;
350 }
351 
353  const irep_idt &calling_function_id,
354  trace_ptrt p_call,
355  locationt l_return,
356  const irep_idt &,
357  working_sett &working_set,
358  const goto_programt &,
359  const goto_functionst &,
360  const namespacet &ns)
361 {
362  // The default implementation is not interprocedural
363  // so the effects of the call are approximated but nothing else
364  return visit_edge(
365  calling_function_id,
366  p_call,
367  calling_function_id,
368  l_return,
369  ns,
370  working_set);
371 }
372 
374  const irep_idt &calling_function_id,
375  trace_ptrt p_call,
376  working_sett &working_set,
377  const goto_programt &caller,
378  const goto_functionst &goto_functions,
379  const namespacet &ns)
380 {
381  locationt l_call = p_call->current_location();
382 
383  PRECONDITION(l_call->is_function_call());
384 
385  locationt l_return = std::next(l_call);
386 
387  // operator() allows analysis of a single goto_program independently
388  // it generates a synthetic goto_functions object for this
389  if(!goto_functions.function_map.empty())
390  {
391  const code_function_callt &code = to_code_function_call(l_call->code);
392  const exprt &callee_expression = code.function();
393 
394  if(callee_expression.id() == ID_symbol)
395  {
396  const irep_idt &callee_function_id =
397  to_symbol_expr(callee_expression).get_identifier();
398 
399  goto_functionst::function_mapt::const_iterator it =
400  goto_functions.function_map.find(callee_function_id);
401 
403  it != goto_functions.function_map.end(),
404  "Function " + id2string(callee_function_id) + "not in function map");
405 
406  const goto_functionst::goto_functiont &callee_fun = it->second;
407 
408  if(callee_fun.body_available())
409  {
411  calling_function_id,
412  p_call,
413  l_return,
414  callee_function_id,
415  working_set,
416  callee_fun.body,
417  goto_functions,
418  ns);
419  }
420  else
421  {
422  // Fall through to the default, body not available, case
423  }
424  }
425  else
426  {
427  // Function pointers are not currently supported and must be removed
429  callee_expression.id() == ID_symbol,
430  "Function pointers and indirect calls must be removed before "
431  "analysis.");
432  }
433  }
434 
435  // If the body is not available then we just do the edge from call to return
436  // in the caller. Domains should over-approximate what the function might do.
437  return visit_edge(
438  calling_function_id,
439  p_call,
440  calling_function_id,
441  l_return,
442  ns,
443  working_set);
444 }
445 
447  const irep_idt &function_id,
448  trace_ptrt p,
449  working_sett &working_set,
450  const goto_programt &goto_program,
451  const goto_functionst &goto_functions,
452  const namespacet &ns)
453 {
454  locationt l = p->current_location();
455  PRECONDITION(l->is_end_function());
456 
457  // Do nothing
458  return false;
459 }
460 
462  const irep_idt &calling_function_id,
463  trace_ptrt p_call,
464  locationt l_return,
465  const irep_idt &callee_function_id,
466  working_sett &working_set,
467  const goto_programt &callee,
468  const goto_functionst &goto_functions,
469  const namespacet &ns)
470 {
471  // This is the edge from call site to function head.
472  {
473  locationt l_begin = callee.instructions.begin();
474 
475  working_sett catch_working_set; // The trace from the next fixpoint
476 
477  // Do the edge from the call site to the beginning of the function
478  bool new_data = visit_edge(
479  calling_function_id,
480  p_call,
481  callee_function_id,
482  l_begin,
483  ns,
484  catch_working_set);
485 
486  // do we need to do/re-do the fixedpoint of the body?
487  if(new_data)
488  fixedpoint(
489  get_next(catch_working_set),
490  callee_function_id,
491  callee,
492  goto_functions,
493  ns);
494  }
495 
496  // This is the edge from function end to return site.
497  {
498  // get location at end of the procedure we have called
499  locationt l_end = --callee.instructions.end();
501  l_end->is_end_function(),
502  "The last instruction of a goto_program must be END_FUNCTION");
503 
504  // Find the histories for a location
505  auto traces = storage->abstract_traces_before(l_end);
506 
507  bool new_data = false;
508 
509  // The history used may mean there are multiple histories at the end of the
510  // function. Some of these can be progressed (for example, if the history
511  // tracks paths within functions), some can't be (for example, not all
512  // calling contexts will be appropriate). We rely on the history's step,
513  // called from visit_edge to prune as applicable.
514  for(auto p_end : *traces)
515  {
516  // do edge from end of function to instruction after call
517  const statet &end_state = get_state(p_end);
518 
519  if(!end_state.is_bottom())
520  {
521  // function exit point reachable in that history
522 
523  new_data |= visit_edge(
524  callee_function_id,
525  p_end,
526  calling_function_id,
527  l_return,
528  ns,
529  working_set);
530  }
531  }
532 
533  return new_data;
534  }
535 }
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:289
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:446
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:410
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:373
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:500
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:415
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
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:25
ai_domain_baset::is_bottom
virtual bool is_bottom() const =0
json_arrayt
Definition: json.h:163
json_objectt
Definition: json.h:298
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:1186
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:510
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:506
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:486
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:1297
ai.h
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:19
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:493
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::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:352
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
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:210
code_function_callt::function
exprt & function()
Definition: std_code.h:1221
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:93
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:461
ai_baset::visit_edge
bool visit_edge(const irep_idt &function_id, trace_ptrt p, const irep_idt &to_function_id, locationt to_l, const namespacet &ns, working_sett &working_set)
Definition: ai.cpp:314
json_stringt
Definition: json.h:268