-
-
Notifications
You must be signed in to change notification settings - Fork 5.5k
/
effects.jl
350 lines (318 loc) · 14.4 KB
/
effects.jl
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
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
"""
effects::Effects
Represents computational effects of a method call.
The effects are a composition of different effect bits that represent some program property
of the method being analyzed. They are represented as `Bool` or `UInt8` bits with the
following meanings:
- `consistent::UInt8`:
* `ALWAYS_TRUE`: this method is guaranteed to return or terminate consistently.
* `ALWAYS_FALSE`: this method may be not return or terminate consistently, and there is
no need for further analysis with respect to this effect property as this conclusion
will not be refined anyway.
* `CONSISTENT_IF_NOTRETURNED`: the `:consistent`-cy of this method can later be refined to
`ALWAYS_TRUE` in a case when the return value of this method never involves newly
allocated mutable objects.
* `CONSISTENT_IF_INACCESSIBLEMEMONLY`: the `:consistent`-cy of this method can later be
refined to `ALWAYS_TRUE` in a case when `:inaccessiblememonly` is proven.
- `effect_free::UInt8`:
* `ALWAYS_TRUE`: this method is free from externally semantically visible side effects.
* `ALWAYS_FALSE`: this method may not be free from externally semantically visible side effects, and there is
no need for further analysis with respect to this effect property as this conclusion
will not be refined anyway.
* `EFFECT_FREE_IF_INACCESSIBLEMEMONLY`: the `:effect-free`-ness of this method can later be
refined to `ALWAYS_TRUE` in a case when `:inaccessiblememonly` is proven.
- `nothrow::Bool`: this method is guaranteed to not throw an exception.
If the execution of this method may raise `MethodError`s and similar exceptions, then
the method is not considered as `:nothrow`.
However, note that environment-dependent errors like `StackOverflowError` or `InterruptException`
are not modeled by this effect and thus a method that may result in `StackOverflowError`
does not necessarily need to taint `:nothrow` (although it should usually taint `:terminates` too).
- `terminates::Bool`: this method is guaranteed to terminate.
- `notaskstate::Bool`: this method does not access any state bound to the current
task and may thus be moved to a different task without changing observable
behavior. Note that this currently implies that `noyield` as well, since
yielding modifies the state of the current task, though this may be split
in the future.
- `inaccessiblememonly::UInt8`:
* `ALWAYS_TRUE`: this method does not access or modify externally accessible mutable memory.
This state corresponds to LLVM's `inaccessiblememonly` function attribute.
* `ALWAYS_FALSE`: this method may access or modify externally accessible mutable memory.
* `INACCESSIBLEMEM_OR_ARGMEMONLY`: this method does not access or modify externally accessible mutable memory,
except that it may access or modify mutable memory pointed to by its call arguments.
This may later be refined to `ALWAYS_TRUE` in a case when call arguments are known to be immutable.
This state corresponds to LLVM's `inaccessiblemem_or_argmemonly` function attribute.
- `noub::Bool`: indicates that the method will not execute any undefined behavior (for any input).
Note that undefined behavior may technically cause the method to violate any other effect
assertions (such as `:consistent` or `:effect_free`) as well, but we do not model this,
and they assume the absence of undefined behavior.
- `nonoverlayed::Bool`: indicates that any methods that may be called within this method
are not defined in an [overlayed method table](@ref OverlayMethodTable).
- `noinbounds::Bool`: If set, indicates that this method does not read the parent's `:inbounds`
state. In particular, it does not have any reached `:boundscheck` exprs, not propagates inbounds
to any children that do.
Note that the representations above are just internal implementation details and thus likely
to change in the future. See [`Base.@assume_effects`](@ref) for more detailed explanation
on the definitions of these properties.
Along the abstract interpretation, `Effects` at each statement are analyzed locally and they
are merged into the single global `Effects` that represents the entire effects of the
analyzed method (see the implementation of `merge_effects!`). Each effect property is
initialized with `ALWAYS_TRUE`/`true` and then transitioned towards `ALWAYS_FALSE`/`false`.
Note that within the current flow-insensitive analysis design, effects detected by local
analysis on each statement usually taint the global conclusion conservatively.
## Key for `show` output of Effects:
The output represents the state of different effect properties in the following order:
1. `consistent` (`c`):
- `+c` (green): `ALWAYS_TRUE`
- `-c` (red): `ALWAYS_FALSE`
- `?c` (yellow): `CONSISTENT_IF_NOTRETURNED` and/or `CONSISTENT_IF_INACCESSIBLEMEMONLY`
2. `effect_free` (`e`):
- `+e` (green): `ALWAYS_TRUE`
- `-e` (red): `ALWAYS_FALSE`
- `?e` (yellow): `EFFECT_FREE_IF_INACCESSIBLEMEMONLY`
3. `nothrow` (`n`):
- `+n` (green): `true`
- `-n` (red): `false`
4. `terminates` (`t`):
- `+t` (green): `true`
- `-t` (red): `false`
5. `notaskstate` (`s`):
- `+s` (green): `true`
- `-s` (red): `false`
6. `inaccessiblememonly` (`m`):
- `+m` (green): `ALWAYS_TRUE`
- `-m` (red): `ALWAYS_FALSE`
- `?m` (yellow): `INACCESSIBLEMEM_OR_ARGMEMONLY`
7. `noub` (`u`):
- `+u` (green): `true`
- `-u` (red): `false`
8. `noinbounds` (`i`):
- `+i` (green): `true`
- `-i` (red): `false`
Additionally, if the `nonoverlayed` property is false, a red prime symbol (′) is displayed after the tuple.
"""
struct Effects
consistent::UInt8
effect_free::UInt8
nothrow::Bool
terminates::Bool
notaskstate::Bool
inaccessiblememonly::UInt8
noub::UInt8
nonoverlayed::Bool
function Effects(
consistent::UInt8,
effect_free::UInt8,
nothrow::Bool,
terminates::Bool,
notaskstate::Bool,
inaccessiblememonly::UInt8,
noub::UInt8,
nonoverlayed::Bool)
return new(
consistent,
effect_free,
nothrow,
terminates,
notaskstate,
inaccessiblememonly,
noub,
nonoverlayed)
end
end
const ALWAYS_TRUE = 0x00
const ALWAYS_FALSE = 0x01
# :consistent-cy bits
const CONSISTENT_IF_NOTRETURNED = 0x01 << 1
const CONSISTENT_IF_INACCESSIBLEMEMONLY = 0x01 << 2
# :effect_free-ness bits
const EFFECT_FREE_IF_INACCESSIBLEMEMONLY = 0x02
"""
`EFFECT_FREE_GLOBALLY` means that the statement is `:effect-free` and does not have a
caller-visible effect, but may not be removed from the function itself. This may e.g.
be used for effects that last only for the scope of the current function.
"""
const EFFECT_FREE_GLOBALLY = 0x03
# :inaccessiblememonly bits
const INACCESSIBLEMEM_OR_ARGMEMONLY = 0x01 << 1
# :noub bits
const NOUB_IF_NOINBOUNDS = 0x01 << 1
const EFFECTS_TOTAL = Effects(ALWAYS_TRUE, ALWAYS_TRUE, true, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
const EFFECTS_THROWS = Effects(ALWAYS_TRUE, ALWAYS_TRUE, false, true, true, ALWAYS_TRUE, ALWAYS_TRUE, true)
const EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, true) # unknown mostly, but it's not overlayed at least (e.g. it's not a call)
const _EFFECTS_UNKNOWN = Effects(ALWAYS_FALSE, ALWAYS_FALSE, false, false, false, ALWAYS_FALSE, ALWAYS_FALSE, false) # unknown really
function Effects(effects::Effects = _EFFECTS_UNKNOWN;
consistent::UInt8 = effects.consistent,
effect_free::UInt8 = effects.effect_free,
nothrow::Bool = effects.nothrow,
terminates::Bool = effects.terminates,
notaskstate::Bool = effects.notaskstate,
inaccessiblememonly::UInt8 = effects.inaccessiblememonly,
noub::UInt8 = effects.noub,
nonoverlayed::Bool = effects.nonoverlayed)
return Effects(
consistent,
effect_free,
nothrow,
terminates,
notaskstate,
inaccessiblememonly,
noub,
nonoverlayed)
end
function is_better_effects(new::Effects, old::Effects)
any_improved = false
if new.consistent == ALWAYS_TRUE
any_improved |= old.consistent != ALWAYS_TRUE
else
if !iszero(new.consistent & CONSISTENT_IF_NOTRETURNED)
old.consistent == ALWAYS_TRUE && return false
any_improved |= iszero(old.consistent & CONSISTENT_IF_NOTRETURNED)
elseif !iszero(new.consistent & CONSISTENT_IF_INACCESSIBLEMEMONLY)
old.consistent == ALWAYS_TRUE && return false
any_improved |= iszero(old.consistent & CONSISTENT_IF_INACCESSIBLEMEMONLY)
else
return false
end
end
if new.effect_free == ALWAYS_TRUE
any_improved |= old.consistent != ALWAYS_TRUE
elseif new.effect_free == EFFECT_FREE_IF_INACCESSIBLEMEMONLY
old.effect_free == ALWAYS_TRUE && return false
any_improved |= old.effect_free != EFFECT_FREE_IF_INACCESSIBLEMEMONLY
elseif new.effect_free != old.effect_free
return false
end
if new.nothrow
any_improved |= !old.nothrow
elseif new.nothrow != old.nothrow
return false
end
if new.terminates
any_improved |= !old.terminates
elseif new.terminates != old.terminates
return false
end
if new.notaskstate
any_improved |= !old.notaskstate
elseif new.notaskstate != old.notaskstate
return false
end
if new.inaccessiblememonly == ALWAYS_TRUE
any_improved |= old.inaccessiblememonly != ALWAYS_TRUE
elseif new.inaccessiblememonly == INACCESSIBLEMEM_OR_ARGMEMONLY
old.inaccessiblememonly == ALWAYS_TRUE && return false
any_improved |= old.inaccessiblememonly != INACCESSIBLEMEM_OR_ARGMEMONLY
elseif new.inaccessiblememonly != old.inaccessiblememonly
return false
end
if new.noub == ALWAYS_TRUE
any_improved |= old.noub != ALWAYS_TRUE
elseif new.noub == NOUB_IF_NOINBOUNDS
old.noub == ALWAYS_TRUE && return false
any_improved |= old.noub != NOUB_IF_NOINBOUNDS
elseif new.noub != old.noub
return false
end
if new.nonoverlayed
any_improved |= !old.nonoverlayed
elseif new.nonoverlayed != old.nonoverlayed
return false
end
return any_improved
end
function merge_effects(old::Effects, new::Effects)
return Effects(
merge_effectbits(old.consistent, new.consistent),
merge_effectbits(old.effect_free, new.effect_free),
merge_effectbits(old.nothrow, new.nothrow),
merge_effectbits(old.terminates, new.terminates),
merge_effectbits(old.notaskstate, new.notaskstate),
merge_effectbits(old.inaccessiblememonly, new.inaccessiblememonly),
merge_effectbits(old.noub, new.noub),
merge_effectbits(old.nonoverlayed, new.nonoverlayed))
end
function merge_effectbits(old::UInt8, new::UInt8)
if old === ALWAYS_FALSE || new === ALWAYS_FALSE
return ALWAYS_FALSE
end
return old | new
end
merge_effectbits(old::Bool, new::Bool) = old & new
is_consistent(effects::Effects) = effects.consistent === ALWAYS_TRUE
is_effect_free(effects::Effects) = effects.effect_free === ALWAYS_TRUE
is_nothrow(effects::Effects) = effects.nothrow
is_terminates(effects::Effects) = effects.terminates
is_notaskstate(effects::Effects) = effects.notaskstate
is_inaccessiblememonly(effects::Effects) = effects.inaccessiblememonly === ALWAYS_TRUE
is_noub(effects::Effects) = effects.noub === ALWAYS_TRUE
is_noub_if_noinbounds(effects::Effects) = effects.noub === NOUB_IF_NOINBOUNDS
is_nonoverlayed(effects::Effects) = effects.nonoverlayed
# implies `is_notaskstate` & `is_inaccessiblememonly`, but not explicitly checked here
is_foldable(effects::Effects) =
is_consistent(effects) &&
(is_noub(effects) || is_noub_if_noinbounds(effects)) &&
is_effect_free(effects) &&
is_terminates(effects)
is_foldable_nothrow(effects::Effects) =
is_foldable(effects) &&
is_nothrow(effects)
# TODO add `is_noub` here?
is_removable_if_unused(effects::Effects) =
is_effect_free(effects) &&
is_terminates(effects) &&
is_nothrow(effects)
is_finalizer_inlineable(effects::Effects) =
is_nothrow(effects) &&
is_notaskstate(effects)
is_consistent_if_notreturned(effects::Effects) = !iszero(effects.consistent & CONSISTENT_IF_NOTRETURNED)
is_consistent_if_inaccessiblememonly(effects::Effects) = !iszero(effects.consistent & CONSISTENT_IF_INACCESSIBLEMEMONLY)
is_effect_free_if_inaccessiblememonly(effects::Effects) = !iszero(effects.effect_free & EFFECT_FREE_IF_INACCESSIBLEMEMONLY)
is_inaccessiblemem_or_argmemonly(effects::Effects) = effects.inaccessiblememonly === INACCESSIBLEMEM_OR_ARGMEMONLY
function encode_effects(e::Effects)
return ((e.consistent % UInt32) << 0) |
((e.effect_free % UInt32) << 3) |
((e.nothrow % UInt32) << 5) |
((e.terminates % UInt32) << 6) |
((e.notaskstate % UInt32) << 7) |
((e.inaccessiblememonly % UInt32) << 8) |
((e.noub % UInt32) << 10) |
((e.nonoverlayed % UInt32) << 12)
end
function decode_effects(e::UInt32)
return Effects(
UInt8((e >> 0) & 0x07),
UInt8((e >> 3) & 0x03),
_Bool((e >> 5) & 0x01),
_Bool((e >> 6) & 0x01),
_Bool((e >> 7) & 0x01),
UInt8((e >> 8) & 0x03),
UInt8((e >> 10) & 0x03),
_Bool((e >> 12) & 0x01))
end
function encode_effects_override(eo::EffectsOverride)
e = 0x0000
eo.consistent && (e |= (0x0001 << 0))
eo.effect_free && (e |= (0x0001 << 1))
eo.nothrow && (e |= (0x0001 << 2))
eo.terminates_globally && (e |= (0x0001 << 3))
eo.terminates_locally && (e |= (0x0001 << 4))
eo.notaskstate && (e |= (0x0001 << 5))
eo.inaccessiblememonly && (e |= (0x0001 << 6))
eo.noub && (e |= (0x0001 << 7))
eo.noub_if_noinbounds && (e |= (0x0001 << 8))
return e
end
function decode_effects_override(e::UInt16)
return EffectsOverride(
!iszero(e & (0x0001 << 0)),
!iszero(e & (0x0001 << 1)),
!iszero(e & (0x0001 << 2)),
!iszero(e & (0x0001 << 3)),
!iszero(e & (0x0001 << 4)),
!iszero(e & (0x0001 << 5)),
!iszero(e & (0x0001 << 6)),
!iszero(e & (0x0001 << 7)),
!iszero(e & (0x0001 << 8)))
end
decode_effects_override_from_ssaflag(flag::UInt32) =
decode_effects_override(UInt16((flag >> NUM_IR_FLAGS) & (1 << NUM_EFFECTS_OVERRIDES - 1)))