Java: Restrict Object.toString dispatch based on a more closed-world assumption.

java/ql/src/semmle/code/java/Collections.qll

@@ -10,12 +10,11 @@ import java
  */
 predicate instantiates(RefType t, GenericType g, int i, RefType arg) {
   t = g.getAParameterizedType() and
+  arg = t.(ParameterizedType).getTypeArgument(i)
+  or
+  t = g.getRawType() and
   exists(g.getTypeParameter(i)) and
-  (
-    arg = t.(ParameterizedType).getTypeArgument(i)
-    or
-    t instanceof RawType and arg instanceof TypeObject
-  )
+  arg instanceof TypeObject
 }
 
 /**
@@ -32,42 +31,18 @@ predicate instantiates(RefType t, GenericType g, int i, RefType arg) {
  *   with the `0`-th type parameter being `Integer` and the `1`-th type parameter being `V`.
  */
 predicate indirectlyInstantiates(RefType t, GenericType g, int i, RefType arg) {
-  exists(RefType tsrc | tsrc = t.getSourceDeclaration() |
-    // base case: `t` directly instantiates `g`
-    tsrc = g and instantiates(t, g, i, arg)
-    or
-    // inductive step
-    exists(RefType sup, RefType suparg |
-      // follow `extends`/`implements`
-      (extendsReftype(tsrc, sup) or implInterface(tsrc, sup)) and
-      // check whether the subtype instantiates `g`
-      indirectlyInstantiates(sup, g, i, suparg)
-    |
-      // if `t` is itself an instantiation of `tsrc` and `sup` instantiates
-      // `g` to one of the type parameters of `tsrc`, we return the corresponding
-      // instantiation in `t`
-      exists(int j | suparg = tsrc.(GenericType).getTypeParameter(j) |
-        instantiates(t, tsrc, j, arg)
-      )
-      or
-      // otherwise, we directly return `suparg`
-      not (
-        t = tsrc.(GenericType).getAParameterizedType() and
-        suparg = tsrc.(GenericType).getATypeParameter()
-      ) and
-      arg = suparg
-    )
+  instantiates(t, g, i, arg)
+  or
+  exists(RefType sup |
+    t.extendsOrImplements(sup) and
+    indirectlyInstantiates(sup, g, i, arg)
   )
 }
 
 /** A reference type that extends a parameterization of `java.util.Collection`. */
 class CollectionType extends RefType {
   CollectionType() {
-    exists(ParameterizedInterface coll |
-      coll.getSourceDeclaration().hasQualifiedName("java.util", "Collection")
-    |
-      this.hasSupertype*(coll)
-    )
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.util", "Collection")
   }
 
   /** Gets the type of elements stored in this collection. */

java/ql/src/semmle/code/java/Maps.qll

@@ -4,11 +4,7 @@ import Collections
 /** A reference type that extends a parameterization of `java.util.Map`. */
 class MapType extends RefType {
   MapType() {
-    exists(ParameterizedInterface coll |
-      coll.getSourceDeclaration().hasQualifiedName("java.util", "Map")
-    |
-      this.hasSupertype*(coll)
-    )
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.util", "Map")
   }
 
   /** Gets the type of keys stored in this map. */

java/ql/src/semmle/code/java/dataflow/TaintTracking.qll

@@ -15,6 +15,7 @@ private import semmle.code.java.frameworks.android.Intent
 private import semmle.code.java.frameworks.Guice
 private import semmle.code.java.frameworks.Protobuf
 private import semmle.code.java.Maps
+private import semmle.code.java.dataflow.internal.ContainerFlow
 
 module TaintTracking {
   /**
@@ -218,6 +219,8 @@ module TaintTracking {
       v.getAFirstUse() = sink
     )
     or
+    containerStep(src, sink)
+    or
     constructorStep(src, sink)
     or
     qualifierToMethodStep(src, sink)
@@ -353,10 +356,6 @@ module TaintTracking {
 
   /** Methods that passes tainted data from qualifier to argument. */
   private predicate taintPreservingQualifierToArgument(Method m, int arg) {
-    m instanceof CollectionMethod and
-    m.hasName("toArray") and
-    arg = 1
-    or
     m.getDeclaringType().hasQualifiedName("java.io", "ByteArrayOutputStream") and
     m.hasName("writeTo") and
     arg = 0
@@ -427,50 +426,6 @@ module TaintTracking {
     or
     m instanceof IntentGetExtraMethod
     or
-    m
-        .getDeclaringType()
-        .getSourceDeclaration()
-        .getASourceSupertype*()
-        .hasQualifiedName("java.util", "Map<>$Entry") and
-    m.hasName("getValue")
-    or
-    m
-        .getDeclaringType()
-        .getSourceDeclaration()
-        .getASourceSupertype*()
-        .hasQualifiedName("java.lang", "Iterable") and
-    m.hasName("iterator")
-    or
-    m
-        .getDeclaringType()
-        .getSourceDeclaration()
-        .getASourceSupertype*()
-        .hasQualifiedName("java.util", "Iterator") and
-    m.hasName("next")
-    or
-    m.getDeclaringType().getSourceDeclaration().hasQualifiedName("java.util", "Enumeration") and
-    m.hasName("nextElement")
-    or
-    m.(MapMethod).hasName("entrySet")
-    or
-    m.(MapMethod).hasName("get")
-    or
-    m.(MapMethod).hasName("remove")
-    or
-    m.(MapMethod).hasName("values")
-    or
-    m.(CollectionMethod).hasName("toArray")
-    or
-    m.(CollectionMethod).hasName("get")
-    or
-    m.(CollectionMethod).hasName("remove") and m.getParameterType(0).(PrimitiveType).hasName("int")
-    or
-    m.(CollectionMethod).hasName("subList")
-    or
-    m.(CollectionMethod).hasName("firstElement")
-    or
-    m.(CollectionMethod).hasName("lastElement")
-    or
     m.getDeclaringType().hasQualifiedName("java.nio", "ByteBuffer") and
     m.hasName("get")
     or
@@ -656,18 +611,6 @@ module TaintTracking {
     method.getDeclaringType().hasQualifiedName("java.io", "ByteArrayOutputStream") and
     method.hasName("write") and
     arg = 0
-    or
-    method.(MapMethod).hasName("put") and arg = 1
-    or
-    method.(MapMethod).hasName("putAll") and arg = 0
-    or
-    method.(CollectionMethod).hasName("add") and arg = method.getNumberOfParameters() - 1
-    or
-    method.(CollectionMethod).hasName("addAll") and arg = method.getNumberOfParameters() - 1
-    or
-    method.(CollectionMethod).hasName("addElement") and arg = 0
-    or
-    method.(CollectionMethod).hasName("set") and arg = 1
   }
 
   /** A comparison or equality test with a constant. */

java/ql/src/semmle/code/java/dataflow/internal/BaseSSA.qll

@@ -298,9 +298,139 @@ private module SsaImpl {
       )
     }
   }
+
+  private module AdjacentUsesImpl {
+    /**
+     * Holds if `rankix` is the rank the index `i` at which there is an SSA definition or explicit use of
+     * `v` in the basic block `b`.
+     */
+    private predicate defUseRank(BaseSsaSourceVariable v, BasicBlock b, int rankix, int i) {
+      i = rank[rankix](int j | any(TrackedSsaDef def).definesAt(v, b, j) or variableUse(v, _, b, j))
+    }
+
+    /** Gets the maximum rank index for the given variable and basic block. */
+    private int lastRank(BaseSsaSourceVariable v, BasicBlock b) {
+      result = max(int rankix | defUseRank(v, b, rankix, _))
+    }
+
+    /** Holds if `v` is defined or used in `b`. */
+    private predicate varOccursInBlock(BaseSsaSourceVariable v, BasicBlock b) {
+      defUseRank(v, b, _, _)
+    }
+
+    /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */
+    private predicate blockPrecedesVar(BaseSsaSourceVariable v, BasicBlock b) {
+      varOccursInBlock(v, b.getABBSuccessor*())
+    }
+
+    /**
+     * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
+     * in `b2` or one of its transitive successors but not in any block on the path
+     * between `b1` and `b2`.
+     */
+    private predicate varBlockReaches(BaseSsaSourceVariable v, BasicBlock b1, BasicBlock b2) {
+      varOccursInBlock(v, b1) and b2 = b1.getABBSuccessor()
+      or
+      exists(BasicBlock mid |
+        varBlockReaches(v, b1, mid) and
+        b2 = mid.getABBSuccessor() and
+        not varOccursInBlock(v, mid) and
+        blockPrecedesVar(v, b2)
+      )
+    }
+
+    /**
+     * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
+     * `b2` but not in any block on the path between `b1` and `b2`.
+     */
+    private predicate varBlockStep(BaseSsaSourceVariable v, BasicBlock b1, BasicBlock b2) {
+      varBlockReaches(v, b1, b2) and
+      varOccursInBlock(v, b2)
+    }
+
+    /**
+     * Holds if `v` occurs at index `i1` in `b1` and at index `i2` in `b2` and
+     * there is a path between them without any occurrence of `v`.
+     */
+    predicate adjacentVarRefs(BaseSsaSourceVariable v, BasicBlock b1, int i1, BasicBlock b2, int i2) {
+      exists(int rankix |
+        b1 = b2 and
+        defUseRank(v, b1, rankix, i1) and
+        defUseRank(v, b2, rankix + 1, i2)
+      )
+      or
+      defUseRank(v, b1, lastRank(v, b1), i1) and
+      varBlockStep(v, b1, b2) and
+      defUseRank(v, b2, 1, i2)
+    }
+  }
+  private import AdjacentUsesImpl
+
+  /**
+   * Holds if the value defined at `def` can reach `use` without passing through
+   * any other uses, but possibly through phi nodes.
+   */
+  cached
+  predicate firstUse(TrackedSsaDef def, RValue use) {
+    exists(BaseSsaSourceVariable v, BasicBlock b1, int i1, BasicBlock b2, int i2 |
+      adjacentVarRefs(v, b1, i1, b2, i2) and
+      def.definesAt(v, b1, i1) and
+      variableUse(v, use, b2, i2)
+    )
+    or
+    exists(
+      BaseSsaSourceVariable v, TrackedSsaDef redef, BasicBlock b1, int i1, BasicBlock b2, int i2
+    |
+      redef instanceof BaseSsaPhiNode
+    |
+      adjacentVarRefs(v, b1, i1, b2, i2) and
+      def.definesAt(v, b1, i1) and
+      redef.definesAt(v, b2, i2) and
+      firstUse(redef, use)
+    )
+  }
+
+  cached
+  module SsaPublic {
+    /**
+     * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
+     * variable, that is, the value read in `use1` can reach `use2` without passing
+     * through any other use or any SSA definition of the variable.
+     */
+    cached
+    predicate baseSsaAdjacentUseUseSameVar(RValue use1, RValue use2) {
+      exists(BaseSsaSourceVariable v, BasicBlock b1, int i1, BasicBlock b2, int i2 |
+        adjacentVarRefs(v, b1, i1, b2, i2) and
+        variableUse(v, use1, b1, i1) and
+        variableUse(v, use2, b2, i2)
+      )
+    }
+
+    /**
+     * Holds if `use1` and `use2` form an adjacent use-use-pair of the same
+     * `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
+     * without passing through any other use or any SSA definition of the variable
+     * except for phi nodes.
+     */
+    cached
+    predicate baseSsaAdjacentUseUse(RValue use1, RValue use2) {
+      baseSsaAdjacentUseUseSameVar(use1, use2)
+      or
+      exists(
+        BaseSsaSourceVariable v, TrackedSsaDef def, BasicBlock b1, int i1, BasicBlock b2, int i2
+      |
+        adjacentVarRefs(v, b1, i1, b2, i2) and
+        variableUse(v, use1, b1, i1) and
+        def.definesAt(v, b2, i2) and
+        firstUse(def, use2) and
+        def instanceof BaseSsaPhiNode
+      )
+    }
+  }
 }
 private import SsaImpl
 private import SsaDefReaches
+import SsaPublic
 
 private newtype TBaseSsaVariable =
   TSsaPhiNode(BaseSsaSourceVariable v, BasicBlock b) { phiNode(v, b) } or
@@ -354,6 +484,16 @@ class BaseSsaVariable extends TBaseSsaVariable {
   /** Gets an access of this SSA variable. */
   RValue getAUse() { ssaDefReachesUse(_, this, result) }
 
+  /**
+   * Gets an access of the SSA source variable underlying this SSA variable
+   * that can be reached from this SSA variable without passing through any
+   * other uses, but potentially through phi nodes.
+   *
+   * Subsequent uses can be found by following the steps defined by
+   * `baseSsaAdjacentUseUse`.
+   */
+  RValue getAFirstUse() { firstUse(this, result) }
+
   /** Holds if this SSA variable is live at the end of `b`. */
   predicate isLiveAtEndOfBlock(BasicBlock b) { ssaDefReachesEndOfBlock(_, this, b) }
 

java/ql/src/semmle/code/java/dataflow/internal/ContainerFlow.qll

@@ -0,0 +1,170 @@
+import java
+import semmle.code.java.Collections
+import semmle.code.java.Maps
+
+private class EntryType extends RefType {
+  EntryType() {
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.util", "Map<>$Entry")
+  }
+
+  RefType getValueType() {
+    exists(GenericType t | t.hasQualifiedName("java.util", "Map<>$Entry") |
+      indirectlyInstantiates(this, t, 1, result)
+    )
+  }
+}
+
+private class IterableType extends RefType {
+  IterableType() {
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.lang", "Iterable")
+  }
+
+  RefType getElementType() {
+    exists(GenericType t | t.hasQualifiedName("java.lang", "Iterable") |
+      indirectlyInstantiates(this, t, 0, result)
+    )
+  }
+}
+
+private class IteratorType extends RefType {
+  IteratorType() {
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.util", "Iterator")
+  }
+
+  RefType getElementType() {
+    exists(GenericType t | t.hasQualifiedName("java.util", "Iterator") |
+      indirectlyInstantiates(this, t, 0, result)
+    )
+  }
+}
+
+private class EnumerationType extends RefType {
+  EnumerationType() {
+    this.getSourceDeclaration().getASourceSupertype*().hasQualifiedName("java.util", "Enumeration")
+  }
+
+  RefType getElementType() {
+    exists(GenericType t | t.hasQualifiedName("java.util", "Enumeration") |
+      indirectlyInstantiates(this, t, 0, result)
+    )
+  }
+}
+
+/**
+ * A type that acts as a container. This includes collections, maps, iterators,
+ * iterables, enumerations, and map entry pairs. For maps and map entry pairs
+ * only the value component is considered to act as a container.
+ */
+class ContainerType extends RefType {
+  ContainerType() {
+    this instanceof EntryType or
+    this instanceof IterableType or
+    this instanceof IteratorType or
+    this instanceof EnumerationType or
+    this instanceof MapType or
+    this instanceof CollectionType
+  }
+
+  /** Gets the type of the contained elements. */
+  RefType getElementType() {
+    result = this.(EntryType).getValueType() or
+    result = this.(IterableType).getElementType() or
+    result = this.(IteratorType).getElementType() or
+    result = this.(EnumerationType).getElementType() or
+    result = this.(MapType).getValueType() or
+    result = this.(CollectionType).getElementType()
+  }
+
+  /**
+   * Gets the type of the contained elements or its upper bound if the type is
+   * a type variable or wildcard.
+   */
+  RefType getElementTypeBound() {
+    exists(RefType e | e = this.getElementType() |
+      result = e and not e instanceof BoundedType
+      or
+      result = e.(BoundedType).getAnUltimateUpperBoundType()
+    )
+  }
+}
+
+private predicate taintPreservingQualifierToMethod(Method m) {
+  m.getDeclaringType() instanceof EntryType and
+  m.hasName("getValue")
+  or
+  m.getDeclaringType() instanceof IterableType and
+  m.hasName("iterator")
+  or
+  m.getDeclaringType() instanceof IteratorType and
+  m.hasName("next")
+  or
+  m.getDeclaringType() instanceof EnumerationType and
+  m.hasName("nextElement")
+  or
+  m.(MapMethod).hasName("entrySet")
+  or
+  m.(MapMethod).hasName("get")
+  or
+  m.(MapMethod).hasName("remove")
+  or
+  m.(MapMethod).hasName("values")
+  or
+  m.(CollectionMethod).hasName("toArray")
+  or
+  m.(CollectionMethod).hasName("get")
+  or
+  m.(CollectionMethod).hasName("remove") and m.getParameterType(0).(PrimitiveType).hasName("int")
+  or
+  m.(CollectionMethod).hasName("subList")
+  or
+  m.(CollectionMethod).hasName("firstElement")
+  or
+  m.(CollectionMethod).hasName("lastElement")
+}
+
+private predicate qualifierToMethodStep(Expr tracked, MethodAccess sink) {
+  taintPreservingQualifierToMethod(sink.getMethod()) and
+  tracked = sink.getQualifier()
+}
+
+private predicate qualifierToArgumentStep(Expr tracked, RValue sink) {
+  exists(MethodAccess ma |
+    ma.getMethod().(CollectionMethod).hasName("toArray") and
+    tracked = ma.getQualifier() and
+    sink = ma.getArgument(1)
+  )
+}
+
+private predicate taintPreservingArgumentToQualifier(Method method, int arg) {
+  method.(MapMethod).hasName("put") and arg = 1
+  or
+  method.(MapMethod).hasName("putAll") and arg = 0
+  or
+  method.(CollectionMethod).hasName("add") and arg = method.getNumberOfParameters() - 1
+  or
+  method.(CollectionMethod).hasName("addAll") and arg = method.getNumberOfParameters() - 1
+  or
+  method.(CollectionMethod).hasName("addElement") and arg = 0
+  or
+  method.(CollectionMethod).hasName("set") and arg = 1
+}
+
+private predicate argToQualifierStep(Expr tracked, Expr sink) {
+  exists(Method m, int i, MethodAccess ma |
+    taintPreservingArgumentToQualifier(m, i) and
+    ma.getMethod() = m and
+    tracked = ma.getArgument(i) and
+    sink = ma.getQualifier()
+  )
+}
+
+/**
+ * Holds if the step from `n1` to `n2` is either extracting a value from a
+ * container, inserting a value into a container, or transforming one container
+ * to another.
+ */
+predicate containerStep(Expr n1, Expr n2) {
+  qualifierToMethodStep(n1, n2) or
+  qualifierToArgumentStep(n1, n2) or
+  argToQualifierStep(n1, n2)
+}

java/ql/src/semmle/code/java/dispatch/ObjFlow.qll

@@ -0,0 +1,326 @@
+import java
+private import VirtualDispatch
+private import semmle.code.java.controlflow.Guards
+private import semmle.code.java.dataflow.internal.BaseSSA
+private import semmle.code.java.dataflow.internal.DataFlowUtil
+private import semmle.code.java.dataflow.internal.DataFlowPrivate
+private import semmle.code.java.dataflow.internal.ContainerFlow
+
+/**
+ * Gets a viable dispatch target for `ma`. This is the input dispatch relation.
+ */
+private Method viableImpl_inp(MethodAccess ma) { result = viableImpl_v3(ma) }
+
+private Callable dispatchCand(Call c) {
+  c instanceof ConstructorCall and result = c.getCallee().getSourceDeclaration()
+  or
+  result = viableImpl_inp(c)
+}
+
+/**
+ * Holds if `p` is the `i`th parameter of a viable dispatch target of `call`.
+ * The instance parameter is considered to have index `-1`.
+ */
+pragma[nomagic]
+private predicate viableParam(Call call, int i, ParameterNode p) {
+  exists(Callable callable |
+    callable = dispatchCand(call) and
+    p.isParameterOf(callable, i)
+  )
+}
+
+/**
+ * Holds if `arg` is a possible argument to `p` taking virtual dispatch into account.
+ */
+private predicate viableArgParam(ArgumentNode arg, ParameterNode p) {
+  exists(int i, Call call |
+    viableParam(call, i, p) and
+    arg.argumentOf(call, i)
+  )
+}
+
+private predicate returnStep(Node n1, Node n2) {
+  exists(ReturnStmt ret, Method m |
+    ret.getEnclosingCallable() = m and
+    ret.getResult() = n1.asExpr() and
+    m = dispatchCand(n2.asExpr())
+  )
+}
+
+/**
+ * Holds if data may flow from `n1` to `n2` in a single step through a call or a return.
+ */
+private predicate callFlowStep(Node n1, Node n2) {
+  returnStep(n1, n2) or
+  viableArgParam(n1, n2)
+}
+
+/**
+ * Holds if data may flow from `n1` to `n2` in a single step through local
+ * flow, calls, returns, fields, array reads or writes, or container taint steps.
+ */
+private predicate step(Node n1, Node n2) {
+  exists(BaseSsaVariable v, BaseSsaVariable def |
+    def.(BaseSsaUpdate).getDefiningExpr().(VariableAssign).getSource() = n1.asExpr()
+    or
+    def.(BaseSsaImplicitInit).isParameterDefinition(n1.asParameter())
+    or
+    exists(EnhancedForStmt for |
+      for.getVariable() = def.(BaseSsaUpdate).getDefiningExpr() and
+      for.getExpr() = n1.asExpr()
+    )
+  |
+    v.getAnUltimateDefinition() = def and
+    v.getAUse() = n2.asExpr()
+  )
+  or
+  baseSsaAdjacentUseUse(n1.asExpr(), n2.asExpr())
+  or
+  exists(Callable c | n1.(InstanceParameterNode).getCallable() = c |
+    exists(InstanceAccess ia |
+      ia = n2.asExpr() and ia.getEnclosingCallable() = c and ia.isOwnInstanceAccess()
+    )
+    or
+    n2.(ImplicitInstanceAccess).getInstanceAccess().(OwnInstanceAccess).getEnclosingCallable() = c
+  )
+  or
+  exists(Field f |
+    f.getAnAssignedValue() = n1.asExpr() and
+    n2.asExpr().(FieldRead).getField() = f
+  )
+  or
+  n2.asExpr().(ParExpr).getExpr() = n1.asExpr()
+  or
+  n2.asExpr().(CastExpr).getExpr() = n1.asExpr()
+  or
+  n2.asExpr().(ConditionalExpr).getTrueExpr() = n1.asExpr()
+  or
+  n2.asExpr().(ConditionalExpr).getFalseExpr() = n1.asExpr()
+  or
+  n2.asExpr().(AssignExpr).getSource() = n1.asExpr()
+  or
+  n2.asExpr().(ArrayInit).getAnInit() = n1.asExpr()
+  or
+  n2.asExpr().(ArrayCreationExpr).getInit() = n1.asExpr()
+  or
+  n2.asExpr().(ArrayAccess).getArray() = n1.asExpr()
+  or
+  exists(Argument arg |
+    n1.asExpr() = arg and arg.isVararg() and n2.(ImplicitVarargsArray).getCall() = arg.getCall()
+  )
+  or
+  exists(AssignExpr a, Field v |
+    a.getSource() = n1.asExpr() and
+    a.getDest().(ArrayAccess).getArray() = v.getAnAccess() and
+    n2.asExpr() = v.getAnAccess().(RValue)
+  )
+  or
+  exists(AssignExpr a |
+    a.getSource() = n1.asExpr() and
+    a.getDest().(ArrayAccess).getArray() = n2.asExpr()
+  )
+  or
+  callFlowStep(n1, n2) and not containerStep(_, n2.asExpr())
+  or
+  containerStep(n1.asExpr(), n2.asExpr())
+  or
+  exists(Field v |
+    containerStep(n1.asExpr(), v.getAnAccess()) and
+    n2.asExpr() = v.getAnAccess()
+  )
+}
+
+/**
+ * Gets the type contained by `t` in the sense of element types of arrays and
+ * collections and upper bounds of type variables and wildcards.
+ *
+ * For example, given `Collection<? extends Foo[]>` the type `Foo` is returned.
+ */
+private RefType getContainedType(RefType t) {
+  not t instanceof Array and
+  not t instanceof ContainerType and
+  not t instanceof BoundedType and
+  result = t
+  or
+  result = getContainedType(t.(Array).getElementType())
+  or
+  result = getContainedType(t.(ContainerType).getElementType())
+  or
+  result = getContainedType(t.(BoundedType).getFirstUpperBoundType())
+}
+
+/**
+ * Holds if `t` can carry a value for which `t` reveals no type information,
+ * possibly nested in an array or container.
+ */
+private predicate containsObj(RefType t) {
+  t instanceof TypeObject
+  or
+  exists(RefType r | containsObj(r) and t = r.getASourceSupertype())
+  or
+  containsObj(getContainedType(t))
+}
+
+/**
+ * A node that can carry a value for which the static type reveals no type
+ * information other than `Object`.
+ */
+private class ObjNode extends Node {
+  ObjNode() { containsObj(this.getTypeBound()) }
+}
+
+private predicate objStep(ObjNode n1, ObjNode n2) { step(n1, n2) }
+
+/**
+ * Holds if `n` has discarded the type information `t`.
+ */
+private predicate source(RefType t, ObjNode n) {
+  exists(Node n1, RefType nt |
+    not n1 instanceof ObjNode and
+    nt = n1.getTypeBound() and
+    step(n1, n) and
+    t = getContainedType(nt)
+  )
+}
+
+/**
+ * Holds if `n` is the qualifier of an `Object.toString()` call.
+ */
+private predicate sink(ObjNode n) {
+  exists(MethodAccess toString |
+    toString.getQualifier() = n.asExpr() and
+    toString.getMethod().hasName("toString")
+  ) and
+  n.getTypeBound().getErasure() instanceof TypeObject
+}
+
+private predicate relevantNodeBack(ObjNode n) {
+  sink(n)
+  or
+  exists(ObjNode mid | objStep(n, mid) and relevantNodeBack(mid))
+}
+
+private predicate relevantNode(ObjNode n) {
+  source(_, n) and relevantNodeBack(n)
+  or
+  exists(ObjNode mid | relevantNode(mid) and objStep(mid, n) and relevantNodeBack(n))
+}
+
+pragma[noinline]
+private predicate objStepPruned(ObjNode n1, ObjNode n2) {
+  objStep(n1, n2) and relevantNode(n1) and relevantNode(n2)
+}
+
+private predicate stepPlus(Node n1, Node n2) = fastTC(objStepPruned/2)(n1, n2)
+
+/**
+ * Holds if the qualifier `n` of an `Object.toString()` call might have type `t`.
+ */
+pragma[noopt]
+private predicate objType(ObjNode n, RefType t) {
+  exists(ObjNode n2 |
+    sink(n) and
+    (stepPlus(n2, n) or n2 = n) and
+    source(t, n2)
+  )
+}
+
+private VirtualMethodAccess objectToString(ObjNode n) {
+  result.getQualifier() = n.asExpr() and sink(n)
+}
+
+/**
+ * Holds if the qualifier of the `Object.toString()` call `ma` might have type `t`.
+ */
+private predicate objectToStringQualType(MethodAccess ma, RefType t) {
+  exists(ObjNode n | ma = objectToString(n) and objType(n, t))
+}
+
+private Method viableImplObjectToString(MethodAccess ma) {
+  exists(Method def, RefType t |
+    objectToStringQualType(ma, t) and
+    def = ma.getMethod() and
+    exists(RefType t2 |
+      result = viableMethodImpl(def, t.getSourceDeclaration(), t2) and
+      not Unification::failsUnification(t, t2)
+    )
+  )
+}
+
+/**
+ * Gets a viable dispatch target for `ma`. This is the output dispatch relation.
+ *
+ * The set of dispatch targets for `Object.toString()` calls are reduced based
+ * on possibly data flow from objects of more specific types to the qualifier.
+ */
+Method viableImpl_out(MethodAccess ma) {
+  result = viableImpl_inp(ma) and
+  (
+    result = viableImplObjectToString(ma) or
+    not ma = objectToString(_)
+  )
+}
+
+private module Unification {
+  pragma[noinline]
+  private predicate unificationTargetLeft(ParameterizedType t1, GenericType g) {
+    objectToStringQualType(_, t1) and t1.getGenericType() = g
+  }
+
+  pragma[noinline]
+  private predicate unificationTargetRight(ParameterizedType t2, GenericType g) {
+    exists(viableMethodImpl(_, _, t2)) and t2.getGenericType() = g
+  }
+
+  private predicate unificationTargets(Type t1, Type t2) {
+    exists(GenericType g | unificationTargetLeft(t1, g) and unificationTargetRight(t2, g))
+    or
+    exists(Array a1, Array a2 |
+      unificationTargets(a1, a2) and
+      t1 = a1.getComponentType() and
+      t2 = a2.getComponentType()
+    )
+    or
+    exists(ParameterizedType pt1, ParameterizedType pt2, int pos |
+      unificationTargets(pt1, pt2) and
+      not pt1.getSourceDeclaration() != pt2.getSourceDeclaration() and
+      t1 = pt1.getTypeArgument(pos) and
+      t2 = pt2.getTypeArgument(pos)
+    )
+  }
+
+  pragma[noinline]
+  private predicate typeArgsOfUnificationTargets(
+    ParameterizedType t1, ParameterizedType t2, int pos, RefType arg1, RefType arg2
+  ) {
+    unificationTargets(t1, t2) and
+    arg1 = t1.getTypeArgument(pos) and
+    arg2 = t2.getTypeArgument(pos)
+  }
+
+  predicate failsUnification(Type t1, Type t2) {
+    unificationTargets(t1, t2) and
+    (
+      exists(RefType arg1, RefType arg2 |
+        typeArgsOfUnificationTargets(t1, t2, _, arg1, arg2) and
+        failsUnification(arg1, arg2)
+      )
+      or
+      failsUnification(t1.(Array).getComponentType(), t2.(Array).getComponentType())
+      or
+      not (
+        t1 instanceof Array and t2 instanceof Array
+        or
+        t1.(PrimitiveType) = t2.(PrimitiveType)
+        or
+        t1.(Class).getSourceDeclaration() = t2.(Class).getSourceDeclaration()
+        or
+        t1.(Interface).getSourceDeclaration() = t2.(Interface).getSourceDeclaration()
+        or
+        t1 instanceof BoundedType and t2 instanceof RefType
+        or
+        t1 instanceof RefType and t2 instanceof BoundedType
+      )
+    )
+  }
+}

java/ql/src/semmle/code/java/dispatch/VirtualDispatch.qll

@@ -1,6 +1,7 @@
 import java
 import semmle.code.java.dataflow.TypeFlow
 private import DispatchFlow as DispatchFlow
+private import ObjFlow as ObjFlow
 private import semmle.code.java.dataflow.internal.BaseSSA
 private import semmle.code.java.controlflow.Guards
 
@@ -41,7 +42,15 @@ cached
 private module Dispatch {
   /** Gets a viable implementation of the method called in the given method access. */
   cached
-  Method viableImpl(MethodAccess ma) { result = DispatchFlow::viableImpl_out(ma) }
+  Method viableImpl(MethodAccess ma) { result = ObjFlow::viableImpl_out(ma) }
+
+  /**
+   * INTERNAL: Use `viableImpl` instead.
+   *
+   * Gets a viable implementation of the method called in the given method access.
+   */
+  cached
+  Method viableImpl_v3(MethodAccess ma) { result = DispatchFlow::viableImpl_out(ma) }
 
   private predicate qualType(VirtualMethodAccess ma, RefType t, boolean exact) {
     exprTypeFlow(ma.getQualifier(), t, exact)