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 
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 {
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 
71 template <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 
157  case ARRAY_INSENSITIVE:
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 
164  case POINTER_INSENSITIVE:
165  return initialize_abstract_object<two_value_pointer_abstract_objectt>(
166  followed_type, top, bottom, e, environment, ns, configuration);
167  case POINTER_SENSITIVE:
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 
174  case STRUCT_INSENSITIVE:
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 
181  case UNION_INSENSITIVE:
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:
197  UNREACHABLE;
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:185
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_namet &name, const irep_idt &value)
Definition: irep.h:431
const irep_idt & id() const
Definition: irep.h:407
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:28
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...