@@ -30,15 +30,23 @@ Instruction getABoundIn(SemBound b, IRFunction func) {
3030/**
3131 * Holds if `i <= b + delta`.
3232 */
33- pragma [ nomagic ]
34- predicate bounded ( Instruction i , Instruction b , int delta ) {
33+ pragma [ inline ]
34+ predicate boundedImpl ( Instruction i , Instruction b , int delta ) {
3535 exists ( SemBound bound , IRFunction func |
3636 semBounded ( getSemanticExpr ( i ) , bound , delta , true , _) and
3737 b = getABoundIn ( bound , func ) and
3838 i .getEnclosingIRFunction ( ) = func
3939 )
4040}
4141
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+
4250/**
4351 * Holds if the combination of `n` and `state` represents an appropriate
4452 * source for the expression `e` suitable for use-use flow.
@@ -135,14 +143,6 @@ class AllocToInvalidPointerConf extends ProductFlow::Configuration {
135143 override predicate isBarrierIn1 ( DataFlow:: Node node ) { this .isSourcePair ( node , _, _, _) }
136144}
137145
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-
146146/**
147147 * Holds if `pai` is non-strictly upper bounded by `sink2 + delta` and `sink1` is the
148148 * left operand of the pointer-arithmetic operation.
@@ -162,8 +162,9 @@ predicate pointerAddInstructionHasBounds(
162162 PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
163163) {
164164 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 )
167168 )
168169}
169170
@@ -184,9 +185,10 @@ predicate isSinkImpl(
184185 * writes to an address that non-strictly upper-bounds `sink`, or `i` is a `LoadInstruction` that
185186 * reads from an address that non-strictly upper-bounds `sink`.
186187 */
188+ pragma [ inline]
187189predicate isInvalidPointerDerefSink ( DataFlow:: Node sink , Instruction i , string operation ) {
188190 exists ( AddressOperand addr , int delta |
189- bounded ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
191+ bounded1 ( addr .getDef ( ) , sink .asInstruction ( ) , delta ) and
190192 delta >= 0 and
191193 i .getAnOperand ( ) = addr
192194 |
@@ -205,6 +207,7 @@ predicate isInvalidPointerDerefSink(DataFlow::Node sink, Instruction i, string o
205207module InvalidPointerToDerefConfig implements DataFlow:: ConfigSig {
206208 predicate isSource ( DataFlow:: Node source ) { invalidPointerToDerefSource ( _, source , _) }
207209
210+ pragma [ inline]
208211 predicate isSink ( DataFlow:: Node sink ) { isInvalidPointerDerefSink ( sink , _, _) }
209212}
210213
@@ -222,10 +225,10 @@ predicate invalidPointerToDerefSource(
222225 PointerArithmeticInstruction pai , DataFlow:: Node source , int delta
223226) {
224227 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
227230 isSinkImpl ( pai , sink1 , _, _) and
228- bounded ( source .asInstruction ( ) , pai , delta ) and
231+ bounded2 ( source .asInstruction ( ) , pai , delta ) and
229232 delta >= 0
230233 )
231234}
@@ -240,7 +243,7 @@ newtype TMergedPathNode =
240243 // pointer, but we want to raise an alert at the dereference.
241244 TPathNodeSink ( Instruction i ) {
242245 exists ( DataFlow:: Node n |
243- InvalidPointerToDerefFlow:: flow ( _ , n ) and
246+ InvalidPointerToDerefFlow:: flowTo ( n ) and
244247 isInvalidPointerDerefSink ( n , i , _)
245248 )
246249 }
@@ -334,6 +337,7 @@ predicate joinOn1(
334337 * that dereferences `p1`. The string `operation` describes whether the `i` is
335338 * a `StoreInstruction` or `LoadInstruction`.
336339 */
340+ pragma [ inline]
337341predicate joinOn2 ( InvalidPointerToDerefFlow:: PathNode p1 , Instruction i , string operation ) {
338342 isInvalidPointerDerefSink ( p1 .getNode ( ) , i , operation )
339343}
0 commit comments