CBMC
liveness_context.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: analyses variable-sensitivity region_contextt
4 
5  Author: Jez Higgins
6 
7 \*******************************************************************/
8 
9 #include "liveness_context.h"
10 
12 {
13  return assign_location.has_value();
14 }
15 
17 {
18  return assign_location.value();
19 }
20 
38  abstract_environmentt &environment,
39  const namespacet &ns,
40  const std::stack<exprt> &stack,
41  const exprt &specifier,
42  const abstract_object_pointert &value,
43  bool merging_write) const
44 {
45  auto updated = std::dynamic_pointer_cast<const liveness_contextt>(
47  environment, ns, stack, specifier, value, merging_write));
48  if(updated == shared_from_this())
49  return shared_from_this();
50 
51  // record the updated write locations
52  auto result =
53  std::dynamic_pointer_cast<liveness_contextt>(updated->mutable_clone());
54  auto value_context =
55  std::dynamic_pointer_cast<const liveness_contextt>(value);
56  if(value_context)
57  result->set_location(value_context->get_location());
58 
59  return result;
60 }
61 
73  const abstract_object_pointert &other,
74  const widen_modet &widen_mode) const
75 {
76  auto cast_other = std::dynamic_pointer_cast<const liveness_contextt>(other);
77 
78  if(cast_other)
79  {
80  auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
81  write_location_contextt::merge(other, widen_mode));
82  return reset_location_on_merge(merged);
83  }
84 
85  return abstract_objectt::merge(other, widen_mode);
86 }
87 
89  const abstract_object_pointert &other) const
90 {
91  auto merged = std::dynamic_pointer_cast<const liveness_contextt>(
93  return reset_location_on_merge(merged);
94 }
95 
97  const liveness_context_ptrt &merged) const
98 {
99  if(merged == shared_from_this())
100  return shared_from_this();
101 
102  auto updated =
103  std::dynamic_pointer_cast<liveness_contextt>(merged->mutable_clone());
104  updated->assign_location.reset();
105  return updated;
106 }
107 
110  const locationst &locations) const
111 {
112  auto result = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
113  result->set_last_written_locations(locations);
114  result->set_location(*locations.cbegin());
115  return result;
116 }
117 
119 {
120  assign_location.emplace(location);
121 }
122 
132  std::ostream &out,
133  const ai_baset &ai,
134  const namespacet &ns) const
135 {
137 
138  if(has_location())
139  out << " @ [" << get_location()->location_number << "]";
140  else
141  out << " @ [undefined]";
142 }
143 
146 {
147  if(assign_location.has_value())
148  return shared_from_this();
149 
150  auto update = std::dynamic_pointer_cast<liveness_contextt>(mutable_clone());
151  update->assign_location = location;
152  auto updated_child = child_abstract_object->merge_location_context(location);
153  update->set_child(updated_child);
154 
155  return update;
156 }
liveness_contextt::reset_location_on_merge
abstract_object_pointert reset_location_on_merge(const liveness_context_ptrt &merged) const
Definition: liveness_context.cpp:96
widen_modet
widen_modet
Definition: abstract_environment.h:32
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:69
liveness_contextt::set_location
void set_location(const locationt &location)
Definition: liveness_context.cpp:118
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:141
liveness_contextt::assign_location
optionalt< locationt > assign_location
Definition: liveness_context.h:93
abstract_objectt::locationt
goto_programt::const_targett locationt
Definition: abstract_object.h:220
context_abstract_objectt::child_abstract_object
abstract_object_pointert child_abstract_object
Definition: context_abstract_object.h:114
abstract_environmentt
Definition: abstract_environment.h:40
exprt
Base class for all expressions.
Definition: expr.h:55
liveness_contextt::abstract_object_merge_internal
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert &other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
Definition: liveness_context.cpp:88
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
abstract_objectt::merge
static combine_result merge(const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)
Definition: abstract_object.cpp:209
liveness_contextt::get_location
locationt get_location() const
Definition: liveness_context.cpp:16
liveness_contextt::update_location_context_internal
context_abstract_object_ptrt update_location_context_internal(const locationst &locations) const override
Definition: liveness_context.cpp:109
liveness_contextt::mutable_clone
internal_abstract_object_pointert mutable_clone() const override
Definition: liveness_context.h:70
write_location_contextt::abstract_object_merge_internal
abstract_object_pointert abstract_object_merge_internal(const abstract_object_pointert &other) const override
Helper function for abstract_objectt::abstract_object_merge to perform any additional actions after t...
Definition: write_location_context.cpp:163
liveness_contextt::merge
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
Definition: liveness_context.cpp:72
write_location_contextt::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: write_location_context.cpp:35
context_abstract_objectt::context_abstract_object_ptrt
std::shared_ptr< context_abstract_objectt > context_abstract_object_ptrt
Definition: context_abstract_object.h:111
write_location_contextt::merge
abstract_object_pointert merge(const abstract_object_pointert &other, const widen_modet &widen_mode) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
Definition: write_location_context.cpp:79
context_abstract_objectt::locationst
std::set< locationt > locationst
Definition: context_abstract_object.h:135
liveness_contextt::liveness_context_ptrt
std::shared_ptr< const liveness_contextt > liveness_context_ptrt
Definition: liveness_context.h:88
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:118
liveness_contextt::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: liveness_context.cpp:37
liveness_context.h
liveness_contextt::has_location
bool has_location() const
Definition: liveness_context.cpp:11
liveness_contextt::merge_location_context
abstract_object_pointert merge_location_context(const locationt &location) const override
Update the merge location context for an abstract object.
Definition: liveness_context.cpp:145
liveness_contextt::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: liveness_context.cpp:131