refactor the concretize algorithm

Author: erik-krogh

java/ql/lib/semmle/code/java/security/performance/ExponentialBackTracking.qll

@@ -313,54 +313,30 @@ private StatePair getAForkPair(State fork) {
   result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
 }
 
-private predicate hasSuffix(Trace suffix, Trace t, int i) {
-  // Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
-  // recursive case, so instead we check it explicitly here.
-  t instanceof RelevantTrace and
-  i = 0 and
-  suffix = t
-  or
-  hasSuffix(Step(_, _, suffix), t, i - 1)
-}
-
-pragma[noinline]
-private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) {
-  hasSuffix(Step(s1, s2, _), t, i)
-}
+/** An implementation of a chain containing chars for use by `Concretizer`. */
+private module CharTreeImpl implements CharTree {
+  class CharNode = Trace;
 
-private class RelevantTrace extends Trace, Step {
-  RelevantTrace() {
-    exists(State fork, StatePair q |
-      isReachableFromFork(fork, q, this, _) and
-      q = getAForkPair(fork)
-    )
-  }
+  CharNode getPrev(CharNode t) { t = Step(_, _, result) }
 
-  pragma[noinline]
-  private string intersect(int i) {
-    exists(InputSymbol s1, InputSymbol s2 |
-      hasTuple(s1, s2, this, i) and
-      result = intersect(s1, s2)
-    )
+  /** 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, _))
   }
 
-  /** Gets a string corresponding to this trace. */
-  // the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
-  // not for recursion
-  language[monotonicAggregates]
-  string concretise() {
-    result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc)
+  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, RelevantTrace t |
+  exists(StatePair q, Trace t |
     isReachableFromFork(fork, q, t, _) and
     q = getAForkPair(fork) and
-    w = t.concretise()
+    w = Concretizer<CharTreeImpl>::concretize(t)
   )
 }
 

java/ql/lib/semmle/code/java/security/performance/ReDoSUtil.qll

@@ -1240,3 +1240,82 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
     result = str.suffix(str.length() - i) + str.prefix(str.length() - i)
   }
 }
