@@ -231,27 +231,39 @@ class SyntheticFieldContent extends Content, TSyntheticFieldContent {
231
231
}
232
232
233
233
/**
234
- * A guard that validates some expression.
234
+ * Holds if the guard `g` validates the expression `e` upon evaluating to `branch` .
235
235
*
236
- * To use this in a configuration, extend the class and provide a
237
- * characteristic predicate precisely specifying the guard, and override
238
- * `checks` to specify what is being validated and in which branch.
236
+ * The expression `e` is expected to be a syntactic part of the guard `g`.
237
+ * For example, the guard `g` might be a call `isSafe(x)` and the expression `e`
238
+ * the argument `x`.
239
+ */
240
+ signature predicate guardChecksSig ( Node g , Expr e , boolean branch ) ;
241
+
242
+ /**
243
+ * Provides a set of barrier nodes for a guard that validates an expression.
239
244
*
240
- * When using a data-flow or taint-flow configuration `cfg`, it is important
241
- * that any classes extending BarrierGuard in scope which are not used in `cfg`
242
- * are disjoint from any classes extending BarrierGuard in scope which are used
243
- * in `cfg`.
245
+ * This is expected to be used in `isBarrier`/`isSanitizer` definitions
246
+ * in data flow and taint tracking.
244
247
*/
245
- abstract class BarrierGuard extends Node {
246
- /** Holds if this guard validates `e` upon evaluating to `branch`. */
247
- abstract predicate checks ( Expr e , boolean branch ) ;
248
+ module BarrierGuard< guardChecksSig / 3 guardChecks> {
249
+ /** Gets a node that is safely guarded by the given guard check. */
250
+ Node getABarrierNode ( ) {
251
+ exists ( Node g , ControlFlow:: ConditionGuardNode guard , Node nd , SsaWithFields var |
252
+ result = var .getAUse ( )
253
+ |
254
+ guards ( g , guard , nd , var ) and
255
+ guard .dominates ( result .getBasicBlock ( ) )
256
+ )
257
+ }
248
258
249
- /** Gets a node guarded by this guard. */
250
- final Node getAGuardedNode ( ) {
259
+ /**
260
+ * Gets a node that is safely guarded by the given guard check.
261
+ */
262
+ Node getABarrierNodeForGuard ( Node guardCheck ) {
251
263
exists ( ControlFlow:: ConditionGuardNode guard , Node nd , SsaWithFields var |
252
264
result = var .getAUse ( )
253
265
|
254
- this . guards ( guard , nd , var ) and
266
+ guards ( guardCheck , guard , nd , var ) and
255
267
guard .dominates ( result .getBasicBlock ( ) )
256
268
)
257
269
}
@@ -263,36 +275,36 @@ abstract class BarrierGuard extends Node {
263
275
* This predicate exists to enforce a good join order in `getAGuardedNode`.
264
276
*/
265
277
pragma [ noinline]
266
- private predicate guards ( ControlFlow:: ConditionGuardNode guard , Node nd , SsaWithFields ap ) {
267
- this . guards ( guard , nd ) and nd = ap .getAUse ( )
278
+ private predicate guards ( Node g , ControlFlow:: ConditionGuardNode guard , Node nd , SsaWithFields ap ) {
279
+ guards ( g , guard , nd ) and nd = ap .getAUse ( )
268
280
}
269
281
270
282
/**
271
283
* Holds if `guard` markes a point in the control-flow graph where this node
272
284
* is known to validate `nd`.
273
285
*/
274
- private predicate guards ( ControlFlow:: ConditionGuardNode guard , Node nd ) {
286
+ private predicate guards ( Node g , ControlFlow:: ConditionGuardNode guard , Node nd ) {
275
287
exists ( boolean branch |
276
- this . checks ( nd .asExpr ( ) , branch ) and
277
- guard .ensures ( this , branch )
288
+ guardChecks ( g , nd .asExpr ( ) , branch ) and
289
+ guard .ensures ( g , branch )
278
290
)
279
291
or
280
292
exists (
281
293
Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , CallNode c ,
282
294
Node resNode , Node check , boolean outcome
283
295
|
284
- this . guardingCall ( f , inp , outp , p , c , nd , resNode ) and
296
+ guardingCall ( g , f , inp , outp , p , c , nd , resNode ) and
285
297
p .checkOn ( check , outcome , resNode ) and
286
298
guard .ensures ( pragma [ only_bind_into ] ( check ) , outcome )
287
299
)
288
300
}
289
301
290
302
pragma [ noinline]
291
303
private predicate guardingCall (
292
- Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , CallNode c , Node nd ,
293
- Node resNode
304
+ Node g , Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , CallNode c ,
305
+ Node nd , Node resNode
294
306
) {
295
- this . guardingFunction ( f , inp , outp , p ) and
307
+ guardingFunction ( g , f , inp , outp , p ) and
296
308
c = f .getACall ( ) and
297
309
nd = inp .getNode ( c ) and
298
310
localFlow ( pragma [ only_bind_out ] ( outp .getNode ( c ) ) , resNode )
@@ -308,7 +320,7 @@ abstract class BarrierGuard extends Node {
308
320
* `false`, `nil` or a non-`nil` value.)
309
321
*/
310
322
private predicate guardingFunction (
311
- Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p
323
+ Node g , Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p
312
324
) {
313
325
exists ( FuncDecl fd , Node arg , Node ret |
314
326
fd .getFunction ( ) = f and
@@ -317,7 +329,7 @@ abstract class BarrierGuard extends Node {
317
329
(
318
330
// Case: a function like "if someBarrierGuard(arg) { return true } else { return false }"
319
331
exists ( ControlFlow:: ConditionGuardNode guard |
320
- this . guards ( guard , arg ) and
332
+ guards ( g , guard , arg ) and
321
333
guard .dominates ( ret .getBasicBlock ( ) )
322
334
|
323
335
exists ( boolean b |
@@ -336,12 +348,12 @@ abstract class BarrierGuard extends Node {
336
348
// or "return !someBarrierGuard(arg) && otherCond(...)"
337
349
exists ( boolean outcome |
338
350
ret = getUniqueOutputNode ( fd , outp ) and
339
- this . checks ( arg .asExpr ( ) , outcome ) and
351
+ guardChecks ( g , arg .asExpr ( ) , outcome ) and
340
352
// This predicate's contract is (p holds of ret ==> arg is checked),
341
353
// (and we have (this has outcome ==> arg is checked))
342
354
// but p.checkOn(ret, outcome, this) gives us (ret has outcome ==> p holds of this),
343
355
// so we need to swap outcome and (specifically boolean) p:
344
- DataFlow:: booleanProperty ( outcome ) .checkOn ( ret , p .asBoolean ( ) , this )
356
+ DataFlow:: booleanProperty ( outcome ) .checkOn ( ret , p .asBoolean ( ) , g )
345
357
)
346
358
or
347
359
// Case: a function like "return guardProxy(arg)"
@@ -351,7 +363,7 @@ abstract class BarrierGuard extends Node {
351
363
DataFlow:: Property outpProp
352
364
|
353
365
ret = getUniqueOutputNode ( fd , outp ) and
354
- this . guardingFunction ( f2 , inp2 , outp2 , outpProp ) and
366
+ guardingFunction ( g , f2 , inp2 , outp2 , outpProp ) and
355
367
c = f2 .getACall ( ) and
356
368
arg = inp2 .getNode ( c ) and
357
369
(
@@ -368,6 +380,34 @@ abstract class BarrierGuard extends Node {
368
380
}
369
381
}
370
382
383
+ /**
384
+ * DEPRECATED: Use `BarrierGuard` module instead.
385
+ *
386
+ * A guard that validates some expression.
387
+ *
388
+ * To use this in a configuration, extend the class and provide a
389
+ * characteristic predicate precisely specifying the guard, and override
390
+ * `checks` to specify what is being validated and in which branch.
391
+ *
392
+ * When using a data-flow or taint-flow configuration `cfg`, it is important
393
+ * that any classes extending BarrierGuard in scope which are not used in `cfg`
394
+ * are disjoint from any classes extending BarrierGuard in scope which are used
395
+ * in `cfg`.
396
+ */
397
+ abstract deprecated class BarrierGuard extends Node {
398
+ /** Holds if this guard validates `e` upon evaluating to `branch`. */
399
+ abstract predicate checks ( Expr e , boolean branch ) ;
400
+
401
+ /** Gets a node guarded by this guard. */
402
+ final Node getAGuardedNode ( ) {
403
+ result = BarrierGuard< barrierGuardChecks / 3 > :: getABarrierNodeForGuard ( this )
404
+ }
405
+ }
406
+
407
+ deprecated private predicate barrierGuardChecks ( Node g , Expr e , boolean branch ) {
408
+ g .( BarrierGuard ) .checks ( e , branch )
409
+ }
410
+
371
411
DataFlow:: Node getUniqueOutputNode ( FuncDecl fd , FunctionOutput outp ) {
372
412
result = unique( DataFlow:: Node n | n = outp .getEntryNode ( fd ) | n )
373
413
}
0 commit comments