GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/attribute.h Lines: 95 125 76.0 %
Date: 2021-03-22 Branches: 567 1213 46.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file attribute.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Dejan Jovanovic
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.
13
 **
14
 ** Node attributes.
15
 **/
16
17
#include "cvc4_private.h"
18
19
/* There are strong constraints on ordering of declarations of
20
 * attributes and nodes due to template use */
21
#include "expr/node.h"
22
#include "expr/type_node.h"
23
24
#ifndef CVC4__EXPR__ATTRIBUTE_H
25
#define CVC4__EXPR__ATTRIBUTE_H
26
27
#include <string>
28
#include "expr/attribute_unique_id.h"
29
30
// include supporting templates
31
#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
32
#include "expr/attribute_internals.h"
33
#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
34
35
namespace CVC4 {
36
namespace expr {
37
namespace attr {
38
39
/**
40
 * Attributes are roughly speaking [almost] global hash tables from Nodes
41
 * (TNodes) to data. Attributes can be thought of as additional fields used to
42
 * extend NodeValues. Attributes are mutable and come in both sat
43
 * context-dependent and non-context dependent varieties. Attributes live only
44
 * as long as the node itself does. If a Node is garbage-collected, Attributes
45
 * associated with it will automatically be garbage collected. (Being in the
46
 * domain of an Attribute does not increase a Node's reference count.) To
47
 * achieve this special relationship with Nodes, Attributes are mapped by hash
48
 * tables (AttrHash<> and CDAttrHash<>) that live in the AttributeManager. The
49
 * AttributeManager is owned by the NodeManager.
50
 *
51
 * Example:
52
 *
53
 * Attributes tend to be defined in a fixed pattern:
54
 *
55
 * ```
56
 * struct InstLevelAttributeId {};
57
 * typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute;
58
 * ```
59
 *
60
 * To get the value of an Attribute InstLevelAttribute on a Node n, use
61
 * ```
62
 * n.getAttribute(InstLevelAttribute());
63
 * ```
64
 *
65
 * To check whether the attribute has been set:
66
 * ```
67
 * n.hasAttribute(InstLevelAttribute());
68
 * ```
69
 *
70
 * To separate Attributes of the same type in the same table, each of the
71
 * structures `struct InstLevelAttributeId {};` is given a different unique value
72
 * at load time. An example is the empty struct InstLevelAttributeId. These
73
 * should be unique for each Attribute. Then via some template messiness when
74
 * InstLevelAttribute() is passed as the argument to getAttribute(...) the load
75
 * time id is instantiated.
76
 */
77
// ATTRIBUTE MANAGER ===========================================================
78
79
/**
80
 * A container for the main attribute tables of the system.  There's a
81
 * one-to-one NodeManager : AttributeManager correspondence.
82
 */
83
7144
class AttributeManager {
84
85
  template <class T>
86
  void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
87
88
  template <class T>
89
  void deleteAllFromTable(AttrHash<T>& table);
90
91
  template <class T>
92
  void deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids);
93
94
  template <class T>
95
  void reconstructTable(AttrHash<T>& table);
96
97
  /**
98
   * getTable<> is a helper template that gets the right table from an
99
   * AttributeManager given its type.
100
   */
101
  template <class T, bool context_dep, class Enable>
102
  friend struct getTable;
103
104
  bool d_inGarbageCollection;
105
106
  void clearDeleteAllAttributesBuffer();
107
108
public:
109
110
  /** Construct an attribute manager. */
111
  AttributeManager();
112
113
  // IF YOU ADD ANY TABLES, don't forget to add them also to the
114
  // implementation of deleteAllAttributes().
115
116
  /** Underlying hash table for boolean-valued attributes */
117
  AttrHash<bool> d_bools;
118
  /** Underlying hash table for integral-valued attributes */
119
  AttrHash<uint64_t> d_ints;
120
  /** Underlying hash table for node-valued attributes */
121
  AttrHash<TNode> d_tnodes;
122
  /** Underlying hash table for node-valued attributes */
123
  AttrHash<Node> d_nodes;
124
  /** Underlying hash table for types attributes */
125
  AttrHash<TypeNode> d_types;
126
  /** Underlying hash table for string-valued attributes */
127
  AttrHash<std::string> d_strings;
128
129
  /**
130
   * Get a particular attribute on a particular node.
131
   *
132
   * @param nv the node about which to inquire
133
   * @param attr the attribute kind to get
134
   * @return the attribute value, if set, or a default-constructed
135
   * AttrKind::value_type if not.
136
   */
137
  template <class AttrKind>
138
  typename AttrKind::value_type getAttribute(NodeValue* nv,
139
                                             const AttrKind& attr) const;
140
141
  /**
142
   * Determine if a particular attribute exists for a particular node.
143
   *
144
   * @param nv the node about which to inquire
145
   * @param attr the attribute kind to inquire about
146
   * @return true if the given node has the given attribute
147
   */
148
  template <class AttrKind>
149
  bool hasAttribute(NodeValue* nv,
150
                    const AttrKind& attr) const;
151
152
  /**
153
   * Determine if a particular attribute exists for a particular node,
154
   * and get it if it does.
155
   *
156
   * @param nv the node about which to inquire
157
   * @param attr the attribute kind to inquire about
158
   * @param ret a pointer to a return value, set in case the node has
159
   * the attribute
160
   * @return true if the given node has the given attribute
161
   */
162
  template <class AttrKind>
163
  bool getAttribute(NodeValue* nv,
164
                    const AttrKind& attr,
165
                    typename AttrKind::value_type& ret) const;
166
167
  /**
168
   * Set a particular attribute on a particular node.
169
   *
170
   * @param nv the node for which to set the attribute
171
   * @param attr the attribute kind to set
172
   * @param value a pointer to a return value, set in case the node has
173
   * the attribute
174
   * @return true if the given node has the given attribute
175
   */
176
  template <class AttrKind>
177
  void setAttribute(NodeValue* nv,
178
                    const AttrKind& attr,
179
                    const typename AttrKind::value_type& value);
180
181
  /**
182
   * Remove all attributes associated to the given node.
183
   *
184
   * @param nv the node from which to delete attributes
185
   */
186
  void deleteAllAttributes(NodeValue* nv);
187
188
  /**
189
   * Remove all attributes from the tables.
190
   */
191
  void deleteAllAttributes();
192
193
  /**
194
   * Returns true if a table is currently being deleted.
195
   */
196
  bool inGarbageCollection() const ;
197
198
  /**
199
   * Determines the AttrTableId of an attribute.
200
   *
201
   * @param attr the attribute
202
   * @return the id of the attribute table.
203
   */
204
  template <class AttrKind>
205
  static AttributeUniqueId getAttributeId(const AttrKind& attr);
206
207
  /** A list of attributes. */
208
  typedef std::vector< const AttributeUniqueId* > AttrIdVec;
209
210
  /** Deletes a list of attributes. */
211
  void deleteAttributes(const AttrIdVec& attributeIds);
212
213
  /**
214
   * debugHook() is an empty function for the purpose of debugging
215
   * the AttributeManager without recompiling all of CVC4.
216
   * Formally this is a nop.
217
   */
218
  void debugHook(int debugFlag);
219
};
220
221
}/* CVC4::expr::attr namespace */
222
223
// MAPPING OF ATTRIBUTE KINDS TO TABLES IN THE ATTRIBUTE MANAGER ===============
224
225
namespace attr {
226
227
/**
228
 * The getTable<> template provides (static) access to the
229
 * AttributeManager field holding the table.
230
 *
231
 * The `Enable` template parameter is used to instantiate the template
232
 * conditionally: If the template substitution of Enable fails (e.g. when using
233
 * `std::enable_if` in the template parameter and the condition is false), the
234
 * instantiation is ignored due to the SFINAE rule.
235
 */
236
template <class T, bool context_dep, class Enable = void>
237
struct getTable;
238
239
/** Access the "d_bools" member of AttributeManager. */
240
template <>
241
struct getTable<bool, false> {
242
  static const AttrTableId id = AttrTableBool;
243
  typedef AttrHash<bool> table_type;
244
42561345
  static inline table_type& get(AttributeManager& am) {
245
42561345
    return am.d_bools;
246
  }
247
801375672
  static inline const table_type& get(const AttributeManager& am) {
248
801375672
    return am.d_bools;
249
  }
250
};
251
252
/** Access the "d_ints" member of AttributeManager. */
253
template <class T>
254
struct getTable<T,
255
                false,
256
                // Use this specialization only for unsigned integers
257
                typename std::enable_if<std::is_unsigned<T>::value>::type>
258
{
259
  static const AttrTableId id = AttrTableUInt64;
260
  typedef AttrHash<uint64_t> table_type;
261
167878
  static inline table_type& get(AttributeManager& am) {
262
167878
    return am.d_ints;
263
  }
264
11198590
  static inline const table_type& get(const AttributeManager& am) {
265
11198590
    return am.d_ints;
266
  }
267
};
268
269
/** Access the "d_tnodes" member of AttributeManager. */
270
template <>
271
struct getTable<TNode, false> {
272
  static const AttrTableId id = AttrTableTNode;
273
  typedef AttrHash<TNode> table_type;
274
2
  static inline table_type& get(AttributeManager& am) {
275
2
    return am.d_tnodes;
276
  }
277
4
  static inline const table_type& get(const AttributeManager& am) {
278
4
    return am.d_tnodes;
279
  }
280
};
281
282
/** Access the "d_nodes" member of AttributeManager. */
283
template <>
284
struct getTable<Node, false> {
285
  static const AttrTableId id = AttrTableNode;
286
  typedef AttrHash<Node> table_type;
287
24195988
  static inline table_type& get(AttributeManager& am) {
288
24195988
    return am.d_nodes;
289
  }
290
255448514
  static inline const table_type& get(const AttributeManager& am) {
291
255448514
    return am.d_nodes;
292
  }
293
};
294
295
/** Access the "d_types" member of AttributeManager. */
296
template <>
297
struct getTable<TypeNode, false> {
298
  static const AttrTableId id = AttrTableTypeNode;
299
  typedef AttrHash<TypeNode> table_type;
300
27337916
  static inline table_type& get(AttributeManager& am) {
301
27337916
    return am.d_types;
302
  }
303
1418125268
  static inline const table_type& get(const AttributeManager& am) {
304
1418125268
    return am.d_types;
305
  }
306
};
307
308
/** Access the "d_strings" member of AttributeManager. */
309
template <>
310
struct getTable<std::string, false> {
311
  static const AttrTableId id = AttrTableString;
312
  typedef AttrHash<std::string> table_type;
313
876178
  static inline table_type& get(AttributeManager& am) {
314
876178
    return am.d_strings;
315
  }
316
1009264
  static inline const table_type& get(const AttributeManager& am) {
317
1009264
    return am.d_strings;
318
  }
319
};
320
321
}/* CVC4::expr::attr namespace */
322
323
// ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
324
325
namespace attr {
326
327
// implementation for AttributeManager::getAttribute()
328
template <class AttrKind>
329
typename AttrKind::value_type
330
821504752
AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
331
  typedef typename AttrKind::value_type value_type;
332
  typedef KindValueToTableValueMapping<value_type> mapping;
333
  typedef typename getTable<value_type, AttrKind::context_dependent>::
334
            table_type table_type;
335
336
821504752
  const table_type& ah =
337
    getTable<value_type, AttrKind::context_dependent>::get(*this);
338
841633876
  typename table_type::const_iterator i =
339
1643009504
    ah.find(std::make_pair(AttrKind::getId(), nv));
340
341
821504752
  if(i == ah.end()) {
342
26432606
    return typename AttrKind::value_type();
343
  }
344
345
795072146
  return mapping::convertBack((*i).second);
346
}
347
348
/* Helper template class for hasAttribute(), specialized based on
349
 * whether AttrKind has a "default value" that all Nodes implicitly
350
 * have or not. */
351
template <bool has_default, class AttrKind>
352
struct HasAttribute;
353
354
/**
355
 * Specialization of HasAttribute<> helper template for AttrKinds
356
 * with a default value.
357
 */
358
template <class AttrKind>
359
struct HasAttribute<true, AttrKind> {
360
  /** This implementation is simple; it's always true. */
361
40
  static inline bool hasAttribute(const AttributeManager* am,
362
                                  NodeValue* nv) {
363
40
    return true;
364
  }
365
366
  /**
367
   * This implementation returns the AttrKind's default value if the
368
   * Node doesn't have the given attribute.
369
   */
370
44
  static inline bool getAttribute(const AttributeManager* am,
371
                                  NodeValue* nv,
372
                                  typename AttrKind::value_type& ret) {
373
    typedef typename AttrKind::value_type value_type;
374
    typedef KindValueToTableValueMapping<value_type> mapping;
375
    typedef typename getTable<value_type,
376
                              AttrKind::context_dependent>::table_type
377
      table_type;
378
379
44
    const table_type& ah =
380
      getTable<value_type, AttrKind::context_dependent>::get(*am);
381
44
    typename table_type::const_iterator i =
382
88
      ah.find(std::make_pair(AttrKind::getId(), nv));
383
384
44
    if(i == ah.end()) {
385
      ret = AttrKind::default_value;
386
    } else {
387
44
      ret = mapping::convertBack((*i).second);
388
    }
389
390
44
    return true;
391
  }
392
};
393
394
/**
395
 * Specialization of HasAttribute<> helper template for AttrKinds
396
 * without a default value.
397
 */
398
template <class AttrKind>
399
struct HasAttribute<false, AttrKind> {
400
873439892
  static inline bool hasAttribute(const AttributeManager* am,
401
                                  NodeValue* nv) {
402
    typedef typename AttrKind::value_type value_type;
403
    //typedef KindValueToTableValueMapping<value_type> mapping;
404
    typedef typename getTable<value_type, AttrKind::context_dependent>::
405
              table_type table_type;
406
407
873439892
    const table_type& ah =
408
      getTable<value_type, AttrKind::context_dependent>::get(*am);
409
1746879784
    typename table_type::const_iterator i =
410
1746879784
      ah.find(std::make_pair(AttrKind::getId(), nv));
411
412
873439892
    if(i == ah.end()) {
413
63023385
      return false;
414
    }
415
416
810416507
    return true;
417
  }
418
419
792212624
  static inline bool getAttribute(const AttributeManager* am,
420
                                  NodeValue* nv,
421
                                  typename AttrKind::value_type& ret) {
422
    typedef typename AttrKind::value_type value_type;
423
    typedef KindValueToTableValueMapping<value_type> mapping;
424
    typedef typename getTable<value_type, AttrKind::context_dependent>::
425
              table_type table_type;
426
427
792212624
    const table_type& ah =
428
      getTable<value_type, AttrKind::context_dependent>::get(*am);
429
1584425248
    typename table_type::const_iterator i =
430
1584425248
      ah.find(std::make_pair(AttrKind::getId(), nv));
431
432
792212624
    if(i == ah.end()) {
433
26367023
      return false;
434
    }
435
436
765845601
    ret = mapping::convertBack((*i).second);
437
438
765845601
    return true;
439
  }
440
};
441
442
template <class AttrKind>
443
873439932
bool AttributeManager::hasAttribute(NodeValue* nv,
444
                                    const AttrKind&) const {
445
  return HasAttribute<AttrKind::has_default_value, AttrKind>::
446
873439932
           hasAttribute(this, nv);
447
}
448
449
template <class AttrKind>
450
792212668
bool AttributeManager::getAttribute(NodeValue* nv,
451
                                    const AttrKind&,
452
                                    typename AttrKind::value_type& ret) const {
453
  return HasAttribute<AttrKind::has_default_value, AttrKind>::
454
792212668
           getAttribute(this, nv, ret);
455
}
456
457
template <class AttrKind>
458
inline void
459
95139307
AttributeManager::setAttribute(NodeValue* nv,
460
                               const AttrKind&,
461
                               const typename AttrKind::value_type& value) {
462
  typedef typename AttrKind::value_type value_type;
463
  typedef KindValueToTableValueMapping<value_type> mapping;
464
  typedef typename getTable<value_type, AttrKind::context_dependent>::
465
            table_type table_type;
466
467
95139307
  table_type& ah =
468
      getTable<value_type, AttrKind::context_dependent>::get(*this);
469
95139307
  ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
470
95139307
}
471
472
/** Search for the NodeValue in all attribute tables and remove it. */
473
template <class T>
474
147236695
inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
475
                                              NodeValue* nv) {
476
  // This cannot use nv as anything other than a pointer!
477
147236695
  const uint64_t last = attr::LastAttributeId<T, false>::getId();
478
2326348499
  for (uint64_t id = 0; id < last; ++id)
479
  {
480
4358223608
    table.erase(std::make_pair(id, nv));
481
  }
482
147236695
}
483
484
/** Remove all attributes from the table. */
485
template <class T>
486
35720
inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
487
35720
  Assert(!d_inGarbageCollection);
