@@ -887,11 +887,10 @@ module PrefixConstruction<isCandidateSig/1 isCandidate> {
887887 /**
888888 * Holds if `state` is the textually last start state for the regular expression.
889889 */
890- private predicate lastStartState ( State state ) {
890+ private predicate lastStartState ( RelevantState state ) {
891891 exists ( RegExpRoot root |
892892 state =
893- max ( State s , Location l |
894- s = stateInRelevantRegexp ( ) and
893+ max ( RelevantState s , Location l |
895894 isStartState ( s ) and
896895 getRoot ( s .getRepr ( ) ) = root and
897896 l = s .getRepr ( ) .getLocation ( )
@@ -963,10 +962,17 @@ module PrefixConstruction<isCandidateSig/1 isCandidate> {
963962 min ( string c | delta ( prev , any ( InputSymbol symbol | c = intersect ( Any ( ) , symbol ) ) , next ) )
964963 }
965964
966- /** Gets a state within a regular expression that contains a candidate state. */
967- pragma [ noinline]
968- State stateInRelevantRegexp ( ) {
969- exists ( State s | isCandidate ( s ) | getRoot ( s .getRepr ( ) ) = getRoot ( result .getRepr ( ) ) )
965+ /** A state within a regular expression that contains a candidate state. */
966+ class RelevantState instanceof State {
967+ RelevantState ( ) {
968+ exists ( State s | isCandidate ( s ) | getRoot ( s .getRepr ( ) ) = getRoot ( this .getRepr ( ) ) )
969+ }
970+
971+ /** Gets a string representation for this state in a regular expression. */
972+ string toString ( ) { result = State .super .toString ( ) }
973+
974+ /** Gets the term represented by this state. */
975+ RegExpTerm getRepr ( ) { result = State .super .getRepr ( ) }
970976 }
971977}
972978
@@ -1007,6 +1013,8 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
10071013
10081014 import PrefixConstruction< isCandidateState / 1 > as Prefix
10091015
1016+ class RelevantState = Prefix:: RelevantState ;
1017+
10101018 /**
10111019 * Predicates for testing the presence of a rejecting suffix.
10121020 *
@@ -1040,32 +1048,26 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
10401048 * This predicate might find impossible suffixes when searching for suffixes of length > 1, which can cause FPs.
10411049 */
10421050 pragma [ noinline]
1043- private predicate isLikelyRejectable ( State s ) {
1044- s = Prefix:: stateInRelevantRegexp ( ) and
1045- (
1046- // exists a reject edge with some char.
1047- hasRejectEdge ( s )
1048- or
1049- hasEdgeToLikelyRejectable ( s )
1050- or
1051- // stopping here is rejection
1052- isRejectState ( s )
1053- )
1051+ private predicate isLikelyRejectable ( RelevantState s ) {
1052+ // exists a reject edge with some char.
1053+ hasRejectEdge ( s )
1054+ or
1055+ hasEdgeToLikelyRejectable ( s )
1056+ or
1057+ // stopping here is rejection
1058+ isRejectState ( s )
10541059 }
10551060
10561061 /**
10571062 * Holds if `s` is not an accept state, and there is no epsilon transition to an accept state.
10581063 */
1059- predicate isRejectState ( State s ) {
1060- s = Prefix:: stateInRelevantRegexp ( ) and not epsilonSucc * ( s ) = Accept ( _)
1061- }
1064+ predicate isRejectState ( RelevantState s ) { not epsilonSucc * ( s ) = Accept ( _) }
10621065
10631066 /**
10641067 * Holds if there is likely a non-empty suffix leading to rejection starting in `s`.
10651068 */
10661069 pragma [ noopt]
1067- predicate hasEdgeToLikelyRejectable ( State s ) {
1068- s = Prefix:: stateInRelevantRegexp ( ) and
1070+ predicate hasEdgeToLikelyRejectable ( RelevantState s ) {
10691071 // all edges (at least one) with some char leads to another state that is rejectable.
10701072 // the `next` states might not share a common suffix, which can cause FPs.
10711073 exists ( string char | char = hasEdgeToLikelyRejectableHelper ( s ) |
@@ -1080,8 +1082,7 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
10801082 * and `s` has not been found to be rejectable by `hasRejectEdge` or `isRejectState`.
10811083 */
10821084 pragma [ noinline]
1083- private string hasEdgeToLikelyRejectableHelper ( State s ) {
1084- s = Prefix:: stateInRelevantRegexp ( ) and
1085+ private string hasEdgeToLikelyRejectableHelper ( RelevantState s ) {
10851086 not hasRejectEdge ( s ) and
10861087 not isRejectState ( s ) and
10871088 deltaClosedChar ( s , result , _)
@@ -1092,9 +1093,7 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
10921093 * along epsilon edges, such that there is a transition from
10931094 * `prev` to `next` that the character symbol `char`.
10941095 */
1095- predicate deltaClosedChar ( State prev , string char , State next ) {
1096- prev = Prefix:: stateInRelevantRegexp ( ) and
1097- next = Prefix:: stateInRelevantRegexp ( ) and
1096+ predicate deltaClosedChar ( RelevantState prev , string char , RelevantState next ) {
10981097 deltaClosed ( prev , getAnInputSymbolMatchingRelevant ( char ) , next )
10991098 }
11001099
0 commit comments