hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-28 10:15:14 +02:00
Code Issues Packages Projects Releases Wiki Activity

rename succ to pumpEnd

Browse Source
This commit is contained in:
erik-krogh
2023-05-11 13:49:18 +02:00
parent 36147e7afc
commit efa53d21fa
1 changed files with 43 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files

86
shared/regex/codeql/regex/nfa/SuperlinearBackTracking.qll
View File

@@ -9,16 +9,16 @@
* Theorem 3 from the paper describes the basic idea.
*
* The following explains the idea using variables and predicate names that are used in the implementation:
* We consider a pair of repetitions, which we will call `pivot` and `succ`.
* We consider a pair of repetitions, which we will call `pivot` and `pumpEnd`.
*
* We create a product automaton of 3-tuples of states (see `StateTuple`).
* There exists a transition `(a,b,c) -> (d,e,f)` in the product automaton
* iff there exists three transitions in the NFA `a->d, b->e, c->f` where those three
* transitions all match a shared character `char`. (see `getAThreewayIntersect`)
*
* We start a search in the product automaton at `(pivot, pivot, succ)`,
* We start a search in the product automaton at `(pivot, pivot, pumpEnd)`,
* and search for a series of transitions (a `Trace`), such that we end
* at `(pivot, succ, succ)` (see `isReachableFromStartTuple`).
* at `(pivot, pumpEnd, pumpEnd)` (see `isReachableFromStartTuple`).
*
* For example, consider the regular expression `/^\d*5\w*$/`.
* The search will start at the tuple `(\d*, \d*, \w*)` and search
@@ -52,7 +52,7 @@ module Make<RegexTreeViewSig TreeImpl> {
private newtype TStateTuple =
MkStateTuple(State q1, State q2, State q3) {
// starts at (pivot, pivot, succ)
// starts at (pivot, pivot, pumpEnd)
isStartLoops(q1, q3) and q1 = q2
or
step(_, _, _, _, q1, q2, q3) and FeasibleTuple::isFeasibleTuple(q1, q2, q3)
@@ -64,7 +64,7 @@ module Make<RegexTreeViewSig TreeImpl> {
*
* We lazily only construct those states that we are actually
* going to need.
* Either a start state `(pivot, pivot, succ)`, or a state
* Either a start state `(pivot, pivot, pumpEnd)`, or a state
* where there exists a transition from an already existing state.
*
* The exponential variant of this query (`js/redos`) uses an optimization
@@ -108,9 +108,9 @@ module Make<RegexTreeViewSig TreeImpl> {
// The states are reachable in the NFA in the order r1 -> r2 -> r3
delta+(r1) = r2 and
delta+(r2) = r3 and
// The first element can reach a beginning (the "pivot" state in a `(pivot, succ)` pair).
// The first element can reach a beginning (the "pivot" state in a `(pivot, pumpEnd)` pair).
canReachABeginning(r1) and
// The last element can reach a target (the "succ" state in a `(pivot, succ)` pair).
// The last element can reach a target (the "pumpEnd" state in a `(pivot, pumpEnd)` pair).
canReachATarget(r3)
}
@@ -132,7 +132,7 @@ module Make<RegexTreeViewSig TreeImpl> {
/**
* Holds if there exists a path in the NFA from `s` to a "pivot" state
* (from a `(pivot, succ)` pair that starts the search).
* (from a `(pivot, pumpEnd)` pair that starts the search).
*/
pragma[noinline]
private predicate canReachABeginning(State s) {
@@ -140,25 +140,25 @@ module Make<RegexTreeViewSig TreeImpl> {
}
/**
* Holds if there exists a path in the NFA from `s` to a "succ" state
* (from a `(pivot, succ)` pair that starts the search).
* Holds if there exists a path in the NFA from `s` to a "pumpEnd" state
* (from a `(pivot, pumpEnd)` pair that starts the search).
*/
pragma[noinline]
private predicate canReachATarget(State s) {
delta+(s) = any(State succ | isStartLoops(_, succ))
delta+(s) = any(State pumpEnd | isStartLoops(_, pumpEnd))
}
}
/**
* Holds if `pivot` and `succ` are a pair of loops that could be the beginning of a quadratic blowup.
* Holds if `pivot` and `pumpEnd` are a pair of loops that could be the beginning of a quadratic blowup.
*
* There is a slight implementation difference compared to the paper: this predicate requires that `pivot != succ`.
* The case where `pivot = succ` causes exponential backtracking and is handled by the `js/redos` query.
* There is a slight implementation difference compared to the paper: this predicate requires that `pivot != pumpEnd`.
* The case where `pivot = pumpEnd` causes exponential backtracking and is handled by the `js/redos` query.
*/
predicate isStartLoops(State pivot, State succ) {
pivot != succ and
succ.getRepr() instanceof InfiniteRepetitionQuantifier and
delta+(pivot) = succ and
predicate isStartLoops(State pivot, State pumpEnd) {
pivot != pumpEnd and
pumpEnd.getRepr() instanceof InfiniteRepetitionQuantifier and
delta+(pivot) = pumpEnd and
(
pivot.getRepr() instanceof InfiniteRepetitionQuantifier
or
@@ -296,7 +296,7 @@ module Make<RegexTreeViewSig TreeImpl> {
/**
* Holds if `tuple` is an end state in our search.
* That means there exists a pair of loops `(pivot, succ)` such that `tuple = (pivot, succ, succ)`.
* That means there exists a pair of loops `(pivot, pumpEnd)` such that `tuple = (pivot, pumpEnd, pumpEnd)`.
*/
predicate isEndTuple(StateTuple tuple) { tuple = getAnEndTuple(_, _) }
@@ -311,45 +311,45 @@ module Make<RegexTreeViewSig TreeImpl> {
shortestDistances(isEndTuple/1, tupleDeltaBackwards/2)(end, r, result)
/**
* Holds if there exists a pair of repetitions `(pivot, succ)` in the regular expression such that:
* `tuple` is reachable from `(pivot, pivot, succ)` in the product automaton,
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, succ, succ)`,
* Holds if there exists a pair of repetitions `(pivot, pumpEnd)` in the regular expression such that:
* `tuple` is reachable from `(pivot, pivot, pumpEnd)` in the product automaton,
* and there is a distance of `dist` from `tuple` to the nearest end-tuple `(pivot, pumpEnd, pumpEnd)`,
* and a path from a start-state to `tuple` follows the transitions in `trace`.
*/
private predicate isReachableFromStartTuple(
State pivot, State succ, StateTuple tuple, Trace trace, int dist
State pivot, State pumpEnd, StateTuple tuple, Trace trace, int dist
) {
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, tuple, dist) and
isReachableFromStartTuple(pivot, pumpEnd, v, s1, s2, s3, tuple, dist) and
trace = Step(s1, s2, s3, v)
)
}
private predicate isReachableFromStartTuple(
State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
State pivot, State pumpEnd, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
StateTuple tuple, int dist
) {
// base case.
isStartLoops(pivot, succ) and
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
isStartLoops(pivot, pumpEnd) and
step(MkStateTuple(pivot, pivot, pumpEnd), s1, s2, s3, tuple) and
tuple = MkStateTuple(_, _, _) and
trace = Nil() and
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
dist = distBackFromEnd(tuple, MkStateTuple(pivot, pumpEnd, pumpEnd))
or
// recursive case
exists(StateTuple p |
isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
isReachableFromStartTuple(pivot, pumpEnd, p, trace, dist + 1) and
dist = distBackFromEnd(tuple, MkStateTuple(pivot, pumpEnd, pumpEnd)) and
step(p, s1, s2, s3, tuple)
)
}
/**
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
* Gets the tuple `(pivot, pumpEnd, pumpEnd)` from the product automaton.
*/
StateTuple getAnEndTuple(State pivot, State succ) {
isStartLoops(pivot, succ) and
result = MkStateTuple(pivot, succ, succ)
StateTuple getAnEndTuple(State pivot, State pumpEnd) {
isStartLoops(pivot, pumpEnd) and
result = MkStateTuple(pivot, pumpEnd, pumpEnd)
}
/** An implementation of a chain containing chars for use by `Concretizer`. */
@@ -360,8 +360,8 @@ module Make<RegexTreeViewSig TreeImpl> {
/** Holds if `n` is used in `isPumpable`. */
predicate isARelevantEnd(CharNode n) {
exists(State pivot, State succ |
isReachableFromStartTuple(pivot, succ, getAnEndTuple(pivot, succ), n, _)
exists(State pivot, State pumpEnd |
isReachableFromStartTuple(pivot, pumpEnd, getAnEndTuple(pivot, pumpEnd), n, _)
)
}
@@ -375,8 +375,8 @@ module Make<RegexTreeViewSig TreeImpl> {
/**
* Holds if matching repetitions of `pump` can:
* 1) Transition from `pivot` back to `pivot`.
* 2) Transition from `pivot` to `succ`.
* 3) Transition from `succ` to `succ`.
* 2) Transition from `pivot` to `pumpEnd`.
* 3) Transition from `pumpEnd` to `pumpEnd`.
*
* From theorem 3 in the paper linked in the top of this file we can therefore conclude that
* the regular expression has polynomial backtracking - if a rejecting suffix exists.
@@ -384,10 +384,10 @@ module Make<RegexTreeViewSig TreeImpl> {
* This predicate is used by `SuperLinearReDoSConfiguration`, and the final results are
* available in the `hasReDoSResult` predicate.
*/
predicate isPumpable(State pivot, State succ, string pump) {
predicate isPumpable(State pivot, State pumpEnd, string pump) {
exists(StateTuple q, Trace t |
isReachableFromStartTuple(pivot, succ, q, t, _) and
q = getAnEndTuple(pivot, succ) and
isReachableFromStartTuple(pivot, pumpEnd, q, t, _) and
q = getAnEndTuple(pivot, pumpEnd) and
pump = Concretizer<CharTreeImpl>::concretize(t)
)
}
@@ -439,8 +439,8 @@ module Make<RegexTreeViewSig TreeImpl> {
* Holds if all non-empty successors to the polynomial backtracking term matches the end of the line.
*/
predicate isAtEndLine() {
forall(RegExpTerm succ | super.getSuccessor+() = succ and not matchesEpsilon(succ) |
succ instanceof RegExpDollar
forall(RegExpTerm pumpEnd | super.getSuccessor+() = pumpEnd and not matchesEpsilon(pumpEnd) |
pumpEnd instanceof RegExpDollar
)
}