cprover
Loading...
Searching...
No Matches
variable_sensitivity_object_factory.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Owen Jones, owen.jones@diffblue.com
6
7\*******************************************************************/
8
10
11#include <util/namespace.h>
12
19#include "liveness_context.h"
26
27template <class context_classt>
34
35template <class abstract_object_classt>
37 const typet type,
38 bool top,
39 bool bottom,
40 const exprt &e,
41 const abstract_environmentt &environment,
42 const namespacet &ns)
43{
44 if(top || bottom)
45 return std::make_shared<abstract_object_classt>(type, top, bottom);
46
47 PRECONDITION(type == ns.follow(e.type()));
48 return std::make_shared<abstract_object_classt>(e, environment, ns);
49}
50
68
85template <class abstract_object_classt>
87 const typet type,
88 bool top,
89 bool bottom,
90 const exprt &e,
91 const abstract_environmentt &environment,
92 const namespacet &ns,
93 const vsd_configt &configuration)
94{
96 type, top, bottom, e, environment, ns);
97
98 return wrap_with_context_object(abstract_object, configuration);
99}
100
103 const typet &type) const
104{
106
107 if(
108 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
109 type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool ||
110 type.id() == ID_integer || type.id() == ID_c_bit_field)
111 {
113 }
114 else if(type.id() == ID_floatbv)
115 {
117 return (float_type == INTERVAL) ? CONSTANT : float_type;
118 }
119 else if(type.id() == ID_array)
120 {
122 }
123 else if(type.id() == ID_pointer)
124 {
126 }
127 else if(type.id() == ID_struct)
128 {
130 }
131 else if(type.id() == ID_union)
132 {
134 }
135 else if(type.id() == ID_dynamic_object)
136 {
137 return HEAP_ALLOCATION;
138 }
139
141}
142
145 const typet &type,
146 bool top,
147 bool bottom,
148 const exprt &e,
149 const abstract_environmentt &environment,
150 const namespacet &ns) const
151{
152 const typet &followed_type = ns.follow(type);
155
157 {
158 case TWO_VALUE:
160 followed_type, top, bottom, e, environment, ns, configuration);
161 case CONSTANT:
163 followed_type, top, bottom, e, environment, ns, configuration);
164 case INTERVAL:
166 followed_type, top, bottom, e, environment, ns, configuration);
167 case VALUE_SET:
169 followed_type, top, bottom, e, environment, ns, configuration);
170
173 followed_type, top, bottom, e, environment, ns, configuration);
174 case ARRAY_SENSITIVE:
176 followed_type, top, bottom, e, environment, ns, configuration);
177
180 followed_type, top, bottom, e, environment, ns, configuration);
183 followed_type, top, bottom, e, environment, ns, configuration);
186 followed_type, top, bottom, e, environment, ns, configuration);
187
190 followed_type, top, bottom, e, environment, ns, configuration);
191 case STRUCT_SENSITIVE:
193 followed_type, top, bottom, e, environment, ns, configuration);
194
197 followed_type, top, bottom, e, environment, ns, configuration);
198
199 case HEAP_ALLOCATION:
200 {
202 dynamic_object.set(
203 ID_identifier, "heap-allocation-" + std::to_string(heap_allocations++));
205 auto heap_pointer =
206 get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
207 return heap_pointer;
208 }
209
210 default:
213 followed_type, top, bottom, e, environment, ns, configuration);
214 }
215}
216
sharing_ptrt< class abstract_objectt > abstract_object_pointert
floatbv_typet float_type()
Definition c_types.cpp:182
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
abstract_object_pointert get_abstract_object(const typet &type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const
Get the appropriate abstract object for the variable under consideration.
abstract_object_pointert wrap_with_context(const abstract_object_pointert &abstract_object) const
ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const
Decide which abstract object type to use for the variable in question.
An abstraction of a single value that just stores a constant.
An abstraction of a pointer that tracks a single pointer.
Maintain data dependencies as a context in the variable sensitivity domain.
An abstraction of an array value.
An abstraction of a structure that stores one abstract object per field.
An interval to represent a set of possible values.
Maintain a context in the variable sensitvity domain that records the liveness region for a given abs...
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
ABSTRACT_OBJECT_TYPET union_abstract_type
struct vsd_configt::@0 context_tracking
ABSTRACT_OBJECT_TYPET pointer_abstract_type
ABSTRACT_OBJECT_TYPET struct_abstract_type
ABSTRACT_OBJECT_TYPET array_abstract_type
ABSTRACT_OBJECT_TYPET value_abstract_type
The base type of all abstract array representations.
The base of all structure abstractions.
The base of all union abstractions.
Value Set Abstract Object.
Value Set of Pointer Abstract Object.
abstract_object_pointert create_context_abstract_object(const abstract_object_pointert &abstract_object)
abstract_object_pointert initialize_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns, const vsd_configt &configuration)
Function: variable_sensitivity_object_factoryt::initialize_abstract_object Initialize the abstract ob...
abstract_object_pointert create_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert wrap_with_context_object(const abstract_object_pointert &abstract_object, const vsd_configt &configuration)
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...