cprover
value_set_pointer_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
11 
16 
19 
25 
32 
38 template <typename Con, typename F>
40  const std::vector<Con> &super_con,
41  std::vector<typename Con::value_type> &sub_con,
42  F f)
43 {
44  size_t n = sub_con.size();
45  if(n == super_con.size())
46  f(sub_con);
47  else
48  {
49  for(const auto &value : super_con[n])
50  {
51  sub_con.push_back(value);
52  apply_comb(super_con, sub_con, f);
53  sub_con.pop_back();
54  }
55  }
56 }
57 
63 template <typename Con, typename F>
64 void for_each_comb(const std::vector<Con> &super_con, F f)
65 {
66  std::vector<typename Con::value_type> sub_con;
67  apply_comb(super_con, sub_con, f);
68 }
69 
71  const typet &type)
73 {
74  values.insert(std::make_shared<constant_pointer_abstract_objectt>(type));
75 }
76 
78  const typet &type,
79  bool top,
80  bool bottom)
81  : abstract_pointer_objectt(type, top, bottom)
82 {
83  values.insert(
84  std::make_shared<constant_pointer_abstract_objectt>(type, top, bottom));
85 }
86 
88  const exprt &expr,
89  const abstract_environmentt &environment,
90  const namespacet &ns)
91  : abstract_pointer_objectt(expr.type(), false, false)
92 {
93  values.insert(
94  std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
95 }
96 
98  const abstract_environmentt &env,
99  const namespacet &ns) const
100 {
101  if(is_top() || is_bottom())
102  {
103  return env.abstract_object_factory(
104  type().subtype(), ns, is_top(), !is_top());
105  }
106 
107  abstract_object_sett results;
108  for(auto value : values)
109  {
110  auto pointer =
111  std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
112  results.insert(pointer->read_dereference(env, ns));
113  }
114 
115  return results.first();
116 }
117 
119  abstract_environmentt &environment,
120  const namespacet &ns,
121  const std::stack<exprt> &stack,
122  const abstract_object_pointert &new_value,
123  bool merging_write) const
124 {
125  if(is_top() || is_bottom())
126  {
128  environment, ns, stack, new_value, merging_write);
129  }
130 
131  for(auto value : values)
132  {
133  auto pointer =
134  std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
135  pointer->write_dereference(
136  environment, ns, stack, new_value, merging_write);
137  }
138 
139  return shared_from_this();
140 }
141 
143  const abstract_object_sett &new_values,
144  const abstract_environmentt &environment) const
145 {
146  auto result = resolve_values(new_values);
147  return environment.add_object_context(result);
148 }
149 
151  const abstract_object_sett &new_values) const
152 {
153  PRECONDITION(!new_values.empty());
154 
155  if(new_values == values)
156  return shared_from_this();
157 
158  auto unwrapped_values = unwrap_and_extract_values(new_values);
159 
160  auto result = std::dynamic_pointer_cast<value_set_pointer_abstract_objectt>(
161  mutable_clone());
162 
163  if(unwrapped_values.size() > max_value_set_size)
164  {
165  result->set_top();
166  }
167  else
168  {
169  result->set_values(unwrapped_values);
170  }
171  return result;
172 }
173 
176 {
177  auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
178  if(cast_other)
179  {
180  auto union_values = values;
181  union_values.insert(cast_other->get_values());
182  return resolve_values(union_values);
183  }
184 
185  return abstract_objectt::merge(other);
186 }
187 
189  const abstract_object_sett &other_values)
190 {
191  PRECONDITION(!other_values.empty());
192  set_not_top();
193  values = other_values;
194 }
195 
197  std::ostream &out,
198  const ai_baset &ai,
199  const namespacet &ns) const
200 {
201  if(is_top())
202  {
203  out << "TOP";
204  }
205  else if(is_bottom())
206  {
207  out << "BOTTOM";
208  }
209  else
210  {
211  out << "value-set-begin: ";
212 
213  values.output(out, ai, ns);
214 
215  out << " :value-set-end";
216  }
217 }
218 
221 {
222  abstract_object_sett unwrapped_values;
223  for(auto const &value : values)
224  {
225  unwrapped_values.insert(
227  }
228 
229  return unwrapped_values;
230 }
231 
234 {
235  auto const &value_as_set =
236  std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
237  if(value_as_set)
238  {
239  PRECONDITION(value_as_set->get_values().size() == 1);
240  PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
241  value_as_set->get_values().first()));
242 
243  return value_as_set->get_values().first();
244  }
245  else
246  return maybe_singleton;
247 }
248 
251 {
252  auto const &context_value =
253  std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
254 
255  return context_value ? context_value->unwrap_context() : maybe_wrapped;
256 }
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void insert(const abstract_object_pointert &o)
abstract_object_pointert first() const
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 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.
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
virtual abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const
Evaluate writing to a pointer's value.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
Base class for all expressions.
Definition: expr.h:54
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The type of an expression, extends irept.
Definition: type.h:28
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
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 ...
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
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.
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
Evaluate reading the pointer's value.
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &new_value, bool merging_write) const override
Evaluate writing to a pointer's value.
An abstraction of a pointer that tracks a single pointer.
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
void for_each_comb(const std::vector< Con > &super_con, F f)
Call the function f on every combination of elements in super_con.
void apply_comb(const std::vector< Con > &super_con, std::vector< typename Con::value_type > &sub_con, F f)
Recursively construct a combination sub_con from super_con and once constructed call f.
static abstract_object_pointert maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped)
Helper for converting context objects into its abstract-value children maybe_wrapped: either an abstr...
static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
static abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
Value Set of Pointer Abstract Object.