Skip to content

Commit 941177e

Browse files
aschackmullaschackmull
authored
Merge pull request github#3762 from hvitved/dataflow/clear-contents
Data flow: Model field clearing
2 parents 3b62bd2 + ff751ac commit 941177e

31 files changed

+558
-79
lines changed

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

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplCommon.qll

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -754,6 +754,13 @@ abstract class AccessPathFront extends TAccessPathFront {
754754
abstract boolean toBoolNonEmpty();
755755

756756
predicate headUsesContent(TypedContent tc) { this = TFrontHead(tc) }
757+
758+
predicate isClearedAt(Node n) {
759+
exists(TypedContent tc |
760+
this.headUsesContent(tc) and
761+
clearsContent(n, tc.getContent())
762+
)
763+
}
757764
}
758765

759766
class AccessPathFrontNil extends AccessPathFront, TFrontNil {

‎cpp/ql/src/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,13 @@ predicate readStep(Node node1, Content f, Node node2) {
216216
)
217217
}
218218

219+
/**
220+
* Holds if values stored inside content `c` are cleared at node `n`.
221+
*/
222+
predicate clearsContent(Node n, Content c) {
223+
none() // stub implementation
224+
}
225+
219226
/**
220227
* Gets a representative (boxed) type for `t` for the purpose of pruning
221228
* possible flow. A single type is used for all numeric types to account for

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

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1051,6 +1051,17 @@ private predicate flowIntoCallNodeCand2(
10511051
}
10521052

10531053
private module LocalFlowBigStep {
1054+
/**
1055+
* A node where some checking is required, and hence the big-step relation
1056+
* is not allowed to step over.
1057+
*/
1058+
private class FlowCheckNode extends Node {
1059+
FlowCheckNode() {
1060+
this instanceof CastNode or
1061+
clearsContent(this, _)
1062+
}
1063+
}
1064+
10541065
/**
10551066
* Holds if `node` can be the first node in a maximal subsequence of local
10561067
* flow steps in a dataflow path.
@@ -1065,7 +1076,7 @@ private module LocalFlowBigStep {
10651076
node instanceof OutNodeExt or
10661077
store(_, _, node, _) or
10671078
read(_, _, node) or
1068-
node instanceof CastNode
1079+
node instanceof FlowCheckNode
10691080
)
10701081
}
10711082

@@ -1083,7 +1094,7 @@ private module LocalFlowBigStep {
10831094
read(node, _, next)
10841095
)
10851096
or
1086-
node instanceof CastNode
1097+
node instanceof FlowCheckNode
10871098
or
10881099
config.isSink(node)
10891100
}
@@ -1127,14 +1138,14 @@ private module LocalFlowBigStep {
11271138
exists(Node mid |
11281139
localFlowStepPlus(node1, mid, preservesValue, t, config, cc) and
11291140
localFlowStepNodeCand1(mid, node2, config) and
1130-
not mid instanceof CastNode and
1141+
not mid instanceof FlowCheckNode and
11311142
nodeCand2(node2, unbind(config))
11321143
)
11331144
or
11341145
exists(Node mid |
11351146
localFlowStepPlus(node1, mid, _, _, config, cc) and
11361147
additionalLocalFlowStepNodeCand2(mid, node2, config) and
1137-
not mid instanceof CastNode and
1148+
not mid instanceof FlowCheckNode and
11381149
preservesValue = false and
11391150
t = getErasedNodeTypeBound(node2) and
11401151
nodeCand2(node2, unbind(config))
@@ -1190,6 +1201,7 @@ private predicate flowCandFwd(
11901201
Configuration config
11911202
) {
11921203
flowCandFwd0(node, fromArg, argApf, apf, config) and
1204+
not apf.isClearedAt(node) and
11931205
if node instanceof CastingNode
11941206
then compatibleTypes(getErasedNodeTypeBound(node), apf.getType())
11951207
else any()

0 commit comments

Comments
 (0)