Skip to content

Commit 25d520a

Browse files
aschackmullaschackmull
authored
Merge pull request github#16785 from aschackmull/dataflow/stage3-notypes
Dataflow: Replace stage 3 type pruning with flow-insensitive type pruning.
2 parents 19b6d24 + fdf6e30 commit 25d520a

File tree

11 files changed

+107
-67
lines changed

11 files changed

+107
-67
lines changed

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -216,7 +216,7 @@ predicate localMustFlowStep(Node node1, Node node2) { none() }
216216

217217
/** Gets the type of `n` used for type pruning. */
218218
Type getNodeType(Node n) {
219-
suppressUnusedNode(n) and
219+
exists(n) and
220220
result instanceof VoidType // stub implementation
221221
}
222222

@@ -227,13 +227,10 @@ string ppReprType(Type t) { none() } // stub implementation
227227
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
228228
* a node of type `t1` to a node of type `t2`.
229229
*/
230-
pragma[inline]
231230
predicate compatibleTypes(Type t1, Type t2) {
232-
any() // stub implementation
231+
t1 instanceof VoidType and t2 instanceof VoidType // stub implementation
233232
}
234233

235-
private predicate suppressUnusedNode(Node n) { any() }
236-
237234
//////////////////////////////////////////////////////////////////////////////
238235
// Java QL library compatibility wrappers
239236
//////////////////////////////////////////////////////////////////////////////

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -988,7 +988,7 @@ predicate localMustFlowStep(Node node1, Node node2) { none() }
988988

989989
/** Gets the type of `n` used for type pruning. */
990990
DataFlowType getNodeType(Node n) {
991-
suppressUnusedNode(n) and
991+
exists(n) and
992992
result instanceof VoidType // stub implementation
993993
}
994994

@@ -999,13 +999,10 @@ string ppReprType(DataFlowType t) { none() } // stub implementation
999999
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
10001000
* a node of type `t1` to a node of type `t2`.
10011001
*/
1002-
pragma[inline]
10031002
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
1004-
any() // stub implementation
1003+
t1 instanceof VoidType and t2 instanceof VoidType // stub implementation
10051004
}
10061005

1007-
private predicate suppressUnusedNode(Node n) { any() }
1008-
10091006
//////////////////////////////////////////////////////////////////////////////
10101007
// Java QL library compatibility wrappers
10111008
//////////////////////////////////////////////////////////////////////////////

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2483,7 +2483,7 @@ private predicate uselessTypebound(DataFlowType dt) {
24832483
)
24842484
}
24852485

