@@ -440,15 +440,24 @@ signature predicate guardChecksSig(CfgNodes::ExprCfgNode g, CfgNode e, boolean b
440
440
* in data flow and taint tracking.
441
441
*/
442
442
module 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
+
443
456
/** Gets a node that is safely guarded by the given guard check. */
444
457
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 )
452
461
)
453
462
or
454
463
result .asExpr ( ) = getAMaybeGuardedCapturedDef ( ) .getARead ( )
0 commit comments