2323 * configuration (see `InvalidPointerToDerefConfig`).
2424 *
2525 * The dataflow traversal defines the set of sources as any dataflow node `n` such that there exists a pointer-arithmetic
26- * instruction `pai` found by `AllocationToInvalidPointer.qll` and a `n.asInstruction() >= pai + deltaDerefSourceAndPai`.
27- * Here, `deltaDerefSourceAndPai` is the constant difference between the source we track for finding a dereference and the
28- * pointer-arithmetic instruction.
26+ * instruction `pai` found by `AllocationToInvalidPointer.qll` and a `n.asInstruction() = pai`.
2927 *
3028 * The set of sinks is defined as any dataflow node `n` such that `addr <= n.asInstruction() + deltaDerefSinkAndDerefAddress`
3129 * for some address operand `addr` and constant difference `deltaDerefSinkAndDerefAddress`. Since an address operand is
3735 * `deltaDerefSinkAndDerefAddress >= 0`. The load attached to `*p` is the "operation". To ensure that the path makes
3836 * intuitive sense, we only pick operations that are control-flow reachable from the dereference sink.
3937 *
40- * To compute how many elements the dereference is beyond the end position of the allocation, we sum the two deltas
41- * `deltaDerefSourceAndPai` and `deltaDerefSinkAndDerefAddress`. This is done in the `operationIsOffBy` predicate
42- * (which is the only predicate exposed by this file).
38+ * We use the `deltaDerefSinkAndDerefAddress` to compute how many elements the dereference is beyond the end position of
39+ * the allocation. This is done in the `operationIsOffBy` predicate (which is the only predicate exposed by this file).
4340 *
4441 * Handling false positives:
4542 *
@@ -96,7 +93,7 @@ int invalidPointerToDereferenceFieldFlowBranchLimit() { result = 0 }
9693private module InvalidPointerToDerefBarrier {
9794 private module BarrierConfig implements DataFlow:: ConfigSig {
9895 additional predicate isSource ( DataFlow:: Node source , PointerArithmeticInstruction pai ) {
99- invalidPointerToDerefSource ( _, pai , _, _ ) and
96+ invalidPointerToDerefSource ( _, pai , _) and
10097 // source <= pai
10198 bounded2 ( source .asInstruction ( ) , pai , any ( int d | d <= 0 ) )
10299 }
@@ -169,11 +166,11 @@ private module InvalidPointerToDerefBarrier {
169166 */
170167private module InvalidPointerToDerefConfig implements DataFlow:: StateConfigSig {
171168 class FlowState extends PointerArithmeticInstruction {
172- FlowState ( ) { invalidPointerToDerefSource ( _, this , _, _ ) }
169+ FlowState ( ) { invalidPointerToDerefSource ( _, this , _) }
173170 }
174171
175172 predicate isSource ( DataFlow:: Node source , FlowState pai ) {
176- invalidPointerToDerefSource ( _, pai , source , _ )
173+ invalidPointerToDerefSource ( _, pai , source )
177174 }
178175
179176 pragma [ inline]
@@ -198,24 +195,17 @@ private import DataFlow::GlobalWithState<InvalidPointerToDerefConfig>
198195
199196/**
200197 * Holds if `allocSource` is dataflow node that represents an allocation that flows to the
201- * left-hand side of the pointer-arithmetic `pai`, and `derefSource <= pai + derefSourcePaiDelta`.
202- *
203- * For example, if `pai` is a pointer-arithmetic operation `p + size` in an expression such
204- * as `(p + size) + 1` and `derefSource` is the node representing `(p + size) + 1`. In this
205- * case `derefSourcePaiDelta` is 1.
198+ * left-hand side of the pointer-arithmetic instruction represented by `derefSource`.
206199 */
207200private predicate invalidPointerToDerefSource (
208- DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
209- int deltaDerefSourceAndPai
201+ DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource
210202) {
211203 // Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
212204 // `rhsSizeDelta` is the constant offset added to the size of the allocation, and
213205 // `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
214206 // and the instruction computing the address for which we will search for a dereference.
215207 AllocToInvalidPointer:: pointerAddInstructionHasBounds ( allocSource , pai , _, _) and
216- // derefSource <= pai + deltaDerefSourceAndPai
217- bounded2 ( derefSource .asInstruction ( ) , pai , deltaDerefSourceAndPai ) and
218- deltaDerefSourceAndPai >= 0
208+ derefSource .asInstruction ( ) = pai
219209}
220210
221211/**
@@ -258,11 +248,9 @@ private Instruction getASuccessor(Instruction instr) {
258248 instr .getBlock ( ) .getASuccessor + ( ) = result .getBlock ( )
259249}
260250
261- private predicate paiForDereferenceSink (
262- PointerArithmeticInstruction pai , DataFlow:: Node derefSink , int deltaDerefSourceAndPai
263- ) {
251+ private predicate paiForDereferenceSink ( PointerArithmeticInstruction pai , DataFlow:: Node derefSink ) {
264252 exists ( DataFlow:: Node derefSource |
265- invalidPointerToDerefSource ( _, pai , derefSource , deltaDerefSourceAndPai ) and
253+ invalidPointerToDerefSource ( _, pai , derefSource ) and
266254 flow ( derefSource , derefSink )
267255 )
268256}
@@ -274,10 +262,10 @@ private predicate paiForDereferenceSink(
274262 */
275263private predicate derefSinkToOperation (
276264 DataFlow:: Node derefSink , PointerArithmeticInstruction pai , DataFlow:: Node operation ,
277- string description , int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress
265+ string description , int deltaDerefSinkAndDerefAddress
278266) {
279267 exists ( Instruction operationInstr , AddressOperand addr |
280- paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) , deltaDerefSourceAndPai ) and
268+ paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) ) and
281269 isInvalidPointerDerefSink ( derefSink , addr , operationInstr , description ,
282270 deltaDerefSinkAndDerefAddress ) and
283271 operationInstr = getASuccessor ( derefSink .asInstruction ( ) ) and
@@ -298,11 +286,7 @@ predicate operationIsOffBy(
298286 DataFlow:: Node allocation , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
299287 DataFlow:: Node derefSink , string description , DataFlow:: Node operation , int delta
300288) {
301- exists ( int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress |
302- invalidPointerToDerefSource ( allocation , pai , derefSource , deltaDerefSourceAndPai ) and
303- flow ( derefSource , derefSink ) and
304- derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSourceAndPai ,
305- deltaDerefSinkAndDerefAddress ) and
306- delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
307- )
289+ invalidPointerToDerefSource ( allocation , pai , derefSource ) and
290+ flow ( derefSource , derefSink ) and
291+ derefSinkToOperation ( derefSink , pai , operation , description , delta )
308292}
0 commit comments