    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    }