diff --git a/Assignment03-extended_typechecking.pdf b/Assignment03-extended_typechecking.pdf new file mode 100644 index 0000000..4cec271 Binary files /dev/null and b/Assignment03-extended_typechecking.pdf differ diff --git a/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java index e13fa57..ac9aa0a 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java @@ -16,6 +16,9 @@ */ package org.apache.commons.text.translate; +import org.checkerframework.checker.index.qual.LTLengthOf; +import org.checkerframework.checker.index.qual.NonNegative; + import java.io.IOException; import java.io.Writer; import java.util.ArrayList; @@ -53,7 +56,9 @@ public class AggregateTranslator extends CharSequenceTranslator { * {@inheritDoc} */ @Override - public int translate(final CharSequence input, final int index, final Writer writer) throws IOException { + public int translate(final CharSequence input, + final @NonNegative @LTLengthOf("#1") int index, + final Writer writer) throws IOException { for (final CharSequenceTranslator translator : translators) { final int consumed = translator.translate(input, index, writer); if (consumed != 0) { diff --git a/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java index 6a96a22..f927b35 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java @@ -23,6 +23,9 @@ import java.io.Writer; import java.util.Locale; import org.apache.commons.lang3.Validate; +import org.checkerframework.checker.index.qual.LTLengthOf; +import org.checkerframework.checker.index.qual.NonNegative; +import org.checkerframework.checker.index.qual.Positive; /** * An API for translating text. @@ -80,7 +83,9 @@ public abstract class CharSequenceTranslator { * @return int count of code points consumed * @throws IOException if and only if the Writer produces an IOException */ - public abstract int translate(CharSequence input, int index, Writer writer) throws IOException; + public abstract int translate(CharSequence input, + @NonNegative @LTLengthOf("#1") int index, + Writer writer) throws IOException; /** * Translate an input onto a Writer. This is intentionally final as its algorithm is @@ -116,8 +121,14 @@ public abstract class CharSequenceTranslator { } // contract with translators is that they have to understand code points // and they just took care of a surrogate pair - for (int pt = 0; pt < consumed; pt++) { - pos += Character.charCount(Character.codePointAt(input, pos)); + // Added pos < len as defensive condition for possibly buggy implementations of translate returning wrong + // number of codepoints consumed + for (int pt = 0; pt < consumed && pos < len; pt++) { + int increment = Character.charCount(Character.codePointAt(input, pos)); + assert pos + increment <= len : "@AssumeAssertion(index): increment corresponds to the number of bytes" + + "of char codepoint at position index[pos]. Adding this quantity results in a valid index or in" + + "the length of the string."; + pos += increment; } } } @@ -130,8 +141,10 @@ public abstract class CharSequenceTranslator { * @return CharSequenceTranslator merging this translator with the others */ public final CharSequenceTranslator with(final CharSequenceTranslator... translators) { - final CharSequenceTranslator[] newArray = new CharSequenceTranslator[translators.length + 1]; + final @Positive int newArrayLen = translators.length + 1; + final CharSequenceTranslator[] newArray = new CharSequenceTranslator[newArrayLen]; newArray[0] = this; + assert translators.length == newArray.length - 1 : "@AssumeAssertion(index): by construction of newArray and newArrayLen"; System.arraycopy(translators, 0, newArray, 1, translators.length); return new AggregateTranslator(newArray); } diff --git a/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java b/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java index 992c46e..c6d482c 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java @@ -16,6 +16,9 @@ */ package org.apache.commons.text.translate; +import org.checkerframework.checker.index.qual.LTLengthOf; +import org.checkerframework.checker.index.qual.NonNegative; + import java.io.IOException; import java.io.Writer; @@ -32,7 +35,9 @@ public abstract class CodePointTranslator extends CharSequenceTranslator { * {@inheritDoc} */ @Override - public final int translate(final CharSequence input, final int index, final Writer writer) throws IOException { + public final int translate(final CharSequence input, + final @NonNegative @LTLengthOf("#1") int index, + final Writer writer) throws IOException { final int codePoint = Character.codePointAt(input, index); final boolean consumed = translate(codePoint, writer); return consumed ? 1 : 0; diff --git a/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java b/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java index d6bb8be..1751f59 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java +++ b/sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java @@ -58,14 +58,28 @@ public final class CsvTranslators { @Override void translateWhole(final CharSequence input, final Writer writer) throws IOException { + final int zeroIndex = 0; + final int oneIndex = 1; + final int lastIndex = input.length() - 1; + + // unfortunately there is no way to encode non-empty length + assert zeroIndex < input.length() && lastIndex >= 0 : + "@AssumeAssertion(index): translateWhole is called by " + + "SinglePassTranslator.translate(CharSequence, int, Writer), and that is part of a template method" + + "implementation that by contract is called only with non-empty `input` CharSequences"; + // is input not quoted? - if (input.charAt(0) != CSV_QUOTE || input.charAt(input.length() - 1) != CSV_QUOTE) { + if (input.charAt(zeroIndex) != CSV_QUOTE || input.charAt(lastIndex) != CSV_QUOTE) { writer.write(input.toString()); return; } + if (oneIndex >= input.length()) { + throw new IllegalArgumentException("input length should be at least 2"); + } + // strip quotes - final String quoteless = input.subSequence(1, input.length() - 1).toString(); + final String quoteless = input.subSequence(oneIndex, lastIndex).toString(); if (StringUtils.containsAny(quoteless, CSV_SEARCH_CHARS)) { // deal with escaped quotes; ie) "" diff --git a/sources/src/main/java/org/apache/commons/text/translate/UnicodeEscaper.java b/sources/src/main/java/org/apache/commons/text/translate/UnicodeEscaper.java index ea7081d..dfade90 100644 --- a/sources/src/main/java/org/apache/commons/text/translate/UnicodeEscaper.java +++ b/sources/src/main/java/org/apache/commons/text/translate/UnicodeEscaper.java @@ -128,11 +128,18 @@ public class UnicodeEscaper extends CodePointTranslator { writer.write(toUtf16Escape(codePoint)); } else { writer.write("\\u"); - writer.write(HEX_DIGITS[codePoint >> 12 & 15]); - writer.write(HEX_DIGITS[codePoint >> 8 & 15]); - writer.write(HEX_DIGITS[codePoint >> 4 & 15]); - writer.write(HEX_DIGITS[codePoint & 15]); + writer.write(hexDigitsAccess(codePoint >> 12)); + writer.write(hexDigitsAccess(codePoint >> 8)); + writer.write(hexDigitsAccess(codePoint >> 4)); + writer.write(hexDigitsAccess(codePoint)); } return true; } + + private char hexDigitsAccess(final int index) { + int i = index & 15; + assert i >= 0 && i < HEX_DIGITS.length + : "@AssumeAssertion(index): bitwise and with 15 always produces numbers in [0,15]"; + return HEX_DIGITS[i]; + } }