mirror of
https://github.com/github/codeql.git
synced 2026-02-11 20:51:06 +01:00
Shared: Add library for unbound lists
This commit is contained in:
Tom Hvitved
@@ -224,25 +224,17 @@ signature module InputSig1<LocationSig Location> {
|
||||
|
||||
module Make1<LocationSig Location, InputSig1<Location> 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<Location> {
|
||||
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<DenseRankInput>::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<Location, UnboundListInput>
|
||||
|
||||
/**
|
||||
* A path into a type.
|
||||
@@ -274,101 +266,10 @@ module Make1<LocationSig Location, InputSig1<Location> 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<LocationSig Location, InputSig1<Location> 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))
|
||||
}
|
||||
|
||||
/**
|
||||
|
||||
153
shared/util/codeql/util/UnboundList.qll
Normal file
153
shared/util/codeql/util/UnboundList.qll
Normal file
@@ -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<LocationSig Location> {
|
||||
/** 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<LocationSig Location, InputSig<Location> 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<DenseRankInput>::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) }
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user