search

typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
990 stars 347 forks source link

Implement same trust-and-verify scheme used for Positive annotations by the Value Checker for other Lower Bound Checker annotations #1358

Closed kelloggm closed 6 years ago

kelloggm commented 6 years ago

This PR extends the same trust-and-verify scheme that the Value Checker already uses for deriving information from @Positive annotations to two other Lower Bound Checker annotations: @NonNegative and @GTENegativeOne.

The primary motivation for extending this scheme is to prevent the sort of difficult-to-reason-about problems with overriding methods that is described in kelloggm#147.

kelloggm commented 6 years ago

As far as I can tell, the tests are failing because this change requires the JDK to be rebuilt (verified locally).

smillst commented 6 years ago

I changed the build file to use a jdk built with this branch. There are still errors: https://travis-ci.org/typetools/checker-framework/jobs/246282200

kelloggm commented 6 years ago

@smillst Both this PR and #1346 are failing their tests and I don't understand why. Can you look into what's happening on Travis? As far as I can tell, it's not related to the actual content of the PRs. Here's the error:

Error while writing report: java.io.FileNotFoundException: /checker-framework/checker/build/jtreg/all/report/text/timeStats.txt (No such file or directory)
mernst commented 6 years ago

@kelloggm I fixed the problem by creating the directory that the error reporter needs. (I don't know why it doesn't do that automatically.)

This revealed the underlying problem, which the system was trying to write into the underlying log file: [jtreg] FAILED: sortwarnings/Main.java

mernst commented 6 years ago

The specific problem is that the expected output contains

OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)

but the actual output contains

OrderOfCheckers.java:14:53: compiler.err.proc.messager: (type.invalid)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)
OrderOfCheckers.java:14:57: compiler.err.proc.messager: (assignment.type.incompatible)

where the first line differs.

mernst commented 6 years ago

The jtreg tests failed in the sortwarnings test producing this output: [jtreg] FAILED: sortwarnings/Main.java

More specifically:

To reproduce this, do: (cd checker && ant jtreg-tests-checkers)

The checker output can be obtained with:

  (cd checker/jtreg/sortwarnings && $ch/bin/javac -processor
  org.checkerframework.checker.index.IndexChecker -AprintErrorStack
  OrderOfCheckers.java ErrorOrders.java)

The checker output causing the test failure is:

  OrderOfCheckers.java:12: error: [type.invalid] [@BottomVal] may not be applied to the type "@IntRangeFromGTENegativeOne int []"
        @GTENegativeOne @UpperBoundBottom @SearchIndexBottom @BottomVal int @BottomVal @SameLenBottom [] x = y;

This error message says: "Given that we already know that the value is at least -1, it doesn't make sense to say @BottomVal, which says that we know nothing about its value, not even a range that its value falls into."

This error seems reasonable. Given the changes in the pull request, it seems that the expected errors have changed, and it makes to change the expected/goal output rather than trying to change the checker to conform to the old expected/goal output.

mernst commented 6 years ago

Some problems are now resolved.

One of the current test failures is an unexpected error:

StringLength.java:76: error: [type.invalid] [@IntRange(from=0, to=2147483647), @UnknownVal] may not be applied to the type "@IntRange(from=0, to=2147483647) @UnknownVal int"
        @IndexOrHigh("s") int i = s.length();
                                          ^

Can you take a look at this, with an eye to finishing off the pull request?

kelloggm commented 6 years ago

The reason the tests were failing is that the annotation on String#length was @LengthOf("this"), which implies @NonNegative. This change converts that into an @IntRange. However, if a string or an array has a length annotation, then that is also transferred to the length. If no length annotation is found, then @IntRange(from=0) is added. These two ways of adding annotations were colliding to create the type.invalid. I removed the LengthOf annotation and replaced it with a LTEqLengthOf annotation. The NonNegative, as I said before, is being applied automatically.

As an aside, sorry this PR has been open for so long and I haven't had the chance to finish it.

mernst commented 6 years ago

Thanks! Your change resolved that problem. The current problem is now on Lambda.java. I haven't investigated it; could you?

kelloggm commented 6 years ago

