cprover
interval_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
13 
14 #include "interval_analysis.h"
15 
16 #include <util/find_symbols.h>
17 
18 #include "interval_domain.h"
19 
31  goto_functionst::goto_functiont &goto_function)
32 {
33  std::set<symbol_exprt> symbols;
34 
35  for(const auto &i : goto_function.body.instructions)
36  i.apply([&symbols](const exprt &e) { find_symbols(e, symbols); });
37 
38  Forall_goto_program_instructions(i_it, goto_function.body)
39  {
40  if(i_it==goto_function.body.instructions.begin())
41  {
42  // first instruction, we instrument
43  }
44  else
45  {
46  goto_programt::const_targett previous = std::prev(i_it);
47 
48  if(previous->is_goto() && !previous->get_condition().is_true())
49  {
50  // we follow a branch, instrument
51  }
52  else if(previous->is_function_call() && !previous->guard.is_true())
53  {
54  // we follow a function call, instrument
55  }
56  else if(i_it->is_target() || i_it->is_function_call())
57  {
58  // we are a target or a function call, instrument
59  }
60  else
61  continue; // don't instrument
62  }
63 
64  const interval_domaint &d=interval_analysis[i_it];
65 
66  exprt::operandst assertion;
67 
68  for(const auto &symbol_expr : symbols)
69  {
70  exprt tmp=d.make_expression(symbol_expr);
71  if(!tmp.is_true())
72  assertion.push_back(tmp);
73  }
74 
75  if(!assertion.empty())
76  {
78  goto_function.body.insert_before_swap(i_it);
80  i_it++; // goes to original instruction
81  t->source_location=i_it->source_location;
82  }
83  }
84 }
85 
89 void interval_analysis(goto_modelt &goto_model)
90 {
92 
93  const namespacet ns(goto_model.symbol_table);
94  interval_analysis(goto_model.goto_functions, ns);
95 
96  for(auto &gf_entry : goto_model.goto_functions.function_map)
97  instrument_intervals(interval_analysis, gf_entry.second);
98 }
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:559
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
function_mapt function_map
::goto_functiont goto_functiont
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
exprt make_expression(const symbol_exprt &) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
#define Forall_goto_program_instructions(it, program)
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
void instrument_intervals(const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function)
Instruments all "post-branch" instructions with assumptions about variable intervals.
Interval Analysis.
Interval Domain.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:41