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 \*******************************************************************/
12 
13 template <class context_classt>
16 {
18  new context_classt{abstract_object, abstract_object->type()});
19 }
20 
21 template <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 {
42  return create_context_abstract_object<data_dependency_contextt>(
43  abstract_object);
44 
45  if(configuration.context_tracking.last_write_context)
46  return create_context_abstract_object<write_location_contextt>(
47  abstract_object);
48 
49  return abstract_object;
50 }
51 
67 template <class abstract_object_classt>
69  const typet type,
70  bool top,
71  bool bottom,
72  const exprt &e,
73  const abstract_environmentt &environment,
74  const namespacet &ns,
75  const vsd_configt &configuration)
76 {
77  auto abstract_object = create_abstract_object<abstract_object_classt>(
78  type, top, bottom, e, environment, ns);
79 
80  return wrap_with_context_object(abstract_object, configuration);
81 }
82 
85  const typet &type) const
86 {
87  ABSTRACT_OBJECT_TYPET abstract_object_type = TWO_VALUE;
88 
89  if(
90  type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
91  type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool ||
92  type.id() == ID_integer || type.id() == ID_c_bit_field)
93  {
95  }
96  else if(type.id() == ID_floatbv)
97  {
99  return (float_type == INTERVAL) ? CONSTANT : float_type;
100  }
101  else if(type.id() == ID_array)
102  {
104  }
105  else if(type.id() == ID_pointer)
106  {
108  }
109  else if(type.id() == ID_struct)
110  {
112  }
113  else if(type.id() == ID_union)
114  {
116  }
117 
118  return abstract_object_type;
119 }
120 
123  const typet &type,
124  bool top,
125  bool bottom,
126  const exprt &e,
127  const abstract_environmentt &environment,
128  const namespacet &ns) const
129 {
130  const typet &followed_type = ns.follow(type);
131  ABSTRACT_OBJECT_TYPET abstract_object_type =
132  get_abstract_object_type(followed_type);
133 
134  switch(abstract_object_type)
135  {
136  case TWO_VALUE:
137  return initialize_abstract_object<abstract_objectt>(
138  followed_type, top, bottom, e, environment, ns, configuration);
139  case CONSTANT:
140  return initialize_abstract_object<constant_abstract_valuet>(
141  followed_type, top, bottom, e, environment, ns, configuration);
142  case INTERVAL:
143  return initialize_abstract_object<interval_abstract_valuet>(
144  followed_type, top, bottom, e, environment, ns, configuration);
145  case VALUE_SET:
147  {
148  return initialize_abstract_object<value_set_abstract_valuet>(
149  followed_type, top, bottom, e, environment, ns, configuration);
150  }
151  return initialize_abstract_object<value_set_abstract_objectt>(
152  followed_type, top, bottom, e, environment, ns, configuration);
153 
154  case ARRAY_INSENSITIVE:
155  return initialize_abstract_object<two_value_array_abstract_objectt>(
156  followed_type, top, bottom, e, environment, ns, configuration);
157  case ARRAY_SENSITIVE:
158  return initialize_abstract_object<full_array_abstract_objectt>(
159  followed_type, top, bottom, e, environment, ns, configuration);
160 
161  case POINTER_INSENSITIVE:
162  return initialize_abstract_object<two_value_pointer_abstract_objectt>(
163  followed_type, top, bottom, e, environment, ns, configuration);
164  case POINTER_SENSITIVE:
165  return initialize_abstract_object<constant_pointer_abstract_objectt>(
166  followed_type, top, bottom, e, environment, ns, configuration);
168  return initialize_abstract_object<value_set_pointer_abstract_objectt>(
169  followed_type, top, bottom, e, environment, ns, configuration);
170 
171  case STRUCT_INSENSITIVE:
172  return initialize_abstract_object<two_value_struct_abstract_objectt>(
173  followed_type, top, bottom, e, environment, ns, configuration);
174  case STRUCT_SENSITIVE:
175  return initialize_abstract_object<full_struct_abstract_objectt>(
176  followed_type, top, bottom, e, environment, ns, configuration);
177 
178  case UNION_INSENSITIVE:
179  return initialize_abstract_object<two_value_union_abstract_objectt>(
180  followed_type, top, bottom, e, environment, ns, configuration);
181 
182  default:
183  UNREACHABLE;
184  return initialize_abstract_object<abstract_objectt>(
185  followed_type, top, bottom, e, environment, ns, configuration);
186  }
187 }
188 
191  const abstract_object_pointert &abstract_object) const
192 {
193  return wrap_with_context_object(abstract_object, configuration);
194 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
VALUE_SET_OF_POINTERS
@ VALUE_SET_OF_POINTERS
Definition: variable_sensitivity_configuration.h:24
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
value_set_abstract_value.h
Value sets for primitives.
variable_sensitivity_object_factory.h
Tracks the user-supplied configuration for VSD and build the correct type of abstract object when nee...
vsd_configt::data_dependency_context
bool data_dependency_context
Definition: variable_sensitivity_configuration.h:52
wrap_with_context_object
abstract_object_pointert wrap_with_context_object(const abstract_object_pointert &abstract_object, const vsd_configt &configuration)
Definition: variable_sensitivity_object_factory.cpp:37
typet
The type of an expression, extends irept.
Definition: type.h:28
vsd_configt::pointer_abstract_type
ABSTRACT_OBJECT_TYPET pointer_abstract_type
Definition: variable_sensitivity_configuration.h:43
CONSTANT
@ CONSTANT
Definition: variable_sensitivity_configuration.h:20
vsd_configt::last_write_context
bool last_write_context
Definition: variable_sensitivity_configuration.h:53
variable_sensitivity_object_factoryt::wrap_with_context
abstract_object_pointert wrap_with_context(const abstract_object_pointert &abstract_object) const
Definition: variable_sensitivity_object_factory.cpp:190
abstract_environmentt
Definition: abstract_environment.h:36
ARRAY_INSENSITIVE
@ ARRAY_INSENSITIVE
Definition: variable_sensitivity_configuration.h:23
exprt
Base class for all expressions.
Definition: expr.h:54
vsd_configt::context_tracking
struct vsd_configt::@0 context_tracking
variable_sensitivity_object_factoryt::get_abstract_object_type
ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const
Decide which abstract object type to use for the variable in question.
Definition: variable_sensitivity_object_factory.cpp:84
vsd_configt
Definition: variable_sensitivity_configuration.h:41
vsd_configt::struct_abstract_type
ABSTRACT_OBJECT_TYPET struct_abstract_type
Definition: variable_sensitivity_configuration.h:44
UNION_INSENSITIVE
@ UNION_INSENSITIVE
Definition: variable_sensitivity_configuration.h:30
VALUE_SET
@ VALUE_SET
Definition: variable_sensitivity_configuration.h:31
INTERVAL
@ INTERVAL
Definition: variable_sensitivity_configuration.h:21
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
ARRAY_SENSITIVE
@ ARRAY_SENSITIVE
Definition: variable_sensitivity_configuration.h:22
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
vsd_configt::array_abstract_type
ABSTRACT_OBJECT_TYPET array_abstract_type
Definition: variable_sensitivity_configuration.h:45
TWO_VALUE
@ TWO_VALUE
Definition: variable_sensitivity_configuration.h:19
vsd_configt::new_value_set
bool new_value_set
Definition: variable_sensitivity_configuration.h:58
create_context_abstract_object
abstract_object_pointert create_context_abstract_object(const abstract_object_pointert &abstract_object)
Definition: variable_sensitivity_object_factory.cpp:15
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
vsd_configt::value_abstract_type
ABSTRACT_OBJECT_TYPET value_abstract_type
Definition: variable_sensitivity_configuration.h:42
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
vsd_configt::union_abstract_type
ABSTRACT_OBJECT_TYPET union_abstract_type
Definition: variable_sensitivity_configuration.h:46
irept::id
const irep_idt & id() const
Definition: irep.h:407
full_array_abstract_object.h
An abstraction of an array value.
POINTER_SENSITIVE
@ POINTER_SENSITIVE
Definition: variable_sensitivity_configuration.h:25
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
variable_sensitivity_object_factoryt::configuration
vsd_configt configuration
Definition: variable_sensitivity_object_factory.h:90
variable_sensitivity_object_factoryt::get_abstract_object
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.
Definition: variable_sensitivity_object_factory.cpp:122
POINTER_INSENSITIVE
@ POINTER_INSENSITIVE
Definition: variable_sensitivity_configuration.h:26
ABSTRACT_OBJECT_TYPET
ABSTRACT_OBJECT_TYPET
Definition: variable_sensitivity_configuration.h:18
STRUCT_SENSITIVE
@ STRUCT_SENSITIVE
Definition: variable_sensitivity_configuration.h:27
value_set_pointer_abstract_object.h
Value Set of Pointer Abstract Object.
vsd_configt::advanced_sensitivities
struct vsd_configt::@1 advanced_sensitivities
initialize_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...
Definition: variable_sensitivity_object_factory.cpp:68
create_abstract_object
abstract_object_pointert create_abstract_object(const typet type, bool top, bool bottom, const exprt &e, const abstract_environmentt &environment, const namespacet &ns)
Definition: variable_sensitivity_object_factory.cpp:22
STRUCT_INSENSITIVE
@ STRUCT_INSENSITIVE
Definition: variable_sensitivity_configuration.h:28