cprover
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\*******************************************************************/
10#include "liveness_context.h"
12
13template <class context_classt>
16{
18 new context_classt{abstract_object, abstract_object->type()});
19}
20
21template <class abstract_object_classt>
23 const typet type,
24 bool top,
25 bool bottom,
26 const exprt &e,
27 const abstract_environmentt &environment,
28 const namespacet &ns)
29{
30 if(top || bottom)
31 return std::make_shared<abstract_object_classt>(type, top, bottom);
32
33 PRECONDITION(type == ns.follow(e.type()));
34 return std::make_shared<abstract_object_classt>(e, environment, ns);
35}
36
38 const abstract_object_pointert &abstract_object,
39 const vsd_configt &configuration)
40{
41 if(configuration.context_tracking.liveness)
42 return create_context_abstract_object<liveness_contextt>(abstract_object);
43
45 return create_context_abstract_object<data_dependency_contextt>(
46 abstract_object);
47
48 if(configuration.context_tracking.last_write_context)
49 return create_context_abstract_object<write_location_contextt>(
50 abstract_object);
51
52 return abstract_object;
53}
54
71template <class abstract_object_classt>
73 const typet type,
74 bool top,
75 bool bottom,
76 const exprt &e,
77 const abstract_environmentt &environment,
78 const namespacet &ns,
79 const vsd_configt &configuration)
80{
81 auto abstract_object = create_abstract_object<abstract_object_classt>(
82 type, top, bottom, e, environment, ns);
83
84 return wrap_with_context_object(abstract_object, configuration);
85}
86
89 const typet &type) const
90{
91 ABSTRACT_OBJECT_TYPET abstract_object_type = TWO_VALUE;
92
93 if(
94 type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
95 type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool ||
96 type.id() == ID_integer || type.id() == ID_c_bit_field)
97 {
99 }
100 else if(type.id() == ID_floatbv)
101 {
103 return (float_type == INTERVAL) ? CONSTANT : float_type;
104 }
105 else if(type.id() == ID_array)
106 {
108 }
109 else if(type.id() == ID_pointer)
110 {
112 }
113 else if(type.id() == ID_struct)
114 {
116 }
117 else if(type.id() == ID_union)
118 {
120 }
121 else if(type.id() == ID_dynamic_object)
122 {
123 return HEAP_ALLOCATION;
124 }
125
126 return abstract_object_type;
127}
128
131 const typet &type,
132 bool top,
133 bool bottom,
134 const exprt &e,
135 const abstract_environmentt &environment,
136 const namespacet &ns) const
137{
138 const typet &followed_type = ns.follow(type);
139 ABSTRACT_OBJECT_TYPET abstract_object_type =
140 get_abstract_object_type(followed_type);
141
142 switch(abstract_object_type)
143 {
144 case TWO_VALUE:
145 return initialize_abstract_object<abstract_objectt>(
146 followed_type, top, bottom, e, environment, ns, configuration);
147 case CONSTANT:
148 return initialize_abstract_object<constant_abstract_valuet>(
149 followed_type, top, bottom, e, environment, ns, configuration);
150 case INTERVAL:
151 return initialize_abstract_object<interval_abstract_valuet>(
152 followed_type, top, bottom, e, environment, ns, configuration);
153 case VALUE_SET:
154 return initialize_abstract_object<value_set_abstract_objectt>(
155 followed_type, top, bottom, e, environment, ns, configuration);
156
158 return initialize_abstract_object<two_value_array_abstract_objectt>(
159 followed_type, top, bottom, e, environment, ns, configuration);
160 case ARRAY_SENSITIVE:
161 return initialize_abstract_object<full_array_abstract_objectt>(
162 followed_type, top, bottom, e, environment, ns, configuration);
163
165 return initialize_abstract_object<two_value_pointer_abstract_objectt>(
166 followed_type, top, bottom, e, environment, ns, configuration);
168 return initialize_abstract_object<constant_pointer_abstract_objectt>(
169 followed_type, top, bottom, e, environment, ns, configuration);
171 return initialize_abstract_object<value_set_pointer_abstract_objectt>(
172 followed_type, top, bottom, e, environment, ns, configuration);
173
175 return initialize_abstract_object<two_value_struct_abstract_objectt>(
176 followed_type, top, bottom, e, environment, ns, configuration);
177 case STRUCT_SENSITIVE:
178 return initialize_abstract_object<full_struct_abstract_objectt>(
179 followed_type, top, bottom, e, environment, ns, configuration);
180
182 return initialize_abstract_object<two_value_union_abstract_objectt>(
183 followed_type, top, bottom, e, environment, ns, configuration);
184
185 case HEAP_ALLOCATION:
186 {
187 auto dynamic_object = exprt(ID_dynamic_object);
189 ID_identifier, "heap-allocation-" + std::to_string(heap_allocations++));
190 auto heap_symbol = unary_exprt(ID_address_of, dynamic_object, e.type());
191 auto heap_pointer =
192 get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
193 return heap_pointer;
194 }
195
196 default:
198 return initialize_abstract_object<abstract_objectt>(
199 followed_type, top, bottom, e, environment, ns, configuration);
200 }
201}
202
205 const abstract_object_pointert &abstract_object) const
206{
207 return wrap_with_context_object(abstract_object, configuration);
208}
sharing_ptrt< class abstract_objectt > abstract_object_pointert
floatbv_typet float_type()
Definition: c_types.cpp:195
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
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:281
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 an array value.
Maintain a context in the variable sensitvity domain that records the liveness region for a given abs...
exprt dynamic_object(const exprt &pointer)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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
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...