cprover
abstract_value_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Jez Higgins, jez@jezuk.co.uk
6 
7 \*******************************************************************/
8 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_VALUE_OBJECT_H
14 
16 #include <util/interval.h>
17 
19 {
20 };
21 
23 
25  std::unique_ptr<index_range_implementationt>;
26 
28 {
29 public:
30  virtual ~index_range_implementationt() = default;
31 
33 
34  virtual const exprt &current() const = 0;
35  virtual bool advance_to_next() = 0;
36 };
37 
39 {
40 public:
41  const exprt &operator*() const
42  {
43  return range->current();
44  }
45  void operator++()
46  {
47  active = range->advance_to_next();
48  }
49  bool operator==(const index_range_iteratort &other) const
50  {
51  if(!active && !other.active)
52  return true;
53  return false;
54  }
55  bool operator!=(const index_range_iteratort &other) const
56  {
57  return !operator==(other);
58  }
59 
61  : range(std::move(rhs.range)), active(rhs.active)
62  {
63  }
66 
67 private:
68  index_range_iteratort() : range(nullptr), active(false)
69  {
70  }
72  : range(std::move(r)), active(true)
73  {
74  active = range->advance_to_next();
75  }
76 
78  bool active;
79 
80  friend class index_ranget;
81 };
82 
84 {
85 public:
87  {
88  }
89  index_ranget(index_ranget &&rhs) : range(rhs.range.release())
90  {
91  }
92  index_ranget(const index_ranget &) = delete;
93  ~index_ranget() = default;
94 
96  {
97  return index_range_iteratort{range->reset()};
98  }
100  {
101  return {};
102  }
103 
104 private:
106 };
107 
109 {
110 protected:
111  explicit single_value_index_ranget(const exprt &val);
112 
113 public:
114  const exprt &current() const override;
115  bool advance_to_next() override;
116 
117 protected:
118  const exprt value;
119 
120 private:
121  bool available;
122 };
123 
126 
128 
130  std::unique_ptr<value_range_implementationt>;
131 
133 {
134 public:
135  virtual ~value_range_implementationt() = default;
136 
138 
139  virtual const abstract_object_pointert &current() const = 0;
140  virtual bool advance_to_next() = 0;
141 };
142 
144 {
145 public:
147  {
148  return range->current();
149  }
150  void operator++()
151  {
152  active = range->advance_to_next();
153  }
154  bool operator==(const value_range_iteratort &other) const
155  {
156  if(!active && !other.active)
157  return true;
158  return false;
159  }
160  bool operator!=(const value_range_iteratort &other) const
161  {
162  return !operator==(other);
163  }
164 
166  : range(std::move(rhs.range)), active(rhs.active)
167  {
168  }
171 
172 private:
173  value_range_iteratort() : range(nullptr), active(false)
174  {
175  }
177  : range(std::move(r)), active(true)
178  {
179  active = range->advance_to_next();
180  }
181 
183  bool active;
184 
185  friend class value_ranget;
186 };
187 
189 {
190 public:
192 
194  {
195  }
196  value_ranget(value_ranget &&rhs) : range(rhs.range.release())
197  {
198  }
199  value_ranget(const value_ranget &) = delete;
200  ~value_ranget() = default;
201 
203  {
204  return value_range_iteratort{range->reset()};
205  }
207  {
208  return {};
209  }
210 
211 private:
213 };
214 
217 
219 {
220 public:
221  const abstract_object_pointert &current() const override
222  {
223  return nothing;
224  }
225  bool advance_to_next() override
226  {
227  return false;
228  }
230  {
231  return util_make_unique<empty_value_ranget>();
232  }
233 
234 private:
236 };
237 
239  public abstract_value_tag
240 {
241 public:
243  {
244  }
245 
246  abstract_value_objectt(const typet &type, bool tp, bool bttm)
247  : abstract_objectt(type, tp, bttm)
248  {
249  }
250 
252  const exprt &expr,
253  const abstract_environmentt &environment,
254  const namespacet &ns)
255  : abstract_objectt(expr, environment, ns)
256  {
257  }
258 
260  {
262  }
263 
265  {
267  }
268 
270 
284  const exprt &expr,
285  const std::vector<abstract_object_pointert> &operands,
286  const abstract_environmentt &environment,
287  const namespacet &ns) const final;
288 
289 protected:
292 
295 };
296 
298 
299 #endif
index_ranget
Definition: abstract_value_object.h:84
single_value_index_ranget
Definition: abstract_value_object.h:109
value_range_implementationt::reset
virtual value_range_implementation_ptrt reset() const =0
abstract_value_pointert
sharing_ptrt< const abstract_value_objectt > abstract_value_pointert
Definition: abstract_value_object.h:297
index_ranget::index_ranget
index_ranget(index_ranget &&rhs)
Definition: abstract_value_object.h:89
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
make_indeterminate_index_range
index_range_implementation_ptrt make_indeterminate_index_range()
Definition: abstract_value_object.cpp:79
abstract_value_objectt::value_range
value_ranget value_range() const
Definition: abstract_value_object.h:264
index_range_implementationt
Definition: abstract_value_object.h:28
make_empty_index_range
index_range_implementation_ptrt make_empty_index_range()
Definition: abstract_value_object.cpp:74
typet
The type of an expression, extends irept.
Definition: type.h:28
empty_value_ranget
Definition: abstract_value_object.h:219
index_range_iteratort::operator++
void operator++()
Definition: abstract_value_object.h:45
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
value_range_iteratort::operator!=
bool operator!=(const value_range_iteratort &other) const
Definition: abstract_value_object.h:160
index_ranget::end
index_range_iteratort end() const
Definition: abstract_value_object.h:99
single_value_index_ranget::current
const exprt & current() const override
Definition: abstract_value_object.cpp:62
value_range_iteratort::operator++
void operator++()
Definition: abstract_value_object.h:150
value_range_iteratort::value_range_iteratort
value_range_iteratort(value_range_implementation_ptrt &&r)
Definition: abstract_value_object.h:176
empty_value_ranget::nothing
abstract_object_pointert nothing
Definition: abstract_value_object.h:235
index_range_iteratort::index_range_iteratort
index_range_iteratort()
Definition: abstract_value_object.h:68
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
sharing_ptrt
std::shared_ptr< const T > sharing_ptrt
Merge is designed to allow different abstractions to be merged gracefully.
Definition: abstract_object.h:73
single_value_index_ranget::value
const exprt value
Definition: abstract_value_object.h:118
value_ranget::value_ranget
value_ranget(value_range_implementation_ptrt r)
Definition: abstract_value_object.h:193
interval.h
value_range_iteratort::active
bool active
Definition: abstract_value_object.h:183
abstract_value_objectt::index_range_implementation
virtual index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const =0
value_range_iteratort::value_range_iteratort
value_range_iteratort(const value_range_iteratort &)=delete
abstract_object.h
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
abstract_value_objectt::value_range_implementation
virtual value_range_implementation_ptrt value_range_implementation() const =0
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
index_range_implementationt::advance_to_next
virtual bool advance_to_next()=0
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.h:251
value_ranget::range
value_range_implementation_ptrt range
Definition: abstract_value_object.h:212
value_ranget::end
value_range_iteratort end() const
Definition: abstract_value_object.h:206
value_range_iteratort::value_range_iteratort
value_range_iteratort(value_range_iteratort &&rhs)
Definition: abstract_value_object.h:165
single_value_index_ranget::single_value_index_ranget
single_value_index_ranget(const exprt &val)
Definition: abstract_value_object.cpp:57
value_ranget::value_type
abstract_object_pointert value_type
Definition: abstract_value_object.h:191
value_range_iteratort::operator*
const abstract_object_pointert & operator*() const
Definition: abstract_value_object.h:146
abstract_value_tag
Definition: abstract_value_object.h:19
empty_value_ranget::current
const abstract_object_pointert & current() const override
Definition: abstract_value_object.h:221
index_range_iteratort::~index_range_iteratort
~index_range_iteratort()=default
abstract_value_objectt
Definition: abstract_value_object.h:240
value_range_iteratort
Definition: abstract_value_object.h:144
index_range_iteratort
Definition: abstract_value_object.h:39
index_range_iteratort::active
bool active
Definition: abstract_value_object.h:78
value_range_implementationt
Definition: abstract_value_object.h:133
index_range_implementationt::current
virtual const exprt & current() const =0
value_range_iteratort::value_range_iteratort
value_range_iteratort()
Definition: abstract_value_object.h:173
value_range_implementationt::advance_to_next
virtual bool advance_to_next()=0
empty_value_ranget::reset
value_range_implementation_ptrt reset() const override
Definition: abstract_value_object.h:229
make_single_value_range
value_range_implementation_ptrt make_single_value_range(const abstract_object_pointert &value)
Definition: abstract_value_object.cpp:113
index_range_implementationt::reset
virtual index_range_implementation_ptrt reset() const =0
value_range_iteratort::operator==
bool operator==(const value_range_iteratort &other) const
Definition: abstract_value_object.h:154
index_range_iteratort::operator*
const exprt & operator*() const
Definition: abstract_value_object.h:41
index_range_iteratort::index_range_iteratort
index_range_iteratort(index_range_iteratort &&rhs)
Definition: abstract_value_object.h:60
index_ranget::index_ranget
index_ranget(const index_ranget &)=delete
index_range_iteratort::range
index_range_implementation_ptrt range
Definition: abstract_value_object.h:77
index_range_iteratort::operator==
bool operator==(const index_range_iteratort &other) const
Definition: abstract_value_object.h:49
empty_value_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.h:225
index_ranget::range
index_range_implementation_ptrt range
Definition: abstract_value_object.h:105
index_ranget::~index_ranget
~index_ranget()=default
abstract_value_objectt::expression_transform
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
Interface for transforms.
Definition: abstract_value_object.cpp:170
abstract_value_objectt::index_range
index_ranget index_range(const namespacet &ns) const
Definition: abstract_value_object.h:259
index_range_implementationt::~index_range_implementationt
virtual ~index_range_implementationt()=default
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const typet &type, bool tp, bool bttm)
Definition: abstract_value_object.h:246
value_range_implementationt::~value_range_implementationt
virtual ~value_range_implementationt()=default
single_value_index_ranget::available
bool available
Definition: abstract_value_object.h:121
value_ranget::value_ranget
value_ranget(const value_ranget &)=delete
single_value_index_ranget::advance_to_next
bool advance_to_next() override
Definition: abstract_value_object.cpp:67
abstract_value_objectt::to_interval
virtual constant_interval_exprt to_interval() const =0
value_ranget::value_ranget
value_ranget(value_ranget &&rhs)
Definition: abstract_value_object.h:196
index_range_iteratort::index_range_iteratort
index_range_iteratort(index_range_implementation_ptrt &&r)
Definition: abstract_value_object.h:71
index_range_iteratort::operator!=
bool operator!=(const index_range_iteratort &other) const
Definition: abstract_value_object.h:55
value_range_implementationt::current
virtual const abstract_object_pointert & current() const =0
value_range_iteratort::range
value_range_implementation_ptrt range
Definition: abstract_value_object.h:182
r
static int8_t r
Definition: irep_hash.h:59
index_ranget::begin
index_range_iteratort begin() const
Definition: abstract_value_object.h:95
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
abstract_objectt
Definition: abstract_object.h:79
index_ranget::index_ranget
index_ranget(index_range_implementation_ptrt r)
Definition: abstract_value_object.h:86
abstract_value_objectt::abstract_value_objectt
abstract_value_objectt(const typet &type)
Definition: abstract_value_object.h:242
index_range_iteratort::index_range_iteratort
index_range_iteratort(const index_range_iteratort &)=delete
value_ranget
Definition: abstract_value_object.h:189
value_range_iteratort::~value_range_iteratort
~value_range_iteratort()=default
value_ranget::~value_ranget
~value_ranget()=default
value_ranget::begin
value_range_iteratort begin() const
Definition: abstract_value_object.h:202