@@ -203,30 +203,42 @@ private class GuardConditionFromIR extends GuardCondition {
203203 * `&&` and `||`. See the detailed explanation on predicate `controls`.
204204 */
205205 private predicate controlsBlock ( BasicBlock controlled , boolean testIsTrue ) {
206- exists ( IRBlock irb , Instruction instr |
206+ exists ( IRBlock irb |
207207 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 )
212210 )
213211 }
212+ }
214213
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 ( ) )
226218 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+ )
230242}
231243
232244/**
0 commit comments