GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdlist.h Lines: 123 129 95.3 %
Date: 2021-03-22 Branches: 878 2390 36.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cdlist.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Clark Barrett
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 Context-dependent list class (only supports append)
13
 **
14
 ** Context-dependent list class.  This list only supports appending
15
 ** to the list; on backtrack, the list is simply shortened.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__CONTEXT__CDLIST_H
21
#define CVC4__CONTEXT__CDLIST_H
22
23
#include <cstring>
24
#include <iterator>
25
#include <string>
26
27
#include "base/check.h"
28
#include "context/cdlist_forward.h"
29
#include "context/context.h"
30
#include "context/context_mm.h"
31
32
namespace CVC4 {
33
namespace context {
34
35
/**
36
 * Generic context-dependent dynamic array.  Note that for efficiency,
37
 * this implementation makes the following assumptions:
38
 *
39
 * 1. Over time, objects are only added to the list.  Objects are only
40
 *    removed when a pop restores the list to a previous state.
41
 *
42
 * 2. T objects can safely be copied using their copy constructor,
43
 *    operator=, and memcpy.
44
 */
45
template <class T, class CleanUpT, class AllocatorT>
46
class CDList : public ContextObj {
47
public:
48
49
  /** The value type with which this CDList<> was instantiated. */
50
  typedef T value_type;
51
52
  /** The cleanup type with which this CDList<> was instantiated. */
53
  typedef CleanUpT CleanUp;
54
55
  /** The allocator type with which this CDList<> was instantiated. */
56
  typedef AllocatorT Allocator;
57
58
protected:
59
60
  /**
61
   * d_list is a dynamic array of objects of type T.
62
   */
63
  T* d_list;
64
65
  /**
66
   * Number of objects in d_list
67
   */
68
  size_t d_size;
69
70
private:
71
72
  static const size_t INITIAL_SIZE = 10;
73
  static const size_t GROWTH_FACTOR = 2;
74
75
  /**
76
   * Whether to call the destructor when items are popped from the
77
   * list.  True by default, but can be set to false by setting the
78
   * second argument in the constructor to false.
79
   */
80
  bool d_callDestructor;
81
82
  /**
83
   * Allocated size of d_list.
84
   */
85
  size_t d_sizeAlloc;
86
87
  /**
88
   * The CleanUp functor.
89
   */
90
  CleanUp d_cleanUp;
91
92
  /**
93
   * Our allocator.
94
   */
95
  Allocator d_allocator;
96
97
protected:
98
  /**
99
   * Private copy constructor used only by save().  d_list and
100
   * d_sizeAlloc are not copied: only the base class information and
101
   * d_size are needed in restore.
102
   */
103
15560306
  CDList(const CDList& l) :
104
    ContextObj(l),
105
    d_list(NULL),
106
15560306
    d_size(l.d_size),
107
    d_callDestructor(false),
108
    d_sizeAlloc(0),
109
    d_cleanUp(l.d_cleanUp),
110
31120612
    d_allocator(l.d_allocator) {
111
46680918
    Debug("cdlist") << "copy ctor: " << this
112
31120612
                    << " from " << &l
113
15560306
                    << " size " << d_size << std::endl;
114
15560306
  }
115
  CDList& operator=(const CDList& l) = delete;
116
117
private:
118
  /**
119
   * Reallocate the array with more space.
120
   * Throws bad_alloc if memory allocation fails.
121
   */
122
532795
  void grow() {
123
532795
    if(d_list == NULL) {
124
      // Allocate an initial list if one does not yet exist
125
355508
      d_sizeAlloc = INITIAL_SIZE;
126
1066524
      Debug("cdlist") << "initial grow of cdlist " << this
127
711016
                      << " level " << getContext()->getLevel()
128
355508
                      << " to " << d_sizeAlloc << std::endl;
129
355508
      if(d_sizeAlloc > d_allocator.max_size()) {
130
        d_sizeAlloc = d_allocator.max_size();
131
      }
132
355508
      d_list = d_allocator.allocate(d_sizeAlloc);
133
355508
      if(d_list == NULL) {
134
        throw std::bad_alloc();
135
      }
136
    } else {
137
      // Allocate a new array with double the size
138
177287
      size_t newSize = GROWTH_FACTOR * d_sizeAlloc;
139
177287
      if(newSize > d_allocator.max_size()) {
140
        newSize = d_allocator.max_size();
141
        Assert(newSize > d_sizeAlloc)
142
            << "cannot request larger list due to allocator limits";
143
      }
144
177287
      T* newList = d_allocator.allocate(newSize);
145
531855
      Debug("cdlist") << "2x grow of cdlist " << this
146
354570
                      << " level " << getContext()->getLevel()
147
177285
                      << " to " << newSize
148
177285
                      << " (from " << d_list
149
177285
                      << " to " << newList << ")" << std::endl;
150
177285
      if(newList == NULL) {
151
        throw std::bad_alloc();
152
      }
153
177285
      std::memcpy(newList, d_list, sizeof(T) * d_sizeAlloc);
154
177285
      d_allocator.deallocate(d_list, d_sizeAlloc);
155
177285
      d_list = newList;
156
177285
      d_sizeAlloc = newSize;
157
    }
158
532793
  }
159
160
  /**
161
   * Implementation of mandatory ContextObj method save: simply copies
162
   * the current size to a copy using the copy constructor (the
163
   * pointer and the allocated size are *not* copied as they are not
164
   * restored on a pop).  The saved information is allocated using the
165
   * ContextMemoryManager.
166
   */
167
11903966
  ContextObj* save(ContextMemoryManager* pCMM) override
168
  {
169
11903966
    ContextObj* data = new(pCMM) CDList<T, CleanUp, Allocator>(*this);
170
35711898
    Debug("cdlist") << "save " << this
171
23807932
                    << " at level " << this->getContext()->getLevel()
172
11903966
                    << " size at " << this->d_size
173
11903966
                    << " sizeAlloc at " << this->d_sizeAlloc
174
11903966
                    << " d_list is " << this->d_list
175
11903966
                    << " data:" << data << std::endl;
176
11903966
    return data;
177
  }
178
179
protected:
180
  /**
181
   * Implementation of mandatory ContextObj method restore: simply
182
   * restores the previous size.  Note that the list pointer and the
183
   * allocated size are not changed.
184
   */
185
15560291
 void restore(ContextObj* data) override
186
 {
187
46680873
   Debug("cdlist") << "restore " << this << " level "
188
31120582
                   << this->getContext()->getLevel() << " data == " << data
189
15560291
                   << " call dtor == " << this->d_callDestructor
190
15560291
                   << " d_list == " << this->d_list << std::endl;
191
15560291
   truncateList(((CDList<T, CleanUp, Allocator>*)data)->d_size);
192
46680873
   Debug("cdlist") << "restore " << this << " level "
193
31120582
                   << this->getContext()->getLevel() << " size back to "
194
15560291
                   << this->d_size << " sizeAlloc at " << this->d_sizeAlloc
195
                   << std::endl;
196
15560291
  }
197
198
  /**
199
   * Given a size parameter smaller than d_size, truncateList()
200
   * removes the elements from the end of the list until d_size equals size.
201
   *
202
   * WARNING! You should only use this function when you know what you are doing.
203
   * This is a primitive operation with strange context dependent behavior!
204
   * It is up to the user of the function to ensure that the saved d_size values
205
   * at lower context levels are less than or equal to size.
206
   */
207
20431012
  void truncateList(const size_t size){
208
20431012
    Assert(size <= d_size);
209
20431012
    if(d_callDestructor) {
210
178537077
      while(d_size != size) {
211
79483810
        --d_size;
212
79483810
        d_cleanUp(&d_list[d_size]);
213
79483810
        d_allocator.destroy(&d_list[d_size]);
214
      }
215
    } else {
216
861555
      d_size = size;
217
    }
218
20431012
  }
219
220
221
public:
222
223
  /**
224
   * Main constructor: d_list starts as NULL, size is 0
225
   */
226
1122422
  CDList(Context* context,
227
         bool callDestructor = true,
228
         const CleanUp& cleanup = CleanUp(),
229
         const Allocator& alloc = Allocator()) :
230
    ContextObj(context),
231
    d_list(NULL),
232
    d_size(0),
233
    d_callDestructor(callDestructor),
234
    d_sizeAlloc(0),
235
    d_cleanUp(cleanup),
236
1122422
    d_allocator(alloc) {
237
1122422
  }
238
239
  /**
240
   * Destructor: delete the list
241
   */
242
1122117
  ~CDList() {
243
1122117
    this->destroy();
244
245
1122117
    if(this->d_callDestructor) {
246
1104119
      truncateList(0);
247
    }
248
249
1122117
    this->d_allocator.deallocate(this->d_list, this->d_sizeAlloc);
250
2244234
  }
251
252
  /**
253
   * Return the current size of (i.e. valid number of objects in) the
254
   * list.
255
   */
256
123452235
  size_t size() const {
257
123452235
    return d_size;
258
  }
259
260
  /**
261
   * Return true iff there are no valid objects in the list.
262
   */
263
17937149
  bool empty() const {
264
17937149
    return d_size == 0;
265
  }
266
267
  /**
268
   * Add an item to the end of the list.
269
   */
270
89855473
  void push_back(const T& data) {
271
269566419
    Debug("cdlist") << "push_back " << this
272
179710946
                    << " " << getContext()->getLevel()
273
89855473
                    << ": make-current, "
274
89855473
                    << "d_list == " << d_list << std::endl;
275
89855473
    makeCurrent();
276
277
269566419
    Debug("cdlist") << "push_back " << this
278
179710946
                    << " " << getContext()->getLevel()
279
89855473
                    << ": grow? " << d_size
280
89855473
                    << " " << d_sizeAlloc << std::endl;
281
89855473
    if(d_size == d_sizeAlloc) {
282
1598385
      Debug("cdlist") << "push_back " << this
283
1065590
                      << " " << getContext()->getLevel()
284
532795
                      << ": grow!" << std::endl;
285
532795
      grow();
286
    }
287
89855471
    Assert(d_size < d_sizeAlloc);
288
289
269566413
    Debug("cdlist") << "push_back " << this
290
179710942
                    << " " << getContext()->getLevel()
291
89855471
                    << ": construct! at " << d_list
292
179710942
                    << "[" << d_size << "] == " << &d_list[d_size]
293
                    << std::endl;
294
89855471
    d_allocator.construct(&d_list[d_size], data);
295
269566413
    Debug("cdlist") << "push_back " << this
296
179710942
                    << " " << getContext()->getLevel()
297
89855471
                    << ": done..." << std::endl;
298
89855471
    ++d_size;
299
269566413
    Debug("cdlist") << "push_back " << this
300
179710942
                    << " " << getContext()->getLevel()
301
89855471
                    << ": size now " << d_size << std::endl;
302
89855471
  }
303
304
  /**
305
   * Access to the ith item in the list.
306
   */
307
103795118
  const T& operator[](size_t i) const {
308
103795118
    Assert(i < d_size) << "index out of bounds in CDList::operator[]";
309
103795118
    return d_list[i];
310
  }
311
312
  /**
313
   * Returns the most recent item added to the list.
314
   */
315
3203
  const T& back() const {
316
3203
    Assert(d_size > 0) << "CDList::back() called on empty list";
317
3203
    return d_list[d_size - 1];
318
  }
319
320
  /**
321
   * Iterator for CDList class.  It has to be const because we don't
322
   * allow items in the list to be changed.  It's a straightforward
323
   * wrapper around a pointer.  Note that for efficiency, we implement
324
   * only prefix increment and decrement.  Also note that it's OK to
325
   * create an iterator from an empty, uninitialized list, as begin()
326
   * and end() will have the same value (NULL).
327
   */
328
  class const_iterator {
329
    T const* d_it;
330
331
2587978
    const_iterator(T const* it) : d_it(it) {}
332
333
    friend class CDList<T, CleanUp, Allocator>;
334
335
  public:
336
337
    // FIXME we support operator--, but do we satisfy all the
338
    // requirements of a bidirectional iterator ?
339
    typedef std::input_iterator_tag iterator_category;
340
    typedef T value_type;
341
    typedef std::ptrdiff_t difference_type;
342
    typedef const T* pointer;
343
    typedef const T& reference;
344
345
52143
    const_iterator() : d_it(NULL) {}
346
347
2
    inline bool operator==(const const_iterator& i) const {
348
2
      return d_it == i.d_it;
349
    }
350
351
14471885
    inline bool operator!=(const const_iterator& i) const {
352
14471885
      return d_it != i.d_it;
353
    }
354
355
13810440
    inline const T& operator*() const {
356
13810440
      return *d_it;
357
    }
358
359
    inline const T* operator->() const { return d_it; }
360
361
    /** Prefix increment */
362
13716836
    const_iterator& operator++() {
363
13716836
      ++d_it;
364
13716836
      return *this;
365
    }
366
367
    /** Prefix decrement */
368
    const_iterator& operator--() { --d_it; return *this; }
369
370
    /** operator+ */
371
74354
    const_iterator operator+(long signed int off) const {
372
74354
      return const_iterator(d_it + off);
373
    }
374
375
    // Postfix operations on iterators: requires a Proxy object to
376
    // hold the intermediate value for dereferencing
377
    class Proxy {
378
      const T* d_t;
379
380
    public:
381
382
      Proxy(const T& p): d_t(&p) {}
383
384
      T& operator*() {
385
        return *d_t;
386
      }
387
    };/* class CDList<>::const_iterator::Proxy */
388
389
    /** Postfix increment: returns Proxy with the old value. */
390
    Proxy operator++(int) {
391
      Proxy e(*(*this));
392
      ++(*this);
393
      return e;
394
    }
395
396
    /** Postfix decrement: returns Proxy with the old value. */
397
    Proxy operator--(int) {
398
      Proxy e(*(*this));
399
      --(*this);
400
      return e;
401
    }
402
403
  };/* class CDList<>::const_iterator */
404
  typedef const_iterator iterator;
405
406
  /**
407
   * Returns an iterator pointing to the first item in the list.
408
   */
409
739665
  const_iterator begin() const {
410
739665
    return const_iterator(static_cast<T const*>(d_list));
411
  }
412
413
  /**
414
   * Returns an iterator pointing one past the last item in the list.
415
   */
416
1773959
  const_iterator end() const {
417
1773959
    return const_iterator(static_cast<T const*>(d_list) + d_size);
418
  }
419
};/* class CDList<> */
420
421
template <class T, class CleanUp>
422
class CDList<T, CleanUp, ContextMemoryAllocator<T> > : public ContextObj {
423
  /* CDList is incompatible for use with a ContextMemoryAllocator.
424
   *
425
   * Explanation:
426
   * If ContextMemoryAllocator is used and d_list grows at a deeper context
427
   * level the reallocated will be reallocated in a context memory region that
428
   * can be destroyed on pop. To support this, a full copy of d_list would have
429
   * to be made. As this is unacceptable for performance in other situations, we
430
   * do not do this.
431
   */
432
433
  static_assert(sizeof(T) == 0,
434
                "Cannot create a CDList with a ContextMemoryAllocator.");
435
};
436
437
}/* CVC4::context namespace */
438
}/* CVC4 namespace */
439
440
#endif /* CVC4__CONTEXT__CDLIST_H */