typetools
Model possible `MatchException`s in control-flow graphs
In various cases, recent Java language constructs like switch expressions may throw a MatchException even when the matching is statically checked to be exhaustive. E.g., this can happen due to separate compilation, where more cases exist in an enum at runtime than were visible at compile time; see the MatchException javadoc for more examples. Currently I don't believe these MatchException cases are modeled by the control-flow graphs generated by the Checker Framework. E.g., I don't see any MatchException case for this test, but you can see the MatchException cases get generated in the bytecodes for a simplified version.
At some point, it would be good to handle at least some cases where MatchExceptions can be thrown, for soundness.
You are right that there are things that can happen at run time that should be impossible, per a compile-time analysis -- and that are impossible, if parts of the program are not changed incompatibly after compilation. This has not been a priority for us so far, but added enum elements are more a compelling example than most. Thanks for brining it up.
Thinking more, this is probably low priority. The reason I reported this was that in looking at the control-flow graph for the test case I didn't even see the second pattern WrappedBoolean(_) present anywhere at the end (see the CFG here). I think maybe it's because CF thinks that is the default branch and optimizes out the pattern match? But that doesn't really reflect the runtime logic, since there is another MatchException case and the code does check for a match. But maybe for static analysis it's not that critical to get this exactly right. More concerning is unsoundness like #7032, but possibly that is unrelated to this issue.