Fix unsound handling of catch parameters and throws clauses

[Ao-senXiong]

Fixes #363. This PR revealed the need for #494 and depends on it being merged first.

[wmdietl]

Thanks for all the improvements to this PR! I have another long list of comments.

[wmdietl]

Changing the error key also requires a change to this file:
https://github.com/eisop/checker-framework/blob/e604d8d10a38d09f7c3e94c4d614b2d729f48085/framework/src/main/java/org/checkerframework/common/basetype/messages.properties#L35C12-L35C19

incompatible is the better term, as there is a comparison between two types.
In a previous discussion we said we do this renaming in a separate PR. Was there a change of mind?

[Ao-senXiong]

I have opened a new PR here #618.

[wmdietl]

So you should undo these changes in this PR, so that we can merge this PR independently of #618.

[wmdietl]

Try having just one top-level class in tests or include something, like 363a in all top-level class names.
Otherwise, it is very easy for two different tests to define a generic class name like MyException and strange behavior can result.

[wmdietl]

This just makes the @Initialized qualifier explicit. Is that the intention?
Should there be a separate constructor that takes an @UnderInitialization parameter, to test all possibilities?

[wmdietl]

It's rather misleading that this constructor, with a char parameter, invokes the MyException constructor with a String argument. The following constructor with a String parameter, invokes a different constructor. Maybe these can be aligned a bit better?

[wmdietl]

This is the same as test1, just with an explicit qualifier. Put them next to each other and add a comment?

[Ao-senXiong]

@wmdietl I try to compare the type of exception that method body throw and the type of catch parameter. Do you have any suggestion on how to get what exception the method body throws?

[Ao-senXiong]

@wmdietl I think we should allow the following code as the exception may not be catched like how Java handle this:

void foo() throw @UnknowInitialization myException {}

void test(){
    try {
        foo()
    } catch (MyException e) {}
}

[wmdietl]

@Ao-senXiong Can you look into wrapping up this change, without the renaming that is done in #618? Let's first fix the soundness issue and then improve the naming.

[wmdietl]

Thanks for getting back to this.

[wmdietl]

allowedExceptions should never be null, so this check is redundant.

[wmdietl]

What is the logic for this subtype test? Shouldn't it be the other way around?
Why is it only comparing the TypeMirrors and not considering annotations?

[Ao-senXiong]

The purpose here is to update required variable, which is used to check subtyping relationship between actual throw type and required.

The logic is: we should only update require only if the exception throwed is a subtype of one of the decleared throw exception in method signature. For example for the following code, we should update required to @Initailized instead of use top annotation in the hierarchy. And since actual throw exception has @UnderInitialization type. so throw type invalid error should be issued

    EISOPIssue363(int dummy1, int dummy2, int dummy3) throws @Initailized MyException {
        // :: error: (throw.type.invalid)
        throw new MyException(this, "UnderInitialization");
    }

[Ao-senXiong]

add test case for methodinvocation.

[wmdietl]

You didn't come back to this comment. Doesn't this mean that from a throw statement, you need to look at both the enclosing catch clauses and only finally at the throws clause on the enclosing method?