cprover
Loading...
Searching...
No Matches
constant_abstract_value.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
10
11#include <util/interval.h>
12#include <util/std_expr.h>
13
16
19
21{
22public:
23 explicit constant_index_ranget(const exprt &val)
25 {
26 }
27
29 {
31 }
32};
33
36{
37 return util_make_unique<constant_index_ranget>(val);
38}
39
41 : abstract_value_objectt(t), value()
42{
43}
44
46 : abstract_value_objectt(e.type(), false, false), value(e)
47{
48}
49
51 const typet &t,
52 bool tp,
53 bool bttm)
54 : abstract_value_objectt(t, tp, bttm), value()
55{
56}
57
59 const exprt &e,
60 const abstract_environmentt &environment,
61 const namespacet &ns)
62 : abstract_value_objectt(e.type(), false, false), value(e)
63{
64}
65
68{
69 exprt val = to_constant();
70 if(!val.is_constant())
72
73 return make_constant_index_range(val);
74}
75
78{
79 return make_single_value_range(shared_from_this());
80}
81
83{
84 if(!is_top() && !is_bottom())
85 {
86 return this->value;
87 }
88 else
89 {
91 }
92}
93
95{
97}
98
100 std::ostream &out,
101 const ai_baset &ai,
102 const namespacet &ns) const
103{
104 if(!is_top() && !is_bottom())
105 {
107 }
108 else
109 {
110 abstract_objectt::output(out, ai, ns);
111 }
112}
113
115 const abstract_value_pointert &other,
116 const widen_modet &widen_mode) const
117{
118 auto other_expr = other->to_constant();
119 if(is_bottom() && other_expr.is_constant())
120 return std::make_shared<constant_abstract_valuet>(other_expr);
121
122 if(value == other_expr) // Can we actually merge these value
123 return shared_from_this();
124
125 return abstract_objectt::merge(other, widen_mode);
126}
127
129 const abstract_value_pointert &other) const
130{
131 auto value_as_interval = constant_interval_exprt(value, value);
132 auto other_interval = other->to_interval();
133
134 if(other_interval.contains(value_as_interval)) // Do they actually meet
135 return shared_from_this();
136
137 return abstract_objectt::meet(other);
138}
139
141 const exprt &lower,
142 const exprt &upper) const
143{
144 return as_value(mutable_clone());
145}
146
148{
149 return equal_exprt(name, value);
150}
151
153 abstract_object_statisticst &statistics,
155 const abstract_environmentt &env,
156 const namespacet &ns) const
157{
158 abstract_objectt::get_statistics(statistics, visited, env, ns);
159 ++statistics.number_of_constants;
160 statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
161}
std::set< abstract_object_pointert > abstract_object_visitedt
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
index_range_implementation_ptrt make_indeterminate_index_range()
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
virtual exprt to_constant() const
Converts to a constant expression if possible.
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool is_bottom() const
Find out if the abstract object is bottom.
virtual internal_abstract_object_pointert mutable_clone() const
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
static combine_result meet(const abstract_object_pointert &op1, const abstract_object_pointert &op2)
Interface method for the meet operation.
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
sharing_ptrt< const abstract_value_objectt > as_value(const abstract_object_pointert &obj) const
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
void output(std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
value_range_implementation_ptrt value_range_implementation() const override
constant_interval_exprt to_interval() const override
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
abstract_value_pointert constrain(const exprt &lower, const exprt &upper) const override
exprt to_constant() const override
Converts to a constant expression if possible.
exprt to_predicate_internal(const exprt &name) const override
to_predicate implementation - derived classes will override
CLONE abstract_object_pointert merge_with_value(const abstract_value_pointert &other, const widen_modet &widen_mode) const override
Merges another abstract value into this one.
abstract_object_pointert meet_with_value(const abstract_value_pointert &other) const override
index_range_implementation_ptrt reset() const override
constant_index_ranget(const exprt &val)
Represents an interval of values.
Definition: interval.h:48
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
static memory_sizet from_bytes(std::size_t bytes)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The type of an expression, extends irept.
Definition: type.h:29
static index_range_implementation_ptrt make_constant_index_range(const exprt &val)
An abstraction of a single value that just stores a constant.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.