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  forall_goto_program_instructions(i_it, goto_function.body)
36  {
37  find_symbols(i_it->code, symbols);
38  find_symbols(i_it->guard, symbols);
39  }
40 
41  Forall_goto_program_instructions(i_it, goto_function.body)
42  {
43  if(i_it==goto_function.body.instructions.begin())
44  {
45  // first instruction, we instrument
46  }
47  else
48  {
49  goto_programt::const_targett previous=i_it;
50  previous--;
51  if(previous->is_goto() && !previous->guard.is_true())
52  {
53  // we follow a branch, instrument
54  }
55  else if(previous->is_function_call() && !previous->guard.is_true())
56  {
57  // we follow a function call, instrument
58  }
59  else if(i_it->is_target() || i_it->is_function_call())
60  {
61  // we are a target or a function call, instrument
62  }
63  else
64  continue; // don't instrument
65  }
66 
67  const interval_domaint &d=interval_analysis[i_it];
68 
69  exprt::operandst assertion;
70 
71  for(const auto &symbol_expr : symbols)
72  {
73  exprt tmp=d.make_expression(symbol_expr);
74  if(!tmp.is_true())
75  assertion.push_back(tmp);
76  }
77 
78  if(!assertion.empty())
79  {
81  goto_function.body.insert_before_swap(i_it);
82  t->make_assumption(conjunction(assertion));
83  i_it++; // goes to original instruction
84  t->source_location=i_it->source_location;
85  t->function=i_it->function;
86  }
87  }
88 }
89 
93 void interval_analysis(goto_modelt &goto_model)
94 {
96 
97  const namespacet ns(goto_model.symbol_table);
98  interval_analysis(goto_model.goto_functions, ns);
99 
100  Forall_goto_functions(f_it, goto_model.goto_functions)
102 }
Interval Analysis.
Definition: ai.h:365
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
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:50
instructionst::iterator targett
Definition: goto_program.h:414
instructionst::const_iterator const_targett
Definition: goto_program.h:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
::goto_functiont goto_functiont
exprt make_expression(const symbol_exprt &) const
std::vector< exprt > operandst
Definition: expr.h:57
Interval Domain.
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.
Base class for all expressions.
Definition: expr.h:54
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:228
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
void interval_analysis(goto_modelt &goto_model)
Initialises the abstract interpretation over interval domain and instruments instructions using inter...
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32