2486-
pragma[inline]
2486+
pragma[nomagic]
24872487
private predicate compatibleTypesDelegateLeft(DataFlowType dt1, DataFlowType dt2) {
24882488
exists(Gvn::GvnType t1, Gvn::GvnType t2 |
24892489
t1 = exprNode(dt1.getADelegateCreation()).(NodeImpl).getDataFlowType().asGvnType() and
@@ -2507,7 +2507,7 @@ private predicate compatibleTypesDelegateLeft(DataFlowType dt1, DataFlowType dt2
25072507
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
25082508
* a node of type `t1` to a node of type `t2`.
25092509
*/
2510-
pragma[inline]
2510+
pragma[nomagic]
25112511
predicate compatibleTypes(DataFlowType dt1, DataFlowType dt2) {
25122512
exists(Gvn::GvnType t1, Gvn::GvnType t2 |
25132513
t1 = dt1.asGvnType() and
@@ -2522,16 +2522,12 @@ predicate compatibleTypes(DataFlowType dt1, DataFlowType dt2) {
25222522
t1.(DataFlowNullType).isConvertibleTo(t2)
25232523
or
25242524
t2.(DataFlowNullType).isConvertibleTo(t1)
2525-
or
2526-
t1 instanceof Gvn::TypeParameterGvnType
2527-
or
2528-
t2 instanceof Gvn::TypeParameterGvnType
2529-
or
2530-
t1 instanceof GvnUnknownType
2531-
or
2532-
t2 instanceof GvnUnknownType
25332525
)
25342526
or
2527+
exists(dt1.asGvnType()) and uselessTypebound(dt2)
2528+
or
2529+
uselessTypebound(dt1) and exists(dt2.asGvnType())
2530+
or
25352531
compatibleTypesDelegateLeft(dt1, dt2)
25362532
or
25372533
compatibleTypesDelegateLeft(dt2, dt1)

‎go/ql/lib/semmle/go/dataflow/internal/DataFlowPrivate.qll

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -222,9 +222,8 @@ string ppReprType(DataFlowType t) { none() }
222222
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
223223
* a node of type `t1` to a node of type `t2`.
224224
*/
225-
pragma[inline]
226225
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
227-
any() // stub implementation
226+
t1 = TTodoDataFlowType() and t2 = TTodoDataFlowType() // stub implementation
228227
}
229228

230229
//////////////////////////////////////////////////////////////////////////////

‎java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -371,18 +371,12 @@ string ppReprType(DataFlowType t) {
371371
else result = t.toString()
372372
}
373373

374-
pragma[nomagic]
375-
private predicate compatibleTypes0(DataFlowType t1, DataFlowType t2) {
376-
erasedHaveIntersection(t1, t2)
377-
}
378-
379374
/**
380375
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
381376
* a node of type `t1` to a node of type `t2`.
382377
*/
383-
bindingset[t1, t2]
384-
pragma[inline_late]
385-
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { compatibleTypes0(t1, t2) }
378+
pragma[nomagic]
379+
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { erasedHaveIntersection(t1, t2) }
386380

387381
/** A node that performs a type cast. */
388382
class CastNode extends ExprNode {

‎python/ql/lib/semmle/python/dataflow/new/internal/DataFlowPrivate.qll

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -564,7 +564,6 @@ predicate neverSkipInPathGraph(Node n) {
564564
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
565565
* a node of type `t1` to a node of type `t2`.
566566
*/
567-
pragma[inline]
568567
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) { any() }
569568

570569
predicate typeStrongerThan(DataFlowType t1, DataFlowType t2) { none() }
@@ -576,8 +575,7 @@ predicate localMustFlowStep(Node nodeFrom, Node nodeTo) { none() }
576575
*/
577576
DataFlowType getNodeType(Node node) {
578577
result = TAnyFlow() and
579-
// Suppress unused variable warning
580-
node = node
578+
exists(node)
581579
}
582580

583581
/** Gets a string representation of a type returned by `getErasedRepr`. */

‎ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2087,7 +2087,6 @@ private predicate compatibleTypesNonSymRefl(DataFlowType t1, DataFlowType t2) {
20872087
* Holds if `t1` and `t2` are compatible, that is, whether data can flow from
20882088
* a node of type `t1` to a node of type `t2`.
20892089
*/
2090-
pragma[inline]
20912090
predicate compatibleTypes(DataFlowType t1, DataFlowType t2) {
20922091
t1 = t2
20932092
or

‎shared/dataflow/codeql/dataflow/DataFlow.qll

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,6 @@ signature module InputSig<LocationSig Location> {
142142
* steps, then it will check that the types of `n1` and `n2` are compatible.
143143
* If they are not, then flow will be blocked.
144144
*/
145-
bindingset[t1, t2]
146145
predicate compatibleTypes(DataFlowType t1, DataFlowType t2);
147146

148147
/**

‎shared/dataflow/codeql/dataflow/internal/DataFlowImpl.qll

Lines changed: 51 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1444,6 +1444,31 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
14441444
)
14451445
}
14461446

1447+
pragma[nomagic]
1448+
private predicate compatibleContainer0(ApHeadContent apc, DataFlowType containerType) {
1449+
exists(DataFlowType containerType0, Content c |
1450+
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
1451+
not isTopType(containerType0) and
1452+
compatibleTypesCached(containerType0, containerType) and
1453+
apc = projectToHeadContent(c)
1454+
)
1455+
}
1456+
1457+
pragma[nomagic]
1458+
private predicate topTypeContent(ApHeadContent apc) {
1459+
exists(DataFlowType containerType0, Content c |
1460+
PrevStage::storeStepCand(_, _, c, _, _, containerType0) and
1461+
isTopType(containerType0) and
1462+
apc = projectToHeadContent(c)
1463+
)
1464+
}
1465+
1466+
bindingset[apc, containerType]
1467+
pragma[inline_late]
1468+
private predicate compatibleContainer(ApHeadContent apc, DataFlowType containerType) {
1469+
compatibleContainer0(apc, containerType)
1470+
}
1471+
14471472
/**
14481473
* Holds if `node` is reachable with access path `ap` from a source.
14491474
*
@@ -1465,7 +1490,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
14651490
) {
14661491
fwdFlow0(node, state, cc, summaryCtx, argT, argAp, t0, ap, apa) and
14671492
PrevStage::revFlow(node, state, apa) and
1468-
filter(node, state, t0, ap, t)
1493+
filter(node, state, t0, ap, t) and
1494+
(
1495+
if castingNodeEx(node)
1496+
then
1497+
ap instanceof ApNil or
1498+
compatibleContainer(getHeadContent(ap), node.getDataFlowType()) or
1499+
topTypeContent(getHeadContent(ap))
1500+
else any()
1501+
)
14691502
}
14701503

14711504
pragma[nomagic]
@@ -2853,20 +2886,22 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
28532886
private import LocalFlowBigStep
28542887

28552888
pragma[nomagic]
2856-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2889+
private predicate castingNodeEx(NodeEx node) {
2890+
node.asNode() instanceof CastingNode or exists(node.asParamReturnNode())
2891+
}
28572892

28582893
private module Stage3Param implements MkStage<Stage2>::StageParam {
28592894
private module PrevStage = Stage2;
28602895

2861-
class Typ = DataFlowType;
2896+
class Typ = Unit;
28622897

28632898
class Ap = ApproxAccessPathFront;
28642899

28652900
class ApNil = ApproxAccessPathFrontNil;
28662901

28672902
PrevStage::Ap getApprox(Ap ap) { result = ap.toBoolNonEmpty() }
28682903

2869-
Typ getTyp(DataFlowType t) { result = t }
2904+
Typ getTyp(DataFlowType t) { any() }
28702905

28712906
bindingset[c, t, tail]
28722907
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> {
29032938
NodeEx node1, FlowState state1, NodeEx node2, FlowState state2, boolean preservesValue,
29042939
Typ t, LocalCc lcc
29052940
) {
2906-
localFlowBigStep(node1, state1, node2, state2, preservesValue, t, _, _) and
2941+
localFlowBigStep(node1, state1, node2, state2, preservesValue, _, _, _) and
2942+
exists(t) and
29072943
exists(lcc)
29082944
}
29092945

@@ -2926,7 +2962,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29262962
// the cons candidates including types are used to construct subsequent
29272963
// access path approximations.
29282964
t0 = t and
2929-
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t0) else any()) and
29302965
(
29312966
notExpectsContent(node)
29322967
or
@@ -2935,11 +2970,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29352970
}
29362971

29372972
bindingset[typ, contentType]
2938-
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2939-
// We need to typecheck stores here, since reverse flow through a getter
2940-
// might have a different type here compared to inside the getter.
2941-
compatibleTypes(typ, contentType)
2942-
}
2973+
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
29432974
}
29442975

29452976
private module Stage3 = MkStage<Stage2>::Stage<Stage3Param>;
@@ -2949,7 +2980,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29492980
if castingNodeEx(node)
29502981
then
29512982
exists(DataFlowType nt | nt = node.getDataFlowType() |
2952-
if typeStrongerThan(nt, t0) then t = nt else (compatibleTypes(nt, t0) and t = t0)
2983+
if typeStrongerThanFilter(nt, t0)
2984+
then t = nt
2985+
else (
2986+
compatibleTypesFilter(nt, t0) and t = t0
2987+
)
29532988
)
29542989
else t = t0
29552990
}
@@ -3048,7 +3083,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
30483083
predicate typecheckStore(Typ typ, DataFlowType contentType) {
30493084
// We need to typecheck stores here, since reverse flow through a getter
30503085
// might have a different type here compared to inside the getter.
3051-
compatibleTypes(typ, contentType)
3086+
compatibleTypesFilter(typ, contentType)
30523087
}
30533088
}
30543089

@@ -3304,7 +3339,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
33043339

33053340
bindingset[typ, contentType]
33063341
predicate typecheckStore(Typ typ, DataFlowType contentType) {
3307-
compatibleTypes(typ, contentType)
3342+
compatibleTypesFilter(typ, contentType)
33083343
}
33093344
}
33103345

@@ -4244,7 +4279,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
42444279
Stage5::storeStepCand(mid.getNodeExOutgoing(), _, c, node, contentType, t) and
42454280
state = mid.getState() and
42464281
cc = mid.getCallContext() and
4247-
compatibleTypes(t0, contentType)
4282+
compatibleTypesFilter(t0, contentType)
42484283
)
42494284
}
42504285

@@ -5294,7 +5329,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
52945329
storeExUnrestricted(midNode, c, node, contentType, t2) and
52955330
ap2.getHead() = c and
52965331
ap2.len() = unbindInt(ap1.len() + 1) and
5297-
compatibleTypes(t1, contentType)
5332+
compatibleTypesFilter(t1, contentType)
52985333
)
52995334
}
53005335

0 commit comments

Comments
 (0)