Skip to content

Commit 71ae090

Browse files
aschackmullaschackmull
committed
Dataflow: Enforce type pruning in all forward stages.
1 parent 9140cbe commit 71ae090

File tree

8 files changed

+168
-120
lines changed

8 files changed

+168
-120
lines changed

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

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
21622162

21632163
private import LocalFlowBigStep
21642164

2165+
pragma[nomagic]
2166+
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2167+
21652168
private module Stage3Param implements MkStage<Stage2>::StageParam {
21662169
private module PrevStage = Stage2;
21672170

@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
22152218
)
22162219
}
22172220

2218-
pragma[nomagic]
2219-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2220-
22212221
bindingset[node, state, t, ap]
22222222
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
22232223
exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
23332333
)
23342334
}
23352335

2336-
pragma[nomagic]
2337-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2338-
23392336
bindingset[node, state, t, ap]
23402337
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
23412338
exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
26132610
}
26142611

26152612
bindingset[node, state, t, ap]
2616-
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
2613+
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
2614+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
2615+
exists(state) and
2616+
exists(ap)
2617+
}
26172618

2618-
// Type checking is not necessary here as it has already been done in stage 3.
26192619
bindingset[typ, contentType]
2620-
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
2620+
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2621+
compatibleTypes(typ, contentType)
2622+
}
26212623
}
26222624

26232625
private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
28192821
or
28202822
// ... or a step from an existing PathNode to another node.
28212823
pathStep(_, node, state, cc, sc, t, ap) and
2822-
Stage5::revFlow(node, state, ap.getApprox())
2824+
Stage5::revFlow(node, state, ap.getApprox()) and
2825+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
28232826
} or
28242827
TPathNodeSink(NodeEx node, FlowState state) {
28252828
exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
34183421
PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
34193422
DataFlowType t, CallContext cc
34203423
) {
3421-
t0 = mid.getType() and
3422-
ap0 = mid.getAp() and
3423-
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
3424-
state = mid.getState() and
3425-
cc = mid.getCallContext()
3424+
exists(DataFlowType contentType |
3425+
t0 = mid.getType() and
3426+
ap0 = mid.getAp() and
3427+
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
3428+
state = mid.getState() and
3429+
cc = mid.getCallContext() and
3430+
compatibleTypes(t0, contentType)
3431+
)
34263432
}
34273433

34283434
private predicate pathOutOfCallable0(

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

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
21622162

21632163
private import LocalFlowBigStep
21642164

2165+
pragma[nomagic]
2166+
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2167+
21652168
private module Stage3Param implements MkStage<Stage2>::StageParam {
21662169
private module PrevStage = Stage2;
21672170

@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
22152218
)
22162219
}
22172220

2218-
pragma[nomagic]
2219-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2220-
22212221
bindingset[node, state, t, ap]
22222222
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
22232223
exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
23332333
)
23342334
}
23352335

2336-
pragma[nomagic]
2337-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2338-
23392336
bindingset[node, state, t, ap]
23402337
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
23412338
exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
26132610
}
26142611

26152612
bindingset[node, state, t, ap]
2616-
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
2613+
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
2614+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
2615+
exists(state) and
2616+
exists(ap)
2617+
}
26172618

2618-
// Type checking is not necessary here as it has already been done in stage 3.
26192619
bindingset[typ, contentType]
2620-
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
2620+
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2621+
compatibleTypes(typ, contentType)
2622+
}
26212623
}
26222624

26232625
private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
28192821
or
28202822
// ... or a step from an existing PathNode to another node.
28212823
pathStep(_, node, state, cc, sc, t, ap) and
2822-
Stage5::revFlow(node, state, ap.getApprox())
2824+
Stage5::revFlow(node, state, ap.getApprox()) and
2825+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
28232826
} or
28242827
TPathNodeSink(NodeEx node, FlowState state) {
28252828
exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
34183421
PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
34193422
DataFlowType t, CallContext cc
34203423
) {
3421-
t0 = mid.getType() and
3422-
ap0 = mid.getAp() and
3423-
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
3424-
state = mid.getState() and
3425-
cc = mid.getCallContext()
3424+
exists(DataFlowType contentType |
3425+
t0 = mid.getType() and
3426+
ap0 = mid.getAp() and
3427+
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
3428+
state = mid.getState() and
3429+
cc = mid.getCallContext() and
3430+
compatibleTypes(t0, contentType)
3431+
)
34263432
}
34273433

34283434
private predicate pathOutOfCallable0(

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

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
21622162

21632163
private import LocalFlowBigStep
21642164

2165+
pragma[nomagic]
2166+
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2167+
21652168
private module Stage3Param implements MkStage<Stage2>::StageParam {
21662169
private module PrevStage = Stage2;
21672170

@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
22152218
)
22162219
}
22172220

2218-
pragma[nomagic]
2219-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2220-
22212221
bindingset[node, state, t, ap]
22222222
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
22232223
exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
23332333
)
23342334
}
23352335

2336-
pragma[nomagic]
2337-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2338-
23392336
bindingset[node, state, t, ap]
23402337
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
23412338
exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
26132610
}
26142611

26152612
bindingset[node, state, t, ap]
2616-
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
2613+
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
2614+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
2615+
exists(state) and
2616+
exists(ap)
2617+
}
26172618

2618-
// Type checking is not necessary here as it has already been done in stage 3.
26192619
bindingset[typ, contentType]
2620-
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
2620+
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2621+
compatibleTypes(typ, contentType)
2622+
}
26212623
}
26222624