488
35720
  d_inGarbageCollection = true;
489
35720
  table.clear();
490
35720
  d_inGarbageCollection = false;
491
35720
  Assert(!d_inGarbageCollection);
492
35720
}
493
494
template <class AttrKind>
495
AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
496
  typedef typename AttrKind::value_type value_type;
497
  AttrTableId tableId = getTable<value_type,
498
                                 AttrKind::context_dependent>::id;
499
  return AttributeUniqueId(tableId, attr.getId());
500
}
501
502
template <class T>
503
void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
504
  d_inGarbageCollection = true;
505
  typedef AttrHash<T> hash_t;
506
507
  typename hash_t::iterator it = table.begin();
508
  typename hash_t::iterator tmp;
509
  typename hash_t::iterator it_end = table.end();
510
511
  std::vector<uint64_t>::const_iterator begin_ids = ids.begin();
512
  std::vector<uint64_t>::const_iterator end_ids = ids.end();
513
514
  size_t initialSize = table.size();
515
  while (it != it_end){
516
    uint64_t id = (*it).first.first;
517
518
    if(std::binary_search(begin_ids, end_ids, id)){
519
      tmp = it;
520
      ++it;
521
      table.erase(tmp);
522
    }else{
523
      ++it;
524
    }
525
  }
526
  d_inGarbageCollection = false;
