maggicl/soft-an03
Archived
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

wip on fixing checker warnings

Browse source
This commit is contained in:
Claudio Maggioni 2023-04-26 11:03:57 +02:00
parent ecb7925340
commit 84c49f645a
6 changed files with 56 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
Assignment03-extended_typechecking.pdf Normal file
View file

Binary file not shown.

7
sources/src/main/java/org/apache/commons/text/translate/AggregateTranslator.java
View file

@ -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) {

21
sources/src/main/java/org/apache/commons/text/translate/CharSequenceTranslator.java
View file

@ -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);
}

7
sources/src/main/java/org/apache/commons/text/translate/CodePointTranslator.java
View file

@ -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;

18
sources/src/main/java/org/apache/commons/text/translate/CsvTranslators.java
View file

@ -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) ""

15
sources/src/main/java/org/apache/commons/text/translate/UnicodeEscaper.java
View file

@ -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];
}
}