26232625
private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
28192821
or
28202822
// ... or a step from an existing PathNode to another node.
28212823
pathStep(_, node, state, cc, sc, t, ap) and
2822-
Stage5::revFlow(node, state, ap.getApprox())
2824+
Stage5::revFlow(node, state, ap.getApprox()) and
2825+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
28232826
} or
28242827
TPathNodeSink(NodeEx node, FlowState state) {
28252828
exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
34183421
PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
34193422
DataFlowType t, CallContext cc
34203423
) {
3421-
t0 = mid.getType() and
3422-
ap0 = mid.getAp() and
3423-
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
3424-
state = mid.getState() and
3425-
cc = mid.getCallContext()
3424+
exists(DataFlowType contentType |
3425+
t0 = mid.getType() and
3426+
ap0 = mid.getAp() and
3427+
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
3428+
state = mid.getState() and
3429+
cc = mid.getCallContext() and
3430+
compatibleTypes(t0, contentType)
3431+
)
34263432
}
34273433

34283434
private predicate pathOutOfCallable0(

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

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
21622162

21632163
private import LocalFlowBigStep
21642164

2165+
pragma[nomagic]
2166+
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2167+
21652168
private module Stage3Param implements MkStage<Stage2>::StageParam {
21662169
private module PrevStage = Stage2;
21672170

@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
22152218
)
22162219
}
22172220

2218-
pragma[nomagic]
2219-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2220-
22212221
bindingset[node, state, t, ap]
22222222
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
22232223
exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
23332333
)
23342334
}
23352335

2336-
pragma[nomagic]
2337-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2338-
23392336
bindingset[node, state, t, ap]
23402337
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
23412338
exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
26132610
}
26142611

26152612
bindingset[node, state, t, ap]
2616-
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
2613+
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
2614+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
2615+
exists(state) and
2616+
exists(ap)
2617+
}
26172618

2618-
// Type checking is not necessary here as it has already been done in stage 3.
26192619
bindingset[typ, contentType]
2620-
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
2620+
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2621+
compatibleTypes(typ, contentType)
2622+
}
26212623
}
26222624

26232625
private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
28192821
or
28202822
// ... or a step from an existing PathNode to another node.
28212823
pathStep(_, node, state, cc, sc, t, ap) and
2822-
Stage5::revFlow(node, state, ap.getApprox())
2824+
Stage5::revFlow(node, state, ap.getApprox()) and
2825+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
28232826
} or
28242827
TPathNodeSink(NodeEx node, FlowState state) {
28252828
exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
34183421
PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
34193422
DataFlowType t, CallContext cc
34203423
) {
3421-
t0 = mid.getType() and
3422-
ap0 = mid.getAp() and
3423-
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
3424-
state = mid.getState() and
3425-
cc = mid.getCallContext()
3424+
exists(DataFlowType contentType |
3425+
t0 = mid.getType() and
3426+
ap0 = mid.getAp() and
3427+
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
3428+
state = mid.getState() and
3429+
cc = mid.getCallContext() and
3430+
compatibleTypes(t0, contentType)
3431+
)
34263432
}
34273433

34283434
private predicate pathOutOfCallable0(

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

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
21622162

21632163
private import LocalFlowBigStep
21642164

2165+
pragma[nomagic]
2166+
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2167+
21652168
private module Stage3Param implements MkStage<Stage2>::StageParam {
21662169
private module PrevStage = Stage2;
21672170

@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
22152218
)
22162219
}
22172220

2218-
pragma[nomagic]
2219-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2220-
22212221
bindingset[node, state, t, ap]
22222222
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
22232223
exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
23332333
)
23342334
}
23352335

2336-
pragma[nomagic]
2337-
private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
2338-
23392336
bindingset[node, state, t, ap]
23402337
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
23412338
exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
26132610
}
26142611

26152612
bindingset[node, state, t, ap]
2616-
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
2613+
predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
2614+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
2615+
exists(state) and
2616+
exists(ap)
2617+
}
26172618

2618-
// Type checking is not necessary here as it has already been done in stage 3.
26192619
bindingset[typ, contentType]
2620-
predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
2620+
predicate typecheckStore(Typ typ, DataFlowType contentType) {
2621+
compatibleTypes(typ, contentType)
2622+
}
26212623
}
26222624

26232625
private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
28192821
or
28202822
// ... or a step from an existing PathNode to another node.
28212823
pathStep(_, node, state, cc, sc, t, ap) and
2822-
Stage5::revFlow(node, state, ap.getApprox())
2824+
Stage5::revFlow(node, state, ap.getApprox()) and
2825+
(if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
28232826
} or
28242827
TPathNodeSink(NodeEx node, FlowState state) {
28252828
exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
34183421
PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
34193422
DataFlowType t, CallContext cc
34203423
) {
3421-
t0 = mid.getType() and
3422-
ap0 = mid.getAp() and
3423-
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
3424-
state = mid.getState() and
3425-
cc = mid.getCallContext()
3424+
exists(DataFlowType contentType |
3425+
t0 = mid.getType() and
3426+
ap0 = mid.getAp() and
3427+
Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
3428+
state = mid.getState() and
3429+
cc = mid.getCallContext() and
3430+
compatibleTypes(t0, contentType)
3431+
)
34263432
}
34273433

34283434
private predicate pathOutOfCallable0(

0 commit comments

Comments
 (0)