@@ -68,14 +68,14 @@ import ReDoSUtil
68
68
* Holds if state `s` might be inside a backtracking repetition.
69
69
*/
70
70
pragma [ noinline]
71
- predicate stateInsideBacktracking ( State s ) {
71
+ private predicate stateInsideBacktracking ( State s ) {
72
72
s .getRepr ( ) .getParent * ( ) instanceof MaybeBacktrackingRepetition
73
73
}
74
74
75
75
/**
76
76
* A infinitely repeating quantifier that might backtrack.
77
77
*/
78
- class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier {
78
+ private class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier {
79
79
MaybeBacktrackingRepetition ( ) {
80
80
exists ( RegExpTerm child |
81
81
child instanceof RegExpAlt or
@@ -89,7 +89,7 @@ class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier {
89
89
/**
90
90
* A state in the product automaton.
91
91
*/
92
- newtype TStatePair =
92
+ private newtype TStatePair =
93
93
/**
94
94
* We lazily only construct those states that we are actually
95
95
* going to need: `(q, q)` for every fork state `q`, and any
@@ -112,7 +112,7 @@ newtype TStatePair =
112
112
* Gets a unique number for a `state`.
113
113
* Is used to create an ordering of states, where states with the same `toString()` will be ordered differently.
114
114
*/
115
- int rankState ( State state ) {
115
+ private int rankState ( State state ) {
116
116
state =
117
117
rank [ result ] ( State s , Location l |
118
118
l = s .getRepr ( ) .getLocation ( )
@@ -124,7 +124,7 @@ int rankState(State state) {
124
124
/**
125
125
* A state in the product automaton.
126
126
*/
127
- class StatePair extends TStatePair {
127
+ private class StatePair extends TStatePair {
128
128
State q1 ;
129
129
State q2 ;
130
130
@@ -145,21 +145,21 @@ class StatePair extends TStatePair {
145
145
*
146
146
* Used in `statePairDist`
147
147
*/
148
- predicate isStatePair ( StatePair p ) { any ( ) }
148
+ private predicate isStatePair ( StatePair p ) { any ( ) }
149
149
150
150
/**
151
151
* Holds if there are transitions from the components of `q` to the corresponding
152
152
* components of `r`.
153
153
*
154
154
* Used in `statePairDist`
155
155
*/
156
- predicate delta2 ( StatePair q , StatePair r ) { step ( q , _, _, r ) }
156
+ private predicate delta2 ( StatePair q , StatePair r ) { step ( q , _, _, r ) }
157
157
158
158
/**
159
159
* Gets the minimum length of a path from `q` to `r` in the
160
160
* product automaton.
161
161
*/
162
- int statePairDist ( StatePair q , StatePair r ) =
162
+ private int statePairDist ( StatePair q , StatePair r ) =
163
163
shortestDistances( isStatePair / 1 , delta2 / 2 ) ( q , r , result )
164
164
165
165
/**
@@ -172,7 +172,7 @@ int statePairDist(StatePair q, StatePair r) =
172
172
* expression cannot be vulnerable to ReDoS attacks anyway).
173
173
*/
174
174
pragma [ noopt]
175
- predicate isFork ( State q , InputSymbol s1 , InputSymbol s2 , State r1 , State r2 ) {
175
+ private predicate isFork ( State q , InputSymbol s1 , InputSymbol s2 , State r1 , State r2 ) {
176
176
stateInsideBacktracking ( q ) and
177
177
exists ( State q1 , State q2 |
178
178
q1 = epsilonSucc * ( q ) and
@@ -222,15 +222,15 @@ predicate isFork(State q, InputSymbol s1, InputSymbol s2, State r1, State r2) {
222
222
* Gets the state pair `(q1, q2)` or `(q2, q1)`; note that only
223
223
* one or the other is defined.
224
224
*/
225
- StatePair mkStatePair ( State q1 , State q2 ) {
225
+ private StatePair mkStatePair ( State q1 , State q2 ) {
226
226
result = MkStatePair ( q1 , q2 ) or result = MkStatePair ( q2 , q1 )
227
227
}
228
228
229
229
/**
230
230
* Holds if there are transitions from the components of `q` to the corresponding
231
231
* components of `r` labelled with `s1` and `s2`, respectively.
232
232
*/
233
- predicate step ( StatePair q , InputSymbol s1 , InputSymbol s2 , StatePair r ) {
233
+ private predicate step ( StatePair q , InputSymbol s1 , InputSymbol s2 , StatePair r ) {
234
234
exists ( State r1 , State r2 | step ( q , s1 , s2 , r1 , r2 ) and r = mkStatePair ( r1 , r2 ) )
235
235
}
236
236
@@ -242,7 +242,7 @@ predicate step(StatePair q, InputSymbol s1, InputSymbol s2, StatePair r) {
242
242
* inside a repetition that might backtrack.
243
243
*/
244
244
pragma [ noopt]
245
- predicate step ( StatePair q , InputSymbol s1 , InputSymbol s2 , State r1 , State r2 ) {
245
+ private predicate step ( StatePair q , InputSymbol s1 , InputSymbol s2 , State r1 , State r2 ) {
246
246
exists ( State q1 , State q2 | q .getLeft ( ) = q1 and q .getRight ( ) = q2 |
247
247
deltaClosed ( q1 , s1 , r1 ) and
248
248
deltaClosed ( q2 , s2 , r2 ) and
@@ -268,7 +268,7 @@ private newtype TTrace =
268
268
* A list of pairs of input symbols that describe a path in the product automaton
269
269
* starting from some fork state.
270
270
*/
271
- class Trace extends TTrace {
271
+ private class Trace extends TTrace {
272
272
/** Gets a textual representation of this element. */
273
273
string toString ( ) {
274
274
this = Nil ( ) and result = "Nil()"
@@ -282,7 +282,7 @@ class Trace extends TTrace {
282
282
/**
283
283
* Gets a string corresponding to the trace `t`.
284
284
*/
285
- string concretise ( Trace t ) {
285
+ private string concretise ( Trace t ) {
286
286
t = Nil ( ) and result = ""
287
287
or
288
288
exists ( InputSymbol s1 , InputSymbol s2 , Trace rest | t = Step ( s1 , s2 , rest ) |
@@ -294,7 +294,7 @@ string concretise(Trace t) {
294
294
* Holds if `r` is reachable from `(fork, fork)` under input `w`, and there is
295
295
* a path from `r` back to `(fork, fork)` with `rem` steps.
296
296
*/
297
- predicate isReachableFromFork ( State fork , StatePair r , Trace w , int rem ) {
297
+ private predicate isReachableFromFork ( State fork , StatePair r , Trace w , int rem ) {
298
298
// base case
299
299
exists ( InputSymbol s1 , InputSymbol s2 , State q1 , State q2 |
300
300
isFork ( fork , s1 , s2 , q1 , q2 ) and
@@ -316,15 +316,15 @@ predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
316
316
* Gets a state in the product automaton from which `(fork, fork)` is
317
317
* reachable in zero or more epsilon transitions.
318
318
*/
319
- StatePair getAForkPair ( State fork ) {
319
+ private StatePair getAForkPair ( State fork ) {
320
320
isFork ( fork , _, _, _, _) and
321
321
result = MkStatePair ( epsilonPred * ( fork ) , epsilonPred * ( fork ) )
322
322
}
323
323
324
324
/**
325
325
* Holds if `fork` is a pumpable fork with word `w`.
326
326
*/
327
- predicate isPumpable ( State fork , string w ) {
327
+ private predicate isPumpable ( State fork , string w ) {
328
328
exists ( StatePair q , Trace t |
329
329
isReachableFromFork ( fork , q , t , _) and
330
330
q = getAForkPair ( fork ) and
0 commit comments