@@ -131,8 +131,10 @@ module Barrier2 {
131
131
}
132
132
133
133
Instruction getABarrierInstruction ( FlowState2 state ) {
134
- exists ( IRGuardCondition g , ValueNumber value , boolean edge |
135
- operandGuardChecks ( g , value .getAUse ( ) , _, state , edge ) and
134
+ exists ( IRGuardCondition g , ValueNumber value , Operand use , boolean edge |
135
+ use = value .getAUse ( ) and
136
+ operandGuardChecks ( pragma [ only_bind_into ] ( g ) , pragma [ only_bind_into ] ( use ) , _,
137
+ pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( edge ) ) and
136
138
result = value .getAnInstruction ( ) and
137
139
g .controls ( result .getBlock ( ) , edge )
138
140
)
@@ -239,11 +241,13 @@ pragma[nomagic]
239
241
predicate pointerAddInstructionHasBounds (
240
242
PointerAddInstruction pai , DataFlow:: Node sink1 , DataFlow:: Node sink2 , int delta
241
243
) {
242
- exists ( Instruction right |
244
+ exists ( Instruction right , Instruction instr2 |
243
245
pai .getRight ( ) = right and
244
246
pai .getLeft ( ) = sink1 .asInstruction ( ) and
245
- bounded1 ( right , sink2 .asInstruction ( ) , delta ) and
246
- not [ right , sink2 .asInstruction ( ) ] = Barrier2:: getABarrierInstruction ( delta )
247
+ instr2 = sink2 .asInstruction ( ) and
248
+ bounded1 ( right , instr2 , delta ) and
249
+ not right = Barrier2:: getABarrierInstruction ( delta ) and
250
+ not instr2 = Barrier2:: getABarrierInstruction ( delta )
247
251
)
248
252
}
249
253
0 commit comments