Merge branch 'main' into add-more-invalid-deref-documentation

This commit is contained in:
Mathias Vorreiter Pedersen
2023-07-24 12:09:19 +02:00
73 changed files with 1144 additions and 868 deletions

View File

@@ -92,16 +92,14 @@ predicate hasSize(HeuristicAllocationExpr alloc, DataFlow::Node n, int state) {
* ```
* In this case, the sink pair identified by the product flow library (without any additional barriers)
* would be `(p, n)` (where `n` is the `n` in `p[n]`), because there exists a pointer-arithmetic
* instruction `pai` such that:
* 1. The left-hand of `pai` flows from the allocation, and
* 2. The right-hand of `pai` is non-strictly upper bounded by `n` (where `n` is the `n` in `p[n]`)
* instruction `pai = a + b` such that:
* 1. the allocation flows to `a`, and
* 2. `b <= n` where `n` is the `n` in `p[n]`
* but because there's a strict comparison that compares `n` against the size of the allocation this
* snippet is fine.
*/
module Barrier2 {
private class FlowState2 = int;
private module BarrierConfig2 implements DataFlow::ConfigSig {
module SizeBarrier {
private module SizeBarrierConfig implements DataFlow::ConfigSig {
predicate isSource(DataFlow::Node source) {
// The sources is the same as in the sources for the second
// projection in the `AllocToInvalidPointerConfig` module.
@@ -109,19 +107,19 @@ module Barrier2 {
}
additional predicate isSink(
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, FlowState2 state,
boolean testIsTrue
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, int k, boolean testIsTrue
) {
// The sink is any "large" side of a relational comparison.
g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
// The sink is any "large" side of a relational comparison. i.e., the `right` expression
// in a guard such as `left < right + k`.
g.comparesLt(left.asOperand(), right.asOperand(), k, true, testIsTrue)
}
predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
}
private import DataFlow::Global<BarrierConfig2>
private import DataFlow::Global<SizeBarrierConfig>
private FlowState2 getAFlowStateForNode(DataFlow::Node node) {
private int getAFlowStateForNode(DataFlow::Node node) {
exists(DataFlow::Node source |
flow(source, node) and
hasSize(_, source, result)
@@ -129,14 +127,14 @@ module Barrier2 {
}
private predicate operandGuardChecks(
IRGuardCondition g, Operand left, Operand right, FlowState2 state, boolean edge
IRGuardCondition g, Operand left, Operand right, int state, boolean edge
) {
exists(DataFlow::Node nLeft, DataFlow::Node nRight, FlowState2 state0 |
exists(DataFlow::Node nLeft, DataFlow::Node nRight, int k |
nRight.asOperand() = right and
nLeft.asOperand() = left and
BarrierConfig2::isSink(nLeft, nRight, g, state0, edge) and
SizeBarrierConfig::isSink(nLeft, nRight, g, k, edge) and
state = getAFlowStateForNode(nRight) and
state0 <= state
k <= state
)
}
@@ -144,7 +142,7 @@ module Barrier2 {
* Gets an instruction that is guarded by a guard condition which ensures that
* the value of the instruction is upper-bounded by size of some allocation.
*/
Instruction getABarrierInstruction(FlowState2 state) {
Instruction getABarrierInstruction(int state) {
exists(IRGuardCondition g, ValueNumber value, Operand use, boolean edge |
use = value.getAUse() and
operandGuardChecks(pragma[only_bind_into](g), pragma[only_bind_into](use), _,
@@ -158,7 +156,7 @@ module Barrier2 {
* Gets a `DataFlow::Node` that is guarded by a guard condition which ensures that
* the value of the node is upper-bounded by size of some allocation.
*/
DataFlow::Node getABarrierNode(FlowState2 state) {
DataFlow::Node getABarrierNode(int state) {
result.asOperand() = getABarrierInstruction(state).getAUse()
}
@@ -166,9 +164,7 @@ module Barrier2 {
* Gets the block of a node that is guarded (see `getABarrierInstruction` or
* `getABarrierNode` for the definition of what it means to be guarded).
*/
IRBlock getABarrierBlock(FlowState2 state) {
result.getAnInstruction() = getABarrierInstruction(state)
}
IRBlock getABarrierBlock(int state) { result.getAnInstruction() = getABarrierInstruction(state) }
}
private module InterestingPointerAddInstruction {
@@ -201,8 +197,8 @@ private module InterestingPointerAddInstruction {
}
/**
* A product-flow configuration for flow from an `(allocation, size)` pair to a pointer-
* arithmetic instruction that is non-strictly upper-bounded by `allocation + size`.
* A product-flow configuration for flow from an `(allocation, size)` pair to a
* pointer-arithmetic operation `pai` such that `pai <= allocation + size`.
*/
private module Config implements ProductFlow::StateConfigSig {
class FlowState1 = Unit;
@@ -210,7 +206,7 @@ private module Config implements ProductFlow::StateConfigSig {
class FlowState2 = int;
predicate isSourcePair(
DataFlow::Node source1, FlowState1 state1, DataFlow::Node source2, FlowState2 state2
DataFlow::Node allocSource, FlowState1 unit, DataFlow::Node sizeSource, FlowState2 sizeAddend
) {
// In the case of an allocation like
// ```cpp
@@ -218,21 +214,21 @@ private module Config implements ProductFlow::StateConfigSig {
// ```
// we use `state2` to remember that there was an offset (in this case an offset of `1`) added
// to the size of the allocation. This state is then checked in `isSinkPair`.
exists(state1) and
hasSize(source1.asConvertedExpr(), source2, state2)
exists(unit) and
hasSize(allocSource.asConvertedExpr(), sizeSource, sizeAddend)
}
predicate isSinkPair(
DataFlow::Node sink1, FlowState1 state1, DataFlow::Node sink2, FlowState2 state2
DataFlow::Node allocSink, FlowState1 unit, DataFlow::Node sizeSink, FlowState2 sizeAddend
) {
exists(state1) and
exists(unit) and
// We check that the delta computed by the range analysis matches the
// state value that we set in `isSourcePair`.
pointerAddInstructionHasBounds0(_, sink1, sink2, state2)
pointerAddInstructionHasBounds0(_, allocSink, sizeSink, sizeAddend)
}
predicate isBarrier2(DataFlow::Node node, FlowState2 state) {
node = Barrier2::getABarrierNode(state)
node = SizeBarrier::getABarrierNode(state)
}
predicate isBarrierIn1(DataFlow::Node node) { isSourcePair(node, _, _, _) }
@@ -245,7 +241,7 @@ private module Config implements ProductFlow::StateConfigSig {
private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<Config>;
/**
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
* Holds if `pai` is non-strictly upper bounded by `sizeSink + delta` and `allocSink` is the
* left operand of the pointer-arithmetic operation.
*
* For example in,
@@ -254,37 +250,37 @@ private module AllocToInvalidPointerFlow = ProductFlow::GlobalWithState<Config>;
* ```
* We will have:
* - `pai` is `p + (size + 1)`,
* - `sink1` is `p`
* - `sink2` is `size`
* - `allocSink` is `p`
* - `sizeSink` is `size`
* - `delta` is `1`.
*/
pragma[nomagic]
private predicate pointerAddInstructionHasBounds0(
PointerAddInstruction pai, DataFlow::Node sink1, DataFlow::Node sink2, int delta
PointerAddInstruction pai, DataFlow::Node allocSink, DataFlow::Node sizeSink, int delta
) {
InterestingPointerAddInstruction::isInteresting(pragma[only_bind_into](pai)) and
exists(Instruction right, Instruction instr2 |
exists(Instruction right, Instruction sizeInstr |
pai.getRight() = right and
pai.getLeft() = sink1.asInstruction() and
instr2 = sink2.asInstruction() and
// pai.getRight() <= sink2 + delta
bounded1(right, instr2, delta) and
not right = Barrier2::getABarrierInstruction(delta) and
not instr2 = Barrier2::getABarrierInstruction(delta)
pai.getLeft() = allocSink.asInstruction() and
sizeInstr = sizeSink.asInstruction() and
// pai.getRight() <= sizeSink + delta
bounded1(right, sizeInstr, delta) and
not right = SizeBarrier::getABarrierInstruction(delta) and
not sizeInstr = SizeBarrier::getABarrierInstruction(delta)
)
}
/**
* Holds if `allocation` flows to `sink1` and `sink1` represents the left-hand
* side of the pointer-arithmetic instruction `pai`, and the right-hand side of `pai`
* is non-strictly upper bounded by the size of `alllocation` + `delta`.
* Holds if `allocation` flows to `allocSink` and `allocSink` represents the left operand
* of the pointer-arithmetic instruction `pai = a + b` (i.e., `allocSink = a`), and
* `b <= allocation + delta`.
*/
pragma[nomagic]
predicate pointerAddInstructionHasBounds(
DataFlow::Node allocation, PointerAddInstruction pai, DataFlow::Node sink1, int delta
DataFlow::Node allocation, PointerAddInstruction pai, DataFlow::Node allocSink, int delta
) {
exists(DataFlow::Node sink2 |
AllocToInvalidPointerFlow::flow(allocation, _, sink1, sink2) and
pointerAddInstructionHasBounds0(pai, sink1, sink2, delta)
exists(DataFlow::Node sizeSink |
AllocToInvalidPointerFlow::flow(allocation, _, allocSink, sizeSink) and
pointerAddInstructionHasBounds0(pai, allocSink, sizeSink, delta)
)
}

View File

@@ -84,10 +84,10 @@ private module InvalidPointerToDerefBarrier {
}
additional predicate isSink(
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, int state, boolean testIsTrue
DataFlow::Node left, DataFlow::Node right, IRGuardCondition g, int k, boolean testIsTrue
) {
// The sink is any "large" side of a relational comparison.
g.comparesLt(left.asOperand(), right.asOperand(), state, true, testIsTrue)
g.comparesLt(left.asOperand(), right.asOperand(), k, true, testIsTrue)
}
predicate isSink(DataFlow::Node sink) { isSink(_, sink, _, _, _) }
@@ -105,12 +105,12 @@ private module InvalidPointerToDerefBarrier {
private predicate operandGuardChecks(
IRGuardCondition g, Operand left, Operand right, int state, boolean edge
) {
exists(DataFlow::Node nLeft, DataFlow::Node nRight, int state0 |
exists(DataFlow::Node nLeft, DataFlow::Node nRight, int k |
nRight.asOperand() = right and
nLeft.asOperand() = left and
BarrierConfig::isSink(nLeft, nRight, g, state0, edge) and
BarrierConfig::isSink(nLeft, nRight, g, k, edge) and
state = getInvalidPointerToDerefSourceDelta(nRight) and
state0 <= state
k <= state
)
}
@@ -150,47 +150,50 @@ private module InvalidPointerToDerefConfig implements DataFlow::ConfigSig {
private import DataFlow::Global<InvalidPointerToDerefConfig>
/**
* Holds if `source1` is dataflow node that represents an allocation that flows to the
* left-hand side of the pointer-arithmetic `pai`, and `derefSource` is a dataflow node with
* a pointer-value that is non-strictly upper bounded by `pai + delta`.
* Holds if `allocSource` is dataflow node that represents an allocation that flows to the
* left-hand side of the pointer-arithmetic `pai`, and `derefSource <= pai + derefSourcePaiDelta`.
*
* For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
* as `(p + size) + 1` and `derefSource` is the node representing `(p + size) + 1`. In this
* case `delta` is 1.
* case `derefSourcePaiDelta` is 1.
*/
private predicate invalidPointerToDerefSource(
DataFlow::Node source1, PointerArithmeticInstruction pai, DataFlow::Node derefSource, int delta
DataFlow::Node allocSource, PointerArithmeticInstruction pai, DataFlow::Node derefSource,
int deltaDerefSourceAndPai
) {
exists(int delta0 |
// Note that `delta` is not necessarily equal to `delta0`:
// `delta0` is the constant offset added to the size of the allocation, and
// delta is the constant difference between the pointer-arithmetic instruction
exists(int rhsSizeDelta |
// Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
// `rhsSizeDelta` is the constant offset added to the size of the allocation, and
// `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
// and the instruction computing the address for which we will search for a dereference.
AllocToInvalidPointer::pointerAddInstructionHasBounds(source1, pai, _, delta0) and
bounded2(derefSource.asInstruction(), pai, delta) and
delta >= 0 and
AllocToInvalidPointer::pointerAddInstructionHasBounds(allocSource, pai, _, rhsSizeDelta) and
// pai <= derefSource + deltaDerefSourceAndPai and deltaDerefSourceAndPai <= 0 is equivalent to
// derefSource >= pai + deltaDerefSourceAndPai and deltaDerefSourceAndPai >= 0
bounded1(pai, derefSource.asInstruction(), deltaDerefSourceAndPai) and
deltaDerefSourceAndPai <= 0 and
// TODO: This condition will go away once #13725 is merged, and then we can make `Barrier2`
// private to `AllocationToInvalidPointer.qll`.
not derefSource.getBasicBlock() = AllocToInvalidPointer::Barrier2::getABarrierBlock(delta0)
not derefSource.getBasicBlock() =
AllocToInvalidPointer::SizeBarrier::getABarrierBlock(rhsSizeDelta)
)
}
/**
* Holds if `sink` is a sink for `InvalidPointerToDerefConfig` and `i` is a `StoreInstruction` that
* writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
* reads from an address that non-strictly upper-bounds `sink`.
* writes to an address `addr` such that `addr <= sink`, or `i` is a `LoadInstruction` that
* reads from an address `addr` such that `addr <= sink`.
*/
pragma[inline]
private predicate isInvalidPointerDerefSink(
DataFlow::Node sink, Instruction i, string operation, int delta
DataFlow::Node sink, Instruction i, string operation, int deltaDerefSinkAndDerefAddress
) {
exists(AddressOperand addr, Instruction s, IRBlock b |
s = sink.asInstruction() and
bounded(addr.getDef(), s, delta) and
delta >= 0 and
bounded(addr.getDef(), s, deltaDerefSinkAndDerefAddress) and
deltaDerefSinkAndDerefAddress >= 0 and
i.getAnOperand() = addr and
b = i.getBlock() and
not b = InvalidPointerToDerefBarrier::getABarrierBlock(delta)
not b = InvalidPointerToDerefBarrier::getABarrierBlock(deltaDerefSinkAndDerefAddress)
|
i instanceof StoreInstruction and
operation = "write"
@@ -230,13 +233,13 @@ private predicate paiForDereferenceSink(PointerArithmeticInstruction pai, DataFl
*/
private predicate derefSinkToOperation(
DataFlow::Node derefSink, PointerArithmeticInstruction pai, DataFlow::Node operation,
string description, int delta
string description, int deltaDerefSinkAndDerefAddress
) {
exists(Instruction i |
exists(Instruction operationInstr |
paiForDereferenceSink(pai, pragma[only_bind_into](derefSink)) and
isInvalidPointerDerefSink(derefSink, i, description, delta) and
i = getASuccessor(derefSink.asInstruction()) and
operation.asInstruction() = i
isInvalidPointerDerefSink(derefSink, operationInstr, description, deltaDerefSinkAndDerefAddress) and
operationInstr = getASuccessor(derefSink.asInstruction()) and
operation.asInstruction() = operationInstr
)
}

View File

@@ -35,14 +35,5 @@ bindingset[i]
pragma[inline_late]
predicate bounded1(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
/**
* Holds if `i <= b + delta`.
*
* This predicate enforces a join-order that ensures that `b` has already been bound.
*/
bindingset[b]
pragma[inline_late]
predicate bounded2(Instruction i, Instruction b, int delta) { boundedImpl(i, b, delta) }
/** Holds if `i <= b + delta`. */
predicate bounded = boundedImpl/3;

View File

@@ -132,8 +132,6 @@ edges
| test.cpp:304:15:304:26 | new[] | test.cpp:308:5:308:29 | ... = ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:356:15:356:23 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:357:24:357:30 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:357:24:357:30 | ... + ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:358:14:358:26 | * ... |
| test.cpp:355:14:355:27 | new[] | test.cpp:359:14:359:32 | * ... |
| test.cpp:356:15:356:23 | ... + ... | test.cpp:356:15:356:23 | ... + ... |
@@ -141,85 +139,45 @@ edges
| test.cpp:356:15:356:23 | ... + ... | test.cpp:358:14:358:26 | * ... |
| test.cpp:356:15:356:23 | ... + ... | test.cpp:359:14:359:32 | * ... |
| test.cpp:356:15:356:23 | ... + ... | test.cpp:359:14:359:32 | * ... |
| test.cpp:357:24:357:30 | ... + ... | test.cpp:357:24:357:30 | ... + ... |
| test.cpp:357:24:357:30 | ... + ... | test.cpp:358:14:358:26 | * ... |
| test.cpp:357:24:357:30 | ... + ... | test.cpp:358:14:358:26 | * ... |
| test.cpp:357:24:357:30 | ... + ... | test.cpp:359:14:359:32 | * ... |
| test.cpp:357:24:357:30 | ... + ... | test.cpp:359:14:359:32 | * ... |
| test.cpp:377:14:377:27 | new[] | test.cpp:378:15:378:23 | ... + ... |
| test.cpp:377:14:377:27 | new[] | test.cpp:378:15:378:23 | ... + ... |
| test.cpp:377:14:377:27 | new[] | test.cpp:381:5:381:9 | ... ++ |
| test.cpp:377:14:377:27 | new[] | test.cpp:381:5:381:9 | ... ++ |
| test.cpp:377:14:377:27 | new[] | test.cpp:384:13:384:16 | * ... |
| test.cpp:378:15:378:23 | ... + ... | test.cpp:378:15:378:23 | ... + ... |
| test.cpp:378:15:378:23 | ... + ... | test.cpp:384:13:384:16 | * ... |
| test.cpp:378:15:378:23 | ... + ... | test.cpp:384:13:384:16 | * ... |
| test.cpp:381:5:381:9 | ... ++ | test.cpp:381:5:381:9 | ... ++ |
| test.cpp:381:5:381:9 | ... ++ | test.cpp:384:13:384:16 | * ... |
| test.cpp:410:14:410:27 | new[] | test.cpp:411:15:411:23 | & ... |
| test.cpp:410:14:410:27 | new[] | test.cpp:411:15:411:23 | & ... |
| test.cpp:410:14:410:27 | new[] | test.cpp:413:5:413:8 | ... ++ |
| test.cpp:410:14:410:27 | new[] | test.cpp:413:5:413:8 | ... ++ |
| test.cpp:410:14:410:27 | new[] | test.cpp:415:7:415:15 | ... = ... |
| test.cpp:411:15:411:23 | & ... | test.cpp:411:15:411:23 | & ... |
| test.cpp:411:15:411:23 | & ... | test.cpp:415:7:415:15 | ... = ... |
| test.cpp:411:15:411:23 | & ... | test.cpp:415:7:415:15 | ... = ... |
| test.cpp:413:5:413:8 | ... ++ | test.cpp:413:5:413:8 | ... ++ |
| test.cpp:413:5:413:8 | ... ++ | test.cpp:415:7:415:15 | ... = ... |
| test.cpp:413:5:413:8 | ... ++ | test.cpp:415:7:415:15 | ... = ... |
| test.cpp:421:14:421:27 | new[] | test.cpp:422:15:422:23 | & ... |
| test.cpp:421:14:421:27 | new[] | test.cpp:422:15:422:23 | & ... |
| test.cpp:421:14:421:27 | new[] | test.cpp:424:5:424:8 | ... ++ |
| test.cpp:421:14:421:27 | new[] | test.cpp:424:5:424:8 | ... ++ |
| test.cpp:421:14:421:27 | new[] | test.cpp:426:7:426:15 | ... = ... |
| test.cpp:422:15:422:23 | & ... | test.cpp:422:15:422:23 | & ... |
| test.cpp:422:15:422:23 | & ... | test.cpp:426:7:426:15 | ... = ... |
| test.cpp:422:15:422:23 | & ... | test.cpp:426:7:426:15 | ... = ... |
| test.cpp:424:5:424:8 | ... ++ | test.cpp:424:5:424:8 | ... ++ |
| test.cpp:424:5:424:8 | ... ++ | test.cpp:426:7:426:15 | ... = ... |
| test.cpp:424:5:424:8 | ... ++ | test.cpp:426:7:426:15 | ... = ... |
| test.cpp:432:14:432:27 | new[] | test.cpp:433:15:433:23 | & ... |
| test.cpp:432:14:432:27 | new[] | test.cpp:433:15:433:23 | & ... |
| test.cpp:432:14:432:27 | new[] | test.cpp:436:5:436:8 | ... ++ |
| test.cpp:432:14:432:27 | new[] | test.cpp:436:5:436:8 | ... ++ |
| test.cpp:432:14:432:27 | new[] | test.cpp:438:7:438:15 | ... = ... |
| test.cpp:433:15:433:23 | & ... | test.cpp:433:15:433:23 | & ... |
| test.cpp:433:15:433:23 | & ... | test.cpp:438:7:438:15 | ... = ... |
| test.cpp:433:15:433:23 | & ... | test.cpp:438:7:438:15 | ... = ... |
| test.cpp:436:5:436:8 | ... ++ | test.cpp:436:5:436:8 | ... ++ |
| test.cpp:436:5:436:8 | ... ++ | test.cpp:438:7:438:15 | ... = ... |
| test.cpp:436:5:436:8 | ... ++ | test.cpp:438:7:438:15 | ... = ... |
| test.cpp:444:14:444:27 | new[] | test.cpp:445:15:445:23 | & ... |
| test.cpp:444:14:444:27 | new[] | test.cpp:445:15:445:23 | & ... |
| test.cpp:444:14:444:27 | new[] | test.cpp:448:5:448:8 | ... ++ |
| test.cpp:444:14:444:27 | new[] | test.cpp:448:5:448:8 | ... ++ |
| test.cpp:444:14:444:27 | new[] | test.cpp:450:7:450:15 | ... = ... |
| test.cpp:445:15:445:23 | & ... | test.cpp:445:15:445:23 | & ... |
| test.cpp:445:15:445:23 | & ... | test.cpp:450:7:450:15 | ... = ... |
| test.cpp:445:15:445:23 | & ... | test.cpp:450:7:450:15 | ... = ... |
| test.cpp:448:5:448:8 | ... ++ | test.cpp:448:5:448:8 | ... ++ |
| test.cpp:448:5:448:8 | ... ++ | test.cpp:450:7:450:15 | ... = ... |
| test.cpp:448:5:448:8 | ... ++ | test.cpp:450:7:450:15 | ... = ... |
| test.cpp:480:14:480:27 | new[] | test.cpp:481:15:481:23 | & ... |
| test.cpp:480:14:480:27 | new[] | test.cpp:481:15:481:23 | & ... |
| test.cpp:480:14:480:27 | new[] | test.cpp:484:5:484:8 | ... ++ |
| test.cpp:480:14:480:27 | new[] | test.cpp:484:5:484:8 | ... ++ |
| test.cpp:480:14:480:27 | new[] | test.cpp:486:7:486:15 | ... = ... |
| test.cpp:481:15:481:23 | & ... | test.cpp:481:15:481:23 | & ... |
| test.cpp:481:15:481:23 | & ... | test.cpp:486:7:486:15 | ... = ... |
| test.cpp:481:15:481:23 | & ... | test.cpp:486:7:486:15 | ... = ... |
| test.cpp:484:5:484:8 | ... ++ | test.cpp:484:5:484:8 | ... ++ |
| test.cpp:484:5:484:8 | ... ++ | test.cpp:486:7:486:15 | ... = ... |
| test.cpp:484:5:484:8 | ... ++ | test.cpp:486:7:486:15 | ... = ... |
| test.cpp:543:14:543:27 | new[] | test.cpp:548:5:548:19 | ... = ... |
| test.cpp:554:14:554:27 | new[] | test.cpp:559:5:559:19 | ... = ... |
| test.cpp:642:14:642:31 | new[] | test.cpp:647:5:647:19 | ... = ... |
| test.cpp:652:14:652:27 | new[] | test.cpp:656:3:656:6 | ... ++ |
| test.cpp:652:14:652:27 | new[] | test.cpp:656:3:656:6 | ... ++ |
| test.cpp:652:14:652:27 | new[] | test.cpp:662:3:662:11 | ... = ... |
| test.cpp:656:3:656:6 | ... ++ | test.cpp:656:3:656:6 | ... ++ |
| test.cpp:656:3:656:6 | ... ++ | test.cpp:662:3:662:11 | ... = ... |
| test.cpp:656:3:656:6 | ... ++ | test.cpp:662:3:662:11 | ... = ... |
| test.cpp:667:14:667:31 | new[] | test.cpp:675:7:675:23 | ... = ... |
nodes
| test.cpp:4:15:4:20 | call to malloc | semmle.label | call to malloc |
@@ -318,45 +276,31 @@ nodes
| test.cpp:355:14:355:27 | new[] | semmle.label | new[] |
| test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:356:15:356:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:357:24:357:30 | ... + ... | semmle.label | ... + ... |
| test.cpp:357:24:357:30 | ... + ... | semmle.label | ... + ... |
| test.cpp:358:14:358:26 | * ... | semmle.label | * ... |
| test.cpp:359:14:359:32 | * ... | semmle.label | * ... |
| test.cpp:377:14:377:27 | new[] | semmle.label | new[] |
| test.cpp:378:15:378:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:378:15:378:23 | ... + ... | semmle.label | ... + ... |
| test.cpp:381:5:381:9 | ... ++ | semmle.label | ... ++ |
| test.cpp:381:5:381:9 | ... ++ | semmle.label | ... ++ |
| test.cpp:384:13:384:16 | * ... | semmle.label | * ... |
| test.cpp:410:14:410:27 | new[] | semmle.label | new[] |
| test.cpp:411:15:411:23 | & ... | semmle.label | & ... |
| test.cpp:411:15:411:23 | & ... | semmle.label | & ... |
| test.cpp:413:5:413:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:413:5:413:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:415:7:415:15 | ... = ... | semmle.label | ... = ... |
| test.cpp:421:14:421:27 | new[] | semmle.label | new[] |
| test.cpp:422:15:422:23 | & ... | semmle.label | & ... |
| test.cpp:422:15:422:23 | & ... | semmle.label | & ... |
| test.cpp:424:5:424:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:424:5:424:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:426:7:426:15 | ... = ... | semmle.label | ... = ... |
| test.cpp:432:14:432:27 | new[] | semmle.label | new[] |
| test.cpp:433:15:433:23 | & ... | semmle.label | & ... |
| test.cpp:433:15:433:23 | & ... | semmle.label | & ... |
| test.cpp:436:5:436:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:436:5:436:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:438:7:438:15 | ... = ... | semmle.label | ... = ... |
| test.cpp:444:14:444:27 | new[] | semmle.label | new[] |
| test.cpp:445:15:445:23 | & ... | semmle.label | & ... |
| test.cpp:445:15:445:23 | & ... | semmle.label | & ... |
| test.cpp:448:5:448:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:448:5:448:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:450:7:450:15 | ... = ... | semmle.label | ... = ... |
| test.cpp:480:14:480:27 | new[] | semmle.label | new[] |
| test.cpp:481:15:481:23 | & ... | semmle.label | & ... |
| test.cpp:481:15:481:23 | & ... | semmle.label | & ... |
| test.cpp:484:5:484:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:484:5:484:8 | ... ++ | semmle.label | ... ++ |
| test.cpp:486:7:486:15 | ... = ... | semmle.label | ... = ... |
| test.cpp:543:14:543:27 | new[] | semmle.label | new[] |
| test.cpp:548:5:548:19 | ... = ... | semmle.label | ... = ... |
@@ -364,10 +308,6 @@ nodes
| test.cpp:559:5:559:19 | ... = ... | semmle.label | ... = ... |
| test.cpp:642:14:642:31 | new[] | semmle.label | new[] |
| test.cpp:647:5:647:19 | ... = ... | semmle.label | ... = ... |
| test.cpp:652:14:652:27 | new[] | semmle.label | new[] |
| test.cpp:656:3:656:6 | ... ++ | semmle.label | ... ++ |
| test.cpp:656:3:656:6 | ... ++ | semmle.label | ... ++ |
| test.cpp:662:3:662:11 | ... = ... | semmle.label | ... = ... |
| test.cpp:667:14:667:31 | new[] | semmle.label | new[] |
| test.cpp:675:7:675:23 | ... = ... | semmle.label | ... = ... |
subpaths
@@ -403,5 +343,4 @@ subpaths
| test.cpp:548:5:548:19 | ... = ... | test.cpp:543:14:543:27 | new[] | test.cpp:548:5:548:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:543:14:543:27 | new[] | new[] | test.cpp:548:8:548:14 | src_pos | src_pos |
| test.cpp:559:5:559:19 | ... = ... | test.cpp:554:14:554:27 | new[] | test.cpp:559:5:559:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:554:14:554:27 | new[] | new[] | test.cpp:559:8:559:14 | src_pos | src_pos |
| test.cpp:647:5:647:19 | ... = ... | test.cpp:642:14:642:31 | new[] | test.cpp:647:5:647:19 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:642:14:642:31 | new[] | new[] | test.cpp:647:8:647:14 | src_pos | src_pos |
| test.cpp:662:3:662:11 | ... = ... | test.cpp:652:14:652:27 | new[] | test.cpp:662:3:662:11 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@ + 1. | test.cpp:652:14:652:27 | new[] | new[] | test.cpp:653:19:653:22 | size | size |
| test.cpp:675:7:675:23 | ... = ... | test.cpp:667:14:667:31 | new[] | test.cpp:675:7:675:23 | ... = ... | This write might be out of bounds, as the pointer might be equal to $@ + $@. | test.cpp:667:14:667:31 | new[] | new[] | test.cpp:675:10:675:18 | ... ++ | ... ++ |

View File

@@ -17,7 +17,7 @@ void test2(int size) {
char* q = p + size - 1; // $ alloc=L16
char a = *q; // GOOD
char b = *(q - 1); // GOOD
char c = *(q + 1); // $ deref=L20 // BAD
char c = *(q + 1); // $ deref=L17->L20 // BAD
char d = *(q + size); // BAD [NOT DETECTED]
char e = *(q - size); // GOOD
char f = *(q + size + 1); // BAD [NOT DETECTED]
@@ -198,7 +198,7 @@ void test12(unsigned len, unsigned index) {
return;
}
p[index] = '\0'; // $ deref=L201 // BAD
p[index] = '\0'; // $ deref=L195->L201 deref=L197->L201 // BAD
}
void test13(unsigned len, unsigned index) {
@@ -210,7 +210,7 @@ void test13(unsigned len, unsigned index) {
return;
}
*q = '\0'; // $ deref=L213 // BAD
*q = '\0'; // $ deref=L206->L213 deref=L209->L213 // BAD
}
bool unknown();
@@ -261,7 +261,7 @@ void test17(unsigned len)
int *end = xs + len; // $ alloc=L260
for (int *x = xs; x <= end; x++)
{
int i = *x; // $ deref=L264 // BAD
int i = *x; // $ deref=L261->L264 deref=L262->L264 // BAD
}
}
@@ -271,7 +271,7 @@ void test18(unsigned len)
int *end = xs + len; // $ alloc=L270
for (int *x = xs; x <= end; x++)
{
*x = 0; // $ deref=L274 // BAD
*x = 0; // $ deref=L271->L274 deref=L272->L274 // BAD
}
}
@@ -355,8 +355,8 @@ void test25(unsigned size) {
char *xs = new char[size];
char *end = xs + size; // $ alloc=L355
char *end_plus_one = end + 1;
int val1 = *end_plus_one; // $ deref=L358+1 // BAD
int val2 = *(end_plus_one + 1); // $ deref=L359+2 // BAD
int val1 = *end_plus_one; // $ deref=L356->L358+1 deref=L357->L358+1 // BAD
int val2 = *(end_plus_one + 1); // $ deref=L356->L359+2 deref=L357->L359+2 // BAD
}
void test26(unsigned size) {
@@ -381,7 +381,7 @@ void test27(unsigned size, bool b) {
end++;
}
int val = *end; // $ deref=L384+1 // BAD
int val = *end; // $ deref=L378->L384+1 deref=L381->L384+1 // BAD
}
void test28(unsigned size) {
@@ -412,7 +412,7 @@ void test28_simple2(unsigned size) {
if (xs < end) {
xs++;
if (xs < end + 1) {
xs[0] = 0; // $ deref=L415 // BAD
xs[0] = 0; // $ deref=L411->L415 deref=L412->L415 deref=L414->L415 // BAD
}
}
}
@@ -423,7 +423,7 @@ void test28_simple3(unsigned size) {
if (xs < end) {
xs++;
if (xs - 1 < end) {
xs[0] = 0; // $ deref=L426 // BAD
xs[0] = 0; // $ deref=L422->L426 deref=L423->L426 deref=L425->L426 // BAD
}
}
}
@@ -435,7 +435,7 @@ void test28_simple4(unsigned size) {
end++;
xs++;
if (xs < end) {
xs[0] = 0; // $ deref=L438 // BAD
xs[0] = 0; // $ deref=L433->L438 deref=L434->L438 deref=L435->L438 // BAD
}
}
}
@@ -447,7 +447,7 @@ void test28_simple5(unsigned size) {
if (xs < end) {
xs++;
if (xs < end) {
xs[0] = 0; // $ deref=L450 // BAD
xs[0] = 0; // $ deref=L445->L450 deref=L446->L450 // BAD
}
}
}
@@ -483,7 +483,7 @@ void test28_simple8(unsigned size) {
if (xs < end) {
xs++;
if (xs < end - 1) {
xs[0] = 0; // $ deref=L486+498 // BAD
xs[0] = 0; // $ deref=L481->L486+498 deref=L482->L486+498 // BAD
}
}
}
@@ -659,7 +659,7 @@ void test32(unsigned size) {
xs++;
if (xs >= end)
return;
xs[0] = 0; // $ deref=L656->L662+1 deref=L657->L662+1 GOOD [FALSE POSITIVE]
xs[0] = 0; // $ GOOD
}
void test33(unsigned size, unsigned src_pos)
@@ -689,4 +689,15 @@ void test_missing_call_context_2(unsigned size) {
int* p = new int[size];
int* end_minus_one = pointer_arithmetic(p, size - 1);
*end_minus_one = '0'; // $ deref=L680->L690->L691 // GOOD
}
void test34(unsigned size) {
char *p = new char[size];
char *end = p + size + 1; // $ alloc=L695
if (p + 1 < end) {
p += 1;
}
if (p + 1 < end) {
int val = *p; // GOOD
}
}

View File

@@ -2157,3 +2157,46 @@ ssa.cpp:
# 431| v431_9(void) = ReturnValue : &:r431_8, m435_4
# 431| v431_10(void) = AliasedUse : m431_3
# 431| v431_11(void) = ExitFunction :
# 438| void Conditional(bool, int, int)
# 438| Block 0
# 438| v438_1(void) = EnterFunction :
# 438| m438_2(unknown) = AliasedDefinition :
# 438| m438_3(unknown) = InitializeNonLocal :
# 438| m438_4(unknown) = Chi : total:m438_2, partial:m438_3
# 438| r438_5(glval<bool>) = VariableAddress[a] :
# 438| m438_6(bool) = InitializeParameter[a] : &:r438_5
# 438| r438_7(glval<int>) = VariableAddress[x] :
# 438| m438_8(int) = InitializeParameter[x] : &:r438_7
# 438| r438_9(glval<int>) = VariableAddress[y] :
# 438| m438_10(int) = InitializeParameter[y] : &:r438_9
# 439| r439_1(glval<int>) = VariableAddress[z] :
# 439| r439_2(glval<bool>) = VariableAddress[a] :
# 439| r439_3(bool) = Load[a] : &:r439_2, m438_6
# 439| v439_4(void) = ConditionalBranch : r439_3
#-----| False -> Block 3
#-----| True -> Block 2
# 439| Block 1
# 439| m439_5(int) = Phi : from 2:m439_12, from 3:m439_16
# 439| r439_6(glval<int>) = VariableAddress[#temp439:13] :
# 439| r439_7(int) = Load[#temp439:13] : &:r439_6, m439_5
# 439| m439_8(int) = Store[z] : &:r439_1, r439_7
# 440| v440_1(void) = NoOp :
# 438| v438_11(void) = ReturnVoid :
# 438| v438_12(void) = AliasedUse : m438_3
# 438| v438_13(void) = ExitFunction :
# 439| Block 2
# 439| r439_9(glval<int>) = VariableAddress[x] :
# 439| r439_10(int) = Load[x] : &:r439_9, m438_8
# 439| r439_11(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_12(int) = Store[#temp439:13] : &:r439_11, r439_10
#-----| Goto -> Block 1
# 439| Block 3
# 439| r439_13(glval<int>) = VariableAddress[y] :
# 439| r439_14(int) = Load[y] : &:r439_13, m438_10
# 439| r439_15(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_16(int) = Store[#temp439:13] : &:r439_15, r439_14
#-----| Goto -> Block 1

View File

@@ -2146,3 +2146,46 @@ ssa.cpp:
# 431| v431_9(void) = ReturnValue : &:r431_8, m435_4
# 431| v431_10(void) = AliasedUse : m431_3
# 431| v431_11(void) = ExitFunction :
# 438| void Conditional(bool, int, int)
# 438| Block 0
# 438| v438_1(void) = EnterFunction :
# 438| m438_2(unknown) = AliasedDefinition :
# 438| m438_3(unknown) = InitializeNonLocal :
# 438| m438_4(unknown) = Chi : total:m438_2, partial:m438_3
# 438| r438_5(glval<bool>) = VariableAddress[a] :
# 438| m438_6(bool) = InitializeParameter[a] : &:r438_5
# 438| r438_7(glval<int>) = VariableAddress[x] :
# 438| m438_8(int) = InitializeParameter[x] : &:r438_7
# 438| r438_9(glval<int>) = VariableAddress[y] :
# 438| m438_10(int) = InitializeParameter[y] : &:r438_9
# 439| r439_1(glval<int>) = VariableAddress[z] :
# 439| r439_2(glval<bool>) = VariableAddress[a] :
# 439| r439_3(bool) = Load[a] : &:r439_2, m438_6
# 439| v439_4(void) = ConditionalBranch : r439_3
#-----| False -> Block 3
#-----| True -> Block 2
# 439| Block 1
# 439| m439_5(int) = Phi : from 2:m439_12, from 3:m439_16
# 439| r439_6(glval<int>) = VariableAddress[#temp439:13] :
# 439| r439_7(int) = Load[#temp439:13] : &:r439_6, m439_5
# 439| m439_8(int) = Store[z] : &:r439_1, r439_7
# 440| v440_1(void) = NoOp :
# 438| v438_11(void) = ReturnVoid :
# 438| v438_12(void) = AliasedUse : m438_3
# 438| v438_13(void) = ExitFunction :
# 439| Block 2
# 439| r439_9(glval<int>) = VariableAddress[x] :
# 439| r439_10(int) = Load[x] : &:r439_9, m438_8
# 439| r439_11(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_12(int) = Store[#temp439:13] : &:r439_11, r439_10
#-----| Goto -> Block 1
# 439| Block 3
# 439| r439_13(glval<int>) = VariableAddress[y] :
# 439| r439_14(int) = Load[y] : &:r439_13, m438_10
# 439| r439_15(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_16(int) = Store[#temp439:13] : &:r439_15, r439_14
#-----| Goto -> Block 1

View File

@@ -434,3 +434,7 @@ int noreturnTest2(int x) {
}
return x;
}
void Conditional(bool a, int x, int y) {
int z = a ? x : y;
}

View File

@@ -2002,3 +2002,45 @@ ssa.cpp:
# 431| v431_8(void) = ReturnValue : &:r431_7, m435_4
# 431| v431_9(void) = AliasedUse : ~m?
# 431| v431_10(void) = ExitFunction :
# 438| void Conditional(bool, int, int)
# 438| Block 0
# 438| v438_1(void) = EnterFunction :
# 438| mu438_2(unknown) = AliasedDefinition :
# 438| mu438_3(unknown) = InitializeNonLocal :
# 438| r438_4(glval<bool>) = VariableAddress[a] :
# 438| m438_5(bool) = InitializeParameter[a] : &:r438_4
# 438| r438_6(glval<int>) = VariableAddress[x] :
# 438| m438_7(int) = InitializeParameter[x] : &:r438_6
# 438| r438_8(glval<int>) = VariableAddress[y] :
# 438| m438_9(int) = InitializeParameter[y] : &:r438_8
# 439| r439_1(glval<int>) = VariableAddress[z] :
# 439| r439_2(glval<bool>) = VariableAddress[a] :
# 439| r439_3(bool) = Load[a] : &:r439_2, m438_5
# 439| v439_4(void) = ConditionalBranch : r439_3
#-----| False -> Block 3
#-----| True -> Block 2
# 439| Block 1
# 439| m439_5(int) = Phi : from 2:m439_12, from 3:m439_16
# 439| r439_6(glval<int>) = VariableAddress[#temp439:13] :
# 439| r439_7(int) = Load[#temp439:13] : &:r439_6, m439_5
# 439| m439_8(int) = Store[z] : &:r439_1, r439_7
# 440| v440_1(void) = NoOp :
# 438| v438_10(void) = ReturnVoid :
# 438| v438_11(void) = AliasedUse : ~m?
# 438| v438_12(void) = ExitFunction :
# 439| Block 2
# 439| r439_9(glval<int>) = VariableAddress[x] :
# 439| r439_10(int) = Load[x] : &:r439_9, m438_7
# 439| r439_11(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_12(int) = Store[#temp439:13] : &:r439_11, r439_10
#-----| Goto -> Block 1
# 439| Block 3
# 439| r439_13(glval<int>) = VariableAddress[y] :
# 439| r439_14(int) = Load[y] : &:r439_13, m438_9
# 439| r439_15(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_16(int) = Store[#temp439:13] : &:r439_15, r439_14
#-----| Goto -> Block 1

View File

@@ -2002,3 +2002,45 @@ ssa.cpp:
# 431| v431_8(void) = ReturnValue : &:r431_7, m435_4
# 431| v431_9(void) = AliasedUse : ~m?
# 431| v431_10(void) = ExitFunction :
# 438| void Conditional(bool, int, int)
# 438| Block 0
# 438| v438_1(void) = EnterFunction :
# 438| mu438_2(unknown) = AliasedDefinition :
# 438| mu438_3(unknown) = InitializeNonLocal :
# 438| r438_4(glval<bool>) = VariableAddress[a] :
# 438| m438_5(bool) = InitializeParameter[a] : &:r438_4
# 438| r438_6(glval<int>) = VariableAddress[x] :
# 438| m438_7(int) = InitializeParameter[x] : &:r438_6
# 438| r438_8(glval<int>) = VariableAddress[y] :
# 438| m438_9(int) = InitializeParameter[y] : &:r438_8
# 439| r439_1(glval<int>) = VariableAddress[z] :
# 439| r439_2(glval<bool>) = VariableAddress[a] :
# 439| r439_3(bool) = Load[a] : &:r439_2, m438_5
# 439| v439_4(void) = ConditionalBranch : r439_3
#-----| False -> Block 3
#-----| True -> Block 2
# 439| Block 1
# 439| m439_5(int) = Phi : from 2:m439_12, from 3:m439_16
# 439| r439_6(glval<int>) = VariableAddress[#temp439:13] :
# 439| r439_7(int) = Load[#temp439:13] : &:r439_6, m439_5
# 439| m439_8(int) = Store[z] : &:r439_1, r439_7
# 440| v440_1(void) = NoOp :
# 438| v438_10(void) = ReturnVoid :
# 438| v438_11(void) = AliasedUse : ~m?
# 438| v438_12(void) = ExitFunction :
# 439| Block 2
# 439| r439_9(glval<int>) = VariableAddress[x] :
# 439| r439_10(int) = Load[x] : &:r439_9, m438_7
# 439| r439_11(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_12(int) = Store[#temp439:13] : &:r439_11, r439_10
#-----| Goto -> Block 1
# 439| Block 3
# 439| r439_13(glval<int>) = VariableAddress[y] :
# 439| r439_14(int) = Load[y] : &:r439_13, m438_9
# 439| r439_15(glval<int>) = VariableAddress[#temp439:13] :
# 439| m439_16(int) = Store[#temp439:13] : &:r439_15, r439_14
#-----| Goto -> Block 1