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 
18 
20 {
21 public:
23  : values(vals), cur(), next(values.begin())
24  {
26  }
27 
28  const exprt &current() const override
29  {
30  return cur;
31  }
32  bool advance_to_next() override
33  {
34  if(next == values.end())
35  return false;
36 
37  cur = (*next)->to_constant();
38  ++next;
39  return true;
40  }
41 
42 private:
46 };
47 
49 {
50  return std::make_shared<value_set_index_ranget>(vals);
51 }
52 
54  const exprt &expr,
55  const std::vector<abstract_object_pointert> &ops);
56 
57 std::vector<abstract_object_sett>
58 unwrap_operands(const std::vector<abstract_object_pointert> &operands);
59 
62 
68 
75 
81 template <typename Con, typename F>
83  const std::vector<Con> &super_con,
84  std::vector<typename Con::value_type> &sub_con,
85  F f)
86 {
87  size_t n = sub_con.size();
88  if(n == super_con.size())
89  f(sub_con);
90  else
91  {
92  for(const auto &value : super_con[n])
93  {
94  sub_con.push_back(value);
95  apply_comb(super_con, sub_con, f);
96  sub_con.pop_back();
97  }
98  }
99 }
100 
106 template <typename Con, typename F>
107 void for_each_comb(const std::vector<Con> &super_con, F f)
108 {
109  std::vector<typename Con::value_type> sub_con;
110  apply_comb(super_con, sub_con, f);
111 }
112 
114  : abstract_value_objectt(type)
115 {
116  values.insert(std::make_shared<constant_abstract_valuet>(type));
117  verify();
118 }
119 
121  const typet &type,
122  bool top,
123  bool bottom)
124  : abstract_value_objectt(type, top, bottom)
125 {
126  values.insert(std::make_shared<constant_abstract_valuet>(type, top, bottom));
127  verify();
128 }
129 
131  const exprt &expr,
132  const abstract_environmentt &environment,
133  const namespacet &ns)
134  : abstract_value_objectt(expr.type(), false, false)
135 {
136  values.insert(
137  std::make_shared<constant_abstract_valuet>(expr, environment, ns));
138  verify();
139 }
140 
143 {
144  if(values.empty())
146 
148 }
149 
151  const exprt &expr,
152  const std::vector<abstract_object_pointert> &operands,
153  const abstract_environmentt &environment,
154  const namespacet &ns) const
155 {
156  PRECONDITION(operands.size() == expr.operands().size());
157 
158  auto collective_operands = unwrap_operands(operands);
159 
160  if(expr.id() == ID_if)
161  return evaluate_conditional(
162  expr.type(), collective_operands, environment, ns);
163 
164  abstract_object_sett resulting_objects;
165 
166  auto dispatcher = values.first();
168  collective_operands,
169  [&resulting_objects, &dispatcher, &expr, &environment, &ns](
170  const std::vector<abstract_object_pointert> &ops) {
171  auto rewritten_expr = rewrite_expression(expr, ops);
172  resulting_objects.insert(
173  dispatcher->expression_transform(rewritten_expr, ops, environment, ns));
174  });
175 
176  return resolve_new_values(resulting_objects, environment);
177 }
178 
180  const typet &type,
181  const std::vector<abstract_object_sett> &operands,
182  const abstract_environmentt &env,
183  const namespacet &ns) const
184 {
185  auto const condition = operands[0];
186 
187  auto const true_result = operands[1];
188  auto const false_result = operands[2];
189 
190  auto all_true = true;
191  auto all_false = true;
192  for(auto v : condition)
193  {
194  auto expr = v->to_constant();
195  all_true = all_true && expr.is_true();
196  all_false = all_false && expr.is_false();
197  }
198  auto indeterminate = !all_true && !all_false;
199 
200  abstract_object_sett resulting_objects;
201  if(all_true || indeterminate)
202  resulting_objects.insert(true_result);
203  if(all_false || indeterminate)
204  resulting_objects.insert(false_result);
205  return resolve_new_values(resulting_objects, env);
206 }
207 
209  abstract_environmentt &environment,
210  const namespacet &ns,
211  const std::stack<exprt> &stack,
212  const exprt &specifier,
213  const abstract_object_pointert &value,
214  bool merging_write) const
215 {
216  abstract_object_sett new_values;
217  for(const auto &st_value : values)
218  {
219  new_values.insert(
220  st_value->write(environment, ns, stack, specifier, value, merging_write));
221  }
222  return resolve_new_values(new_values, environment);
223 }
224 
226  const abstract_object_sett &new_values,
227  const abstract_environmentt &environment) const
228 {
229  auto result = resolve_values(new_values);
230  return environment.add_object_context(result);
231 }
232 
234  const abstract_object_sett &new_values) const
235 {
236  PRECONDITION(!new_values.empty());
237 
238  if(new_values == values)
239  return shared_from_this();
240 
241  auto unwrapped_values = unwrap_and_extract_values(new_values);
242 
243  if(unwrapped_values.size() > max_value_set_size)
244  {
245  return to_interval(unwrapped_values);
246  }
247  //if(unwrapped_values.size() == 1)
248  //{
249  // return (*unwrapped_values.begin());
250  //}
251 
252  auto result =
253  std::dynamic_pointer_cast<value_set_abstract_objectt>(mutable_clone());
254  result->set_values(unwrapped_values);
255  return result;
256 }
257 
260 {
261  auto cast_other = std::dynamic_pointer_cast<const value_set_tag>(other);
262  if(cast_other)
263  {
264  auto union_values = values;
265  union_values.insert(cast_other->get_values());
266  return resolve_values(union_values);
267  }
268 
269  return abstract_objectt::merge(other);
270 }
271 
273  const abstract_object_sett &other_values) const
274 {
275  PRECONDITION(!other_values.empty());
276 
277  exprt lower_expr = (*other_values.begin())->to_constant();
278  exprt upper_expr = (*other_values.begin())->to_constant();
279  for(const auto &value : other_values)
280  {
281  const auto &value_expr = value->to_constant();
282  lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
283  upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
284  }
285  return std::make_shared<interval_abstract_valuet>(
286  constant_interval_exprt(lower_expr, upper_expr));
287 }
288 
290  const abstract_object_sett &other_values)
291 {
292  PRECONDITION(!other_values.empty());
293  set_not_top();
294  values = other_values;
295  verify();
296 }
297 
299  std::ostream &out,
300  const ai_baset &ai,
301  const namespacet &ns) const
302 {
303  if(is_top())
304  {
305  out << "TOP";
306  }
307  else if(is_bottom())
308  {
309  out << "BOTTOM";
310  }
311  else
312  {
313  out << "value-set-begin: ";
314 
315  values.output(out, ai, ns);
316 
317  out << " :value-set-end";
318  }
319 }
320 
322  const exprt &expr,
323  const std::vector<abstract_object_pointert> &ops)
324 {
325  auto operands_expr = exprt::operandst{};
326  for(auto v : ops)
327  operands_expr.push_back(v->to_constant());
328  auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr));
329  return rewritten_expr;
330 }
331 
332 std::vector<abstract_object_sett>
333 unwrap_operands(const std::vector<abstract_object_pointert> &operands)
334 {
335  auto unwrapped = std::vector<abstract_object_sett>{};
336 
337  for(const auto &op : operands)
338  {
339  auto vsab =
340  std::dynamic_pointer_cast<const value_set_tag>(maybe_unwrap_context(op));
341  INVARIANT(vsab, "should be a value set abstract object");
342  unwrapped.push_back(vsab->get_values());
343  }
344 
345  return unwrapped;
346 }
347 
350 {
351  abstract_object_sett unwrapped_values;
352  for(auto const &value : values)
353  {
354  unwrapped_values.insert(
356  }
357 
358  return unwrapped_values;
359 }
360 
363 {
364  auto const &value_as_set =
365  std::dynamic_pointer_cast<const value_set_tag>(maybe_singleton);
366  if(value_as_set)
367  {
368  PRECONDITION(value_as_set->get_values().size() == 1);
369  PRECONDITION(!std::dynamic_pointer_cast<const context_abstract_objectt>(
370  value_as_set->get_values().first()));
371 
372  return value_as_set->get_values().first();
373  }
374  else
375  return maybe_singleton;
376 }
377 
380 {
381  auto const &context_value =
382  std::dynamic_pointer_cast<const context_abstract_objectt>(maybe_wrapped);
383 
384  return context_value ? context_value->unwrap_context() : maybe_wrapped;
385 }
sharing_ptrt< class abstract_objectt > abstract_object_pointert
index_range_ptrt make_indeterminate_index_range()
std::shared_ptr< index_ranget > index_range_ptrt
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
const_iterator begin() const
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const
void insert(const abstract_object_pointert &o)
value_sett::const_iterator const_iterator
abstract_object_pointert first() const
const_iterator end() const
virtual bool is_top() const
Find out if the abstract object is top.
virtual bool verify() const
Verify the internal structure of an abstract_object is correct.
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.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
Represents an interval of values.
Definition: interval.h:56
static exprt get_max(const exprt &a, const exprt &b)
Definition: interval.cpp:959
static exprt get_min(const exprt &a, const exprt &b)
Definition: interval.cpp:964
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
const irep_idt & id() const
Definition: irep.h:407
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
index_range_ptrt index_range(const namespacet &ns) const override
void set_values(const abstract_object_sett &other_values)
Setter for updating the stored values.
abstract_object_pointert resolve_values(const abstract_object_sett &new_values) const
Update the set of stored values to new_values.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Merge two sets of constraints by appending to the first one.
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.
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 ...
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Interface for transforms.
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.
exprt to_constant() const override
Converts to a constant expression if possible.
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const
const exprt & current() const override
value_set_index_ranget(const abstract_object_sett &vals)
const abstract_object_sett & values
abstract_object_sett::const_iterator next
An abstraction of a single value that just stores a constant.
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...
An interval to represent a set of possible values.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
The base type of all abstract array representations.
void for_each_comb(const std::vector< Con > &super_con, F f)
Call the function f on every combination of elements in super_con.
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...
index_range_ptrt make_value_set_index_range(const abstract_object_sett &vals)
abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton)
Helper for converting singleton value sets into its only value.
abstract_object_sett unwrap_and_extract_values(const abstract_object_sett &values)
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.
std::vector< abstract_object_sett > unwrap_operands(const std::vector< abstract_object_pointert > &operands)
exprt rewrite_expression(const exprt &expr, const std::vector< abstract_object_pointert > &ops)
Value Set Abstract Object.