CVC3

cdflags.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cdflags.cpp
00004  *\brief Implementation for CDFlags class
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Jan 26 16:53:28 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  *
00017  * <hr>
00018  *
00019  */
00020 /*****************************************************************************/
00021 
00022 
00023 #include "cdflags.h"
00024 #include "memory_manager_context.h"
00025 
00026 
00027 using namespace CVC3;
00028 using namespace std;
00029 
00030 
00031 void CDFlags::update(unsigned mask, int scope, bool setMask)
00032 {
00033   DebugAssert(mask && (mask & (mask-1)) == 0, "Expected single bit mask");
00034   if (scope < 0 || d_scope->level() <= scope) {
00035     makeCurrent(scope);
00036     if (setMask) d_flags = d_flags | mask;
00037     else d_flags = d_flags & ~mask;
00038   }
00039   else {
00040     // Kind of ugly: have to "change the past", but that's the price we pay for
00041     // keeping all the flags in one word for efficiency.
00042     IF_DEBUG(bool on = (d_flags & mask) != 0;)
00043 
00044     // Update current object
00045     if (setMask) d_flags = d_flags | mask;
00046     else d_flags = d_flags & ~mask;
00047 
00048     ContextObjChain** lastPtr = &d_restore;
00049     CDFlags* pastFlags;
00050     Scope* lastScope = d_scope;
00051     bool done = false;
00052 
00053     // Update past objects
00054     while (true) {
00055       pastFlags = (CDFlags*)((*lastPtr)->d_data);
00056       DebugAssert(pastFlags != NULL, "expected non-NULL data");
00057       if (pastFlags->d_scope->level() >= scope) {
00058         DebugAssert((on && (pastFlags->d_flags & mask))
00059              || (!on && !(pastFlags->d_flags & mask)),
00060                     "Expected no change in flag since scope");
00061         if (setMask) {
00062           pastFlags->d_flags = pastFlags->d_flags | mask;
00063         }
00064         else {
00065           pastFlags->d_flags = pastFlags->d_flags & ~mask;
00066         }
00067         if (pastFlags->d_scope->level() == scope) {
00068           done = true; break;
00069         }
00070         lastScope = pastFlags->d_scope;
00071       } else break;
00072       lastPtr = &((*lastPtr)->d_restore);
00073       DebugAssert(*lastPtr != NULL, "Should always be object at scope 0");
00074     }
00075     if (done) return;
00076 
00077     // No past object exists at the target scope: create one
00078     DebugAssert(lastScope != NULL &&
00079                 lastScope->level() > scope,
00080                 "Expected lastScope to be above target scope");
00081     while (lastScope->level() > scope) lastScope = lastScope->prevScope();
00082 
00083     ContextObj* data = pastFlags->makeCopy(lastScope->getCMM());
00084 
00085     pastFlags->d_scope = lastScope;
00086 
00087     ContextObjChain* obj = new(lastScope->getCMM())
00088       ContextObjChain(data, this, (*lastPtr)->d_restore);
00089     (*lastPtr)->d_restore = obj;
00090     lastScope->addToChain(obj);
00091 
00092     // Update newly created past object
00093     if (setMask) {
00094       pastFlags->d_flags = pastFlags->d_flags | mask;
00095     }
00096     else {
00097       pastFlags->d_flags = pastFlags->d_flags & ~mask;
00098     }
00099   }
00100 }