Skip to content

C++: Fix some FPs in cpp/invalid-pointer-deref #12961

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -233,26 +233,64 @@ module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {

module InvalidPointerToDerefFlow = DataFlow::Global<InvalidPointerToDerefConfig>;

/**
* Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
* pointer-value that is non-strictly upper bounded by `pai + delta`.
*
* For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
* as `(p + size) + 1` and `source` is the node representing `(p + size) + 1`. In this
* case `delta` is 1.
*/
predicate invalidPointerToDerefSource(
PointerArithmeticInstruction pai, DataFlow::Node source, int delta
) {
exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
pragma[only_bind_out](p.getNode()) = sink1 and
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p), _) and
isSinkImpl(pai, sink1, _, _) and
bounded2(source.asInstruction(), pai, delta) and
delta >= 0
)
module InvalidPointerToDerefSource {
private predicate conversionStep(Instruction iFrom, Instruction iTo) {
iTo.(CopyValueInstruction).getSourceValue() = iFrom or
iTo.(ConvertInstruction).getUnary() = iFrom or
iTo.(CheckedConvertOrNullInstruction).getUnary() = iFrom or
iTo.(InheritanceConversionInstruction).getUnary() = iFrom or
// it's fine to treat pointer arithmetic as conversions as conversions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// it's fine to treat pointer arithmetic as conversions as conversions
// it's fine to treat pointer arithmetic as conversions

// here as we'll use the range analysis library to ensure that the pointer
// arithmetic operation didn't modify the value too much (see the uses of
// `bounded2` in `invalidPointerToDerefSource`).
iTo.(PointerArithmeticInstruction).getLeft() = iFrom
}

/** Holds if `instr` flows to a `StoreInstruction`'s source value operand. */
private predicate isStored(Instruction instr) {
instr = any(StoreInstruction store).getSourceValue()
or
exists(Instruction i | isStored(i) and conversionStep(instr, i))
}

/** Holds if `instr` flows to a `LoadInstruction`'s source address operand. */
private predicate isLoaded(Instruction instr) {
instr = any(LoadInstruction store).getSourceAddress()
or
exists(Instruction i | isLoaded(i) and conversionStep(instr, i))
}

/**
* A `PointerArithmeticInstruction` that either flows to a `StoreInstruction`'s value
* operand, or is used as an address in a `LoadInstruction`.
*/
private class StoredOrLoadedPointerArithmeticInstruction extends PointerArithmeticInstruction {
StoredOrLoadedPointerArithmeticInstruction() { isStored(this) or isLoaded(this) }
}

/**
* Holds if `pai` is a pointer-arithmetic operation and `source` is a dataflow node with a
* pointer-value that is non-strictly upper bounded by `pai + delta`.
*
* For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
* as `(p + size) + 1` and `source` is the node representing `(p + size) + 1`. In this
* case `delta` is 1.
*/
predicate invalidPointerToDerefSource(
StoredOrLoadedPointerArithmeticInstruction pai, DataFlow::Node source, int delta
) {
exists(AllocToInvalidPointerFlow::PathNode1 p, DataFlow::Node sink1 |
pragma[only_bind_out](p.getNode()) = sink1 and
AllocToInvalidPointerFlow::flowPath(_, _, pragma[only_bind_into](p), _) and
isSinkImpl(pai, sink1, _, _) and
bounded2(source.asInstruction(), pai, delta) and
delta >= 0
)
}
}

import InvalidPointerToDerefSource

