@@ -381,6 +381,21 @@ module Make<
381381 abstract predicate isBarrier ( string output , string kind , Provenance provenance , string model ) ;
382382 }
383383
384+ /** A barrier guard element. */
385+ abstract class BarrierGuardElement extends SinkBaseFinal {
386+ bindingset [ this ]
387+ BarrierGuardElement ( ) { any ( ) }
388+
389+ /**
390+ * Holds if this element is a flow barrier guard of kind `kind`, for data
391+ * flowing in as described by `input`, when `this` evaluates to `branch`.
392+ */
393+ pragma [ nomagic]
394+ abstract predicate isBarrierGuard (
395+ string input , string branch , string kind , Provenance provenance , string model
396+ ) ;
397+ }
398+
384399 private signature predicate hasKindSig ( string kind ) ;
385400
386401 signature class NeutralCallableSig extends SummarizedCallableBaseFinal {
@@ -748,6 +763,19 @@ module Make<
748763 )
749764 }
750765
766+ private predicate isRelevantBarrierGuard (
767+ BarrierGuardElement e , string input , string branch , string kind , Provenance provenance ,
768+ string model
769+ ) {
770+ e .isBarrierGuard ( input , branch , kind , provenance , model ) and
771+ (
772+ provenance .isManual ( )
773+ or
774+ provenance .isGenerated ( ) and
775+ not exists ( Provenance p | p .isManual ( ) and e .isBarrierGuard ( _, _, kind , p , _) )
776+ )
777+ }
778+
751779 private predicate flowSpec ( string spec ) {
752780 exists ( SummarizedCallable c |
753781 c .propagatesFlow ( spec , _, _, _, _, _)
@@ -759,6 +787,8 @@ module Make<
759787 or
760788 isRelevantBarrier ( _, spec , _, _, _)
761789 or
790+ isRelevantBarrierGuard ( _, spec , _, _, _, _)
791+ or
762792 isRelevantSink ( _, spec , _, _, _)
763793 }
764794
@@ -1554,6 +1584,19 @@ module Make<
15541584 )
15551585 }
15561586
1587+ /**
1588+ * Holds if `barrierGuard` is a relevant barrier guard element with input specification `inSpec`.
1589+ */
1590+ predicate barrierSpec (
1591+ BarrierGuardElement barrierGuard , SummaryComponentStack inSpec , string branch , string kind ,
1592+ string model
1593+ ) {
1594+ exists ( string input |
1595+ isRelevantBarrierGuard ( barrierGuard , input , branch , kind , _, model ) and
1596+ External:: interpretSpec ( input , inSpec )
1597+ )
1598+ }
1599+
15571600 signature module TypesInputSig {
15581601 /** Gets the type of content `c`. */
15591602 DataFlowType getContentType ( ContentSet c ) ;
0 commit comments