From 08339fe0dfcb56fa5bd0a0b954e47e7f5ff6abf0 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Wed, 17 Dec 2025 13:08:11 +0100 Subject: [PATCH 1/2] Shared: Add library for unbound lists --- .../typeinference/internal/TypeInference.qll | 121 ++------------ shared/util/codeql/util/UnboundList.qll | 153 ++++++++++++++++++ 2 files changed, 162 insertions(+), 112 deletions(-) create mode 100644 shared/util/codeql/util/UnboundList.qll diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 4bb348979c1c..f53f15b5a6ab 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -224,25 +224,17 @@ signature module InputSig1 { module Make1 Input1> { private import Input1 + private import codeql.util.UnboundList as UnboundListImpl - private module TypeParameter { - private import codeql.util.DenseRank + private module UnboundListInput implements UnboundListImpl::InputSig { + class Element = TypeParameter; - private module DenseRankInput implements DenseRankInputSig { - class Ranked = TypeParameter; + predicate getId = getTypeParameterId/1; - predicate getRank = getTypeParameterId/1; - } - - int getRank(TypeParameter tp) { tp = DenseRank::denseRank(result) } - - string encode(TypeParameter tp) { result = getRank(tp).toString() } - - bindingset[s] - TypeParameter decode(string s) { encode(result) = s } + predicate getLengthLimit = getTypePathLimit/0; } - final private class String = string; + private import UnboundListImpl::Make /** * A path into a type. @@ -274,101 +266,10 @@ module Make1 Input1> { * implementation uses unique type parameter identifiers, in order to not mix * up type parameters from different types. */ - class TypePath extends String { - bindingset[this] - TypePath() { exists(this) } - - bindingset[this] - private TypeParameter getTypeParameter(int i) { - result = TypeParameter::decode(this.splitAt(".", i)) - } - - /** Gets a textual representation of this type path. */ - bindingset[this] - string toString() { - result = - concat(int i, TypeParameter tp | - tp = this.getTypeParameter(i) - | - tp.toString(), "." order by i - ) - } - - /** Holds if this type path is empty. */ - predicate isEmpty() { this = "" } - - /** Gets the length of this path. */ - bindingset[this] - pragma[inline_late] - int length() { - // Same as - // `result = count(this.indexOf("."))` - // but performs better because it doesn't use an aggregate - result = this.regexpReplaceAll("[0-9]+", "").length() - } - - /** Gets the path obtained by appending `suffix` onto this path. */ - bindingset[this, suffix] - TypePath append(TypePath suffix) { - result = this + suffix and - ( - not exists(getTypePathLimit()) - or - result.length() <= getTypePathLimit() - ) - } - - /** - * Gets the path obtained by appending `suffix` onto this path. - * - * Unlike `append`, this predicate has `result` in the binding set, - * so there is no need to check the length of `result`. - */ - bindingset[this, result] - TypePath appendInverse(TypePath suffix) { suffix = result.stripPrefix(this) } - - /** Gets the path obtained by removing `prefix` from this path. */ - bindingset[this, prefix] - TypePath stripPrefix(TypePath prefix) { this = prefix + result } - - /** Holds if this path starts with `tp`, followed by `suffix`. */ - bindingset[this] - predicate isCons(TypeParameter tp, TypePath suffix) { - exists(string regexp | regexp = "([0-9]+)\\.(.*)" | - tp = TypeParameter::decode(this.regexpCapture(regexp, 1)) and - suffix = this.regexpCapture(regexp, 2) - ) - } - - /** Holds if this path starts with `prefix`, followed by `tp`. */ - bindingset[this] - predicate isSnoc(TypePath prefix, TypeParameter tp) { - exists(string regexp | regexp = "(|.+\\.)([0-9]+)\\." | - prefix = this.regexpCapture(regexp, 1) and - tp = TypeParameter::decode(this.regexpCapture(regexp, 2)) - ) - } - - /** Gets the head of this path, if any. */ - bindingset[this] - TypeParameter getHead() { result = this.getTypeParameter(0) } - } + class TypePath = UnboundList; /** Provides predicates for constructing `TypePath`s. */ - module TypePath { - /** Gets the empty type path. */ - TypePath nil() { result.isEmpty() } - - /** Gets the singleton type path `tp`. */ - TypePath singleton(TypeParameter tp) { result = TypeParameter::encode(tp) + "." } - - /** - * Gets the type path obtained by appending the singleton type path `tp` - * onto `suffix`. - */ - bindingset[suffix] - TypePath cons(TypeParameter tp, TypePath suffix) { result = singleton(tp).append(suffix) } - } + module TypePath = UnboundList; /** * A class that has a type tree associated with it. @@ -600,11 +501,7 @@ module Make1 Input1> { private TypeParameter getNthTypeParameter(TypeAbstraction abs, int i) { result = - rank[i + 1](TypeParameter tp | - tp = abs.getATypeParameter() - | - tp order by TypeParameter::getRank(tp) - ) + rank[i + 1](TypeParameter tp | tp = abs.getATypeParameter() | tp order by getRank(tp)) } /** diff --git a/shared/util/codeql/util/UnboundList.qll b/shared/util/codeql/util/UnboundList.qll new file mode 100644 index 000000000000..78432fb77dd4 --- /dev/null +++ b/shared/util/codeql/util/UnboundList.qll @@ -0,0 +1,153 @@ +/** + * Provides logic for representing unbound lists. + * + * The lists are represented internally as strings, and generally it should + * be preferred to instead use a `newtype` representation, but in certain + * cases where this is not feasible (typically because of performance) unbound + * lists can be used. + */ +overlay[local?] +module; + +private import Location + +/** Provide the input to `Make`. */ +signature module InputSig { + /** An element. */ + class Element { + /** Gets a textual representation of this element. */ + string toString(); + + /** Gets the location of this element. */ + Location getLocation(); + } + + /** Gets a unique ID used to identify element `e` amongst all elements. */ + int getId(Element e); + + /** + * Gets a textual representation for element `e`, which will be used in the + * `toString` representation for unbound lists. + */ + default string getElementString(Element e) { result = e.toString() } + + /** Gets an optional length limit for unbound lists. */ + default int getLengthLimit() { none() } +} + +final private class String = string; + +/** Provides the `UnboundList` implementation. */ +module Make Input> { + private import Input + private import codeql.util.DenseRank + + // Use dense ranking to assign compact IDs to elements + private module DenseRankInput implements DenseRankInputSig { + class Ranked = Element; + + predicate getRank = getId/1; + } + + /** Gets the rank of element `e`, which is used internally in the string encoding. */ + int getRank(Element e) { e = DenseRank::denseRank(result) } + + private string encode(Element e) { result = getRank(e).toString() } + + bindingset[s] + private Element decode(string s) { encode(result) = s } + + /** + * An unbound list encoded as a string. + */ + class UnboundList extends String { + bindingset[this] + UnboundList() { exists(this) } + + /** Gets the `i`th element in this list. */ + bindingset[this] + private Element getElement(int i) { result = decode(this.splitAt(".", i)) } + + /** Gets a textual representation of this list. */ + bindingset[this] + string toString() { + result = + concat(int i, Element e | e = this.getElement(i) | getElementString(e), "." order by i) + } + + /** Holds if this list is empty. */ + predicate isEmpty() { this = "" } + + /** Gets the length of this list. */ + bindingset[this] + pragma[inline_late] + int length() { + // Same as + // `result = count(this.indexOf("."))` + // but performs better because it doesn't use an aggregate + result = this.regexpReplaceAll("[0-9]+", "").length() + } + + /** Gets the list obtained by appending `suffix` onto this list. */ + bindingset[this, suffix] + UnboundList append(UnboundList suffix) { + result = this + suffix and + ( + not exists(getLengthLimit()) + or + result.length() <= getLengthLimit() + ) + } + + /** + * Gets the list obtained by appending `suffix` onto this list. + * + * Unlike `append`, this predicate has `result` in the binding set, + * so there is no need to check the length of `result`. + */ + bindingset[this, result] + UnboundList appendInverse(UnboundList suffix) { suffix = result.stripPrefix(this) } + + /** Gets the list obtained by removing `prefix` from this list. */ + bindingset[this, prefix] + UnboundList stripPrefix(UnboundList prefix) { this = prefix + result } + + /** Holds if this list starts with `e`, followed by `suffix`. */ + bindingset[this] + predicate isCons(Element e, UnboundList suffix) { + exists(string regexp | regexp = "([0-9]+)\\.(.*)" | + e = decode(this.regexpCapture(regexp, 1)) and + suffix = this.regexpCapture(regexp, 2) + ) + } + + /** Holds if this list starts with `prefix`, followed by `e`. */ + bindingset[this] + predicate isSnoc(UnboundList prefix, Element e) { + exists(string regexp | regexp = "(|.+\\.)([0-9]+)\\." | + prefix = this.regexpCapture(regexp, 1) and + e = decode(this.regexpCapture(regexp, 2)) + ) + } + + /** Gets the head of this list, if any. */ + bindingset[this] + Element getHead() { result = this.getElement(0) } + } + + /** Provides predicates for constructing `UnboundList`s. */ + module UnboundList { + /** Gets the empty list. */ + UnboundList nil() { result.isEmpty() } + + /** Gets the singleton list `e`. */ + UnboundList singleton(Element e) { result = encode(e) + "." } + + /** + * Gets the list obtained by appending the singleton list `e` + * onto `suffix`. + */ + bindingset[suffix] + UnboundList cons(Element e, UnboundList suffix) { result = singleton(e).append(suffix) } + } +} From b6cda4a29bd67a03b63e4f4f3a7b3a7994f0b7d4 Mon Sep 17 00:00:00 2001 From: Tom Hvitved Date: Wed, 17 Dec 2025 13:44:47 +0100 Subject: [PATCH 2/2] Update shared/util/codeql/util/UnboundList.qll Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- shared/util/codeql/util/UnboundList.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/util/codeql/util/UnboundList.qll b/shared/util/codeql/util/UnboundList.qll index 78432fb77dd4..d9a8b905a135 100644 --- a/shared/util/codeql/util/UnboundList.qll +++ b/shared/util/codeql/util/UnboundList.qll @@ -11,7 +11,7 @@ module; private import Location -/** Provide the input to `Make`. */ +/** Provides the input to `Make`. */ signature module InputSig { /** An element. */ class Element {