@@ -30,15 +30,23 @@ Instruction getABoundIn(SemBound b, IRFunction func) {
30
30
/**
31
31
* Holds if `i <= b + delta`.
32
32
*/
33
- pragma [ nomagic ]
34
- predicate bounded ( Instruction i , Instruction b , int delta ) {
33
+ pragma [ inline ]
34
+ predicate boundedImpl ( Instruction i , Instruction b , int delta ) {
35
35
exists ( SemBound bound , IRFunction func |
36
36
semBounded ( getSemanticExpr ( i ) , bound , delta , true , _) and
37
37
b = getABoundIn ( bound , func ) and
38
38
i .getEnclosingIRFunction ( ) = func
39
39
)
40
40
}
41
41
42
+ bindingset [ i]
43
+ pragma [ inline_late]
44
+ predicate bounded1 ( Instruction i , Instruction b , int delta ) { boundedImpl ( i , b , delta ) }
45
+
46
+ bindingset [ b]
47
+ pragma [ inline_late]
48
+ predicate bounded2 ( Instruction i , Instruction b , int delta ) { boundedImpl ( i , b , delta ) }
49
+
42
50
/**
43
51
* Holds if the combination of `n` and `state` represents an appropriate
44
52
* source for the expression `e` suitable for use-use flow.
@@ -135,14 +143,6 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
135
143
override predicate isBarrierIn1 ( DataFlow:: Node node ) { this .isSourcePair ( node , _, _, _) }
136
144
}
137
145
138
- pragma [ nomagic]
139
- predicate pointerAddInstructionHasOperands (
140
- PointerAddInstruction pai , Instruction left , Instruction right
141
- ) {
142
- pai .getLeft ( ) = left and
143
- pai .getRight ( ) = right
144
- }
145
-
146
146
/**
147
147
* Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
148
148
* left operand of the pointer-arithmetic operation.
@@ -162,8 +162,9 @@ predicate pointerAddInstructionHasBounds(
162
162
PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
163
163
) {
164
164
exists ( Instruction right |
165
- pointerAddInstructionHasOperands ( pai , sink1 .asInstruction ( ) , right ) and
166
- bounded ( right , sink2 .asInstruction ( ) , delta )
165
+ pai .getRight ( ) = right and
166
+ pai .getLeft ( ) = sink1 .asInstruction ( ) and
167
+ bounded1 ( right , sink2 .asInstruction ( ) , delta )
167
168
)
168
169
}
169
170
@@ -184,9 +185,10 @@ predicate isSinkImpl(
184
185
* writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
185
186
* reads from an address that non-strictly upper-bounds `sink`.
186
187
*/
188
+ pragma [ inline]
187
189
predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation ) {
188
190
exists ( AddressOperand addr , int delta |
189
- bounded ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
191
+ bounded1 ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
190
192
delta >= 0 and
191
193
i .getAnOperand ( ) = addr
192
194
|
@@ -205,6 +207,7 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
205
207
module InvalidPointerToDerefConfig implements DataFlow:: ConfigSig {
206
208
predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, source , _) }
207
209
210
+ pragma [ inline]
208
211
predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
209
212
}
210
213
@@ -222,10 +225,10 @@ predicate invalidPointerToDerefSource(
222
225
PointerArithmeticInstruction pai , DataFlow:: Node source , int delta
223
226
) {
224
227
exists ( ProductFlow:: Configuration conf , DataFlow:: PathNode p , DataFlow:: Node sink1 |
225
- p .getNode ( ) = sink1 and
226
- conf .hasFlowPath ( _, _, p , _) and
228
+ pragma [ only_bind_out ] ( p .getNode ( ) ) = sink1 and
229
+ conf .hasFlowPath ( _, _, pragma [ only_bind_into ] ( p ) , _) and
227
230
isSinkImpl ( pai , sink1 , _, _) and
228
- bounded ( source .asInstruction ( ) , pai , delta ) and
231
+ bounded2 ( source .asInstruction ( ) , pai , delta ) and
229
232
delta >= 0
230
233
)
231
234
}
@@ -240,7 +243,7 @@ newtype TMergedPathNode =
240
243
// pointer, but we want to raise an alert at the dereference.
241
244
TPathNodeSink ( Instruction i ) {
242
245
exists ( DataFlow:: Node n |
243
- InvalidPointerToDerefFlow:: flow ( _ , n ) and
246
+ InvalidPointerToDerefFlow:: flowTo ( n ) and
244
247
isInvalidPointerDerefSink ( n , i , _)
245
248
)
246
249
}
@@ -334,6 +337,7 @@ predicate joinOn1(
334
337
* that dereferences `p1`. The string `operation` describes whether the `i` is
335
338
* a `StoreInstruction` or `LoadInstruction`.
336
339
*/
340
+ pragma [ inline]
337
341
predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation ) {
338
342
isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
339
343
}
0 commit comments