cprover
interval_domain.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval Domain
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_INTERVAL_DOMAIN_H
13 #define CPROVER_ANALYSES_INTERVAL_DOMAIN_H
14 
15 #include <util/ieee_float.h>
16 #include <util/integer_interval.h>
17 #include <util/interval_template.h>
18 
19 #include "ai.h"
20 
22 
24 {
25 public:
26  // Trivial, conjunctive interval domain for both float
27  // and integers. The categorization 'float' and 'integers'
28  // is done by is_int and is_float.
29 
31  {
32  }
33 
34  void transform(
35  const irep_idt &function_from,
36  locationt from,
37  const irep_idt &function_to,
38  locationt to,
39  ai_baset &ai,
40  const namespacet &ns) final override;
41 
42  void output(
43  std::ostream &out,
44  const ai_baset &ai,
45  const namespacet &ns) const override;
46 
47 protected:
48  bool join(const interval_domaint &b);
49 
50 public:
51  bool merge(
52  const interval_domaint &b,
53  locationt,
54  locationt)
55  {
56  return join(b);
57  }
58 
59  // no states
60  void make_bottom() final override
61  {
62  int_map.clear();
63  float_map.clear();
64  bottom=true;
65  }
66 
67  // all states
68  void make_top() final override
69  {
70  int_map.clear();
71  float_map.clear();
72  bottom=false;
73  }
74 
75  void make_entry() final override
76  {
77  make_top();
78  }
79 
80  bool is_bottom() const override final
81  {
82  #if 0
83  // This invariant should hold but is not correctly enforced at the moment.
84  DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),
85  "If the domain is bottom the value maps must be empty");
86  #endif
87 
88  return bottom;
89  }
90 
91  bool is_top() const override final
92  {
93  return !bottom && int_map.empty() && float_map.empty();
94  }
95 
96  exprt make_expression(const symbol_exprt &) const;
97 
98  void assume(const exprt &, const namespacet &);
99 
100  static bool is_int(const typet &src)
101  {
102  return src.id()==ID_signedbv || src.id()==ID_unsignedbv;
103  }
104 
105  static bool is_float(const typet &src)
106  {
107  return src.id()==ID_floatbv;
108  }
109 
110  virtual bool ai_simplify(
111  exprt &condition,
112  const namespacet &ns) const override;
113 
114 protected:
115  bool bottom;
116 
117  typedef std::map<irep_idt, integer_intervalt> int_mapt;
118  typedef std::map<irep_idt, ieee_float_intervalt> float_mapt;
119 
122 
123  void havoc_rec(const exprt &);
124  void assume_rec(const exprt &, bool negation=false);
125  void assume_rec(const exprt &lhs, irep_idt id, const exprt &rhs);
126  void assign(const class code_assignt &assignment);
129 };
130 
131 #endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H
interval_domaint::bottom
bool bottom
Definition: interval_domain.h:115
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
integer_interval.h
interval_domaint::assume
void assume(const exprt &, const namespacet &)
Definition: interval_domain.cpp:349
typet
The type of an expression, extends irept.
Definition: type.h:29
interval_domaint::is_float
static bool is_float(const typet &src)
Definition: interval_domain.h:105
interval_domaint::int_mapt
std::map< irep_idt, integer_intervalt > int_mapt
Definition: interval_domain.h:117
interval_domaint::interval_domaint
interval_domaint()
Definition: interval_domain.h:30
interval_domaint::merge
bool merge(const interval_domaint &b, locationt, locationt)
Definition: interval_domain.h:51
interval_domaint::float_mapt
std::map< irep_idt, ieee_float_intervalt > float_mapt
Definition: interval_domain.h:118
exprt
Base class for all expressions.
Definition: expr.h:53
interval_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Definition: interval_domain.cpp:23
interval_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: interval_domain.h:75
interval_domaint::assign
void assign(const class code_assignt &assignment)
Definition: interval_domain.cpp:209
interval_domaint::get_float_rec
ieee_float_intervalt get_float_rec(const exprt &)
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
interval_templatet
Definition: interval_template.h:20
interval_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: interval_domain.h:68
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
interval_template.h
interval_domaint::get_int_rec
integer_intervalt get_int_rec(const exprt &)
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
interval_domaint::assume_rec
void assume_rec(const exprt &, bool negation=false)
Definition: interval_domain.cpp:356
interval_domaint::transform
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
Definition: interval_domain.cpp:59
ieee_float_intervalt
interval_templatet< ieee_floatt > ieee_float_intervalt
Definition: interval_domain.h:21
interval_domaint::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
Definition: interval_domain.cpp:482
irept::id
const irep_idt & id() const
Definition: irep.h:418
interval_domaint::is_top
bool is_top() const override final
Definition: interval_domain.h:91
ai.h
Abstract Interpretation.
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:76
interval_domaint::is_bottom
bool is_bottom() const override final
Definition: interval_domain.h:80
interval_domaint
Definition: interval_domain.h:24
interval_domaint::float_map
float_mapt float_map
Definition: interval_domain.h:121
interval_domaint::make_expression
exprt make_expression(const symbol_exprt &) const
Definition: interval_domain.cpp:402
ieee_float.h
interval_domaint::join
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
Definition: interval_domain.cpp:151
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
interval_domaint::make_bottom
void make_bottom() final override
no states
Definition: interval_domain.h:60
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
interval_domaint::is_int
static bool is_int(const typet &src)
Definition: interval_domain.h:100
interval_domaint::havoc_rec
void havoc_rec(const exprt &)
Definition: interval_domain.cpp:215
interval_domaint::int_map
int_mapt int_map
Definition: interval_domain.h:120