62
62
* a suffix `x` (possible empty) that is most likely __not__ accepted.
63
63
*/
64
64
65
- import ReDoSUtil
65
+ private import ReDoSUtil
66
66
67
67
/**
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
@@ -145,15 +145,15 @@ 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
@@ -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
@@ -230,7 +230,7 @@ StatePair mkStatePair(State q1, State q2) {
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
@@ -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
@@ -324,7 +324,7 @@ StatePair getAForkPair(State fork) {
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