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 
68 template <class abstract_object_classt>
70  const typet type,
71  bool top,
72  bool bottom,
73  const exprt &e,
74  const abstract_environmentt &environment,
75  const namespacet &ns,
76  const vsd_configt &configuration)
77 {
78  auto abstract_object = create_abstract_object<abstract_object_classt>(
79  type, top, bottom, e, environment, ns);
80 
81  return wrap_with_context_object(abstract_object, configuration);
82 }
83 
86  const typet &type) const
87 {
88  ABSTRACT_OBJECT_TYPET abstract_object_type = TWO_VALUE;
89 
90  if(
91  type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
92  type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool ||
93  type.id() == ID_integer || type.id() == ID_c_bit_field)
94  {
96  }
97  else if(type.id() == ID_floatbv)
98  {
100  return (float_type == INTERVAL) ? CONSTANT : float_type;
101  }
102  else if(type.id() == ID_array)
103  {
105  }
106  else if(type.id() == ID_pointer)
107  {
109  }
110  else if(type.id() == ID_struct)
111  {
113  }
114  else if(type.id() == ID_union)
115  {
117  }
118 
119  return abstract_object_type;
120 }
121 
124  const typet &type,
125  bool top,
126  bool bottom,
127  const exprt &e,
128  const abstract_environmentt &environment,
129  const namespacet &ns) const
130 {
131  const typet &followed_type = ns.follow(type);
132  ABSTRACT_OBJECT_TYPET abstract_object_type =
133  get_abstract_object_type(followed_type);
134 
135  switch(abstract_object_type)
136  {
137  case TWO_VALUE:
138  return initialize_abstract_object<abstract_objectt>(
139  followed_type, top, bottom, e, environment, ns, configuration);
140  case CONSTANT:
141  return initialize_abstract_object<constant_abstract_valuet>(
142  followed_type, top, bottom, e, environment, ns, configuration);
143  case INTERVAL:
144  return initialize_abstract_object<interval_abstract_valuet>(
145  followed_type, top, bottom, e, environment, ns, configuration);
146  case VALUE_SET:
148  {
149  return initialize_abstract_object<value_set_abstract_valuet>(
150  followed_type, top, bottom, e, environment, ns, configuration);
151  }
152  return initialize_abstract_object<value_set_abstract_objectt>(
153  followed_type, top, bottom, e, environment, ns, configuration);
154 
155  case ARRAY_INSENSITIVE:
156  return initialize_abstract_object<two_value_array_abstract_objectt>(
157  followed_type, top, bottom, e, environment, ns, configuration);
158  case ARRAY_SENSITIVE:
159  return initialize_abstract_object<full_array_abstract_objectt>(
160  followed_type, top, bottom, e, environment, ns, configuration);
161 
162  case POINTER_INSENSITIVE:
163  return initialize_abstract_object<two_value_pointer_abstract_objectt>(
164  followed_type, top, bottom, e, environment, ns, configuration);
165  case POINTER_SENSITIVE:
166  return initialize_abstract_object<constant_pointer_abstract_objectt>(
167  followed_type, top, bottom, e, environment, ns, configuration);
169  return initialize_abstract_object<value_set_pointer_abstract_objectt>(
170  followed_type, top, bottom, e, environment, ns, configuration);
171 
172  case STRUCT_INSENSITIVE:
173  return initialize_abstract_object<two_value_struct_abstract_objectt>(
174  followed_type, top, bottom, e, environment, ns, configuration);
175  case STRUCT_SENSITIVE:
176  return initialize_abstract_object<full_struct_abstract_objectt>(
177  followed_type, top, bottom, e, environment, ns, configuration);
178 
179  case UNION_INSENSITIVE:
180  return initialize_abstract_object<two_value_union_abstract_objectt>(
181  followed_type, top, bottom, e, environment, ns, configuration);
182 
183  default:
184  UNREACHABLE;
185  return initialize_abstract_object<abstract_objectt>(
186  followed_type, top, bottom, e, environment, ns, configuration);
187  }
188 }
189 
192  const abstract_object_pointert &abstract_object) const
193 {
194  return wrap_with_context_object(abstract_object, configuration);
195 }
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:191
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:85
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:52
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:123
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:69
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