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
#define CLONE
sharing_ptrt< class abstract_objectt > abstract_object_pointert
std::set< goto_programt::const_targett > locationst
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
const typet & type() const override
Get the real type of the variable this abstract object is representing.
bool operator()(goto_programt::const_targett instruction, goto_programt::const_targett other_instruction) const
std::set< goto_programt::const_targett > get_data_dominators() const
Return the set of data dominators associated with this node.
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...
abstract_object_pointert set_data_deps(const dependencest &dependencies) const
Set the given set of data dependencies for this data_dependency_context object.
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...
data_dependency_contextt(const abstract_object_pointert child, const typet &type, bool top, bool bottom)
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...
std::set< goto_programt::const_targett > get_data_dependencies() const
Return the set of data dependencies associated with this node.
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...
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.
data_dependency_contextt(const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
abstract_object_pointert set_data_deps(const locationst &locations) const
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.
data_dependency_contextt(const abstract_object_pointert child, const typet &type)
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...
std::set< goto_programt::const_targett, location_ordert > dependencest
abstract_object_pointert insert_data_deps(const locationst &locations) const
Base class for all expressions.
Definition: expr.h:54
instructionst::const_iterator const_targett
Definition: goto_program.h:551
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
The type of an expression, extends irept.
Definition: type.h:28
General implementation of an abstract_objectt which tracks the last written locations for a given abs...
There are different ways of handling arrays, structures, unions and pointers.
Maintain a context in the variable sensitvity domain that records write locations for a given abstrac...