diff --git a/python/ql/lib/semmle/python/security/BadTagFilterQuery.qll b/python/ql/lib/semmle/python/security/BadTagFilterQuery.qll
index 95bfbeeeb5d..446e4487a0f 100644
--- a/python/ql/lib/semmle/python/security/BadTagFilterQuery.qll
+++ b/python/ql/lib/semmle/python/security/BadTagFilterQuery.qll
@@ -2,155 +2,7 @@
  * Provides predicates for reasoning about bad tag filter vulnerabilities.
  */
 
-import regexp.RegexpMatching
-
-/**
- * Holds if the regexp `root` should be tested against `str`.
- * Implements the `isRegexpMatchingCandidateSig` signature from `RegexpMatching`.
- * `ignorePrefix` toggles whether the regular expression should be treated as accepting any prefix if it's unanchored.
- * `testWithGroups` toggles whether it's tested which groups are filled by a given input string.
- */
-private predicate isBadTagFilterCandidate(
-  RootTerm root, string str, boolean ignorePrefix, boolean testWithGroups
-) {
-  // the regexp must mention "<" and ">" explicitly.
-  forall(string angleBracket | angleBracket = ["<", ">"] |
-    any(RegExpConstant term | term.getValue().matches("%" + angleBracket + "%")).getRootTerm() =
-      root
-  ) and
-  ignorePrefix = true and
-  (
-    str = ["<!-- foo -->", "<!-- foo --!>", "<!- foo ->", "<foo>", "<script>"] and
-    testWithGroups = true
-    or
-    str =
-      [
-        "<!-- foo -->", "<!- foo ->", "<!-- foo --!>", "<!-- foo\n -->", "<script>foo</script>",
-        "<script \n>foo</script>", "<script >foo\n</script>", "<foo ></foo>", "<foo>",
-        "<foo src=\"foo\"></foo>", "<script>", "<script src=\"foo\"></script>",
-        "<script src='foo'></script>", "<SCRIPT>foo</SCRIPT>", "<script\tsrc=\"foo\"/>",
-        "<script\tsrc='foo'></script>", "<sCrIpT>foo</ScRiPt>", "<script src=\"foo\">foo</script >",
-        "<script src=\"foo\">foo</script foo=\"bar\">", "<script src=\"foo\">foo</script\t\n bar>"
-      ] and
-    testWithGroups = false
-  )
-}
-
-/**
- * A regexp that matches some string from the `isBadTagFilterCandidate` predicate.
- */
-class HtmlMatchingRegExp extends RootTerm {
-  HtmlMatchingRegExp() { RegexpMatching<isBadTagFilterCandidate/4>::matches(this, _) }
-
-  /** Holds if this regexp matched `str`, where `str` is one of the string from `isBadTagFilterCandidate`. */
-  predicate matches(string str) { RegexpMatching<isBadTagFilterCandidate/4>::matches(this, str) }
-
-  /** Holds if this regexp fills capture group `g' when matching `str', where `str` is one of the string from `isBadTagFilterCandidate`. */
-  predicate fillsCaptureGroup(string str, int g) {
-    RegexpMatching<isBadTagFilterCandidate/4>::fillsCaptureGroup(this, str, g)
-  }
-}
-
-/** DEPRECATED: Alias for HtmlMatchingRegExp */
-deprecated class HTMLMatchingRegExp = HtmlMatchingRegExp;
-
-/**
- * Holds if `regexp` matches some HTML tags, but misses some HTML tags that it should match.
- *
- * When adding a new case to this predicate, make sure the test string used in `matches(..)` calls are present in `HTMLMatchingRegExp::test` / `HTMLMatchingRegExp::testWithGroups`.
- */
-predicate isBadRegexpFilter(HtmlMatchingRegExp regexp, string msg) {
-  // CVE-2021-33829 - matching both "<!-- foo -->" and "<!-- foo --!>", but in different capture groups
-  regexp.matches("<!-- foo -->") and
-  regexp.matches("<!-- foo --!>") and
-  exists(int a, int b | a != b |
-    regexp.fillsCaptureGroup("<!-- foo -->", a) and
-    // <!-- foo --> might be ambiguously parsed (matching both capture groups), and that is ok here.
-    regexp.fillsCaptureGroup("<!-- foo --!>", b) and
-    not regexp.fillsCaptureGroup("<!-- foo --!>", a) and
-    msg =
-      "Comments ending with --> are matched differently from comments ending with --!>. The first is matched with capture group "
-        + a + " and comments ending with --!> are matched with capture group " +
-        strictconcat(int i | regexp.fillsCaptureGroup("<!-- foo --!>", i) | i.toString(), ", ") +
-        "."
-  )
-  or
-  // CVE-2020-17480 - matching "<!-- foo -->" and other tags, but not "<!-- foo --!>".
-  exists(int group, int other |
-    group != other and
-    regexp.fillsCaptureGroup("<!-- foo -->", group) and
-    regexp.fillsCaptureGroup("<foo>", other) and
-    not regexp.matches("<!-- foo --!>") and
-    not regexp.fillsCaptureGroup("<!-- foo -->", any(int i | i != group)) and
-    not regexp.fillsCaptureGroup("<!- foo ->", group) and
-    not regexp.fillsCaptureGroup("<foo>", group) and
-    not regexp.fillsCaptureGroup("<script>", group) and
-    msg =
-      "This regular expression only parses --> (capture group " + group +
-        ") and not --!> as an HTML comment end tag."
-  )
-  or
-  regexp.matches("<!-- foo -->") and
-  not regexp.matches("<!-- foo\n -->") and
-  not regexp.matches("<!- foo ->") and
-  not regexp.matches("<foo>") and
-  not regexp.matches("<script>") and
-  msg = "This regular expression does not match comments containing newlines."
-  or
-  regexp.matches("<script>foo</script>") and
-  regexp.matches("<script src=\"foo\"></script>") and
-  not regexp.matches("<foo ></foo>") and
-  (
-    not regexp.matches("<script \n>foo</script>") and
-    msg = "This regular expression matches <script></script>, but not <script \\n></script>"
-    or
-    not regexp.matches("<script >foo\n</script>") and
-    msg = "This regular expression matches <script>...</script>, but not <script >...\\n</script>"
-  )
-  or
-  regexp.matches("<script>foo</script>") and
-  regexp.matches("<script src=\"foo\"></script>") and
-  not regexp.matches("<script src='foo'></script>") and
-  not regexp.matches("<foo>") and
-  msg = "This regular expression does not match script tags where the attribute uses single-quotes."
-  or
-  regexp.matches("<script>foo</script>") and
-  regexp.matches("<script src='foo'></script>") and
-  not regexp.matches("<script src=\"foo\"></script>") and
-  not regexp.matches("<foo>") and
-  msg = "This regular expression does not match script tags where the attribute uses double-quotes."
-  or
-  regexp.matches("<script>foo</script>") and
-  regexp.matches("<script src='foo'></script>") and
-  not regexp.matches("<script\tsrc='foo'></script>") and
-  not regexp.matches("<foo>") and
-  not regexp.matches("<foo src=\"foo\"></foo>") and
-  msg = "This regular expression does not match script tags where tabs are used between attributes."
-  or
-  regexp.matches("<script>foo</script>") and
-  not RegExpFlags::isIgnoreCase(regexp) and
-  not regexp.matches("<foo>") and
-  not regexp.matches("<foo ></foo>") and
-  (
-    not regexp.matches("<SCRIPT>foo</SCRIPT>") and
-    msg = "This regular expression does not match upper case <SCRIPT> tags."
-    or
-    not regexp.matches("<sCrIpT>foo</ScRiPt>") and
-    regexp.matches("<SCRIPT>foo</SCRIPT>") and
-    msg = "This regular expression does not match mixed case <sCrIpT> tags."
-  )
-  or
-  regexp.matches("<script src=\"foo\"></script>") and
-  not regexp.matches("<foo>") and
-  not regexp.matches("<foo ></foo>") and
-  (
-    not regexp.matches("<script src=\"foo\">foo</script >") and
-    msg = "This regular expression does not match script end tags like </script >."
-    or
-    not regexp.matches("<script src=\"foo\">foo</script foo=\"bar\">") and
-    msg = "This regular expression does not match script end tags like </script foo=\"bar\">."
-    or
-    not regexp.matches("<script src=\"foo\">foo</script\t\n bar>") and
-    msg = "This regular expression does not match script end tags like </script\\t\\n bar>."
-  )
-}
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// BadTagFilterQuery should be used directly from the shared pack, and not from this file.
+deprecated import codeql.regex.nfa.BadTagFilterQuery::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/lib/semmle/python/security/OverlyLargeRangeQuery.qll b/python/ql/lib/semmle/python/security/OverlyLargeRangeQuery.qll
index 65e662f0bc5..49ec333161c 100644
--- a/python/ql/lib/semmle/python/security/OverlyLargeRangeQuery.qll
+++ b/python/ql/lib/semmle/python/security/OverlyLargeRangeQuery.qll
@@ -2,288 +2,7 @@
  * Classes and predicates for working with suspicious character ranges.
  */
 
