FilesExpand file tree

main

/

Option.qll

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

150 lines (124 loc) · 4.14 KB

main

/

Option.qll

Copy path

Top

File metadata and controls

• Code
• Blame

150 lines (124 loc) · 4.14 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

/** Provides a module for constructing optional versions of types. */

overlay[local?]

module;

private import Location

/** A type with `toString`. */

private signature class TypeWithToString {

bindingset[this]

string toString();

}

/** A type with `toString` and `hasLocationInfo` */

private signature class TypeWithLocationInfo {

bindingset[this]

string toString();

predicate hasLocationInfo(

string filePath, int startLine, int startColumn, int endLine, int endColumn

);

}

/**

* Constructs an `Option` type that is a disjoint union of the given type and an

* additional singleton element.

*/

module Option<TypeWithToString T> {

private newtype TOption =

TNone() or

TSome(T c)

/**

* An option type. This is either a singleton `None` or a `Some` wrapping the

* given type.

*/

class Option extends TOption {

/** Gets a textual representation of this element. */

string toString() {

this = TNone() and result = "(none)"

or

exists(T c | this = TSome(c) and result = c.toString())

}

/** Gets the wrapped element, if any. */

T asSome() { this = TSome(result) }

/** Holds if this option is the singleton `None`. */

predicate isNone() { this = TNone() }

}

/** The singleton `None` element. */

class None extends Option, TNone { }

/** A wrapper for the given type. */

class Some extends Option, TSome { }

/** Gets the given element wrapped as an `Option`. */

Some some(T c) { result = TSome(c) }

/** Gets the `None` value. */

None none_() { any() }

}

/**

* Constructs an `Option` type that is a disjoint union of the given type and an

* additional singleton element, and has a `hasLocationInfo` predicate.

* `T` must have a `hasLocationInfo` predicate.

*/

module OptionWithLocationInfo<TypeWithLocationInfo T> {

private module O = Option<T>;

final private class BaseOption = O::Option;

/**

* An option type. This is either a singleton `None` or a `Some` wrapping the

* given type.

*/

class Option extends BaseOption {

/**

* Holds if this element is at the specified location.

* The location spans column `startColumn` of line `startLine` to

* column `endColumn` of line `endLine` in file `filepath`.

* For more information, see

* [Providing locations in CodeQL queries](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).

*/

predicate hasLocationInfo(

string filePath, int startLine, int startColumn, int endLine, int endColumn

) {

this.isNone() and

filePath = "" and

startLine = 0 and

startColumn = 0 and

endLine = 0 and

endColumn = 0

or

this.asSome().hasLocationInfo(filePath, startLine, startColumn, endLine, endColumn)

}

}

/** The singleton `None` element. */

class None extends Option instanceof O::None { }

/** A wrapper for the given type. */

class Some extends Option instanceof O::Some { }

/** Gets the given element wrapped as an `Option`. */

Some some(T c) { result.asSome() = c }

}

private module WithLocation<LocationSig Location> {

signature class LocatableType {

bindingset[this]

string toString();

Location getLocation();

}

}

/**

* Constructs an `Option` type that is a disjoint union of the given type and an

* additional singleton element, and has a `getLocation` predicate.

* `T` must have a `getLocation` predicate with a result type of `Location`.

*/

module LocatableOption<LocationSig Location, WithLocation<Location>::LocatableType T> {

private module O = Option<T>;

final private class BaseOption = O::Option;

/**

* An option type. This is either a singleton `None` or a `Some` wrapping the

* given type.

*/

class Option extends BaseOption {

Location getLocation() {

result = this.asSome().getLocation()

or

this.isNone() and

result.hasLocationInfo("", 0, 0, 0, 0)

}

}

/** The singleton `None` element. */

class None extends Option instanceof O::None { }

/** A wrapper for the given type. */

class Some extends Option instanceof O::Some { }

/** Gets the given element wrapped as an `Option`. */

Some some(T c) { result.asSome() = c }

}