Fix unsound handling of catch parameters and throws clauses

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

@@ -425,6 +425,7 @@ private boolean isNewArrayInToArray(NewArrayTree tree) {
     @Override
     protected void checkThrownExpression(ThrowTree tree) {
         checkForNullability(tree.getExpression(), THROWING_NULLABLE);
+        super.checkThrownExpression(tree);
     }
 
     /** Case 5: Check for synchronizing locks. */

checker/tests/guieffect/ThrowCatchTest.java

@@ -17,15 +17,15 @@ class Inner {}
     // Type var test
     <E extends @UI PolyUIException> void throwTypeVarUI1(E ex1, @UI E ex2) throws PolyUIException {
         if (flag) {
-            // :: error: (throw.type.invalid)
+            // :: error: (throw.type.incompatible)
             throw ex1;
         }
-        // :: error: (throw.type.invalid)
+        // :: error: (throw.type.incompatible)
         throw ex2;
     }
 
     <@UI E extends @UI PolyUIException> void throwTypeVarUI2(E ex1) throws PolyUIException {
-        // :: error: (throw.type.invalid)
+        // :: error: (throw.type.incompatible)
         throw ex1;
     }
 
@@ -48,7 +48,7 @@ class Inner {}
     <@AlwaysSafe E extends @UI PolyUIException> void throwTypeVarMixed(E ex1, @AlwaysSafe E ex2)
             throws PolyUIException {
         if (flag) {
-            // :: error: (throw.type.invalid)
+            // :: error: (throw.type.incompatible)
             throw ex1;
         }
         throw ex2;
@@ -75,7 +75,7 @@ void throwNull() {
 
     void throwDeclared() {
         try {
-            // :: error: (throw.type.invalid)
+            // :: error: (throw.type.incompatible)
             throw ui;
         } catch (@UI PolyUIException UIParam) {
 

checker/tests/initialization/EISOPIssue363a.java

@@ -0,0 +1,154 @@
+// Test case for issue 363:
+// https://github.com/eisop/checker-framework/issues/363
+
+import org.checkerframework.checker.initialization.qual.NotOnlyInitialized;
+import org.checkerframework.checker.initialization.qual.UnderInitialization;
+import org.checkerframework.checker.initialization.qual.UnknownInitialization;
+
+public class EISOPIssue363a {
+    class MyException extends Exception {
+        @NotOnlyInitialized EISOPIssue363a cause;
+
+        MyException(EISOPIssue363a cause) {
+            this.cause = cause;
+        }
+
+        MyException(@UnderInitialization EISOPIssue363a cause, String dummy) {
+            this.cause = cause;
+        }
+
+        MyException(@UnknownInitialization EISOPIssue363a cause, int dummy) {
+            this.cause = cause;
+        }
+    }
+
+    Object field;
+
+    EISOPIssue363a() throws MyException {
+        // :: error: (throw.type.incompatible)
+        // :: error: (argument.type.incompatible)
+        throw new MyException(this);
+    }
+
+    EISOPIssue363a(boolean dummy1, boolean dummy2) throws MyException {
+        // :: error: (throw.type.incompatible)
+        throw new MyException(this, 0);
+    }
+
+    EISOPIssue363a(boolean dummy1, boolean dummy2, boolean dummy3) throws MyException {
+        // :: error: (throw.type.incompatible)
+        throw new MyException(this, "UnderInitialization");
+    }
+
+    EISOPIssue363a(int dummy) throws @UnknownInitialization MyException {
+        throw new MyException(this, 0);
+    }
+
+    EISOPIssue363a(int dummy1, int dummy2) throws @UnknownInitialization MyException {
+        throw new MyException(this, "UnderInitialization");
+    }
+
+    EISOPIssue363a(int dummy1, int dummy2, int dummy3) throws @UnknownInitialization MyException {
+        // :: error: (argument.type.incompatible)
+        throw new MyException(this);
+    }
+
+    EISOPIssue363a(String dummy) throws @UnderInitialization MyException {
+        throw new MyException(this, "UnderInitialization");
+    }
+
+    EISOPIssue363a(String dummy1, String dummy2) throws @UnderInitialization MyException {
+        throw new MyException(this, 0);
+    }
+
+    EISOPIssue363a(String dummy1, String dummy2, String dummy3)
+            throws @UnderInitialization MyException {
+        // :: error: (argument.type.incompatible)
+        throw new MyException(this);
+    }
+
+    void test1() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a(1);
+        } catch (MyException ex) {
+            ex.cause.field.toString();
+        }
+    }
+
+    void test2() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a();
+        } catch (@UnknownInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    void test3() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a();
+        } catch (@UnderInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    void test4() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a(1);
+        } catch (MyException ex) {
+            ex.cause.field.toString();
+        }
+    }
+
+    void test5() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a(1);
+        } catch (@UnknownInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    void test6() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a(1);
+        } catch (@UnderInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    void test7() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a("UnderInitialization");
+        } catch (MyException ex) {
+            ex.cause.field.toString();
+        }
+    }
+
+    void test8() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a("UnderInitialization");
+        } catch (@UnknownInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    void test9() {
+        try {
+            EISOPIssue363a obj = new EISOPIssue363a("UnderInitialization");
+        } catch (@UnderInitialization MyException ex) {
+            // :: error: (dereference.of.nullable)
+            ex.cause.field.toString();
+        }
+    }
+
+    <X extends Throwable> void throwIfInstanceOf(Throwable throwable, Class<X> declaredType)
+            throws X {
+        if (declaredType.isInstance(throwable)) {
+            throw declaredType.cast(throwable);
+        }
+    }
+}

