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