cprover
Loading...
Searching...
No Matches
interval_domain.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interval Domain
4
5Author: 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>
18
19#include "ai_domain.h"
20
22
24{
25public:
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 trace_ptrt trace_from,
37 const irep_idt &function_to,
38 trace_ptrt trace_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
47protected:
48 bool join(const interval_domaint &b);
49
50public:
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
111protected:
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 exprt &lhs, const exprt &rhs);
126};
127
128#endif // CPROVER_ANALYSES_INTERVAL_DOMAIN_H
Abstract Interpretation Domain.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:55
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
void assign(const exprt &lhs, const exprt &rhs)
static bool is_int(const typet &src)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
bool is_bottom() const override final
void make_bottom() final override
no states
float_mapt float_map
void assume_rec(const exprt &, bool negation=false)
bool is_top() const override final
integer_intervalt get_int_rec(const exprt &)
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_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...
exprt make_expression(const symbol_exprt &) const
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
std::map< irep_idt, ieee_float_intervalt > float_mapt
ieee_float_intervalt get_float_rec(const exprt &)
bool merge(const interval_domaint &b, trace_ptrt, trace_ptrt)
void make_entry() final override
Make this domain a reasonable entry-point state.
std::map< irep_idt, integer_intervalt > int_mapt
void havoc_rec(const exprt &)
void assume(const exprt &, const namespacet &)
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
static bool is_float(const typet &src)
const irep_idt & id() const
Definition: irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The type of an expression, extends irept.
Definition: type.h:29
interval_templatet< ieee_floatt > ieee_float_intervalt
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510