The Index checker with all string-related changes merged has been run on daikon. All array warnings have been ignored.
String warnings
False positives
Due to a limitation in the index checker, it issued a warning for a correct code.
(1) #9: Length refinement by startsWith, endsWith with a static final variable
This pattern is currently supported for literals, but does not work when a static final variable is used instead.
Reported as argument.type.incompatible when calling substring.
VarInfoName:77
dcomp/DCRuntime.java:2066
dcomp/DCRuntime.java:2266
(2) #4: Adding an offset to an index returned from indexOf
When calling indexOf, checking that the returned index is not -1 and adding the length of the argument to that index, the result should be @IndexOrHigh.
Reported as argument.type.incompatible when calling substring.
(3) #10: indexOf!=-1 means subsequent calls will succeed too
The code checks that s.indexOf(t)!=-1, then in the branch calls indexOf again with the same arguments.
These calls cannot return -1 and should be usable as an index without further checking.
Some cases can be solved by extracting the indexOf call to a local variable. However lastIndexOf should succeed as well.
Colud be solved by adding an annotation @ContainsSubstring(t).
Reported as lowerbound:argument.type.incompatible when calling substring.
inv/FeatureExtractor.java:631
inv/FeatureExtractor.java:634
inv/FeatureExtractor.java:858
inv/FeatureExtractor.java:979
inv/FeatureExtractor.java:1004
Daikon.java:1174
diff/MatchCountVisitor2.java:97 (in conditional expression)
11: (4) Longer than (or same) relation
A relation between two sequences, meaning one of them is at least as long as another. Could be expressed by a new annotation @LongerThanEq("s"). Can be inferred from concatenation and substring, and refined by startsWith, endsWith. Related to kelloggm#158.
VarInfoName.java:1284 (probably will not work here without additional care, because "" is special cased)
ContextSplitterFactory.java:162
tools/jtb/Ast.java:1146 (first checked two strings are not equal, then after endsWith succeeds, it should infer that one is strictly longer than other, therefore a.length()-b.length()-1 is non-negative; when calling charAt)
related to VarInfo:2922 in (17)
(5) #12: Refinement of upper bound by !=
When i!=a.length-1, then @LTLengthOf("a") can be refined to @LTLengthOf(value="a",offset="1").
Some cases can be solved by adding annotation @IndexOrHigh and changing == to >=.
util/UtilMDE.java:2565, FileIO:2429 (@IndexFor(s) int i; if(i==s.length()-1)break; s.charAt(i+1))
util/UtilMDE.java:2561, util/UtilMDE.java:2567, util/UtilMDE.java:2572, util/UtilMDE.java:2580, util/UtilMDE.java:2594, util/UtilMDE.java:2611, util/UtilMDE.java:2620 (same as above)
(6) Regex Matcher.start, Matcher.end
Warnings related to indices returned from Matcher.start, Matcher.end methods.
Reported as argument.type.incompatible when calling substring with one of these two methods as arguments.
(6a) #8: Removed lower bound annotations
Some lower bound annotations are missing in the annotated JDK for the Matcher class. They were in the annotated JDK in the past, but they were removed.
config/HtmlToTexinfo:33 (in Matcher.find)
config/HtmlToTexinfo.java:34 (2×)
config/HtmlToTexinfo.java:40
(6b) #13: Upper bounds
The indices returned from start and end should be IndexOrHigh for the input sequence.
Could be solved by creating an annotation @MatcherFor("s") for the matcher variable, however the input sequence can be changed by reset.
HtmlToTexinfo.java:34 (2×)
HtmlToTexinfo.java:36 (2×)
HtmlToTexinfo.java:40
(6c) #14: Lower bound on non-optional group
If a group in regex must always match, then start and end always return non-negative for that group.
HtmlToTexinfo.java:36 (2×)
(7) #15: @MinLen by loop bound condition
A string is generated using concatenation of non-empty parts in a loop. When the bound of the loop is checked to be at least a certain number, then the generated string has at least a certain minimum length.
Reported as upperbound:argument.type.incompatible when calling substring.
The code assumes that the string returned from StringTokenizer.nextToken is non-empty. Is that correct?
PptCountVisitor.java:232
diff/MatchCountVisitor.java:161
(9) #5: write(string, int, int) is @IndexFor, not @IndexOrHigh
This method is annotated consistently with the char[] counterpart. However, the @IndexFor annotation on the second argument is too strict.
util/UtilMDE.java:1272
test/inv/InvariantAddAndCheckTester.java:202
test/inv/InvariantAddAndCheckTester.java:217
(10) #17: startsWith or endsWith in a helper method
Refinement of string length after checking startsWith or endsWith is supported, but this check can be hidden in a helper method. Probably could be solved by EnsuresQualifierIf(LongerThanEq).
asm/X86Instruction.java:69 (2×)
asm/X86Instruction.java:82 (2×)
PptName.java:317
asm/Operand.java:133 (2×)
(11) #18: Length refinement after a.indexOf(s)!=-1
When a.indexOf(s)!=-1 is checked, the length of a could be refined the same as it is for startsWith or endsWith.
Debug.java:755
(12) #19: If !a.endsWith(c), then a.indexOf(c)<a.length-1
PrintInvariants.java:668
(13) Substring on static final string
chicory/DaikonClassInfo.java:82
(14) #20 Math.max preserves IndexFor
When two indices are merged using Math.max, the result is also an index. Will a polymorphic qualifier work?
tools/jtb/PptNameMatcher.java:345
Complex program logic or bugs
Either the logic of the program ensures a complex property that is hard to express
or it is a bug (hard to tell).
(15) String has a minimum length
Reported as argument.type.incompatible, usually when calling substring.
OneOfStringSequence.java:404, inv/unary/sequence/OneOfSequence.java:445 inv/unary/sequence/OneOfFloatSequence.java:374 and 16 other classes (this.getClass().toString().substring(6))
tools/TraceSelect.java:326 (2×; in string comparer)
ContextSplitterFactory.java:151
ContextSplitterFactory.java:152
ContextSplitterFactory.java:162
AnnotateNullable.java:118
dcomp/DCRuntime.java:2257 (class name contains . before :, returned from a toString method
config/ParameterDoclet.java:183: (two related getters, checks startsWith on a string returned from one getter, then calls indexOf on a string returned from the other getter)
diff/Diff.java:790, MatchCountVisitor.java:57, diff/MatchCountVisitor.java:66, diff/MatchCountVisitor.java:82, diff/MatchCountVisitor.java:96 (a getter returns a string which always contains a constant substring)
diff/MatchCountVisitor2.java:118
diff/MultiDiffVisitor.java:59
(17) Complex precondition
Reported as argument.type.incompatible usually when calling substring.
VarInfoName:627 (argument cannot be "~")
VarInfo:2922 (a!=b + longer than refinement by startsWith)
diff/PptCountVisitor.java:163 (2×; argument contains two substrings)
tools/runtimechecker/InstrumentVisitor.java:1239 (class name starts with package name and a dot, if package name is not empty
util/UtilMDE.java:740, util/UtilMDE.java:749 (after checking suffix by endsWith, while(s.charAt(i)=='c')++i; is safe. This warning can be hidden by adding a indexOf annotation, which should not work but does maybe because kelloggm#81)
(20) Complex field invariant
tools/ExtractConsequent.java:404 (name!='.')
False positives solved by writing annotations
argument.type.incompatible when calling substring or charAt. For annotations added on method parameters, call sites were not checked. For annotations added on method return types, they were not checked.
The Index checker with all string-related changes merged has been run on daikon. All
arraywarnings have been ignored.String warnings
False positives
Due to a limitation in the index checker, it issued a warning for a correct code.
(1) #9: Length refinement by
startsWith,endsWithwith astatic finalvariableThis pattern is currently supported for literals, but does not work when a static final variable is used instead. Reported as
argument.type.incompatiblewhen callingsubstring.(2) #4: Adding an offset to an index returned from
indexOfWhen calling
indexOf, checking that the returned index is not-1and adding the length of the argument to that index, the result should be@IndexOrHigh. Reported asargument.type.incompatiblewhen callingsubstring.startsWith)(3) #10:
indexOf!=-1means subsequent calls will succeed tooThe code checks that
s.indexOf(t)!=-1, then in the branch callsindexOfagain with the same arguments. These calls cannot return -1 and should be usable as an index without further checking. Some cases can be solved by extracting theindexOfcall to a local variable. HoweverlastIndexOfshould succeed as well. Colud be solved by adding an annotation@ContainsSubstring(t). Reported aslowerbound:argument.type.incompatiblewhen calling substring.11: (4) Longer than (or same) relation
A relation between two sequences, meaning one of them is at least as long as another. Could be expressed by a new annotation
@LongerThanEq("s"). Can be inferred from concatenation andsubstring, and refined bystartsWith,endsWith. Related to kelloggm#158.""is special cased)endsWithsucceeds, it should infer that one is strictly longer than other, thereforea.length()-b.length()-1is non-negative; when callingcharAt)(5) #12: Refinement of upper bound by
!=When
i!=a.length-1, then@LTLengthOf("a")can be refined to@LTLengthOf(value="a",offset="1"). Some cases can be solved by adding annotation@IndexOrHighand changing==to>=.@IndexFor(s) int i; if(i==s.length()-1)break; s.charAt(i+1))(6) Regex
Matcher.start,Matcher.endWarnings related to indices returned from
Matcher.start,Matcher.endmethods. Reported asargument.type.incompatiblewhen callingsubstringwith one of these two methods as arguments.(6a) #8: Removed lower bound annotations
Some lower bound annotations are missing in the annotated JDK for the
Matcherclass. They were in the annotated JDK in the past, but they were removed.Matcher.find)(6b) #13: Upper bounds
The indices returned from
startandendshould beIndexOrHighfor the input sequence. Could be solved by creating an annotation@MatcherFor("s")for the matcher variable, however the input sequence can be changed byreset.(6c) #14: Lower bound on non-optional group
If a group in regex must always match, then
startandendalways return non-negative for that group.(7) #15:
@MinLenby loop bound conditionA string is generated using concatenation of non-empty parts in a loop. When the bound of the loop is checked to be at least a certain number, then the generated string has at least a certain minimum length. Reported as
upperbound:argument.type.incompatiblewhen callingsubstring.(8) #16:
@Minlen(1)onStringTokenizer.nextTokenThe code assumes that the string returned from
StringTokenizer.nextTokenis non-empty. Is that correct?(9) #5:
write(string, int, int)is@IndexFor, not@IndexOrHighThis method is annotated consistently with the
char[]counterpart. However, the@IndexForannotation on the second argument is too strict.(10) #17:
startsWithorendsWithin a helper methodRefinement of string length after checking
startsWithorendsWithis supported, but this check can be hidden in a helper method. Probably could be solved byEnsuresQualifierIf(LongerThanEq).(11) #18: Length refinement after
a.indexOf(s)!=-1When
a.indexOf(s)!=-1is checked, the length ofacould be refined the same as it is forstartsWithorendsWith.(12) #19: If
!a.endsWith(c), thena.indexOf(c)<a.length-1(13) Substring on static final string
(14) #20
Math.maxpreservesIndexForWhen two indices are merged using
Math.max, the result is also an index. Will a polymorphic qualifier work?Complex program logic or bugs
Either the logic of the program ensures a complex property that is hard to express or it is a bug (hard to tell).
(15) String has a minimum length
Reported as
argument.type.incompatible, usually when callingsubstring.this.getClass().toString().substring(6))Matcher.replaceFirstpreserves length)UtilMDE.unescapeNonJavapreserves non-emptiness)(16) String contains a substring
Reported as
argument.type.incompatiblewhen callingsubstringwith an index returned fromindexOf.).before:, returned from a toString methodstartsWithon a string returned from one getter, then callsindexOfon a string returned from the other getter)(17) Complex precondition
Reported as
argument.type.incompatibleusually when callingsubstring."~")a!=b+ longer than refinement bystartsWith)[])'.')(18) Complex index computation
Reported as
argument.type.incompatibleusually when callingsubstring. The index is computed using division operator.(19) Other complex property
IndexFor)new File(fileName).getName()preserves@MinLen)endsWith,while(s.charAt(i)=='c')++i;is safe. This warning can be hidden by adding aindexOfannotation, which should not work but does maybe because kelloggm#81)(20) Complex field invariant
name!='.')False positives solved by writing annotations
argument.type.incompatiblewhen callingsubstringorcharAt. For annotations added on method parameters, call sites were not checked. For annotations added on method return types, they were not checked.substring, add@MinLen)charAt(2×), add@MinLen)@IndexFor)@IndexOrHigh)@MinLen)@MinLen(1)oncom.sun.org.apache.bcel.internal.generic.InvokeInstruction.getMethodName)@NonNegativeonAnnotateVisitor.getTabbedIndex)@NonNegative)True positives
The program might trigger an out-of-bounds exception.
main,args[0]must contain'.')Non-string warnings
These warnings were not analyzed becaue they are not related to strings.
Invalid overrides
override.return.invalidObject.cloneshould be@PolySameLen: 65 classesReader.readshould be@IndexOrLow(#1): 2 classesInputStream.readshould be@IndexOrLow(#1): 1 classjava.util.AbstractMap.size: 2 classes + 4 innerjava.util.List.size: 1 classjava.util.CharSequence.lengthshould be@NonNegative: 1 class (daikon.util.StringBuilderDelimited)argument.type.incompatibleSystem.arraycopy: 44 occurences in 6 classesnew ArrayList()should be@NonNegative: 12 occurences in 7 classesnew HashMap()should be@NonNegative: 2 occurences in 1 classesnew BitSet()should be@NonNegative: 2 occurences in 2 classesVector: 1 occurence in 1 classArrays.fill: 1 occurence in 1 classArrays.sort: 27 occurence in 9 classArrayList.get: 2 occurences in 2 classesBitSet.set/get: 7 occurences in 4 classesLineNumberReader: 1 occurence in 1 classRandom.nextInt: 6 occurences in 6 classeswritewith arrays 4 occurences in 1 classWriter.write(int)should be@NonNegative: 1 occurence in 1 class