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  Forall_goto_functions(f_it, goto_model.goto_functions)
98 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
conjunction
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:51
exprt
Base class for all expressions.
Definition: expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
goto_modelt
Definition: goto_model.h:26
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
find_symbols.h
instrument_intervals
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.
Definition: interval_analysis.cpp:29
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
find_symbols
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,...
Definition: find_symbols.cpp:23
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
interval_domain.h
Interval Domain.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
interval_domaint
Definition: interval_domain.h:24
interval_domaint::make_expression
exprt make_expression(const symbol_exprt &) const
Definition: interval_domain.cpp:402
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
interval_analysis.h
Interval Analysis.
interval_analysis
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
Definition: interval_analysis.cpp:89