Java: Support SCCs in TypeFlow. #10240
Conversation
|
dca looks harmless. |
| * this HOP is not currently supported for newtypes. | ||
| * | ||
| * A straightforward implementation would be: | ||
| * ``` |
| * ``` | ||
| * but this is quadratic in the size of the SCCs. | ||
| * | ||
| * Instead we find local maxima and determine the SCC representatives from those. |
There was a problem hiding this comment.
mention that locality means adjacency in the SCC graph
|
|
||
| private predicate sccEdge(TypeFlowNode n1, TypeFlowNode n2) { anyStep(n1, n2) and anyStep+(n2, n1) } | ||
|
|
||
| /* |
There was a problem hiding this comment.
Perhaps add all the SCC related stuff in a private module, and let this comment be QL doc for that module.
| ( | ||
| r = 1 and candJoinType(n, t) | ||
| or | ||
| flowJoin(r - 1, n, t) and Edge::edgeRank(r, _, n) |
There was a problem hiding this comment.
Can the edgeRank conjunct be removed if the forall below becomes a forex?
There was a problem hiding this comment.
Semantically, yes. But the codegen will be worse. A forex(vars | range | term) currently desugars to exists(vars | range | term) and forall(vars | range | term) so that would give an additional recursive call (which we might or might not be lucky enough to have the optimiser deduplicate at the RA level after join-ordering, since the delta of a forall is equal to the delta of a forex).
| ) | ||
| } | ||
|
|
||
| private predicate edgeRank2(int r2, int r1, TypeFlowNode n) { |
There was a problem hiding this comment.
As discussed offline, I think this predicate deserves a comment.
TypeFlow is calculating type bounds through universal flow, and thus uses recursion through forall. Least fixpoint semantics means that we previously didn't get any bounds for SCCs. This PR fixes this by applying SCC reduction and calculating type bounds on the resulting DAG. This improves virtual dispatch precision.
The existing recursion-through-forall-by-way-of-edge-ranking is refactored into a parameterised module.