GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/attribute_internals.h Lines: 68 68 100.0 %
Date: 2021-03-22 Branches: 58 184 31.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file attribute_internals.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Andres Noetzli
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 Node attributes' internals.
13
 **
14
 ** Node attributes' internals.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
20
#  error expr/attribute_internals.h should only be included by expr/attribute.h
21
#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
22
23
#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H
24
#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H
25
26
#include <unordered_map>
27
28
namespace CVC4 {
29
namespace expr {
30
31
// ATTRIBUTE HASH FUNCTIONS ====================================================
32
33
namespace attr {
34
35
/**
36
 * A hash function for attribute table keys.  Attribute table keys are
37
 * pairs, (unique-attribute-id, Node).
38
 */
39
struct AttrHashFunction {
40
  enum { LARGE_PRIME = 32452843ul };
41
3917471406
  std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
42
3917471406
    return p.first * LARGE_PRIME + p.second->getId();
43
  }
44
};/* struct AttrHashFunction */
45
46
/**
47
 * A hash function for boolean-valued attribute table keys; here we
48
 * don't have to store a pair as the key, because we use a known bit
49
 * in [0..63] for each attribute
50
 */
51
struct AttrBoolHashFunction {
52
873384356
  std::size_t operator()(NodeValue* nv) const {
53
873384356
    return (size_t)nv->getId();
54
  }
55
};/* struct AttrBoolHashFunction */
56
57
}/* CVC4::expr::attr namespace */
58
59
// ATTRIBUTE TYPE MAPPINGS =====================================================
60
61
namespace attr {
62
63
/**
64
 * KindValueToTableValueMapping is a compile-time-only mechanism to
65
 * convert "attribute value types" into "table value types" and back
66
 * again.
67
 *
68
 * Each instantiation < T > is expected to have three members:
69
 *
70
 *   typename table_value_type
71
 *
72
 *      A type representing the underlying table's value_type for
73
 *      attribute value type (T).  It may be different from T, e.g. T
74
 *      could be a pointer-to-Foo, but the underlying table value_type
75
 *      might be pointer-to-void.
76
 *
77
 *   static [convertible-to-table_value_type] convert([convertible-from-T])
78
 *
79
 *      Converts a T into a table_value_type.  Used to convert an
80
 *      attribute value on setting it (and assigning it into the
81
 *      underlying table).  See notes on specializations of
82
 *      KindValueToTableValueMapping, below.
83
 *
84
 *   static [convertible-to-T] convertBack([convertible-from-table_value_type])
85
 *
86
 *      Converts a table_value_type back into a T.  Used to convert an
87
 *      underlying table value back into the attribute's expected type
88
 *      when retrieving it from the table.  See notes on
89
 *      specializations of KindValueToTableValueMapping, below.
90
 *
91
 * This general (non-specialized) implementation of the template does
92
 * nothing.
93
 *
94
 * The `Enable` template parameter is used to instantiate the template
95
 * conditionally: If the template substitution of Enable fails (e.g. when using
96
 * `std::enable_if` in the template parameter and the condition is false), the
97
 * instantiation is ignored due to the SFINAE rule.
98
 */
99
template <class T, class Enable = void>
100
struct KindValueToTableValueMapping
101
{
102
  /** Simple case: T == table_value_type */
103
  typedef T table_value_type;
104
  /** No conversion necessary */
105
52410084
  inline static T convert(const T& t) { return t; }
106
  /** No conversion necessary */
107
780713501
  inline static T convertBack(const T& t) { return t; }
108
};
109
110
/**
111
 * This converts arbitrary unsigned integers (up to 64-bit) to and from 64-bit
112
 * integers s.t. they can be stored in the hash table for integral-valued
113
 * attributes.
114
 */
115
template <class T>
116
struct KindValueToTableValueMapping<
117
    T,
118
    // Use this specialization only for unsigned integers
119
    typename std::enable_if<std::is_unsigned<T>::value>::type>
120
{
121
  typedef uint64_t table_value_type;
122
  /** Convert from unsigned integer to uint64_t */
123
42729223
  static uint64_t convert(const T& t)
124
  {
125
    static_assert(sizeof(T) <= sizeof(uint64_t),
126
                  "Cannot store integer attributes of a bit-width that is "
127
                  "greater than 64-bits");
128
42729223
    return static_cast<uint64_t>(t);
129
  }
130
  /** Convert from uint64_t to unsigned integer */
131
780204290
  static T convertBack(const uint64_t& t) { return static_cast<T>(t); }
132
};
133
134
}/* CVC4::expr::attr namespace */
135
136
// ATTRIBUTE HASH TABLES =======================================================
137
138
namespace attr {
139
140
// Returns a 64 bit integer with a single `bit` set when `bit` < 64.
141
// Avoids problems in (1 << x) when sizeof(x) <= sizeof(uint64_t).
142
817508297
inline uint64_t GetBitSet(uint64_t bit)
143
{
144
817508297
  constexpr uint64_t kOne = 1;
145
817508297
  return kOne << bit;
146
}
147
148
/**
149
 * An "AttrHash<value_type>"---the hash table underlying
150
 * attributes---is simply a mapping of pair<unique-attribute-id, Node>
151
 * to value_type using our specialized hash function for these pairs.
152
 */
153
template <class value_type>
154
71545
class AttrHash :
155
    public std::unordered_map<std::pair<uint64_t, NodeValue*>,
156
                               value_type,
157
                               AttrHashFunction> {
158
};/* class AttrHash<> */
159
160
/**
161
 * In the case of Boolean-valued attributes we have a special
162
 * "AttrHash<bool>" to pack bits together in words.
163
 */
164
template <>
165
14309
class AttrHash<bool> :
166
    protected std::unordered_map<NodeValue*,
167
                                  uint64_t,
168
                                  AttrBoolHashFunction> {
169
170
  /** A "super" type, like in Java, for easy reference below. */
171
  typedef std::unordered_map<NodeValue*, uint64_t, AttrBoolHashFunction> super;
172
173
  /**
174
   * BitAccessor allows us to return a bit "by reference."  Of course,
175
   * we don't require bit-addressibility supported by the system, we
176
   * do it with a complex type.
177
   */
178
  class BitAccessor {
179
180
    uint64_t& d_word;
181
182
    uint64_t d_bit;
183
184
   public:
185
42561345
    BitAccessor(uint64_t& word, uint64_t bit) : d_word(word), d_bit(bit) {}
186
187
42561345
    BitAccessor& operator=(bool b) {
188
42561345
      if(b) {
189
        // set the bit
190
35662355
        d_word |= GetBitSet(d_bit);
191
      } else {
192
        // clear the bit
193
6898990
        d_word &= ~GetBitSet(d_bit);
194
      }
195
196
42561345
      return *this;
197
    }
198
199
    operator bool() const { return (d_word & GetBitSet(d_bit)) ? true : false; }
200
  };/* class AttrHash<bool>::BitAccessor */
201
202
  /**
203
   * A (somewhat degenerate) iterator over boolean-valued attributes.
204
   * This iterator doesn't support anything except comparison and
205
   * dereference.  It's intended just for the result of find() on the
206
   * table.
207
   */
208
  class BitIterator {
209
210
    std::pair<NodeValue* const, uint64_t>* d_entry;
211
212
    uint64_t d_bit;
213
214
   public:
215
216
    BitIterator() :
217
      d_entry(NULL),
218
      d_bit(0) {
219
    }
220
221
    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, uint64_t bit)
222
        : d_entry(&entry), d_bit(bit)
223
    {
224
    }
225
226
    std::pair<NodeValue* const, BitAccessor> operator*() {
227
      return std::make_pair(d_entry->first,
228
                            BitAccessor(d_entry->second, d_bit));
229
    }
230
231
    bool operator==(const BitIterator& b) {
232
      return d_entry == b.d_entry && d_bit == b.d_bit;
233
    }
234
  };/* class AttrHash<bool>::BitIterator */
235
236
  /**
237
   * A (somewhat degenerate) const_iterator over boolean-valued
238
   * attributes.  This const_iterator doesn't support anything except
239
   * comparison and dereference.  It's intended just for the result of
240
   * find() on the table.
241
   */
242
  class ConstBitIterator {
243
244
    const std::pair<NodeValue* const, uint64_t>* d_entry;
245
246
    uint64_t d_bit;
247
248
   public:
249
250
827804392
    ConstBitIterator() :
251
      d_entry(NULL),
252
827804392
      d_bit(0) {
253
827804392
    }
254
255
774946952
    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
256
                     uint64_t bit)
257
774946952
        : d_entry(&entry), d_bit(bit)
258
    {
259
774946952
    }
260
261
774946952
    std::pair<NodeValue* const, bool> operator*()
262
    {
263
1549893904
      return std::make_pair(
264
2324840856
          d_entry->first, (d_entry->second & GetBitSet(d_bit)) ? true : false);
265
    }
266
267
801375672
    bool operator==(const ConstBitIterator& b) {
268
801375672
      return d_entry == b.d_entry && d_bit == b.d_bit;
269
    }
270
  };/* class AttrHash<bool>::ConstBitIterator */
271
272
public:
273
274
  typedef std::pair<uint64_t, NodeValue*> key_type;
275
  typedef bool data_type;
276
  typedef std::pair<const key_type, data_type> value_type;
277
278
  /** an iterator type; see above for limitations */
279
  typedef BitIterator iterator;
280
  /** a const_iterator type; see above for limitations */
281
  typedef ConstBitIterator const_iterator;
282
283
  /**
284
   * Find the boolean value in the hash table.  Returns something ==
285
   * end() if not found.
286
   */
287
  BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
288
    super::iterator i = super::find(k.second);
289
    if(i == super::end()) {
290
      return BitIterator();
291
    }
292
    /*
293
    Debug.printf("boolattr",
294
                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
295
                 &(*i).second,
296
                 (uint64_t)((*i).second),
297
                 uint64_t(k.first));
298
    */
299
    return BitIterator(*i, k.first);
300
  }
