@@ -5,6 +5,7 @@ overlay[local?]
55module ;
66
77private import go
8+ private import semmle.go.controlflow.Guards
89private import semmle.go.dataflow.FunctionInputsAndOutputs
910private import semmle.go.dataflow.ExternalFlow
1011private import DataFlowPrivate
@@ -355,27 +356,65 @@ private module WithParam<ParamSig P> {
355356 signature predicate guardChecksSig ( Node g , Expr e , boolean branch , P param ) ;
356357}
357358
359+ /**
360+ * Holds if the guard `g` validates the expression `e` upon evaluating to `value`.
361+ *
362+ * The expression `e` is expected to be a syntactic part of the guard `g`.
363+ */
364+ signature predicate valueGuardChecksSig ( Guard g , Expr e , GuardValue value ) ;
365+
366+ bindingset [ this ]
367+ private signature class ValueParamSig ;
368+
369+ private module WithValueParam< ValueParamSig P> {
370+ /**
371+ * Holds if the guard `g` validates the expression `e` upon evaluating to `value`.
372+ *
373+ * The expression `e` is expected to be a syntactic part of the guard `g`.
374+ */
375+ signature predicate guardChecksSig ( Guard g , Expr e , GuardValue value , P param ) ;
376+ }
377+
378+ /**
379+ * Provides a set of barrier nodes for a guard that validates an expression.
380+ */
381+ module BarrierGuardValue< valueGuardChecksSig / 3 guardChecks> {
382+ private predicate guardChecksWithParam ( Guard g , Expr e , GuardValue value , Unit param ) {
383+ guardChecks ( g , e , value ) and exists ( param )
384+ }
385+
386+ private module B = ParameterizedBarrierGuardValue< Unit , guardChecksWithParam / 4 > ;
387+
388+ /** Gets a node that is safely guarded by the given guard check. */
389+ Node getABarrierNode ( ) { result = B:: getABarrierNode ( _) }
390+ }
391+
358392/**
359393 * Provides a set of barrier nodes for a guard that validates an expression.
360394 *
361395 * This is expected to be used in `isBarrier`/`isSanitizer` definitions
362396 * in data flow and taint tracking.
363397 */
364398module BarrierGuard< guardChecksSig / 3 guardChecks> {
365- private predicate guardChecks ( Node g , Expr e , boolean branch , Unit param ) {
366- guardChecks ( g , e , branch ) and exists ( param )
399+ private predicate guardChecksValue ( Guard g , Expr e , GuardValue value ) {
400+ guardChecks ( DataFlow :: exprNode ( g ) , e , value . asBooleanValue ( ) )
367401 }
368402
369- private module B = ParameterizedBarrierGuard < Unit , guardChecks / 4 > ;
403+ private module B = BarrierGuardValue < guardChecksValue / 3 > ;
370404
371405 /** Gets a node that is safely guarded by the given guard check. */
372- Node getABarrierNode ( ) { result = B:: getABarrierNode ( _ ) }
406+ Node getABarrierNode ( ) { result = B:: getABarrierNode ( ) }
373407
374408 /**
375409 * Gets a node that is safely guarded by the given guard check.
376410 */
377411 Node getABarrierNodeForGuard ( Node guardCheck ) {
378- result = B:: getABarrierNodeForGuard ( guardCheck , _)
412+ result =
413+ ParameterizedBarrierGuard< Unit , guardChecksWithParam / 4 > :: getABarrierNodeForGuard ( guardCheck , _)
414+ }
415+
416+ private predicate guardChecksWithParam ( Node g , Expr e , boolean branch , Unit param ) {
417+ guardChecks ( g , e , branch ) and exists ( param )
379418 }
380419}
381420
@@ -385,148 +424,70 @@ module BarrierGuard<guardChecksSig/3 guardChecks> {
385424 * This is expected to be used in `isBarrier`/`isSanitizer` definitions
386425 * in data flow and taint tracking.
387426 */
388- module ParameterizedBarrierGuard< ParamSig P, WithParam< P > :: guardChecksSig / 4 guardChecks> {
427+ module ParameterizedBarrierGuardValue<
428+ ValueParamSig P, WithValueParam< P > :: guardChecksSig / 4 guardChecks>
429+ {
430+ private module WrappedGuardChecks = ParameterizedValidationWrapper< P , guardChecks / 4 > ;
431+
389432 /** Gets a node that is safely guarded by the given guard check. */
390433 Node getABarrierNode ( P param ) {
391- exists ( ControlFlow :: ConditionGuardNode guard , SsaWithFields var |
434+ exists ( Guard guard , GuardValue value , SsaWithFields var |
392435 result = pragma [ only_bind_out ] ( var ) .getAUse ( )
393436 |
394- guards ( _, guard , _, var , param ) and
395- pragma [ only_bind_out ] ( guard ) .dominates ( result .getBasicBlock ( ) )
437+ guards ( _, guard , value , _, var , param ) and
438+ pragma [ only_bind_out ] ( guard ) .valueControls ( result .getBasicBlock ( ) , value )
396439 )
397440 }
398441
399442 /**
400443 * Gets a node that is safely guarded by the given guard check.
401444 */
402445 Node getABarrierNodeForGuard ( Node guardCheck , P param ) {
403- exists ( ControlFlow :: ConditionGuardNode guard , SsaWithFields var | result = var .getAUse ( ) |
404- guards ( guardCheck , guard , _, var , param ) and
405- guard .dominates ( result .getBasicBlock ( ) )
446+ exists ( Guard guard , GuardValue value , SsaWithFields var | result = var .getAUse ( ) |
447+ guards ( guardCheck , guard , value , _, var , param ) and
448+ guard .valueControls ( result .getBasicBlock ( ) , value )
406449 )
407450 }
408451
409452 /**
410- * Holds if `guard` marks a point in the control-flow graph where `g`
411- * is known to validate `nd`, which is represented by `ap`.
453+ * Holds if `guard` evaluating to `value` marks a point in the control-flow
454+ * graph where `g` is known to validate `nd`, which is represented by `ap`.
455+ * `param` is the caller-supplied parameter associated with that validation.
412456 *
413457 * This predicate exists to enforce a good join order in `getAGuardedNode`.
414458 */
415459 pragma [ noinline]
416- private predicate guards (
417- Node g , ControlFlow:: ConditionGuardNode guard , Node nd , SsaWithFields ap , P param
418- ) {
419- guards ( g , guard , nd , param ) and nd = ap .getAUse ( )
460+ private predicate guards ( Node g , Guard guard , GuardValue value , Node nd , SsaWithFields ap , P param ) {
461+ guards ( g , guard , value , nd , param ) and nd = ap .getAUse ( )
420462 }
421463
422464 /**
423- * Holds if `guard` marks a point in the control-flow graph where `g`
424- * is known to validate `nd`.
465+ * Holds if `guard` evaluating to `value` marks a point in the control-flow
466+ * graph where `g` is known to validate `nd`. `param` is the caller-supplied
467+ * parameter associated with that validation.
425468 */
426- private predicate guards ( Node g , ControlFlow:: ConditionGuardNode guard , Node nd , P param ) {
427- exists ( boolean branch |
428- guardChecks ( g , nd .asExpr ( ) , branch , param ) and
429- guard .ensures ( g , branch )
430- )
431- or
432- exists ( DataFlow:: Property p , Node resNode , Node check , boolean outcome |
433- guardingCall ( g , _, _, _, p , _, nd , resNode , param ) and
434- p .checkOn ( check , outcome , resNode ) and
435- guard .ensures ( pragma [ only_bind_into ] ( check ) , outcome )
436- )
469+ private predicate guards ( Node g , Guard guard , GuardValue value , Node nd , P param ) {
470+ WrappedGuardChecks:: guardChecks ( guard , nd .asExpr ( ) , value , param ) and
471+ g = DataFlow:: exprNode ( guard )
437472 }
473+ }
438474
439- bindingset [ inp, c]
440- pragma [ inline_late]
441- private Node getInputNode ( FunctionInput inp , CallNode c ) { result = inp .getNode ( c ) }
442-
443- bindingset [ outp, c]
444- pragma [ inline_late]
445- private Node getOutputNode ( FunctionOutput outp , CallNode c ) { result = outp .getNode ( c ) }
446-
447- pragma [ noinline]
448- private predicate guardingCall (
449- Node g , Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , CallNode c ,
450- Node nd , Node resNode , P param
451- ) {
452- guardingFunction ( g , f , inp , outp , p , param ) and
453- c = f .getACall ( ) and
454- nd = getInputNode ( inp , c ) and
455- localFlow ( getOutputNode ( outp , c ) , resNode )
475+ /**
476+ * Provides a set of barrier nodes for a Boolean guard that validates an expression.
477+ */
478+ module ParameterizedBarrierGuard< ParamSig P, WithParam< P > :: guardChecksSig / 4 guardChecks> {
479+ private predicate guardChecksValue ( Guard g , Expr e , GuardValue value , P param ) {
480+ guardChecks ( DataFlow:: exprNode ( g ) , e , value .asBooleanValue ( ) , param )
456481 }
457482
458- private predicate onlyPossibleReturnSatisfyingProperty (
459- FuncDecl fd , FunctionOutput outp , Node ret , DataFlow:: Property p
460- ) {
461- exists ( boolean b |
462- onlyPossibleReturnOfBool ( fd , outp , ret , b ) and
463- p .isBoolean ( b )
464- )
465- or
466- onlyPossibleReturnOfNonNil ( fd , outp , ret ) and
467- p .isNonNil ( )
468- or
469- onlyPossibleReturnOfNil ( fd , outp , ret ) and
470- p .isNil ( )
471- }
483+ private module B = ParameterizedBarrierGuardValue< P , guardChecksValue / 4 > ;
472484
473- /**
474- * Holds if whenever `p` holds of output `outp` of function `f`, this node
475- * is known to validate the input `inp` of `f`.
476- *
477- * We check this by looking for guards on `inp` that dominate a `return` statement that
478- * is the only `return` in `f` that can return `true`. This means that if `f` returns `true`,
479- * the guard must have been satisfied. (Similar reasoning is applied for statements returning
480- * `false`, `nil` or a non-`nil` value.)
481- */
482- private predicate guardingFunction (
483- Node g , Function f , FunctionInput inp , FunctionOutput outp , DataFlow:: Property p , P param
484- ) {
485- exists ( FuncDecl fd , Node arg , Node ret |
486- fd .getFunction ( ) = f and
487- localFlow ( inp .getExitNode ( fd ) , pragma [ only_bind_out ] ( arg ) ) and
488- (
489- // Case: a function like "if someBarrierGuard(arg) { return true } else { return false }"
490- exists ( ControlFlow:: ConditionGuardNode guard |
491- guards ( g , pragma [ only_bind_out ] ( guard ) , arg , param ) and
492- guard .dominates ( pragma [ only_bind_out ] ( ret ) .getBasicBlock ( ) )
493- |
494- onlyPossibleReturnSatisfyingProperty ( fd , outp , ret , p )
495- )
496- or
497- // Case: a function like "return someBarrierGuard(arg)"
498- // or "return !someBarrierGuard(arg) && otherCond(...)"
499- exists ( boolean outcome |
500- ret = getUniqueOutputNode ( fd , outp ) and
501- guardChecks ( g , arg .asExpr ( ) , outcome , param ) and
502- // This predicate's contract is (p holds of ret ==> arg is checked),
503- // (and we have (this has outcome ==> arg is checked))
504- // but p.checkOn(ret, outcome, this) gives us (ret has outcome ==> p holds of this),
505- // so we need to swap outcome and (specifically boolean) p:
506- DataFlow:: booleanProperty ( outcome ) .checkOn ( ret , p .asBoolean ( ) , g )
507- )
508- or
509- // Case: a function like "return guardProxy(arg)"
510- // or "return !guardProxy(arg) || otherCond(...)"
511- exists (
512- Function f2 , FunctionInput inp2 , FunctionOutput outp2 , CallNode c ,
513- DataFlow:: Property outpProp
514- |
515- ret = getUniqueOutputNode ( fd , outp ) and
516- guardingFunction ( g , f2 , inp2 , outp2 , outpProp , param ) and
517- c = f2 .getACall ( ) and
518- arg = inp2 .getNode ( c ) and
519- (
520- // See comment above ("This method's contract...") for rationale re: the inversion of
521- // `p` and `outpProp` here:
522- outpProp .checkOn ( ret , p .asBoolean ( ) , outp2 .getNode ( c ) )
523- or
524- // The particular case where p is non-boolean (i.e., nil or non-nil), and we directly return `c`:
525- outpProp = p and ret = outp2 .getNode ( c )
526- )
527- )
528- )
529- )
485+ /** Gets a node that is safely guarded by the given guard check. */
486+ Node getABarrierNode ( P param ) { result = B:: getABarrierNode ( param ) }
487+
488+ /** Gets a node that is safely guarded by the given guard check. */
489+ Node getABarrierNodeForGuard ( Node guardCheck , P param ) {
490+ result = B:: getABarrierNodeForGuard ( guardCheck , param )
530491 }
531492}
532493
@@ -544,18 +505,6 @@ predicate possiblyReturnsBool(FuncDecl fd, FunctionOutput res, Node ret, Boolean
544505 not ret .getBoolValue ( ) != b
545506}
546507
547- /**
548- * Holds if `ret` is the only data-flow node whose value contributes to the output `res` of `fd`
549- * that may have Boolean value `b`, since all the other output nodes have a Boolean value
550- * other than `b`.
551- */
552- private predicate onlyPossibleReturnOfBool ( FuncDecl fd , FunctionOutput res , Node ret , boolean b ) {
553- possiblyReturnsBool ( fd , res , ret , b ) and
554- forall ( Node otherRet | otherRet = res .getEntryNode ( fd ) and otherRet != ret |
555- otherRet .getBoolValue ( ) != b
556- )
557- }
558-
559508/**
560509 * Holds if `ret` is a data-flow node whose value contributes to the output `res` of `fd`,
561510 * and that node may evaluate to a value other than `nil`.
@@ -565,21 +514,10 @@ predicate possiblyReturnsNonNil(FuncDecl fd, FunctionOutput res, Node ret) {
565514 not exprRefersToNil ( ret .asExpr ( ) )
566515}
567516
568- /**
569- * Holds if `ret` is the only data-flow node whose value contributes to the output `res` of `fd`
570- * that may have a value other than `nil`, since all the other output nodes evaluate to `nil`.
571- */
572- private predicate onlyPossibleReturnOfNonNil ( FuncDecl fd , FunctionOutput res , Node ret ) {
573- possiblyReturnsNonNil ( fd , res , ret ) and
574- forall ( Node otherRet | otherRet = res .getEntryNode ( fd ) and otherRet != ret |
575- exprRefersToNil ( otherRet .asExpr ( ) )
576- )
577- }
578-
579517/**
580518 * Holds if function `f`'s result `output`, which must be a return value, cannot be nil.
581519 */
582- private predicate certainlyReturnsNonNil ( Function f , FunctionOutput output ) {
520+ predicate certainlyReturnsNonNil ( Function f , FunctionOutput output ) {
583521 output .isResult ( _) and
584522 (
585523 f .hasQualifiedName ( "errors" , "New" )
@@ -597,22 +535,10 @@ private predicate certainlyReturnsNonNil(Function f, FunctionOutput output) {
597535/**
598536 * Holds if `node` cannot be `nil`.
599537 */
600- private predicate isCertainlyNotNil ( DataFlow:: Node node ) {
538+ predicate isCertainlyNotNil ( DataFlow:: Node node ) {
601539 node instanceof DataFlow:: AddressOperationNode
602540 or
603541 exists ( DataFlow:: CallNode c , FunctionOutput output | output .getExitNode ( c ) = node |
604542 certainlyReturnsNonNil ( c .getTarget ( ) , output )
605543 )
606544}
607-
608- /**
609- * Holds if `ret` is the only data-flow node whose value contributes to the output `res` of `fd`
610- * that returns `nil`, since all the other output nodes are known to be non-nil.
611- */
612- private predicate onlyPossibleReturnOfNil ( FuncDecl fd , FunctionOutput res , DataFlow:: Node ret ) {
613- ret = res .getEntryNode ( fd ) and
614- exprRefersToNil ( ret .asExpr ( ) ) and
615- forall ( DataFlow:: Node otherRet | otherRet = res .getEntryNode ( fd ) and otherRet != ret |
616- isCertainlyNotNil ( otherRet )
617- )
618- }
0 commit comments