-// We don't need the NFA utils, just the regexp tree.
-// but the below is a nice shared library that exposes the API we need.
-import regexp.NfaUtils
-
-/**
- * Gets a rank for `range` that is unique for ranges in the same file.
- * Prioritizes ranges that match more characters.
- */
-int rankRange(RegExpCharacterRange range) {
-  range =
-    rank[result](RegExpCharacterRange r, Location l, int low, int high |
-      r.getLocation() = l and
-      isRange(r, low, high)
-    |
-      r order by (high - low) desc, l.getStartLine(), l.getStartColumn()
-    )
-}
-
-/** Holds if `range` spans from the unicode code points `low` to `high` (both inclusive). */
-predicate isRange(RegExpCharacterRange range, int low, int high) {
-  exists(string lowc, string highc |
-    range.isRange(lowc, highc) and
-    low.toUnicode() = lowc and
-    high.toUnicode() = highc
-  )
-}
-
-/** Holds if `char` is an alpha-numeric character. */
-predicate isAlphanumeric(string char) {
-  // written like this to avoid having a bindingset for the predicate
-  char = [[48 .. 57], [65 .. 90], [97 .. 122]].toUnicode() // 0-9, A-Z, a-z
-}
-
-/**
- * Holds if the given ranges are from the same character class
- * and there exists at least one character matched by both ranges.
- */
-predicate overlap(RegExpCharacterRange a, RegExpCharacterRange b) {
-  exists(RegExpCharacterClass clz |
-    a = clz.getAChild() and
-    b = clz.getAChild() and
-    a != b
-  |
-    exists(int alow, int ahigh, int blow, int bhigh |
-      isRange(a, alow, ahigh) and
-      isRange(b, blow, bhigh) and
-      alow <= bhigh and
-      blow <= ahigh
-    )
-  )
-}
-
-/**
- * Holds if `range` overlaps with the char class `escape` from the same character class.
- */
-predicate overlapsWithCharEscape(RegExpCharacterRange range, RegExpCharacterClassEscape escape) {
-  exists(RegExpCharacterClass clz, string low, string high |
-    range = clz.getAChild() and
-    escape = clz.getAChild() and
-    range.isRange(low, high)
-  |
-    escape.getValue() = "w" and
-    getInRange(low, high).regexpMatch("\\w")
-    or
-    escape.getValue() = "d" and
-    getInRange(low, high).regexpMatch("\\d")
-    or
-    escape.getValue() = "s" and
-    getInRange(low, high).regexpMatch("\\s")
-  )
-}
-
-/** Gets the unicode code point for a `char`. */
-bindingset[char]
-int toCodePoint(string char) { result.toUnicode() = char }
-
-/** A character range that appears to be overly wide. */
-class OverlyWideRange extends RegExpCharacterRange {
-  OverlyWideRange() {
-    exists(int low, int high, int numChars |
-      isRange(this, low, high) and
-      numChars = (1 + high - low) and
-      this.getRootTerm().isUsedAsRegExp() and
-      numChars >= 10
-    |
-      // across the Z-a range (which includes backticks)
-      toCodePoint("Z") >= low and
-      toCodePoint("a") <= high
-      or
-      // across the 9-A range (which includes e.g. ; and ?)
-      toCodePoint("9") >= low and
-      toCodePoint("A") <= high
-      or
-      // a non-alphanumeric char as part of the range boundaries
-      exists(int bound | bound = [low, high] | not isAlphanumeric(bound.toUnicode())) and
-      // while still being ascii
-      low < 128 and
-      high < 128
-    ) and
-    // allowlist for known ranges
-    not this = allowedWideRanges()
-  }
-
-  /** Gets a string representation of a character class that matches the same chars as this range. */
-  string printEquivalent() { result = RangePrinter::printEquivalentCharClass(this) }
-}
-
-/** Gets a range that should not be reported as an overly wide range. */
-RegExpCharacterRange allowedWideRanges() {
-  // ~ is the last printable ASCII character, it's used right in various wide ranges.
-  result.isRange(_, "~")
-  or
-  // the same with " " and "!". " " is the first printable character, and "!" is the first non-white-space printable character.
-  result.isRange([" ", "!"], _)
-  or
-  // the `[@-_]` range is intentional
-  result.isRange("@", "_")
-  or
-  // starting from the zero byte is a good indication that it's purposely matching a large range.
-  result.isRange(0.toUnicode(), _)
-}
-
-/** Gets a char between (and including) `low` and `high`. */
-bindingset[low, high]
-private string getInRange(string low, string high) {
-  result = [toCodePoint(low) .. toCodePoint(high)].toUnicode()
-}
-
-/** A module computing an equivalent character class for an overly wide range. */
-module RangePrinter {
-  bindingset[char]
-  bindingset[result]
-  private string next(string char) {
-    exists(int prev, int next |
-      prev.toUnicode() = char and
-      next.toUnicode() = result and
-      next = prev + 1
-    )
-  }
-
-  /** Gets the points where the parts of the pretty printed range should be cut off. */
-  private string cutoffs() { result = ["A", "Z", "a", "z", "0", "9"] }
-
-  /** Gets the char to use in the low end of a range for a given `cut` */
-  private string lowCut(string cut) {
-    cut = ["A", "a", "0"] and
-    result = cut
-    or
-    cut = ["Z", "z", "9"] and
-    result = next(cut)
-  }
-
-  /** Gets the char to use in the high end of a range for a given `cut` */
-  private string highCut(string cut) {
-    cut = ["Z", "z", "9"] and
-    result = cut
-    or
-    cut = ["A", "a", "0"] and
-    next(result) = cut
-  }
-
-  /** Gets the cutoff char used for a given `part` of a range when pretty-printing it. */
-  private string cutoff(OverlyWideRange range, int part) {
-    exists(int low, int high | isRange(range, low, high) |
-      result =
-        rank[part + 1](string cut |
-          cut = cutoffs() and low < toCodePoint(cut) and toCodePoint(cut) < high
-        |
-          cut order by toCodePoint(cut)
-        )
-    )
-  }
-
-  /** Gets the number of parts we should print for a given `range`. */
-  private int parts(OverlyWideRange range) { result = 1 + count(cutoff(range, _)) }
-
-  /** Holds if the given part of a range should span from `low` to `high`. */
-  private predicate part(OverlyWideRange range, int part, string low, string high) {
-    // first part.
-    part = 0 and
-    (
-      range.isRange(low, high) and
-      parts(range) = 1
-      or
-      parts(range) >= 2 and
-      range.isRange(low, _) and
-      high = highCut(cutoff(range, part))
-    )
-    or
-    // middle
-    part >= 1 and
-    part < parts(range) - 1 and
-    low = lowCut(cutoff(range, part - 1)) and
-    high = highCut(cutoff(range, part))
-    or
-    // last.
-    part = parts(range) - 1 and
-    low = lowCut(cutoff(range, part - 1)) and
-    range.isRange(_, high)
-  }
-
-  /** Gets an escaped `char` for use in a character class. */
-  bindingset[char]
-  private string escape(string char) {
-    exists(string reg | reg = "(\\[|\\]|\\\\|-|/)" |
-      if char.regexpMatch(reg) then result = "\\" + char else result = char
-    )
-  }
-
-  /** Gets a part of the equivalent range. */
-  private string printEquivalentCharClass(OverlyWideRange range, int part) {
-    exists(string low, string high | part(range, part, low, high) |
-      if
-        isAlphanumeric(low) and
-        isAlphanumeric(high)
-      then result = low + "-" + high
-      else
-        result =
-          strictconcat(string char | char = getInRange(low, high) | escape(char) order by char)
-    )
-  }
-
-  /** Gets the entire pretty printed equivalent range. */
-  string printEquivalentCharClass(OverlyWideRange range) {
-    result =
-      strictconcat(string r, int part |
-        r = "[" and part = -1 and exists(range)
-        or
-        r = printEquivalentCharClass(range, part)
-        or
-        r = "]" and part = parts(range)
-      |
-        r order by part
-      )
-  }
-}
-
-/** Gets a char range that is overly large because of `reason`. */
-RegExpCharacterRange getABadRange(string reason, int priority) {
-  result instanceof OverlyWideRange and
-  priority = 0 and
-  exists(string equiv | equiv = result.(OverlyWideRange).printEquivalent() |
-    if equiv.length() <= 50
-    then reason = "is equivalent to " + equiv
-    else reason = "is equivalent to " + equiv.substring(0, 50) + "..."
-  )
-  or
-  priority = 1 and
-  exists(RegExpCharacterRange other |
-    reason = "overlaps with " + other + " in the same character class" and
-    rankRange(result) < rankRange(other) and
-    overlap(result, other)
-  )
-  or
-  priority = 2 and
-  exists(RegExpCharacterClassEscape escape |
-    reason = "overlaps with " + escape + " in the same character class" and
-    overlapsWithCharEscape(result, escape)
-  )
-  or
-  reason = "is empty" and
-  priority = 3 and
-  exists(int low, int high |
-    isRange(result, low, high) and
-    low > high
-  )
-}
-
-/** Holds if `range` matches suspiciously many characters. */
-predicate problem(RegExpCharacterRange range, string reason) {
-  reason =
-    strictconcat(string m, int priority |
-      range = getABadRange(m, priority)
-    |
-      m, ", and " order by priority desc
-    ) and
-  // specifying a range using an escape is usually OK.
-  not range.getAChild() instanceof RegExpEscape and
-  // Unicode escapes in strings are interpreted before it turns into a regexp,
-  // so e.g. [\u0001-\uFFFF] will just turn up as a range between two constants.
-  // We therefore exclude these ranges.
-  range.getRootTerm().getParent() instanceof RegExpLiteral and
-  // is used as regexp (mostly for JS where regular expressions are parsed eagerly)
-  range.getRootTerm().isUsedAsRegExp()
-}
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// OverlyLargeRangeQuery should be used directly from the shared pack, and not from this file.
+deprecated import codeql.regex.OverlyLargeRangeQuery::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/lib/semmle/python/security/dataflow/PolynomialReDoSCustomizations.qll b/python/ql/lib/semmle/python/security/dataflow/PolynomialReDoSCustomizations.qll
index 7e1a2c9561c..fac16730f2c 100644
--- a/python/ql/lib/semmle/python/security/dataflow/PolynomialReDoSCustomizations.qll
+++ b/python/ql/lib/semmle/python/security/dataflow/PolynomialReDoSCustomizations.qll
@@ -11,7 +11,7 @@ private import semmle.python.dataflow.new.TaintTracking
 private import semmle.python.Concepts
 private import semmle.python.dataflow.new.RemoteFlowSources
 private import semmle.python.dataflow.new.BarrierGuards
