C++: Simplify 'InvalidPointerToDereference.qll' now that the difference between 'derefSource' and 'pai' is always 0.

This commit is contained in:
Mathias Vorreiter Pedersen
2023-10-30 15:53:48 +00:00
parent c8edf3151b
commit 1e699ec0e5

View File

@@ -96,7 +96,7 @@ int invalidPointerToDereferenceFieldFlowBranchLimit() { result = 0 }
private module InvalidPointerToDerefBarrier { private module InvalidPointerToDerefBarrier {
private module BarrierConfig implements DataFlow::ConfigSig { private module BarrierConfig implements DataFlow::ConfigSig {
additional predicate isSource(DataFlow::Node source, PointerArithmeticInstruction pai) { additional predicate isSource(DataFlow::Node source, PointerArithmeticInstruction pai) {
invalidPointerToDerefSource(_, pai, _, _) and invalidPointerToDerefSource(_, pai, _) and
// source <= pai // source <= pai
bounded2(source.asInstruction(), pai, any(int d | d <= 0)) bounded2(source.asInstruction(), pai, any(int d | d <= 0))
} }
@@ -169,11 +169,11 @@ private module InvalidPointerToDerefBarrier {
*/ */
private module InvalidPointerToDerefConfig implements DataFlow::StateConfigSig { private module InvalidPointerToDerefConfig implements DataFlow::StateConfigSig {
class FlowState extends PointerArithmeticInstruction { class FlowState extends PointerArithmeticInstruction {
FlowState() { invalidPointerToDerefSource(_, this, _, _) } FlowState() { invalidPointerToDerefSource(_, this, _) }
} }
predicate isSource(DataFlow::Node source, FlowState pai) { predicate isSource(DataFlow::Node source, FlowState pai) {
invalidPointerToDerefSource(_, pai, source, _) invalidPointerToDerefSource(_, pai, source)
} }
pragma[inline] pragma[inline]
@@ -201,16 +201,14 @@ private import DataFlow::GlobalWithState<InvalidPointerToDerefConfig>
* left-hand side of the pointer-arithmetic instruction represented by `derefSource`. * left-hand side of the pointer-arithmetic instruction represented by `derefSource`.
*/ */
private predicate invalidPointerToDerefSource( private predicate invalidPointerToDerefSource(
DataFlow::Node allocSource, PointerArithmeticInstruction pai, DataFlow::Node derefSource, DataFlow::Node allocSource, PointerArithmeticInstruction pai, DataFlow::Node derefSource
int deltaDerefSourceAndPai
) { ) {
// Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`: // Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
// `rhsSizeDelta` is the constant offset added to the size of the allocation, and // `rhsSizeDelta` is the constant offset added to the size of the allocation, and
// `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction // `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
// and the instruction computing the address for which we will search for a dereference. // and the instruction computing the address for which we will search for a dereference.
AllocToInvalidPointer::pointerAddInstructionHasBounds(allocSource, pai, _, _) and AllocToInvalidPointer::pointerAddInstructionHasBounds(allocSource, pai, _, _) and
derefSource.asInstruction() = pai and derefSource.asInstruction() = pai
deltaDerefSourceAndPai = 0
} }
/** /**
@@ -253,11 +251,9 @@ private Instruction getASuccessor(Instruction instr) {
instr.getBlock().getASuccessor+() = result.getBlock() instr.getBlock().getASuccessor+() = result.getBlock()
} }
private predicate paiForDereferenceSink( private predicate paiForDereferenceSink(PointerArithmeticInstruction pai, DataFlow::Node derefSink) {
PointerArithmeticInstruction pai, DataFlow::Node derefSink, int deltaDerefSourceAndPai
) {
exists(DataFlow::Node derefSource | exists(DataFlow::Node derefSource |
invalidPointerToDerefSource(_, pai, derefSource, deltaDerefSourceAndPai) and invalidPointerToDerefSource(_, pai, derefSource) and
flow(derefSource, derefSink) flow(derefSource, derefSink)
) )
} }
@@ -269,10 +265,10 @@ private predicate paiForDereferenceSink(
*/ */
private predicate derefSinkToOperation( private predicate derefSinkToOperation(
DataFlow::Node derefSink, PointerArithmeticInstruction pai, DataFlow::Node operation, DataFlow::Node derefSink, PointerArithmeticInstruction pai, DataFlow::Node operation,
string description, int deltaDerefSourceAndPai, int deltaDerefSinkAndDerefAddress string description, int deltaDerefSinkAndDerefAddress
) { ) {
exists(Instruction operationInstr, AddressOperand addr | exists(Instruction operationInstr, AddressOperand addr |
paiForDereferenceSink(pai, pragma[only_bind_into](derefSink), deltaDerefSourceAndPai) and paiForDereferenceSink(pai, pragma[only_bind_into](derefSink)) and
isInvalidPointerDerefSink(derefSink, addr, operationInstr, description, isInvalidPointerDerefSink(derefSink, addr, operationInstr, description,
deltaDerefSinkAndDerefAddress) and deltaDerefSinkAndDerefAddress) and
operationInstr = getASuccessor(derefSink.asInstruction()) and operationInstr = getASuccessor(derefSink.asInstruction()) and
@@ -293,11 +289,7 @@ predicate operationIsOffBy(
DataFlow::Node allocation, PointerArithmeticInstruction pai, DataFlow::Node derefSource, DataFlow::Node allocation, PointerArithmeticInstruction pai, DataFlow::Node derefSource,
DataFlow::Node derefSink, string description, DataFlow::Node operation, int delta DataFlow::Node derefSink, string description, DataFlow::Node operation, int delta
) { ) {
exists(int deltaDerefSourceAndPai, int deltaDerefSinkAndDerefAddress | invalidPointerToDerefSource(allocation, pai, derefSource) and
invalidPointerToDerefSource(allocation, pai, derefSource, deltaDerefSourceAndPai) and flow(derefSource, derefSink) and
flow(derefSource, derefSink) and derefSinkToOperation(derefSink, pai, operation, description, delta)
derefSinkToOperation(derefSink, pai, operation, description, deltaDerefSourceAndPai,
deltaDerefSinkAndDerefAddress) and
delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
)
} }