001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package escjava.translate;
004    
005    /** This class provides an interface through which one can create a
006      * unique ID for given references.  It is used by ESC/Java to associate
007      * more information with a given asserted condition.
008      **/
009    
010    import javafe.util.Assert;
011    
012    public class AuxInfo {
013      
014      /** Initializes the data structures, clearing any previous information
015        * of which IDs have been used.  This method should be called before
016        * any other in this class.  The method may also free and null out
017        * certain structures, aiming to help the garbage collector.
018        **/
019      
020      public static void reset() {
021        // drop all but the first buffer
022        AuxInfoLink d = first;
023        while (d != null) {
024          d = d.clean();
025        }
026        last = first;
027        n = 0;
028        usedInLast = 0;
029      }
030    
031      /** Creates and returns an ID for the reference <code>o</code>.
032        * The returned ID has not been returned since the last call to
033        * <code>reset</code>, even if this method has been called for
034        * the same <code>o</code> since then.
035        **/
036    
037      //@ ensures 0 <= \result;
038      public static int put(/*@ non_null */ Object o) {
039        if (usedInLast == AuxInfoLink.LINK_BUFFER_SIZE) {
040          last.next = new AuxInfoLink();
041          last = last.next;
042          usedInLast = 0;
043        }
044        //@ assert usedInLast < AuxInfoLink.LINK_BUFFER_SIZE;
045        int id = n;
046        last.a[usedInLast] = o;
047        usedInLast++;
048        n++;
049        return id;
050      }
051    
052      /** Returns the reference associated with <code>id</code>, as returned
053        * by <code>put</code> since the last call to <code>reset</code>
054        * It is assumed that <code>id</code> has indeed been returned by
055        * <code>put</code> since the last call to <code>reset</code>.
056        **/
057      
058      //@ requires 0 <= id;
059      //@ ensures \result != null;
060      public static Object get(int id) {
061        // first find containing buffer
062        AuxInfoLink d = first;
063        //@ loop_invariant d != null;
064        //@ loop_invariant 0 <= id;
065        while (AuxInfoLink.LINK_BUFFER_SIZE <= id) {
066          //@ assume d.next != null;
067          d = d.next;
068          id -= AuxInfoLink.LINK_BUFFER_SIZE;
069        }
070        Object o = d.a[id];
071        // Assert.notNull(o); this assert does fail!
072        //@ assume o != null;
073        return o;
074      }
075    
076      private static /*@ non_null */ AuxInfoLink first = new AuxInfoLink();
077      private static /*@ non_null */ AuxInfoLink last = first;
078      //@ private invariant last.next == null;
079    
080      /*@ spec_public */
081      private static int n = 0;
082      //@ invariant 0 <= n;
083    
084      /*@ spec_public */
085      private static int usedInLast = 0;
086      //@ invariant 0 <= usedInLast && usedInLast <= AuxInfoLink.LINK_BUFFER_SIZE;
087      //@ invariant usedInLast <= n;
088    }
089    
090    class AuxInfoLink {
091      static final int LINK_BUFFER_SIZE = 1024;
092      /*@ non_null */ Object[] a = new Object[LINK_BUFFER_SIZE];
093      //@ invariant a.length == LINK_BUFFER_SIZE;
094      //@ invariant \typeof(a) == \type(Object[]);
095      AuxInfoLink next = null;
096    
097      //@ modifies this.next;
098      //@ ensures \result == \old(this.next);
099      //@ ensures this.next == null;
100      AuxInfoLink clean() {
101        // try to help garbage collector
102        for (int i = 0; i < a.length; i++) {
103          a[i] = null;
104        }
105        AuxInfoLink n = next;
106        next = null;
107        return n;
108      }
109    
110      //@ ensures next == null;
111      AuxInfoLink() {
112      }
113    }