@@ -750,6 +750,27 @@ module Private {
750750 )
751751 }
752752
753+ /**
754+ * Holds if `p` can reach `n` in a summarized callable, using only value-preserving
755+ * local steps. `clearsOrExpects` records whether any node on the path from `p` to
756+ * `n` either clears or expects contents.
757+ */
758+ private predicate paramReachesLocal ( ParamNode p , Node n , boolean clearsOrExpects ) {
759+ viableParam ( _, _, _, p ) and
760+ n = p and
761+ clearsOrExpects = false
762+ or
763+ exists ( Node mid , boolean clearsOrExpectsMid |
764+ paramReachesLocal ( p , mid , clearsOrExpectsMid ) and
765+ summaryLocalStep ( mid , n , true ) and
766+ if
767+ summaryClearsContent ( n , _) or
768+ summaryExpectsContent ( n , _)
769+ then clearsOrExpects = true
770+ else clearsOrExpects = clearsOrExpectsMid
771+ )
772+ }
773+
753774 /**
754775 * Holds if use-use flow starting from `arg` should be prohibited.
755776 *
@@ -759,15 +780,11 @@ module Private {
759780 */
760781 pragma [ nomagic]
761782 predicate prohibitsUseUseFlow ( ArgNode arg , SummarizedCallable sc ) {
762- exists ( ParamNode p , Node mid , ParameterPosition ppos , Node ret |
783+ exists ( ParamNode p , ParameterPosition ppos , Node ret |
784+ paramReachesLocal ( p , ret , true ) and
763785 p = summaryArgParam0 ( _, arg , sc ) and
764786 p .isParameterOf ( _, pragma [ only_bind_into ] ( ppos ) ) and
765- summaryLocalStep ( p , mid , true ) and
766- summaryLocalStep ( mid , ret , true ) and
767787 isParameterPostUpdate ( ret , _, pragma [ only_bind_into ] ( ppos ) )
768- |
769- summaryClearsContent ( mid , _) or
770- summaryExpectsContent ( mid , _)
771788 )
772789 }
773790
0 commit comments