    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