001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.parser; 004 005 import java.io.IOException; 006 import javafe.util.CorrelatedReader; 007 import javafe.util.FilterCorrelatedReader; 008 import javafe.util.Assert; 009 010 /** 011 * This {@link FilterCorrelatedReader} creates the illusion that the 012 * additional \@-signs, etc. allowed in the JML annotation syntax are 013 * really just whitespace. 014 * 015 * @see javafe.util.FilterCorrelatedReader 016 * @author Rustan Leino 017 */ 018 019 public class JmlCorrelatedReader extends FilterCorrelatedReader 020 { 021 // Comment classifiers. 022 023 public static final int EOL_COMMENT = 0; 024 public static final int C_COMMENT = 1; 025 public static final int JAVADOC_COMMENT = 2; 026 public static final int COMMENTS_KINDS = 3; 027 028 /** 029 * Constructs a <code>JmlCorrelatedReader</code> with 030 * <code>child</code> as the underlying {@link CorrelatedReader}. 031 * After calling this constructor, the caller should no longer use 032 * <code>child</code> directly. 033 * 034 * <p> <code>commentKind</code> is {@link #EOL_COMMENT} to indicate 035 * a slash-slash comment, {@link #C_COMMENT} to indicate an ordinary 036 * slash-star comment, and {@link #JAVADOC_COMMENT} to indicate that 037 * the portion to be read resides inside a (pair of tags in a) 038 * Javadoc comment. 039 */ 040 041 //@ requires 0 <= commentKind && commentKind < COMMENTS_KINDS; 042 protected JmlCorrelatedReader(/*@ non_null */ CorrelatedReader child, 043 int commentKind) { 044 super(child); 045 switch (commentKind) { 046 case EOL_COMMENT: 047 prefixMode = 2; // disallow initial @-signs 048 specialCharacter = '@'; 049 allowSpecialSuffix = false; 050 break; 051 case C_COMMENT: 052 specialCharacter = '@'; 053 allowSpecialSuffix = true; 054 break; 055 default: 056 Assert.precondition("invalidate value for commentKind"); 057 // fall-through (to please compiler) 058 case JAVADOC_COMMENT: 059 specialCharacter = '*'; 060 allowSpecialSuffix = false; 061 break; 062 } 063 } 064 065 066 // Reading and filtering 067 068 /** 069 * The lines of the input consist of (0) a number of whitespace 070 * characters, (1) a number of special characters ('@' in ordinary 071 * comments and '*' inside Javadoc comments), and followed by (2) 072 * the "real meat". The variable <code>prefixMode</code> indicates 073 * which of these three segments are currently being scanned. 074 */ 075 076 //@ spec_public 077 private int prefixMode = 1; /* 0-whitespace, 1-special, 2-meat */ 078 //@ invariant 0 <= prefixMode && prefixMode < 3; 079 080 /** Indicates the special character. */ 081 082 //@ spec_public 083 private final int specialCharacter; 084 085 /** 086 * This variable is included so that @-signs at the end of a 087 * pragma-containing comment can be ignored. In particular, it 088 * counts the number of characters read but not reported. These 089 * characters will be a number of @-signs followed by one more 090 * character (or -1, if at end-of-pragma). @-signs that immediately 091 * follow the first whitespace characters on a line are always 092 * "reported" (since these are actually reported as spaces anyway). 093 * In the steady state of this correlated reader, {@link 094 * #unreturnedChars} is non-zero only when {@link 095 * #lastUnreturnedChar} is not an @-sign. 096 * 097 * <p> unreturnedChars is not used (actually, is 0) when 098 * scanning Javadoc comments. 099 */ 100 101 //@ spec_public 102 private int unreturnedChars = 0; 103 //@ invariant 0 <= unreturnedChars; 104 //@ invariant prefixMode < 2 ==> unreturnedChars == 0; 105 //@ invariant specialCharacter != '@' ==> unreturnedChars == 0; 106 107 /** 108 * If there are unreturned characters, lastUnreturnedChar 109 * indicates the last of these characters. 110 */ 111 112 //@ spec_public 113 private int lastUnreturnedChar; 114 /*@ readable lastUnreturnedChar if unreturnedChars != 0; */ 115 //@ invariant lastUnreturnedChar != '@'; 116 117 /** 118 * Indicates whether or not a sequence of consecutive special 119 * characters at the end of the comment are to be treated as white 120 * space. This is only done for the special character '@'. 121 */ 122 123 //@ spec_public 124 private final boolean allowSpecialSuffix; 125 //@ invariant allowSpecialSuffix ==> specialCharacter == '@'; 126 127 /** 128 * Reads the next character from this input stream. Performs Unicode 129 * conversion and JML filtering. Requires that the stream is open. 130 * 131 * @return A Unicode character, or -1. 132 */ 133 public int read() throws IOException { 134 /*-@ uninitialized */ int ch = 0; // dummy assignment 135 if (unreturnedChars == 0) { 136 ch = child.read(); 137 if (ch == '\n') { 138 prefixMode = 0; 139 } else if (prefixMode == 0 && Character.isWhitespace((char)ch)) { 140 // remain in this mode 141 } else if (prefixMode < 2) { 142 if (ch == specialCharacter) { 143 ch = ' '; // treat the special character as a space 144 prefixMode = 1; 145 } else { 146 prefixMode = 2; // enter meat mode 147 } 148 } else if (allowSpecialSuffix && ch == specialCharacter) { 149 unreturnedChars++; 150 do { 151 lastUnreturnedChar = child.read(); 152 unreturnedChars++; 153 } while (lastUnreturnedChar == specialCharacter); 154 if (escjava.Main.options().parsePlus && lastUnreturnedChar == '+') { 155 lastUnreturnedChar = child.read(); 156 unreturnedChars++; 157 } 158 } 159 } 160 if (unreturnedChars > 0) { 161 if (unreturnedChars == 1) { 162 ch = lastUnreturnedChar; 163 } else if (lastUnreturnedChar == -1) { 164 ch = ' '; 165 } else { 166 ch = specialCharacter; 167 } 168 unreturnedChars--; 169 } 170 return ch; 171 } 172 173 174 // Getting Locations 175 176 public int getLocation() { 177 return super.getLocation() - unreturnedChars; 178 } 179 180 181 // [Un]marking 182 183 //@ spec_public 184 private int prefixModeAtMark; /*@ readable prefixModeAtMark if marked; */ 185 //@ invariant 0 <= prefixModeAtMark && prefixModeAtMark <= 2; 186 187 //@ spec_public 188 private int unreturnedCharsAtMark; /*@ readable unreturnedCharsAtMark if marked; */ 189 //@ invariant 0 <= unreturnedCharsAtMark; 190 //@ invariant prefixModeAtMark < 2 ==> unreturnedCharsAtMark == 0; 191 //@ invariant specialCharacter != '@' ==> unreturnedCharsAtMark == 0; 192 193 //@ spec_public 194 private int lastUnreturnedCharAtMark; /*@ readable lastUnreturnedCharAtMark if marked; */ 195 //@ invariant lastUnreturnedCharAtMark != '@'; 196 197 public void mark() { 198 super.mark(); 199 prefixModeAtMark = prefixMode; 200 unreturnedCharsAtMark = unreturnedChars; 201 lastUnreturnedCharAtMark = lastUnreturnedChar; //@ nowarn Unreadable; 202 } 203 204 public void reset() throws IOException { 205 prefixMode = prefixModeAtMark; 206 unreturnedChars = unreturnedCharsAtMark; 207 lastUnreturnedChar = lastUnreturnedCharAtMark; 208 super.reset(); 209 } 210 } // end of class JmlCorrelatedReader 211 212 /* 213 * Local Variables: 214 * Mode: Java 215 * fill-column: 85 216 * End: 217 */ 218