527
  static const size_t ReconstructShrinkRatio = 8;
528
  if(initialSize/ReconstructShrinkRatio > table.size()){
529
    reconstructTable(table);
530
  }
531
}
532
533
template <class T>
534
void AttributeManager::reconstructTable(AttrHash<T>& table){
535
  d_inGarbageCollection = true;
536
  typedef AttrHash<T> hash_t;
537
  hash_t cpy;
538
  cpy.insert(table.begin(), table.end());
539
  cpy.swap(table);
540
  d_inGarbageCollection = false;
541
}
542
543
544
}/* CVC4::expr::attr namespace */
545
}/* CVC4::expr namespace */
546
547
template <class AttrKind>
548
inline typename AttrKind::value_type
549
13335502
NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
550
13335502
  return d_attrManager->getAttribute(nv, AttrKind());
551
}
552
553
template <class AttrKind>
554
702750
inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
555
                                      const AttrKind&) const {
556
702750
  return d_attrManager->hasAttribute(nv, AttrKind());
557
}
558
559
template <class AttrKind>
560
inline bool
561
NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
562
                          typename AttrKind::value_type& ret) const {
563
  return d_attrManager->getAttribute(nv, AttrKind(), ret);
564
}
565
566
template <class AttrKind>
567
inline void
568
52486
NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
569
                          const typename AttrKind::value_type& value) {
570
52486
  d_attrManager->setAttribute(nv, AttrKind(), value);
571
52486
}
572
573
template <class AttrKind>
574
inline typename AttrKind::value_type
575
808169250
NodeManager::getAttribute(TNode n, const AttrKind&) const {
576
808169250
  return d_attrManager->getAttribute(n.d_nv, AttrKind());
577
}
578
579
template <class AttrKind>
580
inline bool
581
872737182
NodeManager::hasAttribute(TNode n, const AttrKind&) const {
582
872737182
  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
583
}
584
585
template <class AttrKind>
586
inline bool
587
792212668
NodeManager::getAttribute(TNode n, const AttrKind&,
588
                          typename AttrKind::value_type& ret) const {
589
792212668
  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
590
}
591
592
template <class AttrKind>
593
inline void
594
95077661
NodeManager::setAttribute(TNode n, const AttrKind&,
595
                          const typename AttrKind::value_type& value) {
596
95077661
  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
597
95077661
}
598
599
template <class AttrKind>
600
inline typename AttrKind::value_type
601
NodeManager::getAttribute(TypeNode n, const AttrKind&) const {
602
  return d_attrManager->getAttribute(n.d_nv, AttrKind());
603
}
604
605
template <class AttrKind>
606
inline bool
607
NodeManager::hasAttribute(TypeNode n, const AttrKind&) const {
608
  return d_attrManager->hasAttribute(n.d_nv, AttrKind());
609
}
610
611
template <class AttrKind>
612
inline bool
613
NodeManager::getAttribute(TypeNode n, const AttrKind&,
614
                          typename AttrKind::value_type& ret) const {
615
  return d_attrManager->getAttribute(n.d_nv, AttrKind(), ret);
616
}
617
618
template <class AttrKind>
619
inline void
620
9160
NodeManager::setAttribute(TypeNode n, const AttrKind&,
621
                          const typename AttrKind::value_type& value) {
622
9160
  d_attrManager->setAttribute(n.d_nv, AttrKind(), value);
623
9160
}
624
625
}/* CVC4 namespace */
626
627
#endif /* CVC4__EXPR__ATTRIBUTE_H */