Shared: Add InverseAppend modules for effecient prefix matching

Author: hvitved

shared/util/codeql/util/Strings.qll

@@ -91,3 +91,194 @@ int asciiPrintable(string char) {
             .charAt(_)
     )
 }
+
+/**
+ * Escapes all characters in `s` that have special meaning in regular expressions.
+ */
+bindingset[s]
+string regexpEscape(string s) {
+  result = s.regexpReplaceAll("([\\\\.*+?\\[^\\]$(){}=!<>|:\\-])", "\\\\$1")
+}
+
+/** Provides the input to `InverseAppend`. */
+signature module InverseAppendInputSig {
+  /** A prefix matching result. */
+  bindingset[this]
+  class Result;
+
+  /**
+   * Holds if `prefix` is a prefix candidate with resulting value `res`.
+   */
+  predicate prefixCandidate(string prefix, Result res);
+}
+
+/** Provides the `inverseAppend` predicate. */
+module InverseAppend<InverseAppendInputSig Input> {
+  /**
+   * Holds if `s = prefix + suffix` with resulting value `res`.
+   *
+   * The predicate avoids unnecessary result fan-out by first constraining the
+   * prefix using a regular expression match.
+   */
+  bindingset[s]
+  predicate inverseAppend(string s, string prefix, string suffix, Input::Result res) {
+    exists(string regexp |
+      regexp =
+        "(" +
+          strictconcat(string prefixCand |
+            Input::prefixCandidate(prefixCand, _)
+          |
+            regexpEscape(prefixCand), "|"
+          ) + ").*" and
+      prefix = s.regexpCapture(regexp, 1) and
+      s = prefix + suffix and
+      Input::prefixCandidate(prefix, res)
+    )
+  }
+}
+
+/** Provides the input to `InverseAppend1`. */
+signature module InverseAppend1InputSig {
+  /** A prefix matching context. */
+  bindingset[this]
+  class C;
+
+  /** A prefix matching result. */
+  bindingset[this]
+  class Result;
+
+  /**
+   * Holds if `prefix` is a prefix candidate in the context `c`
+   * with resulting value `res`.
+   */
+  predicate prefixCandidate(string prefix, C c, Result res);
+}
+
+/** Provides the `inverseAppend` predicate. */
+module InverseAppend1<InverseAppend1InputSig Input> {
+  /**
+   * Holds if `s = prefix + suffix` in the context `c` with resulting
+   * value `res`.
+   *
+   * The predicate avoids unnecessary result fan-out by first constraining the
+   * prefix using a regular expression match.
+   */
+  bindingset[s]
+  predicate inverseAppend(string s, string prefix, string suffix, Input::C c, Input::Result res) {
+    exists(string regexp |
+      regexp =
+        "(" +
+          strictconcat(string prefixCand |
+            Input::prefixCandidate(prefixCand, c, _)
+          |
+            regexpEscape(prefixCand), "|"
+          ) + ").*" and
+      prefix = s.regexpCapture(regexp, 1) and
+      s = prefix + suffix and
+      Input::prefixCandidate(prefix, c, res)
+    )
+  }
+}
+
+/** Provides the input to `InverseAppend2`. */
+signature module InverseAppend2InputSig {
+  /** A prefix matching context. */
+  bindingset[this]
+  class C1;
+
+  /** A prefix matching context. */
+  bindingset[this]
+  class C2;
+
+  /** A prefix matching result. */
+  bindingset[this]
+  class Result;
+
+  /**
+   * Holds if `prefix` is a prefix candidate in the context `(c1, c2)`
+   * with resulting value `res`.
+   */
+  predicate prefixCandidate(string prefix, C1 c1, C2 c2, Result res);
+}
+
+/** Provides the `inverseAppend` predicate. */
+module InverseAppend2<InverseAppend2InputSig Input> {
+  /**
+   * Holds if `s = prefix + suffix` in the context `(c1, c2)` with resulting
+   * value `res`.
+   *
+   * The predicate avoids unnecessary result fan-out by first constraining the
+   * prefix using a regular expression match.
+   */
+  bindingset[s]
+  predicate inverseAppend(
+    string s, string prefix, string suffix, Input::C1 c1, Input::C2 c2, Input::Result res
+  ) {
+    exists(string regexp |
+      regexp =
+        "(" +
+          strictconcat(string prefixCand |
+            Input::prefixCandidate(prefixCand, c1, c2, _)
+          |
+            regexpEscape(prefixCand), "|"
+          ) + ").*" and
+      prefix = s.regexpCapture(regexp, 1) and
+      s = prefix + suffix and
+      Input::prefixCandidate(prefix, c1, c2, res)
+    )
+  }
+}
+
+/** Provides the input to `InverseAppend3`. */
+signature module InverseAppend3InputSig {
+  /** A prefix matching context. */
+  bindingset[this]
+  class C1;
+
+  /** A prefix matching context. */
+  bindingset[this]
+  class C2;
+
+  /** A prefix matching context. */
+  bindingset[this]
+  class C3;
+
+  /** A prefix matching result. */
+  bindingset[this]
+  class Result;
+
+  /**
+   * Holds if `prefix` is a prefix candidate in the context `(c1, c2, c3)`
+   * with resulting value `res`.
+   */
+  predicate prefixCandidate(string prefix, C1 c1, C2 c2, C3 c3, Result res);
+}
+
+/** Provides the `inverseAppend` predicate. */
+module InverseAppend3<InverseAppend3InputSig Input> {
+  /**
+   * Holds if `s = prefix + suffix` in the context `(c1, c2, c3)` with resulting
+   * value `res`.
+   *
+   * The predicate avoids unnecessary result fan-out by first constraining the
+   * prefix using a regular expression match.
+   */
+  bindingset[s]
+  predicate inverseAppend(
+    string s, string prefix, string suffix, Input::C1 c1, Input::C2 c2, Input::C3 c3,
+    Input::Result res
+  ) {
+    exists(string regexp |
+      regexp =
+        "(" +
+          strictconcat(string prefixCand |
+            Input::prefixCandidate(prefixCand, c1, c2, c3, _)
+          |
+            regexpEscape(prefixCand), "|"
+          ) + ").*" and
+      prefix = s.regexpCapture(regexp, 1) and
+      s = prefix + suffix and
+      Input::prefixCandidate(prefix, c1, c2, c3, res)
+    )
+  }
+}