@@ -1013,12 +1013,18 @@ module Internal {
10131013 * Holds if pre-basic-block `bb` only is reached when guard `g` has abstract value `v`,
10141014 * not taking implications into account.
10151015 */
1016+ pragma [ nomagic]
10161017 private predicate preControlsDirect ( Guard g , PreBasicBlocks:: PreBasicBlock bb , AbstractValue v ) {
10171018 exists ( PreBasicBlocks:: ConditionBlock cb , ConditionalSuccessor s | cb .controls ( bb , s ) |
10181019 v .branch ( cb .getLastElement ( ) , s , g )
10191020 )
10201021 }
10211022
1023+ pragma [ nomagic]
1024+ private predicate preControlsDefDirect ( Guard g , PreSsa:: Definition def , AbstractValue v ) {
1025+ preControlsDirect ( g , def .getBasicBlock ( ) , v )
1026+ }
1027+
10221028 /** Holds if pre-basic-block `bb` only is reached when guard `g` has abstract value `v`. */
10231029 predicate preControls ( Guard g , PreBasicBlocks:: PreBasicBlock bb , AbstractValue v ) {
10241030 preControlsDirect ( g , bb , v )
@@ -1111,36 +1117,47 @@ module Internal {
11111117 )
11121118 }
11131119
1114- pragma [ noinline ]
1120+ pragma [ nomagic ]
11151121 private predicate conditionalAssign0 (
11161122 Guard guard , AbstractValue vGuard , PreSsa:: PhiNode phi , Expr e , PreSsa:: Definition upd ,
1117- PreBasicBlocks:: PreBasicBlock bbGuard
1123+ PreBasicBlocks:: PreBasicBlock bbGuard , PreBasicBlocks :: PreBasicBlock bbPhi
11181124 ) {
11191125 e = upd .getDefinition ( ) .getSource ( ) and
11201126 upd = phi .getAnInput ( ) and
1121- preControlsDirect ( guard , upd . getBasicBlock ( ) , vGuard ) and
1127+ preControlsDefDirect ( guard , upd , vGuard ) and
11221128 bbGuard .getAnElement ( ) = guard and
1123- bbGuard .strictlyDominates ( phi .getBasicBlock ( ) ) and
1124- not preControlsDirect ( guard , phi .getBasicBlock ( ) , vGuard )
1129+ bbPhi = phi .getBasicBlock ( )
11251130 }
11261131
11271132 pragma [ noinline]
11281133 private predicate conditionalAssign1 (
1134+ Guard guard , AbstractValue vGuard , PreSsa:: PhiNode phi , Expr e , PreSsa:: Definition upd ,
1135+ PreBasicBlocks:: PreBasicBlock bbGuard
1136+ ) {
1137+ exists ( PreBasicBlocks:: PreBasicBlock bbPhi |
1138+ conditionalAssign0 ( guard , vGuard , phi , e , upd , bbGuard , bbPhi ) and
1139+ bbGuard .strictlyDominates ( bbPhi ) and
1140+ not preControlsDefDirect ( guard , phi , vGuard )
1141+ )
1142+ }
1143+
1144+ pragma [ noinline]
1145+ private predicate conditionalAssign2 (
11291146 Guard guard , AbstractValue vGuard , PreSsa:: PhiNode phi , Expr e , PreSsa:: Definition upd ,
11301147 PreBasicBlocks:: PreBasicBlock bbGuard , PreSsa:: Definition other
11311148 ) {
1132- conditionalAssign0 ( guard , vGuard , phi , e , upd , bbGuard ) and
1149+ conditionalAssign1 ( guard , vGuard , phi , e , upd , bbGuard ) and
11331150 other != upd and
11341151 other = phi .getAnInput ( )
11351152 }
11361153
11371154 pragma [ noinline]
1138- private predicate conditionalAssign2 (
1155+ private predicate conditionalAssign3 (
11391156 Guard guard , AbstractValue vGuard , PreSsa:: Definition def , Expr e , PreSsa:: Definition upd ,
11401157 PreBasicBlocks:: PreBasicBlock bbGuard , PreSsa:: Definition other
11411158 ) {
1142- conditionalAssign1 ( guard , vGuard , def , e , upd , bbGuard , other ) and
1143- preControlsDirect ( guard , other . getBasicBlock ( ) , vGuard .getDualValue ( ) )
1159+ conditionalAssign2 ( guard , vGuard , def , e , upd , bbGuard , other ) and
1160+ preControlsDefDirect ( guard , other , vGuard .getDualValue ( ) )
11441161 }
11451162
11461163 /** Gets the successor block that is reached when guard `g` has abstract value `v`. */
@@ -1153,11 +1170,11 @@ module Internal {
11531170 }
11541171
11551172 pragma [ noinline]
1156- private predicate conditionalAssign3 (
1173+ private predicate conditionalAssign4 (
11571174 Guard guard , AbstractValue vGuard , PreSsa:: Definition def , Expr e , PreSsa:: Definition upd ,
11581175 PreBasicBlocks:: PreBasicBlock bbGuard , PreSsa:: Definition other
11591176 ) {
1160- conditionalAssign1 ( guard , vGuard , def , e , upd , bbGuard , other ) and
1177+ conditionalAssign2 ( guard , vGuard , def , e , upd , bbGuard , other ) and
11611178 other .getBasicBlock ( ) .dominates ( bbGuard ) and
11621179 not other .isLiveAtEndOfBlock ( getConditionalSuccessor ( guard , vGuard ) )
11631180 }
@@ -1184,25 +1201,25 @@ module Internal {
11841201 )
11851202 or
11861203 exists ( PreSsa:: Definition upd , PreBasicBlocks:: PreBasicBlock bbGuard |
1187- conditionalAssign0 ( guard , vGuard , def , e , upd , bbGuard )
1204+ conditionalAssign1 ( guard , vGuard , def , e , upd , bbGuard )
11881205 |
11891206 forall ( PreSsa:: Definition other |
1190- conditionalAssign1 ( guard , vGuard , def , e , upd , bbGuard , other )
1207+ conditionalAssign2 ( guard , vGuard , def , e , upd , bbGuard , other )
11911208 |
11921209 // For example:
11931210 // if (guard)
11941211 // upd = a;
11951212 // else
11961213 // other = b;
11971214 // def = phi(upd, other)
1198- conditionalAssign2 ( guard , vGuard , def , e , upd , bbGuard , other )
1215+ conditionalAssign3 ( guard , vGuard , def , e , upd , bbGuard , other )
11991216 or
12001217 // For example:
12011218 // other = a;
12021219 // if (guard)
12031220 // upd = b;
12041221 // def = phi(other, upd)
1205- conditionalAssign3 ( guard , vGuard , def , e , upd , bbGuard , other )
1222+ conditionalAssign4 ( guard , vGuard , def , e , upd , bbGuard , other )
12061223 )
12071224 )
12081225 }
0 commit comments