@@ -289,8 +289,25 @@ private ControlFlowNode getAGuardBranchSuccessor(Guard g, boolean branch) {
289289 result = g .( SwitchCase ) .getControlFlowNode ( ) and branch = true
290290}
291291
292+ /**
293+ * Holds if `guard` dominates `phi` and `guard` evaluating to `branch` controls the definition
294+ * `upd = e` where `upd` is a possible input to `phi`.
295+ */
296+ private predicate guardControlsPhiBranch (
297+ SsaExplicitUpdate upd , SsaPhiNode phi , Guard guard , boolean branch , Expr e
298+ ) {
299+ guard .directlyControls ( upd .getBasicBlock ( ) , branch ) and
300+ upd .getDefiningExpr ( ) .( VariableAssign ) .getSource ( ) .getProperExpr ( ) = e and
301+ upd = phi .getAPhiInput ( ) and
302+ getBasicBlockOfGuard ( guard ) .bbStrictlyDominates ( phi .getBasicBlock ( ) )
303+ }
304+
292305/**
293306 * Holds if `v` is conditionally assigned `e` under the condition that `guard` evaluates to `branch`.
307+ *
308+ * The evaluation of `guard` dominates the definition of `v` and `guard` evaluating to `branch`
309+ * implies that `e` is assigned to `v`. In particular, this allows us to conclude that if `v` has
310+ * a value different from `e` then `guard` must have evaluated to `branch.booleanNot()`.
294311 */
295312private predicate conditionalAssign ( SsaVariable v , Guard guard , boolean branch , Expr e ) {
296313 exists ( ConditionalExpr c |
@@ -303,11 +320,8 @@ private predicate conditionalAssign(SsaVariable v, Guard guard, boolean branch,
303320 )
304321 or
305322 exists ( SsaExplicitUpdate upd , SsaPhiNode phi |
306- guard .directlyControls ( upd .getBasicBlock ( ) , branch ) and
307- upd .getDefiningExpr ( ) .( VariableAssign ) .getSource ( ) .getProperExpr ( ) = e and
308323 phi = v and
309- upd = phi .getAPhiInput ( ) and
310- getBasicBlockOfGuard ( guard ) .bbStrictlyDominates ( phi .getBasicBlock ( ) ) and
324+ guardControlsPhiBranch ( upd , phi , guard , branch , e ) and
311325 not guard .directlyControls ( phi .getBasicBlock ( ) , branch ) and
312326 forall ( SsaVariable other | other != upd and other = phi .getAPhiInput ( ) |
313327 guard .directlyControls ( other .getBasicBlock ( ) , branch .booleanNot ( ) )
0 commit comments