cprover
context_abstract_object.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity context_abstract_object
4 
5  Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
10 
12 {
13  return child_abstract_object;
14 }
15 
17 {
18  child_abstract_object = child;
19 }
20 
22 {
23  if(!child_abstract_object->is_top())
24  set_child(child_abstract_object->make_top());
25 }
26 
28 {
29  if(child_abstract_object->is_top())
30  set_child(child_abstract_object->clear_top());
31 }
32 
50  abstract_environmentt &environment,
51  const namespacet &ns,
52  const std::stack<exprt> &stack,
53  const exprt &specifier,
54  const abstract_object_pointert &value,
55  bool merging_write) const
56 {
57  abstract_object_pointert updated_child = child_abstract_object->write(
58  environment, ns, stack, specifier, value, merging_write);
59 
60  // Only perform an update if the write to the child has in fact changed it...
61  if(updated_child == child_abstract_object)
62  return shared_from_this();
63 
64  // Need to ensure the result of the write is still wrapped in a context
65  const auto &result =
66  std::dynamic_pointer_cast<context_abstract_objectt>(mutable_clone());
67 
68  // Update the child and record the updated write locations
69  result->set_child(updated_child);
70 
71  return result;
72 }
73 
87  const exprt &expr,
88  const std::vector<abstract_object_pointert> &operands,
89  const abstract_environmentt &environment,
90  const namespacet &ns) const
91 {
92  PRECONDITION(expr.operands().size() == operands.size());
93 
94  std::vector<abstract_object_pointert> child_operands;
95 
97  operands.begin(),
98  operands.end(),
99  std::back_inserter(child_operands),
100  [](const abstract_object_pointert &op) {
101  PRECONDITION(op != nullptr);
102  auto p = std::dynamic_pointer_cast<const context_abstract_objectt>(op);
103  INVARIANT(p, "Operand shall be of type context_abstract_objectt");
104  return p->child_abstract_object;
105  });
106 
107  return child_abstract_object->expression_transform(
108  expr, child_operands, environment, ns);
109 }
110 
120  std::ostream &out,
121  const ai_baset &ai,
122  const namespacet &ns) const
123 {
124  child_abstract_object->output(out, ai, ns);
125 }
126 
136  const abstract_object_pointert before) const
137 {
138  // Default implementation, with no other information to go on
139  // falls back to relying on copy-on-write and pointer inequality
140  // to indicate if an abstract_objectt has been modified
141  auto before_context =
142  std::dynamic_pointer_cast<const context_abstract_objectt>(before);
143 
144  return this->child_abstract_object.get() !=
145  before_context->child_abstract_object.get();
146 }
147 
149 {
150  return child_abstract_object->unwrap_context();
151 }
152 
154  abstract_object_statisticst &statistics,
155  abstract_object_visitedt &visited,
156  const abstract_environmentt &env,
157  const namespacet &ns) const
158 {
159  abstract_objectt::get_statistics(statistics, visited, env, ns);
160  if(visited.find(child_abstract_object) == visited.end())
161  {
162  child_abstract_object->get_statistics(statistics, visited, env, ns);
163  }
164  statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this));
165 }
context_abstract_objectt::expression_transform
abstract_object_pointert expression_transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
Try to resolve an expression with the maximum level of precision available.
Definition: context_abstract_object.cpp:86
context_abstract_objectt::set_top_internal
void set_top_internal() override
Definition: context_abstract_object.cpp:21
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
context_abstract_objectt::output
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
Output a representation of the value of this abstract object.
Definition: context_abstract_object.cpp:119
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:157
context_abstract_object.h
General implementation of a an abstract_objectt which can track side information in the form of a 'co...
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
context_abstract_objectt::get_child
abstract_object_pointert get_child() const
Definition: context_abstract_object.cpp:11
abstract_objectt::get_statistics
virtual void get_statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const
Definition: abstract_object.cpp:284
context_abstract_objectt::unwrap_context
abstract_object_pointert unwrap_context() const override
Definition: context_abstract_object.cpp:148
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
abstract_object_statisticst
Definition: abstract_object_statistics.h:19
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
context_abstract_objectt::write
abstract_object_pointert write(abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
A helper function to evaluate writing to a component of an abstract object.
Definition: context_abstract_object.cpp:49
context_abstract_objectt::set_not_top_internal
void set_not_top_internal() override
Definition: context_abstract_object.cpp:27
context_abstract_objectt::child_abstract_object
CLONE abstract_object_pointert child_abstract_object
Definition: context_abstract_object.h:101
abstract_object_visitedt
std::set< abstract_object_pointert > abstract_object_visitedt
Definition: abstract_object.h:76
context_abstract_objectt::has_been_modified
bool has_been_modified(const abstract_object_pointert before) const override
Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state...
Definition: context_abstract_object.cpp:135
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
exprt::operands
operandst & operands()
Definition: expr.h:96
context_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: context_abstract_object.cpp:153
memory_sizet::from_bytes
static memory_sizet from_bytes(std::size_t bytes)
Definition: memory_units.cpp:38
abstract_objectt::mutable_clone
virtual internal_abstract_object_pointert mutable_clone() const
Definition: abstract_object.h:404
context_abstract_objectt::set_child
void set_child(const abstract_object_pointert &child)
Definition: context_abstract_object.cpp:16