-private import semmle.python.RegexTreeView
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
 private import semmle.python.ApiGraphs
 
 /**
@@ -20,6 +20,9 @@ private import semmle.python.ApiGraphs
  * vulnerabilities, as well as extension points for adding your own.
  */
 module PolynomialReDoS {
+  private import TreeView
+  import codeql.regex.nfa.SuperlinearBackTracking::Make<TreeView>
+
   /**
    * A data flow source for "polynomial regular expression denial of service (ReDoS)" vulnerabilities.
    */
diff --git a/python/ql/lib/semmle/python/security/regexp/ExponentialBackTracking.qll b/python/ql/lib/semmle/python/security/regexp/ExponentialBackTracking.qll
index 4a608890249..f4628b883da 100644
--- a/python/ql/lib/semmle/python/security/regexp/ExponentialBackTracking.qll
+++ b/python/ql/lib/semmle/python/security/regexp/ExponentialBackTracking.qll
@@ -62,284 +62,7 @@
  *     a suffix `x` (possible empty) that is most likely __not__ accepted.
  */
 
-import NfaUtils
-
-/**
- * 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 |
-      stateInsideBacktracking(s) and
-      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 `(fork, fork)` state pairs when `isFork(fork, _, _, _, _)` holds.
- *
- * Used in `statePairDistToFork`
- */
-private predicate isStatePairFork(StatePair p) {
-  exists(State fork | p = MkStatePair(fork, fork) and isFork(fork, _, _, _, _))
-}
-
-/**
- * Holds if there are transitions from the components of `q` to the corresponding
- * components of `r`.
- *
- * Used in `statePairDistToFork`
- */
-private predicate reverseStep(StatePair r, StatePair q) { step(q, _, _, r) }
-
-/**
- * Gets the minimum length of a path from `q` to `r` in the
- * product automaton.
- */
-private int statePairDistToFork(StatePair q, StatePair r) =
-  shortestDistances(isStatePairFork/1, reverseStep/2)(r, q, 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 heuristic, 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) { isReachableFromFork(_, _, s1, s2, t, _) }
-
-/**
- * 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 + ")"
-    )
-  }
-}
-
-/**
- * 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) {
-  exists(InputSymbol s1, InputSymbol s2, Trace v |
-    isReachableFromFork(fork, r, s1, s2, v, rem) and
-    w = Step(s1, s2, v)
-  )
-}
-
-private predicate isReachableFromFork(
-  State fork, StatePair r, InputSymbol s1, InputSymbol s2, Trace v, int rem
-) {
-  // base case
-  exists(State q1, State q2 |
-    isFork(fork, s1, s2, q1, q2) and
-    r = MkStatePair(q1, q2) and
-    v = Nil() and
-    rem = statePairDistToFork(r, MkStatePair(fork, fork))
-  )
-  or
-  // recursive case
-  exists(StatePair p |
-    isReachableFromFork(fork, p, v, rem + 1) and
-    step(p, s1, s2, r) and
-    rem = statePairDistToFork(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))
-}
-
-/** An implementation of a chain containing chars for use by `Concretizer`. */
-private module CharTreeImpl implements CharTree {
-  class CharNode = Trace;
-
-  CharNode getPrev(CharNode t) { t = Step(_, _, result) }
-
-  /** Holds if `n` is a trace that is used by `concretize` in `isPumpable`. */
-  predicate isARelevantEnd(CharNode n) {
-    exists(State f | isReachableFromFork(f, getAForkPair(f), n, _))
-  }
-
-  string getChar(CharNode t) {
-    exists(InputSymbol s1, InputSymbol s2 | t = Step(s1, s2, _) | result = intersect(s1, s2))
-  }
-}
-
-/**
- * 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 = Concretizer<CharTreeImpl>::concretize(t)
-  )
-}
-
-/** Holds if `state` has exponential ReDoS */
-predicate hasReDoSResult = ReDoSPruning<isPumpable/2>::hasReDoSResult/4;
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// ExponentialBackTracking should be used directly from the shared pack, and not from this file.
+deprecated private import codeql.regex.nfa.ExponentialBackTracking::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/lib/semmle/python/security/regexp/NfaUtils.qll b/python/ql/lib/semmle/python/security/regexp/NfaUtils.qll
index 5ff0cb6a39e..942830d95b2 100644
--- a/python/ql/lib/semmle/python/security/regexp/NfaUtils.qll
+++ b/python/ql/lib/semmle/python/security/regexp/NfaUtils.qll
@@ -7,1332 +7,7 @@
  * other queries that benefit from reasoning about NFAs.
  */
 
-import NfaUtilsSpecific
-
-/**
- * Gets the char after `c` (from a simplified ASCII table).
- */
-private string nextChar(string c) { exists(int code | code = ascii(c) | code + 1 = ascii(result)) }
-
-/**
- * Gets an approximation for the ASCII code for `char`.
- * Only the easily printable chars are included (so no newline, tab, null, etc).
- */
-private int ascii(string char) {
-  char =
-    rank[result](string c |
-      c =
-        "! \"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\\]^_`abcdefghijklmnopqrstuvwxyz{|}~"
-            .charAt(_)
-    )
-}
-
-/**
- * Holds if `t` matches at least an epsilon symbol.
- *
- * That is, this term does not restrict the language of the enclosing regular expression.
- *
- * This is implemented as an under-approximation, and this predicate does not hold for sub-patterns in particular.
- */
-predicate matchesEpsilon(RegExpTerm t) {
-  t instanceof RegExpStar
-  or
-  t instanceof RegExpOpt
-  or
-  t.(RegExpRange).getLowerBound() = 0
-  or
-  exists(RegExpTerm child |
-    child = t.getAChild() and
-    matchesEpsilon(child)
-  |
-    t instanceof RegExpAlt or
-    t instanceof RegExpGroup or
-    t instanceof RegExpPlus or
-    t instanceof RegExpRange
-  )
-  or
-  matchesEpsilon(t.(RegExpBackRef).getGroup())
-  or
-  forex(RegExpTerm child | child = t.(RegExpSequence).getAChild() | matchesEpsilon(child))
-}
-
-/**
- * A lookahead/lookbehind that matches the empty string.
- */
-class EmptyPositiveSubPattern extends RegExpSubPattern {
-  EmptyPositiveSubPattern() {
-    (
-      this instanceof RegExpPositiveLookahead
-      or
-      this instanceof RegExpPositiveLookbehind
-    ) and
-    matchesEpsilon(this.getOperand())
-  }
-}
-
-/** DEPRECATED: Use `EmptyPositiveSubPattern` instead. */
-deprecated class EmptyPositiveSubPatttern = EmptyPositiveSubPattern;
-
-/**
- * A branch in a disjunction that is the root node in a literal, or a literal
- * whose root node is not a disjunction.
- */
-class RegExpRoot extends RegExpTerm {
-  RegExpRoot() {
-    exists(RegExpParent parent |
-      exists(RegExpAlt alt |
-        alt.isRootTerm() and
-        this = alt.getAChild() and
-        parent = alt.getParent()
-      )
-      or
-      this.isRootTerm() and
-      not this instanceof RegExpAlt and
-      parent = this.getParent()
-    )
-  }
-
-  /**
-   * Holds if this root term is relevant to the ReDoS analysis.
-   */
-  predicate isRelevant() {
-    // is actually used as a RegExp
-    this.isUsedAsRegExp() and
-    // not excluded for library specific reasons
-    not isExcluded(this.getRootTerm().getParent())
-  }
-}
-
-/**
- * A constant in a regular expression that represents valid Unicode character(s).
- */
-private class RegexpCharacterConstant extends RegExpConstant {
-  RegexpCharacterConstant() { this.isCharacter() }
-}
-
-/**
- * A regexp term that is relevant for this ReDoS analysis.
- */
-class RelevantRegExpTerm extends RegExpTerm {
-  RelevantRegExpTerm() { getRoot(this).isRelevant() }
-}
-
-/**
- * Holds if `term` is the chosen canonical representative for all terms with string representation `str`.
- * The string representation includes which flags are used with the regular expression.
- *
- * Using canonical representatives gives a huge performance boost when working with tuples containing multiple `InputSymbol`s.
- * The number of `InputSymbol`s is decreased by 3 orders of magnitude or more in some larger benchmarks.
- */
-private predicate isCanonicalTerm(RelevantRegExpTerm term, string str) {
-  term =
-    min(RelevantRegExpTerm t, Location loc, File file |
-      loc = t.getLocation() and
-      file = t.getFile() and
-      str = getCanonicalizationString(t)
-    |
-      t order by t.getFile().getRelativePath(), loc.getStartLine(), loc.getStartColumn()
-    )
-}
-
-/**
- * Gets a string representation of `term` that is used for canonicalization.
- */
-private string getCanonicalizationString(RelevantRegExpTerm term) {
-  exists(string ignoreCase |
-    (if RegExpFlags::isIgnoreCase(term.getRootTerm()) then ignoreCase = "i" else ignoreCase = "") and
-    result = term.getRawValue() + "|" + ignoreCase
-  )
-}
-
-/**
- * An abstract input symbol, representing a set of concrete characters.
- */
-private newtype TInputSymbol =
-  /** An input symbol corresponding to character `c`. */
-  Char(string c) {
-    c =
-      any(RegexpCharacterConstant cc |
-        cc instanceof RelevantRegExpTerm and
-        not RegExpFlags::isIgnoreCase(cc.getRootTerm())
-      ).getValue().charAt(_)
-    or
-    // normalize everything to lower case if the regexp is case insensitive
-    c =
-      any(RegexpCharacterConstant cc, string char |
-        cc instanceof RelevantRegExpTerm and
-        RegExpFlags::isIgnoreCase(cc.getRootTerm()) and
-        char = cc.getValue().charAt(_)
-      |
-        char.toLowerCase()
-      )
-  } or
-  /**
-   * An input symbol representing all characters matched by
-   * a (non-universal) character class that has string representation `charClassString`.
-   */
-  CharClass(string charClassString) {
-    exists(RelevantRegExpTerm recc | isCanonicalTerm(recc, charClassString) |
-      recc instanceof RegExpCharacterClass and
-      not recc.(RegExpCharacterClass).isUniversalClass()
-      or
-      isEscapeClass(recc, _)
-    )
-  } or
-  /** An input symbol representing all characters matched by `.`. */
-  Dot() or
-  /** An input symbol representing all characters. */
-  Any() or
-  /** An epsilon transition in the automaton. */
-  Epsilon()
-
-/**
- * Gets the the CharClass corresponding to the canonical representative `term`.
- */
-private CharClass getCharClassForCanonicalTerm(RegExpTerm term) {
-  exists(string str | isCanonicalTerm(term, str) | result = CharClass(str))
-}
-
-/**
- * Gets a char class that represents `term`, even when `term` is not the canonical representative.
- */
-CharacterClass getCanonicalCharClass(RegExpTerm term) {
-  exists(string str | str = getCanonicalizationString(term) and result = CharClass(str))
-}
-
-/**
- * Holds if `a` and `b` are input symbols from the same regexp.
- */
-private predicate sharesRoot(InputSymbol a, InputSymbol b) {
-  exists(RegExpRoot root |
-    belongsTo(a, root) and
-    belongsTo(b, root)
-  )
-}
-
-/**
- * Holds if the `a` is an input symbol from a regexp that has root `root`.
- */
-private predicate belongsTo(InputSymbol a, RegExpRoot root) {
-  exists(State s | getRoot(s.getRepr()) = root |
-    delta(s, a, _)
-    or
-    delta(_, a, s)
-  )
-}
-
-/**
- * An abstract input symbol, representing a set of concrete characters.
- */
-class InputSymbol extends TInputSymbol {
-  InputSymbol() { not this instanceof Epsilon }
-
-  /**
-   * Gets a string representation of this input symbol.
-   */
-  string toString() {
-    this = Char(result)
-    or
-    this = CharClass(result)
-    or
-    this = Dot() and result = "."
-    or
-    this = Any() and result = "[^]"
-  }
-}
-
-/**
- * An abstract input symbol that represents a character class.
- */
-abstract class CharacterClass extends InputSymbol {
-  /**
-   * Gets a character that is relevant for intersection-tests involving this
-   * character class.
-   *
-   * Specifically, this is any of the characters mentioned explicitly in the
-   * character class, offset by one if it is inverted. For character class escapes,
-   * the result is as if the class had been written out as a series of intervals.
-   *
-   * This set is large enough to ensure that for any two intersecting character
-   * classes, one contains a relevant character from the other.
-   */
-  abstract string getARelevantChar();
-
-  /**
-   * Holds if this character class matches `char`.
-   */
-  bindingset[char]
-  abstract predicate matches(string char);
-
-  /**
-   * Gets a character matched by this character class.
-   */
-  string choose() { result = this.getARelevantChar() and this.matches(result) }
-}
-
-/**
- * Provides implementations for `CharacterClass`.
- */
-private module CharacterClasses {
-  /**
-   * Holds if the character class `cc` has a child (constant or range) that matches `char`.
-   */
-  pragma[noinline]
-  predicate hasChildThatMatches(RegExpCharacterClass cc, string char) {
-    if RegExpFlags::isIgnoreCase(cc.getRootTerm())
-    then
-      // normalize everything to lower case if the regexp is case insensitive
-      exists(string c | hasChildThatMatchesIgnoringCasingFlags(cc, c) | char = c.toLowerCase())
-    else hasChildThatMatchesIgnoringCasingFlags(cc, char)
-  }
-
-  /**
-   * Holds if the character class `cc` has a child (constant or range) that matches `char`.
-   * Ignores whether the character class is inside a regular expression that has the ignore case flag.
-   */
-  pragma[noinline]
-  predicate hasChildThatMatchesIgnoringCasingFlags(RegExpCharacterClass cc, string char) {
-    exists(getCharClassForCanonicalTerm(cc)) and
-    exists(RegExpTerm child | child = cc.getAChild() |
-      char = child.(RegexpCharacterConstant).getValue()
-      or
-      rangeMatchesOnLetterOrDigits(child, char)
-      or
-      not rangeMatchesOnLetterOrDigits(child, _) and
-      char = getARelevantChar() and
-      exists(string lo, string hi | child.(RegExpCharacterRange).isRange(lo, hi) |
-        lo <= char and
-        char <= hi
-      )
-      or
-      exists(string charClass | isEscapeClass(child, charClass) |
-        charClass.toLowerCase() = charClass and
-        classEscapeMatches(charClass, char)
-        or
-        char = getARelevantChar() and
-        charClass.toUpperCase() = charClass and
-        not classEscapeMatches(charClass, char)
-      )
-    )
-  }
-
-  /**
-   * Holds if `range` is a range on lower-case, upper-case, or digits, and matches `char`.
-   * This predicate is used to restrict the searchspace for ranges by only joining `getAnyPossiblyMatchedChar`
-   * on a few ranges.
-   */
-  private predicate rangeMatchesOnLetterOrDigits(RegExpCharacterRange range, string char) {
-    exists(string lo, string hi |
-      range.isRange(lo, hi) and lo = lowercaseLetter() and hi = lowercaseLetter()
-    |
-      lo <= char and
-      char <= hi and
-      char = lowercaseLetter()
-    )
-    or
-    exists(string lo, string hi |
-      range.isRange(lo, hi) and lo = upperCaseLetter() and hi = upperCaseLetter()
-    |
-      lo <= char and
-      char <= hi and
-      char = upperCaseLetter()
-    )
-    or
-    exists(string lo, string hi | range.isRange(lo, hi) and lo = digit() and hi = digit() |
-      lo <= char and
-      char <= hi and
-      char = digit()
-    )
-  }
-
-  private string lowercaseLetter() { result = "abcdefghijklmnopqrstuvwxyz".charAt(_) }
-
-  private string upperCaseLetter() { result = "ABCDEFGHIJKLMNOPQRSTUVWXYZ".charAt(_) }
-
-  private string digit() { result = [0 .. 9].toString() }
-
-  /**
-   * Gets a char that could be matched by a regular expression.
-   * Includes all printable ascii chars, all constants mentioned in a regexp, and all chars matches by the regexp `/\s|\d|\w/`.
-   */
-  string getARelevantChar() {
-    exists(ascii(result))
-    or
-    exists(RegexpCharacterConstant c | result = c.getValue().charAt(_))
-    or
-    classEscapeMatches(_, result)
-  }
-
-  /**
-   * Gets a char that is mentioned in the character class `c`.
-   */
-  private string getAMentionedChar(RegExpCharacterClass c) {
-    exists(RegExpTerm child | child = c.getAChild() |
-      result = child.(RegexpCharacterConstant).getValue()
-      or
-      child.(RegExpCharacterRange).isRange(result, _)
-      or
-      child.(RegExpCharacterRange).isRange(_, result)
-      or
-      exists(string charClass | isEscapeClass(child, charClass) |
-        result = min(string s | classEscapeMatches(charClass.toLowerCase(), s))
-        or
-        result = max(string s | classEscapeMatches(charClass.toLowerCase(), s))
-      )
-    )
-  }
-
-  bindingset[char, cc]
-  private string caseNormalize(string char, RegExpTerm cc) {
-    if RegExpFlags::isIgnoreCase(cc.getRootTerm())
-    then result = char.toLowerCase()
-    else result = char
-  }
-
-  /**
-   * An implementation of `CharacterClass` for positive (non inverted) character classes.
-   */
-  private class PositiveCharacterClass extends CharacterClass {
-    RegExpCharacterClass cc;
-
-    PositiveCharacterClass() { this = getCharClassForCanonicalTerm(cc) and not cc.isInverted() }
-
-    override string getARelevantChar() { result = caseNormalize(getAMentionedChar(cc), cc) }
-
-    override predicate matches(string char) { hasChildThatMatches(cc, char) }
-  }
-
-  /**
-   * An implementation of `CharacterClass` for inverted character classes.
-   */
-  private class InvertedCharacterClass extends CharacterClass {
-    RegExpCharacterClass cc;
-
-    InvertedCharacterClass() { this = getCharClassForCanonicalTerm(cc) and cc.isInverted() }
-
-    override string getARelevantChar() {
-      result = nextChar(caseNormalize(getAMentionedChar(cc), cc)) or
-      nextChar(result) = caseNormalize(getAMentionedChar(cc), cc)
-    }
-
-    bindingset[char]
-    override predicate matches(string char) { not hasChildThatMatches(cc, char) }
-  }
-
-  /**
-   * Holds if the character class escape `clazz` (\d, \s, or \w) matches `char`.
-   */
-  pragma[noinline]
-  private predicate classEscapeMatches(string clazz, string char) {
-    clazz = "d" and
-    char = "0123456789".charAt(_)
-    or
-    clazz = "s" and
-    char = [" ", "\t", "\r", "\n", 11.toUnicode(), 12.toUnicode()] // 11.toUnicode() = \v, 12.toUnicode() = \f
-    or
-    clazz = "w" and
-    char = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_".charAt(_)
-  }
-
-  /**
-   * An implementation of `CharacterClass` for \d, \s, and \w.
-   */
-  private class PositiveCharacterClassEscape extends CharacterClass {
-    string charClass;
-    RegExpTerm cc;
-
-    PositiveCharacterClassEscape() {
-      isEscapeClass(cc, charClass) and
-      this = getCharClassForCanonicalTerm(cc) and
-      charClass = ["d", "s", "w"]
-    }
-
-    override string getARelevantChar() {
-      charClass = "d" and
-      result = ["0", "9"]
-      or
-      charClass = "s" and
-      result = " "
-      or
-      charClass = "w" and
-      if RegExpFlags::isIgnoreCase(cc.getRootTerm())
-      then result = ["a", "z", "_", "0", "9"]
-      else result = ["a", "Z", "_", "0", "9"]
-    }
-
-    override predicate matches(string char) { classEscapeMatches(charClass, char) }
-
-    override string choose() {
-      charClass = "d" and
-      result = "9"
-      or
-      charClass = "s" and
-      result = " "
-      or
-      charClass = "w" and
-      result = "a"
-    }
-  }
-
-  /**
-   * An implementation of `CharacterClass` for \D, \S, and \W.
-   */
-  private class NegativeCharacterClassEscape extends CharacterClass {
-    string charClass;
-
-    NegativeCharacterClassEscape() {
-      exists(RegExpTerm cc |
-        isEscapeClass(cc, charClass) and
-        this = getCharClassForCanonicalTerm(cc) and
-        charClass = ["D", "S", "W"]
-      )
-    }
-
-    override string getARelevantChar() {
-      charClass = "D" and
-      result = ["a", "Z", "!"]
-      or
-      charClass = "S" and
-      result = ["a", "9", "!"]
-      or
-      charClass = "W" and
-      result = [" ", "!"]
-    }
-
-    bindingset[char]
-    override predicate matches(string char) {
-      not classEscapeMatches(charClass.toLowerCase(), char)
-    }
-  }
-
-  /** Gets a representative for all char classes that match the same chars as `c`. */
-  CharacterClass normalize(CharacterClass c) {
-    exists(string normalization |
-      normalization = getNormalizationString(c) and
-      result =
-        min(CharacterClass cc, string raw |
-          getNormalizationString(cc) = normalization and cc = CharClass(raw)
-        |
-          cc order by raw
-        )
-    )
-  }
-
-  /** Gets a string representing all the chars matched by `c` */
-  private string getNormalizationString(CharacterClass c) {
-    (c instanceof PositiveCharacterClass or c instanceof PositiveCharacterClassEscape) and
-    result = concat(string char | c.matches(char) and char = CharacterClasses::getARelevantChar())
-    or
-    (c instanceof InvertedCharacterClass or c instanceof NegativeCharacterClassEscape) and
-    // the string produced by the concat can not contain repeated chars
-    // so by starting the below with "nn" we can guarantee that
-    // it will not overlap with the above case.
-    // and a negative char class can never match the same chars as a positive one, so we don't miss any results from this.
-    result =
-      "nn:" +
-        concat(string char | not c.matches(char) and char = CharacterClasses::getARelevantChar())
-  }
-}
-
-private class EdgeLabel extends TInputSymbol {
-  string toString() {
-    this = Epsilon() and result = ""
-    or
-    exists(InputSymbol s | this = s and result = s.toString())
-  }
-}
-
-/**
- * A RegExp term that acts like a plus.
- * Either it's a RegExpPlus, or it is a range {1,X} where X is >= 30.
- * 30 has been chosen as a threshold because for exponential blowup 2^30 is enough to get a decent DOS attack.
- */
-private class EffectivelyPlus extends RegExpTerm {
-  EffectivelyPlus() {
-    this instanceof RegExpPlus
-    or
-    exists(RegExpRange range |
-      range.getLowerBound() = 1 and
-      (range.getUpperBound() >= 30 or not exists(range.getUpperBound()))
-    |
-      this = range
-    )
-  }
-}
-
-/**
- * A RegExp term that acts like a star.
- * Either it's a RegExpStar, or it is a range {0,X} where X is >= 30.
- */
-private class EffectivelyStar extends RegExpTerm {
-  EffectivelyStar() {
-    this instanceof RegExpStar
-    or
-    exists(RegExpRange range |
-      range.getLowerBound() = 0 and
-      (range.getUpperBound() >= 30 or not exists(range.getUpperBound()))
-    |
-      this = range
-    )
-  }
-}
-
-/**
- * A RegExp term that acts like a question mark.
- * Either it's a RegExpQuestion, or it is a range {0,1}.
- */
-private class EffectivelyQuestion extends RegExpTerm {
-  EffectivelyQuestion() {
-    this instanceof RegExpOpt
-    or
-    exists(RegExpRange range | range.getLowerBound() = 0 and range.getUpperBound() = 1 |
-      this = range
-    )
-  }
-}
-
-/**
- * Gets the state before matching `t`.
- */
-pragma[inline]
-private State before(RegExpTerm t) { result = Match(t, 0) }
-
-/**
- * Gets a state the NFA may be in after matching `t`.
- */
-State after(RegExpTerm t) {
-  exists(RegExpAlt alt | t = alt.getAChild() | result = after(alt))
-  or
-  exists(RegExpSequence seq, int i | t = seq.getChild(i) |
-    result = before(seq.getChild(i + 1))
-    or
-    i + 1 = seq.getNumChild() and result = after(seq)
-  )
-  or
-  exists(RegExpGroup grp | t = grp.getAChild() | result = after(grp))
-  or
-  exists(EffectivelyStar star | t = star.getAChild() |
-    not isPossessive(star) and
-    result = before(star)
-  )
-  or
-  exists(EffectivelyPlus plus | t = plus.getAChild() |
-    not isPossessive(plus) and
-    result = before(plus)
-    or
-    result = after(plus)
-  )
-  or
-  exists(EffectivelyQuestion opt | t = opt.getAChild() | result = after(opt))
-  or
-  exists(RegExpRoot root | t = root |
-    if matchesAnySuffix(root) then result = AcceptAnySuffix(root) else result = Accept(root)
-  )
-}
-
-/**
- * Holds if the NFA has a transition from `q1` to `q2` labelled with `lbl`.
- */
-predicate delta(State q1, EdgeLabel lbl, State q2) {
-  exists(RegexpCharacterConstant s, int i |
-    q1 = Match(s, i) and
-    (
-      not RegExpFlags::isIgnoreCase(s.getRootTerm()) and
-      lbl = Char(s.getValue().charAt(i))
-      or
-      // normalize everything to lower case if the regexp is case insensitive
-      RegExpFlags::isIgnoreCase(s.getRootTerm()) and
-      exists(string c | c = s.getValue().charAt(i) | lbl = Char(c.toLowerCase()))
-    ) and
-    (
-      q2 = Match(s, i + 1)
-      or
-      s.getValue().length() = i + 1 and
-      q2 = after(s)
-    )
-  )
-  or
-  exists(RegExpDot dot | q1 = before(dot) and q2 = after(dot) |
-    if RegExpFlags::isDotAll(dot.getRootTerm()) then lbl = Any() else lbl = Dot()
-  )
-  or
-  exists(RegExpCharacterClass cc |
-    cc.isUniversalClass() and q1 = before(cc) and lbl = Any() and q2 = after(cc)
-    or
-    q1 = before(cc) and
-    lbl = CharacterClasses::normalize(CharClass(getCanonicalizationString(cc))) and
-    q2 = after(cc)
-  )
-  or
-  exists(RegExpTerm cc | isEscapeClass(cc, _) |
-    q1 = before(cc) and
-    lbl = CharacterClasses::normalize(CharClass(getCanonicalizationString(cc))) and
-    q2 = after(cc)
-  )
-  or
-  exists(RegExpAlt alt | lbl = Epsilon() | q1 = before(alt) and q2 = before(alt.getAChild()))
-  or
-  exists(RegExpSequence seq | lbl = Epsilon() | q1 = before(seq) and q2 = before(seq.getChild(0)))
-  or
-  exists(RegExpGroup grp | lbl = Epsilon() | q1 = before(grp) and q2 = before(grp.getChild(0)))
-  or
-  exists(EffectivelyStar star | lbl = Epsilon() |
-    q1 = before(star) and q2 = before(star.getChild(0))
-    or
-    q1 = before(star) and q2 = after(star)
-  )
-  or
-  exists(EffectivelyPlus plus | lbl = Epsilon() |
-    q1 = before(plus) and q2 = before(plus.getChild(0))
-  )
-  or
-  exists(EffectivelyQuestion opt | lbl = Epsilon() |
-    q1 = before(opt) and q2 = before(opt.getChild(0))
-    or
-    q1 = before(opt) and q2 = after(opt)
-  )
-  or
-  exists(RegExpRoot root | q1 = AcceptAnySuffix(root) |
-    lbl = Any() and q2 = q1
-    or
-    lbl = Epsilon() and q2 = Accept(root)
-  )
-  or
-  exists(RegExpRoot root | q1 = Match(root, 0) | matchesAnyPrefix(root) and lbl = Any() and q2 = q1)
-  or
-  exists(RegExpDollar dollar | q1 = before(dollar) |
-    lbl = Epsilon() and q2 = Accept(getRoot(dollar))
-  )
-  or
-  exists(EmptyPositiveSubPattern empty | q1 = before(empty) | lbl = Epsilon() and q2 = after(empty))
-}
-
-/**
- * Gets a state that `q` has an epsilon transition to.
- */
-State epsilonSucc(State q) { delta(q, Epsilon(), result) }
-
-/**
- * Gets a state that has an epsilon transition to `q`.
- */
-State epsilonPred(State q) { q = epsilonSucc(result) }
-
-/**
- * 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`.
- */
-predicate deltaClosed(State q1, InputSymbol s, State q2) { delta(epsilonSucc*(q1), s, q2) }
-
-/**
- * Gets the root containing the given term, that is, the root of the literal,
- * or a branch of the root disjunction.
- */
-RegExpRoot getRoot(RegExpTerm term) {
-  result = term or
-  result = getRoot(term.getParent())
-}
-
-/**
- * A state in the NFA.
- */
-newtype TState =
-  /**
-   * A state representing that the NFA is about to match a term.
-   * `i` is used to index into multi-char literals.
-   */
-  Match(RelevantRegExpTerm t, int i) {
-    i = 0
-    or
-    exists(t.(RegexpCharacterConstant).getValue().charAt(i))
-  } or
-  /**
-   * An accept state, where exactly the given input string is accepted.
-   */
-  Accept(RegExpRoot l) { l.isRelevant() } or
-  /**
-   * An accept state, where the given input string, or any string that has this
-   * string as a prefix, is accepted.
-   */
-  AcceptAnySuffix(RegExpRoot l) { l.isRelevant() }
-
-/**
- * Gets a state that is about to match the regular expression `t`.
- */
-State mkMatch(RegExpTerm t) { result = Match(t, 0) }
-
-/**
- * A state in the NFA corresponding to a regular expression.
- *
- * Each regular expression literal `l` has one accepting state
- * `Accept(l)`, one state that accepts all suffixes `AcceptAnySuffix(l)`,
- * and a state `Match(t, i)` for every subterm `t`,
- * which represents the state of the NFA before starting to
- * match `t`, or the `i`th character in `t` if `t` is a constant.
- */
-class State extends TState {
-  RegExpTerm repr;
-
-  State() {
-    this = Match(repr, _) or
-    this = Accept(repr) or
-    this = AcceptAnySuffix(repr)
-  }
-
-  /**
-   * Gets a string representation for this state in a regular expression.
-   */
-  string toString() {
-    exists(int i | this = Match(repr, i) | result = "Match(" + repr + "," + i + ")")
-    or
-    this instanceof Accept and
-    result = "Accept(" + repr + ")"
-    or
-    this instanceof AcceptAnySuffix and
-    result = "AcceptAny(" + repr + ")"
-  }
-
-  /**
-   * Gets the location for this state.
-   */
-  Location getLocation() { result = repr.getLocation() }
-
-  /**
-   * Gets the term represented by this state.
-   */
-  RegExpTerm getRepr() { result = repr }
-}
-
-/**
- * Gets the minimum char that is matched by both the character classes `c` and `d`.
- */
-private string getMinOverlapBetweenCharacterClasses(CharacterClass c, CharacterClass d) {
-  result = min(getAOverlapBetweenCharacterClasses(c, d))
-}
-
-/**
- * Gets a char that is matched by both the character classes `c` and `d`.
- * And `c` and `d` is not the same character class.
- */
-private string getAOverlapBetweenCharacterClasses(CharacterClass c, CharacterClass d) {
-  sharesRoot(c, d) and
-  result = [c.getARelevantChar(), d.getARelevantChar()] and
-  c.matches(result) and
-  d.matches(result) and
-  not c = d
-}
-
-/**
- * Gets a character that is represented by both `c` and `d`.
- */
-string intersect(InputSymbol c, InputSymbol d) {
-  (sharesRoot(c, d) or [c, d] = Any()) and
-  (
-    c = Char(result) and
-    d = getAnInputSymbolMatching(result)
-    or
-    result = getMinOverlapBetweenCharacterClasses(c, d)
-    or
-    result = c.(CharacterClass).choose() and
-    (
-      d = c
-      or
-      d = Dot() and
-      not (result = "\n" or result = "\r")
-      or
-      d = Any()
-    )
-    or
-    (c = Dot() or c = Any()) and
-    (d = Dot() or d = Any()) and
-    result = "a"
-  )
-  or
-  result = intersect(d, c)
-}
-
-/**
- * Gets a symbol that matches `char`.
- */
-bindingset[char]
-InputSymbol getAnInputSymbolMatching(string char) {
-  result = Char(char)
-  or
-  result.(CharacterClass).matches(char)
-  or
-  result = Dot() and
-  not (char = "\n" or char = "\r")
-  or
-  result = Any()
-}
-
-/**
- * Holds if `state` is a start state.
- */
-predicate isStartState(State state) {
-  state = mkMatch(any(RegExpRoot r))
-  or
-  exists(RegExpCaret car | state = after(car))
-}
-
-/**
- * Holds if `state` is a candidate for ReDoS with string `pump`.
- */
-signature predicate isCandidateSig(State state, string pump);
-
-/**
- * Holds if `state` is a candidate for ReDoS.
- */
-signature predicate isCandidateSig(State state);
-
-/**
- * Predicates for constructing a prefix string that leads to a given state.
- */
-module PrefixConstruction<isCandidateSig/1 isCandidate> {
-  /**
-   * Holds if `state` is the textually last start state for the regular expression.
-   */
-  private predicate lastStartState(RelevantState state) {
-    exists(RegExpRoot root |
-      state =
-        max(RelevantState s, Location l |
-          isStartState(s) and
-          getRoot(s.getRepr()) = root and
-          l = s.getRepr().getLocation()
-        |
-          s
-          order by
-            l.getStartLine(), l.getStartColumn(), s.getRepr().toString(), l.getEndColumn(),
-            l.getEndLine()
-        )
-    )
-  }
-
-  /**
-   * Holds if there exists any transition (Epsilon() or other) from `a` to `b`.
-   */
-  private predicate existsTransition(State a, State b) { delta(a, _, b) }
-
-  /**
-   * Gets the minimum number of transitions it takes to reach `state` from the `start` state.
-   */
-  int prefixLength(State start, State state) =
-    shortestDistances(lastStartState/1, existsTransition/2)(start, state, result)
-
-  /**
-   * Gets the minimum number of transitions it takes to reach `state` from the start state.
-   */
-  private int lengthFromStart(State state) { result = prefixLength(_, state) }
-
-  /**
-   * Gets a string for which the regular expression will reach `state`.
-   *
-   * Has at most one result for any given `state`.
-   * This predicate will not always have a result even if there is a ReDoS issue in
-   * the regular expression.
-   */
-  string prefix(State state) {
-    lastStartState(state) and
-    result = ""
-    or
-    // the search stops past the last redos candidate state.
-    lengthFromStart(state) <= max(lengthFromStart(any(State s | isCandidate(s)))) and
-    exists(State prev |
-      // select a unique predecessor (by an arbitrary measure)
-      prev =
-        min(State s, Location loc |
-          lengthFromStart(s) = lengthFromStart(state) - 1 and
-          loc = s.getRepr().getLocation() and
-          delta(s, _, state)
-        |
-          s
-          order by
-            loc.getStartLine(), loc.getStartColumn(), loc.getEndLine(), loc.getEndColumn(),
-            s.getRepr().toString()
-        )
-    |
-      // greedy search for the shortest prefix
-      result = prefix(prev) and delta(prev, Epsilon(), state)
-      or
-      not delta(prev, Epsilon(), state) and
-      result = prefix(prev) + getCanonicalEdgeChar(prev, state)
-    )
-  }
-
-  /**
-   * Gets a canonical char for which there exists a transition from `prev` to `next` in the NFA.
-   */
-  private string getCanonicalEdgeChar(State prev, State next) {
-    result =
-      min(string c | delta(prev, any(InputSymbol symbol | c = intersect(Any(), symbol)), next))
-  }
-
-  /** A state within a regular expression that contains a candidate state. */
-  class RelevantState instanceof State {
-    RelevantState() {
-      exists(State s | isCandidate(s) | getRoot(s.getRepr()) = getRoot(this.getRepr()))
-    }
-
-    /** Gets a string representation for this state in a regular expression. */
-    string toString() { result = State.super.toString() }
-
-    /** Gets the term represented by this state. */
-    RegExpTerm getRepr() { result = State.super.getRepr() }
-  }
-}
-
-/**
- * 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.
- */
-module ReDoSPruning<isCandidateSig/2 isCandidate> {
-  /**
-   * Holds if repeating `pump` starting at `state` is a candidate for causing backtracking.
-   * No check whether a rejected suffix exists has been made.
-   */
-  private predicate isReDoSCandidate(State state, string pump) {
-    isCandidate(state, pump) and
-    not state = acceptsAnySuffix() and // pruning early - these can never get stuck in a rejecting state.
-    (
-      not isCandidate(epsilonSucc+(state), _)
-      or
-      epsilonSucc+(state) = state and
-      state =
-        max(State s, Location l |
-          s = epsilonSucc+(state) and
-          l = s.getRepr().getLocation() and
-          isCandidate(s, _) and
-          s.getRepr() instanceof InfiniteRepetitionQuantifier
-        |
-          s order by l.getStartLine(), l.getStartColumn(), l.getEndColumn(), l.getEndLine()
-        )
-    )
-  }
-
-  /** Gets a state that can reach the `accept-any` state using only epsilon steps. */
-  private State acceptsAnySuffix() { epsilonSucc*(result) = AcceptAnySuffix(_) }
-
-  predicate isCandidateState(State s) { isReDoSCandidate(s, _) }
-
-  import PrefixConstruction<isCandidateState/1> as Prefix
-
-  class RelevantState = Prefix::RelevantState;
-
-  /**
-   * Predicates for testing the presence of a rejecting suffix.
-   *
-   * These predicates are used to ensure that the all states reached from the fork
-   * by repeating `w` have a rejecting suffix.
-   *
-   * For example, a regexp like `/^(a+)+/` will accept any string as long the prefix is
-   * some number of `"a"`s, and it is therefore not possible to construct a rejecting suffix.
-   *
-   * A regexp like `/(a+)+$/` or `/(a+)+b/` trivially has a rejecting suffix,
-   * as the suffix "X" will cause both the regular expressions to be rejected.
-   *
-   * The string `w` is repeated any number of times because it needs to be
-   * infinitely repeatable for the attack to work.
-   * For the regular expression `/((ab)+)*abab/` the accepting state is not reachable from the fork
-   * using epsilon transitions. But any attempt at repeating `w` will end in a state that accepts all suffixes.
-   */
-  private module SuffixConstruction {
-    /**
-     * Holds if all states reachable from `fork` by repeating `w`
-     * are likely rejectable by appending some suffix.
-     */
-    predicate reachesOnlyRejectableSuffixes(State fork, string w) {
-      isReDoSCandidate(fork, w) and
-      forex(State next | next = process(fork, w, w.length() - 1) | isLikelyRejectable(next)) and
-      not getProcessPrevious(fork, _, w) = acceptsAnySuffix() // we stop `process(..)` early if we can, check here if it happened.
-    }
-
-    /**
-     * Holds if there likely exists a suffix starting from `s` that leads to the regular expression being rejected.
-     * This predicate might find impossible suffixes when searching for suffixes of length > 1, which can cause FPs.
-     */
-    pragma[noinline]
-    private predicate isLikelyRejectable(RelevantState s) {
-      // exists a reject edge with some char.
-      hasRejectEdge(s)
-      or
-      hasEdgeToLikelyRejectable(s)
-      or
-      // stopping here is rejection
-      isRejectState(s)
-    }
-
-    /**
-     * Holds if `s` is not an accept state, and there is no epsilon transition to an accept state.
-     */
-    predicate isRejectState(RelevantState s) { not epsilonSucc*(s) = Accept(_) }
-
-    /**
-     * Holds if there is likely a non-empty suffix leading to rejection starting in `s`.
-     */
-    pragma[noopt]
-    predicate hasEdgeToLikelyRejectable(RelevantState s) {
-      // all edges (at least one) with some char leads to another state that is rejectable.
-      // the `next` states might not share a common suffix, which can cause FPs.
-      exists(string char | char = hasEdgeToLikelyRejectableHelper(s) |
-        // noopt to force `hasEdgeToLikelyRejectableHelper` to be first in the join-order.
-        exists(State next | deltaClosedChar(s, char, next) | isLikelyRejectable(next)) and
-        forall(State next | deltaClosedChar(s, char, next) | isLikelyRejectable(next))
-      )
-    }
-
-    /**
-     * Gets a char for there exists a transition away from `s`,
-     * and `s` has not been found to be rejectable by `hasRejectEdge` or `isRejectState`.
-     */
-    pragma[noinline]
-    private string hasEdgeToLikelyRejectableHelper(RelevantState s) {
-      not hasRejectEdge(s) and
-      not isRejectState(s) and
-      deltaClosedChar(s, result, _)
-    }
-
-    /**
-     * Holds if there is a state `next` that can be reached from `prev`
-     * along epsilon edges, such that there is a transition from
-     * `prev` to `next` that the character symbol `char`.
-     */
-    predicate deltaClosedChar(RelevantState prev, string char, RelevantState next) {
-      deltaClosed(prev, getAnInputSymbolMatchingRelevant(char), next)
-    }
-
-    pragma[noinline]
-    InputSymbol getAnInputSymbolMatchingRelevant(string char) {
-      char = relevant(_) and
-      result = getAnInputSymbolMatching(char)
-    }
-
-    pragma[noinline]
-    RegExpRoot relevantRoot() {
-      exists(RegExpTerm term, State s |
-        s.getRepr() = term and isCandidateState(s) and result = term.getRootTerm()
-      )
-    }
-
-    /**
-     * Gets a char used for finding possible suffixes inside `root`.
-     */
-    pragma[noinline]
-    private string relevant(RegExpRoot root) {
-      root = relevantRoot() and
-      (
-        exists(ascii(result)) and exists(root)
-        or
-        exists(InputSymbol s | belongsTo(s, root) | result = intersect(s, _))
-        or
-        // The characters from `hasSimpleRejectEdge`. Only `\n` is really needed (as `\n` is not in the `ascii` relation).
-        // The three chars must be kept in sync with `hasSimpleRejectEdge`.
-        result = ["|", "\n", "Z"] and exists(root)
-      )
-    }
-
-    /**
-     * Holds if there exists a `char` such that there is no edge from `s` labeled `char` in our NFA.
-     * The NFA does not model reject states, so the above is the same as saying there is a reject edge.
-     */
-    private predicate hasRejectEdge(State s) {
-      hasSimpleRejectEdge(s)
-      or
-      not hasSimpleRejectEdge(s) and
-      exists(string char | char = relevant(getRoot(s.getRepr())) | not deltaClosedChar(s, char, _))
-    }
-
-    /**
-     * Holds if there is no edge from `s` labeled with "|", "\n", or "Z" in our NFA.
-     * This predicate is used as a cheap pre-processing to speed up `hasRejectEdge`.
-     */
-    private predicate hasSimpleRejectEdge(State s) {
-      // The three chars were chosen arbitrarily. The three chars must be kept in sync with `relevant`.
-      exists(string char | char = ["|", "\n", "Z"] | not deltaClosedChar(s, char, _))
-    }
-
-    /**
-     * Gets a state that can be reached from pumpable `fork` consuming all
-     * chars in `w` any number of times followed by the first `i+1` characters of `w`.
-     */
-    pragma[noopt]
-    private State process(State fork, string w, int i) {
-      exists(State prev | prev = getProcessPrevious(fork, i, w) |
-        not prev = acceptsAnySuffix() and // we stop `process(..)` early if we can. If the successor accepts any suffix, then we know it can never be rejected.
-        exists(string char, InputSymbol sym |
-          char = w.charAt(i) and
-          deltaClosed(prev, sym, result) and
-          // noopt to prevent joining `prev` with all possible `chars` that could transition away from `prev`.
-          // Instead only join with the set of `chars` where a relevant `InputSymbol` has already been found.
-          sym = getAProcessInputSymbol(char)
-        )
-      )
-    }
-
-    /**
-     * Gets a state that can be reached from pumpable `fork` consuming all
-     * chars in `w` any number of times followed by the first `i` characters of `w`.
-     */
-    private State getProcessPrevious(State fork, int i, string w) {
-      isReDoSCandidate(fork, w) and
-      (
-        i = 0 and result = fork
-        or
-        result = process(fork, w, i - 1)
-        or
-        // repeat until fixpoint
-        i = 0 and
-        result = process(fork, w, w.length() - 1)
-      )
-    }
-
-    /**
-     * Gets an InputSymbol that matches `char`.
-     * The predicate is specialized to only have a result for the `char`s that are relevant for the `process` predicate.
-     */
-    private InputSymbol getAProcessInputSymbol(string char) {
-      char = getAProcessChar() and
-      result = getAnInputSymbolMatching(char)
-    }
-
-    /**
-     * Gets a `char` that occurs in a `pump` string.
-     */
-    private string getAProcessChar() { result = any(string s | isReDoSCandidate(_, s)).charAt(_) }
-  }
-
-  /**
-   * Holds if `term` may cause superlinear backtracking on strings containing many repetitions of `pump`.
-   * Gets the shortest string that causes superlinear backtracking.
-   */
-  private predicate isReDoSAttackable(RegExpTerm term, string pump, State s) {
-    exists(int i, string c | s = Match(term, i) |
-      c =
-        min(string w |
-          isCandidate(s, w) and
-          SuffixConstruction::reachesOnlyRejectableSuffixes(s, w)
-        |
-          w order by w.length(), w
-        ) and
-      pump = escape(rotate(c, i))
-    )
-  }
-
-  /**
-   * Holds if the state `s` (represented by the term `t`) can have backtracking with repetitions of `pump`.
-   *
-   * `prefixMsg` contains a friendly message for a prefix that reaches `s` (or `prefixMsg` is the empty string if the prefix is empty or if no prefix could be found).
-   */
-  predicate hasReDoSResult(RegExpTerm t, string pump, State s, string prefixMsg) {
-    isReDoSAttackable(t, pump, s) and
-    (
-      prefixMsg = "starting with '" + escape(Prefix::prefix(s)) + "' and " and
-      not Prefix::prefix(s) = ""
-      or
-      Prefix::prefix(s) = "" and prefixMsg = ""
-      or
-      not exists(Prefix::prefix(s)) and prefixMsg = ""
-    )
-  }
-
-  /**
-   * Gets the result of backslash-escaping newlines, carriage-returns and
-   * backslashes in `s`.
-   */
-  bindingset[s]
-  private string escape(string s) {
-    result =
-      s.replaceAll("\\", "\\\\")
-          .replaceAll("\n", "\\n")
-          .replaceAll("\r", "\\r")
-          .replaceAll("\t", "\\t")
-  }
-
-  /**
-   * Gets `str` with the last `i` characters moved to the front.
-   *
-   * We use this to adjust the pump string to match with the beginning of
-   * a RegExpTerm, so it doesn't start in the middle of a constant.
-   */
-  bindingset[str, i]
-  private string rotate(string str, int i) {
-    result = str.suffix(str.length() - i) + str.prefix(str.length() - i)
-  }
-}
-
-/**
- * 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`.
- */
-signature module CharTree {
-  /** A node in the tree. */
-  class CharNode;
-
-  /** Gets the previous node in the tree from `t`. */
-  CharNode getPrev(CharNode t);
-
-  /**
-   * Holds if `n` is at the end of a tree. I.e. a node that should have a result in the `Concretizer` module.
-   * Such a node can still have children.
-   */
-  predicate isARelevantEnd(CharNode n);
-
-  /** Gets a char associated with `t`. */
-  string getChar(CharNode t);
-}
-
-/**
- * Implements an algorithm for computing all possible strings
- * from following a tree of nodes (as described in `CharTree`).
- *
- * The string is build using one big concat, where all the chars are computed first.
- * See `concretize`.
- */
-module Concretizer<CharTree Impl> {
-  private class Node = Impl::CharNode;
-
-  private predicate getPrev = Impl::getPrev/1;
-
-  private predicate isARelevantEnd = Impl::isARelevantEnd/1;
-
-  private predicate getChar = Impl::getChar/1;
-
-  /** Holds if `n` is on a path from the root to a leaf, and is therefore relevant for the results in `concretize`. */
-  private predicate isRelevant(Node n) {
-    isARelevantEnd(n)
-    or
-    exists(Node succ | isRelevant(succ) | n = getPrev(succ))
-  }
-
-  /** Holds if `n` is a root with no predecessors. */
-  private predicate isRoot(Node n) { not exists(getPrev(n)) }
-
-  /** Gets the distance from a root to `n`. */
-  private int nodeDepth(Node n) {
-    result = 0 and isRoot(n)
-    or
-    isRelevant(n) and
-    exists(Node prev | result = nodeDepth(prev) + 1 | prev = getPrev(n))
-  }
-
-  /** Gets an ancestor of `end`, where `end` is a node that should have a result in `concretize`. */
-  private Node getAnAncestor(Node end) { isARelevantEnd(end) and result = getPrev*(end) }
-
-  /** Gets the `i`th character on the path from the root to `n`. */
-  pragma[noinline]
-  private string getPrefixChar(Node n, int i) {
-    exists(Node ancestor |
-      result = getChar(ancestor) and
-      ancestor = getAnAncestor(n) and
-      i = nodeDepth(ancestor)
-    )
-  }
-
-  /** Gets a string corresponding to `node`. */
-  language[monotonicAggregates]
-  string concretize(Node n) {
-    result = strictconcat(int i | exists(getPrefixChar(n, i)) | getPrefixChar(n, i) order by i)
-  }
-}
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// NfaUtils should be used directly from the shared pack, and not from this file.
+deprecated private import codeql.regex.nfa.NfaUtils::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/lib/semmle/python/security/regexp/NfaUtilsSpecific.qll b/python/ql/lib/semmle/python/security/regexp/NfaUtilsSpecific.qll
deleted file mode 100644
index 70ed5bcedad..00000000000
--- a/python/ql/lib/semmle/python/security/regexp/NfaUtilsSpecific.qll
+++ /dev/null
@@ -1,75 +0,0 @@
-/**
- * Provides Python-specific definitions for use in the NfaUtils module.
- */
-
-import python
-import semmle.python.RegexTreeView
-
-/**
- * Holds if `term` is an escape class representing e.g. `\d`.
- * `clazz` is which character class it represents, e.g. "d" for `\d`.
- */
-predicate isEscapeClass(RegExpTerm term, string clazz) {
-  exists(RegExpCharacterClassEscape escape | term = escape | escape.getValue() = clazz)
-}
-
-/**
- * Holds if `term` is a possessive quantifier.
- * As python's regexes do not support possessive quantifiers, this never holds, but is used by the shared library.
- */
-predicate isPossessive(RegExpQuantifier term) { none() }
-
-/**
- * Holds if the regex that `term` is part of is used in a way that ignores any leading prefix of the input it's matched against.
- * Not yet implemented for Python.
- */
-predicate matchesAnyPrefix(RegExpTerm term) { any() }
-
-/**
- * Holds if the regex that `term` is part of is used in a way that ignores any trailing suffix of the input it's matched against.
- * Not yet implemented for Python.
- */
-predicate matchesAnySuffix(RegExpTerm term) { any() }
-
-/**
- * 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()
-  }
-}
diff --git a/python/ql/lib/semmle/python/security/regexp/RegexpMatching.qll b/python/ql/lib/semmle/python/security/regexp/RegexpMatching.qll
index e2c75ff980b..d73a67add16 100644
--- a/python/ql/lib/semmle/python/security/regexp/RegexpMatching.qll
+++ b/python/ql/lib/semmle/python/security/regexp/RegexpMatching.qll
@@ -3,155 +3,7 @@
  * and for testing which capture groups are filled when a particular regexp matches a string.
  */
 
-import NfaUtils
-
-/** A root term */
-class RootTerm extends RegExpTerm {
-  RootTerm() { this.isRootTerm() }
-}
-
-/**
- * Holds if it should be tested whether `root` matches `str`.
- *
- * If `ignorePrefix` is true, then a regexp without a start anchor will be treated as if it had a start anchor.
- * E.g. a regular expression `/foo$/` will match any string that ends with "foo",
- * but if `ignorePrefix` is true, it will only match "foo".
- *
- * If `testWithGroups` is true, then the `RegexpMatching::fillsCaptureGroup` predicate can be used to determine which capture
- * groups are filled by a string.
- */
-signature predicate isRegexpMatchingCandidateSig(
-  RootTerm root, string str, boolean ignorePrefix, boolean testWithGroups
-);
-
-/**
- * A module for determining if a regexp matches a given string,
- * and reasoning about which capture groups are filled by a given string.
- *
- * The module parameter `isCandidate` determines which strings should be tested,
- * and the results can be read from the `matches` and `fillsCaptureGroup` predicates.
- */
-module RegexpMatching<isRegexpMatchingCandidateSig/4 isCandidate> {
-  /**
-   * Gets a state the regular expression `reg` can be in after matching the `i`th char in `str`.
-   * The regular expression is modeled as a non-determistic finite automaton,
-   * the regular expression can therefore be in multiple states after matching a character.
-   *
-   * It's a forward search to all possible states, and there is thus no guarantee that the state is on a path to an accepting state.
-   */
-  private State getAState(RootTerm reg, int i, string str, boolean ignorePrefix) {
-    // start state, the -1 position before any chars have been matched
-    i = -1 and
-    isCandidate(reg, str, ignorePrefix, _) and
-    result.getRepr().getRootTerm() = reg and
-    isStartState(result)
-    or
-    // recursive case
-    result = getAStateAfterMatching(reg, _, str, i, _, ignorePrefix)
-  }
-
-  /**
-   * Gets the next state after the `prev` state from `reg`.
-   * `prev` is the state after matching `fromIndex` chars in `str`,
-   * and the result is the state after matching `toIndex` chars in `str`.
-   *
-   * This predicate is used as a step relation in the forwards search (`getAState`),
-   * and also as a step relation in the later backwards search (`getAStateThatReachesAccept`).
-   */
-  private State getAStateAfterMatching(
-    RootTerm reg, State prev, string str, int toIndex, int fromIndex, boolean ignorePrefix
-  ) {
-    // the basic recursive case - outlined into a noopt helper to make performance work out.
-    result = getAStateAfterMatchingAux(reg, prev, str, toIndex, fromIndex, ignorePrefix)
-    or
-    // we can skip past word boundaries if the next char is a non-word char.
-    fromIndex = toIndex and
-    prev.getRepr() instanceof RegExpWordBoundary and
-    prev = getAState(reg, toIndex, str, ignorePrefix) and
-    after(prev.getRepr()) = result and
-    str.charAt(toIndex + 1).regexpMatch("\\W") // \W matches any non-word char.
-  }
-
-  pragma[noopt]
-  private State getAStateAfterMatchingAux(
-    RootTerm reg, State prev, string str, int toIndex, int fromIndex, boolean ignorePrefix
-  ) {
-    prev = getAState(reg, fromIndex, str, ignorePrefix) and
-    fromIndex = toIndex - 1 and
-    exists(string char | char = str.charAt(toIndex) | specializedDeltaClosed(prev, char, result)) and
-    not discardedPrefixStep(prev, result, ignorePrefix)
-  }
-
-  /** Holds if a step from `prev` to `next` should be discarded when the `ignorePrefix` flag is set. */
-  private predicate discardedPrefixStep(State prev, State next, boolean ignorePrefix) {
-    prev = mkMatch(any(RegExpRoot r)) and
-    ignorePrefix = true and
-    next = prev
-  }
-
-  // The `deltaClosed` relation specialized to the chars that exists in strings tested by a `MatchedRegExp`.
-  private predicate specializedDeltaClosed(State prev, string char, State next) {
-    deltaClosed(prev, specializedGetAnInputSymbolMatching(char), next)
-  }
-
-  // The `getAnInputSymbolMatching` relation specialized to the chars that exists in strings tested by a `MatchedRegExp`.
-  pragma[noinline]
-  private InputSymbol specializedGetAnInputSymbolMatching(string char) {
-    exists(string s, RootTerm r | isCandidate(r, s, _, _) | char = s.charAt(_)) and
-    result = getAnInputSymbolMatching(char)
-  }
-
-  /**
-   * Gets the `i`th state on a path to the accepting state when `reg` matches `str`.
-   * Starts with an accepting state as found by `getAState` and searches backwards
-   * to the start state through the reachable states (as found by `getAState`).
-   *
-   * This predicate satisfies the invariant that the result state can be reached with `i` steps from a start state,
-   * and an accepting state can be found after (`str.length() - 1 - i`) steps from the result.
-   * The result state is therefore always on a valid path where `reg` accepts `str`.
-   *
-   * This predicate is only used to find which capture groups a regular expression has filled,
-   * and thus the search is only performed for the strings in the `testWithGroups(..)` predicate.
-   */
-  private State getAStateThatReachesAccept(RootTerm reg, int i, string str, boolean ignorePrefix) {
-    // base case, reaches an accepting state from the last state in `getAState(..)`
-    isCandidate(reg, str, ignorePrefix, true) and
-    i = str.length() - 1 and
-    result = getAState(reg, i, str, ignorePrefix) and
-    epsilonSucc*(result) = Accept(_)
-    or
-    // recursive case. `next` is the next state to be matched after matching `prev`.
-    // this predicate is doing a backwards search, so `prev` is the result we are looking for.
-    exists(State next, State prev, int fromIndex, int toIndex |
-      next = getAStateThatReachesAccept(reg, toIndex, str, ignorePrefix) and
-      next = getAStateAfterMatching(reg, prev, str, toIndex, fromIndex, ignorePrefix) and
-      i = fromIndex and
-      result = prev
-    )
-  }
-
-  /** Gets the capture group number that `term` belongs to. */
-  private int group(RegExpTerm term) {
-    exists(RegExpGroup grp | grp.getNumber() = result | term.getParent*() = grp)
-  }
-
-  /**
-   * Holds if `reg` matches `str`, where `str` is in the `isCandidate` predicate.
-   */
-  predicate matches(RootTerm reg, string str) {
-    exists(State state | state = getAState(reg, str.length() - 1, str, _) |
-      epsilonSucc*(state) = Accept(_)
-    )
-  }
-
-  /**
-   * Holds if matching `str` against `reg` may fill capture group number `g`.
-   * Only holds if `str` is in the `testWithGroups` predicate.
-   */
-  predicate fillsCaptureGroup(RootTerm reg, string str, int g) {
-    exists(State s |
-      s = getAStateThatReachesAccept(reg, _, str, _) and
-      g = group(s.getRepr())
-    )
-  }
-}
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// RegexpMatching should be used directly from the shared pack, and not from this file.
+deprecated import codeql.regex.nfa.RegexpMatching::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/lib/semmle/python/security/regexp/SuperlinearBackTracking.qll b/python/ql/lib/semmle/python/security/regexp/SuperlinearBackTracking.qll
index 14a69dc0644..6eca3722e09 100644
--- a/python/ql/lib/semmle/python/security/regexp/SuperlinearBackTracking.qll
+++ b/python/ql/lib/semmle/python/security/regexp/SuperlinearBackTracking.qll
@@ -1,11 +1,4 @@
 /**
- * Provides classes for working with regular expressions that can
- * perform backtracking in superlinear time.
- */
-
-import NfaUtils
-
-/*
  * 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
@@ -42,377 +35,7 @@ import NfaUtils
  * It also doesn't find all transitions in the product automaton, which can cause false negatives.
  */
 
-/**
- * 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 representation 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) {
-    isReachableFromStartTuple(_, _, t, 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 + ")"
-    )
-  }
-}
-
-/**
- * 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`.
- */
-private predicate isReachableFromStartTuple(
-  State pivot, State succ, StateTuple tuple, Trace trace, int dist
-) {
-  exists(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace v |
-    isReachableFromStartTuple(pivot, succ, v, s1, s2, s3, tuple, dist) and
-    trace = Step(s1, s2, s3, v)
-  )
-}
-
-private predicate isReachableFromStartTuple(
-  State pivot, State succ, Trace trace, InputSymbol s1, InputSymbol s2, InputSymbol s3,
-  StateTuple tuple, int dist
-) {
-  // base case.
-  exists(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 = Nil() and
-    dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ))
-  )
-  or
-  // recursive case
-  exists(StateTuple p |
-    isReachableFromStartTuple(pivot, succ, p, trace, dist + 1) and
-    dist = distBackFromEnd(tuple, MkStateTuple(pivot, succ, succ)) and
-    step(p, s1, s2, s3, tuple)
-  )
-}
-
-/**
- * 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)
-}
-
-/** An implementation of a chain containing chars for use by `Concretizer`. */
-private module CharTreeImpl implements CharTree {
-  class CharNode = Trace;
-
-  CharNode getPrev(CharNode t) { t = Step(_, _, _, result) }
-
-  /** Holds if `n` is used in `isPumpable`. */
-  predicate isARelevantEnd(CharNode n) {
-    exists(State pivot, State succ |
-      isReachableFromStartTuple(pivot, succ, getAnEndTuple(pivot, succ), n, _)
-    )
-  }
-
-  string getChar(CharNode t) {
-    exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 | t = Step(s1, s2, s3, _) |
-      result = getAThreewayIntersect(s1, s2, s3)
-    )
-  }
-}
-
-/**
- * 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 = Concretizer<CharTreeImpl>::concretize(t)
-  )
-}
-
-/**
- * Holds if states starting in `state` can have polynomial backtracking with the string `pump`.
- */
-predicate isReDoSCandidate(State state, string pump) { isPumpable(_, state, pump) }
-
-/**
- * Holds if repetitions of `pump` at `t` will cause polynomial backtracking.
- */
-predicate polynomialReDoS(RegExpTerm t, string pump, string prefixMsg, RegExpTerm prev) {
-  exists(State s, State pivot |
-    ReDoSPruning<isReDoSCandidate/2>::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) {
-  polynomialReDoS(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 }
-}
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+// SuperlinearBackTracking should be used directly from the shared pack, and not from this file.
+deprecated private import codeql.regex.nfa.SuperlinearBackTracking::Make<TreeView> as Dep
+import Dep
diff --git a/python/ql/src/Security/CWE-020/OverlyLargeRange.ql b/python/ql/src/Security/CWE-020/OverlyLargeRange.ql
index b4d2caf5e80..6bf7f41d8ed 100644
--- a/python/ql/src/Security/CWE-020/OverlyLargeRange.ql
+++ b/python/ql/src/Security/CWE-020/OverlyLargeRange.ql
@@ -12,8 +12,9 @@
  *       external/cwe/cwe-020
  */
 
-import semmle.python.security.OverlyLargeRangeQuery
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+import codeql.regex.OverlyLargeRangeQuery::Make<TreeView>
 
-from RegExpCharacterRange range, string reason
+from TreeView::RegExpCharacterRange range, string reason
 where problem(range, reason)
 select range, "Suspicious character range that " + reason + "."
diff --git a/python/ql/src/Security/CWE-116/BadTagFilter.ql b/python/ql/src/Security/CWE-116/BadTagFilter.ql
index 654df65275b..afcf73f357a 100644
--- a/python/ql/src/Security/CWE-116/BadTagFilter.ql
+++ b/python/ql/src/Security/CWE-116/BadTagFilter.ql
@@ -14,7 +14,8 @@
  *       external/cwe/cwe-186
  */
 
-import semmle.python.security.BadTagFilterQuery
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+import codeql.regex.nfa.BadTagFilterQuery::Make<TreeView>
 
 from HtmlMatchingRegExp regexp, string msg
 where msg = min(string m | isBadRegexpFilter(regexp, m) | m order by m.length(), m) // there might be multiple, we arbitrarily pick the shortest one
diff --git a/python/ql/src/Security/CWE-730/PolynomialReDoS.ql b/python/ql/src/Security/CWE-730/PolynomialReDoS.ql
index 1637686c1d8..1b315c651c3 100644
--- a/python/ql/src/Security/CWE-730/PolynomialReDoS.ql
+++ b/python/ql/src/Security/CWE-730/PolynomialReDoS.ql
@@ -14,7 +14,6 @@
  */
 
 import python
-import semmle.python.security.regexp.SuperlinearBackTracking
 import semmle.python.security.dataflow.PolynomialReDoSQuery
 import DataFlow::PathGraph
 
diff --git a/python/ql/src/Security/CWE-730/ReDoS.ql b/python/ql/src/Security/CWE-730/ReDoS.ql
index 0e66d3cdb79..4ba35c598da 100644
--- a/python/ql/src/Security/CWE-730/ReDoS.ql
+++ b/python/ql/src/Security/CWE-730/ReDoS.ql
@@ -14,10 +14,10 @@
  *       external/cwe/cwe-400
  */
 
-import python
-import semmle.python.security.regexp.ExponentialBackTracking
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+import codeql.regex.nfa.ExponentialBackTracking::Make<TreeView>
 
-from RegExpTerm t, string pump, State s, string prefixMsg
+from TreeView::RegExpTerm t, string pump, State s, string prefixMsg
 where
   hasReDoSResult(t, pump, s, prefixMsg) and
   // exclude verbose mode regexes for now
diff --git a/python/ql/test/query-tests/Security/CWE-730-PolynomialReDoS/PolynomialBackTracking.ql b/python/ql/test/query-tests/Security/CWE-730-PolynomialReDoS/PolynomialBackTracking.ql
index 8d0aa2f8f91..19c905be1fe 100644
--- a/python/ql/test/query-tests/Security/CWE-730-PolynomialReDoS/PolynomialBackTracking.ql
+++ b/python/ql/test/query-tests/Security/CWE-730-PolynomialReDoS/PolynomialBackTracking.ql
@@ -1,5 +1,6 @@
 import python
-import semmle.python.security.regexp.SuperlinearBackTracking
+private import semmle.python.RegexTreeView::RegexTreeView as TreeView
+import codeql.regex.nfa.SuperlinearBackTracking::Make<TreeView>
 
 from PolynomialBackTrackingTerm t
-select t.getRegex(), t, t.getReason()
+select t.(TreeView::RegExpTerm).getRegex(), t, t.getReason()