checker/tests/initialization/EISOPIssue363b.java

@@ -0,0 +1,94 @@
+// Test multiple throw excetion in method signature for issue 363:
+// https://github.com/eisop/checker-framework/issues/363
+
+import org.checkerframework.checker.initialization.qual.NotOnlyInitialized;
+import org.checkerframework.checker.initialization.qual.UnderInitialization;
+import org.checkerframework.checker.initialization.qual.UnknownInitialization;
+
+public class EISOPIssue363b {
+    class MyException1 extends Exception {
+        @NotOnlyInitialized EISOPIssue363b cause;
+
+        MyException1(EISOPIssue363b cause) {
+            this.cause = cause;
+        }
+
+        MyException1(@UnderInitialization EISOPIssue363b cause, String dummy) {
+            this.cause = cause;
+        }
+
+        MyException1(@UnknownInitialization EISOPIssue363b cause, int dummy) {
+            this.cause = cause;
+        }
+    }
+
+    class MyException2 extends Exception {
+        @NotOnlyInitialized EISOPIssue363b cause;
+
+        MyException2(EISOPIssue363b cause) {
+            this.cause = cause;
+        }
+
+        MyException2(@UnderInitialization EISOPIssue363b cause, String dummy) {
+            this.cause = cause;
+        }
+
+        MyException2(@UnknownInitialization EISOPIssue363b cause, int dummy) {
+            this.cause = cause;
+        }
+    }
+
+    Object field;
+
+    EISOPIssue363b(int dummy) throws MyException1, MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException1(this, 0);
+    }
+
+    EISOPIssue363b(int dummy1, int dummy2) throws MyException1, MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException2(this, 0);
+    }
+
+    EISOPIssue363b(boolean dummy) throws @UnknownInitialization MyException1, MyException2 {
+        throw new MyException1(this, 0);
+    }
+
+    EISOPIssue363b(boolean dummy1, boolean dummy2)
+            throws @UnknownInitialization MyException1, MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException2(this, 0);
+    }
+
+    EISOPIssue363b(boolean dummy1, boolean dummy2, boolean dummy3)
+            throws MyException1, @UnknownInitialization MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException1(this, 0);
+    }
+
+    EISOPIssue363b(boolean dummy1, boolean dummy2, boolean dummy3, boolean dummy4)
+            throws MyException1, @UnknownInitialization MyException2 {
+        throw new MyException2(this, 0);
+    }
+
+    EISOPIssue363b(String dummy) throws @UnderInitialization MyException1, MyException2 {
+        throw new MyException1(this, "UnderInitialization");
+    }
+
+    EISOPIssue363b(String dummy1, String dummy2)
+            throws @UnderInitialization MyException1, MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException2(this, "UnderInitialization");
+    }
+
+    EISOPIssue363b(String dummy1, String dummy2, String dummy3)
+            throws MyException1, @UnderInitialization MyException2 {
+        // :: error: (throw.type.incompatible)
+        throw new MyException1(this, "UnderInitialization");
+    }
+
+    EISOPIssue363b(String dummy1, String dummy2, String dummy3, String dummy4)
+            throws MyException1, @UnderInitialization MyException2 {
+        throw new MyException2(this, "UnderInitialization");
+    }
+}

checker/tests/lock/TestTreeKinds.java

