@@ -1322,19 +1322,31 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1322
1322
}
1323
1323
}
1324
1324
1325
- cached
1326
- private newtype TNode =
1327
- TParamNode ( DfInput:: Parameter p ) { DfInput:: ssaDefInitializesParam ( _, p ) } or
1328
- TExprNode ( DfInput:: Expr e , Boolean isPost ) {
1329
- e = DfInput:: getARead ( _)
1330
- or
1331
- DfInput:: ssaDefAssigns ( _, e ) and
1332
- isPost = false
1333
- } or
1334
- TSsaDefinitionNode ( DefinitionExt def ) or
1335
- TSsaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) {
1336
- def .hasInputFromBlock ( _, _, _, _, input )
1325
+ private module Cached {
1326
+ cached
1327
+ newtype TNode =
1328
+ TParamNode ( DfInput:: Parameter p ) { DfInput:: ssaDefInitializesParam ( _, p ) } or
1329
+ TExprNode ( DfInput:: Expr e , Boolean isPost ) {
1330
+ e = DfInput:: getARead ( _)
1331
+ or
1332
+ DfInput:: ssaDefAssigns ( _, e ) and
1333
+ isPost = false
1334
+ } or
1335
+ TSsaDefinitionNode ( DefinitionExt def ) or
1336
+ TSsaInputNode ( SsaInputDefinitionExt def , BasicBlock input ) {
1337
+ def .hasInputFromBlock ( _, _, _, _, input )
1338
+ }
1339
+
1340
+ cached
1341
+ Definition getAPhiInputDef ( SsaInputNode n ) {
1342
+ exists ( SsaInputDefinitionExt phi , BasicBlock bb |
1343
+ phi .hasInputFromBlock ( result , _, _, _, bb ) and
1344
+ n .isInputInto ( phi , bb )
1345
+ )
1337
1346
}
1347
+ }
1348
+
1349
+ private import Cached
1338
1350
1339
1351
/**
1340
1352
* A data flow node that we need to reference in the value step relation.
@@ -1606,46 +1618,56 @@ module Make<LocationSig Location, InputSig<Location> Input> {
1606
1618
nodeTo .( ExprNode ) .getExpr ( ) = DfInput:: getARead ( def )
1607
1619
}
1608
1620
1609
- pragma [ nomagic]
1610
- private predicate guardControlsSsaRead (
1611
- DfInput:: Guard g , boolean branch , Definition def , ExprNode n
1612
- ) {
1613
- exists ( BasicBlock bb , DfInput:: Expr e |
1614
- e = n .getExpr ( ) and
1615
- DfInput:: getARead ( def ) = e and
1616
- DfInput:: guardControlsBlock ( g , bb , branch ) and
1617
- e .hasCfgNode ( bb , _)
1618
- )
1619
- }
1620
-
1621
- pragma [ nomagic]
1622
- private predicate guardControlsPhiInput (
1623
- DfInput:: Guard g , boolean branch , Definition def , BasicBlock input , SsaInputDefinitionExt phi
1624
- ) {
1625
- phi .hasInputFromBlock ( def , _, _, _, input ) and
1626
- (
1627
- DfInput:: guardControlsBlock ( g , input , branch )
1628
- or
1629
- exists ( int last |
1630
- last = input .length ( ) - 1 and
1631
- g .hasCfgNode ( input , last ) and
1632
- DfInput:: getAConditionalBasicBlockSuccessor ( input , branch ) = phi .getBasicBlock ( )
1633
- )
1634
- )
1635
- }
1621
+ /**
1622
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `branch`.
1623
+ *
1624
+ * The expression `e` is expected to be a syntactic part of the guard `g`.
1625
+ * For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
1626
+ * the argument `x`.
1627
+ */
1628
+ signature predicate guardChecksSig ( DfInput:: Guard g , DfInput:: Expr e , boolean branch ) ;
1636
1629
1637
1630
/**
1638
- * Gets a node that reads SSA defininition `def`, and which is guarded by
1639
- * `g` evaluating to `branch`.
1631
+ * Provides a set of barrier nodes for a guard that validates an expression.
1632
+ *
1633
+ * This is expected to be used in `isBarrier`/`isSanitizer` definitions
1634
+ * in data flow and taint tracking.
1640
1635
*/
1641
- pragma [ nomagic]
1642
- Node getABarrierNode ( DfInput:: Guard g , Definition def , boolean branch ) {
1643
- guardControlsSsaRead ( g , branch , def , result )
1644
- or
1645
- exists ( BasicBlock input , SsaInputDefinitionExt phi |
1646
- guardControlsPhiInput ( g , branch , def , input , phi ) and
1647
- result .( SsaInputNode ) .isInputInto ( phi , input )
1648
- )
1636
+ module BarrierGuard< guardChecksSig / 3 guardChecks> {
1637
+ pragma [ nomagic]
1638
+ private predicate guardChecksSsaDef ( DfInput:: Guard g , Definition def , boolean branch ) {
1639
+ guardChecks ( g , DfInput:: getARead ( def ) , branch )
1640
+ }
1641
+
1642
+ /** Gets a node that is safely guarded by the given guard check. */
1643
+ pragma [ nomagic]
1644
+ Node getABarrierNode ( ) {
1645
+ exists ( DfInput:: Guard g , boolean branch , Definition def , BasicBlock bb |
1646
+ guardChecksSsaDef ( g , def , branch )
1647
+ |
1648
+ // guard controls a read
1649
+ exists ( DfInput:: Expr e |
1650
+ e = DfInput:: getARead ( def ) and
1651
+ e .hasCfgNode ( bb , _) and
1652
+ DfInput:: guardControlsBlock ( g , bb , branch ) and
1653
+ result .( ExprNode ) .getExpr ( ) = e
1654
+ )
1655
+ or
1656
+ // guard controls input block to a phi node
1657
+ exists ( SsaInputDefinitionExt phi |
1658
+ def = getAPhiInputDef ( result ) and
1659
+ result .( SsaInputNode ) .isInputInto ( phi , bb )
1660
+ |
1661
+ DfInput:: guardControlsBlock ( g , bb , branch )
1662
+ or
1663
+ exists ( int last |
1664
+ last = bb .length ( ) - 1 and
1665
+ g .hasCfgNode ( bb , last ) and
1666
+ DfInput:: getAConditionalBasicBlockSuccessor ( bb , branch ) = phi .getBasicBlock ( )
1667
+ )
1668
+ )
1669
+ )
1670
+ }
1649
1671
}
1650
1672
}
1651
1673
}
0 commit comments