Module Make

Classes and predicates that create an NFA and various algorithms for working with it.

Import path

import codeql.regex.nfa.NfaUtils

Predicates

after	Gets a state the NFA may be in after matching `t`.
delta	Holds if the NFA has a transition from `q1` to `q2` labelled with `lbl`.
deltaClosed	Holds if there is a state `q` that can be reached from `q1` along epsilon edges, such that there is a transition from `q` to `q2` that consumes symbol `s`.
epsilonPred	Gets a state that has an epsilon transition to `q`.
epsilonSucc	Gets a state that `q` has an epsilon transition to.
getAnInputSymbolMatching	Gets a symbol that matches `char`.
getCanonicalCharClass	Gets a char class that represents `term`, even when `term` is not the canonical representative.
getRoot	Gets the root containing the given term, that is, the root of the literal, or a branch of the root disjunction.
getTermLocationString	Gets a string for the full location of `t`.
intersect	Gets a character that is represented by both `c` and `d`.
isStartState	Holds if `state` is a start state.
matchesEpsilon	Holds if `t` matches at least an epsilon symbol.
mkMatch	Gets a state that is about to match the regular expression `t`.

Classes

CharacterClass	An abstract input symbol that represents a character class.
EmptyPositiveSubPattern	A lookahead/lookbehind that matches the empty string.
InputSymbol	An abstract input symbol, representing a set of concrete characters.
RegExpRoot	A branch in a disjunction that is the root node in a literal, or a literal whose root node is not a disjunction.
RelevantRegExpTerm	A regexp term that is relevant for this ReDoS analysis.
State	A state in the NFA corresponding to a regular expression.

Datatypes

TState

A state in the NFA.

Modules

Concretizer	Implements an algorithm for computing all possible strings from following a tree of nodes (as described in `CharTree`).
PrefixConstruction	Predicates for constructing a prefix string that leads to a given state.
ReDoSPruning	A module for pruning candidate ReDoS states. The candidates are specified by the `isCandidate` signature predicate. The candidates are checked for rejecting suffixes and deduplicated, and the resulting ReDoS states are read by the `hasReDoSResult` predicate.

Predicate signatures

isCandidateSig	Holds if `state` is a candidate for ReDoS.
isCandidateSig	Holds if `state` is a candidate for ReDoS with string `pump`.

Module signatures

CharTree

A module that describes a tree where each node has one or more associated characters, also known as a trie. The root node has no associated character. This module is a signature used in Concretizer.

Parameters

TreeImpl

RegexTreeViewSig