@@ -207,22 +207,20 @@ private predicate unknownSign(Instruction i) {
207207}
208208
209209/**
210- * Holds if `lowerbound` is a lower bound for `bounded` at `pos `. This is restricted
210+ * Holds if `lowerbound` is a lower bound for `bounded``. This is restricted
211211 * to only include bounds for which we might determine a sign.
212212 */
213- private predicate lowerBound ( IRGuardCondition comp , Instruction lowerbound , Instruction bounded , Instruction pos , boolean isStrict ) {
213+ private predicate lowerBound ( IRGuardCondition comp , Operand lowerbound , Operand bounded , boolean isStrict ) {
214214 exists ( int adjustment , Instruction compared |
215- valueNumber ( bounded ) = valueNumber ( compared ) and
216- bounded = pos .getAnOperand ( ) and
217- not unknownSign ( lowerbound ) and
218- (
219- isStrict = true and
220- adjustment = 0
221- or
222- isStrict = false and
223- adjustment = 1
224- ) and
225- comp .ensuresLt ( lowerbound , compared , adjustment , pos .getBlock ( ) , true )
215+ valueNumber ( bounded .getDefinitionInstruction ( ) ) = valueNumber ( compared ) and
216+ (
217+ isStrict = true and
218+ adjustment = 0
219+ or
220+ isStrict = false and
221+ adjustment = 1
222+ ) and
223+ comp .ensuresLt ( lowerbound .getDefinitionInstruction ( ) , compared , adjustment , bounded .getInstruction ( ) .getBlock ( ) , true )
226224 )
227225}
228226
@@ -231,19 +229,17 @@ private predicate lowerBound(IRGuardCondition comp, Instruction lowerbound, Inst
231229 * Holds if `upperbound` is an upper bound for `bounded` at `pos`. This is restricted
232230 * to only include bounds for which we might determine a sign.
233231 */
234- private predicate upperBound ( IRGuardCondition comp , Instruction upperbound , Instruction bounded , Instruction pos , boolean isStrict ) {
232+ private predicate upperBound ( IRGuardCondition comp , Operand upperbound , Operand bounded , boolean isStrict ) {
235233 exists ( int adjustment , Instruction compared |
236- valueNumber ( bounded ) = valueNumber ( compared ) and
237- bounded = pos .getAnOperand ( ) and
238- not unknownSign ( upperbound ) and
239- (
240- isStrict = true and
241- adjustment = 0
242- or
243- isStrict = false and
244- adjustment = 1
245- ) and
246- comp .ensuresLt ( compared , upperbound , adjustment , pos .getBlock ( ) , true )
234+ valueNumber ( bounded .getDefinitionInstruction ( ) ) = valueNumber ( compared ) and
235+ (
236+ isStrict = true and
237+ adjustment = 0
238+ or
239+ isStrict = false and
240+ adjustment = 1
241+ ) and
242+ comp .ensuresLt ( compared , upperbound .getDefinitionInstruction ( ) , adjustment , bounded .getInstruction ( ) .getBlock ( ) , true )
247243 )
248244}
249245
@@ -254,12 +250,10 @@ private predicate upperBound(IRGuardCondition comp, Instruction upperbound, Inst
254250 * - `isEq = true` : `bounded = eqbound`
255251 * - `isEq = false` : `bounded != eqbound`
256252 */
257- private predicate eqBound ( IRGuardCondition guard , Instruction eqbound , Instruction bounded , Instruction pos , boolean isEq ) {
253+ private predicate eqBound ( IRGuardCondition guard , Operand eqbound , Operand bounded , boolean isEq ) {
258254 exists ( Instruction compared |
259- not unknownSign ( eqbound ) and
260- valueNumber ( bounded ) = valueNumber ( compared ) and
261- bounded = pos .getAnOperand ( ) and
262- guard .ensuresEq ( compared , eqbound , 0 , pos .getBlock ( ) , isEq )
255+ valueNumber ( bounded .getDefinitionInstruction ( ) ) = valueNumber ( compared ) and
256+ guard .ensuresEq ( compared , eqbound .getDefinitionInstruction ( ) , 0 , bounded .getInstruction ( ) .getBlock ( ) , isEq )
263257 )
264258}
265259
@@ -269,56 +263,56 @@ private predicate eqBound(IRGuardCondition guard, Instruction eqbound, Instructi
269263 * Holds if `bound` is a bound for `v` at `pos` that needs to be positive in
270264 * order for `v` to be positive.
271265 */
272- private predicate posBound ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
273- upperBound ( comp , bound , v , pos , _) or
274- eqBound ( comp , bound , v , pos , true )
266+ private predicate posBound ( IRGuardCondition comp , Operand bound , Operand op ) {
267+ upperBound ( comp , bound , op , _) or
268+ eqBound ( comp , bound , op , true )
275269}
276270
277271/**
278272 * Holds if `bound` is a bound for `v` at `pos` that needs to be negative in
279273 * order for `v` to be negative.
280274 */
281- private predicate negBound ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
282- lowerBound ( comp , bound , v , pos , _) or
283- eqBound ( comp , bound , v , pos , true )
275+ private predicate negBound ( IRGuardCondition comp , Operand bound , Operand op ) {
276+ lowerBound ( comp , bound , op , _) or
277+ eqBound ( comp , bound , op , true )
284278}
285279
286280/**
287281 * Holds if `bound` is a bound for `v` at `pos` that can restrict whether `v`
288282 * can be zero.
289283 */
290- private predicate zeroBound ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
291- lowerBound ( comp , bound , v , pos , _) or
292- upperBound ( comp , bound , v , pos , _) or
293- eqBound ( comp , bound , v , pos , _)
284+ private predicate zeroBound ( IRGuardCondition comp , Operand bound , Operand op ) {
285+ lowerBound ( comp , bound , op , _) or
286+ upperBound ( comp , bound , op , _) or
287+ eqBound ( comp , bound , op , _)
294288}
295289
296290/** Holds if `bound` allows `v` to be positive at `pos`. */
297- private predicate posBoundOk ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
298- posBound ( comp , bound , v , pos ) and TPos ( ) = operandSign ( comp , bound )
291+ private predicate posBoundOk ( IRGuardCondition comp , Operand bound , Operand op ) {
292+ posBound ( comp , bound , op ) and TPos ( ) = operandSign ( bound )
299293}
300294
301295/** Holds if `bound` allows `v` to be negative at `pos`. */
302- private predicate negBoundOk ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
303- negBound ( comp , bound , v , pos ) and TNeg ( ) = operandSign ( comp , bound )
296+ private predicate negBoundOk ( IRGuardCondition comp , Operand bound , Operand op ) {
297+ negBound ( comp , bound , op ) and TNeg ( ) = operandSign ( bound )
304298}
305299
306300/** Holds if `bound` allows `v` to be zero at `pos`. */
307- private predicate zeroBoundOk ( IRGuardCondition comp , Instruction bound , Instruction v , Instruction pos ) {
308- lowerBound ( comp , bound , v , pos , _) and TNeg ( ) = operandSign ( comp , bound ) or
309- lowerBound ( comp , bound , v , pos , false ) and TZero ( ) = operandSign ( comp , bound ) or
310- upperBound ( comp , bound , v , pos , _) and TPos ( ) = operandSign ( comp , bound ) or
311- upperBound ( comp , bound , v , pos , false ) and TZero ( ) = operandSign ( comp , bound ) or
312- eqBound ( comp , bound , v , pos , true ) and TZero ( ) = operandSign ( comp , bound ) or
313- eqBound ( comp , bound , v , pos , false ) and TZero ( ) != operandSign ( comp , bound )
301+ private predicate zeroBoundOk ( IRGuardCondition comp , Operand bound , Operand op ) {
302+ lowerBound ( comp , bound , op , _) and TNeg ( ) = operandSign ( bound ) or
303+ lowerBound ( comp , bound , op , false ) and TZero ( ) = operandSign ( bound ) or
304+ upperBound ( comp , bound , op , _) and TPos ( ) = operandSign ( bound ) or
305+ upperBound ( comp , bound , op , false ) and TZero ( ) = operandSign ( bound ) or
306+ eqBound ( comp , bound , op , true ) and TZero ( ) = operandSign ( bound ) or
307+ eqBound ( comp , bound , op , false ) and TZero ( ) != operandSign ( bound )
314308}
315309
316310private Sign binaryOpLhsSign ( Instruction i ) {
317- result = operandSign ( i , i . ( BinaryInstruction ) . getLeftOperand ( ) )
311+ result = operandSign ( i . getAnOperand ( ) . ( LeftOperand ) )
318312}
319313
320314private Sign binaryOpRhsSign ( Instruction i ) {
321- result = operandSign ( i , i . ( BinaryInstruction ) . getRightOperand ( ) )
315+ result = operandSign ( i . getAnOperand ( ) . ( RightOperand ) )
322316}
323317
324318pragma [ noinline]
@@ -327,44 +321,44 @@ private predicate binaryOpSigns(Instruction i, Sign lhs, Sign rhs) {
327321 rhs = binaryOpRhsSign ( i )
328322}
329323
330- private Sign unguardedOperandSign ( Instruction pos , Instruction operand ) {
331- result = instructionSign ( operand ) and
332- not hasGuard ( operand , pos , result )
324+ private Sign unguardedOperandSign ( Operand operand ) {
325+ result = instructionSign ( operand . getDefinitionInstruction ( ) ) and
326+ not hasGuard ( operand , result )
333327}
334328
335- private Sign guardedOperandSign ( Instruction pos , Instruction operand ) {
336- result = instructionSign ( operand ) and
337- hasGuard ( operand , pos , result )
329+ private Sign guardedOperandSign ( Operand operand ) {
330+ result = instructionSign ( operand . getDefinitionInstruction ( ) ) and
331+ hasGuard ( operand , result )
338332}
339333
340- private Sign guardedOperandSignOk ( Instruction pos , Instruction operand ) {
341- result = TPos ( ) and forex ( IRGuardCondition guard , Instruction bound | posBound ( guard , bound , operand , pos ) | posBoundOk ( guard , bound , operand , pos ) ) or
342- result = TNeg ( ) and forex ( IRGuardCondition guard , Instruction bound | negBound ( guard , bound , operand , pos ) | negBoundOk ( guard , bound , operand , pos ) ) or
343- result = TZero ( ) and forex ( IRGuardCondition guard , Instruction bound | zeroBound ( guard , bound , operand , pos ) | zeroBoundOk ( guard , bound , operand , pos ) )
334+ private Sign guardedOperandSignOk ( Operand operand ) {
335+ result = TPos ( ) and forex ( IRGuardCondition guard , Operand bound | posBound ( guard , bound , operand ) | posBoundOk ( guard , bound , operand ) ) or
336+ result = TNeg ( ) and forex ( IRGuardCondition guard , Operand bound | negBound ( guard , bound , operand ) | negBoundOk ( guard , bound , operand ) ) or
337+ result = TZero ( ) and forex ( IRGuardCondition guard , Operand bound | zeroBound ( guard , bound , operand ) | zeroBoundOk ( guard , bound , operand ) )
344338}
345339
346340/**
347341 * Holds if there is a bound that might restrict whether `v` has the sign `s`
348342 * at `pos`.
349343 */
350- private predicate hasGuard ( Instruction v , Instruction pos , Sign s ) {
351- s = TPos ( ) and posBound ( _, _, v , pos )
344+ private predicate hasGuard ( Operand op , Sign s ) {
345+ s = TPos ( ) and posBound ( _, _, op )
352346 or
353- s = TNeg ( ) and negBound ( _, _, v , pos )
347+ s = TNeg ( ) and negBound ( _, _, op )
354348 or
355- s = TZero ( ) and zeroBound ( _, _, v , pos )
349+ s = TZero ( ) and zeroBound ( _, _, op )
356350}
357351
358- cached private module SignAnalysisCached {
352+ cached module SignAnalysisCached {
359353 /**
360354 * Gets a sign that `operand` may have at `pos`, taking guards into account.
361355 */
362356 cached
363- Sign operandSign ( Instruction pos , Instruction operand ) {
364- result = unguardedOperandSign ( pos , operand )
357+ Sign operandSign ( Operand operand ) {
358+ result = unguardedOperandSign ( operand )
365359 or
366- result = guardedOperandSign ( pos , operand ) and
367- result = guardedOperandSignOk ( pos , operand )
360+ result = guardedOperandSign ( operand ) and
361+ result = guardedOperandSignOk ( operand )
368362 }
369363
370364 cached
@@ -392,18 +386,14 @@ cached private module SignAnalysisCached {
392386 then fromSigned = true
393387 else fromSigned = false
394388 ) and
395- result = castSign ( operandSign ( ci , prior ) , fromSigned , toSigned , getCastKind ( ci ) )
389+ result = castSign ( operandSign ( ci . getAnOperand ( ) ) , fromSigned , toSigned , getCastKind ( ci ) )
396390 )
397391 or
398- exists ( Instruction prior |
399- prior = i .( CopyInstruction ) .getSourceValue ( )
400- |
401- result = operandSign ( i , prior )
402- )
392+ result = operandSign ( i .getAnOperand ( ) .( CopySourceOperand ) )
403393 or
404- result = operandSign ( i , i .( BitComplementInstruction ) .getOperand ( ) ) .bitnot ( )
394+ result = operandSign ( i .( BitComplementInstruction ) .getAnOperand ( ) ) .bitnot ( )
405395 or
406- result = operandSign ( i , i .( NegateInstruction ) .getOperand ( ) ) .neg ( )
396+ result = operandSign ( i .( NegateInstruction ) .getAnOperand ( ) ) .neg ( )
407397 or
408398 exists ( Sign s1 , Sign s2 |
409399 binaryOpSigns ( i , s1 , s2 )
@@ -436,58 +426,58 @@ cached private module SignAnalysisCached {
436426 )
437427 or
438428 // use hasGuard here?
439- result = operandSign ( i , i .( PhiInstruction ) .getAnOperand ( ) )
429+ result = operandSign ( i .( PhiInstruction ) .getAnOperand ( ) )
440430 )
441431 }
442432}
443433
444434/** Holds if `i` can be positive and cannot be negative. */
445- predicate positive ( Instruction i ) {
435+ predicate positiveInstruction ( Instruction i ) {
446436 instructionSign ( i ) = TPos ( ) and
447437 not instructionSign ( i ) = TNeg ( )
448438}
449439
450440/** Holds if `i` at `pos` can be positive at and cannot be negative. */
451- predicate positive ( Instruction i , Instruction pos ) {
452- operandSign ( pos , i ) = TPos ( ) and
453- not operandSign ( pos , i ) = TNeg ( )
441+ predicate positive ( Operand op ) {
442+ operandSign ( op ) = TPos ( ) and
443+ not operandSign ( op ) = TNeg ( )
454444}
455445
456446/** Holds if `i` can be negative and cannot be positive. */
457- predicate negative ( Instruction i ) {
447+ predicate negativeInstruction ( Instruction i ) {
458448 instructionSign ( i ) = TNeg ( ) and
459449 not instructionSign ( i ) = TPos ( )
460450}
461451
462452/** Holds if `i` at `pos` can be negative and cannot be positive. */
463- predicate negative ( Instruction i , Instruction pos ) {
464- operandSign ( pos , i ) = TNeg ( ) and
465- not operandSign ( pos , i ) = TPos ( )
453+ predicate negative ( Operand op ) {
454+ operandSign ( op ) = TNeg ( ) and
455+ not operandSign ( op ) = TPos ( )
466456}
467457
468458/** Holds if `i` is strictly positive. */
469- predicate strictlyPositive ( Instruction i ) {
459+ predicate strictlyPositiveInstruction ( Instruction i ) {
470460 instructionSign ( i ) = TPos ( ) and
471461 not instructionSign ( i ) = TNeg ( ) and
472462 not instructionSign ( i ) = TZero ( )
473463}
474464
475465/** Holds if `i` is strictly positive at `pos`. */
476- predicate strictlyPositive ( Instruction i , Instruction pos ) {
477- operandSign ( pos , i ) = TPos ( ) and
478- not operandSign ( pos , i ) = TNeg ( ) and
479- not operandSign ( pos , i ) = TZero ( )
466+ predicate strictlyPositive ( Operand op ) {
467+ operandSign ( op ) = TPos ( ) and
468+ not operandSign ( op ) = TNeg ( ) and
469+ not operandSign ( op ) = TZero ( )
480470}
481471/** Holds if `i` is strictly negative. */
482- predicate strictlyNegative ( Instruction i ) {
472+ predicate strictlyNegativeInstruction ( Instruction i ) {
483473 instructionSign ( i ) = TNeg ( ) and
484474 not instructionSign ( i ) = TPos ( ) and
485475 not instructionSign ( i ) = TZero ( )
486476}
487477
488478/** Holds if `i` is strictly negative at `pos`. */
489- predicate strictlyNegative ( Instruction i , Instruction pos ) {
490- operandSign ( pos , i ) = TNeg ( ) and
491- not operandSign ( pos , i ) = TPos ( ) and
492- not operandSign ( pos , i ) = TZero ( )
479+ predicate strictlyNegative ( Operand op ) {
480+ operandSign ( op ) = TNeg ( ) and
481+ not operandSign ( op ) = TPos ( ) and
482+ not operandSign ( op ) = TZero ( )
493483}
0 commit comments