C++: Take into account the delta at the final sink in cpp/invalid-pointer-deref

This commit is contained in:
Jeroen Ketema
2023-05-30 18:23:22 +02:00
parent de974cc18a
commit f5ed02a433
2 changed files with 13 additions and 19 deletions

View File

@@ -185,8 +185,8 @@ predicate isSinkImpl(
* reads from an address that non-strictly upper-bounds `sink`.
*/
pragma[inline]
predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string operation) {
exists(AddressOperand addr, int delta |
predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string operation, int delta) {
exists(AddressOperand addr |
bounded1(addr.getDef(), sink.asInstruction(), delta) and
delta >= 0 and
i.getAnOperand() = addr
@@ -207,7 +207,7 @@ module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) { invalidPointerToDerefSource(_, source, _) }
pragma[inline]
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _) }
predicate isSink(DataFlow::Node sink) { isInvalidPointerDerefSink(sink, _, _, _) }
predicate isBarrier(DataFlow::Node node) {
node = any(DataFlow::SsaPhiNode phi | not phi.isPhiRead()).getAnInput(true)
@@ -247,7 +247,7 @@ newtype TMergedPathNode =
TPathNodeSink(Instruction i) {
exists(DataFlow::Node n |
InvalidPointerToDerefFlow::flowTo(n) and
isInvalidPointerDerefSink(n, i, _)
isInvalidPointerDerefSink(n, i, _, _)
)
}
@@ -321,7 +321,7 @@ query predicate edges(MergedPathNode node1, MergedPathNode node2) {
or
node1.asPathNode3().getASuccessor() = node2.asPathNode3()
or
joinOn2(node1.asPathNode3(), node2.asSinkNode(), _)
joinOn2(node1.asPathNode3(), node2.asSinkNode(), _, _)
}
query predicate subpaths(
@@ -352,32 +352,32 @@ predicate joinOn1(
* a `StoreInstruction` or `LoadInstruction`.
*/
pragma[inline]
predicate joinOn2(InvalidPointerToDerefFlow::PathNode p1, Instruction i, string operation) {
isInvalidPointerDerefSink(p1.getNode(), i, operation)
predicate joinOn2(InvalidPointerToDerefFlow::PathNode p1, Instruction i, string operation, int delta) {
isInvalidPointerDerefSink(p1.getNode(), i, operation, delta)
}
predicate hasFlowPath(
MergedPathNode source1, MergedPathNode sink, InvalidPointerToDerefFlow::PathNode source3,
PointerArithmeticInstruction pai, string operation
PointerArithmeticInstruction pai, string operation, int delta
) {
exists(InvalidPointerToDerefFlow::PathNode sink3, AllocToInvalidPointerFlow::PathNode1 sink1 |
AllocToInvalidPointerFlow::flowPath(source1.asPathNode1(), _, sink1, _) and
joinOn1(pai, sink1, source3) and
InvalidPointerToDerefFlow::flowPath(source3, sink3) and
joinOn2(sink3, sink.asSinkNode(), operation)
joinOn2(sink3, sink.asSinkNode(), operation, delta)
)
}
from
MergedPathNode source, MergedPathNode sink, int k, string kstr,
MergedPathNode source, MergedPathNode sink, int k2, int k3, string kstr,
InvalidPointerToDerefFlow::PathNode source3, PointerArithmeticInstruction pai, string operation,
Expr offset, DataFlow::Node n
where
hasFlowPath(source, sink, source3, pai, operation) and
invalidPointerToDerefSource(pai, source3.getNode(), k) and
hasFlowPath(source, sink, source3, pai, operation, k3) and
invalidPointerToDerefSource(pai, source3.getNode(), k2) and
offset = pai.getRight().getUnconvertedResultExpression() and
n = source.asPathNode1().getNode() and
if k = 0 then kstr = "" else kstr = " + " + k
if (k2 + k3) = 0 then kstr = "" else kstr = " + " + (k2 + k3)
select sink, source, sink,
"This " + operation + " might be out of bounds, as the pointer might be equal to $@ + $@" + kstr +
".", n, n.toString(), offset, offset.toString()

View File

@@ -727,14 +727,11 @@ subpaths
#select
| test.cpp:6:14:6:15 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:6:14:6:15 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
| test.cpp:8:14:8:21 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:8:14:8:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
| test.cpp:8:14:8:21 | Load: * ... | test.cpp:4:15:4:20 | call to malloc | test.cpp:8:14:8:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:4:15:4:20 | call to malloc | call to malloc | test.cpp:5:19:5:22 | size | size |
| test.cpp:20:14:20:21 | Load: * ... | test.cpp:16:15:16:20 | call to malloc | test.cpp:20:14:20:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:16:15:16:20 | call to malloc | call to malloc | test.cpp:17:19:17:22 | size | size |
| test.cpp:30:14:30:15 | Load: * ... | test.cpp:28:15:28:20 | call to malloc | test.cpp:30:14:30:15 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:28:15:28:20 | call to malloc | call to malloc | test.cpp:29:20:29:27 | ... + ... | ... + ... |
| test.cpp:32:14:32:21 | Load: * ... | test.cpp:28:15:28:20 | call to malloc | test.cpp:32:14:32:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:28:15:28:20 | call to malloc | call to malloc | test.cpp:29:20:29:27 | ... + ... | ... + ... |
| test.cpp:32:14:32:21 | Load: * ... | test.cpp:28:15:28:20 | call to malloc | test.cpp:32:14:32:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:28:15:28:20 | call to malloc | call to malloc | test.cpp:29:20:29:27 | ... + ... | ... + ... |
| test.cpp:42:14:42:15 | Load: * ... | test.cpp:40:15:40:20 | call to malloc | test.cpp:42:14:42:15 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:40:15:40:20 | call to malloc | call to malloc | test.cpp:41:20:41:27 | ... - ... | ... - ... |
| test.cpp:44:14:44:21 | Load: * ... | test.cpp:40:15:40:20 | call to malloc | test.cpp:44:14:44:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:40:15:40:20 | call to malloc | call to malloc | test.cpp:41:20:41:27 | ... - ... | ... - ... |
| test.cpp:44:14:44:21 | Load: * ... | test.cpp:40:15:40:20 | call to malloc | test.cpp:44:14:44:21 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:40:15:40:20 | call to malloc | call to malloc | test.cpp:41:20:41:27 | ... - ... | ... - ... |
| test.cpp:67:9:67:14 | Store: ... = ... | test.cpp:52:19:52:24 | call to malloc | test.cpp:67:9:67:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:52:19:52:24 | call to malloc | call to malloc | test.cpp:53:20:53:23 | size | size |
| test.cpp:96:9:96:14 | Store: ... = ... | test.cpp:82:17:82:22 | call to malloc | test.cpp:96:9:96:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:82:17:82:22 | call to malloc | call to malloc | test.cpp:83:27:83:30 | size | size |
| test.cpp:110:9:110:14 | Store: ... = ... | test.cpp:82:17:82:22 | call to malloc | test.cpp:110:9:110:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:82:17:82:22 | call to malloc | call to malloc | test.cpp:83:27:83:30 | size | size |
@@ -752,7 +749,4 @@ subpaths
| test.cpp:341:5:341:21 | Store: ... = ... | test.cpp:325:14:325:27 | new[] | test.cpp:341:5:341:21 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:325:14:325:27 | new[] | new[] | test.cpp:326:20:326:23 | size | size |
| test.cpp:350:15:350:19 | Load: * ... | test.cpp:347:14:347:27 | new[] | test.cpp:350:15:350:19 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:347:14:347:27 | new[] | new[] | test.cpp:348:20:348:23 | size | size |
| test.cpp:358:14:358:26 | Load: * ... | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:358:14:358:26 | Load: * ... | test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:359:14:359:32 | Load: * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:359:14:359:32 | Load: * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 2. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |
| test.cpp:359:14:359:32 | Load: * ... | test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:355:14:355:27 | new[] | new[] | test.cpp:356:20:356:23 | size | size |