FazBrowse GitHub Viewer
|
Trending
|
URL:
|
Home
Tools:
[Download Repo ZIP]
[View Raw Code]
[Original HTTPS Page]
codeql/cpp/ql/src/Microsoft/SAL.qll at codeql-cli/v2.19.0 · github/codeql · GitHub
Uh oh!
There was an error while loading.
Please reload this page
.
github
/
codeql
Public
Notifications
You must be signed in to change notification settings
Fork
2.1k
Star
10k
Code
Issues
997
Pull requests
467
Discussions
Actions
Projects
Security and quality
0
Insights
Additional navigation options
Code
Issues
Pull requests
Discussions
Actions
Projects
Security and quality
Insights
Expand file tree
Breadcrumbs
codeql
/
cpp
/
ql
/
src
/
Microsoft
/
SAL.qll
Copy path
More file actions
More file actions
Latest commit
History
History
History
218 lines (194 loc) · 6.22 KB
Breadcrumbs
codeql
/
cpp
/
ql
/
src
/
Microsoft
/
SAL.qll
Copy path
File metadata and controls
218 lines (194 loc) · 6.22 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
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
/**
* Provides classes for identifying and reasoning about Microsoft source code
* annotation language (SAL) macros.
*/
import
cpp
/**
* A SAL macro defined in `sal.h` or a similar header file.
*/
class
SalMacro
extends
Macro
{
SalMacro
(
)
{
this
.
getFile
(
)
.
getBaseName
(
)
=
[
"sal.h"
,
"specstrings_strict.h"
,
"specstrings.h"
,
"w32p.h"
,
"minwindef.h"
]
and
(
// Dialect for Windows 8 and above
this
.
getName
(
)
.
matches
(
"\\_%\\_"
)
or
// Dialect for Windows 7
this
.
getName
(
)
.
matches
(
"\\_\\_%"
)
)
}
}
pragma
[
noinline
]
private
predicate
isTopLevelMacroAccess
(
MacroAccess
ma
)
{
not
exists
(
ma
.
getParentInvocation
(
)
)
}
/**
* An invocation of a SAL macro (excluding invocations inside other macros).
*/
class
SalAnnotation
extends
MacroInvocation
{
SalAnnotation
(
)
{
this
.
getMacro
(
)
instanceof
SalMacro
and
isTopLevelMacroAccess
(
this
)
}
/** Gets the `Declaration` annotated by `this`. */
Declaration
getDeclaration
(
)
{
annotatesAt
(
this
,
result
.
getADeclarationEntry
(
)
,
_
,
_
)
and
not
result
instanceof
Type
// exclude typedefs
}
/** Gets the `DeclarationEntry` annotated by `this`. */
DeclarationEntry
getDeclarationEntry
(
)
{
annotatesAt
(
this
,
result
,
_
,
_
)
and
not
result
instanceof
TypeDeclarationEntry
// exclude typedefs
}
}
/**
* A SAL macro indicating that the return value of a function should always be
* checked.
*/
class
SalCheckReturn
extends
SalAnnotation
{
SalCheckReturn
(
)
{
this
.
getMacro
(
)
.
(
SalMacro
)
.
getName
(
)
=
[
"_Check_return_"
,
"_Must_inspect_result_"
]
}
}
/**
* A SAL macro indicating that a pointer variable or return value should not be
* `NULL`.
*/
class
SalNotNull
extends
SalAnnotation
{
SalNotNull
(
)
{
exists
(
SalMacro
m
|
m
=
this
.
getMacro
(
)
|
not
m
.
getName
(
)
.
matches
(
"%\\_opt\\_%"
)
and
(
m
.
getName
(
)
.
matches
(
"_In%"
)
or
m
.
getName
(
)
.
matches
(
"_Out%"
)
or
m
.
getName
(
)
=
"_Ret_notnull_"
)
)
and
exists
(
Type
t
|
t
=
this
.
getDeclaration
(
)
.
(
Variable
)
.
getType
(
)
or
t
=
this
.
getDeclaration
(
)
.
(
Function
)
.
getType
(
)
|
t
.
getUnspecifiedType
(
)
instanceof
PointerType
)
}
}
/**
* A SAL macro indicating that a value may be `NULL`.
*/
class
SalMaybeNull
extends
SalAnnotation
{
SalMaybeNull
(
)
{
exists
(
SalMacro
m
|
m
=
this
.
getMacro
(
)
|
m
.
getName
(
)
.
matches
(
"%\\_opt\\_%"
)
or
m
.
getName
(
)
.
matches
(
"\\_Ret_maybenull\\_%"
)
or
m
.
getName
(
)
=
"_Result_nullonfailure_"
)
}
}
/**
* A parameter annotated by one or more SAL annotations.
*/
class
SalParameter
extends
Parameter
{
/** One of this parameter's annotations. */
SalAnnotation
a
;
SalParameter
(
)
{
annotatesAt
(
a
,
this
.
getADeclarationEntry
(
)
,
_
,
_
)
}
predicate
isIn
(
)
{
a
.
getMacroName
(
)
.
toLowerCase
(
)
.
matches
(
"%\\_in%"
)
}
predicate
isOut
(
)
{
a
.
getMacroName
(
)
.
toLowerCase
(
)
.
matches
(
"%\\_out%"
)
}
predicate
isInOut
(
)
{
a
.
getMacroName
(
)
.
toLowerCase
(
)
.
matches
(
"%\\_inout%"
)
}
}
///////////////////////////////////////////////////////////////////////////////
// Implementation details
/**
* Holds if `a` annotates the declaration entry `d` and
* its start position is the `idx`th position in `file` that holds a SAL element.
*/
private
predicate
annotatesAt
(
SalAnnotation
a
,
DeclarationEntry
d
,
File
file
,
int
idx
)
{
annotatesAtPosition
(
a
.
(
SalElement
)
.
getStartPosition
(
)
,
d
,
file
,
idx
)
}
/**
* Holds if `pos` is the `idx`th position in `file` that holds a SAL element,
* which annotates the declaration entry `d` (by occurring before it without
* any other declaration entries in between).
*/
// For performance reasons, do not mention the annotation itself here,
// but compute with positions instead. This performs better on databases
// with many annotations at the same position.
private
predicate
annotatesAtPosition
(
SalPosition
pos
,
DeclarationEntry
d
,
File
file
,
int
idx
)
{
pos
=
salRelevantPositionAt
(
file
,
idx
)
and
salAnnotationPos
(
pos
)
and
(
// Base case: `pos` right before `d`
d
.
(
SalElement
)
.
getStartPosition
(
)
=
salRelevantPositionAt
(
file
,
idx
+
1
)
or
// Recursive case: `pos` right before some annotation on `d`
annotatesAtPosition
(
_
,
d
,
file
,
idx
+
1
)
)
}
/**
* A SAL element, that is, a SAL annotation or a declaration entry
* that may have SAL annotations.
*/
class
SalElement
extends
Element
{
SalElement
(
)
{
containsSalAnnotation
(
this
.
(
DeclarationEntry
)
.
getFile
(
)
)
or
this
instanceof
SalAnnotation
}
predicate
hasStartPosition
(
File
file
,
int
line
,
int
col
)
{
exists
(
Location
loc
|
loc
=
this
.
getLocation
(
)
|
file
=
loc
.
getFile
(
)
and
line
=
loc
.
getStartLine
(
)
and
col
=
loc
.
getStartColumn
(
)
)
}
predicate
hasEndPosition
(
File
file
,
int
line
,
int
col
)
{
exists
(
Location
loc
|
loc
=
this
.
(
FunctionDeclarationEntry
)
.
getBlock
(
)
.
getLocation
(
)
or
this
=
any
(
VariableDeclarationEntry
vde
|
vde
.
isDefinition
(
)
and
loc
=
vde
.
getVariable
(
)
.
getInitializer
(
)
.
getLocation
(
)
)
|
file
=
loc
.
getFile
(
)
and
line
=
loc
.
getEndLine
(
)
and
col
=
loc
.
getEndColumn
(
)
)
}
SalPosition
getStartPosition
(
)
{
exists
(
File
file
,
int
line
,
int
col
|
this
.
hasStartPosition
(
file
,
line
,
col
)
and
result
=
MkSalPosition
(
file
,
line
,
col
)
)
}
}
/** Holds if `file` contains a SAL annotation. */
pragma
[
noinline
]
private
predicate
containsSalAnnotation
(
File
file
)
{
any
(
SalAnnotation
a
)
.
getFile
(
)
=
file
}
/**
* A source-file position of a `SALElement`. Unlike location, this denotes a
* point in the file rather than a range.
*/
private
newtype
SalPosition
=
MkSalPosition
(
File
file
,
int
line
,
int
col
)
{
exists
(
SalElement
e
|
e
.
hasStartPosition
(
file
,
line
,
col
)
or
e
.
hasEndPosition
(
file
,
line
,
col
)
)
}
/** Holds if `pos` is the start position of a SAL annotation. */
pragma
[
noinline
]
private
predicate
salAnnotationPos
(
SalPosition
pos
)
{
any
(
SalAnnotation
a
)
.
(
SalElement
)
.
getStartPosition
(
)
=
pos
}
/**
* Gets the `idx`th position in `file` that holds a SAL element,
* ordering positions lexicographically by their start line and start column.
*/
private
SalPosition
salRelevantPositionAt
(
File
file
,
int
idx
)
{
result
=
rank
[
idx
]
(
SalPosition
pos
,
int
line
,
int
col
|
pos
=
MkSalPosition
(
file
,
line
,
col
)
|
pos
order
by
line
,
col
)
}
Back
|
FazBrowse Home
|
New Git URL