@@ -440,15 +440,24 @@ signature predicate guardChecksSig(CfgNodes::ExprCfgNode g, CfgNode e, boolean b
440440 * in data flow and taint tracking.
441441 */
442442module BarrierGuard< guardChecksSig / 3 guardChecks> {
443+ pragma [ nomagic]
444+ private predicate guardChecksSsaDef ( CfgNodes:: ExprCfgNode g , boolean branch , Ssa:: Definition def ) {
445+ guardChecks ( g , def .getARead ( ) , branch )
446+ }
447+
448+ pragma [ nomagic]
449+ private predicate guardControlsSsaDef (
450+ CfgNodes:: ExprCfgNode g , boolean branch , Ssa:: Definition def , Node n
451+ ) {
452+ def .getARead ( ) = n .asExpr ( ) and
453+ guardControlsBlock ( g , n .asExpr ( ) .getBasicBlock ( ) , branch )
454+ }
455+
443456 /** Gets a node that is safely guarded by the given guard check. */
444457 Node getABarrierNode ( ) {
445- exists (
446- CfgNodes:: ExprCfgNode g , boolean branch , CfgNodes:: ExprCfgNode testedNode , Ssa:: Definition def
447- |
448- def .getARead ( ) = testedNode and
449- def .getARead ( ) = result .asExpr ( ) and
450- guardChecks ( g , testedNode , branch ) and
451- guardControlsBlock ( g , result .asExpr ( ) .getBasicBlock ( ) , branch )
458+ exists ( CfgNodes:: ExprCfgNode g , boolean branch , Ssa:: Definition def |
459+ guardChecksSsaDef ( g , branch , def ) and
460+ guardControlsSsaDef ( g , branch , def , result )
452461 )
453462 or
454463 result .asExpr ( ) = getAMaybeGuardedCapturedDef ( ) .getARead ( )
0 commit comments