newtype TMergedPathNode =
// The path nodes computed by the first projection of `AllocToInvalidPointerConf`
TPathNode1(AllocToInvalidPointerFlow::PathNode1 p) or
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -576,16 +576,10 @@ edges
| test.cpp:213:6:213:6 | q | test.cpp:213:5:213:13 | Store: ... = ... |
| test.cpp:221:17:221:22 | call to malloc | test.cpp:222:5:222:5 | p |
| test.cpp:231:18:231:30 | new[] | test.cpp:232:3:232:9 | newname |
| test.cpp:232:3:232:9 | newname | test.cpp:232:3:232:16 | access to array |
| test.cpp:232:3:232:16 | access to array | test.cpp:232:3:232:20 | Store: ... = ... |
| test.cpp:238:20:238:32 | new[] | test.cpp:239:5:239:11 | newname |
| test.cpp:239:5:239:11 | newname | test.cpp:239:5:239:18 | access to array |
| test.cpp:239:5:239:18 | access to array | test.cpp:239:5:239:22 | Store: ... = ... |
| test.cpp:248:24:248:30 | call to realloc | test.cpp:249:9:249:9 | p |
| test.cpp:248:24:248:30 | call to realloc | test.cpp:250:22:250:22 | p |
| test.cpp:248:24:248:30 | call to realloc | test.cpp:254:9:254:9 | p |
| test.cpp:254:9:254:9 | p | test.cpp:254:9:254:12 | access to array |
| test.cpp:254:9:254:12 | access to array | test.cpp:254:9:254:16 | Store: ... = ... |
| test.cpp:260:13:260:24 | new[] | test.cpp:261:14:261:15 | xs |
| test.cpp:261:14:261:15 | xs | test.cpp:261:14:261:21 | ... + ... |
| test.cpp:261:14:261:15 | xs | test.cpp:261:14:261:21 | ... + ... |
Expand Down Expand Up @@ -716,9 +710,6 @@ edges
| test.cpp:171:9:171:14 | Store: ... = ... | test.cpp:143:18:143:23 | call to malloc | test.cpp:171:9:171:14 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:143:18:143:23 | call to malloc | call to malloc | test.cpp:144:29:144:32 | size | size |
| test.cpp:201:5:201:19 | Store: ... = ... | test.cpp:194:23:194:28 | call to malloc | test.cpp:201:5:201:19 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:194:23:194:28 | call to malloc | call to malloc | test.cpp:195:21:195:23 | len | len |
| test.cpp:213:5:213:13 | Store: ... = ... | test.cpp:205:23:205:28 | call to malloc | test.cpp:213:5:213:13 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:205:23:205:28 | call to malloc | call to malloc | test.cpp:206:21:206:23 | len | len |
| test.cpp:232:3:232:20 | Store: ... = ... | test.cpp:231:18:231:30 | new[] | test.cpp:232:3:232:20 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:231:18:231:30 | new[] | new[] | test.cpp:232:11:232:15 | index | index |
| test.cpp:239:5:239:22 | Store: ... = ... | test.cpp:238:20:238:32 | new[] | test.cpp:239:5:239:22 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:238:20:238:32 | new[] | new[] | test.cpp:239:13:239:17 | index | index |
| test.cpp:254:9:254:16 | Store: ... = ... | test.cpp:248:24:248:30 | call to realloc | test.cpp:254:9:254:16 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:248:24:248:30 | call to realloc | call to realloc | test.cpp:254:11:254:11 | i | i |
| test.cpp:264:13:264:14 | Load: * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
| test.cpp:264:13:264:14 | Load: * ... | test.cpp:260:13:260:24 | new[] | test.cpp:264:13:264:14 | Load: * ... | This read might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:260:13:260:24 | new[] | new[] | test.cpp:261:19:261:21 | len | len |
| test.cpp:274:5:274:10 | Store: ... = ... | test.cpp:270:13:270:24 | new[] | test.cpp:274:5:274:10 | Store: ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:270:13:270:24 | new[] | new[] | test.cpp:271:19:271:21 | len | len |
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -229,14 +229,14 @@ void test15(unsigned index) {
return;
}
int* newname = new int[size];
newname[index] = 0; // GOOD [FALSE POSITIVE]
newname[index] = 0; // GOOD
}

void test16(unsigned index) {
unsigned size = index + 13;
if(size >= index) {
int* newname = new int[size];
newname[index] = 0; // GOOD [FALSE POSITIVE]
newname[index] = 0; // GOOD
}
}

Expand All @@ -251,7 +251,7 @@ void test17(unsigned *p, unsigned x, unsigned k) {
// The following access is okay because:
// n = 3*p[0] + k >= p[0] + k >= p[1] + k > p[1] = i
// (where p[0] denotes the original value for p[0])
p[i] = x; // GOOD [FALSE POSITIVE]
p[i] = x; // GOOD
}
}

Expand Down