301
302
  /** The "off the end" iterator */
303
  BitIterator end() {
304
    return BitIterator();
305
  }
306
307
  /**
308
   * Find the boolean value in the hash table.  Returns something ==
309
   * end() if not found.
310
   */
311
801375672
  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
312
801375672
    super::const_iterator i = super::find(k.second);
313
801375672
    if(i == super::end()) {
314
26428720
      return ConstBitIterator();
315
    }
316
    /*
317
    Debug.printf("boolattr",
318
                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
319
                 &(*i).second,
320
                 (uint64_t)((*i).second),
321
                 uint64_t(k.first));
322
    */
323
774946952
    return ConstBitIterator(*i, k.first);
324
  }
325
326
  /** The "off the end" const_iterator */
327
801375672
  ConstBitIterator end() const {
328
801375672
    return ConstBitIterator();
329
  }
330
331
  /**
332
   * Access the hash table using the underlying operator[].  Inserts
333
   * the key into the table (associated to default value) if it's not
334
   * already there.
335
   */
336
42561345
  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
337
42561345
    uint64_t& word = super::operator[](k.second);
338
42561345
    return BitAccessor(word, k.first);
339
  }
340
341
  /**
342
   * Delete all flags from the given node.
343
   */
344
29447339
  void erase(NodeValue* nv) {
345
29447339
    super::erase(nv);
346
29447339
  }
