cprover
constant_pointer_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity
4 
5  Author: Thomas Kiley, thomas.kiley@diffblue.com
6 
7 \*******************************************************************/
8 
10 
11 #include <analyses/ai.h>
13 #include <util/pointer_expr.h>
14 #include <util/std_expr.h>
15 #include <util/std_types.h>
16 
17 #include <ostream>
18 
20  const typet &type)
22 {
23  PRECONDITION(type.id() == ID_pointer);
24 }
25 
27  const typet &type,
28  bool top,
29  bool bottom)
30  : abstract_pointer_objectt(type, top, bottom)
31 {
32  PRECONDITION(type.id() == ID_pointer);
33 }
34 
37  : abstract_pointer_objectt(old), value_stack(old.value_stack)
38 {
39 }
40 
42  const exprt &expr,
43  const abstract_environmentt &environment,
44  const namespacet &ns)
45  : abstract_pointer_objectt(expr, environment, ns),
46  value_stack(expr, environment, ns)
47 {
48  PRECONDITION(expr.type().id() == ID_pointer);
50  {
51  set_top();
52  }
53  else
54  {
55  set_not_top();
56  }
57 }
58 
61 {
62  auto cast_other =
63  std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(other);
64  if(cast_other)
65  {
66  return merge_constant_pointers(cast_other);
67  }
68  else
69  {
70  // TODO(tkiley): How do we set the result to be toppish?
71  return abstract_pointer_objectt::merge(other);
72  }
73 }
74 
77  const constant_pointer_abstract_pointert &other) const
78 {
79  if(is_bottom())
80  {
81  return std::make_shared<constant_pointer_abstract_objectt>(*other);
82  }
83  else
84  {
85  bool matching_pointer =
86  value_stack.to_expression() == other->value_stack.to_expression();
87 
88  if(matching_pointer)
89  {
90  return shared_from_this();
91  }
92  else
93  {
94  return abstract_pointer_objectt::merge(other);
95  }
96  }
97 }
98 
100 {
101  if(is_top() || is_bottom())
102  {
104  }
105  else
106  {
107  // TODO(tkiley): I think we would like to eval this before using it
108  // in the to_constant.
109  return value_stack.to_expression();
110  }
111 }
112 
114  std::ostream &out,
115  const ai_baset &ai,
116  const namespacet &ns) const
117 {
118  if(is_top() || is_bottom() || value_stack.is_top_value())
119  {
121  }
122  else
123  {
124  out << "ptr ->(";
125  const exprt &value = value_stack.to_expression();
126  if(value.id() == ID_address_of)
127  {
128  const auto &addressee = to_address_of_expr(value).object();
129  if(addressee.id() == ID_symbol)
130  {
131  const symbol_exprt &symbol_pointed_to(to_symbol_expr(addressee));
132 
133  out << symbol_pointed_to.get_identifier();
134  }
135  else if(addressee.id() == ID_index)
136  {
137  auto const &array_index = to_index_expr(addressee);
138  auto const &array = array_index.array();
139  if(array.id() == ID_symbol)
140  {
141  auto const &array_symbol = to_symbol_expr(array);
142  out << array_symbol.get_identifier() << "[";
143  if(array_index.index().id() == ID_constant)
144  out << to_constant_expr(array_index.index()).get_value();
145  else
146  out << "?";
147  out << "]";
148  }
149  }
150  }
151 
152  out << ")";
153  }
154 }
155 
157  const abstract_environmentt &env,
158  const namespacet &ns) const
159 {
160  if(is_top() || is_bottom() || value_stack.is_top_value())
161  {
162  // Return top if dereferencing a null pointer or we are top
163  bool is_value_top = is_top() || value_stack.is_top_value();
164  return env.abstract_object_factory(
165  type().subtype(), ns, is_value_top, !is_value_top);
166  }
167  else
168  {
169  return env.eval(
171  }
172 }
173 
175  abstract_environmentt &environment,
176  const namespacet &ns,
177  const std::stack<exprt> &stack,
178  const abstract_object_pointert &new_value,
179  bool merging_write) const
180 {
181  if(is_top() || is_bottom() || value_stack.is_top_value())
182  {
184  environment, ns, stack, new_value, merging_write);
185  }
186  else
187  {
188  if(stack.empty())
189  {
190  // We should not be changing the type of an abstract object
191  PRECONDITION(new_value->type() == ns.follow(type().subtype()));
192 
193  // Get an expression that we can assign to
195  if(merging_write)
196  {
197  abstract_object_pointert pointed_value = environment.eval(value, ns);
198  abstract_object_pointert merged_value =
199  abstract_objectt::merge(pointed_value, new_value);
200  environment.assign(value, merged_value, ns);
201  }
202  else
203  {
204  environment.assign(value, new_value, ns);
205  }
206  }
207  else
208  {
210  abstract_object_pointert pointed_value = environment.eval(value, ns);
211  abstract_object_pointert modified_value =
212  environment.write(pointed_value, new_value, stack, ns, merging_write);
213  environment.assign(value, modified_value, ns);
214 
215  // but the pointer itself does not change!
216  }
217  return std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
218  shared_from_this());
219  }
220 }
221 
223  abstract_object_statisticst &statistics,
224  abstract_object_visitedt &visited,
225  const abstract_environmentt &env,
226  const namespacet &ns) const
227 {
228  abstract_pointer_objectt::get_statistics(statistics, visited, env, ns);
229  // don't bother following nullptr
230  if(!is_top() && !is_bottom() && !value_stack.is_top_value())
231  {
232  read_dereference(env, ns)->get_statistics(statistics, visited, env, ns);
233  }
234  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
235 }
constant_pointer_abstract_objectt::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Print the value of the pointer.
Definition: constant_pointer_abstract_object.cpp:113
write_stackt::is_top_value
bool is_top_value() const
Is the stack representing an unknown value and hence can't be written to or read from.
Definition: write_stack.cpp:207
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
abstract_objectt::is_top
virtual bool is_top() const
Find out if the abstract object is top.
Definition: abstract_object.cpp:150
abstract_objectt::merge
static abstract_object_pointert merge(abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
Clones the first parameter and merges it with the second.
Definition: abstract_object.cpp:189
abstract_objectt::output
virtual void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print the value of the abstract object.
Definition: abstract_object.cpp:170
constant_pointer_abstract_objectt::merge_constant_pointers
abstract_object_pointert merge_constant_pointers(const constant_pointer_abstract_pointert &other) const
Merges two constant pointers.
Definition: constant_pointer_abstract_object.cpp:76
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:209
abstract_environmentt::write
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
Definition: abstract_environment.cpp:183
constant_pointer_abstract_objectt::merge
abstract_object_pointert merge(abstract_object_pointert op1) const override
Set this abstract object to be the result of merging this abstract object.
Definition: constant_pointer_abstract_object.cpp:60
typet
The type of an expression, extends irept.
Definition: type.h:28
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
abstract_objectt::type
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
Definition: abstract_object.cpp:53
constant_pointer_abstract_objectt::write_dereference
abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a pointers value.
Definition: constant_pointer_abstract_object.cpp:174
constant_pointer_abstract_objectt::value_stack
write_stackt value_stack
Definition: constant_pointer_abstract_object.h:140
abstract_environmentt::assign
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
Definition: abstract_environment.cpp:93
abstract_pointer_objectt
Definition: abstract_pointer_object.h:22
abstract_objectt::set_top
void set_top()
Definition: abstract_object.h:449
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
abstract_pointer_objectt::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: abstract_pointer_object.cpp:86
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
constant_pointer_abstract_objectt::constant_pointer_abstract_pointert
sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert
Definition: constant_pointer_abstract_object.h:23
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
constant_pointer_abstract_objectt::read_dereference
abstract_object_pointert read_dereference(const abstract_environmentt &env, const namespacet &ns) const override
A helper function to dereference a value from a pointer.
Definition: constant_pointer_abstract_object.cpp:156
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
abstract_environmentt::abstract_object_factory
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
Definition: abstract_environment.cpp:251
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
constant_pointer_abstract_objectt
Definition: constant_pointer_abstract_object.h:20
std_types.h
Pre-defined types.
constant_pointer_abstract_object.h
An abstraction of a pointer that tracks a single pointer.
pointer_expr.h
API to expression classes for Pointers.
abstract_environment.h
An abstract version of a program environment.
abstract_objectt::to_constant
virtual exprt to_constant() const
Converts to a constant expression if possible.
Definition: abstract_object.cpp:165
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
constant_pointer_abstract_objectt::to_constant
exprt to_constant() const override
To try and find a constant expression for this abstract object.
Definition: constant_pointer_abstract_object.cpp:99
abstract_environmentt::eval
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
Definition: abstract_environment.cpp:37
irept::id
const irep_idt & id() const
Definition: irep.h:407
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
abstract_pointer_objectt::write_dereference
virtual abstract_object_pointert write_dereference(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const
Evaluate writing to a pointer's value.
Definition: abstract_pointer_object.cpp:70
ai.h
Abstract Interpretation.
constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
constant_pointer_abstract_objectt(const typet &type)
Definition: constant_pointer_abstract_object.cpp:19
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
abstract_object_statisticst::objects_memory_usage
memory_sizet objects_memory_usage
An underestimation of the memory usage of the abstract objects.
Definition: abstract_object_statistics.h:28
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
abstract_objectt::set_not_top
void set_not_top()
Definition: abstract_object.h:454
constant_pointer_abstract_objectt::get_statistics
void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
Definition: constant_pointer_abstract_object.cpp:222
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
abstract_objectt::is_bottom
virtual bool is_bottom() const
Find out if the abstract object is bottom.
Definition: abstract_object.cpp:155
write_stackt::to_expression
exprt to_expression() const
Convert the stack to an expression that can be used to write to.
Definition: write_stack.cpp:174
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2676
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701