cprover
value_set_abstract_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: diffblue
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
13 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
14 
17 
19  public value_set_tag
20 {
21 public:
23  explicit value_set_abstract_objectt(const typet &type);
24 
26  value_set_abstract_objectt(const typet &type, bool top, bool bottom);
27 
29  const exprt &expr,
30  const abstract_environmentt &environment,
31  const namespacet &ns);
32 
33  index_range_ptrt index_range(const namespacet &ns) const override;
34 
36  exprt to_constant() const override
37  {
38  verify();
39  return values.size() == 1 ? (*values.begin())->to_constant()
41  }
42 
48  const exprt &expr,
49  const std::vector<abstract_object_pointert> &operands,
50  const abstract_environmentt &environment,
51  const namespacet &ns) const override;
52 
55  const abstract_object_sett &get_values() const override
56  {
57  return values;
58  }
59 
62  void set_values(const abstract_object_sett &other_values);
63 
66  static const size_t max_value_set_size = 10;
67 
72  abstract_environmentt &environment,
73  const namespacet &ns,
74  const std::stack<exprt> &stack,
75  const exprt &specifier,
76  const abstract_object_pointert &value,
77  bool merging_write) const override;
78 
79  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
80  const override;
81 
82 protected:
83  CLONE
84 
87 
88 private:
90  const typet &type,
91  const std::vector<abstract_object_sett> &operands,
92  const abstract_environmentt &env,
93  const namespacet &ns) const;
94 
102  const abstract_object_sett &new_values,
103  const abstract_environmentt &environment) const;
104 
111  resolve_values(const abstract_object_sett &new_values) const;
112 
113  // data
115 
120  to_interval(const abstract_object_sett &other_values) const;
121 };
122 
123 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H
value_set_abstract_objectt::values
abstract_object_sett values
Definition: value_set_abstract_object.h:114
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:259
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_object_sett::begin
const_iterator begin() const
Definition: abstract_object_set.h:47
value_set_tag
Definition: abstract_object_set.h:78
typet
The type of an expression, extends irept.
Definition: type.h:28
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_abstract_objectt::index_range
index_range_ptrt index_range(const namespacet &ns) const override
Definition: value_set_abstract_object.cpp:142
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
CLONE
#define CLONE
Definition: abstract_object.h:47
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:208
index_range_ptrt
std::shared_ptr< index_ranget > index_range_ptrt
Definition: abstract_value_object.h:43
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:66
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_object_sett::size
value_sett::size_type size() const
Definition: abstract_object_set.h:56
value_set_abstract_objectt
Definition: value_set_abstract_object.h:20
abstract_value_objectt
Definition: abstract_value_object.h:50
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:225
abstract_object_set.h
an unordered set of value objects
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:298
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
value_set_abstract_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 override
Interface for transforms.
Definition: value_set_abstract_object.cpp:150
value_set_abstract_objectt::get_values
const abstract_object_sett & get_values() const override
Getter for the set of stored abstract objects.
Definition: value_set_abstract_object.h:55
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
value_set_abstract_objectt::to_interval
abstract_object_pointert to_interval(const abstract_object_sett &other_values) const
Cast the set of values other_values to an interval.
Definition: value_set_abstract_object.cpp:272
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:289
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_set_abstract_objectt
value_set_abstract_objectt(const typet &type)
Definition: value_set_abstract_object.cpp:113
value_set_abstract_objectt::evaluate_conditional
abstract_object_pointert evaluate_conditional(const typet &type, const std::vector< abstract_object_sett > &operands, const abstract_environmentt &env, const namespacet &ns) const
Definition: value_set_abstract_object.cpp:179
abstract_objectt::top
bool top
Definition: abstract_object.h:363
value_set_abstract_objectt::to_constant
exprt to_constant() const override
Converts to a constant expression if possible.
Definition: value_set_abstract_object.h:36
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:233
abstract_value_object.h
Common behaviour for abstract objects modelling values - constants, intervals, etc.