347
348
  /**
349
   * Clear the hash table.
350
   */
351
7144
  void clear() {
352
7144
    super::clear();
353
7144
  }
354
355
  /** Is the hash table empty? */
356
  bool empty() const {
357
    return super::empty();
358
  }
359
360
  /** This is currently very misleading! */
361
  size_t size() const {
362
    return super::size();
363
  }
364
};/* class AttrHash<bool> */
365
366
}/* CVC4::expr::attr namespace */
367
368
// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
369
370
namespace attr {
371
372
/**
373
 * This is the last-attribute-assigner.  IDs are not globally
374
 * unique; rather, they are unique for each table_value_type.
375
 */
376
template <class T, bool context_dep>
377
struct LastAttributeId {
378
 public:
379
995945
  static uint64_t getNextId() {
380
995945
    uint64_t* id = raw_id();
381
995945
    const uint64_t next_id = *id;
382
995945
    ++(*id);
383
995945
    return next_id;
384
  }
385
147236701
  static uint64_t getId() {
386
147236701
    return *raw_id();
387
  }
388
 private:
389
148232646
  static uint64_t* raw_id()
390
  {
391
    static uint64_t s_id = 0;
392
148232646
    return &s_id;
393
  }
394
};
395
396
}/* CVC4::expr::attr namespace */
397
398
// ATTRIBUTE DEFINITION ========================================================
399
400
/**
401
 * An "attribute type" structure.
402
 *
403
 * @param T the tag for the attribute kind.
404
 *
405
 * @param value_t the underlying value_type for the attribute kind
406
 *
407
 * @param context_dep whether this attribute kind is
408
 * context-dependent
409
 */
