Skip to content

Commit ed02c2c

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

File tree

2 files changed

+160
-112
lines changed

2 files changed

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

0 commit comments

Comments
 (0)