mirror of
https://github.com/github/codeql.git
synced 2026-04-27 01:35:13 +02:00
Port redos libraries from Python
This commit is contained in:
Joe Farebrother
@@ -140,6 +140,7 @@ private module Frameworks {
|
||||
private import semmle.code.java.frameworks.jOOQ
|
||||
private import semmle.code.java.frameworks.JMS
|
||||
private import semmle.code.java.frameworks.RabbitMQ
|
||||
private import semmle.code.java.regex.RegexFlow
|
||||
}
|
||||
|
||||
private predicate sourceModelCsv(string row) {
|
||||
|
||||
18
java/ql/lib/semmle/code/java/regex/RegexFlow.qll
Normal file
18
java/ql/lib/semmle/code/java/regex/RegexFlow.qll
Normal file
@@ -0,0 +1,18 @@
|
||||
import java
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
private class RegexSinkCsv extends SinkModelCsv {
|
||||
override predicate row(string row) {
|
||||
row =
|
||||
[
|
||||
//"namespace;type;subtypes;name;signature;ext;input;kind"
|
||||
"java.util.regex;Pattern;false;compile;(String);;Argument[0];regex-use",
|
||||
"java.util.regex;Pattern;false;compile;(String,int);;Argument[0];regex-use",
|
||||
"java.util.regex;Pattern;false;matches;(String,CharSequence);;Argument[0];regex-use",
|
||||
"java.util;String;false;matches;(String);;Argument[0];regex-use",
|
||||
"java.util;String;false;split;(String);;Argument[0];regex-use",
|
||||
"java.util;String;false;split;(String,int);;Argument[0];regex-use",
|
||||
"com.google.common.base;Splitter;false;onPattern;(String);;Argument[0];regex-use"
|
||||
]
|
||||
}
|
||||
}
|
||||
998
java/ql/lib/semmle/code/java/regex/RegexTreeView.qll
Normal file
998
java/ql/lib/semmle/code/java/regex/RegexTreeView.qll
Normal file
@@ -0,0 +1,998 @@
|
||||
/** Provides a class hierarchy corresponding to a parse tree of regular expressions. */
|
||||
|
||||
import java
|
||||
private import semmle.code.java.regex.regex
|
||||
|
||||
/**
|
||||
* An element containing a regular expression term, that is, either
|
||||
* a string literal (parsed as a regular expression)
|
||||
* or another regular expression term.
|
||||
*
|
||||
* For sequences and alternations, we require at least one child.
|
||||
* Otherwise, we wish to represent the term differently.
|
||||
* This avoids multiple representations of the same term.
|
||||
*/
|
||||
newtype TRegExpParent =
|
||||
/** A string literal used as a regular expression */
|
||||
TRegExpLiteral(Regex re) or
|
||||
/** A quantified term */
|
||||
TRegExpQuantifier(Regex re, int start, int end) { re.qualifiedItem(start, end, _, _) } or
|
||||
/** A sequence term */
|
||||
TRegExpSequence(Regex re, int start, int end) {
|
||||
re.sequence(start, end) and
|
||||
exists(seqChild(re, start, end, 1)) // if a sequence does not have more than one element, it should be treated as that element instead.
|
||||
} or
|
||||
/** An alternation term */
|
||||
TRegExpAlt(Regex re, int start, int end) {
|
||||
re.alternation(start, end) and
|
||||
exists(int part_end |
|
||||
re.alternationOption(start, end, start, part_end) and
|
||||
part_end < end
|
||||
) // if an alternation does not have more than one element, it should be treated as that element instead.
|
||||
} or
|
||||
/** A character class term */
|
||||
TRegExpCharacterClass(Regex re, int start, int end) { re.charSet(start, end) } or
|
||||
/** A character range term */
|
||||
TRegExpCharacterRange(Regex re, int start, int end) { re.charRange(_, start, _, _, end) } or
|
||||
/** A group term */
|
||||
TRegExpGroup(Regex re, int start, int end) { re.group(start, end) } or
|
||||
/** A special character */
|
||||
TRegExpSpecialChar(Regex re, int start, int end) { re.specialCharacter(start, end, _) } or
|
||||
/** A normal character */
|
||||
TRegExpNormalChar(Regex re, int start, int end) { re.normalCharacter(start, end) } or
|
||||
/** A back reference */
|
||||
TRegExpBackRef(Regex re, int start, int end) { re.backreference(start, end) }
|
||||
|
||||
/**
|
||||
* An element containing a regular expression term, that is, either
|
||||
* a string literal (parsed as a regular expression)
|
||||
* or another regular expression term.
|
||||
*/
|
||||
class RegExpParent extends TRegExpParent {
|
||||
/** Gets a textual representation of this element. */
|
||||
string toString() { result = "RegExpParent" }
|
||||
|
||||
/** Gets the `i`th child term. */
|
||||
abstract RegExpTerm getChild(int i);
|
||||
|
||||
/** Gets a child term . */
|
||||
RegExpTerm getAChild() { result = this.getChild(_) }
|
||||
|
||||
/** Gets the number of child terms. */
|
||||
int getNumChild() { result = count(this.getAChild()) }
|
||||
|
||||
/** Gets the associated regex. */
|
||||
abstract Regex getRegex();
|
||||
}
|
||||
|
||||
/** A string literal used as a regular expression */
|
||||
class RegExpLiteral extends TRegExpLiteral, RegExpParent {
|
||||
Regex re;
|
||||
|
||||
RegExpLiteral() { this = TRegExpLiteral(re) }
|
||||
|
||||
override RegExpTerm getChild(int i) { i = 0 and result.getRegex() = re and result.isRootTerm() }
|
||||
|
||||
/** Holds if dot, `.`, matches all characters, including newlines. */
|
||||
predicate isDotAll() { re.getAMode() = "DOTALL" }
|
||||
|
||||
/** Holds if this regex matching is case-insensitive for this regex. */
|
||||
predicate isIgnoreCase() { re.getAMode() = "IGNORECASE" }
|
||||
|
||||
/** Get a string representing all modes for this regex. */
|
||||
string getFlags() { result = concat(string mode | mode = re.getAMode() | mode, " | ") }
|
||||
|
||||
override Regex getRegex() { result = re }
|
||||
|
||||
/** Gets the primary QL class for this regex. */
|
||||
string getPrimaryQLClass() { result = "RegExpLiteral" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A regular expression term, that is, a syntactic part of a regular expression.
|
||||
*/
|
||||
class RegExpTerm extends RegExpParent {
|
||||
Regex re;
|
||||
int start;
|
||||
int end;
|
||||
|
||||
RegExpTerm() {
|
||||
this = TRegExpAlt(re, start, end)
|
||||
or
|
||||
this = TRegExpBackRef(re, start, end)
|
||||
or
|
||||
this = TRegExpCharacterClass(re, start, end)
|
||||
or
|
||||
this = TRegExpCharacterRange(re, start, end)
|
||||
or
|
||||
this = TRegExpNormalChar(re, start, end)
|
||||
or
|
||||
this = TRegExpGroup(re, start, end)
|
||||
or
|
||||
this = TRegExpQuantifier(re, start, end)
|
||||
or
|
||||
this = TRegExpSequence(re, start, end)
|
||||
or
|
||||
this = TRegExpSpecialChar(re, start, end)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the outermost term of this regular expression.
|
||||
*/
|
||||
RegExpTerm getRootTerm() {
|
||||
this.isRootTerm() and result = this
|
||||
or
|
||||
result = this.getParent().(RegExpTerm).getRootTerm()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this term is part of a string literal
|
||||
* that is interpreted as a regular expression.
|
||||
*/
|
||||
predicate isUsedAsRegExp() { any() }
|
||||
|
||||
/**
|
||||
* Holds if this is the root term of a regular expression.
|
||||
*/
|
||||
predicate isRootTerm() { start = 0 and end = re.getText().length() }
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
result = this.(RegExpAlt).getChild(i)
|
||||
or
|
||||
result = this.(RegExpBackRef).getChild(i)
|
||||
or
|
||||
result = this.(RegExpCharacterClass).getChild(i)
|
||||
or
|
||||
result = this.(RegExpCharacterRange).getChild(i)
|
||||
or
|
||||
result = this.(RegExpNormalChar).getChild(i)
|
||||
or
|
||||
result = this.(RegExpGroup).getChild(i)
|
||||
or
|
||||
result = this.(RegExpQuantifier).getChild(i)
|
||||
or
|
||||
result = this.(RegExpSequence).getChild(i)
|
||||
or
|
||||
result = this.(RegExpSpecialChar).getChild(i)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the parent term of this regular expression term, or the
|
||||
* regular expression literal if this is the root term.
|
||||
*/
|
||||
RegExpParent getParent() { result.getAChild() = this }
|
||||
|
||||
override Regex getRegex() { result = re }
|
||||
|
||||
/** Gets the offset at which this term starts. */
|
||||
int getStart() { result = start }
|
||||
|
||||
/** Gets the offset at which this term ends. */
|
||||
int getEnd() { result = end }
|
||||
|
||||
override string toString() { result = re.getText().substring(start, end) }
|
||||
|
||||
/**
|
||||
* Gets the location of the surrounding regex, as locations inside the regex do not exist.
|
||||
* To get location information corresponding to the term inside the regex,
|
||||
* use `hasLocationInfo`.
|
||||
*/
|
||||
Location getLocation() { result = re.getLocation() }
|
||||
|
||||
/** Holds if this term is found at the specified location offsets. */
|
||||
predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
) {
|
||||
exists(int re_start, int re_end |
|
||||
re.getLocation().hasLocationInfo(filepath, startline, re_start, endline, re_end) and
|
||||
startcolumn = re_start + start + 4 and
|
||||
endcolumn = re_start + end + 3
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the file in which this term is found. */
|
||||
File getFile() { result = this.getLocation().getFile() }
|
||||
|
||||
/** Gets the raw source text of this term. */
|
||||
string getRawValue() { result = this.toString() }
|
||||
|
||||
/** Gets the string literal in which this term is found. */
|
||||
RegExpLiteral getLiteral() { result = TRegExpLiteral(re) }
|
||||
|
||||
/** Gets the regular expression term that is matched (textually) before this one, if any. */
|
||||
RegExpTerm getPredecessor() {
|
||||
exists(RegExpTerm parent | parent = this.getParent() |
|
||||
result = parent.(RegExpSequence).previousElement(this)
|
||||
or
|
||||
not exists(parent.(RegExpSequence).previousElement(this)) and
|
||||
not parent instanceof RegExpSubPattern and
|
||||
result = parent.getPredecessor()
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the regular expression term that is matched (textually) after this one, if any. */
|
||||
RegExpTerm getSuccessor() {
|
||||
exists(RegExpTerm parent | parent = this.getParent() |
|
||||
result = parent.(RegExpSequence).nextElement(this)
|
||||
or
|
||||
not exists(parent.(RegExpSequence).nextElement(this)) and
|
||||
not parent instanceof RegExpSubPattern and
|
||||
result = parent.getSuccessor()
|
||||
)
|
||||
}
|
||||
|
||||
/** Gets the primary QL class for this term. */
|
||||
string getPrimaryQLClass() { result = "RegExpTerm" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A quantified regular expression term.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* ((ECMA|Java)[sS]cript)*
|
||||
* ```
|
||||
*/
|
||||
class RegExpQuantifier extends RegExpTerm, TRegExpQuantifier {
|
||||
int part_end;
|
||||
boolean maybe_empty;
|
||||
boolean may_repeat_forever;
|
||||
|
||||
RegExpQuantifier() {
|
||||
this = TRegExpQuantifier(re, start, end) and
|
||||
re.qualifiedPart(start, part_end, end, maybe_empty, may_repeat_forever)
|
||||
}
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
i = 0 and
|
||||
result.getRegex() = re and
|
||||
result.getStart() = start and
|
||||
result.getEnd() = part_end
|
||||
}
|
||||
|
||||
/** Hols if this term may match an unlimited number of times. */
|
||||
predicate mayRepeatForever() { may_repeat_forever = true }
|
||||
|
||||
/** Gets the qualifier for this term. That is e.g "?" for "a?". */
|
||||
string getQualifier() { result = re.getText().substring(part_end, end) }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpQuantifier" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A regular expression term that permits unlimited repetitions.
|
||||
*/
|
||||
class InfiniteRepetitionQuantifier extends RegExpQuantifier {
|
||||
InfiniteRepetitionQuantifier() { this.mayRepeatForever() }
|
||||
}
|
||||
|
||||
/**
|
||||
* A star-quantified term.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* \w*
|
||||
* ```
|
||||
*/
|
||||
class RegExpStar extends InfiniteRepetitionQuantifier {
|
||||
RegExpStar() { this.getQualifier().charAt(0) = "*" }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpStar" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A plus-quantified term.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* \w+
|
||||
* ```
|
||||
*/
|
||||
class RegExpPlus extends InfiniteRepetitionQuantifier {
|
||||
RegExpPlus() { this.getQualifier().charAt(0) = "+" }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpPlus" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An optional term.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* ;?
|
||||
* ```
|
||||
*/
|
||||
class RegExpOpt extends RegExpQuantifier {
|
||||
RegExpOpt() { this.getQualifier().charAt(0) = "?" }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpOpt" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A range-quantified term
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* \w{2,4}
|
||||
* \w{2,}
|
||||
* \w{2}
|
||||
* ```
|
||||
*/
|
||||
class RegExpRange extends RegExpQuantifier {
|
||||
string upper;
|
||||
string lower;
|
||||
|
||||
RegExpRange() { re.multiples(part_end, end, lower, upper) }
|
||||
|
||||
/** Gets the string defining the upper bound of this range, if any. */
|
||||
string getUpper() { result = upper }
|
||||
|
||||
/** Gets the string defining the lower bound of this range, if any. */
|
||||
string getLower() { result = lower }
|
||||
|
||||
/**
|
||||
* Gets the upper bound of the range, if any.
|
||||
*
|
||||
* If there is no upper bound, any number of repetitions is allowed.
|
||||
* For a term of the form `r{lo}`, both the lower and the upper bound
|
||||
* are `lo`.
|
||||
*/
|
||||
int getUpperBound() { result = this.getUpper().toInt() }
|
||||
|
||||
/** Gets the lower bound of the range. */
|
||||
int getLowerBound() { result = this.getLower().toInt() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpRange" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A sequence term.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* (ECMA|Java)Script
|
||||
* ```
|
||||
*
|
||||
* This is a sequence with the elements `(ECMA|Java)` and `Script`.
|
||||
*/
|
||||
class RegExpSequence extends RegExpTerm, TRegExpSequence {
|
||||
RegExpSequence() { this = TRegExpSequence(re, start, end) }
|
||||
|
||||
override RegExpTerm getChild(int i) { result = seqChild(re, start, end, i) }
|
||||
|
||||
/** Gets the element preceding `element` in this sequence. */
|
||||
RegExpTerm previousElement(RegExpTerm element) { element = this.nextElement(result) }
|
||||
|
||||
/** Gets the element following `element` in this sequence. */
|
||||
RegExpTerm nextElement(RegExpTerm element) {
|
||||
exists(int i |
|
||||
element = this.getChild(i) and
|
||||
result = this.getChild(i + 1)
|
||||
)
|
||||
}
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpSequence" }
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private int seqChildEnd(Regex re, int start, int end, int i) {
|
||||
result = seqChild(re, start, end, i).getEnd()
|
||||
}
|
||||
|
||||
// moved out so we can use it in the charpred
|
||||
private RegExpTerm seqChild(Regex re, int start, int end, int i) {
|
||||
re.sequence(start, end) and
|
||||
(
|
||||
i = 0 and
|
||||
result.getRegex() = re and
|
||||
result.getStart() = start and
|
||||
exists(int itemEnd |
|
||||
re.item(start, itemEnd) and
|
||||
result.getEnd() = itemEnd
|
||||
)
|
||||
or
|
||||
i > 0 and
|
||||
result.getRegex() = re and
|
||||
exists(int itemStart | itemStart = seqChildEnd(re, start, end, i - 1) |
|
||||
result.getStart() = itemStart and
|
||||
re.item(itemStart, result.getEnd())
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* An alternative term, that is, a term of the form `a|b`.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* ECMA|Java
|
||||
* ```
|
||||
*/
|
||||
class RegExpAlt extends RegExpTerm, TRegExpAlt {
|
||||
RegExpAlt() { this = TRegExpAlt(re, start, end) }
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
i = 0 and
|
||||
result.getRegex() = re and
|
||||
result.getStart() = start and
|
||||
exists(int part_end |
|
||||
re.alternationOption(start, end, start, part_end) and
|
||||
result.getEnd() = part_end
|
||||
)
|
||||
or
|
||||
i > 0 and
|
||||
result.getRegex() = re and
|
||||
exists(int part_start |
|
||||
part_start = this.getChild(i - 1).getEnd() + 1 // allow for the |
|
||||
|
|
||||
result.getStart() = part_start and
|
||||
re.alternationOption(start, end, part_start, result.getEnd())
|
||||
)
|
||||
}
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpAlt" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An escaped regular expression term, that is, a regular expression
|
||||
* term starting with a backslash, which is not a backreference.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* \.
|
||||
* \w
|
||||
* ```
|
||||
*/
|
||||
class RegExpEscape extends RegExpNormalChar {
|
||||
RegExpEscape() { re.escapedCharacter(start, end) }
|
||||
|
||||
/**
|
||||
* Gets the name of the escaped; for example, `w` for `\w`.
|
||||
* TODO: Handle named escapes.
|
||||
*/
|
||||
override string getValue() {
|
||||
this.isIdentityEscape() and result = this.getUnescaped()
|
||||
or
|
||||
this.getUnescaped() = "n" and result = "\n"
|
||||
or
|
||||
this.getUnescaped() = "r" and result = "\r"
|
||||
or
|
||||
this.getUnescaped() = "t" and result = "\t"
|
||||
or
|
||||
// TODO: Find a way to include a formfeed character
|
||||
// this.getUnescaped() = "f" and result = " "
|
||||
// or
|
||||
this.isUnicode() and
|
||||
result = this.getUnicode()
|
||||
}
|
||||
|
||||
/** Holds if this terms name is given by the part following the escape character. */
|
||||
predicate isIdentityEscape() { not this.getUnescaped() in ["n", "r", "t", "f"] }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpEscape" }
|
||||
|
||||
/** Gets the part of the term following the escape character. That is e.g. "w" if the term is "\w". */
|
||||
private string getUnescaped() { result = this.getText().suffix(1) }
|
||||
|
||||
/**
|
||||
* Gets the text for this escape. That is e.g. "\w".
|
||||
*/
|
||||
private string getText() { result = re.getText().substring(start, end) }
|
||||
|
||||
/**
|
||||
* Holds if this is a unicode escape.
|
||||
*/
|
||||
private predicate isUnicode() { this.getText().prefix(2) = ["\\u", "\\U"] }
|
||||
|
||||
/**
|
||||
* Gets the unicode char for this escape.
|
||||
* E.g. for `\u0061` this returns "a".
|
||||
*/
|
||||
private string getUnicode() {
|
||||
exists(int codepoint | codepoint = sum(this.getHexValueFromUnicode(_)) |
|
||||
result = codepoint.toUnicode()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets int value for the `index`th char in the hex number of the unicode escape.
|
||||
* E.g. for `\u0061` and `index = 2` this returns 96 (the number `6` interpreted as hex).
|
||||
*/
|
||||
private int getHexValueFromUnicode(int index) {
|
||||
this.isUnicode() and
|
||||
exists(string hex, string char | hex = this.getText().suffix(2) |
|
||||
char = hex.charAt(index) and
|
||||
result = 16.pow(hex.length() - index - 1) * toHex(char)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the hex number for the `hex` char.
|
||||
*/
|
||||
private int toHex(string hex) {
|
||||
hex = [0 .. 9].toString() and
|
||||
result = hex.toInt()
|
||||
or
|
||||
result = 10 and hex = ["a", "A"]
|
||||
or
|
||||
result = 11 and hex = ["b", "B"]
|
||||
or
|
||||
result = 12 and hex = ["c", "C"]
|
||||
or
|
||||
result = 13 and hex = ["d", "D"]
|
||||
or
|
||||
result = 14 and hex = ["e", "E"]
|
||||
or
|
||||
result = 15 and hex = ["f", "F"]
|
||||
}
|
||||
|
||||
/**
|
||||
* A character class escape in a regular expression.
|
||||
* That is, an escaped charachter that denotes multiple characters.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* \w
|
||||
* \S
|
||||
* ```
|
||||
*/
|
||||
class RegExpCharacterClassEscape extends RegExpEscape {
|
||||
RegExpCharacterClassEscape() { this.getValue() in ["d", "D", "s", "S", "w", "W"] }
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpCharacterClassEscape" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A character class in a regular expression.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* [a-z_]
|
||||
* [^<>&]
|
||||
* ```
|
||||
*/
|
||||
class RegExpCharacterClass extends RegExpTerm, TRegExpCharacterClass {
|
||||
RegExpCharacterClass() { this = TRegExpCharacterClass(re, start, end) }
|
||||
|
||||
/** Holds if this character class is inverted, matching the opposite of its content. */
|
||||
predicate isInverted() { re.getChar(start + 1) = "^" }
|
||||
|
||||
/** Gets the `i`th char inside this charater class. */
|
||||
string getCharThing(int i) { result = re.getChar(i + start) }
|
||||
|
||||
/** Holds if this character class can match anything. */
|
||||
predicate isUniversalClass() {
|
||||
// [^]
|
||||
this.isInverted() and not exists(this.getAChild())
|
||||
or
|
||||
// [\w\W] and similar
|
||||
not this.isInverted() and
|
||||
exists(string cce1, string cce2 |
|
||||
cce1 = this.getAChild().(RegExpCharacterClassEscape).getValue() and
|
||||
cce2 = this.getAChild().(RegExpCharacterClassEscape).getValue()
|
||||
|
|
||||
cce1 != cce2 and cce1.toLowerCase() = cce2.toLowerCase()
|
||||
)
|
||||
}
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
i = 0 and
|
||||
result.getRegex() = re and
|
||||
exists(int itemStart, int itemEnd |
|
||||
result.getStart() = itemStart and
|
||||
re.char_set_start(start, itemStart) and
|
||||
re.char_set_child(start, itemStart, itemEnd) and
|
||||
result.getEnd() = itemEnd
|
||||
)
|
||||
or
|
||||
i > 0 and
|
||||
result.getRegex() = re and
|
||||
exists(int itemStart | itemStart = this.getChild(i - 1).getEnd() |
|
||||
result.getStart() = itemStart and
|
||||
re.char_set_child(start, itemStart, result.getEnd())
|
||||
)
|
||||
}
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpCharacterClass" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A character range in a character class in a regular expression.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* a-z
|
||||
* ```
|
||||
*/
|
||||
class RegExpCharacterRange extends RegExpTerm, TRegExpCharacterRange {
|
||||
int lower_end;
|
||||
int upper_start;
|
||||
|
||||
RegExpCharacterRange() {
|
||||
this = TRegExpCharacterRange(re, start, end) and
|
||||
re.charRange(_, start, lower_end, upper_start, end)
|
||||
}
|
||||
|
||||
/** Holds if this range goes from `lo` to `hi`, in effect is `lo-hi`. */
|
||||
predicate isRange(string lo, string hi) {
|
||||
lo = re.getText().substring(start, lower_end) and
|
||||
hi = re.getText().substring(upper_start, end)
|
||||
}
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
i = 0 and
|
||||
result.getRegex() = re and
|
||||
result.getStart() = start and
|
||||
result.getEnd() = lower_end
|
||||
or
|
||||
i = 1 and
|
||||
result.getRegex() = re and
|
||||
result.getStart() = upper_start and
|
||||
result.getEnd() = end
|
||||
}
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpCharacterRange" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A normal character in a regular expression, that is, a character
|
||||
* without special meaning. This includes escaped characters.
|
||||
*
|
||||
* Examples:
|
||||
* ```
|
||||
* t
|
||||
* \t
|
||||
* ```
|
||||
*/
|
||||
class RegExpNormalChar extends RegExpTerm, TRegExpNormalChar {
|
||||
RegExpNormalChar() { this = TRegExpNormalChar(re, start, end) }
|
||||
|
||||
/**
|
||||
* Holds if this constant represents a valid Unicode character (as opposed
|
||||
* to a surrogate code point that does not correspond to a character by itself.)
|
||||
*/
|
||||
predicate isCharacter() { any() }
|
||||
|
||||
/** Gets the string representation of the char matched by this term. */
|
||||
string getValue() { result = re.getText().substring(start, end) }
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpNormalChar" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A constant regular expression term, that is, a regular expression
|
||||
* term matching a single string. Currently, this will always be a single character.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* a
|
||||
* ```
|
||||
*/
|
||||
class RegExpConstant extends RegExpTerm {
|
||||
string value;
|
||||
|
||||
RegExpConstant() {
|
||||
this = TRegExpNormalChar(re, start, end) and
|
||||
not this instanceof RegExpCharacterClassEscape and
|
||||
// exclude chars in qualifiers
|
||||
// TODO: push this into regex library
|
||||
not exists(int qstart, int qend | re.qualifiedPart(_, qstart, qend, _, _) |
|
||||
qstart <= start and end <= qend
|
||||
) and
|
||||
value = this.(RegExpNormalChar).getValue()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this constant represents a valid Unicode character (as opposed
|
||||
* to a surrogate code point that does not correspond to a character by itself.)
|
||||
*/
|
||||
predicate isCharacter() { any() }
|
||||
|
||||
/** Gets the string matched by this constant term. */
|
||||
string getValue() { result = value }
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpConstant" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A grouped regular expression.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (ECMA|Java)
|
||||
* (?:ECMA|Java)
|
||||
* (?<quote>['"])
|
||||
* ```
|
||||
*/
|
||||
class RegExpGroup extends RegExpTerm, TRegExpGroup {
|
||||
RegExpGroup() { this = TRegExpGroup(re, start, end) }
|
||||
|
||||
/**
|
||||
* Gets the index of this capture group within the enclosing regular
|
||||
* expression literal.
|
||||
*
|
||||
* For example, in the regular expression `/((a?).)(?:b)/`, the
|
||||
* group `((a?).)` has index 1, the group `(a?)` nested inside it
|
||||
* has index 2, and the group `(?:b)` has no index, since it is
|
||||
* not a capture group.
|
||||
*/
|
||||
int getNumber() { result = re.getGroupNumber(start, end) }
|
||||
|
||||
/** Holds if this is a named capture group. */
|
||||
predicate isNamed() { exists(this.getName()) }
|
||||
|
||||
/** Gets the name of this capture group, if any. */
|
||||
string getName() { result = re.getGroupName(start, end) }
|
||||
|
||||
override RegExpTerm getChild(int i) {
|
||||
result.getRegex() = re and
|
||||
i = 0 and
|
||||
re.groupContents(start, end, result.getStart(), result.getEnd())
|
||||
}
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpGroup" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A special character in a regular expression.
|
||||
*
|
||||
* Examples:
|
||||
* ```
|
||||
* ^
|
||||
* $
|
||||
* .
|
||||
* ```
|
||||
*/
|
||||
class RegExpSpecialChar extends RegExpTerm, TRegExpSpecialChar {
|
||||
string char;
|
||||
|
||||
RegExpSpecialChar() {
|
||||
this = TRegExpSpecialChar(re, start, end) and
|
||||
re.specialCharacter(start, end, char)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this constant represents a valid Unicode character (as opposed
|
||||
* to a surrogate code point that does not correspond to a character by itself.)
|
||||
*/
|
||||
predicate isCharacter() { any() }
|
||||
|
||||
/** Gets the char for this term. */
|
||||
string getChar() { result = char }
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpSpecialChar" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A dot regular expression.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* .
|
||||
* ```
|
||||
*/
|
||||
class RegExpDot extends RegExpSpecialChar {
|
||||
RegExpDot() { this.getChar() = "." }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpDot" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A dollar assertion `$` matching the end of a line.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* $
|
||||
* ```
|
||||
*/
|
||||
class RegExpDollar extends RegExpSpecialChar {
|
||||
RegExpDollar() { this.getChar() = "$" }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpDollar" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A caret assertion `^` matching the beginning of a line.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```
|
||||
* ^
|
||||
* ```
|
||||
*/
|
||||
class RegExpCaret extends RegExpSpecialChar {
|
||||
RegExpCaret() { this.getChar() = "^" }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpCaret" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A zero-width match, that is, either an empty group or an assertion.
|
||||
*
|
||||
* Examples:
|
||||
* ```
|
||||
* ()
|
||||
* (?=\w)
|
||||
* ```
|
||||
*/
|
||||
class RegExpZeroWidthMatch extends RegExpGroup {
|
||||
RegExpZeroWidthMatch() { re.zeroWidthMatch(start, end) }
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpZeroWidthMatch" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A zero-width lookahead or lookbehind assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?=\w)
|
||||
* (?!\n)
|
||||
* (?<=\.)
|
||||
* (?<!\\)
|
||||
* ```
|
||||
*/
|
||||
class RegExpSubPattern extends RegExpZeroWidthMatch {
|
||||
RegExpSubPattern() { not re.emptyGroup(start, end) }
|
||||
|
||||
/** Gets the lookahead term. */
|
||||
RegExpTerm getOperand() {
|
||||
exists(int in_start, int in_end | re.groupContents(start, end, in_start, in_end) |
|
||||
result.getRegex() = re and
|
||||
result.getStart() = in_start and
|
||||
result.getEnd() = in_end
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A zero-width lookahead assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?=\w)
|
||||
* (?!\n)
|
||||
* ```
|
||||
*/
|
||||
abstract class RegExpLookahead extends RegExpSubPattern { }
|
||||
|
||||
/**
|
||||
* A positive-lookahead assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?=\w)
|
||||
* ```
|
||||
*/
|
||||
class RegExpPositiveLookahead extends RegExpLookahead {
|
||||
RegExpPositiveLookahead() { re.positiveLookaheadAssertionGroup(start, end) }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpPositiveLookahead" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A negative-lookahead assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?!\n)
|
||||
* ```
|
||||
*/
|
||||
class RegExpNegativeLookahead extends RegExpLookahead {
|
||||
RegExpNegativeLookahead() { re.negativeLookaheadAssertionGroup(start, end) }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpNegativeLookahead" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A zero-width lookbehind assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?<=\.)
|
||||
* (?<!\\)
|
||||
* ```
|
||||
*/
|
||||
abstract class RegExpLookbehind extends RegExpSubPattern { }
|
||||
|
||||
/**
|
||||
* A positive-lookbehind assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?<=\.)
|
||||
* ```
|
||||
*/
|
||||
class RegExpPositiveLookbehind extends RegExpLookbehind {
|
||||
RegExpPositiveLookbehind() { re.positiveLookbehindAssertionGroup(start, end) }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpPositiveLookbehind" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A negative-lookbehind assertion.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* (?<!\\)
|
||||
* ```
|
||||
*/
|
||||
class RegExpNegativeLookbehind extends RegExpLookbehind {
|
||||
RegExpNegativeLookbehind() { re.negativeLookbehindAssertionGroup(start, end) }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpNegativeLookbehind" }
|
||||
}
|
||||
|
||||
/**
|
||||
* A back reference, that is, a term of the form `\i` or `\k<name>`
|
||||
* in a regular expression.
|
||||
*
|
||||
* Examples:
|
||||
*
|
||||
* ```
|
||||
* \1
|
||||
* (?P=quote)
|
||||
* ```
|
||||
*/
|
||||
class RegExpBackRef extends RegExpTerm, TRegExpBackRef {
|
||||
RegExpBackRef() { this = TRegExpBackRef(re, start, end) }
|
||||
|
||||
/**
|
||||
* Gets the number of the capture group this back reference refers to, if any.
|
||||
*/
|
||||
int getNumber() { result = re.getBackrefNumber(start, end) }
|
||||
|
||||
/**
|
||||
* Gets the name of the capture group this back reference refers to, if any.
|
||||
*/
|
||||
string getName() { result = re.getBackrefName(start, end) }
|
||||
|
||||
/** Gets the capture group this back reference refers to. */
|
||||
RegExpGroup getGroup() {
|
||||
result.getLiteral() = this.getLiteral() and
|
||||
(
|
||||
result.getNumber() = this.getNumber() or
|
||||
result.getName() = this.getName()
|
||||
)
|
||||
}
|
||||
|
||||
override RegExpTerm getChild(int i) { none() }
|
||||
|
||||
override string getPrimaryQLClass() { result = "RegExpBackRef" }
|
||||
}
|
||||
|
||||
/** Gets the parse tree resulting from parsing `re`, if such has been constructed. */
|
||||
RegExpTerm getParsedRegExp(StringLiteral re) { result.getRegex() = re and result.isRootTerm() }
|
||||
907
java/ql/lib/semmle/code/java/regex/regex.qll
Normal file
907
java/ql/lib/semmle/code/java/regex/regex.qll
Normal file
@@ -0,0 +1,907 @@
|
||||
import java
|
||||
import semmle.code.java.dataflow.DataFlow2
|
||||
import semmle.code.java.dataflow.ExternalFlow
|
||||
|
||||
class RegexFlowConf extends DataFlow2::Configuration {
|
||||
RegexFlowConf() { this = "RegexFlowConf" }
|
||||
|
||||
override predicate isSource(DataFlow2::Node node) { node.asExpr() instanceof StringLiteral }
|
||||
|
||||
override predicate isSink(DataFlow2::Node node) { sinkNode(node, "regex-use") }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `s` is used as a regex, with the mode `mode` (if known).
|
||||
* If regex mode is not known, `mode` will be `"None"`.
|
||||
*/
|
||||
predicate used_as_regex(Expr s, string mode) {
|
||||
any(RegexFlowConf c).hasFlow(DataFlow2::exprNode(s), _) and
|
||||
mode = "None" // TODO: proper mode detection
|
||||
}
|
||||
|
||||
/**
|
||||
* A string literal that is used as a regular exprssion.
|
||||
* TODO: adjust parser for java regex syntax
|
||||
*/
|
||||
abstract class RegexString extends Expr {
|
||||
RegexString() { this instanceof StringLiteral }
|
||||
|
||||
/**
|
||||
* Helper predicate for `char_set_start(int start, int end)`.
|
||||
*
|
||||
* In order to identify left brackets ('[') which actually start a character class,
|
||||
* we perform a left to right scan of the string.
|
||||
*
|
||||
* To avoid negative recursion we return a boolean. See `escaping`,
|
||||
* the helper for `escapingChar`, for a clean use of this pattern.
|
||||
*
|
||||
* result is true for those start chars that actually mark a start of a char set.
|
||||
*/
|
||||
boolean char_set_start(int pos) {
|
||||
exists(int index |
|
||||
// is opening bracket
|
||||
this.char_set_delimiter(index, pos) = true and
|
||||
(
|
||||
// if this is the first bracket, `pos` starts a char set
|
||||
index = 1 and result = true
|
||||
or
|
||||
// if the previous char set delimiter was not a closing bracket, `pos` does
|
||||
// not start a char set. This is needed to handle cases such as `[[]` (a
|
||||
// char set that matches the `[` char)
|
||||
index > 1 and
|
||||
not this.char_set_delimiter(index - 1, _) = false and
|
||||
result = false
|
||||
or
|
||||
// special handling of cases such as `[][]` (the character-set of the characters `]` and `[`).
|
||||
exists(int prev_closing_bracket_pos |
|
||||
// previous bracket is a closing bracket
|
||||
this.char_set_delimiter(index - 1, prev_closing_bracket_pos) = false and
|
||||
if
|
||||
// check if the character that comes before the previous closing bracket
|
||||
// is an opening bracket (taking `^` into account)
|
||||
exists(int pos_before_prev_closing_bracket |
|
||||
if this.getChar(prev_closing_bracket_pos - 1) = "^"
|
||||
then pos_before_prev_closing_bracket = prev_closing_bracket_pos - 2
|
||||
else pos_before_prev_closing_bracket = prev_closing_bracket_pos - 1
|
||||
|
|
||||
this.char_set_delimiter(index - 2, pos_before_prev_closing_bracket) = true
|
||||
)
|
||||
then
|
||||
// brackets without anything in between is not valid character ranges, so
|
||||
// the first closing bracket in `[]]` and `[^]]` does not count,
|
||||
//
|
||||
// and we should _not_ mark the second opening bracket in `[][]` and `[^][]`
|
||||
// as starting a new char set. ^ ^
|
||||
exists(int pos_before_prev_closing_bracket |
|
||||
this.char_set_delimiter(index - 2, pos_before_prev_closing_bracket) = true
|
||||
|
|
||||
result = this.char_set_start(pos_before_prev_closing_bracket).booleanNot()
|
||||
)
|
||||
else
|
||||
// if not, `pos` does in fact mark a real start of a character range
|
||||
result = true
|
||||
)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Helper predicate for chars that could be character-set delimiters.
|
||||
* Holds if the (non-escaped) char at `pos` in the string, is the (one-based) `index` occurrence of a bracket (`[` or `]`) in the string.
|
||||
* Result if `true` is the char is `[`, and `false` if the char is `]`.
|
||||
*/
|
||||
boolean char_set_delimiter(int index, int pos) {
|
||||
pos = rank[index](int p | this.nonEscapedCharAt(p) = "[" or this.nonEscapedCharAt(p) = "]") and
|
||||
(
|
||||
this.nonEscapedCharAt(pos) = "[" and result = true
|
||||
or
|
||||
this.nonEscapedCharAt(pos) = "]" and result = false
|
||||
)
|
||||
}
|
||||
|
||||
/** Hold is a character set starts between `start` and `end`. */
|
||||
predicate char_set_start(int start, int end) {
|
||||
this.char_set_start(start) = true and
|
||||
(
|
||||
this.getChar(start + 1) = "^" and end = start + 2
|
||||
or
|
||||
not this.getChar(start + 1) = "^" and end = start + 1
|
||||
)
|
||||
}
|
||||
|
||||
/** Whether there is a character class, between start (inclusive) and end (exclusive) */
|
||||
predicate charSet(int start, int end) {
|
||||
exists(int inner_start, int inner_end |
|
||||
this.char_set_start(start, inner_start) and
|
||||
not this.char_set_start(_, start)
|
||||
|
|
||||
end = inner_end + 1 and
|
||||
inner_end > inner_start and
|
||||
this.nonEscapedCharAt(inner_end) = "]" and
|
||||
not exists(int mid | this.nonEscapedCharAt(mid) = "]" | mid > inner_start and mid < inner_end)
|
||||
)
|
||||
}
|
||||
|
||||
/** An indexed version of `char_set_token/3` */
|
||||
private predicate char_set_token(int charset_start, int index, int token_start, int token_end) {
|
||||
token_start =
|
||||
rank[index](int start, int end | this.char_set_token(charset_start, start, end) | start) and
|
||||
this.char_set_token(charset_start, token_start, token_end)
|
||||
}
|
||||
|
||||
/** Either a char or a - */
|
||||
private predicate char_set_token(int charset_start, int start, int end) {
|
||||
this.char_set_start(charset_start, start) and
|
||||
(
|
||||
this.escapedCharacter(start, end)
|
||||
or
|
||||
exists(this.nonEscapedCharAt(start)) and end = start + 1
|
||||
)
|
||||
or
|
||||
this.char_set_token(charset_start, _, start) and
|
||||
(
|
||||
this.escapedCharacter(start, end)
|
||||
or
|
||||
exists(this.nonEscapedCharAt(start)) and
|
||||
end = start + 1 and
|
||||
not this.getChar(start) = "]"
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the character set starting at `charset_start` contains either
|
||||
* a character or a range found between `start` and `end`.
|
||||
*/
|
||||
predicate char_set_child(int charset_start, int start, int end) {
|
||||
this.char_set_token(charset_start, start, end) and
|
||||
not exists(int range_start, int range_end |
|
||||
this.charRange(charset_start, range_start, _, _, range_end) and
|
||||
range_start <= start and
|
||||
range_end >= end
|
||||
)
|
||||
or
|
||||
this.charRange(charset_start, start, _, _, end)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the character set starting at `charset_start` contains a character range
|
||||
* with lower bound found between `start` and `lower_end`
|
||||
* and upper bound found between `upper_start` and `end`.
|
||||
*/
|
||||
predicate charRange(int charset_start, int start, int lower_end, int upper_start, int end) {
|
||||
exists(int index |
|
||||
this.charRangeEnd(charset_start, index) = true and
|
||||
this.char_set_token(charset_start, index - 2, start, lower_end) and
|
||||
this.char_set_token(charset_start, index, upper_start, end)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Helper predicate for `charRange`.
|
||||
* We can determine where character ranges end by a left to right sweep.
|
||||
*
|
||||
* To avoid negative recursion we return a boolean. See `escaping`,
|
||||
* the helper for `escapingChar`, for a clean use of this pattern.
|
||||
*/
|
||||
private boolean charRangeEnd(int charset_start, int index) {
|
||||
this.char_set_token(charset_start, index, _, _) and
|
||||
(
|
||||
index in [1, 2] and result = false
|
||||
or
|
||||
index > 2 and
|
||||
exists(int connector_start |
|
||||
this.char_set_token(charset_start, index - 1, connector_start, _) and
|
||||
this.nonEscapedCharAt(connector_start) = "-" and
|
||||
result =
|
||||
this.charRangeEnd(charset_start, index - 2)
|
||||
.booleanNot()
|
||||
.booleanAnd(this.charRangeEnd(charset_start, index - 1).booleanNot())
|
||||
)
|
||||
or
|
||||
not exists(int connector_start |
|
||||
this.char_set_token(charset_start, index - 1, connector_start, _) and
|
||||
this.nonEscapedCharAt(connector_start) = "-"
|
||||
) and
|
||||
result = false
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if the character at `pos` is a "\" that is actually escaping what comes after. */
|
||||
predicate escapingChar(int pos) { this.escaping(pos) = true }
|
||||
|
||||
/**
|
||||
* Helper predicate for `escapingChar`.
|
||||
* In order to avoid negative recusrion, we return a boolean.
|
||||
* This way, we can refer to `escaping(pos - 1).booleanNot()`
|
||||
* rather than to a negated version of `escaping(pos)`.
|
||||
*/
|
||||
private boolean escaping(int pos) {
|
||||
pos = -1 and result = false
|
||||
or
|
||||
this.getChar(pos) = "\\" and result = this.escaping(pos - 1).booleanNot()
|
||||
or
|
||||
this.getChar(pos) != "\\" and result = false
|
||||
}
|
||||
|
||||
/** Gets the text of this regex */
|
||||
string getText() { result = this.(StringLiteral).getValue() }
|
||||
|
||||
string getChar(int i) { result = this.getText().charAt(i) }
|
||||
|
||||
string nonEscapedCharAt(int i) {
|
||||
result = this.getText().charAt(i) and
|
||||
not exists(int x, int y | this.escapedCharacter(x, y) and i in [x .. y - 1])
|
||||
}
|
||||
|
||||
private predicate isOptionDivider(int i) { this.nonEscapedCharAt(i) = "|" }
|
||||
|
||||
private predicate isGroupEnd(int i) { this.nonEscapedCharAt(i) = ")" and not this.inCharSet(i) }
|
||||
|
||||
private predicate isGroupStart(int i) { this.nonEscapedCharAt(i) = "(" and not this.inCharSet(i) }
|
||||
|
||||
predicate failedToParse(int i) {
|
||||
exists(this.getChar(i)) and
|
||||
not exists(int start, int end |
|
||||
this.top_level(start, end) and
|
||||
start <= i and
|
||||
end > i
|
||||
)
|
||||
}
|
||||
|
||||
/** Named unicode characters, eg \N{degree sign} */
|
||||
private predicate escapedName(int start, int end) {
|
||||
this.escapingChar(start) and
|
||||
this.getChar(start + 1) = "N" and
|
||||
this.getChar(start + 2) = "{" and
|
||||
this.getChar(end - 1) = "}" and
|
||||
end > start and
|
||||
not exists(int i | start + 2 < i and i < end - 1 | this.getChar(i) = "}")
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if an escaped character is found between `start` and `end`.
|
||||
* Escaped characters include hex values, octal values and named escapes,
|
||||
* but excludes backreferences.
|
||||
*/
|
||||
predicate escapedCharacter(int start, int end) {
|
||||
this.escapingChar(start) and
|
||||
not this.numbered_backreference(start, _, _) and
|
||||
(
|
||||
// hex value \xhh
|
||||
this.getChar(start + 1) = "x" and end = start + 4
|
||||
or
|
||||
// octal value \o, \oo, or \ooo
|
||||
end in [start + 2 .. start + 4] and
|
||||
forall(int i | i in [start + 1 .. end - 1] | this.isOctal(i)) and
|
||||
not (
|
||||
end < start + 4 and
|
||||
this.isOctal(end)
|
||||
)
|
||||
or
|
||||
// 16-bit hex value \uhhhh
|
||||
this.getChar(start + 1) = "u" and end = start + 6
|
||||
or
|
||||
// 32-bit hex value \Uhhhhhhhh
|
||||
this.getChar(start + 1) = "U" and end = start + 10
|
||||
or
|
||||
escapedName(start, end)
|
||||
or
|
||||
// escape not handled above, update when adding a new case
|
||||
not this.getChar(start + 1) in ["x", "u", "U", "N"] and
|
||||
not exists(this.getChar(start + 1).toInt()) and
|
||||
end = start + 2
|
||||
)
|
||||
}
|
||||
|
||||
pragma[inline]
|
||||
private predicate isOctal(int index) { this.getChar(index) = [0 .. 7].toString() }
|
||||
|
||||
/** Holds if `index` is inside a character set. */
|
||||
predicate inCharSet(int index) {
|
||||
exists(int x, int y | this.charSet(x, y) and index in [x + 1 .. y - 2])
|
||||
}
|
||||
|
||||
/**
|
||||
* 'simple' characters are any that don't alter the parsing of the regex.
|
||||
*/
|
||||
private predicate simpleCharacter(int start, int end) {
|
||||
end = start + 1 and
|
||||
not this.charSet(start, _) and
|
||||
not this.charSet(_, start + 1) and
|
||||
exists(string c | c = this.getChar(start) |
|
||||
exists(int x, int y, int z |
|
||||
this.charSet(x, z) and
|
||||
this.char_set_start(x, y)
|
||||
|
|
||||
start = y
|
||||
or
|
||||
start = z - 2
|
||||
or
|
||||
start > y and start < z - 2 and not this.charRange(_, _, start, end, _)
|
||||
)
|
||||
or
|
||||
not this.inCharSet(start) and
|
||||
not c = "(" and
|
||||
not c = "[" and
|
||||
not c = ")" and
|
||||
not c = "|" and
|
||||
not this.qualifier(start, _, _, _)
|
||||
)
|
||||
}
|
||||
|
||||
predicate character(int start, int end) {
|
||||
(
|
||||
this.simpleCharacter(start, end) and
|
||||
not exists(int x, int y | this.escapedCharacter(x, y) and x <= start and y >= end)
|
||||
or
|
||||
this.escapedCharacter(start, end)
|
||||
) and
|
||||
not exists(int x, int y | this.group_start(x, y) and x <= start and y >= end) and
|
||||
not exists(int x, int y | this.backreference(x, y) and x <= start and y >= end)
|
||||
}
|
||||
|
||||
predicate normalCharacter(int start, int end) {
|
||||
this.character(start, end) and
|
||||
not this.specialCharacter(start, end, _)
|
||||
}
|
||||
|
||||
predicate specialCharacter(int start, int end, string char) {
|
||||
this.character(start, end) and
|
||||
end = start + 1 and
|
||||
char = this.getChar(start) and
|
||||
(char = "$" or char = "^" or char = ".") and
|
||||
not this.inCharSet(start)
|
||||
}
|
||||
|
||||
/** Whether the text in the range start,end is a group */
|
||||
predicate group(int start, int end) {
|
||||
this.groupContents(start, end, _, _)
|
||||
or
|
||||
this.emptyGroup(start, end)
|
||||
}
|
||||
|
||||
/** Gets the number of the group in start,end */
|
||||
int getGroupNumber(int start, int end) {
|
||||
this.group(start, end) and
|
||||
result =
|
||||
count(int i | this.group(i, _) and i < start and not this.non_capturing_group_start(i, _)) + 1
|
||||
}
|
||||
|
||||
/** Gets the name, if it has one, of the group in start,end */
|
||||
string getGroupName(int start, int end) {
|
||||
this.group(start, end) and
|
||||
exists(int name_end |
|
||||
this.named_group_start(start, name_end) and
|
||||
result = this.getText().substring(start + 4, name_end - 1)
|
||||
)
|
||||
}
|
||||
|
||||
/** Whether the text in the range start, end is a group and can match the empty string. */
|
||||
predicate zeroWidthMatch(int start, int end) {
|
||||
this.emptyGroup(start, end)
|
||||
or
|
||||
this.negativeAssertionGroup(start, end)
|
||||
or
|
||||
this.positiveLookaheadAssertionGroup(start, end)
|
||||
or
|
||||
this.positiveLookbehindAssertionGroup(start, end)
|
||||
}
|
||||
|
||||
/** Holds if an empty group is found between `start` and `end`. */
|
||||
predicate emptyGroup(int start, int end) {
|
||||
exists(int endm1 | end = endm1 + 1 |
|
||||
this.group_start(start, endm1) and
|
||||
this.isGroupEnd(endm1)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate emptyMatchAtStartGroup(int start, int end) {
|
||||
this.emptyGroup(start, end)
|
||||
or
|
||||
this.negativeAssertionGroup(start, end)
|
||||
or
|
||||
this.positiveLookaheadAssertionGroup(start, end)
|
||||
}
|
||||
|
||||
private predicate emptyMatchAtEndGroup(int start, int end) {
|
||||
this.emptyGroup(start, end)
|
||||
or
|
||||
this.negativeAssertionGroup(start, end)
|
||||
or
|
||||
this.positiveLookbehindAssertionGroup(start, end)
|
||||
}
|
||||
|
||||
private predicate negativeAssertionGroup(int start, int end) {
|
||||
exists(int in_start |
|
||||
this.negative_lookahead_assertion_start(start, in_start)
|
||||
or
|
||||
this.negative_lookbehind_assertion_start(start, in_start)
|
||||
|
|
||||
this.groupContents(start, end, in_start, _)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if a negative lookahead is found between `start` and `end` */
|
||||
predicate negativeLookaheadAssertionGroup(int start, int end) {
|
||||
exists(int in_start | this.negative_lookahead_assertion_start(start, in_start) |
|
||||
this.groupContents(start, end, in_start, _)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if a negative lookbehind is found between `start` and `end` */
|
||||
predicate negativeLookbehindAssertionGroup(int start, int end) {
|
||||
exists(int in_start | this.negative_lookbehind_assertion_start(start, in_start) |
|
||||
this.groupContents(start, end, in_start, _)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if a positive lookahead is found between `start` and `end` */
|
||||
predicate positiveLookaheadAssertionGroup(int start, int end) {
|
||||
exists(int in_start | this.lookahead_assertion_start(start, in_start) |
|
||||
this.groupContents(start, end, in_start, _)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if a positive lookbehind is found between `start` and `end` */
|
||||
predicate positiveLookbehindAssertionGroup(int start, int end) {
|
||||
exists(int in_start | this.lookbehind_assertion_start(start, in_start) |
|
||||
this.groupContents(start, end, in_start, _)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate group_start(int start, int end) {
|
||||
this.non_capturing_group_start(start, end)
|
||||
or
|
||||
this.flag_group_start(start, end, _)
|
||||
or
|
||||
this.named_group_start(start, end)
|
||||
or
|
||||
this.named_backreference_start(start, end)
|
||||
or
|
||||
this.lookahead_assertion_start(start, end)
|
||||
or
|
||||
this.negative_lookahead_assertion_start(start, end)
|
||||
or
|
||||
this.lookbehind_assertion_start(start, end)
|
||||
or
|
||||
this.negative_lookbehind_assertion_start(start, end)
|
||||
or
|
||||
this.comment_group_start(start, end)
|
||||
or
|
||||
this.simple_group_start(start, end)
|
||||
}
|
||||
|
||||
private predicate non_capturing_group_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = ":" and
|
||||
end = start + 3
|
||||
}
|
||||
|
||||
private predicate simple_group_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) != "?" and
|
||||
end = start + 1
|
||||
}
|
||||
|
||||
private predicate named_group_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "P" and
|
||||
this.getChar(start + 3) = "<" and
|
||||
not this.getChar(start + 4) = "=" and
|
||||
not this.getChar(start + 4) = "!" and
|
||||
exists(int name_end |
|
||||
name_end = min(int i | i > start + 4 and this.getChar(i) = ">") and
|
||||
end = name_end + 1
|
||||
)
|
||||
}
|
||||
|
||||
private predicate named_backreference_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "P" and
|
||||
this.getChar(start + 3) = "=" and
|
||||
// Should this be looking for unescaped ")"?
|
||||
// TODO: test this
|
||||
end = min(int i | i > start + 4 and this.getChar(i) = "?")
|
||||
}
|
||||
|
||||
private predicate flag_group_start(int start, int end, string c) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
end = start + 3 and
|
||||
c = this.getChar(start + 2) and
|
||||
c in ["i", "L", "m", "s", "u", "x"]
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the mode of this regular expression string if
|
||||
* it is defined by a prefix.
|
||||
*/
|
||||
string getModeFromPrefix() {
|
||||
exists(string c | this.flag_group_start(_, _, c) |
|
||||
c = "i" and result = "IGNORECASE"
|
||||
or
|
||||
c = "L" and result = "LOCALE"
|
||||
or
|
||||
c = "m" and result = "MULTILINE"
|
||||
or
|
||||
c = "s" and result = "DOTALL"
|
||||
or
|
||||
c = "u" and result = "UNICODE"
|
||||
or
|
||||
c = "x" and result = "VERBOSE"
|
||||
)
|
||||
}
|
||||
|
||||
private predicate lookahead_assertion_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "=" and
|
||||
end = start + 3
|
||||
}
|
||||
|
||||
private predicate negative_lookahead_assertion_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "!" and
|
||||
end = start + 3
|
||||
}
|
||||
|
||||
private predicate lookbehind_assertion_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "<" and
|
||||
this.getChar(start + 3) = "=" and
|
||||
end = start + 4
|
||||
}
|
||||
|
||||
private predicate negative_lookbehind_assertion_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "<" and
|
||||
this.getChar(start + 3) = "!" and
|
||||
end = start + 4
|
||||
}
|
||||
|
||||
private predicate comment_group_start(int start, int end) {
|
||||
this.isGroupStart(start) and
|
||||
this.getChar(start + 1) = "?" and
|
||||
this.getChar(start + 2) = "#" and
|
||||
end = start + 3
|
||||
}
|
||||
|
||||
predicate groupContents(int start, int end, int in_start, int in_end) {
|
||||
this.group_start(start, in_start) and
|
||||
end = in_end + 1 and
|
||||
this.top_level(in_start, in_end) and
|
||||
this.isGroupEnd(in_end)
|
||||
}
|
||||
|
||||
private predicate named_backreference(int start, int end, string name) {
|
||||
this.named_backreference_start(start, start + 4) and
|
||||
end = min(int i | i > start + 4 and this.getChar(i) = ")") + 1 and
|
||||
name = this.getText().substring(start + 4, end - 2)
|
||||
}
|
||||
|
||||
private predicate numbered_backreference(int start, int end, int value) {
|
||||
this.escapingChar(start) and
|
||||
// starting with 0 makes it an octal escape
|
||||
not this.getChar(start + 1) = "0" and
|
||||
exists(string text, string svalue, int len |
|
||||
end = start + len and
|
||||
text = this.getText() and
|
||||
len in [2 .. 3]
|
||||
|
|
||||
svalue = text.substring(start + 1, start + len) and
|
||||
value = svalue.toInt() and
|
||||
// value is composed of digits
|
||||
forall(int i | i in [start + 1 .. start + len - 1] | this.getChar(i) = [0 .. 9].toString()) and
|
||||
// a longer reference is not possible
|
||||
not (
|
||||
len = 2 and
|
||||
exists(text.substring(start + 1, start + len + 1).toInt())
|
||||
) and
|
||||
// 3 octal digits makes it an octal escape
|
||||
not forall(int i | i in [start + 1 .. start + 4] | this.isOctal(i))
|
||||
// TODO: Inside a character set, all numeric escapes are treated as characters.
|
||||
)
|
||||
}
|
||||
|
||||
/** Whether the text in the range start,end is a back reference */
|
||||
predicate backreference(int start, int end) {
|
||||
this.numbered_backreference(start, end, _)
|
||||
or
|
||||
this.named_backreference(start, end, _)
|
||||
}
|
||||
|
||||
/** Gets the number of the back reference in start,end */
|
||||
int getBackrefNumber(int start, int end) { this.numbered_backreference(start, end, result) }
|
||||
|
||||
/** Gets the name, if it has one, of the back reference in start,end */
|
||||
string getBackrefName(int start, int end) { this.named_backreference(start, end, result) }
|
||||
|
||||
private predicate baseItem(int start, int end) {
|
||||
this.character(start, end) and
|
||||
not exists(int x, int y | this.charSet(x, y) and x <= start and y >= end)
|
||||
or
|
||||
this.group(start, end)
|
||||
or
|
||||
this.charSet(start, end)
|
||||
or
|
||||
this.backreference(start, end)
|
||||
}
|
||||
|
||||
private predicate qualifier(int start, int end, boolean maybe_empty, boolean may_repeat_forever) {
|
||||
this.short_qualifier(start, end, maybe_empty, may_repeat_forever) and
|
||||
not this.getChar(end) = "?"
|
||||
or
|
||||
exists(int short_end | this.short_qualifier(start, short_end, maybe_empty, may_repeat_forever) |
|
||||
if this.getChar(short_end) = "?" then end = short_end + 1 else end = short_end
|
||||
)
|
||||
}
|
||||
|
||||
private predicate short_qualifier(
|
||||
int start, int end, boolean maybe_empty, boolean may_repeat_forever
|
||||
) {
|
||||
(
|
||||
this.getChar(start) = "+" and maybe_empty = false and may_repeat_forever = true
|
||||
or
|
||||
this.getChar(start) = "*" and maybe_empty = true and may_repeat_forever = true
|
||||
or
|
||||
this.getChar(start) = "?" and maybe_empty = true and may_repeat_forever = false
|
||||
) and
|
||||
end = start + 1
|
||||
or
|
||||
exists(string lower, string upper |
|
||||
this.multiples(start, end, lower, upper) and
|
||||
(if lower = "" or lower.toInt() = 0 then maybe_empty = true else maybe_empty = false) and
|
||||
if upper = "" then may_repeat_forever = true else may_repeat_forever = false
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a repetition quantifier is found between `start` and `end`,
|
||||
* with the given lower and upper bounds. If a bound is omitted, the corresponding
|
||||
* string is empty.
|
||||
*/
|
||||
predicate multiples(int start, int end, string lower, string upper) {
|
||||
exists(string text, string match, string inner |
|
||||
text = this.getText() and
|
||||
end = start + match.length() and
|
||||
inner = match.substring(1, match.length() - 1)
|
||||
|
|
||||
match = text.regexpFind("\\{[0-9]+\\}", _, start) and
|
||||
lower = inner and
|
||||
upper = lower
|
||||
or
|
||||
match = text.regexpFind("\\{[0-9]*,[0-9]*\\}", _, start) and
|
||||
exists(int commaIndex |
|
||||
commaIndex = inner.indexOf(",") and
|
||||
lower = inner.prefix(commaIndex) and
|
||||
upper = inner.suffix(commaIndex + 1)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the text in the range start,end is a qualified item, where item is a character,
|
||||
* a character set or a group.
|
||||
*/
|
||||
predicate qualifiedItem(int start, int end, boolean maybe_empty, boolean may_repeat_forever) {
|
||||
this.qualifiedPart(start, _, end, maybe_empty, may_repeat_forever)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a qualified part is found between `start` and `part_end` and the qualifier is
|
||||
* found between `part_end` and `end`.
|
||||
*
|
||||
* `maybe_empty` is true if the part is optional.
|
||||
* `may_repeat_forever` is true if the part may be repeated unboundedly.
|
||||
*/
|
||||
predicate qualifiedPart(
|
||||
int start, int part_end, int end, boolean maybe_empty, boolean may_repeat_forever
|
||||
) {
|
||||
this.baseItem(start, part_end) and
|
||||
this.qualifier(part_end, end, maybe_empty, may_repeat_forever)
|
||||
}
|
||||
|
||||
/** Holds if the range `start`, `end` contains a character, a quantifier, a character set or a group. */
|
||||
predicate item(int start, int end) {
|
||||
this.qualifiedItem(start, end, _, _)
|
||||
or
|
||||
this.baseItem(start, end) and not this.qualifier(end, _, _, _)
|
||||
}
|
||||
|
||||
private predicate subsequence(int start, int end) {
|
||||
(
|
||||
start = 0 or
|
||||
this.group_start(_, start) or
|
||||
this.isOptionDivider(start - 1)
|
||||
) and
|
||||
this.item(start, end)
|
||||
or
|
||||
exists(int mid |
|
||||
this.subsequence(start, mid) and
|
||||
this.item(mid, end)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the text in the range start,end is a sequence of 1 or more items, where an item is a character,
|
||||
* a character set or a group.
|
||||
*/
|
||||
predicate sequence(int start, int end) {
|
||||
this.sequenceOrQualified(start, end) and
|
||||
not this.qualifiedItem(start, end, _, _)
|
||||
}
|
||||
|
||||
private predicate sequenceOrQualified(int start, int end) {
|
||||
this.subsequence(start, end) and
|
||||
not this.item_start(end)
|
||||
}
|
||||
|
||||
private predicate item_start(int start) {
|
||||
this.character(start, _) or
|
||||
this.isGroupStart(start) or
|
||||
this.charSet(start, _) or
|
||||
this.backreference(start, _)
|
||||
}
|
||||
|
||||
private predicate item_end(int end) {
|
||||
this.character(_, end)
|
||||
or
|
||||
exists(int endm1 | this.isGroupEnd(endm1) and end = endm1 + 1)
|
||||
or
|
||||
this.charSet(_, end)
|
||||
or
|
||||
this.qualifier(_, end, _, _)
|
||||
}
|
||||
|
||||
private predicate top_level(int start, int end) {
|
||||
this.subalternation(start, end, _) and
|
||||
not this.isOptionDivider(end)
|
||||
}
|
||||
|
||||
private predicate subalternation(int start, int end, int item_start) {
|
||||
this.sequenceOrQualified(start, end) and
|
||||
not this.isOptionDivider(start - 1) and
|
||||
item_start = start
|
||||
or
|
||||
start = end and
|
||||
not this.item_end(start) and
|
||||
this.isOptionDivider(end) and
|
||||
item_start = start
|
||||
or
|
||||
exists(int mid |
|
||||
this.subalternation(start, mid, _) and
|
||||
this.isOptionDivider(mid) and
|
||||
item_start = mid + 1
|
||||
|
|
||||
this.sequenceOrQualified(item_start, end)
|
||||
or
|
||||
not this.item_start(end) and end = item_start
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the text in the range start,end is an alternation
|
||||
*/
|
||||
predicate alternation(int start, int end) {
|
||||
this.top_level(start, end) and
|
||||
exists(int less | this.subalternation(start, less, _) and less < end)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the text in the range start,end is an alternation and the text in part_start, part_end is one of the
|
||||
* options in that alternation.
|
||||
*/
|
||||
predicate alternationOption(int start, int end, int part_start, int part_end) {
|
||||
this.alternation(start, end) and
|
||||
this.subalternation(start, part_end, part_start)
|
||||
}
|
||||
|
||||
/** A part of the regex that may match the start of the string. */
|
||||
private predicate firstPart(int start, int end) {
|
||||
start = 0 and end = this.getText().length()
|
||||
or
|
||||
exists(int x | this.firstPart(x, end) |
|
||||
this.emptyMatchAtStartGroup(x, start) or
|
||||
this.qualifiedItem(x, start, true, _) or
|
||||
this.specialCharacter(x, start, "^")
|
||||
)
|
||||
or
|
||||
exists(int y | this.firstPart(start, y) |
|
||||
this.item(start, end)
|
||||
or
|
||||
this.qualifiedPart(start, end, y, _, _)
|
||||
)
|
||||
or
|
||||
exists(int x, int y | this.firstPart(x, y) |
|
||||
this.groupContents(x, y, start, end)
|
||||
or
|
||||
this.alternationOption(x, y, start, end)
|
||||
)
|
||||
}
|
||||
|
||||
/** A part of the regex that may match the end of the string. */
|
||||
private predicate lastPart(int start, int end) {
|
||||
start = 0 and end = this.getText().length()
|
||||
or
|
||||
exists(int y | this.lastPart(start, y) |
|
||||
this.emptyMatchAtEndGroup(end, y)
|
||||
or
|
||||
this.qualifiedItem(end, y, true, _)
|
||||
or
|
||||
this.specialCharacter(end, y, "$")
|
||||
or
|
||||
y = end + 2 and this.escapingChar(end) and this.getChar(end + 1) = "Z"
|
||||
)
|
||||
or
|
||||
exists(int x |
|
||||
this.lastPart(x, end) and
|
||||
this.item(start, end)
|
||||
)
|
||||
or
|
||||
exists(int y | this.lastPart(start, y) | this.qualifiedPart(start, end, y, _, _))
|
||||
or
|
||||
exists(int x, int y | this.lastPart(x, y) |
|
||||
this.groupContents(x, y, start, end)
|
||||
or
|
||||
this.alternationOption(x, y, start, end)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the item at [start, end) is one of the first items
|
||||
* to be matched.
|
||||
*/
|
||||
predicate firstItem(int start, int end) {
|
||||
(
|
||||
this.character(start, end)
|
||||
or
|
||||
this.qualifiedItem(start, end, _, _)
|
||||
or
|
||||
this.charSet(start, end)
|
||||
) and
|
||||
this.firstPart(start, end)
|
||||
}
|
||||
|
||||
/**
|
||||
* Whether the item at [start, end) is one of the last items
|
||||
* to be matched.
|
||||
*/
|
||||
predicate lastItem(int start, int end) {
|
||||
(
|
||||
this.character(start, end)
|
||||
or
|
||||
this.qualifiedItem(start, end, _, _)
|
||||
or
|
||||
this.charSet(start, end)
|
||||
) and
|
||||
this.lastPart(start, end)
|
||||
}
|
||||
}
|
||||
|
||||
/** A string literal used as a regular expression */
|
||||
class Regex extends RegexString {
|
||||
Regex() { used_as_regex(this, _) }
|
||||
|
||||
/**
|
||||
* Gets a mode (if any) of this regular expression. Can be any of:
|
||||
* DEBUG
|
||||
* IGNORECASE
|
||||
* LOCALE
|
||||
* MULTILINE
|
||||
* DOTALL
|
||||
* UNICODE
|
||||
* VERBOSE
|
||||
*/
|
||||
string getAMode() {
|
||||
result != "None" and
|
||||
used_as_regex(this, result)
|
||||
or
|
||||
result = this.getModeFromPrefix()
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,342 @@
|
||||
/**
|
||||
* This library implements the analysis described in the following two papers:
|
||||
*
|
||||
* James Kirrage, Asiri Rathnayake, Hayo Thielecke: Static Analysis for
|
||||
* Regular Expression Denial-of-Service Attacks. NSS 2013.
|
||||
* (http://www.cs.bham.ac.uk/~hxt/research/reg-exp-sec.pdf)
|
||||
* Asiri Rathnayake, Hayo Thielecke: Static Analysis for Regular Expression
|
||||
* Exponential Runtime via Substructural Logics. 2014.
|
||||
* (https://www.cs.bham.ac.uk/~hxt/research/redos_full.pdf)
|
||||
*
|
||||
* The basic idea is to search for overlapping cycles in the NFA, that is,
|
||||
* states `q` such that there are two distinct paths from `q` to itself
|
||||
* that consume the same word `w`.
|
||||
*
|
||||
* For any such state `q`, an attack string can be constructed as follows:
|
||||
* concatenate a prefix `v` that takes the NFA to `q` with `n` copies of
|
||||
* the word `w` that leads back to `q` along two different paths, followed
|
||||
* by a suffix `x` that is _not_ accepted in state `q`. A backtracking
|
||||
* implementation will need to explore at least 2^n different ways of going
|
||||
* from `q` back to itself while trying to match the `n` copies of `w`
|
||||
* before finally giving up.
|
||||
*
|
||||
* Now in order to identify overlapping cycles, all we have to do is find
|
||||
* pumpable forks, that is, states `q` that can transition to two different
|
||||
* states `r1` and `r2` on the same input symbol `c`, such that there are
|
||||
* paths from both `r1` and `r2` to `q` that consume the same word. The latter
|
||||
* condition is equivalent to saying that `(q, q)` is reachable from `(r1, r2)`
|
||||
* in the product NFA.
|
||||
*
|
||||
* This is what the library does. It makes a simple attempt to construct a
|
||||
* prefix `v` leading into `q`, but only to improve the alert message.
|
||||
* And the library tries to prove the existence of a suffix that ensures
|
||||
* rejection. This check might fail, which can cause false positives.
|
||||
*
|
||||
* Finally, sometimes it depends on the translation whether the NFA generated
|
||||
* for a regular expression has a pumpable fork or not. We implement one
|
||||
* particular translation, which may result in false positives or negatives
|
||||
* relative to some particular JavaScript engine.
|
||||
*
|
||||
* More precisely, the library constructs an NFA from a regular expression `r`
|
||||
* as follows:
|
||||
*
|
||||
* * Every sub-term `t` gives rise to an NFA state `Match(t,i)`, representing
|
||||
* the state of the automaton before attempting to match the `i`th character in `t`.
|
||||
* * There is one accepting state `Accept(r)`.
|
||||
* * There is a special `AcceptAnySuffix(r)` state, which accepts any suffix string
|
||||
* by using an epsilon transition to `Accept(r)` and an any transition to itself.
|
||||
* * Transitions between states may be labelled with epsilon, or an abstract
|
||||
* input symbol.
|
||||
* * Each abstract input symbol represents a set of concrete input characters:
|
||||
* either a single character, a set of characters represented by a
|
||||
* character class, or the set of all characters.
|
||||
* * The product automaton is constructed lazily, starting with pair states
|
||||
* `(q, q)` where `q` is a fork, and proceding along an over-approximate
|
||||
* step relation.
|
||||
* * The over-approximate step relation allows transitions along pairs of
|
||||
* abstract input symbols where the symbols have overlap in the characters they accept.
|
||||
* * Once a trace of pairs of abstract input symbols that leads from a fork
|
||||
* back to itself has been identified, we attempt to construct a concrete
|
||||
* string corresponding to it, which may fail.
|
||||
* * Lastly we ensure that any state reached by repeating `n` copies of `w` has
|
||||
* a suffix `x` (possible empty) that is most likely __not__ accepted.
|
||||
*/
|
||||
|
||||
import ReDoSUtil
|
||||
|
||||
/**
|
||||
* Holds if state `s` might be inside a backtracking repetition.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate stateInsideBacktracking(State s) {
|
||||
s.getRepr().getParent*() instanceof MaybeBacktrackingRepetition
|
||||
}
|
||||
|
||||
/**
|
||||
* A infinitely repeating quantifier that might backtrack.
|
||||
*/
|
||||
private class MaybeBacktrackingRepetition extends InfiniteRepetitionQuantifier {
|
||||
MaybeBacktrackingRepetition() {
|
||||
exists(RegExpTerm child |
|
||||
child instanceof RegExpAlt or
|
||||
child instanceof RegExpQuantifier
|
||||
|
|
||||
child.getParent+() = this
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* A state in the product automaton.
|
||||
*/
|
||||
private newtype TStatePair =
|
||||
/**
|
||||
* We lazily only construct those states that we are actually
|
||||
* going to need: `(q, q)` for every fork state `q`, and any
|
||||
* pair of states that can be reached from a pair that we have
|
||||
* already constructed. To cut down on the number of states,
|
||||
* we only represent states `(q1, q2)` where `q1` is lexicographically
|
||||
* no bigger than `q2`.
|
||||
*
|
||||
* States are only constructed if both states in the pair are
|
||||
* inside a repetition that might backtrack.
|
||||
*/
|
||||
MkStatePair(State q1, State q2) {
|
||||
isFork(q1, _, _, _, _) and q2 = q1
|
||||
or
|
||||
(step(_, _, _, q1, q2) or step(_, _, _, q2, q1)) and
|
||||
rankState(q1) <= rankState(q2)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a unique number for a `state`.
|
||||
* Is used to create an ordering of states, where states with the same `toString()` will be ordered differently.
|
||||
*/
|
||||
private int rankState(State state) {
|
||||
state =
|
||||
rank[result](State s, Location l |
|
||||
l = s.getRepr().getLocation()
|
||||
|
|
||||
s order by l.getStartLine(), l.getStartColumn(), s.toString()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A state in the product automaton.
|
||||
*/
|
||||
private class StatePair extends TStatePair {
|
||||
State q1;
|
||||
State q2;
|
||||
|
||||
StatePair() { this = MkStatePair(q1, q2) }
|
||||
|
||||
/** Gets a textual representation of this element. */
|
||||
string toString() { result = "(" + q1 + ", " + q2 + ")" }
|
||||
|
||||
/** Gets the first component of the state pair. */
|
||||
State getLeft() { result = q1 }
|
||||
|
||||
/** Gets the second component of the state pair. */
|
||||
State getRight() { result = q2 }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds for all constructed state pairs.
|
||||
*
|
||||
* Used in `statePairDist`
|
||||
*/
|
||||
private predicate isStatePair(StatePair p) { any() }
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to the corresponding
|
||||
* components of `r`.
|
||||
*
|
||||
* Used in `statePairDist`
|
||||
*/
|
||||
private predicate delta2(StatePair q, StatePair r) { step(q, _, _, r) }
|
||||
|
||||
/**
|
||||
* Gets the minimum length of a path from `q` to `r` in the
|
||||
* product automaton.
|
||||
*/
|
||||
private int statePairDist(StatePair q, StatePair r) =
|
||||
shortestDistances(isStatePair/1, delta2/2)(q, r, result)
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from `q` to `r1` and from `q` to `r2`
|
||||
* labelled with `s1` and `s2`, respectively, where `s1` and `s2` do not
|
||||
* trivially have an empty intersection.
|
||||
*
|
||||
* This predicate only holds for states associated with regular expressions
|
||||
* that have at least one repetition quantifier in them (otherwise the
|
||||
* expression cannot be vulnerable to ReDoS attacks anyway).
|
||||
*/
|
||||
pragma[noopt]
|
||||
private predicate isFork(State q, InputSymbol s1, InputSymbol s2, State r1, State r2) {
|
||||
stateInsideBacktracking(q) and
|
||||
exists(State q1, State q2 |
|
||||
q1 = epsilonSucc*(q) and
|
||||
delta(q1, s1, r1) and
|
||||
q2 = epsilonSucc*(q) and
|
||||
delta(q2, s2, r2) and
|
||||
// Use pragma[noopt] to prevent intersect(s1,s2) from being the starting point of the join.
|
||||
// From (s1,s2) it would find a huge number of intermediate state pairs (q1,q2) originating from different literals,
|
||||
// and discover at the end that no `q` can reach both `q1` and `q2` by epsilon transitions.
|
||||
exists(intersect(s1, s2))
|
||||
|
|
||||
s1 != s2
|
||||
or
|
||||
r1 != r2
|
||||
or
|
||||
r1 = r2 and q1 != q2
|
||||
or
|
||||
// If q can reach itself by epsilon transitions, then there are two distinct paths to the q1/q2 state:
|
||||
// one that uses the loop and one that doesn't. The engine will separately attempt to match with each path,
|
||||
// despite ending in the same state. The "fork" thus arises from the choice of whether to use the loop or not.
|
||||
// To avoid every state in the loop becoming a fork state,
|
||||
// we arbitrarily pick the InfiniteRepetitionQuantifier state as the canonical fork state for the loop
|
||||
// (every epsilon-loop must contain such a state).
|
||||
//
|
||||
// We additionally require that the there exists another InfiniteRepetitionQuantifier `mid` on the path from `q` to itself.
|
||||
// This is done to avoid flagging regular expressions such as `/(a?)*b/` - that only has polynomial runtime, and is detected by `js/polynomial-redos`.
|
||||
// The below code is therefore a heuritic, that only flags regular expressions such as `/(a*)*b/`,
|
||||
// and does not flag regular expressions such as `/(a?b?)c/`, but the latter pattern is not used frequently.
|
||||
r1 = r2 and
|
||||
q1 = q2 and
|
||||
epsilonSucc+(q) = q and
|
||||
exists(RegExpTerm term | term = q.getRepr() | term instanceof InfiniteRepetitionQuantifier) and
|
||||
// One of the mid states is an infinite quantifier itself
|
||||
exists(State mid, RegExpTerm term |
|
||||
mid = epsilonSucc+(q) and
|
||||
term = mid.getRepr() and
|
||||
term instanceof InfiniteRepetitionQuantifier and
|
||||
q = epsilonSucc+(mid) and
|
||||
not mid = q
|
||||
)
|
||||
) and
|
||||
stateInsideBacktracking(r1) and
|
||||
stateInsideBacktracking(r2)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the state pair `(q1, q2)` or `(q2, q1)`; note that only
|
||||
* one or the other is defined.
|
||||
*/
|
||||
private StatePair mkStatePair(State q1, State q2) {
|
||||
result = MkStatePair(q1, q2) or result = MkStatePair(q2, q1)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to the corresponding
|
||||
* components of `r` labelled with `s1` and `s2`, respectively.
|
||||
*/
|
||||
private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, StatePair r) {
|
||||
exists(State r1, State r2 | step(q, s1, s2, r1, r2) and r = mkStatePair(r1, r2))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to `r1` and `r2`
|
||||
* labelled with `s1` and `s2`, respectively.
|
||||
*
|
||||
* We only consider transitions where the resulting states `(r1, r2)` are both
|
||||
* inside a repetition that might backtrack.
|
||||
*/
|
||||
pragma[noopt]
|
||||
private predicate step(StatePair q, InputSymbol s1, InputSymbol s2, State r1, State r2) {
|
||||
exists(State q1, State q2 | q.getLeft() = q1 and q.getRight() = q2 |
|
||||
deltaClosed(q1, s1, r1) and
|
||||
deltaClosed(q2, s2, r2) and
|
||||
// use noopt to force the join on `intersect` to happen last.
|
||||
exists(intersect(s1, s2))
|
||||
) and
|
||||
stateInsideBacktracking(r1) and
|
||||
stateInsideBacktracking(r2)
|
||||
}
|
||||
|
||||
private newtype TTrace =
|
||||
Nil() or
|
||||
Step(InputSymbol s1, InputSymbol s2, TTrace t) {
|
||||
exists(StatePair p |
|
||||
isReachableFromFork(_, p, t, _) and
|
||||
step(p, s1, s2, _)
|
||||
)
|
||||
or
|
||||
t = Nil() and isFork(_, s1, s2, _, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* A list of pairs of input symbols that describe a path in the product automaton
|
||||
* starting from some fork state.
|
||||
*/
|
||||
private class Trace extends TTrace {
|
||||
/** Gets a textual representation of this element. */
|
||||
string toString() {
|
||||
this = Nil() and result = "Nil()"
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, Trace t | this = Step(s1, s2, t) |
|
||||
result = "Step(" + s1 + ", " + s2 + ", " + t + ")"
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a string corresponding to the trace `t`.
|
||||
*/
|
||||
private string concretise(Trace t) {
|
||||
t = Nil() and result = ""
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, Trace rest | t = Step(s1, s2, rest) |
|
||||
result = concretise(rest) + intersect(s1, s2)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `r` is reachable from `(fork, fork)` under input `w`, and there is
|
||||
* a path from `r` back to `(fork, fork)` with `rem` steps.
|
||||
*/
|
||||
private predicate isReachableFromFork(State fork, StatePair r, Trace w, int rem) {
|
||||
// base case
|
||||
exists(InputSymbol s1, InputSymbol s2, State q1, State q2 |
|
||||
isFork(fork, s1, s2, q1, q2) and
|
||||
r = MkStatePair(q1, q2) and
|
||||
w = Step(s1, s2, Nil()) and
|
||||
rem = statePairDist(r, MkStatePair(fork, fork))
|
||||
)
|
||||
or
|
||||
// recursive case
|
||||
exists(StatePair p, Trace v, InputSymbol s1, InputSymbol s2 |
|
||||
isReachableFromFork(fork, p, v, rem + 1) and
|
||||
step(p, s1, s2, r) and
|
||||
w = Step(s1, s2, v) and
|
||||
rem >= statePairDist(r, MkStatePair(fork, fork))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a state in the product automaton from which `(fork, fork)` is
|
||||
* reachable in zero or more epsilon transitions.
|
||||
*/
|
||||
private StatePair getAForkPair(State fork) {
|
||||
isFork(fork, _, _, _, _) and
|
||||
result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `fork` is a pumpable fork with word `w`.
|
||||
*/
|
||||
private predicate isPumpable(State fork, string w) {
|
||||
exists(StatePair q, Trace t |
|
||||
isReachableFromFork(fork, q, t, _) and
|
||||
q = getAForkPair(fork) and
|
||||
w = concretise(t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* An instantiation of `ReDoSConfiguration` for exponential backtracking.
|
||||
*/
|
||||
class ExponentialReDoSConfiguration extends ReDoSConfiguration {
|
||||
ExponentialReDoSConfiguration() { this = "ExponentialReDoSConfiguration" }
|
||||
|
||||
override predicate isReDoSCandidate(State state, string pump) { isPumpable(state, pump) }
|
||||
}
|
||||
1135
java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll
Normal file
1135
java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll
Normal file
File diff suppressed because it is too large
Load Diff
@@ -0,0 +1,49 @@
|
||||
/**
|
||||
* This module should provide a class hierarchy corresponding to a parse tree of regular expressions.
|
||||
*/
|
||||
|
||||
import java
|
||||
import semmle.code.java.regex.RegexTreeView
|
||||
|
||||
/**
|
||||
* Holds if the regular expression should not be considered.
|
||||
*
|
||||
* We make the pragmatic performance optimization to ignore regular expressions in files
|
||||
* that does not belong to the project code (such as installed dependencies).
|
||||
*/
|
||||
predicate isExcluded(RegExpParent parent) {
|
||||
not exists(parent.getRegex().getLocation().getFile().getRelativePath())
|
||||
or
|
||||
// Regexes with many occurrences of ".*" may cause the polynomial ReDoS computation to explode, so
|
||||
// we explicitly exclude these.
|
||||
count(int i | exists(parent.getRegex().getText().regexpFind("\\.\\*", i, _)) | i) > 10
|
||||
}
|
||||
|
||||
/**
|
||||
* A module containing predicates for determining which flags a regular expression have.
|
||||
*/
|
||||
module RegExpFlags {
|
||||
/**
|
||||
* Holds if `root` has the `i` flag for case-insensitive matching.
|
||||
*/
|
||||
predicate isIgnoreCase(RegExpTerm root) {
|
||||
root.isRootTerm() and
|
||||
root.getLiteral().isIgnoreCase()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the flags for `root`, or the empty string if `root` has no flags.
|
||||
*/
|
||||
string getFlags(RegExpTerm root) {
|
||||
root.isRootTerm() and
|
||||
result = root.getLiteral().getFlags()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `root` has the `s` flag for multi-line matching.
|
||||
*/
|
||||
predicate isDotAll(RegExpTerm root) {
|
||||
root.isRootTerm() and
|
||||
root.getLiteral().isDotAll()
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,420 @@
|
||||
/**
|
||||
* Provides classes for working with regular expressions that can
|
||||
* perform backtracking in superlinear time.
|
||||
*/
|
||||
|
||||
import ReDoSUtil
|
||||
|
||||
/*
|
||||
* This module implements the analysis described in the paper:
|
||||
* Valentin Wustholz, Oswaldo Olivo, Marijn J. H. Heule, and Isil Dillig:
|
||||
* Static Detection of DoS Vulnerabilities in
|
||||
* Programs that use Regular Expressions
|
||||
* (Extended Version).
|
||||
* (https://arxiv.org/pdf/1701.04045.pdf)
|
||||
*
|
||||
* 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 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)`,
|
||||
* and search for a series of transitions (a `Trace`), such that we end
|
||||
* at `(pivot, succ, succ)` (see `isReachableFromStartTuple`).
|
||||
*
|
||||
* For example, consider the regular expression `/^\d*5\w*$/`.
|
||||
* The search will start at the tuple `(\d*, \d*, \w*)` and search
|
||||
* for a path to `(\d*, \w*, \w*)`.
|
||||
* This path exists, and consists of a single transition in the product automaton,
|
||||
* where the three corresponding NFA edges all match the character `"5"`.
|
||||
*
|
||||
* The start-state in the NFA has an any-transition to itself, this allows us to
|
||||
* flag regular expressions such as `/a*$/` - which does not have a start anchor -
|
||||
* and can thus start matching anywhere.
|
||||
*
|
||||
* The implementation is not perfect.
|
||||
* It has the same suffix detection issue as the `js/redos` query, which can cause false positives.
|
||||
* It also doesn't find all transitions in the product automaton, which can cause false negatives.
|
||||
*/
|
||||
|
||||
/**
|
||||
* An instantiaion of `ReDoSConfiguration` for superlinear ReDoS.
|
||||
*/
|
||||
class SuperLinearReDoSConfiguration extends ReDoSConfiguration {
|
||||
SuperLinearReDoSConfiguration() { this = "SuperLinearReDoSConfiguration" }
|
||||
|
||||
override predicate isReDoSCandidate(State state, string pump) { isPumpable(_, state, pump) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets any root (start) state of a regular expression.
|
||||
*/
|
||||
private State getRootState() { result = mkMatch(any(RegExpRoot r)) }
|
||||
|
||||
private newtype TStateTuple =
|
||||
MkStateTuple(State q1, State q2, State q3) {
|
||||
// starts at (pivot, pivot, succ)
|
||||
isStartLoops(q1, q3) and q1 = q2
|
||||
or
|
||||
step(_, _, _, _, q1, q2, q3) and FeasibleTuple::isFeasibleTuple(q1, q2, q3)
|
||||
}
|
||||
|
||||
/**
|
||||
* A state in the product automaton.
|
||||
* The product automaton contains 3-tuples of states.
|
||||
*
|
||||
* We lazily only construct those states that we are actually
|
||||
* going to need.
|
||||
* Either a start state `(pivot, pivot, succ)`, or a state
|
||||
* where there exists a transition from an already existing state.
|
||||
*
|
||||
* The exponential variant of this query (`js/redos`) uses an optimization
|
||||
* trick where `q1 <= q2`. This trick cannot be used here as the order
|
||||
* of the elements matter.
|
||||
*/
|
||||
class StateTuple extends TStateTuple {
|
||||
State q1;
|
||||
State q2;
|
||||
State q3;
|
||||
|
||||
StateTuple() { this = MkStateTuple(q1, q2, q3) }
|
||||
|
||||
/**
|
||||
* Gest a string repesentation of this tuple.
|
||||
*/
|
||||
string toString() { result = "(" + q1 + ", " + q2 + ", " + q3 + ")" }
|
||||
|
||||
/**
|
||||
* Holds if this tuple is `(r1, r2, r3)`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate isTuple(State r1, State r2, State r3) { r1 = q1 and r2 = q2 and r3 = q3 }
|
||||
}
|
||||
|
||||
/**
|
||||
* A module for determining feasible tuples for the product automaton.
|
||||
*
|
||||
* The implementation is split into many predicates for performance reasons.
|
||||
*/
|
||||
private module FeasibleTuple {
|
||||
/**
|
||||
* Holds if the tuple `(r1, r2, r3)` might be on path from a start-state to an end-state in the product automaton.
|
||||
*/
|
||||
pragma[inline]
|
||||
predicate isFeasibleTuple(State r1, State r2, State r3) {
|
||||
// The first element is either inside a repetition (or the start state itself)
|
||||
isRepetitionOrStart(r1) and
|
||||
// The last element is inside a repetition
|
||||
stateInsideRepetition(r3) and
|
||||
// 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).
|
||||
canReachABeginning(r1) and
|
||||
// The last element can reach a target (the "succ" state in a `(pivot, succ)` pair).
|
||||
canReachATarget(r3)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `s` is either inside a repetition, or is the start state (which is a repetition).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate isRepetitionOrStart(State s) { stateInsideRepetition(s) or s = getRootState() }
|
||||
|
||||
/**
|
||||
* Holds if state `s` might be inside a backtracking repetition.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate stateInsideRepetition(State s) {
|
||||
s.getRepr().getParent*() instanceof InfiniteRepetitionQuantifier
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a path in the NFA from `s` to a "pivot" state
|
||||
* (from a `(pivot, succ)` pair that starts the search).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate canReachABeginning(State s) {
|
||||
delta+(s) = any(State pivot | isStartLoops(pivot, _))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a path in the NFA from `s` to a "succ" state
|
||||
* (from a `(pivot, succ)` pair that starts the search).
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate canReachATarget(State s) { delta+(s) = any(State succ | isStartLoops(_, succ)) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `pivot` and `succ` 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.
|
||||
*/
|
||||
predicate isStartLoops(State pivot, State succ) {
|
||||
pivot != succ and
|
||||
succ.getRepr() instanceof InfiniteRepetitionQuantifier and
|
||||
delta+(pivot) = succ and
|
||||
(
|
||||
pivot.getRepr() instanceof InfiniteRepetitionQuantifier
|
||||
or
|
||||
pivot = mkMatch(any(RegExpRoot root))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a state for which there exists a transition in the NFA from `s'.
|
||||
*/
|
||||
State delta(State s) { delta(s, _, result) }
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to the corresponding
|
||||
* components of `r` labelled with `s1`, `s2`, and `s3`, respectively.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate step(StateTuple q, InputSymbol s1, InputSymbol s2, InputSymbol s3, StateTuple r) {
|
||||
exists(State r1, State r2, State r3 |
|
||||
step(q, s1, s2, s3, r1, r2, r3) and r = MkStateTuple(r1, r2, r3)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there are transitions from the components of `q` to `r1`, `r2`, and `r3
|
||||
* labelled with `s1`, `s2`, and `s3`, respectively.
|
||||
*/
|
||||
pragma[noopt]
|
||||
predicate step(
|
||||
StateTuple q, InputSymbol s1, InputSymbol s2, InputSymbol s3, State r1, State r2, State r3
|
||||
) {
|
||||
exists(State q1, State q2, State q3 | q.isTuple(q1, q2, q3) |
|
||||
deltaClosed(q1, s1, r1) and
|
||||
deltaClosed(q2, s2, r2) and
|
||||
deltaClosed(q3, s3, r3) and
|
||||
// use noopt to force the join on `getAThreewayIntersect` to happen last.
|
||||
exists(getAThreewayIntersect(s1, s2, s3))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a char that is matched by all the edges `s1`, `s2`, and `s3`.
|
||||
*
|
||||
* The result is not complete, and might miss some combination of edges that share some character.
|
||||
*/
|
||||
pragma[noinline]
|
||||
string getAThreewayIntersect(InputSymbol s1, InputSymbol s2, InputSymbol s3) {
|
||||
result = minAndMaxIntersect(s1, s2) and result = [intersect(s2, s3), intersect(s1, s3)]
|
||||
or
|
||||
result = minAndMaxIntersect(s1, s3) and result = [intersect(s2, s3), intersect(s1, s2)]
|
||||
or
|
||||
result = minAndMaxIntersect(s2, s3) and result = [intersect(s1, s2), intersect(s1, s3)]
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the minimum and maximum characters that intersect between `a` and `b`.
|
||||
* This predicate is used to limit the size of `getAThreewayIntersect`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
string minAndMaxIntersect(InputSymbol a, InputSymbol b) {
|
||||
result = [min(intersect(a, b)), max(intersect(a, b))]
|
||||
}
|
||||
|
||||
private newtype TTrace =
|
||||
Nil() or
|
||||
Step(InputSymbol s1, InputSymbol s2, InputSymbol s3, TTrace t) {
|
||||
exists(StateTuple p |
|
||||
isReachableFromStartTuple(_, _, p, t, _) and
|
||||
step(p, s1, s2, s3, _)
|
||||
)
|
||||
or
|
||||
exists(State pivot, State succ | isStartLoops(pivot, succ) |
|
||||
t = Nil() and step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* A list of tuples of input symbols that describe a path in the product automaton
|
||||
* starting from some start state.
|
||||
*/
|
||||
class Trace extends TTrace {
|
||||
/**
|
||||
* Gets a string representation of this Trace that can be used for debug purposes.
|
||||
*/
|
||||
string toString() {
|
||||
this = Nil() and result = "Nil()"
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t | this = Step(s1, s2, s3, t) |
|
||||
result = "Step(" + s1 + ", " + s2 + ", " + s3 + ", " + t + ")"
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a string corresponding to the trace `t`.
|
||||
*/
|
||||
string concretise(Trace t) {
|
||||
t = Nil() and result = ""
|
||||
or
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace rest | t = Step(s1, s2, s3, rest) |
|
||||
result = concretise(rest) + getAThreewayIntersect(s1, s2, s3)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if there exists a transition from `r` to `q` in the product automaton.
|
||||
* Notice that the arguments are flipped, and thus the direction is backwards.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate tupleDeltaBackwards(StateTuple q, StateTuple r) { step(r, _, _, _, q) }
|
||||
|
||||
/**
|
||||
* 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)`.
|
||||
*/
|
||||
predicate isEndTuple(StateTuple tuple) { tuple = getAnEndTuple(_, _) }
|
||||
|
||||
/**
|
||||
* Gets the minimum length of a path from `r` to some an end state `end`.
|
||||
*
|
||||
* The implementation searches backwards from the end-tuple.
|
||||
* This approach was chosen because it is way more efficient if the first predicate given to `shortestDistances` is small.
|
||||
* The `end` argument must always be an end state.
|
||||
*/
|
||||
int distBackFromEnd(StateTuple r, StateTuple end) =
|
||||
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)`,
|
||||
* and a path from a start-state to `tuple` follows the transitions in `trace`.
|
||||
*/
|
||||
predicate isReachableFromStartTuple(State pivot, State succ, StateTuple tuple, Trace trace, int dist) {
|
||||
// base case. The first step is inlined to start the search after all possible 1-steps, and not just the ones with the shortest path.
|
||||
exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, State q1, State q2, State q3 |
|
||||
isStartLoops(pivot, succ) and
|
||||
step(MkStateTuple(pivot, pivot, succ), s1, s2, s3, tuple) and
|
||||
tuple = MkStateTuple(q1, q2, q3) and
|
||||
trace = Step(s1, s2, s3, Nil()) and
|
||||
dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
|
||||
)
|
||||
or
|
||||
// recursive case
|
||||
exists(StateTuple p, Trace v, InputSymbol s1, InputSymbol s2, InputSymbol s3 |
|
||||
isReachableFromStartTuple(pivot, succ, p, v, dist + 1) and
|
||||
dist = isReachableFromStartTupleHelper(pivot, succ, tuple, p, s1, s2, s3) and
|
||||
trace = Step(s1, s2, s3, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Helper predicate for the recursive case in `isReachableFromStartTuple`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private int isReachableFromStartTupleHelper(
|
||||
State pivot, State succ, StateTuple r, StateTuple p, InputSymbol s1, InputSymbol s2,
|
||||
InputSymbol s3
|
||||
) {
|
||||
result = distBackFromEnd(r, MkStateTuple(pivot, succ, succ)) and
|
||||
step(p, s1, s2, s3, r)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the tuple `(pivot, succ, succ)` from the product automaton.
|
||||
*/
|
||||
StateTuple getAnEndTuple(State pivot, State succ) {
|
||||
isStartLoops(pivot, succ) and
|
||||
result = MkStateTuple(pivot, succ, succ)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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`.
|
||||
*
|
||||
* 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.
|
||||
*
|
||||
* This predicate is used by `SuperLinearReDoSConfiguration`, and the final results are
|
||||
* available in the `hasReDoSResult` predicate.
|
||||
*/
|
||||
predicate isPumpable(State pivot, State succ, string pump) {
|
||||
exists(StateTuple q, Trace t |
|
||||
isReachableFromStartTuple(pivot, succ, q, t, _) and
|
||||
q = getAnEndTuple(pivot, succ) and
|
||||
pump = concretise(t)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if repetitions of `pump` at `t` will cause polynomial backtracking.
|
||||
*/
|
||||
predicate polynimalReDoS(RegExpTerm t, string pump, string prefixMsg, RegExpTerm prev) {
|
||||
exists(State s, State pivot |
|
||||
hasReDoSResult(t, pump, s, prefixMsg) and
|
||||
isPumpable(pivot, s, _) and
|
||||
prev = pivot.getRepr()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a message for why `term` can cause polynomial backtracking.
|
||||
*/
|
||||
string getReasonString(RegExpTerm term, string pump, string prefixMsg, RegExpTerm prev) {
|
||||
polynimalReDoS(term, pump, prefixMsg, prev) and
|
||||
result =
|
||||
"Strings " + prefixMsg + "with many repetitions of '" + pump +
|
||||
"' can start matching anywhere after the start of the preceeding " + prev
|
||||
}
|
||||
|
||||
/**
|
||||
* A term that may cause a regular expression engine to perform a
|
||||
* polynomial number of match attempts, relative to the input length.
|
||||
*/
|
||||
class PolynomialBackTrackingTerm extends InfiniteRepetitionQuantifier {
|
||||
string reason;
|
||||
string pump;
|
||||
string prefixMsg;
|
||||
RegExpTerm prev;
|
||||
|
||||
PolynomialBackTrackingTerm() {
|
||||
reason = getReasonString(this, pump, prefixMsg, prev) and
|
||||
// there might be many reasons for this term to have polynomial backtracking - we pick the shortest one.
|
||||
reason = min(string msg | msg = getReasonString(this, _, _, _) | msg order by msg.length(), msg)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if all non-empty successors to the polynomial backtracking term matches the end of the line.
|
||||
*/
|
||||
predicate isAtEndLine() {
|
||||
forall(RegExpTerm succ | this.getSuccessor+() = succ and not matchesEpsilon(succ) |
|
||||
succ instanceof RegExpDollar
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the string that should be repeated to cause this regular expression to perform polynomially.
|
||||
*/
|
||||
string getPumpString() { result = pump }
|
||||
|
||||
/**
|
||||
* Gets a message for which prefix a matching string must start with for this term to cause polynomial backtracking.
|
||||
*/
|
||||
string getPrefixMessage() { result = prefixMsg }
|
||||
|
||||
/**
|
||||
* Gets a predecessor to `this`, which also loops on the pump string, and thereby causes polynomial backtracking.
|
||||
*/
|
||||
RegExpTerm getPreviousLoop() { result = prev }
|
||||
|
||||
/**
|
||||
* Gets the reason for the number of match attempts.
|
||||
*/
|
||||
string getReason() { result = reason }
|
||||
}
|
||||
Reference in New Issue
Block a user