410
template <class T, class value_t, bool context_dep = false>
411
class Attribute
412
{
413
  /**
414
   * The unique ID associated to this attribute.  Assigned statically,
415
   * at load time.
416
   */
417
  static const uint64_t s_id;
418
419
public:
420
421
  /** The value type for this attribute. */
422
  typedef value_t value_type;
423
424
  /** Get the unique ID associated to this attribute. */
425
1738359602
  static inline uint64_t getId() { return s_id; }
426
427
  /**
428
   * This attribute does not have a default value: calling
429
   * hasAttribute() for a Node that hasn't had this attribute set will
430
   * return false, and getAttribute() for the Node will return a
431
   * default-constructed value_type.
432
   */
433
  static const bool has_default_value = false;
434
435
  /**
436
   * Expose this setting to the users of this Attribute kind.
437
   */
438
  static const bool context_dependent = context_dep;
439
440
  /**
441
   * Register this attribute kind and check that the ID is a valid ID
442
   * for bool-valued attributes.  Fail an assert if not.  Otherwise
443
   * return the id.
444
   */
445
658029
  static inline uint64_t registerAttribute() {
446
    typedef typename attr::KindValueToTableValueMapping<value_t>::
447
                     table_value_type table_value_type;
448
658029
    return attr::LastAttributeId<table_value_type, context_dep>::getNextId();
449
  }
450
};/* class Attribute<> */
451
452
/**
453
 * An "attribute type" structure for boolean flags (special).
454
 */
455
template <class T, bool context_dep>
456
class Attribute<T, bool, context_dep>
457
{
458
  /** IDs for bool-valued attributes are actually bit assignments. */
459
  static const uint64_t s_id;
460
461
public:
462
463
  /** The value type for this attribute; here, bool. */
464
  typedef bool value_type;
465
466
  /** Get the unique ID associated to this attribute. */
467
843937017
  static inline uint64_t getId() { return s_id; }
468
469
  /**
470
   * Such bool-valued attributes ("flags") have a default value: they
471
   * are false for all nodes on entry.  Calling hasAttribute() for a
472
   * Node that hasn't had this attribute set will return true, and
473
   * getAttribute() for the Node will return the default_value below.
474
   */
475
  static const bool has_default_value = true;
476
477
  /**
478
   * Default value of the attribute for Nodes without one explicitly
479
   * set.
480
   */
481
  static const bool default_value = false;
482
483
  /**
484
   * Expose this setting to the users of this Attribute kind.
485
   */
486
  static const bool context_dependent = context_dep;
487
488
  /**
489
   * Register this attribute kind and check that the ID is a valid ID
490
   * for bool-valued attributes.  Fail an assert if not.  Otherwise
491
   * return the id.
492
   */
493
337916
  static inline uint64_t registerAttribute() {
494
337916
    const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId();
495
337916
    AlwaysAssert(id <= 63) << "Too many boolean node attributes registered "
496
                              "during initialization !";
497
337916
    return id;
498
  }
499
};/* class Attribute<..., bool, ...> */
500
501
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
502
503
/** Assign unique IDs to attributes at load time. */
504
template <class T, class value_t, bool context_dep>
505
1191579
const uint64_t Attribute<T, value_t, context_dep>::s_id =
506
658029
    Attribute<T, value_t,  context_dep>::registerAttribute();
507
508
509
/** Assign unique IDs to attributes at load time. */
510
template <class T, bool context_dep>
511
640257
const uint64_t Attribute<T, bool, context_dep>::s_id =
512
337916
    Attribute<T, bool, context_dep>::registerAttribute();
513
514
}/* CVC4::expr namespace */
515
}/* CVC4 namespace */
516
517
#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */