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\*******************************************************************/
10#include "liveness_context.h"
12
13template <class context_classt>
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
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{
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{
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
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);
141
143 {
144 case TWO_VALUE:
146 followed_type, top, bottom, e, environment, ns, configuration);
147 case CONSTANT:
149 followed_type, top, bottom, e, environment, ns, configuration);
150 case INTERVAL:
152 followed_type, top, bottom, e, environment, ns, configuration);
153 case VALUE_SET:
155 followed_type, top, bottom, e, environment, ns, configuration);
156
159 followed_type, top, bottom, e, environment, ns, configuration);
160 case ARRAY_SENSITIVE:
162 followed_type, top, bottom, e, environment, ns, configuration);
163
166 followed_type, top, bottom, e, environment, ns, configuration);
169 followed_type, top, bottom, e, environment, ns, configuration);
172 followed_type, top, bottom, e, environment, ns, configuration);
173
176 followed_type, top, bottom, e, environment, ns, configuration);
177 case STRUCT_SENSITIVE:
179 followed_type, top, bottom, e, environment, ns, configuration);
180
183 followed_type, top, bottom, e, environment, ns, configuration);
184
185 case HEAP_ALLOCATION:
186 {
189 ID_identifier, "heap-allocation-" + std::to_string(heap_allocations++));
191 auto heap_pointer =
192 get_abstract_object(e.type(), false, false, heap_symbol, environment, ns);
193 return heap_pointer;
194 }
195
196 default:
199 followed_type, top, bottom, e, environment, ns, configuration);
200 }
201}
202
sharing_ptrt< class abstract_objectt > abstract_object_pointert
floatbv_typet float_type()
Definition c_types.cpp:195
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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...