66
66
* module. Since the node we are tracking is not necessarily _equal_ to the pointer-arithmetic instruction, but rather satisfies
67
67
* `node.asInstruction() <= pai + deltaDerefSourceAndPai`, we need to account for the delta when checking if a guard is sufficiently
68
68
* 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
+ * ```
74
77
*/
75
78
76
79
private import cpp
@@ -82,76 +85,102 @@ private import RangeAnalysisUtil
82
85
83
86
private module InvalidPointerToDerefBarrier {
84
87
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 ) )
88
92
}
89
93
94
+ predicate isSource ( DataFlow:: Node source ) { isSource ( source , _) }
95
+
90
96
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
92
98
) {
93
99
// 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 )
95
101
}
96
102
97
103
predicate isSink ( DataFlow:: Node sink ) { isSink ( _, sink , _, _, _) }
98
104
}
99
105
100
106
private module BarrierFlow = DataFlow:: Global< BarrierConfig > ;
101
107
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
+ */
109
114
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
111
116
) {
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 )
118
122
)
119
123
}
120
124
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 |
123
130
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
128
139
)
129
140
}
130
141
131
- DataFlow:: Node getABarrierNode ( ) { result .asOperand ( ) = getABarrierInstruction ( _) .getAUse ( ) }
142
+ DataFlow:: Node getABarrierNode ( PointerArithmeticInstruction pai ) {
143
+ result .asOperand ( ) = getABarrierInstruction ( pai ) .getAUse ( )
144
+ }
132
145
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
+ }
135
152
}
136
153
137
154
/**
138
155
* A configuration to track flow from a pointer-arithmetic operation found
139
156
* by `AllocToInvalidPointerConfig` to a dereference of the pointer.
140
157
*/
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
+ }
143
166
144
167
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 ( ) }
146
171
147
172
predicate isBarrier ( DataFlow:: Node node ) {
148
173
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 )
151
180
}
152
181
}
153
182
154
- private import DataFlow:: Global < InvalidPointerToDerefConfig >
183
+ private import DataFlow:: GlobalWithState < InvalidPointerToDerefConfig >
155
184
156
185
/**
157
186
* Holds if `allocSource` is dataflow node that represents an allocation that flows to the
@@ -165,19 +194,14 @@ private predicate invalidPointerToDerefSource(
165
194
DataFlow:: Node allocSource , PointerArithmeticInstruction pai , DataFlow:: Node derefSource ,
166
195
int deltaDerefSourceAndPai
167
196
) {
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
181
205
}
182
206
183
207
/**
@@ -187,15 +211,14 @@ private predicate invalidPointerToDerefSource(
187
211
*/
188
212
pragma [ inline]
189
213
private 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
191
216
) {
192
- exists ( AddressOperand addr , Instruction s , IRBlock b |
217
+ exists ( Instruction s |
193
218
s = sink .asInstruction ( ) and
194
219
bounded ( addr .getDef ( ) , s , deltaDerefSinkAndDerefAddress ) and
195
220
deltaDerefSinkAndDerefAddress >= 0 and
196
- i .getAnOperand ( ) = addr and
197
- b = i .getBlock ( ) and
198
- not b = InvalidPointerToDerefBarrier:: getABarrierBlock ( deltaDerefSinkAndDerefAddress )
221
+ i .getAnOperand ( ) = addr
199
222
|
200
223
i instanceof StoreInstruction and
201
224
operation = "write"
@@ -221,9 +244,11 @@ private Instruction getASuccessor(Instruction instr) {
221
244
instr .getBlock ( ) .getASuccessor + ( ) = result .getBlock ( )
222
245
}
223
246
224
- private predicate paiForDereferenceSink ( PointerArithmeticInstruction pai , DataFlow:: Node derefSink ) {
247
+ private predicate paiForDereferenceSink (
248
+ PointerArithmeticInstruction pai , DataFlow:: Node derefSink , int deltaDerefSourceAndPai
249
+ ) {
225
250
exists ( DataFlow:: Node derefSource |
226
- invalidPointerToDerefSource ( _, pai , derefSource , _ ) and
251
+ invalidPointerToDerefSource ( _, pai , derefSource , deltaDerefSourceAndPai ) and
227
252
flow ( derefSource , derefSink )
228
253
)
229
254
}
@@ -235,13 +260,15 @@ private predicate paiForDereferenceSink(PointerArithmeticInstruction pai, DataFl
235
260
*/
236
261
private predicate derefSinkToOperation (
237
262
DataFlow:: Node derefSink , PointerArithmeticInstruction pai , DataFlow:: Node operation ,
238
- string description , int deltaDerefSinkAndDerefAddress
263
+ string description , int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress
239
264
) {
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
243
269
operationInstr = getASuccessor ( derefSink .asInstruction ( ) ) and
244
- operation .asInstruction ( ) = operationInstr
270
+ operation .asInstruction ( ) = operationInstr and
271
+ not addr = InvalidPointerToDerefBarrier:: getABarrierAddressOperand ( pai )
245
272
)
246
273
}
247
274
@@ -260,7 +287,8 @@ predicate operationIsOffBy(
260
287
exists ( int deltaDerefSourceAndPai , int deltaDerefSinkAndDerefAddress |
261
288
invalidPointerToDerefSource ( allocation , pai , derefSource , deltaDerefSourceAndPai ) and
262
289
flow ( derefSource , derefSink ) and
263
- derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSinkAndDerefAddress ) and
290
+ derefSinkToOperation ( derefSink , pai , operation , description , deltaDerefSourceAndPai ,
291
+ deltaDerefSinkAndDerefAddress ) and
264
292
delta = deltaDerefSourceAndPai + deltaDerefSinkAndDerefAddress
265
293
)
266
294
}
0 commit comments