FilesExpand file tree

main

/

UnboundList.qll

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

201 lines (168 loc) · 6.32 KB

main

/

UnboundList.qll

Copy path

Top

File metadata and controls

• Code
• Blame

201 lines (168 loc) · 6.32 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

/**

* 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

/** Provides 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) }

cached

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]

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 = "" }

bindingset[this]

private int stringLength() { result = super.length() }

/** 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 elem |

// it is more efficient to not create a capture group for the suffix, since

// `regexpCapture` will then always join in both groups, only to afterwards filter

// based on the requested group (the group number is not part of the binding set

// of `regexpCapture`)

elem = this.regexpCapture("^([0-9]+)\\..*$", 1) and

e = decode(elem) and

suffix = this.suffix(elem.length() + 1)

)

}

/** Holds if this list starts with `prefix`, followed by `e`. */

bindingset[this]

predicate isSnoc(UnboundList prefix, Element e) {

// same remark as above about not using multiple capture groups

prefix = this.regexpCapture("^(|.+\\.)[0-9]+\\.$", 1) and

e = decode(this.substring(prefix.stringLength(), this.stringLength() - 1))

}

/** Gets the head of this list, if any. */

bindingset[this]

Element getHead() { result = this.getElement(0) }

/**

* Gets the `i`th prefix of this list, if any.

*

* Only holds when this list is non-empty, and only returns proper prefixes.

*/

bindingset[this]

UnboundList getProperPrefix(int i) {

exists(string regexp, int occurrenceOffset | regexp = "[0-9]+\\." |

exists(this.regexpFind(regexp, i, occurrenceOffset)) and

result = this.prefix(occurrenceOffset)

)

}

/**

* Gets a prefix of this list, if any.

*

* Only holds when this list is non-empty, and only returns proper prefixes.

*/

bindingset[this]

UnboundList getAProperPrefix() { result = this.getProperPrefix(_) }

/**

* Gets a prefix of this list, including the list itself.

*/

bindingset[this]

UnboundList getAPrefix() { result = [this, this.getAProperPrefix()] }

/**

* Holds if this list is a prefix of `other`.

*

* This is equivalent to `this = other.getAPrefix()`, but more performant.

*/

bindingset[this, other]

predicate isPrefixOf(UnboundList other) { this = other.prefix(this.stringLength()) }

}

/** 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 element `e` onto `suffix`.

*/

bindingset[suffix]

UnboundList cons(Element e, UnboundList suffix) { result = singleton(e).append(suffix) }

/**

* Gets the list obtained by appending the element `e` after `prefix`.

*/

bindingset[prefix]

UnboundList snoc(UnboundList prefix, Element e) { result = prefix.append(singleton(e)) }

}

}