Merge pull request #16785 from aschackmull/dataflow/stage3-notypes

Dataflow: Replace stage 3 type pruning with flow-insensitive type pruning.
This commit is contained in:
Anders Schack-Mulligen
2024-06-24 15:21:37 +02:00
committed by GitHub
11 changed files with 107 additions and 67 deletions

View File

@@ -216,7 +216,7 @@ predicate localMustFlowStep(Node node1, Node node2) { none() }
/** Gets the type of `n` used for type pruning. */
Type getNodeType(Node n) {
suppressUnusedNode(n) and
exists(n) and
result instanceof VoidType // stub implementation
}
@@ -227,13 +227,10 @@ string ppReprType(Type t) { none() } // stub implementation
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(Type t1, Type t2) {
any() // stub implementation
t1 instanceof VoidType and t2 instanceof VoidType // stub implementation
}
private predicate suppressUnusedNode(Node n) { any() }
//////////////////////////////////////////////////////////////////////////////
// Java QL library compatibility wrappers
//////////////////////////////////////////////////////////////////////////////

View File

@@ -988,7 +988,7 @@ predicate localMustFlowStep(Node node1, Node node2) { none() }
/** Gets the type of `n` used for type pruning. */
DataFlowType getNodeType(Node n) {
suppressUnusedNode(n) and
exists(n) and
result instanceof VoidType // stub implementation
}
@@ -999,13 +999,10 @@ string ppReprType(DataFlowType t) { none() } // stub implementation
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
any() // stub implementation
t1 instanceof VoidType and t2 instanceof VoidType // stub implementation
}
private predicate suppressUnusedNode(Node n) { any() }
//////////////////////////////////////////////////////////////////////////////
// Java QL library compatibility wrappers
//////////////////////////////////////////////////////////////////////////////

View File

