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 transform(
36  const irep_idt &function_from,
37  locationt from,
38  const irep_idt &function_to,
39  locationt to,
40  ai_baset &ai,
41  const namespacet &ns) final override;
42 
43  void output(
44  std::ostream &out,
45  const ai_baset &ai,
46  const namespacet &ns) const override;
47 
48 protected:
49  bool join(const interval_domaint &b);
50 
51 public:
52  bool merge(
53  const interval_domaint &b,
54  locationt,
55  locationt)
56  {
57  return join(b);
58  }
59 
60  // no states
61  void make_bottom() final override
62  {
63  int_map.clear();
64  float_map.clear();
65  bottom=true;
66  }
67 
68  // all states
69  void make_top() final override
70  {
71  int_map.clear();
72  float_map.clear();
73  bottom=false;
74  }
75 
76  void make_entry() final override
77  {
78  make_top();
79  }
80 
81  bool is_bottom() const override final
82  {
83  #if 0
84  // This invariant should hold but is not correctly enforced at the moment.
85  DATA_INVARIANT(!bottom || (int_map.empty() && float_map.empty()),
86  "If the domain is bottom the value maps must be empty");
87  #endif
88 
89  return bottom;
90  }
91 
92  bool is_top() const override final
93  {
94  return !bottom && int_map.empty() && float_map.empty();
95  }
96 
97  exprt make_expression(const symbol_exprt &) const;
98 
99  void assume(const exprt &, const namespacet &);
100 
101  static bool is_int(const typet &src)
102  {
103  return src.id()==ID_signedbv || src.id()==ID_unsignedbv;
104  }
105 
106  static bool is_float(const typet &src)
107  {
108  return src.id()==ID_floatbv;
109  }
110 
111  virtual bool ai_simplify(
112  exprt &condition,
113  const namespacet &ns) const override;
114 
115 protected:
116  bool bottom;
117 
118  typedef std::map<irep_idt, integer_intervalt> int_mapt;
119  typedef std::map<irep_idt, ieee_float_intervalt> float_mapt;
120 
123 
124  void havoc_rec(const exprt &);
125  void assume_rec(const exprt &, bool negation=false);
126  void assume_rec(const exprt &lhs, irep_idt id, const exprt &rhs);
127  void assign(const class code_assignt &assignment);
130 };
131 
132 #endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H
The type of an expression, extends irept.
Definition: type.h:27
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 &)
bool merge(const interval_domaint &b, locationt, locationt)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
void make_entry() final override
Make this domain a reasonable entry-point state.
ieee_float_intervalt get_float_rec(const exprt &)
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, locationt to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
const irep_idt & id() const
Definition: irep.h:259
std::map< irep_idt, ieee_float_intervalt > float_mapt
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void assign(const class code_assignt &assignment)
integer_intervalt get_int_rec(const exprt &)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
interval_templatet< ieee_floatt > ieee_float_intervalt
void assume_rec(const exprt &, bool negation=false)
bool is_top() const override final
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
float_mapt float_map
exprt make_expression(const symbol_exprt &) const
void make_bottom() final override
no states
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.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:143
static bool is_int(const typet &src)
bool is_bottom() const override final
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
A codet representing an assignment in the program.
Definition: std_code.h:256