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