@@ -335,7 +335,7 @@ void testTreeTypes() {
         // throwing a guarded object - when throwing an exception, it must be @GuardedBy({}). Even
         // @GuardedByUnknown is not allowed.
         try {
-            // :: error: (throw.type.invalid)
+            // :: error: (throw.type.incompatible)
             throw exception;
         } catch (Exception e) {
         }

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -153,6 +153,7 @@
 import javax.lang.model.type.TypeKind;
 import javax.lang.model.type.TypeMirror;
 import javax.lang.model.util.ElementFilter;
+import javax.lang.model.util.Types;
 
 /* NO-AFU
    import org.checkerframework.common.wholeprograminference.WholeProgramInference;
@@ -3052,11 +3053,23 @@ private AnnotationMirrorSet getExceptionParameterLowerBoundAnnotationsCached() {
      * @param tree a CatchTree to check
      */
     protected void checkExceptionParameter(CatchTree tree) {
-        AnnotationMirrorSet requiredAnnotations =
+        Set<? extends AnnotationMirror> requiredAnnotations =
                 getExceptionParameterLowerBoundAnnotationsCached();
         VariableTree excParamTree = tree.getParameter();
         AnnotatedTypeMirror excParamType = atypeFactory.getAnnotatedType(excParamTree);
-
+        //        List<AnnotatedTypeMirror> exceptionList =
+        // atypeFactory.getAnnotatedType(methodTree).getThrownTypes();
+        //        if (methodTree != null && exceptionList != null) {
+        //            for (AnnotatedTypeMirror exception : exceptionList) {
+        //                Types typesUtil = atypeFactory.getProcessingEnv().getTypeUtils();
+        //                if (typesUtil.isSubtype(
+        //                        excParamType.getUnderlyingType(), exception.getUnderlyingType()))
+        // {
+        //                    requiredAnnotations = excParamType.getEffectiveAnnotations();
+        //                    break;
+        //                }
+        //            }
+        //        }
         for (AnnotationMirror required : requiredAnnotations) {
             AnnotationMirror found = excParamType.getAnnotationInHierarchy(required);
             assert found != null;
@@ -3116,15 +3129,35 @@ protected void checkThrownExpression(ThrowTree tree) {
         AnnotatedTypeMirror throwType = atypeFactory.getAnnotatedType(tree.getExpression());
         TypeMirror throwTM = throwType.getUnderlyingType();
         Set<? extends AnnotationMirror> required = getThrowUpperBoundAnnotations();
+        if (methodTree != null) {
+            List<AnnotatedTypeMirror> exceptionList =
+                    atypeFactory.getAnnotatedType(methodTree).getThrownTypes();
+            if (exceptionList != null) {
+                for (AnnotatedTypeMirror exception : exceptionList) {
+                    Types typesUtil = atypeFactory.getProcessingEnv().getTypeUtils();
+                    if (typesUtil.isSubtype(
+                            exception.getUnderlyingType(), throwType.getUnderlyingType())) {
+                        // use the type of the exception in the method signature if this exception
+                        // is a subtype of it, otherwise use top to permit runtime exceptions not
+                        // declared.
+                        required = exception.getEffectiveAnnotations();
+                        break;
+                    }
+                }
+            }
+        }
         switch (throwType.getKind()) {
             case NULL:
             case DECLARED:
             case TYPEVAR:
             case WILDCARD:
                 if (!typeHierarchy.isSubtypeShallowEffective(throwType, required)) {
-                    AnnotationMirrorSet found = throwType.getEffectiveAnnotations();
+                    AnnotationMirrorSet foundEffective = throwType.getEffectiveAnnotations();
                     checker.reportError(
-                            tree.getExpression(), "throw.type.invalid", found, required);
+                            tree.getExpression(),
+                            "throw.type.incompatible",
+                            foundEffective,
+                            required);
                 }
                 break;
 
@@ -3133,15 +3166,18 @@ protected void checkThrownExpression(ThrowTree tree) {
                 AnnotationMirrorSet foundPrimary = unionType.getAnnotations();
                 if (!qualHierarchy.isSubtypeShallow(foundPrimary, required, throwTM)) {
                     checker.reportError(
-                            tree.getExpression(), "throw.type.invalid", foundPrimary, required);
+                            tree.getExpression(),
+                            "throw.type.incompatible",
+                            foundPrimary,
+                            required);
                 }
                 for (AnnotatedTypeMirror altern : unionType.getAlternatives()) {
                     TypeMirror alternTM = altern.getUnderlyingType();
                     if (!qualHierarchy.isSubtypeShallow(
                             altern.getAnnotations(), required, alternTM)) {
                         checker.reportError(
                                 tree.getExpression(),
-                                "throw.type.invalid",
+                                "throw.type.incompatible",
                                 altern.getAnnotations(),
                                 required);
                     }