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 }