forked from ocaml/ocaml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
simple_value_approx.mli
501 lines (418 loc) · 18.7 KB
/
simple_value_approx.mli
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
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Pierre Chambart, OCamlPro *)
(* Mark Shinwell and Leo White, Jane Street Europe *)
(* *)
(* Copyright 2013--2016 OCamlPro SAS *)
(* Copyright 2014--2016 Jane Street Group LLC *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
[@@@ocaml.warning "+a-4-9-30-40-41-42"]
(** Simple approximations to the runtime results of computations.
This pass is designed for speed rather than accuracy; the performance
is important since it is used heavily during inlining. *)
type 'a boxed_int =
| Int32 : int32 boxed_int
| Int64 : int64 boxed_int
| Nativeint : nativeint boxed_int
type value_string = {
contents : string option; (* [None] if unknown or mutable *)
size : int;
}
type unresolved_value =
| Set_of_closures_id of Set_of_closures_id.t
| Symbol of Symbol.t
type unknown_because_of =
| Unresolved_value of unresolved_value
| Other
(** A value of type [t] corresponds to an "approximation" of the result of
a computation in the program being compiled. That is to say, it
represents what knowledge we have about such a result at compile time.
The simplification pass exploits this information to partially evaluate
computations.
At a high level, an approximation for a value [v] has three parts:
- the "description" (for example, "the constant integer 42");
- an optional variable;
- an optional symbol or symbol field.
If the variable (resp. symbol) is present then that variable (resp.
symbol) may be used to obtain the value [v].
The exact semantics of the variable and symbol fields follows.
Approximations are deduced at particular points in an expression tree,
but may subsequently be propagated to other locations.
At the point at which an approximation is built for some value [v], we can
construct a set of variables (call the set [S]) that are known to alias the
same value [v]. Each member of [S] will have the same or a more precise
[descr] field in its approximation relative to the approximation for [v].
(An increase in precision may currently be introduced for pattern
matches.) If [S] is non-empty then it is guaranteed that there is a
unique member of [S] that was declared in a scope further out ("earlier")
than all other members of [S]. If such a member exists then it is
recorded in the [var] field. Otherwise [var] is [None].
Analogous to the construction of the set [S], we can construct a set [T]
consisting of all symbols that are known to alias the value whose
approximation is being constructed. If [T] is non-empty then the
[symbol] field is set to some member of [T]; it does not matter which
one. (There is no notion of scope for symbols.)
Note about mutable blocks:
Mutable blocks are always represented by [Value_unknown] or
[Value_bottom]. Any other approximation could leave the door open to
a miscompilation. Such bad scenarios are most likely a user using
[Obj.magic] or [Obj.set_field] in an inappropriate situation.
Such a situation might be:
[let x = (1, 1) in
Obj.set_field (Obj.repr x) 0 (Obj.repr 2);
assert(fst x = 2)]
The user would probably expect the assertion to be true, but the
compiler could in fact propagate the value of [x] across the
[Obj.set_field].
Insisting that mutable blocks have [Value_unknown] or [Value_bottom]
approximations certainly won't always prevent this kind of error, but
should help catch many of them.
It is possible that there may be some false positives, with correct
but unreachable code causing this check to fail. However the likelihood
of this seems sufficiently low, especially compared to the advantages
gained by performing the check, that we include it.
An example of a pattern that might trigger a false positive is:
[type a = { a : int }
type b = { mutable b : int }
type _ t =
| A : a t
| B : b t
let f (type x) (v:x t) (r:x) =
match v with
| A -> r.a
| B -> r.b <- 2; 3
let v =
let r =
ref A in
r := A; (* Some pattern that the compiler can't understand *)
f !r { a = 1 }]
When inlining [f], the B branch is unreachable, yet the compiler
cannot prove it and must therefore keep it.
*)
type t = private {
descr : descr;
var : Variable.t option;
symbol : (Symbol.t * int option) option;
}
and descr = private
| Value_block of Tag.t * t array
| Value_int of int
| Value_char of char
| Value_constptr of int
| Value_float of float option
| Value_boxed_int : 'a boxed_int * 'a -> descr
| Value_set_of_closures of value_set_of_closures
| Value_closure of value_closure
| Value_string of value_string
| Value_float_array of value_float_array
| Value_unknown of unknown_because_of
| Value_bottom
| Value_extern of Export_id.t
| Value_symbol of Symbol.t
| Value_unresolved of unresolved_value
(* No description was found for this value *)
and value_closure = {
set_of_closures : t;
closure_id : Closure_id.t;
}
and function_declarations = private {
is_classic_mode: bool;
set_of_closures_id : Set_of_closures_id.t;
set_of_closures_origin : Set_of_closures_origin.t;
funs : function_declaration Variable.Map.t;
}
and function_body = private {
free_variables : Variable.Set.t;
free_symbols : Symbol.Set.t;
stub : bool;
dbg : Debuginfo.t;
inline : Lambda.inline_attribute;
specialise : Lambda.specialise_attribute;
is_a_functor : bool;
body : Flambda.t;
}
and function_declaration = private {
closure_origin : Closure_origin.t;
params : Parameter.t list;
function_body : function_body option;
}
(* CR-soon mshinwell: add support for the approximations of the results, so we
can do all of the tricky higher-order cases. *)
(* when [is_classic_mode] is [false], functions in [function_declarations]
are guaranteed to have function bodies (ie:
[function_declaration.function_body] will be of the [Some] variant).
When it [is_classic_mode] is [true], however, no guarantees about the
function_bodies are given.
*)
and value_set_of_closures = private {
function_decls : function_declarations;
bound_vars : t Var_within_closure.Map.t;
free_vars : Flambda.specialised_to Variable.Map.t;
invariant_params : Variable.Set.t Variable.Map.t Lazy.t;
recursive : Variable.Set.t Lazy.t;
size : int option Variable.Map.t Lazy.t;
(** For functions that are very likely to be inlined, the size of the
function's body. *)
specialised_args : Flambda.specialised_to Variable.Map.t;
(* Any freshening that has been applied to [function_decls]. *)
freshening : Freshening.Project_var.t;
direct_call_surrogates : Closure_id.t Closure_id.Map.t;
}
and value_float_array_contents =
| Contents of t array
| Unknown_or_mutable
and value_float_array = {
contents : value_float_array_contents;
size : int;
}
(** Extraction of the description of approximation(s). *)
val descr : t -> descr
val descrs : t list -> descr list
(** Pretty-printing of approximations to a formatter. *)
val print : Format.formatter -> t -> unit
val print_descr : Format.formatter -> descr -> unit
val print_value_set_of_closures
: Format.formatter
-> value_set_of_closures
-> unit
val print_function_declarations
: Format.formatter
-> function_declarations
-> unit
val function_declarations_approx
: keep_body:(Variable.t -> Flambda.function_declaration -> bool)
-> Flambda.function_declarations
-> function_declarations
val create_value_set_of_closures
: function_decls:function_declarations
-> bound_vars:t Var_within_closure.Map.t
-> free_vars:Flambda.specialised_to Variable.Map.t
-> invariant_params:Variable.Set.t Variable.Map.t lazy_t
-> recursive:Variable.Set.t Lazy.t
-> specialised_args:Flambda.specialised_to Variable.Map.t
-> freshening:Freshening.Project_var.t
-> direct_call_surrogates:Closure_id.t Closure_id.Map.t
-> value_set_of_closures
val update_freshening_of_value_set_of_closures
: value_set_of_closures
-> freshening:Freshening.Project_var.t
-> value_set_of_closures
(** Basic construction of approximations. *)
val value_unknown : unknown_because_of -> t
val value_int : int -> t
val value_char : char -> t
val value_float : float -> t
val value_any_float : t
val value_mutable_float_array : size:int -> t
val value_immutable_float_array : t array -> t
val value_string : int -> string option -> t
val value_boxed_int : 'i boxed_int -> 'i -> t
val value_constptr : int -> t
val value_block : Tag.t -> t array -> t
val value_extern : Export_id.t -> t
val value_symbol : Symbol.t -> t
val value_bottom : t
val value_unresolved : unresolved_value -> t
(** Construct a closure approximation given the approximation of the
corresponding set of closures and the closure ID of the closure to
be projected from such set. [closure_var] and/or [set_of_closures_var]
may be specified to augment the approximation with variables that may
be used to access the closure value itself, so long as they are in
scope at the proposed point of use. *)
val value_closure
: ?closure_var:Variable.t
-> ?set_of_closures_var:Variable.t
-> ?set_of_closures_symbol:Symbol.t
-> value_set_of_closures
-> Closure_id.t
-> t
(** Construct a set of closures approximation. [set_of_closures_var] is as for
the parameter of the same name in [value_closure], above. *)
val value_set_of_closures
: ?set_of_closures_var:Variable.t
-> value_set_of_closures
-> t
(** Take the given constant and produce an appropriate approximation for it
together with an Flambda expression representing it. *)
val make_const_int : int -> Flambda.t * t
val make_const_char : char -> Flambda.t * t
val make_const_ptr : int -> Flambda.t * t
val make_const_bool : bool -> Flambda.t * t
val make_const_float : float -> Flambda.t * t
val make_const_boxed_int : 'i boxed_int -> 'i -> Flambda.t * t
val make_const_int_named : int -> Flambda.named * t
val make_const_char_named : char -> Flambda.named * t
val make_const_ptr_named : int -> Flambda.named * t
val make_const_bool_named : bool -> Flambda.named * t
val make_const_float_named : float -> Flambda.named * t
val make_const_boxed_int_named : 'i boxed_int -> 'i -> Flambda.named * t
(** Augment an approximation with a given variable (see comment above).
If the approximation was already augmented with a variable, the one
passed to this function replaces it within the approximation. *)
val augment_with_variable : t -> Variable.t -> t
(** Like [augment_with_variable], but for symbol information. *)
val augment_with_symbol : t -> Symbol.t -> t
(** Like [augment_with_symbol], but for symbol field information. *)
val augment_with_symbol_field : t -> Symbol.t -> int -> t
(** Replace the description within an approximation. *)
val replace_description : t -> descr -> t
(** Improve the description by taking the kind into account *)
val augment_with_kind : t -> Lambda.value_kind -> t
(** Improve the kind by taking the description into account *)
val augment_kind_with_approx : t -> Lambda.value_kind -> Lambda.value_kind
val equal_boxed_int : 'a boxed_int -> 'a -> 'b boxed_int -> 'b -> bool
(* CR-soon mshinwell for pchambart: Add comment describing semantics. (Maybe
we should move the comment from the .ml file into here.) *)
val meet : really_import_approx:(t -> t) -> t -> t -> t
(** An approximation is "known" iff it is not [Value_unknown]. *)
val known : t -> bool
(** An approximation is "useful" iff it is neither unknown nor bottom. *)
val useful : t -> bool
(** Whether all approximations in the given list do *not* satisfy [useful]. *)
val all_not_useful : t list -> bool
(** Whether to warn on attempts to mutate a value.
It must have been resolved (it cannot be [Value_extern] or
[Value_symbol]). (See comment above for further explanation.) *)
val warn_on_mutation : t -> bool
type simplification_summary =
| Nothing_done
| Replaced_term
type simplification_result = Flambda.t * simplification_summary * t
type simplification_result_named = Flambda.named * simplification_summary * t
(** Given an expression and its approximation, attempt to simplify the
expression to a constant (with associated approximation), taking into
account whether the expression has any side effects. *)
val simplify : t -> Flambda.t -> simplification_result
(** As for [simplify], but also enables us to simplify based on equalities
between variables. The caller must provide a function that tells us
whether, if we simplify to a given variable, the value of that variable
will be accessible in the current environment. *)
val simplify_using_env
: t
-> is_present_in_env:(Variable.t -> bool)
-> Flambda.t
-> simplification_result
val simplify_named : t -> Flambda.named -> simplification_result_named
val simplify_named_using_env
: t
-> is_present_in_env:(Variable.t -> bool)
-> Flambda.named
-> simplification_result_named
(** If the given approximation identifies another variable and
[is_present_in_env] deems it to be in scope, return that variable (wrapped
in a [Some]), otherwise return [None]. *)
val simplify_var_to_var_using_env
: t
-> is_present_in_env:(Variable.t -> bool)
-> Variable.t option
val simplify_var : t -> (Flambda.named * t) option
type get_field_result =
| Ok of t
| Unreachable
(** Given the approximation [t] of a value, expected to correspond to a block
(in the [Pmakeblock] sense of the word), and a field index then return
an appropriate approximation for that field of the block (or
[Unreachable] if the code with the approximation [t] is unreachable).
N.B. Not all cases of unreachable code are returned as [Unreachable].
*)
val get_field : t -> field_index:int -> get_field_result
type checked_approx_for_block =
| Wrong
| Ok of Tag.t * t array
(** Try to prove that a value with the given approximation may be used
as a block. *)
val check_approx_for_block : t -> checked_approx_for_block
(** Find the approximation for a bound variable in a set-of-closures
approximation. A fatal error is produced if the variable is not bound in
the given approximation. *)
val approx_for_bound_var : value_set_of_closures -> Var_within_closure.t -> t
(** Given a set-of-closures approximation and a closure ID, apply any
freshening specified by the approximation to the closure ID, and return
the resulting ID. Causes a fatal error if the resulting closure ID does
not correspond to any function declaration in the approximation. *)
val freshen_and_check_closure_id
: value_set_of_closures
-> Closure_id.t
-> Closure_id.t
type strict_checked_approx_for_set_of_closures =
| Wrong
| Ok of Variable.t option * value_set_of_closures
val strict_check_approx_for_set_of_closures
: t
-> strict_checked_approx_for_set_of_closures
type checked_approx_for_set_of_closures =
| Wrong
| Unresolved of unresolved_value
| Unknown
| Unknown_because_of_unresolved_value of unresolved_value
(* In the [Ok] case, there may not be a variable associated with the set of
closures; it might be out of scope. *)
| Ok of Variable.t option * value_set_of_closures
(** Try to prove that a value with the given approximation may be used as a
set of closures. Values coming from external compilation units with
unresolved approximations are permitted. *)
val check_approx_for_set_of_closures : t -> checked_approx_for_set_of_closures
type checked_approx_for_closure =
| Wrong
| Ok of value_closure * Variable.t option
* Symbol.t option * value_set_of_closures
(** Try to prove that a value with the given approximation may be used as a
closure. Values coming from external compilation units with unresolved
approximations are not permitted. *)
(* CR-someday mshinwell: naming is inconsistent: this is as "strict"
as "strict_check_approx_for_set_of_closures" *)
val check_approx_for_closure : t -> checked_approx_for_closure
type checked_approx_for_closure_allowing_unresolved =
| Wrong
| Unresolved of unresolved_value
| Unknown
| Unknown_because_of_unresolved_value of unresolved_value
| Ok of value_closure * Variable.t option
* Symbol.t option * value_set_of_closures
(** As for [check_approx_for_closure], but values coming from external
compilation units with unresolved approximations are permitted. *)
val check_approx_for_closure_allowing_unresolved
: t
-> checked_approx_for_closure_allowing_unresolved
(** Returns the value if it can be proved to be a constant float *)
val check_approx_for_float : t -> float option
(** Returns the value if it can be proved to be a constant float array *)
val float_array_as_constant : value_float_array -> float list option
(** Returns the value if it can be proved to be a constant string *)
val check_approx_for_string : t -> string option
type switch_branch_selection =
| Cannot_be_taken
| Can_be_taken
| Must_be_taken
(** Check that the branch is compatible with the approximation *)
val potentially_taken_const_switch_branch : t -> int -> switch_branch_selection
val potentially_taken_block_switch_branch : t -> int -> switch_branch_selection
val function_arity : function_declaration -> int
(** Create a set of function declarations based on another set of function
declarations. *)
val update_function_declarations
: function_declarations
-> funs:function_declaration Variable.Map.t
-> function_declarations
val import_function_declarations_for_pack
: function_declarations
-> (Set_of_closures_id.t -> Set_of_closures_id.t)
-> (Set_of_closures_origin.t -> Set_of_closures_origin.t)
-> function_declarations
val update_function_declaration_body
: function_declaration
-> (Flambda.t -> Flambda.t)
-> function_declaration
(** Creates a map from closure IDs to function declarations by iterating over
all sets of closures in the given map. *)
val make_closure_map
: function_declarations Set_of_closures_id.Map.t
-> function_declarations Closure_id.Map.t
val clear_function_bodies : function_declarations -> function_declarations