6666 * module. Since the node we are tracking is not necessarily _equal_ to the pointer-arithmetic instruction, but rather satisfies
6767 * `node.asInstruction() <= pai + deltaDerefSourceAndPai`, we need to account for the delta when checking if a guard is sufficiently
6868 * strong to infer that a future dereference is safe. To do this, we check that the guard guarantees that a node `n` satisfies
69- * `n < node + k` where `node` is a node we know is equal to the value of the dereference source (i.e., it satisfies
70- * `node.asInstruction() <= pai + deltaDerefSourceAndPai`) and `k <= deltaDerefSourceAndPai`. Combining this we have
71- * `n < node + k <= node + deltaDerefSourceAndPai <= pai + 2*deltaDerefSourceAndPai` (TODO: Oops. This math doesn't quite work out.
72- * I think this is because we need to redefine the `BarrierConfig` to start flow at the pointer-arithmetic instruction instead of
73- * at the dereference source. When combined with TODO above it's easy to show that this guard ensures that the dereference is safe).
69+ * `n < node + k` where `node` is a node such that `node <= pai`. Thus, we know that any node `m` such that `m <= n + delta` where
70+ * `delta + k <= 0` will be safe because:
71+ * ```
72+ * m <= n + delta
73+ * < node + k + delta
74+ * <= pai + k + delta
75+ * <= pai
76+ * ```
7477 */
7578
7679private import cpp
@@ -82,76 +85,102 @@ private import RangeAnalysisUtil
8285
8386private module InvalidPointerToDerefBarrier {
8487 private module BarrierConfig implements DataFlow:: ConfigSig {
85- predicate isSource ( DataFlow:: Node source ) {
86- // The sources is the same as in the sources for `InvalidPointerToDerefConfig`.
87- invalidPointerToDerefSource ( _, _, source , _)
88+ additional predicate isSource ( DataFlow:: Node source , PointerArithmeticInstruction pai ) {
89+ invalidPointerToDerefSource ( _, pai , _, _) and
90+ // source <= pai
91+ bounded2 ( source .asInstruction ( ) , pai , any ( int d | d <= 0 ) )
8892 }
8993
94+ predicate isSource ( DataFlow:: Node source ) { isSource ( source , _) }
95+
9096 additional predicate isSink (
91- DataFlow:: Node left , DataFlow:: Node right , IRGuardCondition g , int k , boolean testIsTrue
97+ DataFlow:: Node small , DataFlow:: Node large , IRGuardCondition g , int k , boolean testIsTrue
9298 ) {
9399 // The sink is any "large" side of a relational comparison.
94- g .comparesLt ( left .asOperand ( ) , right .asOperand ( ) , k , true , testIsTrue )
100+ g .comparesLt ( small .asOperand ( ) , large .asOperand ( ) , k , true , testIsTrue )
95101 }
96102
97103 predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
98104 }
99105
100106 private module BarrierFlow = DataFlow:: Global< BarrierConfig > ;
101107
102- private int getInvalidPointerToDerefSourceDelta ( DataFlow:: Node node ) {
103- exists ( DataFlow:: Node source |
104- BarrierFlow:: flow ( source , node ) and
105- invalidPointerToDerefSource ( _, _, source , result )
106- )
107- }
108-
108+ /**
109+ * Holds if `g` ensures that `small < large + k` if `g` evaluates to `edge`.
110+ *
111+ * Additionally, it also holds that `large <= pai`. Thus, when `g` evaluates to `edge`
112+ * it holds that `small < pai + k`.
113+ */
109114 private predicate operandGuardChecks (
110- IRGuardCondition g , Operand left , Operand right , int state , boolean edge
115+ PointerArithmeticInstruction pai , IRGuardCondition g , Operand small , int k , boolean edge
111116 ) {
112- exists ( DataFlow:: Node nLeft , DataFlow:: Node nRight , int k |
113- nRight .asOperand ( ) = right and
114- nLeft .asOperand ( ) = left and
115- BarrierConfig:: isSink ( nLeft , nRight , g , k , edge ) and
116- state = getInvalidPointerToDerefSourceDelta ( nRight ) and
117- k <= state
117+ exists ( DataFlow:: Node source , DataFlow:: Node nSmall , DataFlow:: Node nLarge |
118+ nSmall .asOperand ( ) = small and
119+ BarrierConfig:: isSource ( source , pai ) and
120+ BarrierFlow:: flow ( source , nLarge ) and
121+ BarrierConfig:: isSink ( nSmall , nLarge , g , k , edge )
118122 )
119123 }
120124
121- Instruction getABarrierInstruction ( int state ) {
122- exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge |
125+ /**
126+ * Gets an instruction `instr` such that `instr < pai`.
127+ */
128+ Instruction getABarrierInstruction ( PointerArithmeticInstruction pai ) {
129+ exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge , int delta , int k |
123130 use = value .getAUse ( ) and
124- operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) , _, state ,
125- pragma [ only_bind_into ] ( edge ) ) and
126- result = value .getAnInstruction ( ) and
127- g .controls ( result .getBlock ( ) , edge )
131+ // value < pai + k
132+ operandGuardChecks ( pai , pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) ,
133+ pragma [ only_bind_into ] ( k ) , pragma [ only_bind_into ] ( edge ) ) and
134+ // result <= value + delta
135+ bounded ( result , value .getAnInstruction ( ) , delta ) and
136+ g .controls ( result .getBlock ( ) , edge ) and
137+ delta + k <= 0
138+ // combining the above we have: result < pai + k + delta <= pai
128139 )
129140 }
130141
131- DataFlow:: Node getABarrierNode ( ) { result .asOperand ( ) = getABarrierInstruction ( _) .getAUse ( ) }
142+ DataFlow:: Node getABarrierNode ( PointerArithmeticInstruction pai ) {
143+ result .asOperand ( ) = getABarrierInstruction ( pai ) .getAUse ( )
144+ }
132145
133- pragma [ nomagic]
134- IRBlock getABarrierBlock ( int state ) { result .getAnInstruction ( ) = getABarrierInstruction ( state ) }
146+ /**
147+ * Gets an address operand whose definition `instr` satisfies `instr < pai`.
148+ */
149+ AddressOperand getABarrierAddressOperand ( PointerArithmeticInstruction pai ) {
150+ result .getDef ( ) = getABarrierInstruction ( pai )
151+ }
135152}
136153
137154/**
138155 * A configuration to track flow from a pointer-arithmetic operation found
139156 * by `AllocToInvalidPointerConfig` to a dereference of the pointer.
140157 */
141- private module InvalidPointerToDerefConfig implements DataFlow:: ConfigSig {
142- predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, _, source , _) }
158+ private module InvalidPointerToDerefConfig implements DataFlow:: StateConfigSig {
159+ class FlowState extends PointerArithmeticInstruction {
160+ FlowState ( ) { invalidPointerToDerefSource ( _, this , _, _) }
161+ }
162+
163+ predicate isSource ( DataFlow:: Node source , FlowState pai ) {
164+ invalidPointerToDerefSource ( _, pai , source , _)
165+ }
143166
144167 pragma [ inline]
145- predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _, _) }
168+ predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _, _, _) }
169+
170+ predicate isSink ( DataFlow:: Node sink , FlowState pai ) { none ( ) }
146171
147172 predicate isBarrier ( DataFlow:: Node node ) {
148173 node = any ( DataFlow:: SsaPhiNode phi | not phi .isPhiRead ( ) ) .getAnInput ( true )
149- or
150- node = InvalidPointerToDerefBarrier:: getABarrierNode ( )
174+ }
175+
176+ predicate isBarrier ( DataFlow:: Node node , FlowState pai ) {
177+ // `node = getABarrierNode(pai)` ensures that node < pai, so this node is safe to dereference.
178+ // Note that this is the only place where the `FlowState` is used in this configuration.
179+ node = InvalidPointerToDerefBarrier:: getABarrierNode ( pai )
151180 }
152181}
153182
154- private import DataFlow:: Global < InvalidPointerToDerefConfig >
183+ private import DataFlow:: GlobalWithState < InvalidPointerToDerefConfig >
155184
156185/**
157186 * Holds if `allocSource` is dataflow node that represents an allocation that flows to the
@@ -165,19 +194,14 @@ private predicate invalidPointerToDerefSource(
165194 DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
166195 int deltaDerefSourceAndPai
167196) {
168- exists ( int rhsSizeDelta |
169- // Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
170- // `rhsSizeDelta` is the constant offset added to the size of the allocation, and
171- // `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
172- // and the instruction computing the address for which we will search for a dereference.
173- AllocToInvalidPointer:: pointerAddInstructionHasBounds ( allocSource , pai , _, rhsSizeDelta ) and
174- bounded2 ( derefSource .asInstruction ( ) , pai , deltaDerefSourceAndPai ) and
175- deltaDerefSourceAndPai >= 0 and
176- // TODO: This condition will go away once #13725 is merged, and then we can make `SizeBarrier`
177- // private to `AllocationToInvalidPointer.qll`.
178- not derefSource .getBasicBlock ( ) =
179- AllocToInvalidPointer:: SizeBarrier:: getABarrierBlock ( rhsSizeDelta )
180- )
197+ // Note that `deltaDerefSourceAndPai` is not necessarily equal to `rhsSizeDelta`:
198+ // `rhsSizeDelta` is the constant offset added to the size of the allocation, and
199+ // `deltaDerefSourceAndPai` is the constant difference between the pointer-arithmetic instruction
200+ // and the instruction computing the address for which we will search for a dereference.
201+ AllocToInvalidPointer:: pointerAddInstructionHasBounds ( allocSource , pai , _, _) and
202+ // derefSource <= pai + deltaDerefSourceAndPai
203+ bounded2 ( derefSource .asInstruction ( ) , pai , deltaDerefSourceAndPai ) and
204+ deltaDerefSourceAndPai >= 0
181205}
182206
183207/**
@@ -187,15 +211,14 @@ private predicate invalidPointerToDerefSource(
187211 */
188212pragma [ inline]
189213private predicate isInvalidPointerDerefSink (
190- DataFlow:: Node sink , Instruction i , string operation , int deltaDerefSinkAndDerefAddress
214+ DataFlow:: Node sink , AddressOperand addr , Instruction i , string operation ,
215+ int deltaDerefSinkAndDerefAddress
191216) {
192- exists ( AddressOperand addr , Instruction s , IRBlock b |
217+ exists ( Instruction s |
193218 s = sink .asInstruction ( ) and
194219 bounded ( addr .getDef ( ) , s , deltaDerefSinkAndDerefAddress ) and
195220 deltaDerefSinkAndDerefAddress >= 0 and
196- i .getAnOperand ( ) = addr and
197- b = i .getBlock ( ) and
198- not b = InvalidPointerToDerefBarrier:: getABarrierBlock ( deltaDerefSinkAndDerefAddress )
221+ i .getAnOperand ( ) = addr
199222 |
200223 i instanceof StoreInstruction and
201224 operation = "write"
@@ -221,9 +244,11 @@ private Instruction getASuccessor(Instruction instr) {
221244 instr .getBlock ( ) .getASuccessor + ( ) = result .getBlock ( )
222245}
223246
224- private predicate paiForDereferenceSink ( PointerArithmeticInstruction pai , DataFlow:: Node derefSink ) {
247+ private predicate paiForDereferenceSink (
248+ PointerArithmeticInstruction pai , DataFlow:: Node derefSink , int deltaDerefSourceAndPai
249+ ) {
225250 exists ( DataFlow:: Node derefSource |
226- invalidPointerToDerefSource ( _, pai , derefSource , _ ) and
251+ invalidPointerToDerefSource ( _, pai , derefSource , deltaDerefSourceAndPai ) and
227252 flow ( derefSource , derefSink )
228253 )
229254}
@@ -235,13 +260,15 @@ private predicate paiForDereferenceSink(PointerArithmeticInstruction pai, DataFl
235260 */
236261private predicate derefSinkToOperation (
237262 DataFlow:: Node derefSink , PointerArithmeticInstruction pai , DataFlow:: Node operation ,
238- string description , int deltaDerefSinkAndDerefAddress
263+ string description , int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress
239264) {
240- exists ( Instruction operationInstr |
241- paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) ) and
242- isInvalidPointerDerefSink ( derefSink , operationInstr , description , deltaDerefSinkAndDerefAddress ) and
265+ exists ( Instruction operationInstr , AddressOperand addr |
266+ paiForDereferenceSink ( pai , pragma [ only_bind_into ] ( derefSink ) , deltaDerefSourceAndPai ) and
267+ isInvalidPointerDerefSink ( derefSink , addr , operationInstr , description ,
268+ deltaDerefSinkAndDerefAddress ) and
243269 operationInstr = getASuccessor ( derefSink .asInstruction ( ) ) and
244- operation .asInstruction ( ) = operationInstr
270+ operation .asInstruction ( ) = operationInstr and
271+ not addr = InvalidPointerToDerefBarrier:: getABarrierAddressOperand ( pai )
245272 )
246273}
247274
@@ -260,7 +287,8 @@ predicate operationIsOffBy(
260287 exists ( int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress |
261288 invalidPointerToDerefSource ( allocation , pai , derefSource , deltaDerefSourceAndPai ) and
262289 flow ( derefSource , derefSink ) and
263- derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSinkAndDerefAddress ) and
290+ derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSourceAndPai ,
291+ deltaDerefSinkAndDerefAddress ) and
264292 delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
265293 )
266294}
0 commit comments