@@ -55,23 +55,33 @@ DataFlow::Node stringSink() {
5555/** Gets a node where regular expressions that flow to the node are used. */
5656DataFlow:: Node regSink ( ) { result = any ( RegexExecution exec ) .getRegex ( ) }
5757
58- private signature module ReachInputSig {
59- DataFlow:: LocalSourceNode start ( TypeTracker t ) ;
58+ private signature module TypeTrackInputSig {
59+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow :: Node start ) ;
6060
61- DataFlow:: Node end ( ) ;
61+ predicate end ( DataFlow:: Node n ) ;
6262
63- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) ;
63+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) ;
6464}
6565
66- private module Reach< ReachInputSig Input> {
66+ /**
67+ * Provides a version of type tracking where we first prune for reachable nodes,
68+ * before doing the type tracking computation.
69+ */
70+ private module TypeTrack< TypeTrackInputSig Input> {
71+ private predicate additionalStep (
72+ DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo
73+ ) {
74+ Input:: additionalStep ( nodeFrom .getALocalUse ( ) , nodeTo )
75+ }
76+
6777 /** Gets a node that is forwards reachable by type-tracking. */
6878 pragma [ nomagic]
6979 private DataFlow:: LocalSourceNode forward ( TypeTracker t ) {
70- result = Input:: start ( t )
80+ result = Input:: start ( t , _ )
7181 or
7282 exists ( TypeTracker t2 | result = forward ( t2 ) .track ( t2 , t ) )
7383 or
74- exists ( TypeTracker t2 | t2 = t .continue ( ) | Input :: additionalStep ( forward ( t2 ) , result ) )
84+ exists ( TypeTracker t2 | t2 = t .continue ( ) | additionalStep ( forward ( t2 ) , result ) )
7585 }
7686
7787 bindingset [ result , tbt]
@@ -90,11 +100,11 @@ private module Reach<ReachInputSig Input> {
90100 result = forwardLateInline ( t ) and
91101 (
92102 t .start ( ) and
93- result . flowsTo ( Input:: end ( ) )
103+ Input:: end ( result . getALocalUse ( ) )
94104 or
95105 exists ( TypeBackTracker t2 | result = backwards ( t2 ) .backtrack ( t2 , t ) )
96106 or
97- exists ( TypeBackTracker t2 | t2 = t .continue ( ) | Input :: additionalStep ( result , backwards ( t2 ) ) )
107+ exists ( TypeBackTracker t2 | t2 = t .continue ( ) | additionalStep ( result , backwards ( t2 ) ) )
98108 )
99109 }
100110
@@ -110,13 +120,13 @@ private module Reach<ReachInputSig Input> {
110120
111121 /** Holds if `n` is forwards and backwards reachable with type tracker `t`. */
112122 pragma [ nomagic]
113- predicate reached ( DataFlow:: LocalSourceNode n , TypeTracker t ) {
123+ private predicate reached ( DataFlow:: LocalSourceNode n , TypeTracker t ) {
114124 n = forward ( t ) and
115125 n = backwardsInlineLate ( t )
116126 }
117127
118128 pragma [ nomagic]
119- TypeTracker stepReached (
129+ private TypeTracker stepReached (
120130 TypeTracker t , DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo
121131 ) {
122132 exists ( StepSummary summary |
@@ -126,11 +136,20 @@ private module Reach<ReachInputSig Input> {
126136 result = t .append ( summary )
127137 )
128138 or
129- Input :: additionalStep ( nodeFrom , nodeTo ) and
139+ additionalStep ( nodeFrom , nodeTo ) and
130140 reached ( nodeFrom , pragma [ only_bind_into ] ( t ) ) and
131141 reached ( nodeTo , pragma [ only_bind_into ] ( t ) ) and
132142 result = t .continue ( )
133143 }
144+
145+ /** Gets a node that has been tracked from the start node `start`. */
146+ DataFlow:: LocalSourceNode track ( DataFlow:: Node start , TypeTracker t ) {
147+ t .start ( ) and
148+ result = Input:: start ( t , start ) and
149+ reached ( result , t )
150+ or
151+ exists ( TypeTracker t2 | t = stepReached ( t2 , track ( start , t2 ) , result ) )
152+ }
134153}
135154
136155/** Holds if `inputStr` is compiled to a regular expression that is returned at `call`. */
@@ -143,47 +162,40 @@ private predicate regFromString(DataFlow::LocalSourceNode inputStr, DataFlow::Ca
143162 )
144163}
145164
146- private module StringReachInput implements ReachInputSig {
147- DataFlow:: LocalSourceNode start ( TypeTracker t ) { result = strStart ( ) and t .start ( ) }
165+ private module StringTypeTrackInput implements TypeTrackInputSig {
166+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow:: Node start ) {
167+ start = strStart ( ) and t .start ( ) and result = start
168+ }
148169
149- DataFlow:: Node end ( ) {
150- result = stringSink ( ) or
151- regFromString ( result , _)
170+ predicate end ( DataFlow:: Node n ) {
171+ n = stringSink ( ) or
172+ regFromString ( n , _)
152173 }
153174
154- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
155- exists ( DataFlow:: Node mid | nodeFrom .flowsTo ( mid ) |
156- // include taint flow through `String` summaries
157- TaintTrackingPrivate:: summaryThroughStepTaint ( mid , nodeTo , any ( String:: SummarizedCallable c ) )
158- or
159- // string concatenations, and
160- exists ( CfgNodes:: ExprNodes:: OperationCfgNode op |
161- op = nodeTo .asExpr ( ) and
162- op .getAnOperand ( ) = mid .asExpr ( ) and
163- op .getExpr ( ) .( Ast:: BinaryOperation ) .getOperator ( ) = "+"
164- )
165- or
166- // string interpolations
167- mid .asExpr ( ) = nodeTo .asExpr ( ) .( CfgNodes:: ExprNodes:: StringlikeLiteralCfgNode ) .getAComponent ( )
175+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
176+ // include taint flow through `String` summaries
177+ TaintTrackingPrivate:: summaryThroughStepTaint ( nodeFrom , nodeTo ,
178+ any ( String:: SummarizedCallable c ) )
179+ or
180+ // string concatenations, and
181+ exists ( CfgNodes:: ExprNodes:: OperationCfgNode op |
182+ op = nodeTo .asExpr ( ) and
183+ op .getAnOperand ( ) = nodeFrom .asExpr ( ) and
184+ op .getExpr ( ) .( Ast:: BinaryOperation ) .getOperator ( ) = "+"
168185 )
186+ or
187+ // string interpolations
188+ nodeFrom .asExpr ( ) =
189+ nodeTo .asExpr ( ) .( CfgNodes:: ExprNodes:: StringlikeLiteralCfgNode ) .getAComponent ( )
169190 }
170191}
171192
172- private module StringReach = Reach< StringReachInput > ;
173-
174193/**
175194 * Gets a node that has been tracked from the string constant `start` to some node.
176195 * This is used to figure out where `start` is evaluated as a regular expression against an input string,
177196 * or where `start` is compiled into a regular expression.
178197 */
179- private DataFlow:: LocalSourceNode trackStrings ( DataFlow:: Node start , TypeTracker t ) {
180- t .start ( ) and
181- start = result and
182- result = strStart ( ) and
183- StringReach:: reached ( result , t )
184- or
185- exists ( TypeTracker t2 | t = StringReach:: stepReached ( t2 , trackStrings ( start , t2 ) , result ) )
186- }
198+ private predicate trackStrings = TypeTrack< StringTypeTrackInput > :: track / 2 ;
187199
188200/** Holds if `strConst` flows to a regex compilation (tracked by `t`), where the resulting regular expression is stored in `reg`. */
189201pragma [ nomagic]
@@ -192,39 +204,25 @@ private predicate regFromStringStart(DataFlow::Node strConst, TypeTracker t, Dat
192204 exists ( t .continue ( ) )
193205}
194206
195- private module RegReachInput implements ReachInputSig {
196- DataFlow:: LocalSourceNode start ( TypeTracker t ) {
197- result = regStart ( ) and
198- t .start ( )
207+ private module RegTypeTrackInput implements TypeTrackInputSig {
208+ DataFlow:: LocalSourceNode start ( TypeTracker t , DataFlow:: Node start ) {
209+ start = regStart ( ) and
210+ t .start ( ) and
211+ result = start
199212 or
200- regFromStringStart ( _ , t , result )
213+ regFromStringStart ( start , t , result )
201214 }
202215
203- DataFlow:: Node end ( ) { result = regSink ( ) }
216+ predicate end ( DataFlow:: Node n ) { n = regSink ( ) }
204217
205- predicate additionalStep ( DataFlow:: LocalSourceNode nodeFrom , DataFlow:: LocalSourceNode nodeTo ) {
206- none ( )
207- }
218+ predicate additionalStep ( DataFlow:: Node nodeFrom , DataFlow:: LocalSourceNode nodeTo ) { none ( ) }
208219}
209220
210- private module RegReach = Reach< RegReachInput > ;
211-
212221/**
213222 * Gets a node that has been tracked from the regular expression `start` to some node.
214223 * This is used to figure out where `start` is executed against an input string.
215224 */
216- private DataFlow:: LocalSourceNode trackRegs ( DataFlow:: Node start , TypeTracker t ) {
217- RegReach:: reached ( result , t ) and
218- (
219- t .start ( ) and
220- start = result and
221- result = regStart ( )
222- or
223- regFromStringStart ( start , t , result )
224- )
225- or
226- exists ( TypeTracker t2 | t = RegReach:: stepReached ( t2 , trackRegs ( start , t2 ) , result ) )
227- }
225+ private predicate trackRegs = TypeTrack< RegTypeTrackInput > :: track / 2 ;
228226
229227/** Gets a node that references a regular expression. */
230228private DataFlow:: LocalSourceNode trackRegexpType ( TypeTracker t ) {
0 commit comments