Java: Implement union type flow and replace ad-hoc variable tracking in dispatch #10334

aschackmull · 2022-09-07T13:11:02Z

This provides a proper replacement for the ad-hoc pre-SSA variable tracking that dispatch used to rely on.

Union types arising from disjunctive instanceof checks are ~~left as future work~~ also supported.

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

hvitved

Looks awesome! I have some questions.

hvitved · 2022-09-13T12:22:03Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+/**
+ * Holds if `n` has type `t` and this information is discarded, such that `t`
+ * might be a better type bound for nodes where `n` flows to. This only includes
+ * the best such bound for each node.


This comment suggests that there is at most one best bound; could there be multiple (two types where neither is a sub type of the other)?

It is possible to have multiple best bounds, yes. But it is fairly rare, to the point where we mostly ignore the possibility.

hvitved · 2022-09-13T12:23:13Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+    te = t.getErasure() and
+    not exists(RefType better |
+      typeFlowBaseCand(n, better) and
+      better != t and


Isn't this implied from the two disjuncts after the |?

The trickiness is that there can be loops in the subtyping relation.

hvitved · 2022-09-13T12:27:49Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+}
+
+/**
+ * Holds if `ioe` checks `v`, its true-successor is `bb`, and `bb` has 2 or more


Perhaps "2 or more" -> "multiple"

hvitved · 2022-09-13T12:28:22Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+ */
+private predicate instanceofDisjunct(InstanceOfExpr ioe, BasicBlock bb, BaseSsaVariable v) {
+  ioe.getExpr() = v.getAUse() and
+  strictcount(bb.getABBPredecessor()) > 1 and


I forget, is something like not exists(unique(...)) more efficient?

With the additional negation, I'd guess not. And strictcount is certainly efficient enough that I think this sort of tweak would lie firmly in the realm of micro-optimisations that's best handled by the optimiser.

hvitved · 2022-09-13T12:32:06Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+  exists(ConditionBlock cb | cb.getCondition() = ioe and cb.getTestSuccessor(true) = bb)
+}
+
+/** Holds if `bb` is disjunctively guarded by two or more `instanceof` tests on `v`. */


Again, multiple

hvitved · 2022-09-13T13:03:36Z

java/ql/test/library-tests/typeflow/uniontypeflow.expected

+| UnionTypes.java:11:5:11:5 | m | 2 | ConcurrentHashMap<String,String> | false |
+| UnionTypes.java:11:5:11:5 | m | 2 | LinkedHashMap<String,String> | false |
+| UnionTypes.java:26:10:26:10 | x | 2 | A2 | true |
+| UnionTypes.java:26:10:26:10 | x | 2 | A3 | false |


Why is this not true?

Because A3 has no subtypes - in those cases we just report upper bounds and don't bother with the lower bounds.

hvitved · 2022-09-13T13:12:47Z

java/ql/lib/semmle/code/java/dataflow/internal/DataFlowDispatch.qll

+        exprTypeFlow(arg, srctype, exact)
+        or
+        not exprTypeFlow(arg, _, _) and
+        exprUnionTypeFlow(arg, srctype, exact)


It would be nice with a data flow test that exhibits this; i.e., a call context that provides a disjunctive type bound, which is better than the disjunctive type bound inside the callee.

hvitved · 2022-09-13T13:16:39Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+    or
+    exists(TypeFlowNode mid | step(mid, n) and hasUnionTypeFlow(mid))
+    or
+    instanceofDisjunctionGuarded(n, _)


Should this rather be part of unionTypeFlowBaseCand?

No, because unionTypeFlowBaseCand consists of nodes that have a single bound that may downstream be combined to disjunctive bounds, whereas instanceofDisjunctionGuarded is already a disjunctive bound.

hvitved · 2022-09-13T13:23:43Z

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll

+    unionTypeFlow(n, weaker, false) and
+    t.getASupertype*() = weaker
+  |
+    exact = true or not weaker.getASupertype*() = t


I don't quite understand why this restriction is there.

We're trying to determine whether we can reduce A | B | ... to just B | .... We can do this either if B is a strictly weaker type than A or if A and B are similar types only distinguished by A being exact and B being an upper bound. Note that we have to be careful not to drop both A and B at the same time if they are equivalent types (in that case we could drop one of them, but that requires an arbitrary choice, which is tricky, so we don't bother with that case).

Ok, I guess this is again because sub typing is not acyclic.

aschackmull · 2022-09-14T08:39:36Z

Looks awesome! I have some questions.

I think I've addressed everything.

aschackmull requested a review from a team as a code owner September 7, 2022 13:11

github-actions bot added the Java label Sep 7, 2022

github-advanced-security bot found potential problems Sep 7, 2022

View reviewed changes

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll Fixed Show fixed Hide fixed

java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll Fixed Show fixed Hide fixed

aschackmull added 9 commits September 13, 2022 13:30

Java: Add dispatch test showing lack of union types.

85d4742

Java: Minor TypeFlow tweaks.

7692a9e

Java: Implement union type flow.

6f06267

Java: Replace ad-hoc variable tracking with union type flow in dispatch.

a8eedce

Java: Replace uses of deprecated variableTrack.

c8b93e0

Java: Fix perf issue.

686e03e

Java: Support instanceof disjunction in union type flow.

d0f7052

Java: extend typeflow tests to cover union types.

0e376b3

Java: Fix test expectation.

b8a1818

aschackmull force-pushed the java/uniontypeflow branch from 73363c1 to b8a1818 Compare September 13, 2022 11:30

aschackmull added the no-change-note-required This PR does not need a change note label Sep 13, 2022

hvitved reviewed Sep 13, 2022

View reviewed changes

aschackmull added 3 commits September 14, 2022 10:16

Java: Adjust qldoc.

83e7bf7

Java: convert test to inline expectation

9f20063

Java: Add test for disjunctive type in call context.

64e2f41

hvitved approved these changes Sep 14, 2022

View reviewed changes

aschackmull merged commit d713910 into github:main Sep 14, 2022

aschackmull deleted the java/uniontypeflow branch September 14, 2022 11:34

Java: Implement union type flow and replace ad-hoc variable tracking in dispatch #10334

Java: Implement union type flow and replace ad-hoc variable tracking in dispatch #10334

Uh oh!

Conversation

aschackmull commented Sep 7, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

hvitved left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

aschackmull commented Sep 14, 2022

Uh oh!

Uh oh!

aschackmull commented Sep 7, 2022 •

edited

Loading