refine exception type of try-catch edges#134
Conversation
|
Previous PR #131. |
|
I rollback the code to the origin/master because in PR #131 , there is marker text-related modification that makes the PR not single-purposed, and then push to the remote repository so that the PR is closed automatically. |
…into cfg-try-catch-edges-refinement
|
@xingweitian Can you have a look at this PR? |
|
We were looking at the case of an expression When /cc @Nargeshdb |
…ypeMirror,Label>>
…into cfg-try-catch-edges-refinement
| TypeMirror caught = pair.first; | ||
| boolean canApply = false; | ||
|
|
||
| if (caught instanceof DeclaredType) { |
There was a problem hiding this comment.
What's the difference between caught instanceof DeclaredType and caught.getKind() == TypeKind.DECLARED?
There was a problem hiding this comment.
A union-type exception, like IOException | NullPointerException is DeclaredType. As a result, a catch block parameterized with a union-type exception will also fall into the if-branch.
| if (canApply) { | ||
| labels.add(pair.second); | ||
| } else { | ||
| assert false : "caught type must be a union or a declared type"; |
There was a problem hiding this comment.
It might be better to write throw new BugInCF("Caught type must be a union or a declared type."); here.
| // Add Throwable to account for unchecked exceptions | ||
| TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable"); | ||
| thrownSet.add(throwableElement.asType()); | ||
| // |
| * Given a type of thrown exception, add the set of possible control flow successor {@link | ||
| * Label}s to the argument set. Return true if the exception is known to be caught by one of | ||
| * those labels and false if it may propagate still further. | ||
| * Given a type of thrown exception, add to the argument set all possible pairs of the |
There was a problem hiding this comment.
It looks like this is redundant to https://github.com/opprop/checker-framework/pull/134/files#diff-852baab2528be0b3ea885d77fe6cdd8bR604. Can we remove it?
| /** | ||
| * Map from exception type to labels of successors that may be reached as a result of that | ||
| * exception. | ||
| * Set of all possible pairs of the refined exception type {@link TypeMirror} and the |
There was a problem hiding this comment.
Pairs of the refined exception types and the corresponding targets' labels?
Maybe remove {@link Label}? or change label to {@link Label}s.
| * | ||
| * @param node the node to hold | ||
| * @param exceptions the exceptions to hold | ||
| * @param exceptions set of all possible pairs of the refined exception type {@link |
There was a problem hiding this comment.
Same as above. Please have a look at all the appears.
| * <p>Return true if the exception is known to be caught by one of those labels and false if | ||
| * it may propagate still further. | ||
| * | ||
| * @param thrown the type of the exception that is declared to be thrown from a method |
There was a problem hiding this comment.
Remove . at the end of the line. @param and @return should not write . at the end of the line. Please change all the usages in this PR.
There was a problem hiding this comment.
Do we also need to update this? Is it still accurate enough? https://github.com/opprop/checker-framework/pull/134/files#diff-852baab2528be0b3ea885d77fe6cdd8bL579
dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java
Show resolved
Hide resolved
| * invocation, waiting to be refined. | ||
| * @param causeLabelPairs the set of all possible pairs of the refined exception type {@link | ||
| * TypeMirror} and the corresponding target's label {@link Label} that may be reached as | ||
| * a result of {@code thrown}. |
There was a problem hiding this comment.
A result of the current exception node?
…ixed `getTypeOfExtendsImplements` (opprop#134)
5 participants
This PR refines the type of exception for try-catch edges, which is shown as the label of each exceptional edge in CFG. The refinement is divided into two cases: (i) If thrown type is a subtype of caught type, then the edge is labeled the type of thrown type; (ii) If thrown type is a supertype of caught type, then the edge is labeled the type of caught type.