Skip to content

Commit 08339fe

Browse files
hvitvedhvitved
committed
Shared: Add library for unbound lists
1 parent 802c465 commit 08339fe

File tree

2 files changed

+162
-112
lines changed

2 files changed

+162
-112
lines changed

‎shared/typeinference/codeql/typeinference/internal/TypeInference.qll‎

Lines changed: 9 additions & 112 deletions
Original file line numberDiff line numberDiff line change
@@ -224,25 +224,17 @@ signature module InputSig1<LocationSig Location> {
224224

225225
module Make1<LocationSig Location, InputSig1<Location> Input1> {
226226
private import Input1
227+
private import codeql.util.UnboundList as UnboundListImpl
227228

228-
private module TypeParameter {
229-
private import codeql.util.DenseRank
229+
private module UnboundListInput implements UnboundListImpl::InputSig<Location> {
230+
class Element = TypeParameter;
230231

231-
private module DenseRankInput implements DenseRankInputSig {
232-
class Ranked = TypeParameter;
232+
predicate getId = getTypeParameterId/1;
233233

234-
predicate getRank = getTypeParameterId/1;
235-
}
236-
237-
int getRank(TypeParameter tp) { tp = DenseRank<DenseRankInput>::denseRank(result) }
238-
239-
string encode(TypeParameter tp) { result = getRank(tp).toString() }
240-
241-
bindingset[s]
242-
TypeParameter decode(string s) { encode(result) = s }
234+
predicate getLengthLimit = getTypePathLimit/0;
243235
}
244236

245-
final private class String = string;
237+
private import UnboundListImpl::Make<Location, UnboundListInput>
246238

247239
/**
248240
* A path into a type.
@@ -274,101 +266,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
274266
* implementation uses unique type parameter identifiers, in order to not mix
275267
* up type parameters from different types.
276268
*/
277-
class TypePath extends String {
278-
bindingset[this]
279-
TypePath() { exists(this) }
280-
281-
bindingset[this]
282-
private TypeParameter getTypeParameter(int i) {
283-
result = TypeParameter::decode(this.splitAt(".", i))
284-
}
285-
286-
/** Gets a textual representation of this type path. */
287-
bindingset[this]
288-
string toString() {
289-
result =
290-
concat(int i, TypeParameter tp |
291-
tp = this.getTypeParameter(i)
292-
|
293-
tp.toString(), "." order by i
294-
)
295-
}
296-
297-
/** Holds if this type path is empty. */
298-
predicate isEmpty() { this = "" }
299-
300-
/** Gets the length of this path. */
301-
bindingset[this]
302-
pragma[inline_late]
303-
int length() {
304-
// Same as
305-
// `result = count(this.indexOf("."))`
306-
// but performs better because it doesn't use an aggregate
307-
result = this.regexpReplaceAll("[0-9]+", "").length()
308-
}
309-
310-
/** Gets the path obtained by appending `suffix` onto this path. */
311-
bindingset[this, suffix]
312-
TypePath append(TypePath suffix) {
313-
result = this + suffix and
314-
(
315-
not exists(getTypePathLimit())
316-
or
317-
result.length() <= getTypePathLimit()
318-
)
319-
}
320-
321-
/**
322-
* Gets the path obtained by appending `suffix` onto this path.
323-
*
324-
* Unlike `append`, this predicate has `result` in the binding set,
325-
* so there is no need to check the length of `result`.
326-
*/
327-
bindingset[this, result]
328-
TypePath appendInverse(TypePath suffix) { suffix = result.stripPrefix(this) }
329-
330-
/** Gets the path obtained by removing `prefix` from this path. */
331-
bindingset[this, prefix]
332-
TypePath stripPrefix(TypePath prefix) { this = prefix + result }
333-
334-
/** Holds if this path starts with `tp`, followed by `suffix`. */
335-
bindingset[this]
336-
predicate isCons(TypeParameter tp, TypePath suffix) {
337-
exists(string regexp | regexp = "([0-9]+)\\.(.*)" |
338-
tp = TypeParameter::decode(this.regexpCapture(regexp, 1)) and
339-
suffix = this.regexpCapture(regexp, 2)
340-
)
341-
}
342-
343-
/** Holds if this path starts with `prefix`, followed by `tp`. */
344-
bindingset[this]
345-
predicate isSnoc(TypePath prefix, TypeParameter tp) {
346-
exists(string regexp | regexp = "(|.+\\.)([0-9]+)\\." |
347-
prefix = this.regexpCapture(regexp, 1) and
348-
tp = TypeParameter::decode(this.regexpCapture(regexp, 2))
349-
)
350-
}
351-
352-
/** Gets the head of this path, if any. */
353-
bindingset[this]
354-
TypeParameter getHead() { result = this.getTypeParameter(0) }
355-
}
269+
class TypePath = UnboundList;
356270

357271
/** Provides predicates for constructing `TypePath`s. */
358-
module TypePath {
359-
/** Gets the empty type path. */
360-
TypePath nil() { result.isEmpty() }
361-
362-
/** Gets the singleton type path `tp`. */
363-
TypePath singleton(TypeParameter tp) { result = TypeParameter::encode(tp) + "." }
364-
365-
/**
366-
* Gets the type path obtained by appending the singleton type path `tp`
367-
* onto `suffix`.
368-
*/
369-
bindingset[suffix]
370-
TypePath cons(TypeParameter tp, TypePath suffix) { result = singleton(tp).append(suffix) }
371-
}
272+
module TypePath = UnboundList;
372273

373274
/**
374275
* A class that has a type tree associated with it.
@@ -600,11 +501,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
600501

601502
private TypeParameter getNthTypeParameter(TypeAbstraction abs, int i) {
602503
result =
603-
rank[i + 1](TypeParameter tp |
604-
tp = abs.getATypeParameter()
605-
|
606-
tp order by TypeParameter::getRank(tp)
607-
)
504+
rank[i + 1](TypeParameter tp | tp = abs.getATypeParameter() | tp order by getRank(tp))
608505
}
609506

610507
/**

‎shared/util/codeql/util/UnboundList.qll‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
/**
2+
* Provides logic for representing unbound lists.
3+
*
4+
* The lists are represented internally as strings, and generally it should
5+
* be preferred to instead use a `newtype` representation, but in certain
6+
* cases where this is not feasible (typically because of performance) unbound
7+
* lists can be used.
8+
*/
9+
overlay[local?]
10+
module;
11+
12+
private import Location
13+
14+
/** Provide the input to `Make`. */
15+
signature module InputSig<LocationSig Location> {
16+
/** An element. */
17+
class Element {
18+
/** Gets a textual representation of this element. */
19+
string toString();
20+
21+
/** Gets the location of this element. */
22+
Location getLocation();
23+
}
24+
25+
/** Gets a unique ID used to identify element `e` amongst all elements. */
26+
int getId(Element e);
27+
28+
/**
29+
* Gets a textual representation for element `e`, which will be used in the
30+
* `toString` representation for unbound lists.
31+
*/
32+
default string getElementString(Element e) { result = e.toString() }
33+
34+
/** Gets an optional length limit for unbound lists. */
35+
default int getLengthLimit() { none() }
36+
}
37+
38+
final private class String = string;
39+
40+
/** Provides the `UnboundList` implementation. */
41+
module Make<LocationSig Location, InputSig<Location> Input> {
42+
private import Input
43+
private import codeql.util.DenseRank
44+
45+
// Use dense ranking to assign compact IDs to elements
46+
private module DenseRankInput implements DenseRankInputSig {
47+
class Ranked = Element;
48+
49+
predicate getRank = getId/1;
50+
}
51+
52+
/** Gets the rank of element `e`, which is used internally in the string encoding. */
53+
int getRank(Element e) { e = DenseRank<DenseRankInput>::denseRank(result) }
54+
55+
private string encode(Element e) { result = getRank(e).toString() }
56+
57+
bindingset[s]
58+
private Element decode(string s) { encode(result) = s }
59+
60+
/**
61+
* An unbound list encoded as a string.
62+
*/
63+
class UnboundList extends String {
64+
bindingset[this]
65+
UnboundList() { exists(this) }
66+
67+
/** Gets the `i`th element in this list. */
68+
bindingset[this]
69+
private Element getElement(int i) { result = decode(this.splitAt(".", i)) }
70+
71+
/** Gets a textual representation of this list. */
72+
bindingset[this]
73+
string toString() {
74+
result =
75+
concat(int i, Element e | e = this.getElement(i) | getElementString(e), "." order by i)
76+
}
77+
78+
/** Holds if this list is empty. */
79+
predicate isEmpty() { this = "" }
80+
81+
/** Gets the length of this list. */
82+
bindingset[this]
83+
pragma[inline_late]
84+
int length() {
85+
// Same as
86+
// `result = count(this.indexOf("."))`
87+
// but performs better because it doesn't use an aggregate
88+
result = this.regexpReplaceAll("[0-9]+", "").length()
89+
}
90+
91+
/** Gets the list obtained by appending `suffix` onto this list. */
92+
bindingset[this, suffix]
93+
UnboundList append(UnboundList suffix) {
94+
result = this + suffix and
95+
(
96+
not exists(getLengthLimit())
97+
or
98+
result.length() <= getLengthLimit()
99+
)
100+
}
101+
102+
/**
103+
* Gets the list obtained by appending `suffix` onto this list.
104+
*
105+
* Unlike `append`, this predicate has `result` in the binding set,
106+
* so there is no need to check the length of `result`.
107+
*/
108+
bindingset[this, result]
109+
UnboundList appendInverse(UnboundList suffix) { suffix = result.stripPrefix(this) }
110+
111+
/** Gets the list obtained by removing `prefix` from this list. */
112+
bindingset[this, prefix]
113+
UnboundList stripPrefix(UnboundList prefix) { this = prefix + result }
114+
115+
/** Holds if this list starts with `e`, followed by `suffix`. */
116+
bindingset[this]
117+
predicate isCons(Element e, UnboundList suffix) {
118+
exists(string regexp | regexp = "([0-9]+)\\.(.*)" |
119+
e = decode(this.regexpCapture(regexp, 1)) and
120+
suffix = this.regexpCapture(regexp, 2)
121+
)
122+
}
123+
124+
/** Holds if this list starts with `prefix`, followed by `e`. */
125+
bindingset[this]
126+
predicate isSnoc(UnboundList prefix, Element e) {
127+
exists(string regexp | regexp = "(|.+\\.)([0-9]+)\\." |
128+
prefix = this.regexpCapture(regexp, 1) and
129+
e = decode(this.regexpCapture(regexp, 2))
130+
)
131+
}
132+
133+
/** Gets the head of this list, if any. */
134+
bindingset[this]
135+
Element getHead() { result = this.getElement(0) }
136+
}
137+
138+
/** Provides predicates for constructing `UnboundList`s. */
139+
module UnboundList {
140+
/** Gets the empty list. */
141+
UnboundList nil() { result.isEmpty() }
142+
143+
/** Gets the singleton list `e`. */
144+
UnboundList singleton(Element e) { result = encode(e) + "." }
145+
146+
/**
147+
* Gets the list obtained by appending the singleton list `e`
148+
* onto `suffix`.
149+
*/
150+
bindingset[suffix]
151+
UnboundList cons(Element e, UnboundList suffix) { result = singleton(e).append(suffix) }
152+
}
153+
}

0 commit comments

Comments
 (0)