+
+/**
+ * A module that describes a tree where each node has one or more accosiated characters.
+ * The root node has no accosiated 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.
+   * A leaf 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 prev | isRelevant(prev) | n = getPrev(prev))
+  }
+
+  /** 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 nodeDist(Node n) {
+    result = 0 and isRoot(n)
+    or
+    isRelevant(n) and
+    exists(Node prev | result = nodeDist(prev) + 1 | prev = getPrev(n))
+  }
+
+  /** Holds if `n` is part of a chain that we want to compute a string for. */
+  private Node getANodeInLongChain(Node end) {
+    isARelevantEnd(end) and result = end
+    or
+    exists(Node prev | prev = getANodeInLongChain(end) | result = getPrev(prev))
+  }
+
+  pragma[noinline]
+  private string getPrefixChar(Node n, int i) {
+    exists(Node prev |
+      result = getChar(prev) and
+      prev = getANodeInLongChain(n) and
+      i = nodeDist(n) - nodeDist(prev)
+    )
+  }
+
+  /** 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 desc)
+  }
+}

java/ql/lib/semmle/code/java/security/performance/SuperlinearBackTracking.qll

@@ -312,49 +312,24 @@ StateTuple getAnEndTuple(State pivot, State succ) {
   result = MkStateTuple(pivot, succ, succ)
 }
 
-private predicate hasSuffix(Trace suffix, Trace t, int i) {
-  // Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
-  // recursive case, so instead we check it explicitly here.
-  t instanceof RelevantTrace and
-  i = 0 and
-  suffix = t
-  or
-  hasSuffix(Step(_, _, _, suffix), t, i - 1)
-}
+/** An implementation of a chain containing chars for use by `Concretizer`. */
+private module CharTreeImpl implements CharTree {
+  class CharNode = Trace;
 
-pragma[noinline]
-private predicate hasTuple(InputSymbol s1, InputSymbol s2, InputSymbol s3, Trace t, int i) {
-  hasSuffix(Step(s1, s2, s3, _), t, i)
-}
+  CharNode getPrev(CharNode t) { t = Step(_, _, _, result) }
 
-private class RelevantTrace extends Trace, Step {
-  RelevantTrace() {
-    exists(State pivot, State succ, StateTuple q |
-      isReachableFromStartTuple(pivot, succ, q, this, _) and
-      q = getAnEndTuple(pivot, succ)
+  /** Holds if `n` is used in `isPumpable`. */
+  predicate isARelevantEnd(CharNode n) {
+    exists(State pivot, State succ |
+      isReachableFromStartTuple(pivot, succ, getAnEndTuple(pivot, succ), n, _)
     )
   }
 
-  pragma[noinline]
-  private string getAThreewayIntersect(int i) {
-    exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 |
-      hasTuple(s1, s2, s3, this, i) and
+  string getChar(CharNode t) {
+    exists(InputSymbol s1, InputSymbol s2, InputSymbol s3 | t = Step(s1, s2, s3, _) |
       result = getAThreewayIntersect(s1, s2, s3)
     )
   }
-
-  /** Gets a string corresponding to this trace. */
-  // the pragma is needed for the case where `getAThreewayIntersect(s1, s2, s3)` has multiple values,
-  // not for recursion
-  language[monotonicAggregates]
-  string concretise() {
-    result =
-      strictconcat(int i |
-        hasTuple(_, _, _, this, i)
-      |
-        this.getAThreewayIntersect(i) order by i desc
-      )
-  }
 }
 
 /**
@@ -370,10 +345,10 @@ private class RelevantTrace extends Trace, Step {
  * available in the `hasReDoSResult` predicate.
  */
 predicate isPumpable(State pivot, State succ, string pump) {
-  exists(StateTuple q, RelevantTrace t |
+  exists(StateTuple q, Trace t |
     isReachableFromStartTuple(pivot, succ, q, t, _) and
     q = getAnEndTuple(pivot, succ) and
-    pump = t.concretise()
+    pump = Concretizer<CharTreeImpl>::concretize(t)
   )
 }
 

javascript/ql/lib/semmle/javascript/security/performance/ExponentialBackTracking.qll

@@ -313,54 +313,30 @@ private StatePair getAForkPair(State fork) {
   result = MkStatePair(epsilonPred*(fork), epsilonPred*(fork))
 }
 
-private predicate hasSuffix(Trace suffix, Trace t, int i) {
-  // Declaring `t` to be a `RelevantTrace` currently causes a redundant check in the
-  // recursive case, so instead we check it explicitly here.
-  t instanceof RelevantTrace and
-  i = 0 and
-  suffix = t
-  or
-  hasSuffix(Step(_, _, suffix), t, i - 1)
-}
-
-pragma[noinline]
-private predicate hasTuple(InputSymbol s1, InputSymbol s2, Trace t, int i) {
-  hasSuffix(Step(s1, s2, _), t, i)
-}
+/** An implementation of a chain containing chars for use by `Concretizer`. */
+private module CharTreeImpl implements CharTree {
+  class CharNode = Trace;
 
-private class RelevantTrace extends Trace, Step {
-  RelevantTrace() {
-    exists(State fork, StatePair q |
-      isReachableFromFork(fork, q, this, _) and
-      q = getAForkPair(fork)
-    )
-  }
+  CharNode getPrev(CharNode t) { t = Step(_, _, result) }
 
-  pragma[noinline]
-  private string intersect(int i) {
-    exists(InputSymbol s1, InputSymbol s2 |
-      hasTuple(s1, s2, this, i) and
-      result = intersect(s1, s2)
-    )
+  /** 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, _))
   }
 
-  /** Gets a string corresponding to this trace. */
-  // the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
-  // not for recursion
-  language[monotonicAggregates]
-  string concretise() {
-    result = strictconcat(int i | hasTuple(_, _, this, i) | this.intersect(i) order by i desc)
+  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, RelevantTrace t |
+  exists(StatePair q, Trace t |
     isReachableFromFork(fork, q, t, _) and
     q = getAForkPair(fork) and
-    w = t.concretise()
+    w = Concretizer<CharTreeImpl>::concretize(t)
   )
 }
 

javascript/ql/lib/semmle/javascript/security/performance/ReDoSUtil.qll

@@ -1240,3 +1240,82 @@ module ReDoSPruning<isCandidateSig/2 isCandidate> {
     result = str.suffix(str.length() - i) + str.prefix(str.length() - i)
   }
 }
+
+/**
+ * A module that describes a tree where each node has one or more accosiated characters.
+ * The root node has no accosiated 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.
+   * A leaf 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 prev | isRelevant(prev) | n = getPrev(prev))
+  }
+
+  /** 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 nodeDist(Node n) {
+    result = 0 and isRoot(n)
+    or
+    isRelevant(n) and
+    exists(Node prev | result = nodeDist(prev) + 1 | prev = getPrev(n))
+  }
+
+  /** Holds if `n` is part of a chain that we want to compute a string for. */
+  private Node getANodeInLongChain(Node end) {
+    isARelevantEnd(end) and result = end
+    or
+    exists(Node prev | prev = getANodeInLongChain(end) | result = getPrev(prev))
+  }
+
+  pragma[noinline]
+  private string getPrefixChar(Node n, int i) {
+    exists(Node prev |
+      result = getChar(prev) and
+      prev = getANodeInLongChain(n) and
+      i = nodeDist(n) - nodeDist(prev)
+    )
+  }
+
+  /** 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 desc)
+  }
+}