add a step over empty lookaheads/lookbehinds

This commit is contained in:
Erik Krogh Kristensen
2021-07-14 21:51:36 +02:00
parent fb57c5f6f0
commit 80d784e37a
5 changed files with 61 additions and 30 deletions

View File

@@ -71,6 +71,49 @@ private int ascii(string char) {
)
}
/**
* Holds if `t` matches at least an epsilon symbol.
*
* That is, this term does not restrict the language of the enclosing regular expression.
*
* This is implemented as an under-approximation, and this predicate does not hold for sub-patterns in particular.
*/
predicate matchesEpsilon(RegExpTerm t) {
t instanceof RegExpStar
or
t instanceof RegExpOpt
or
t.(RegExpRange).getLowerBound() = 0
or
exists(RegExpTerm child |
child = t.getAChild() and
matchesEpsilon(child)
|
t instanceof RegExpAlt or
t instanceof RegExpGroup or
t instanceof RegExpPlus or
t instanceof RegExpRange
)
or
matchesEpsilon(t.(RegExpBackRef).getGroup())
or
forex(RegExpTerm child | child = t.(RegExpSequence).getAChild() | matchesEpsilon(child))
}
/**
* A lookahead/lookbehind that matches the empty string.
*/
class EmptyPositiveSubPatttern extends RegExpSubPattern {
EmptyPositiveSubPatttern() {
(
this instanceof RegExpPositiveLookahead
or
this instanceof RegExpPositiveLookbehind
) and
matchesEpsilon(this.getOperand())
}
}
/**
* A branch in a disjunction that is the root node in a literal, or a literal
* whose root node is not a disjunction.
@@ -550,6 +593,10 @@ predicate delta(State q1, EdgeLabel lbl, State q2) {
exists(RegExpDollar dollar | q1 = before(dollar) |
lbl = Epsilon() and q2 = Accept(getRoot(dollar))
)
or
exists(EmptyPositiveSubPatttern empty | q1 = before(empty) |
lbl = Epsilon() and q2 = after(empty)
)
}
/**

View File

@@ -363,35 +363,6 @@ predicate polynimalReDoS(RegExpTerm t, string pump, string prefixMsg, RegExpTerm
)
}
/**
* Holds if `t` matches at least an epsilon symbol.
*
* That is, this term does not restrict the language of the enclosing regular expression.
*
* This is implemented as an under-approximation, and this predicate does not hold for sub-patterns in particular.
*/
private predicate matchesEpsilon(RegExpTerm t) {
t instanceof RegExpStar
or
t instanceof RegExpOpt
or
t.(RegExpRange).getLowerBound() = 0
or
exists(RegExpTerm child |
child = t.getAChild() and
matchesEpsilon(child)
|
t instanceof RegExpAlt or
t instanceof RegExpGroup or
t instanceof RegExpPlus or
t instanceof RegExpRange
)
or
matchesEpsilon(t.(RegExpBackRef).getGroup())
or
forex(RegExpTerm child | child = t.(RegExpSequence).getAChild() | matchesEpsilon(child))
}
/**
* Gets a message for why `term` can cause polynomial backtracking.
*/