That's the same problem; because the change I made was in the JDK, this branch needs to use its own annotated JDK instead of the prebuilt version when running the travis tests. I've switched which is being used.

mernst commented 6 years ago

Thanks for updating the JDK. Suzanne hadn't thought it was necessary for this pull request. Now, the Travis job gets all the way to the jtreg tests (almost the end) before failing one of the jtreg tests:

    [jtreg] FAILED: sortwarnings/Main.java
smillst commented 6 years ago

Suzanne hadn't thought it was necessary for this pull request.

This pull request was using it's own jdk. Martin changed the jdk (https://github.com/typetools/checker-framework/pull/1358/commits/efc562b337dcce7e06d3f4d61dee9de8e3c058b0), so he also updated the jdk that this branch was using.

kelloggm commented 6 years ago

The tests on this pull request are finally passing, after debugging some travis failures. This needs to be reviewed.

smillst commented 6 years ago

The code changes are correct and are ready to be merged. But first can would you please merge master into this branch and rebuilt the jdk?

kelloggm commented 6 years ago

Will do.

On Mon, Sep 25, 2017 at 3:37 PM, Suzanne Millstein <notifications@github.com

wrote:

The code changes are correct and are ready to be merged. But first can would you please merge master into this branch and rebuilt the jdk?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/typetools/checker-framework/pull/1358#issuecomment-332033860, or mute the thread https://github.com/notifications/unsubscribe-auth/ADxuti9tgDLBWWkyT5rDP4dSgf_sAmr-ks5smCstgaJpZM4OBjDE .

kelloggm commented 6 years ago

This pull request is blocked.

The tests are failing with type.invalid errors, which appear whenever any code that uses java.lang.String#length is used. The error claims that both an @UnknownVal annotation and an @IntRange(from = 0, to = 2147483647) are present, so the type is invalid. I traced the @UnknownVal annotation to the file statically-executable.astub, which contains the Value Checker's JDK annotations, and to the Index JDK's java/lang/String.java file, which contains an @LengthOf("this") annotation, which is an alias for @NonNegative. It seems that when the Index JDK is built, both the @NonNegative annotation and the @UnknownVal annotation remain in the bytecode; we confirmed this by unzipping the jdk8.jar file produced by this branch and inspecting java/lang/String.class using javap -v.

This doesn't happen when just compiling classes using the Index Checker, so we believe this is a problem with the stubparser. It seems to not be putting the derived @IntRange annotation into bytecode, and instead preferring the implicit @UnknownVal from the stub file.

smillst commented 6 years ago

I corrected the Jtreg test that I added. With your changes, it now passes. So, all that's left is to rebuild the annotated jdk, make sure the tests pass here and then merge.

kelloggm commented 6 years ago

Awesome. I'll start rebuilding the JDK now.

mernst commented 6 years ago

The tests are failing for this pull request, so it isn't yet ready to merge.

kelloggm commented 6 years ago

The tests are failing because the JDK being used by this pull request hasn't been updated with the contents of the pull request. We won't merge the PR until travis shows the tests passing.

smillst commented 6 years ago

I just pushed changes to the jdk to master, which I just merged in.

kelloggm commented 6 years ago

@smillst, this is now failing because the Nullness Checker's tests are failing. The failing test was added in one of your recent merge commits: 48ca028. Do you know why these might be failing? https://travis-ci.org/typetools/checker-framework/jobs/280582094

smillst commented 6 years ago

I just pushed changes to the jdk to master, which I just merged in.

Did you rebuild the jdk after I did that?

kelloggm commented 6 years ago

No, the JDK is from this morning. I'll rebuild it; I didn't realize I'd need to.

On Wed, Sep 27, 2017 at 2:48 PM, Suzanne Millstein <notifications@github.com

wrote:

I just pushed changes to the jdk to master, which I just merged in.

Did you rebuild the jdk after I did that?

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHub https://github.com/typetools/checker-framework/pull/1358#issuecomment-332665689, or mute the thread https://github.com/notifications/unsubscribe-auth/ADxutu8vw44f9djXGwt1Hwpa3XuG4RHFks5smsLCgaJpZM4OBjDE .