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/mp_arith.h>
17 
18 #include "ai.h"
19 #include "interval_template.h"
20 
23 
25 {
26 public:
27  // Trivial, conjunctive interval domain for both float
28  // and integers. The categorization 'float' and 'integers'
29  // is done by is_int and is_float.
30 
32  {
33  }
34 
35  void
36  transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
37  final override;
38 
39  void output(
40  std::ostream &out,
41  const ai_baset &ai,
42  const namespacet &ns) const override;
43 
44 protected:
45  bool join(const interval_domaint &b);
46 
47 public:
48  bool merge(
49  const interval_domaint &b,
50  locationt from,
51  locationt to)
52  {
53  return join(b);
54  }
55 
56  // no states
57  void make_bottom() final override
58  {
59  int_map.clear();
60  float_map.clear();
61  bottom=true;
62  }
63 
64  // all states
65  void make_top() final override
66  {
67  int_map.clear();
68  float_map.clear();
69  bottom=false;
70  }
71 
72  void make_entry() final override
73  {
74  make_top();
75  }
76 
77  bool is_bottom() const override final
78  {
79  #if 0
80  // This invariant should hold but is not correctly enforced at the moment.
81  DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),
82  "If the domain is bottom the value maps must be empty");
83  #endif
84 
85  return bottom;
86  }
87 
88  bool is_top() const override final
89  {
90  return !bottom && int_map.empty() && float_map.empty();
91  }
92 
93  exprt make_expression(const symbol_exprt &) const;
94 
95  void assume(const exprt &, const namespacet &);
96 
97  static bool is_int(const typet &src)
98  {
99  return src.id()==ID_signedbv || src.id()==ID_unsignedbv;
100  }
101 
102  static bool is_float(const typet &src)
103  {
104  return src.id()==ID_floatbv;
105  }
106 
107  virtual bool ai_simplify(
108  exprt &condition,
109  const namespacet &ns) const override;
110 
111 protected:
112  bool bottom;
113 
114  typedef std::map<irep_idt, integer_intervalt> int_mapt;
115  typedef std::map<irep_idt, ieee_float_intervalt> float_mapt;
116 
119 
120  void havoc_rec(const exprt &);
121  void assume_rec(const exprt &, bool negation=false);
122  void assume_rec(const exprt &lhs, irep_idt id, const exprt &rhs);
123  void assign(const class code_assignt &assignment);
126 };
127 
128 #endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H
The type of an expression.
Definition: type.h:22
static bool is_float(const typet &src)
std::map< irep_idt, integer_intervalt > int_mapt
void havoc_rec(const exprt &)
interval_templatet< mp_integer > integer_intervalt
void assume(const exprt &, const namespacet &)
void make_top() final override
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
void make_entry() final override
ieee_float_intervalt get_float_rec(const exprt &)
const irep_idt & id() const
Definition: irep.h:189
std::map< irep_idt, ieee_float_intervalt > float_mapt
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void assign(const class code_assignt &assignment)
bool merge(const interval_domaint &b, locationt from, locationt to)
integer_intervalt get_int_rec(const exprt &)
TO_BE_DOCUMENTED.
Definition: namespace.h:74
interval_templatet< ieee_floatt > ieee_float_intervalt
void assume_rec(const exprt &, bool negation=false)
bool is_top() const override final
float_mapt float_map
exprt make_expression(const symbol_exprt &) const
void make_bottom() final override
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
Abstract Interpretation.
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
goto_programt::const_targett locationt
Definition: ai.h:44
Expression to hold a symbol (variable)
Definition: std_expr.h:90
static bool is_int(const typet &src)
bool is_bottom() const override final
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
Assignment.
Definition: std_code.h:195