@@ -2483,7 +2483,7 @@ private predicate uselessTypebound(DataFlowType dt) {
)
}
pragma[inline]
pragma[nomagic]
private predicate compatibleTypesDelegateLeft(DataFlowType dt1, DataFlowType dt2) {
exists(Gvn::GvnType t1, Gvn::GvnType t2 |
t1 = exprNode(dt1.getADelegateCreation()).(NodeImpl).getDataFlowType().asGvnType() and
@@ -2507,7 +2507,7 @@ private predicate compatibleTypesDelegateLeft(DataFlowType dt1, DataFlowType dt2
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
pragma[nomagic]
predicate compatibleTypes(DataFlowType dt1, DataFlowType dt2) {
exists(Gvn::GvnType t1, Gvn::GvnType t2 |
t1 = dt1.asGvnType() and
@@ -2522,16 +2522,12 @@ predicate compatibleTypes(DataFlowType dt1, DataFlowType dt2) {
t1.(DataFlowNullType).isConvertibleTo(t2)
or
t2.(DataFlowNullType).isConvertibleTo(t1)
or
t1 instanceof Gvn::TypeParameterGvnType
or
t2 instanceof Gvn::TypeParameterGvnType
or
t1 instanceof GvnUnknownType
or
t2 instanceof GvnUnknownType
)
or
exists(dt1.asGvnType()) and uselessTypebound(dt2)
or
uselessTypebound(dt1) and exists(dt2.asGvnType())
or
compatibleTypesDelegateLeft(dt1, dt2)
or
compatibleTypesDelegateLeft(dt2, dt1)

View File

@@ -222,9 +222,8 @@ string ppReprType(DataFlowType t) { none() }
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
any() // stub implementation
t1 = TTodoDataFlowType() and t2 = TTodoDataFlowType() // stub implementation
}
//////////////////////////////////////////////////////////////////////////////

View File

@@ -371,18 +371,12 @@ string ppReprType(DataFlowType t) {
else result = t.toString()
}
pragma[nomagic]
private predicate compatibleTypes0(DataFlowType t1, DataFlowType t2) {
erasedHaveIntersection(t1, t2)
}
/**
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
bindingset[t1, t2]
pragma[inline_late]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { compatibleTypes0(t1, t2) }
pragma[nomagic]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { erasedHaveIntersection(t1, t2) }
/** A node that performs a type cast. */
class CastNode extends ExprNode {

View File

@@ -564,7 +564,6 @@ predicate neverSkipInPathGraph(Node n) {
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { any() }
predicate typeStrongerThan(DataFlowType t1, DataFlowType t2) { none() }
@@ -576,8 +575,7 @@ predicate localMustFlowStep(Node nodeFrom, Node nodeTo) { none() }
*/
DataFlowType getNodeType(Node node) {
result = TAnyFlow() and
// Suppress unused variable warning
node = node
exists(node)
}
/** Gets a string representation of a type returned by `getErasedRepr`. */

View File

@@ -2087,7 +2087,6 @@ private predicate compatibleTypesNonSymRefl(DataFlowType t1, DataFlowType t2) {
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
t1 = t2
or

View File

@@ -142,7 +142,6 @@ signature module InputSig<LocationSig Location> {
* steps, then it will check that the types of `n1` and `n2` are compatible.
* If they are not, then flow will be blocked.
*/
bindingset[t1, t2]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2);
/**

View File

@@ -1444,6 +1444,31 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
)
}
pragma[nomagic]
private predicate compatibleContainer0(ApHeadContent apc, DataFlowType containerType) {
exists(DataFlowType containerType0, Content c |
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
not isTopType(containerType0) and
compatibleTypesCached(containerType0, containerType) and
apc = projectToHeadContent(c)
)
}
pragma[nomagic]
private predicate topTypeContent(ApHeadContent apc) {
exists(DataFlowType containerType0, Content c |
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
isTopType(containerType0) and
apc = projectToHeadContent(c)
)
}
bindingset[apc, containerType]
pragma[inline_late]
private predicate compatibleContainer(ApHeadContent apc, DataFlowType containerType) {
compatibleContainer0(apc, containerType)
}
/**
* Holds if `node` is reachable with access path `ap` from a source.
*
@@ -1465,7 +1490,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
) {
fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t0, ap, apa) and
PrevStage::revFlow(node, state, apa) and
filter(node, state, t0, ap, t)
filter(node, state, t0, ap, t) and
(
if castingNodeEx(node)
then
ap instanceof ApNil or
compatibleContainer(getHeadContent(ap), node.getDataFlowType()) or
topTypeContent(getHeadContent(ap))
else any()
)
}
pragma[nomagic]
@@ -2853,12 +2886,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
private import LocalFlowBigStep
pragma[nomagic]
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
private predicate castingNodeEx(NodeEx node) {
node.asNode() instanceof CastingNode or exists(node.asParamReturnNode())
}
private module Stage3Param implements MkStage<Stage2>::StageParam {
private module PrevStage = Stage2;
class Typ = DataFlowType;
class Typ = Unit;
class Ap = ApproxAccessPathFront;
@@ -2866,7 +2901,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
PrevStage::Ap getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
Typ getTyp(DataFlowType t) { result = t }
Typ getTyp(DataFlowType t) { any() }
bindingset[c, t, tail]
Ap apCons(Content c, Typ t, Ap tail) { result.getAHead() = c and exists(t) and exists(tail) }
@@ -2903,7 +2938,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
Typ t, LocalCc lcc
) {
localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _, _) and
localFlowBigStep(node1, state1, node2, state2, preservesValue, _, _, _) and
exists(t) and
exists(lcc)
}
@@ -2926,7 +2962,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
// the cons candidates including types are used to construct subsequent
// access path approximations.
t0 = t and
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t0) else any()) and
(
notExpectsContent(node)
or
@@ -2935,11 +2970,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
}
bindingset[typ, contentType]
predicate typecheckStore(Typ typ, DataFlowType contentType) {
// We need to typecheck stores here, since reverse flow through a getter
// might have a different type here compared to inside the getter.
compatibleTypes(typ, contentType)
}
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
}
private module Stage3 = MkStage<Stage2>::Stage<Stage3Param>;
@@ -2949,7 +2980,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
if castingNodeEx(node)
then
exists(DataFlowType nt | nt = node.getDataFlowType() |
if typeStrongerThan(nt, t0) then t = nt else (compatibleTypes(nt, t0) and t = t0)
if typeStrongerThanFilter(nt, t0)
then t = nt
else (
compatibleTypesFilter(nt, t0) and t = t0
)
)
else t = t0
}
@@ -3048,7 +3083,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
predicate typecheckStore(Typ typ, DataFlowType contentType) {
// We need to typecheck stores here, since reverse flow through a getter
// might have a different type here compared to inside the getter.
compatibleTypes(typ, contentType)
compatibleTypesFilter(typ, contentType)
}
}
@@ -3304,7 +3339,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
bindingset[typ, contentType]
predicate typecheckStore(Typ typ, DataFlowType contentType) {
compatibleTypes(typ, contentType)
compatibleTypesFilter(typ, contentType)
}
}
@@ -4244,7 +4279,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
Stage5::storeStepCand(mid.getNodeExOutgoing(), _, c, node, contentType, t) and
state = mid.getState() and
cc = mid.getCallContext() and
compatibleTypes(t0, contentType)
compatibleTypesFilter(t0, contentType)
)
}
@@ -5294,7 +5329,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
storeExUnrestricted(midNode, c, node, contentType, t2) and
ap2.getHead() = c and
ap2.len() = unbindInt(ap1.len() + 1) and
compatibleTypes(t1, contentType)
compatibleTypesFilter(t1, contentType)
)
}

View File

@@ -288,7 +288,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
revLambdaFlow0(lambdaCall, kind, node, t, toReturn, toJump, lastCall) and
not expectsContent(node, _) and
if castNode(node) or node instanceof ArgNode or node instanceof ReturnNode
then compatibleTypes(t, getNodeDataFlowType(node))
then compatibleTypesFilter(t, getNodeDataFlowType(node))
else any()
}
@@ -886,6 +886,20 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
cached
predicate nodeDataFlowType(Node n, DataFlowType t) { t = getNodeType(n) }
cached
predicate compatibleTypesCached(DataFlowType t1, DataFlowType t2) { compatibleTypes(t1, t2) }
private predicate relevantType(DataFlowType t) { t = getNodeType(_) }
cached
predicate isTopType(DataFlowType t) {
strictcount(DataFlowType t0 | relevantType(t0)) =
strictcount(DataFlowType t0 | relevantType(t0) and compatibleTypesCached(t, t0))
}
cached
predicate typeStrongerThanCached(DataFlowType t1, DataFlowType t2) { typeStrongerThan(t1, t2) }
cached
predicate jumpStepCached(Node node1, Node node2) { jumpStep(node1, node2) }
@@ -1118,7 +1132,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
exists(ParameterPosition ppos |
viableParam(call, ppos, p) and
argumentPositionMatch(call, arg, ppos) and
compatibleTypes(getNodeDataFlowType(arg), getNodeDataFlowType(p)) and
compatibleTypesFilter(getNodeDataFlowType(arg), getNodeDataFlowType(p)) and
golangSpecificParamArgFilter(call, p, arg)
)
}
@@ -1271,10 +1285,10 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
then
// normal flow through
read = TReadStepTypesNone() and
compatibleTypes(getNodeDataFlowType(p), getNodeDataFlowType(node))
compatibleTypesFilter(getNodeDataFlowType(p), getNodeDataFlowType(node))
or
// getter
compatibleTypes(read.getContentType(), getNodeDataFlowType(node))
compatibleTypesFilter(read.getContentType(), getNodeDataFlowType(node))
else any()
}
@@ -1307,7 +1321,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
readStepWithTypes(mid, read.getContainerType(), read.getContent(), node,
read.getContentType()) and
Cand::parameterValueFlowReturnCand(p, _, true) and
compatibleTypes(getNodeDataFlowType(p), read.getContainerType())
compatibleTypesFilter(getNodeDataFlowType(p), read.getContainerType())
)
or
parameterValueFlow0_0(TReadStepTypesNone(), p, node, read, model)
@@ -1368,11 +1382,11 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
|
// normal flow through
read = TReadStepTypesNone() and
compatibleTypes(getNodeDataFlowType(arg), getNodeDataFlowType(out))
compatibleTypesFilter(getNodeDataFlowType(arg), getNodeDataFlowType(out))
or
// getter
compatibleTypes(getNodeDataFlowType(arg), read.getContainerType()) and
compatibleTypes(read.getContentType(), getNodeDataFlowType(out))
compatibleTypesFilter(getNodeDataFlowType(arg), read.getContainerType()) and
compatibleTypesFilter(read.getContentType(), getNodeDataFlowType(out))
)
}
@@ -1622,7 +1636,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
bindingset[t1, t2]
pragma[inline_late]
private predicate typeStrongerThan0(DataFlowType t1, DataFlowType t2) { typeStrongerThan(t1, t2) }
predicate compatibleTypesFilter(DataFlowType t1, DataFlowType t2) {
compatibleTypesCached(t1, t2)
}
bindingset[t1, t2]
pragma[inline_late]
predicate typeStrongerThanFilter(DataFlowType t1, DataFlowType t2) {
typeStrongerThanCached(t1, t2)
}
private predicate callEdge(DataFlowCall call, DataFlowCallable c, ArgNode arg, ParamNode p) {
viableParamArg(call, p, arg) and
@@ -1703,7 +1725,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
nodeDataFlowType(arg, at) and
nodeDataFlowType(p, pt) and
relevantCallEdge(_, _, arg, p) and
typeStrongerThan0(pt, at)
typeStrongerThanFilter(pt, at)
)
or
exists(ParamNode p, DataFlowType at, DataFlowType pt |
@@ -1714,7 +1736,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
nodeDataFlowType(p, pt) and
paramMustFlow(p, arg) and
relevantCallEdge(_, _, arg, _) and
typeStrongerThan0(at, pt)
typeStrongerThanFilter(at, pt)
)
or
exists(ParamNode p |
@@ -1754,7 +1776,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
nodeDataFlowType(arg, at) and
nodeDataFlowType(p, pt) and
relevantCallEdge(_, _, arg, p) and
typeStrongerThan0(at, pt)
typeStrongerThanFilter(at, pt)
)
or
exists(ArgNode arg |
@@ -1823,8 +1845,13 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
* stronger then compatibility is checked and `t1` is returned.
*/
bindingset[t1, t2]
pragma[inline_late]
DataFlowType getStrongestType(DataFlowType t1, DataFlowType t2) {
if typeStrongerThan(t2, t1) then result = t2 else (compatibleTypes(t1, t2) and result = t1)
if typeStrongerThanCached(t2, t1)
then result = t2
else (
compatibleTypesFilter(t1, t2) and result = t1
)
}
/**
@@ -1945,7 +1972,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
exists(DataFlowType t1, DataFlowType t2 |
typeFlowArgType(arg, t1, cc) and
relevantArgParamIn(arg, p, t2) and
compatibleTypes(t1, t2)
compatibleTypesFilter(t1, t2)
)
}
@@ -1989,7 +2016,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
exists(DataFlowType t1, DataFlowType t2 |
typeFlowParamType(p, t1, false) and
relevantArgParamOut(arg, p, t2) and
compatibleTypes(t1, t2)
compatibleTypesFilter(t1, t2)
)
}

View File

@@ -1310,7 +1310,6 @@ string ppReprType(DataFlowType t) { none() }
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
* a node of type `t1` to a node of type `t2`.
*/
pragma[inline]
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { any() }
abstract class PostUpdateNodeImpl extends Node {