cprover
data_dependency_context.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: analyses variable-sensitivity data_dependency_context
4 
5 Author: Diffblue Ltd
6 
7 \*******************************************************************/
8 
14 #ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
15 #define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
16 
18 #include "write_location_context.h"
19 
21 {
22 public:
23  // These constructors mirror those in the base abstract_objectt, but with
24  // the addition of an extra argument which is the abstract_objectt to wrap.
26  const abstract_object_pointert child,
27  const typet &type)
29  {
30  }
31 
33  const abstract_object_pointert child,
34  const typet &type,
35  bool top,
36  bool bottom)
38  {
39  }
40 
42  const abstract_object_pointert child,
43  const exprt &expr,
44  const abstract_environmentt &environment,
45  const namespacet &ns)
46  : write_location_contextt(child, expr, environment, ns)
47  {
48  }
49 
51  abstract_environmentt &environment,
52  const namespacet &ns,
53  const std::stack<exprt> &stack,
54  const exprt &specifier,
55  const abstract_object_pointert &value,
56  bool merging_write) const override;
57 
59  const abstract_objectt::locationst &locations,
60  const bool update_sub_elements) const override;
61 
62  bool has_been_modified(const abstract_object_pointert before) const override;
63 
64  std::set<goto_programt::const_targett> get_data_dependencies() const;
65  std::set<goto_programt::const_targett> get_data_dominators() const;
66 
67  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
68  const override;
69 
70 protected:
71  CLONE
72 
74 
76  const abstract_object_pointert other) const override;
77 
78 private:
80  {
81  public:
82  bool operator()(
83  goto_programt::const_targett instruction,
84  goto_programt::const_targett other_instruction) const
85  {
86  return instruction->location_number > other_instruction->location_number;
87  }
88  };
89  typedef std::set<goto_programt::const_targett, location_ordert> dependencest;
92 
94  insert_data_deps(const dependencest &dependencies) const;
95 
97  set_data_deps(const dependencest &dependencies) const;
98 
100  {
101  // `locationst` is unsorted, so convert this to a sorted `dependenciest`
102  dependencest dependencies(locations.begin(), locations.end());
103 
104  return insert_data_deps(dependencies);
105  }
106 
108  {
109  // `locationst` is unsorted, so convert this to a sorted `dependenciest`
110  dependencest dependencies(locations.begin(), locations.end());
111 
112  return set_data_deps(dependencies);
113  }
114 };
115 
116 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_DATA_DEPENDENCY_CONTEXT_H
data_dependency_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: data_dependency_context.cpp:340
data_dependency_contextt::update_location_context
abstract_object_pointert update_location_context(const abstract_objectt::locationst &locations, const bool update_sub_elements) const override
Update the location context for an abstract object, potentially propogating the update to any childre...
Definition: data_dependency_context.cpp:216
abstract_object_pointert
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Definition: abstract_object.h:75
data_dependency_contextt::location_ordert::operator()
bool operator()(goto_programt::const_targett instruction, goto_programt::const_targett other_instruction) const
Definition: data_dependency_context.h:82
typet
The type of an expression, extends irept.
Definition: type.h:28
data_dependency_contextt::data_dependency_contextt
data_dependency_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
Definition: data_dependency_context.h:41
data_dependency_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: data_dependency_context.cpp:186
data_dependency_contextt::get_data_dependencies
std::set< goto_programt::const_targett > get_data_dependencies() const
Return the set of data dependencies associated with this node.
Definition: data_dependency_context.cpp:318
abstract_environmentt
Definition: abstract_environment.h:36
exprt
Base class for all expressions.
Definition: expr.h:54
write_location_context.h
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...
data_dependency_contextt::location_ordert
Definition: data_dependency_context.h:80
CLONE
#define CLONE
Definition: abstract_object.h:47
data_dependency_contextt::data_dependency_contextt
data_dependency_contextt(const abstract_object_pointert child, const typet &type)
Definition: data_dependency_context.h:25
data_dependency_contextt::data_dependency_contextt
data_dependency_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
Definition: data_dependency_context.h:32
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
data_dependency_contextt::insert_data_deps
abstract_object_pointert insert_data_deps(const locationst &locations) const
Definition: data_dependency_context.h:99
data_dependency_contextt::merge
CLONE abstract_object_pointert merge(abstract_object_pointert other) const override
Create a new abstract object that is the result of merging this abstract object with a given abstract...
Definition: data_dependency_context.cpp:238
abstract_objectt::locationst
std::set< goto_programt::const_targett > locationst
Definition: abstract_object.h:215
context_abstract_objectt::type
const typet & type() const override
Get the real type of the variable this abstract object is representing.
Definition: context_abstract_object.h:58
write_location_contextt
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
Definition: write_location_context.h:35
abstract_objectt::bottom
bool bottom
Definition: abstract_object.h:362
data_dependency_contextt
Definition: data_dependency_context.h:21
data_dependency_contextt::dependencest
std::set< goto_programt::const_targett, location_ordert > dependencest
Definition: data_dependency_context.h:89
data_dependency_contextt::get_data_dominators
std::set< goto_programt::const_targett > get_data_dominators() const
Return the set of data dominators associated with this node.
Definition: data_dependency_context.cpp:332
variable_sensitivity_domain.h
There are different ways of handling arrays, structures, unions and pointers.
data_dependency_contextt::set_data_deps
abstract_object_pointert set_data_deps(const locationst &locations) const
Definition: data_dependency_context.h:107
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
data_dependency_contextt::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: data_dependency_context.cpp:28
data_dependency_contextt::insert_data_deps
abstract_object_pointert insert_data_deps(const dependencest &dependencies) const
Insert the given set of data dependencies into the data dependencies set for this data_dependency_con...
Definition: data_dependency_context.cpp:82
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
abstract_objectt::top
bool top
Definition: abstract_object.h:363
data_dependency_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: data_dependency_context.cpp:295
data_dependency_contextt::set_data_deps
abstract_object_pointert set_data_deps(const dependencest &dependencies) const
Set the given set of data dependencies for this data_dependency_context object.
Definition: data_dependency_context.cpp:139
data_dependency_contextt::data_deps
dependencest data_deps
Definition: data_dependency_context.h:90
data_dependency_contextt::data_dominators
dependencest data_dominators
Definition: data_dependency_context.h:91