src/expr/node_manager.cpp

   1 /*********************                                                        */
   2 /** node_manager.cpp
   3  ** Original author: mdeters
   4  ** Major contributors: dejan
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Expression manager implementation.
  14  **/
  15
  16 #include "node_manager.h"
  17
  18 #include <ext/hash_set>
  19
  20 using namespace std;
  21 using namespace CVC4::expr;
  22 using __gnu_cxx::hash_set;
  23
  24 namespace CVC4 {
  25
  26 __thread NodeManager* NodeManager::s_current = 0;
  27
  28 NodeManager::NodeManager(context::Context* ctxt) :
  29   d_attrManager(ctxt),
  30   d_nodeUnderDeletion(NULL),
  31   d_reclaiming(false) {
  32   poolInsert( &expr::NodeValue::s_null );
  33
  34   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
  35     Kind k = Kind(i);
  36
  37     if(hasOperator(k)) {
  38       d_operators[i] = mkConst(Kind(k));
  39     }
  40   }
  41 }
  42
  43 NodeManager::~NodeManager() {
  44   // have to ensure "this" is the current NodeManager during
  45   // destruction of operators, because they get GCed.
  46
  47   NodeManagerScope nms(this);
  48
  49   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
  50     d_operators[i] = Node::null();
  51   }
  52
  53   while(!d_zombies.empty()) {
  54     reclaimZombies();
  55   }
  56
  57   poolRemove( &expr::NodeValue::s_null );
  58 }
  59
  60 /**
  61  * This class ensure that NodeManager::d_reclaiming gets set to false
  62  * even on exceptional exit from NodeManager::reclaimZombies().
  63  */
  64 struct Reclaim {
  65   bool& d_reclaimField;
  66   Reclaim(bool& reclaim) :
  67     d_reclaimField(reclaim) {
  68
  69     Debug("gc") << ">> setting RECLAIM field\n";
  70     d_reclaimField = true;
  71   }
  72   ~Reclaim() {
  73     Debug("gc") << "<< clearing RECLAIM field\n";
  74     d_reclaimField = false;
  75   }
  76 };
  77
  78 struct NVReclaim {
  79   NodeValue*& d_reclaimField;
  80   NVReclaim(NodeValue*& reclaim) :
  81     d_reclaimField(reclaim) {
  82
  83     Debug("gc") << ">> setting NVRECLAIM field\n";
  84   }
  85   ~NVReclaim() {
  86     Debug("gc") << "<< clearing NVRECLAIM field\n";
  87     d_reclaimField = NULL;
  88   }
  89 };
  90
  91 void NodeManager::reclaimZombies() {
  92   // FIXME multithreading
  93
  94   Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
  95
  96   // during reclamation, reclaimZombies() is never supposed to be called
  97   Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
  98
  99   // whether exit is normal or exceptional, the Reclaim dtor is called
 100   // and ensures that d_reclaiming is set back to false.
 101   Reclaim r(d_reclaiming);
 102
 103   // We copy the set away and clear the NodeManager's set of zombies.
 104   // This is because reclaimZombie() decrements the RC of the
 105   // NodeValue's children, which may (recursively) reclaim them.
 106   //
 107   // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
 108   // then becomes a zombie (NodeManager::gc(B) is called).
 109   //
 110   // One way to handle B's zombification is simply to put it into
 111   // d_zombies.  This is what we do.  However, if we're currently
 112   // processing d_zombies in the loop below, such addition may be
 113   // invisible to us (B is leaked) or even invalidate our iterator,
 114   // causing a crash.
 115
 116   vector<NodeValue*> zombies;
 117   zombies.reserve(d_zombies.size());
 118   std::copy(d_zombies.begin(),
 119             d_zombies.end(),
 120             std::back_inserter(zombies));
 121   d_zombies.clear();
 122
 123   for(vector<NodeValue*>::iterator i = zombies.begin();
 124       i != zombies.end();
 125       ++i) {
 126     NodeValue* nv = *i;
 127
 128     // collect ONLY IF still zero
 129     if(nv->d_rc == 0) {
 130       Debug("gc") << "deleting node value " << nv
 131                   << " [" << nv->d_id << "]: " << *nv << "\n";
 132
 133       // remove from the pool
 134       if(nv->getKind() != kind::VARIABLE) {
 135         poolRemove(nv);
 136       }
 137
 138       // whether exit is normal or exceptional, the NVReclaim dtor is
 139       // called and ensures that d_nodeUnderDeletion is set back to
 140       // NULL.
 141       NVReclaim rc(d_nodeUnderDeletion);
 142       d_nodeUnderDeletion = nv;
 143
 144       // remove attributes
 145       d_attrManager.deleteAllAttributes(nv);
 146
 147       // decr ref counts of children
 148       nv->decrRefCounts();
 149       free(nv);
 150     }
 151   }
 152 }
 153
 154 }/* CVC4 namespace */