GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdo.h Lines: 33 33 100.0 %
Date: 2021-03-22 Branches: 64 176 36.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cdo.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Clark Barrett, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A context-dependent object.
13
 **
14
 ** A context-dependent object.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__CONTEXT__CDO_H
20
#define CVC4__CONTEXT__CDO_H
21
22
#include "context/context.h"
23
24
25
namespace CVC4 {
26
namespace context {
27
28
/**
29
 * Most basic template for context-dependent objects.  Simply makes a copy
30
 * (using the copy constructor) of class T when saving, and copies it back
31
 * (using operator=) during restore.
32
 */
33
template <class T>
34
class CDO : public ContextObj {
35
36
  /**
37
   * The data of type T being stored in this context-dependent object.
38
   */
39
  T d_data;
40
41
protected:
42
43
  /**
44
   * Copy constructor - it's private to ensure it is only used by save().
45
   * Basic CDO objects, cannot be copied-they have to be unique.
46
   */
47
28290933
  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
48
49
  /**
50
   * operator= for CDO is private to ensure CDO object is not copied.
51
   */
52
  CDO<T>& operator=(const CDO<T>& cdo) = delete;
53
54
  /**
55
   * Implementation of mandatory ContextObj method save: simply copies the
56
   * current data to a copy using the copy constructor.  Memory is allocated
57
   * using the ContextMemoryManager.
58
   */
59
28290933
  ContextObj* save(ContextMemoryManager* pCMM) override
60
  {
61
28290933
    Debug("context") << "save cdo " << this;
62
28290933
    ContextObj* p = new(pCMM) CDO<T>(*this);
63
28290933
    Debug("context") << " to " << p << std::endl;
64
28290933
    return p;
65
  }
66
67
  /**
68
   * Implementation of mandatory ContextObj method restore: simply copies the
69
   * saved data back from the saved copy using operator= for T.
70
   */
71
28290923
  void restore(ContextObj* pContextObj) override
72
  {
73
    //Debug("context") << "restore cdo " << this;
74
28290923
    CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
75
28290923
    d_data = p->d_data;
76
    //Debug("context") << " to " << get() << std::endl;
77
    // Explicitly call destructor as it will not otherwise get called.
78
491063
    p->d_data.~T();
79
28290923
  }
80
81
public:
82
83
  /**
84
   * Main constructor - uses default constructor for T to create the initial
85
   * value of d_data.
86
   */
87
210633
  CDO(Context* context) :
88
    ContextObj(context),
89
210633
    d_data(T()) {
90
210633
  }
91
92
  /**
93
   * Main constructor - uses default constructor for T to create the
94
   * initial value of d_data.
95
   *
96
   * This version takes an argument that specifies whether this CDO<>
97
   * was itself allocated in context memory.  If it was, it is linked
98
   * with the current scope rather than scope 0.
99
   *
100
   * WARNING: Read the notes in src/context/context.h on "Gotchas when
101
   * allocating contextual objects with non-standard allocators."
102
   */
103
12412
  CDO(bool allocatedInCMM, Context* context) :
104
    ContextObj(allocatedInCMM, context),
105
12412
    d_data(T()) {
106
12412
  }
107
108
  /**
109
   * Constructor from object of type T.  Creates a ContextObj and sets the data
110
   * to the given data value.  Note that this value is only valid in the
111
   * current Scope.  If the Scope is popped, the value will revert to whatever
112
   * is assigned by the default constructor for T
113
   */
114
2356743
  CDO(Context* context, const T& data) :
115
    ContextObj(context),
116
2356743
    d_data(T()) {
117
2356743
    makeCurrent();
118
2356743
    d_data = data;
119
2356743
  }
120
121
  /**
122
   * Constructor from object of type T.  Creates a ContextObj and sets the data
123
   * to the given data value.  Note that this value is only valid in the
124
   * current Scope.  If the Scope is popped, the value will revert to whatever
125
   * is assigned by the default constructor for T.
126
   *
127
   * This version takes an argument that specifies whether this CDO<>
128
   * was itself allocated in context memory.  If it was, it is linked
129
   * with the current scope rather than scope 0.
130
   *
131
   * WARNING: Read the notes in src/context/context.h on "Gotchas when
132
   * allocating contextual objects with non-standard allocators."
133
   */
134
  CDO(bool allocatedInCMM, Context* context, const T& data) :
135
    ContextObj(allocatedInCMM, context),
136
    d_data(T()) {
137
    makeCurrent();
138
    d_data = data;
139
  }
140
141
  /**
142
   * Destructor - call destroy() method
143
   */
144
2578944
  ~CDO() { destroy(); }
145
146
  /**
147
   * Set the data in the CDO.  First call makeCurrent.
148
   */
149
156632489
  void set(const T& data) {
150
156632489
    makeCurrent();
151
156632489
    d_data = data;
152
156632489
  }
153
154
  /**
155
   * Get the current data from the CDO.  Read-only.
156
   */
157
1195010151
  const T& get() const { return d_data; }
158
159
  /**
160
   * For convenience, define operator T() to be the same as get().
161
   */
162
978893091
  operator T() { return get(); }
163
164
  /**
165
   * For convenience, define operator const T() to be the same as get().
166
   */
167
180667516
  operator const T() const { return get(); }
168
169
  /**
170
   * For convenience, define operator= that takes an object of type T.
171
   */
172
156008823
  CDO<T>& operator=(const T& data) {
173
156008823
    set(data);
174
156008823
    return *this;
175
  }
176
177
};/* class CDO */
178
179
}/* CVC4::context namespace */
180
}/* CVC4 namespace */
181
182
#endif /* CVC4__CONTEXT__CDO_H */