@@ -147,7 +147,7 @@ abstract class Configuration extends string {
147147 */
148148 predicate isBarrier ( DataFlow:: Node node ) {
149149 exists ( BarrierGuardNode guard |
150- isBarrierGuard ( guard ) and
150+ isBarrierGuardInternal ( guard ) and
151151 guard .internalBlocks ( node , "" )
152152 )
153153 }
@@ -181,7 +181,7 @@ abstract class Configuration extends string {
181181 */
182182 predicate isLabeledBarrier ( DataFlow:: Node node , FlowLabel lbl ) {
183183 exists ( BarrierGuardNode guard |
184- isBarrierGuard ( guard ) and
184+ isBarrierGuardInternal ( guard ) and
185185 guard .internalBlocks ( node , lbl )
186186 )
187187 or
@@ -198,6 +198,12 @@ abstract class Configuration extends string {
198198 */
199199 predicate isBarrierGuard ( BarrierGuardNode guard ) { none ( ) }
200200
201+ private predicate isBarrierGuardInternal ( BarrierGuardNode guard ) {
202+ isBarrierGuard ( guard )
203+ or
204+ guard .( AdditionalBarrierGuardNode ) .appliesTo ( this )
205+ }
206+
201207 /**
202208 * Holds if data may flow from `source` to `sink` for this configuration.
203209 */
@@ -302,42 +308,27 @@ abstract class BarrierGuardNode extends DataFlow::Node {
302308 exists ( SsaRefinementNode ref , boolean outcome |
303309 nd = DataFlow:: ssaDefinitionNode ( ref ) and
304310 forex ( SsaVariable input | input = ref .getAnInput ( ) |
305- asExpr ( ) = ref .getGuard ( ) .getTest ( ) and
311+ getExpr ( ) = ref .getGuard ( ) .getTest ( ) and
306312 outcome = ref .getGuard ( ) .( ConditionGuardNode ) .getOutcome ( ) and
307- internalBlocksExpr ( outcome , input .getAUse ( ) , label )
313+ barrierGuardBlocksExpr ( this , outcome , input .getAUse ( ) , label )
308314 )
309315 )
310316 or
311317 // 2) `nd` is an instance of an access path `p`, and dominated by a barrier for `p`
312318 exists ( AccessPath p , BasicBlock bb , ConditionGuardNode cond , boolean outcome |
313319 nd = DataFlow:: valueNode ( p .getAnInstanceIn ( bb ) ) and
314- asExpr ( ) = cond .getTest ( ) and
320+ getExpr ( ) = cond .getTest ( ) and
315321 outcome = cond .getOutcome ( ) and
316- internalBlocksAccessPath ( outcome , p , label ) and
322+ barrierGuardBlocksAccessPath ( this , outcome , p , label ) and
317323 cond .dominates ( bb )
318324 )
319325 }
320326
321- /**
322- * Holds if data flow node `nd` acts as a barrier for data flow.
323- *
324- * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
325- */
326- private predicate internalBlocksExpr ( boolean outcome , Expr test , string label ) {
327- blocks ( outcome , test ) and label = ""
327+ /** Gets the corresponding expression, including that of reflective calls. */
328+ private Expr getExpr ( ) {
329+ result = asExpr ( )
328330 or
329- blocks ( outcome , test , label )
330- }
331-
332- /**
333- * Holds if data flow node `nd` acts as a barrier for data flow due to aliasing through
334- * an access path.
335- *
336- * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
337- */
338- pragma [ noinline]
339- private predicate internalBlocksAccessPath ( boolean outcome , AccessPath ap , string label ) {
340- internalBlocksExpr ( outcome , ap .getAnInstance ( ) , label )
331+ this = DataFlow:: reflectiveCallNode ( result )
341332 }
342333
343334 /**
@@ -353,6 +344,32 @@ abstract class BarrierGuardNode extends DataFlow::Node {
353344 predicate blocks ( boolean outcome , Expr e , FlowLabel label ) { none ( ) }
354345}
355346
347+ /**
348+ * Holds if data flow node `nd` acts as a barrier for data flow.
349+ *
350+ * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
351+ */
352+ private predicate barrierGuardBlocksExpr ( BarrierGuardNode guard , boolean outcome , Expr test , string label ) {
353+ guard .blocks ( outcome , test ) and label = ""
354+ or
355+ guard .blocks ( outcome , test , label )
356+ or
357+ // Handle labelled barrier guard functions specially, to avoid negative recursion
358+ // through the non-abstract 3-argument version of blocks().
359+ guard .( AdditionalBarrierGuardCall ) .internalBlocksLabel ( outcome , test , label )
360+ }
361+
362+ /**
363+ * Holds if data flow node `nd` acts as a barrier for data flow due to aliasing through
364+ * an access path.
365+ *
366+ * `label` is bound to the blocked label, or the empty string if all labels should be blocked.
367+ */
368+ pragma [ noinline]
369+ private predicate barrierGuardBlocksAccessPath ( BarrierGuardNode guard , boolean outcome , AccessPath ap , string label ) {
370+ barrierGuardBlocksExpr ( guard , outcome , ap .getAnInstance ( ) , label )
371+ }
372+
356373/**
357374 * A guard node that only blocks specific labels.
358375 */
@@ -1186,3 +1203,110 @@ module PathGraph {
11861203 not pred = finalMidNode ( succ )
11871204 }
11881205}
1206+
1207+
1208+
1209+ /**
1210+ * Gets an operand of the given `&&` operator.
1211+ *
1212+ * We use this to construct the transitive closure over a relation
1213+ * that does not include all of `BinaryExpr.getAnOperand`.
1214+ */
1215+ private Expr getALogicalAndOperand ( LogAndExpr e ) {
1216+ result = e .getAnOperand ( )
1217+ }
1218+
1219+ /**
1220+ * Gets an operand of the given `||` operator.
1221+ *
1222+ * We use this to construct the transitive closure over a relation
1223+ * that does not include all of `BinaryExpr.getAnOperand`.
1224+ */
1225+ private Expr getALogicalOrOperand ( LogOrExpr e ) {
1226+ result = e .getAnOperand ( )
1227+ }
1228+
1229+ /**
1230+ * A `BarrierGuardNode` that controls which data flow
1231+ * configurations it is used in.
1232+ *
1233+ * Note: For performance reasons, all subclasses of this class should be part
1234+ * of the standard library. Override `Configuration::isBarrierGuard`
1235+ * for analysis-specific barrier guards.
1236+ */
1237+ abstract class AdditionalBarrierGuardNode extends BarrierGuardNode {
1238+ abstract predicate appliesTo ( Configuration cfg ) ;
1239+ }
1240+
1241+ /**
1242+ * A function that returns the result of a barrier guard.
1243+ */
1244+ private class BarrierGuardFunction extends Function {
1245+ DataFlow:: ParameterNode sanitizedParameter ;
1246+ BarrierGuardNode guard ;
1247+ boolean guardOutcome ;
1248+ string label ;
1249+
1250+ BarrierGuardFunction ( ) {
1251+ exists ( Expr e |
1252+ exists ( Expr returnExpr |
1253+ returnExpr = guard .asExpr ( )
1254+ or
1255+ // ad hoc support for conjunctions:
1256+ getALogicalAndOperand + ( returnExpr ) = guard .asExpr ( ) and guardOutcome = true
1257+ or
1258+ // ad hoc support for disjunctions:
1259+ getALogicalOrOperand + ( returnExpr ) = guard .asExpr ( ) and guardOutcome = false
1260+ |
1261+ exists ( SsaExplicitDefinition ssa |
1262+ ssa .getDef ( ) .getSource ( ) = returnExpr and
1263+ ssa .getVariable ( ) .getAUse ( ) = getAReturnedExpr ( )
1264+ )
1265+ or
1266+ returnExpr = getAReturnedExpr ( )
1267+ ) and
1268+ sanitizedParameter .flowsToExpr ( e ) and
1269+ barrierGuardBlocksExpr ( guard , guardOutcome , e , label )
1270+ ) and
1271+ getNumParameter ( ) = 1 and
1272+ sanitizedParameter .getParameter ( ) = getParameter ( 0 )
1273+ }
1274+
1275+ /**
1276+ * Holds if this function sanitizes argument `e` of call `call`, provided the call evaluates to `outcome`.
1277+ */
1278+ predicate isBarrierCall ( DataFlow:: CallNode call , Expr e , boolean outcome , string lbl ) {
1279+ exists ( DataFlow:: Node arg |
1280+ arg .asExpr ( ) = e and
1281+ arg = call .getArgument ( 0 ) and
1282+ call .getNumArgument ( ) = 1 and
1283+ argumentPassing ( call , arg , this , sanitizedParameter ) and
1284+ outcome = guardOutcome and
1285+ lbl = label
1286+ )
1287+ }
1288+
1289+ /**
1290+ * Holds if this function applies to the flow in `cfg`.
1291+ */
1292+ predicate appliesTo ( Configuration cfg ) { cfg .isBarrierGuard ( guard ) }
1293+ }
1294+
1295+ /**
1296+ * A call that sanitizes an argument.
1297+ */
1298+ private class AdditionalBarrierGuardCall extends AdditionalBarrierGuardNode , DataFlow:: CallNode {
1299+ BarrierGuardFunction f ;
1300+
1301+ AdditionalBarrierGuardCall ( ) { f .isBarrierCall ( this , _, _, _) }
1302+
1303+ override predicate blocks ( boolean outcome , Expr e ) {
1304+ f .isBarrierCall ( this , e , outcome , "" )
1305+ }
1306+
1307+ predicate internalBlocksLabel ( boolean outcome , Expr e , DataFlow:: FlowLabel label ) {
1308+ f .isBarrierCall ( this , e , outcome , label )
1309+ }
1310+
1311+ override predicate appliesTo ( Configuration cfg ) { f .appliesTo ( cfg ) }
1312+ }
0 commit comments