@@ -203,30 +203,42 @@ private class GuardConditionFromIR extends GuardCondition {
203
203
* `&&` and `||`. See the detailed explanation on predicate `controls`.
204
204
*/
205
205
private predicate controlsBlock ( BasicBlock controlled , boolean testIsTrue ) {
206
- exists ( IRBlock irb , Instruction instr |
206
+ exists ( IRBlock irb |
207
207
ir .controls ( irb , testIsTrue ) and
208
- instr = irb .getAnInstruction ( ) and
209
- instr .getAst ( ) .( ControlFlowNode ) .getBasicBlock ( ) = controlled and
210
- not isUnreachedBlock ( irb ) and
211
- not this .excludeAsControlledInstruction ( instr )
208
+ nonExcludedIRAndBasicBlock ( irb , controlled ) and
209
+ not isUnreachedBlock ( irb )
212
210
)
213
211
}
212
+ }
214
213
215
- private predicate excludeAsControlledInstruction ( Instruction instr ) {
216
- // Exclude the temporaries generated by a ternary expression.
217
- exists ( TranslatedConditionalExpr tce |
218
- instr = tce .getInstruction ( ConditionValueFalseStoreTag ( ) )
219
- or
220
- instr = tce .getInstruction ( ConditionValueTrueStoreTag ( ) )
221
- or
222
- instr = tce .getInstruction ( ConditionValueTrueTempAddressTag ( ) )
223
- or
224
- instr = tce .getInstruction ( ConditionValueFalseTempAddressTag ( ) )
225
- )
214
+ private predicate excludeAsControlledInstruction ( Instruction instr ) {
215
+ // Exclude the temporaries generated by a ternary expression.
216
+ exists ( TranslatedConditionalExpr tce |
217
+ instr = tce .getInstruction ( ConditionValueFalseStoreTag ( ) )
226
218
or
227
- // Exclude unreached instructions, as their AST is the whole function and not a block.
228
- instr instanceof UnreachedInstruction
229
- }
219
+ instr = tce .getInstruction ( ConditionValueTrueStoreTag ( ) )
220
+ or
221
+ instr = tce .getInstruction ( ConditionValueTrueTempAddressTag ( ) )
222
+ or
223
+ instr = tce .getInstruction ( ConditionValueFalseTempAddressTag ( ) )
224
+ )
225
+ or
226
+ // Exclude unreached instructions, as their AST is the whole function and not a block.
227
+ instr instanceof UnreachedInstruction
228
+ }
229
+
230
+ /**
231
+ * Holds if `irb` is the `IRBlock` corresponding to the AST basic block
232
+ * `controlled`, and `irb` does not contain any instruction(s) that should make
233
+ * the `irb` be ignored.
234
+ */
235
+ pragma [ nomagic]
236
+ private predicate nonExcludedIRAndBasicBlock ( IRBlock irb , BasicBlock controlled ) {
237
+ exists ( Instruction instr |
238
+ instr = irb .getAnInstruction ( ) and
239
+ instr .getAst ( ) .( ControlFlowNode ) .getBasicBlock ( ) = controlled and
240
+ not excludeAsControlledInstruction ( instr )
241
+ )
230
242
}
231
243
232
244
/**
0 commit comments