Skip to content

Commit a0ef795

Browse files
committed
Updating FlowAfterFree to not enforce dominance of source/sink. DoubleFree and UseAfterFree queries now enforce dominance.
1 parent e18ee79 commit a0ef795

File tree

3 files changed

+56
-23
lines changed

3 files changed

+56
-23
lines changed

cpp/ql/src/Critical/DoubleFree.ql

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313

1414
import cpp
1515
import semmle.code.cpp.dataflow.new.DataFlow
16+
import semmle.code.cpp.ir.IR
1617
import FlowAfterFree
1718
import DoubleFree::PathGraph
1819

@@ -43,11 +44,26 @@ predicate isExcludeFreePair(DeallocationExpr dealloc1, Expr e) {
4344

4445
module DoubleFree = FlowFromFree<isFree/2, isExcludeFreePair/2>;
4546

46-
from DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2
47+
/*
48+
* In order to reduce false positives, the set of sinks is restricted to only those
49+
* that satisfy at least one of the following two criteria:
50+
* 1. The source dominates the sink, or
51+
* 2. The sink post-dominates the source.
52+
*/
53+
54+
from
55+
DoubleFree::PathNode source, DoubleFree::PathNode sink, DeallocationExpr dealloc, Expr e2,
56+
DataFlow::Node srcNode, DataFlow::Node sinkNode
4757
where
4858
DoubleFree::flowPath(source, sink) and
49-
isFree(source.getNode(), _, _, dealloc) and
50-
isFree(sink.getNode(), e2)
51-
select sink.getNode(), source, sink,
59+
source.getNode() = srcNode and
60+
sink.getNode() = sinkNode and
61+
isFree(srcNode, _, _, dealloc) and
62+
isFree(sinkNode, e2) and
63+
(
64+
sinkStrictlyPostDominatesSource(srcNode, sinkNode) or
65+
sourceStrictlyDominatesSink(srcNode, sinkNode)
66+
)
67+
select sinkNode, source, sink,
5268
"Memory pointed to by '" + e2.toString() + "' may already have been freed by $@.", dealloc,
5369
dealloc.toString()

cpp/ql/src/Critical/FlowAfterFree.qll

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -38,14 +38,25 @@ predicate strictlyDominates(IRBlock b1, int i1, IRBlock b2, int i2) {
3838
b1.strictlyDominates(b2)
3939
}
4040

41+
predicate sinkStrictlyPostDominatesSource(DataFlow::Node source, DataFlow::Node sink) {
42+
exists(IRBlock b1, int i1, IRBlock b2, int i2 |
43+
source.hasIndexInBlock(b1, i1) and
44+
sink.hasIndexInBlock(b2, i2) and
45+
strictlyPostDominates(b2, i2, b1, i1)
46+
)
47+
}
48+
49+
predicate sourceStrictlyDominatesSink(DataFlow::Node source, DataFlow::Node sink) {
50+
exists(IRBlock b1, int i1, IRBlock b2, int i2 |
51+
source.hasIndexInBlock(b1, i1) and
52+
sink.hasIndexInBlock(b2, i2) and
53+
strictlyDominates(b1, i1, b2, i2)
54+
)
55+
}
56+
4157
/**
4258
* Constructs a `FlowFromFreeConfig` module that can be used to find flow between
4359
* a pointer being freed by some deallocation function, and a user-specified sink.
44-
*
45-
* In order to reduce false positives, the set of sinks is restricted to only those
46-
* that satisfy at least one of the following two criteria:
47-
* 1. The source dominates the sink, or
48-
* 2. The sink post-dominates the source.
4960
*/
5061
module FlowFromFree<isSinkSig/2 isASink, isExcludedSig/2 isExcluded> {
5162
module FlowFromFreeConfig implements DataFlow::StateConfigSig {
@@ -59,20 +70,11 @@ module FlowFromFree<isSinkSig/2 isASink, isExcludedSig/2 isExcluded> {
5970

6071
pragma[inline]
6172
predicate isSink(DataFlow::Node sink, FlowState state) {
62-
exists(
63-
Expr e, DataFlow::Node source, IRBlock b1, int i1, IRBlock b2, int i2,
64-
DeallocationExpr dealloc
65-
|
73+
exists(Expr e, DeallocationExpr dealloc |
6674
isASink(sink, e) and
67-
isFree(source, _, state, dealloc) and
75+
isFree(_, _, state, dealloc) and
6876
e != state and
69-
source.hasIndexInBlock(b1, i1) and
70-
sink.hasIndexInBlock(b2, i2) and
7177
not isExcluded(dealloc, e)
72-
|
73-
strictlyDominates(b1, i1, b2, i2)
74-
or
75-
strictlyPostDominates(b2, i2, b1, i1)
7678
)
7779
}
7880

cpp/ql/src/Critical/UseAfterFree.ql

Lines changed: 18 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -175,9 +175,24 @@ predicate isExcludeFreeUsePair(DeallocationExpr dealloc1, Expr e) {
175175

176176
module UseAfterFree = FlowFromFree<isUse/2, isExcludeFreeUsePair/2>;
177177

178-
from UseAfterFree::PathNode source, UseAfterFree::PathNode sink, DeallocationExpr dealloc
178+
/*
179+
* In order to reduce false positives, the set of sinks is restricted to only those
180+
* that satisfy at least one of the following two criteria:
181+
* 1. The source dominates the sink, or
182+
* 2. The sink post-dominates the source.
183+
*/
184+
185+
from
186+
UseAfterFree::PathNode source, UseAfterFree::PathNode sink, DeallocationExpr dealloc,
187+
DataFlow::Node srcNode, DataFlow::Node sinkNode
179188
where
180189
UseAfterFree::flowPath(source, sink) and
181-
isFree(source.getNode(), _, _, dealloc)
182-
select sink.getNode(), source, sink, "Memory may have been previously freed by $@.", dealloc,
190+
source.getNode() = srcNode and
191+
sink.getNode() = sinkNode and
192+
isFree(srcNode, _, _, dealloc) and
193+
(
194+
sinkStrictlyPostDominatesSource(srcNode, sinkNode) or
195+
sourceStrictlyDominatesSink(srcNode, sinkNode)
196+
)
197+
select sinkNode, source, sink, "Memory may have been previously freed by $@.", dealloc,
183198
dealloc.toString()

0 commit comments

Comments
 (0)