cprover
value_set_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: diffblue
6 
7 \*******************************************************************/
8 
11 
17 #include <util/make_unique.h>
18 
20 make_value_set_index_range(const std::set<exprt> &vals);
21 
23 {
24 public:
25  explicit value_set_index_ranget(const std::set<exprt> &vals)
26  : values(vals), cur(), next(values.begin())
27  {
28  PRECONDITION(!values.empty());
29  }
30 
31  const exprt &current() const override
32  {
33  return cur;
34  }
35  bool advance_to_next() override
36  {
37  if(next == values.end())
38  return false;
39 
40  cur = *next;
41  ++next;
42  return true;
43  }
45  {
47  }
48 
49 private:
50  std::set<exprt> values;
52  std::set<exprt>::const_iterator next;
53 };
54 
56 make_value_set_index_range(const std::set<exprt> &vals)
57 {
58  return util_make_unique<value_set_index_ranget>(vals);
59 }
60 
63 
65 {
66 public:
68  : values(vals), cur(), next(values.begin())
69  {
71  }
72 
73  const abstract_object_pointert &current() const override
74  {
75  return cur;
76  }
77  bool advance_to_next() override
78  {
79  if(next == values.end())
80  return false;
81 
82  cur = *next;
83  ++next;
84  return true;
85  }
87  {
89  }
90 
91 private:
95 };
96 
99 {
100  return util_make_unique<value_set_value_ranget>(vals);
101 }
102 
105 
111 
112 static bool are_any_top(const abstract_object_sett &set);
113 
115  : abstract_value_objectt(type)
116 {
117  values.insert(std::make_shared<constant_abstract_valuet>(type));
118  verify();
119 }
120 
122  const typet &type,
123  bool top,
124  bool bottom)
125  : abstract_value_objectt(type, top, bottom)
126 {
127  values.insert(std::make_shared<constant_abstract_valuet>(type, top, bottom));
128  verify();
129 }
130 
132  const exprt &expr,
133  const abstract_environmentt &environment,
134  const namespacet &ns)
135  : abstract_value_objectt(expr.type(), false, false)
136 {
137  values.insert(
138  std::make_shared<constant_abstract_valuet>(expr, environment, ns));
139  verify();
140 }
141 
144  const namespacet &ns) const
145 {
146  if(values.empty())
148 
149  std::set<exprt> flattened;
150  for(const auto &o : values)
151  {
152  const auto &v = std::dynamic_pointer_cast<const abstract_value_objectt>(o);
153  for(auto e : v->index_range(ns))
154  flattened.insert(e);
155  }
156 
157  return make_value_set_index_range(flattened);
158 }
159 
162 {
164 }
165 
167 {
168  verify();
169 
170  if(values.size() == 1)
171  return values.first()->to_constant();
172 
173  auto interval = to_interval();
174  if(interval.is_single_value_interval())
175  return interval.get_lower();
176 
178 }
179 
181 {
182  return values.to_interval();
183 }
184 
186  abstract_environmentt &environment,
187  const namespacet &ns,
188  const std::stack<exprt> &stack,
189  const exprt &specifier,
190  const abstract_object_pointert &value,
191  bool merging_write) const
192 {
193  abstract_object_sett new_values;
194  for(const auto &st_value : values)
195  {
196  new_values.insert(
197  st_value->write(environment, ns, stack, specifier, value, merging_write));
198  }
199  return resolve_new_values(new_values, environment);
200 }
201 
203  const abstract_object_sett &new_values,
204  const abstract_environmentt &environment) const
205 {
206  auto result = resolve_values(new_values);
207  return environment.add_object_context(result);
208 }
209 
211  const abstract_object_sett &new_values) const
212 {
213  PRECONDITION(!new_values.empty());
214 
215  if(new_values == values)
216  return shared_from_this();
217 
218  auto unwrapped_values = unwrap_and_extract_values(new_values);
219 
220  if(unwrapped_values.size() > max_value_set_size)
221  {
222  return std::make_shared<interval_abstract_valuet>(
223  unwrapped_values.to_interval());
224  }
225  //if(unwrapped_values.size() == 1)
226  //{
227  // return (*unwrapped_values.begin());
228  //}
229 
230  auto result =
231  std::dynamic_pointer_cast<value_set_abstract_objectt>(mutable_clone());
232  result->set_values(unwrapped_values);
233  return result;
234 }
235 
238 {
239  auto union_values = !is_bottom() ? values : abstract_object_sett{};
240 
241  auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
242  if(other_value_set)
243  {
244  union_values.insert(other_value_set->get_values());
245  return resolve_values(union_values);
246  }
247 
248  auto other_value =
249  std::dynamic_pointer_cast<const abstract_value_objectt>(other);
250  if(other_value)
251  {
252  union_values.insert(other_value);
253  return resolve_values(union_values);
254  }
255 
256  return abstract_objectt::merge(other);
257 }
258 
260 {
261  values.clear();
262  values.insert(std::make_shared<constant_abstract_valuet>(type()));
263 }
264 
266  const abstract_object_sett &other_values)
267 {
268  PRECONDITION(!other_values.empty());
269  if(are_any_top(other_values))
270  {
271  set_top();
272  }
273  else
274  {
275  set_not_top();
276  values = other_values;
277  }
278  set_not_bottom();
279  verify();
280 }
281 
283  std::ostream &out,
284  const ai_baset &ai,
285  const namespacet &ns) const
286 {
287  if(is_top())
288  {
289  out << "TOP";
290  }
291  else if(is_bottom())
292  {
293  out << "BOTTOM";
294  }
295  else
296  {
297  out << "value-set-begin: ";
298 
299  values.output(out, ai, ns);
300 
301  out << " :value-set-end";
302  }
303 }
304 
307 {
308  auto const &context_value =
309  std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
310 
311  return context_value ? context_value->unwrap_context() : maybe_wrapped;
312 }
313 
316 {
317  abstract_object_sett unwrapped_values;
318  for(auto const &value : values)
319  {
320  unwrapped_values.insert(
322  }
323 
324  return unwrapped_values;
325 }
326 
329 {
330  auto const &value_as_set =
331  std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
332  if(value_as_set)
333  {
334  PRECONDITION(value_as_set->get_values().size() == 1);
335  PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
336  value_as_set->get_values().first()));
337 
338  return value_as_set->get_values().first();
339  }
340  else
341  return maybe_singleton;
342 }
343 
344 static bool are_any_top(const abstract_object_sett &set)
345 {
346  return std::find_if(
347  set.begin(), set.end(), [](const abstract_object_pointert &value) {
348  return value->is_top();
349  }) != set.end();
350 }
abstract_object_sett::clear
void clear()
Definition: abstract_object_set.h:75
are_any_top
static bool are_any_top(const abstract_object_sett &set)
Definition: value_set_abstract_object.cpp:344
value_set_abstract_objectt::values
abstract_object_sett values
Definition: value_set_abstract_object.h:97
value_set_abstract_objectt::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
Definition: value_set_abstract_object.cpp:237
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
index_range_implementationt
Definition: abstract_value_object.h:28
abstract_objectt::merge
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
Definition: abstract_object.cpp:189
abstract_object_sett::begin
const_iterator begin() const
Definition: abstract_object_set.h:52
unwrap_and_extract_values
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Definition: value_set_abstract_object.cpp:315
typet
The type of an expression, extends irept.
Definition: type.h:28
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
value_set_index_ranget::next
std::set< exprt >::const_iterator next
Definition: value_set_abstract_object.cpp:52
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
abstract_object_sett
Definition: abstract_object_set.h:19
value_set_value_ranget::reset
value_range_implementation_ptrt reset() const override
Definition: value_set_abstract_object.cpp:86
abstract_object_sett::empty
bool empty() const
Definition: abstract_object_set.h:65
abstract_objectt::set_top
void set_top()
Definition: abstract_object.h:449
abstract_object_sett::end
const_iterator end() const
Definition: abstract_object_set.h:56
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
abstract_object_sett::const_iterator
value_sett::const_iterator const_iterator
Definition: abstract_object_set.h:25
value_set_abstract_objectt::to_interval
constant_interval_exprt to_interval() const override
Definition: value_set_abstract_object.cpp:180
value_set_abstract_objectt::write
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
Definition: value_set_abstract_object.cpp:185
value_set_value_ranget::advance_to_next
bool advance_to_next() override
Definition: value_set_abstract_object.cpp:77
value_set_index_ranget::advance_to_next
bool advance_to_next() override
Definition: value_set_abstract_object.cpp:35
value_set_value_ranget::next
abstract_object_sett::const_iterator next
Definition: value_set_abstract_object.cpp:94
constant_interval_exprt
Represents an interval of values.
Definition: interval.h:56
value_set_abstract_objectt::max_value_set_size
static const size_t max_value_set_size
The threshold size for value-sets: past this threshold the object is either converted to interval or ...
Definition: value_set_abstract_object.h:55
value_range_implementation_ptrt
std::unique_ptr< value_range_implementationt > value_range_implementation_ptrt
Definition: abstract_value_object.h:130
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
maybe_extract_single_value
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
Definition: value_set_abstract_object.cpp:328
make_value_set_value_range
static value_range_implementation_ptrt make_value_set_value_range(const abstract_object_sett &vals)
Definition: value_set_abstract_object.cpp:98
make_unique.h
value_set_value_ranget::current
const abstract_object_pointert & current() const override
Definition: value_set_abstract_object.cpp:73
abstract_object_sett::size
value_sett::size_type size() const
Definition: abstract_object_set.h:61
abstract_value_objectt
Definition: abstract_value_object.h:240
value_set_abstract_object.h
Value Set Abstract Object.
value_set_abstract_objectt::resolve_new_values
abstract_object_pointert resolve_new_values(const abstract_object_sett &new_values, const abstract_environmentt &environment) const
Update the set of stored values to new_values.
Definition: value_set_abstract_object.cpp:202
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
value_range_implementationt
Definition: abstract_value_object.h:133
value_set_index_ranget::current
const exprt & current() const override
Definition: value_set_abstract_object.cpp:31
value_set_abstract_objectt::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Definition: value_set_abstract_object.cpp:282
abstract_object_sett::insert
void insert(const abstract_object_pointert &o)
Definition: abstract_object_set.h:29
value_set_abstract_objectt::index_range_implementation
index_range_implementation_ptrt index_range_implementation(const namespacet &ns) const override
Definition: value_set_abstract_object.cpp:143
abstract_object_sett::first
abstract_object_pointert first() const
Definition: abstract_object_set.h:47
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
make_value_set_index_range
static index_range_implementation_ptrt make_value_set_index_range(const std::set< exprt > &vals)
Definition: value_set_abstract_object.cpp:56
value_set_index_ranget::reset
index_range_implementation_ptrt reset() const override
Definition: value_set_abstract_object.cpp:44
value_set_index_ranget
Definition: value_set_abstract_object.cpp:23
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
value_set_value_ranget::values
const abstract_object_sett & values
Definition: value_set_abstract_object.cpp:92
value_set_index_ranget::value_set_index_ranget
value_set_index_ranget(const std::set< exprt > &vals)
Definition: value_set_abstract_object.cpp:25
value_set_value_ranget::value_set_value_ranget
value_set_value_ranget(const abstract_object_sett &vals)
Definition: value_set_abstract_object.cpp:67
abstract_environmentt::add_object_context
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
Definition: abstract_environment.cpp:282
value_set_index_ranget::values
std::set< exprt > values
Definition: value_set_abstract_object.cpp:50
interval_abstract_value.h
An interval to represent a set of possible values.
abstract_objectt::set_not_bottom
void set_not_bottom()
Definition: abstract_object.h:459
two_value_array_abstract_object.h
The base type of all abstract array representations.
value_set_abstract_objectt::set_values
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
Definition: value_set_abstract_object.cpp:265
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_objectt::verify
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
Definition: abstract_object.cpp:160
value_set_abstract_objectt::value_range_implementation
value_range_implementation_ptrt value_range_implementation() const override
Definition: value_set_abstract_object.cpp:161
value_set_value_ranget
Definition: value_set_abstract_object.cpp:65
value_set_abstract_objectt::value_set_abstract_objectt
value_set_abstract_objectt(const typet &type)
Definition: value_set_abstract_object.cpp:114
abstract_objectt::set_not_top
void set_not_top()
Definition: abstract_object.h:454
maybe_unwrap_context
static abstract_object_pointert maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped)
Definition: value_set_abstract_object.cpp:306
abstract_object_sett::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
Definition: abstract_object_set.cpp:23
value_set_index_ranget::cur
exprt cur
Definition: value_set_abstract_object.cpp:51
value_set_abstract_objectt::set_top_internal
void set_top_internal() override
Definition: value_set_abstract_object.cpp:259
abstract_objectt::top
bool top
Definition: abstract_object.h:363
index_range_implementation_ptrt
std::unique_ptr< index_range_implementationt > index_range_implementation_ptrt
Definition: abstract_value_object.h:25
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
value_set_abstract_objectt::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: value_set_abstract_object.cpp:166
value_set_value_ranget::cur
abstract_object_pointert cur
Definition: value_set_abstract_object.cpp:93
value_set_abstract_objectt::resolve_values
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
Definition: value_set_abstract_object.cpp:210
abstract_object_sett::to_interval
constant_interval_exprt to_interval() const
Calculate the set of values as an interval.
Definition: abstract_object_set.cpp:40
make_indeterminate_index_range
index_range_implementation_ptrt make_indeterminate_index_range()
Definition: abstract_value_object.cpp:79
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:404
constant_abstract_value.h
An abstraction of a single value that just stores a constant.