Phantom let support in Cmm (#2070)

master
Mark Shinwell 2018-10-16 07:20:56 +01:00 committed by GitHub
parent 74e3b9a215
commit 72378c0ad1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
12 changed files with 171 additions and 41 deletions

76
.depend
View File

@ -213,8 +213,10 @@ typing/envaux.cmo : typing/subst.cmi typing/printtyp.cmi typing/path.cmi \
typing/envaux.cmx : typing/subst.cmx typing/printtyp.cmx typing/path.cmx \
typing/ident.cmx typing/env.cmx typing/envaux.cmi
typing/envaux.cmi : typing/subst.cmi typing/path.cmi typing/env.cmi
typing/ident.cmo : utils/identifiable.cmi utils/clflags.cmi typing/ident.cmi
typing/ident.cmx : utils/identifiable.cmx utils/clflags.cmx typing/ident.cmi
typing/ident.cmo : utils/misc.cmi utils/identifiable.cmi utils/clflags.cmi \
typing/ident.cmi
typing/ident.cmx : utils/misc.cmx utils/identifiable.cmx utils/clflags.cmx \
typing/ident.cmi
typing/ident.cmi : utils/identifiable.cmi
typing/includeclass.cmo : typing/types.cmi typing/printtyp.cmi \
typing/path.cmi typing/ctype.cmi parsing/builtin_attributes.cmi \
@ -308,17 +310,17 @@ typing/printpat.cmi : typing/typedtree.cmi parsing/asttypes.cmi
typing/printtyp.cmo : utils/warnings.cmi typing/types.cmi \
typing/primitive.cmi typing/predef.cmi typing/path.cmi \
parsing/parsetree.cmi typing/outcometree.cmi typing/oprint.cmi \
utils/numbers.cmi utils/misc.cmi parsing/longident.cmi \
parsing/location.cmi typing/ident.cmi typing/env.cmi typing/ctype.cmi \
utils/clflags.cmi parsing/builtin_attributes.cmi typing/btype.cmi \
parsing/asttypes.cmi typing/printtyp.cmi
utils/misc.cmi parsing/longident.cmi parsing/location.cmi \
typing/ident.cmi typing/env.cmi typing/ctype.cmi utils/clflags.cmi \
parsing/builtin_attributes.cmi typing/btype.cmi parsing/asttypes.cmi \
typing/printtyp.cmi
typing/printtyp.cmx : utils/warnings.cmx typing/types.cmx \
typing/primitive.cmx typing/predef.cmx typing/path.cmx \
parsing/parsetree.cmi typing/outcometree.cmi typing/oprint.cmx \
utils/numbers.cmx utils/misc.cmx parsing/longident.cmx \
parsing/location.cmx typing/ident.cmx typing/env.cmx typing/ctype.cmx \
utils/clflags.cmx parsing/builtin_attributes.cmx typing/btype.cmx \
parsing/asttypes.cmi typing/printtyp.cmi
utils/misc.cmx parsing/longident.cmx parsing/location.cmx \
typing/ident.cmx typing/env.cmx typing/ctype.cmx utils/clflags.cmx \
parsing/builtin_attributes.cmx typing/btype.cmx parsing/asttypes.cmi \
typing/printtyp.cmi
typing/printtyp.cmi : typing/types.cmi typing/path.cmi \
typing/outcometree.cmi parsing/longident.cmi parsing/location.cmi \
typing/ident.cmi typing/env.cmi parsing/asttypes.cmi
@ -836,10 +838,10 @@ asmcomp/asmpackager.cmx : typing/typemod.cmx bytecomp/translmod.cmx \
utils/clflags.cmx utils/ccomp.cmx asmcomp/asmlink.cmx asmcomp/asmgen.cmx \
asmcomp/asmpackager.cmi
asmcomp/asmpackager.cmi : typing/env.cmi middle_end/backend_intf.cmi
asmcomp/backend_var.cmo : typing/printtyp.cmi typing/path.cmi \
typing/ident.cmi middle_end/debuginfo.cmi asmcomp/backend_var.cmi
asmcomp/backend_var.cmx : typing/printtyp.cmx typing/path.cmx \
typing/ident.cmx middle_end/debuginfo.cmx asmcomp/backend_var.cmi
asmcomp/backend_var.cmo : typing/path.cmi typing/ident.cmi \
middle_end/debuginfo.cmi asmcomp/backend_var.cmi
asmcomp/backend_var.cmx : typing/path.cmx typing/ident.cmx \
middle_end/debuginfo.cmx asmcomp/backend_var.cmi
asmcomp/backend_var.cmi : typing/path.cmi typing/ident.cmi \
middle_end/debuginfo.cmi
asmcomp/branch_relaxation.cmo : utils/misc.cmi asmcomp/mach.cmi \
@ -891,14 +893,14 @@ asmcomp/clambda.cmi : bytecomp/lambda.cmi middle_end/debuginfo.cmi \
asmcomp/closure.cmo : utils/warnings.cmi bytecomp/switch.cmi \
bytecomp/simplif.cmi bytecomp/semantics_of_primitives.cmi \
typing/primitive.cmi utils/numbers.cmi utils/misc.cmi \
parsing/location.cmi bytecomp/lambda.cmi typing/env.cmi \
parsing/location.cmi bytecomp/lambda.cmi typing/ident.cmi typing/env.cmi \
middle_end/debuginfo.cmi utils/config.cmi asmcomp/compilenv.cmi \
utils/clflags.cmi asmcomp/clambda.cmi asmcomp/backend_var.cmi \
parsing/asttypes.cmi asmcomp/arch.cmo asmcomp/closure.cmi
asmcomp/closure.cmx : utils/warnings.cmx bytecomp/switch.cmx \
bytecomp/simplif.cmx bytecomp/semantics_of_primitives.cmx \
typing/primitive.cmx utils/numbers.cmx utils/misc.cmx \
parsing/location.cmx bytecomp/lambda.cmx typing/env.cmx \
parsing/location.cmx bytecomp/lambda.cmx typing/ident.cmx typing/env.cmx \
middle_end/debuginfo.cmx utils/config.cmx asmcomp/compilenv.cmx \
utils/clflags.cmx asmcomp/clambda.cmx asmcomp/backend_var.cmx \
parsing/asttypes.cmi asmcomp/arch.cmx asmcomp/closure.cmi
@ -914,13 +916,13 @@ asmcomp/closure_offsets.cmx : middle_end/base_types/variable.cmx \
asmcomp/closure_offsets.cmi : middle_end/base_types/var_within_closure.cmi \
middle_end/flambda.cmi middle_end/base_types/closure_id.cmi
asmcomp/cmm.cmo : bytecomp/lambda.cmi middle_end/debuginfo.cmi \
asmcomp/backend_var.cmi parsing/asttypes.cmi asmcomp/arch.cmo \
asmcomp/cmm.cmi
asmcomp/clambda.cmi asmcomp/backend_var.cmi parsing/asttypes.cmi \
asmcomp/arch.cmo asmcomp/cmm.cmi
asmcomp/cmm.cmx : bytecomp/lambda.cmx middle_end/debuginfo.cmx \
asmcomp/backend_var.cmx parsing/asttypes.cmi asmcomp/arch.cmx \
asmcomp/cmm.cmi
asmcomp/clambda.cmx asmcomp/backend_var.cmx parsing/asttypes.cmi \
asmcomp/arch.cmx asmcomp/cmm.cmi
asmcomp/cmm.cmi : bytecomp/lambda.cmi middle_end/debuginfo.cmi \
asmcomp/backend_var.cmi parsing/asttypes.cmi
asmcomp/clambda.cmi asmcomp/backend_var.cmi parsing/asttypes.cmi
asmcomp/cmmgen.cmo : asmcomp/un_anf.cmi typing/types.cmi bytecomp/switch.cmi \
asmcomp/strmatch.cmi asmcomp/proc.cmi bytecomp/printlambda.cmi \
typing/primitive.cmi utils/numbers.cmi utils/misc.cmi bytecomp/lambda.cmi \
@ -1130,18 +1132,18 @@ asmcomp/mach.cmi : asmcomp/debug/reg_availability_set.cmi asmcomp/reg.cmi \
middle_end/debuginfo.cmi asmcomp/cmm.cmi asmcomp/backend_var.cmi \
asmcomp/arch.cmo
asmcomp/printclambda.cmo : bytecomp/printlambda.cmi bytecomp/lambda.cmi \
asmcomp/clambda.cmi asmcomp/backend_var.cmi parsing/asttypes.cmi \
asmcomp/printclambda.cmi
typing/ident.cmi asmcomp/clambda.cmi asmcomp/backend_var.cmi \
parsing/asttypes.cmi asmcomp/printclambda.cmi
asmcomp/printclambda.cmx : bytecomp/printlambda.cmx bytecomp/lambda.cmx \
asmcomp/clambda.cmx asmcomp/backend_var.cmx parsing/asttypes.cmi \
asmcomp/printclambda.cmi
typing/ident.cmx asmcomp/clambda.cmx asmcomp/backend_var.cmx \
parsing/asttypes.cmi asmcomp/printclambda.cmi
asmcomp/printclambda.cmi : asmcomp/clambda.cmi
asmcomp/printcmm.cmo : bytecomp/lambda.cmi middle_end/debuginfo.cmi \
asmcomp/cmm.cmi asmcomp/backend_var.cmi parsing/asttypes.cmi \
asmcomp/printcmm.cmi
asmcomp/printcmm.cmx : bytecomp/lambda.cmx middle_end/debuginfo.cmx \
asmcomp/cmm.cmx asmcomp/backend_var.cmx parsing/asttypes.cmi \
asmcomp/printcmm.cmi
asmcomp/printcmm.cmo : asmcomp/printclambda.cmi bytecomp/lambda.cmi \
middle_end/debuginfo.cmi asmcomp/cmm.cmi asmcomp/backend_var.cmi \
parsing/asttypes.cmi asmcomp/printcmm.cmi
asmcomp/printcmm.cmx : asmcomp/printclambda.cmx bytecomp/lambda.cmx \
middle_end/debuginfo.cmx asmcomp/cmm.cmx asmcomp/backend_var.cmx \
parsing/asttypes.cmi asmcomp/printcmm.cmi
asmcomp/printcmm.cmi : middle_end/debuginfo.cmi asmcomp/cmm.cmi
asmcomp/printlinear.cmo : asmcomp/printmach.cmi asmcomp/printcmm.cmi \
asmcomp/mach.cmi asmcomp/linearize.cmi middle_end/debuginfo.cmi \
@ -2460,14 +2462,14 @@ toplevel/genprintval.cmi : typing/types.cmi typing/path.cmi \
typing/outcometree.cmi typing/env.cmi
toplevel/opttopdirs.cmo : utils/warnings.cmi typing/types.cmi \
typing/printtyp.cmi toplevel/opttoploop.cmi utils/misc.cmi \
parsing/longident.cmi typing/ident.cmi typing/env.cmi typing/ctype.cmi \
utils/config.cmi driver/compdynlink.cmi utils/clflags.cmi \
asmcomp/asmlink.cmi toplevel/opttopdirs.cmi
parsing/longident.cmi typing/env.cmi typing/ctype.cmi utils/config.cmi \
driver/compdynlink.cmi utils/clflags.cmi asmcomp/asmlink.cmi \
toplevel/opttopdirs.cmi
toplevel/opttopdirs.cmx : utils/warnings.cmx typing/types.cmx \
typing/printtyp.cmx toplevel/opttoploop.cmx utils/misc.cmx \
parsing/longident.cmx typing/ident.cmx typing/env.cmx typing/ctype.cmx \
utils/config.cmx driver/compdynlink.cmi utils/clflags.cmx \
asmcomp/asmlink.cmx toplevel/opttopdirs.cmi
parsing/longident.cmx typing/env.cmx typing/ctype.cmx utils/config.cmx \
driver/compdynlink.cmi utils/clflags.cmx asmcomp/asmlink.cmx \
toplevel/opttopdirs.cmi
toplevel/opttopdirs.cmi : parsing/longident.cmi
toplevel/opttoploop.cmo : utils/warnings.cmi typing/types.cmi \
typing/typemod.cmi typing/typedtree.cmi typing/typecore.cmi \

View File

@ -437,6 +437,12 @@ Working version
- GPR#2065: Add [Proc.destroyed_at_reloadretaddr].
(Mark Shinwell, review by Damien Doligez)
- GPR#2060: "Phantom let" support for the Clambda language.
(Mark Shinwell, review by Vincent Laviron)
- GPR#2070: "Phantom let" support for the Cmm language.
(Mark Shinwell, review by Vincent Laviron)
- GPR#2072: Always associate a scope to a type
(Thomas Refis, review by Jacques Garrigue and Leo White)

View File

@ -68,6 +68,8 @@ and instrument = function
(* these cases add no logging, but instrument subexpressions *)
| Clet (v, e, body) -> Clet (v, instrument e, instrument body)
| Cphantom_let (v, defining_expr, body) ->
Cphantom_let (v, defining_expr, instrument body)
| Cassign (v, e) -> Cassign (v, instrument e)
| Ctuple es -> Ctuple (List.map instrument es)
| Cop (op, es, dbg) -> Cop (op, List.map instrument es, dbg)

View File

@ -41,7 +41,7 @@ and uphantom_defining_expr =
| Uphantom_var of Backend_var.t
| Uphantom_offset_var of { var : Backend_var.t; offset_in_words : int; }
| Uphantom_read_field of { var : Backend_var.t; field : int; }
| Uphantom_read_symbol_field of { sym : uconstant; field : int; }
| Uphantom_read_symbol_field of { sym : string; field : int; }
| Uphantom_block of { tag : int; fields : Backend_var.t list; }
and ulambda =

View File

@ -48,7 +48,7 @@ and uphantom_defining_expr =
(** The phantom-let-bound-variable's value is found by adding the given
number of words to the pointer contained in the given identifier, then
dereferencing. *)
| Uphantom_read_symbol_field of { sym : uconstant; field : int; }
| Uphantom_read_symbol_field of { sym : string; field : int; }
(** As for [Uphantom_read_var_field], but with the pointer specified by
a symbol. *)
| Uphantom_block of { tag : int; fields : Backend_var.t list; }

View File

@ -116,6 +116,15 @@ type raise_kind =
type rec_flag = Nonrecursive | Recursive
type phantom_defining_expr =
| Cphantom_const_int of Targetint.t
| Cphantom_const_symbol of string
| Cphantom_var of Backend_var.t
| Cphantom_offset_var of { var : Backend_var.t; offset_in_words : int; }
| Cphantom_read_field of { var : Backend_var.t; field : int; }
| Cphantom_read_symbol_field of { sym : string; field : int; }
| Cphantom_block of { tag : int; fields : Backend_var.t list; }
type memory_chunk =
Byte_unsigned
| Byte_signed
@ -159,6 +168,8 @@ type expression =
| Cblockheader of nativeint * Debuginfo.t
| Cvar of Backend_var.t
| Clet of Backend_var.With_provenance.t * expression * expression
| Cphantom_let of Backend_var.With_provenance.t
* phantom_defining_expr option * expression
| Cassign of Backend_var.t * expression
| Ctuple of expression list
| Cop of operation * expression list * Debuginfo.t

View File

@ -93,6 +93,33 @@ type raise_kind =
type rec_flag = Nonrecursive | Recursive
type phantom_defining_expr =
(* CR-soon mshinwell: Convert this to [Targetint.OCaml.t] (or whatever the
representation of "target-width OCaml integers of type [int]"
becomes when merged). *)
| Cphantom_const_int of Targetint.t
(** The phantom-let-bound variable is a constant integer.
The argument must be the tagged representation of an integer within
the range of type [int] on the target. (Analogously to [Cconst_int].) *)
| Cphantom_const_symbol of string
(** The phantom-let-bound variable is an alias for a symbol. *)
| Cphantom_var of Backend_var.t
(** The phantom-let-bound variable is an alias for another variable. The
aliased variable must not be a bound by a phantom let. *)
| Cphantom_offset_var of { var : Backend_var.t; offset_in_words : int; }
(** The phantom-let-bound-variable's value is defined by adding the given
number of words to the pointer contained in the given identifier. *)
| Cphantom_read_field of { var : Backend_var.t; field : int; }
(** The phantom-let-bound-variable's value is found by adding the given
number of words to the pointer contained in the given identifier, then
dereferencing. *)
| Cphantom_read_symbol_field of { sym : string; field : int; }
(** As for [Uphantom_read_var_field], but with the pointer specified by
a symbol. *)
| Cphantom_block of { tag : int; fields : Backend_var.t list; }
(** The phantom-let-bound variable points at a block with the given
structure. *)
type memory_chunk =
Byte_unsigned
| Byte_signed
@ -139,6 +166,8 @@ and expression =
| Cblockheader of nativeint * Debuginfo.t
| Cvar of Backend_var.t
| Clet of Backend_var.With_provenance.t * expression * expression
| Cphantom_let of Backend_var.With_provenance.t
* phantom_defining_expr option * expression
| Cassign of Backend_var.t * expression
| Ctuple of expression list
| Cop of operation * expression list * Debuginfo.t

View File

@ -133,6 +133,10 @@ let int_const n =
let cint_const n =
Cint(Nativeint.add (Nativeint.shift_left (Nativeint.of_int n) 1) 1n)
let targetint_const n =
Targetint.add (Targetint.shift_left (Targetint.of_int n) 1)
Targetint.one
let add_no_overflow n x c dbg =
let d = n + x in
if d = 0 then c else Cop(Caddi, [c; Cconst_int d], dbg)
@ -1789,7 +1793,30 @@ let rec transl env e =
(call_met obj args))
| Ulet(str, kind, id, exp, body) ->
transl_let env str kind id exp body
| Uphantom_let (_var, _defining_expr, body) -> transl env body
| Uphantom_let (var, defining_expr, body) ->
let defining_expr =
match defining_expr with
| None -> None
| Some defining_expr ->
let defining_expr =
match defining_expr with
| Uphantom_const (Uconst_ref (sym, _defining_expr)) ->
Cphantom_const_symbol sym
| Uphantom_read_symbol_field { sym; field; } ->
Cphantom_read_symbol_field { sym; field; }
| Uphantom_const (Uconst_int i) | Uphantom_const (Uconst_ptr i) ->
Cphantom_const_int (targetint_const i)
| Uphantom_var var -> Cphantom_var var
| Uphantom_read_field { var; field; } ->
Cphantom_read_field { var; field; }
| Uphantom_offset_var { var; offset_in_words; } ->
Cphantom_offset_var { var; offset_in_words; }
| Uphantom_block { tag; fields; } ->
Cphantom_block { tag; fields; }
in
Some defining_expr
in
Cphantom_let (var, defining_expr, transl env body)
| Uletrec(bindings, body) ->
transl_letrec env bindings (transl env body)

View File

@ -71,7 +71,7 @@ and phantom_defining_expr ppf = function
| Uphantom_read_field { var; field; } ->
Format.fprintf ppf "%a[%d]" Backend_var.print var field
| Uphantom_read_symbol_field { sym; field; } ->
Format.fprintf ppf "%a[%d]" uconstant sym field
Format.fprintf ppf "%s[%d]" sym field
| Uphantom_block { tag; fields; } ->
Format.fprintf ppf "[%d: " tag;
List.iter (fun field ->

View File

@ -19,3 +19,8 @@ open Format
val clambda: formatter -> ulambda -> unit
val approx: formatter -> value_approximation -> unit
val structured_constant: formatter -> ustructured_constant -> unit
val phantom_defining_expr_opt
: formatter
-> uphantom_defining_expr option
-> unit

View File

@ -76,6 +76,29 @@ let raise_kind fmt = function
| Raise_withtrace -> Format.fprintf fmt "raise_withtrace"
| Raise_notrace -> Format.fprintf fmt "raise_notrace"
let phantom_defining_expr ppf defining_expr =
match defining_expr with
| Cphantom_const_int i -> Targetint.print ppf i
| Cphantom_const_symbol sym -> Format.pp_print_string ppf sym
| Cphantom_var var -> V.print ppf var
| Cphantom_offset_var { var; offset_in_words; } ->
Format.fprintf ppf "%a+(%d)" V.print var offset_in_words
| Cphantom_read_field { var; field; } ->
Format.fprintf ppf "%a[%d]" V.print var field
| Cphantom_read_symbol_field { sym; field; } ->
Format.fprintf ppf "%s[%d]" sym field
| Cphantom_block { tag; fields; } ->
Format.fprintf ppf "[%d: " tag;
List.iter (fun field ->
Format.fprintf ppf "%a; " V.print field)
fields;
Format.fprintf ppf "]"
let phantom_defining_expr_opt ppf defining_expr =
match defining_expr with
| None -> Format.pp_print_string ppf "()"
| Some defining_expr -> phantom_defining_expr ppf defining_expr
let operation d = function
| Capply _ty -> "app" ^ Debuginfo.to_string d
| Cextcall(lbl, _ty, _alloc, _) ->
@ -147,6 +170,25 @@ let rec expr ppf = function
fprintf ppf
"@[<2>(let@ @[<2>%a@ %a@]@ %a)@]"
VP.print id expr def sequence body
| Cphantom_let(var, def, (Cphantom_let(_, _, _) as body)) ->
let print_binding var ppf def =
fprintf ppf "@[<2>%a@ %a@]" VP.print var
phantom_defining_expr_opt def
in
let rec in_part ppf = function
| Cphantom_let(var, def, body) ->
fprintf ppf "@ %a" (print_binding var) def;
in_part ppf body
| exp -> exp in
fprintf ppf "@[<2>(let?@ @[<1>(%a" (print_binding var) def;
let exp = in_part ppf body in
fprintf ppf ")@]@ %a)@]" sequence exp
| Cphantom_let(var, def, body) ->
fprintf ppf
"@[<2>(let?@ @[<2>%a@ %a@]@ %a)@]"
VP.print var
phantom_defining_expr_opt def
sequence body
| Cassign(id, exp) ->
fprintf ppf "@[<2>(assign @[<2>%a@ %a@])@]" V.print id expr exp
| Ctuple el ->

View File

@ -298,6 +298,7 @@ method is_simple_expr = function
| Cvar _ -> true
| Ctuple el -> List.for_all self#is_simple_expr el
| Clet(_id, arg, body) -> self#is_simple_expr arg && self#is_simple_expr body
| Cphantom_let(_var, _defining_expr, body) -> self#is_simple_expr body
| Csequence(e1, e2) -> self#is_simple_expr e1 && self#is_simple_expr e2
| Cop(op, args, _) ->
begin match op with
@ -333,6 +334,7 @@ method effects_of exp =
| Ctuple el -> EC.join_list_map el self#effects_of
| Clet (_id, arg, body) ->
EC.join (self#effects_of arg) (self#effects_of body)
| Cphantom_let (_var, _defining_expr, body) -> self#effects_of body
| Csequence (e1, e2) ->
EC.join (self#effects_of e1) (self#effects_of e2)
| Cifthenelse (cond, ifso, ifnot) ->
@ -670,6 +672,8 @@ method emit_expr (env:environment) exp =
None -> None
| Some r1 -> self#emit_expr (self#bind_let env v r1) e2
end
| Cphantom_let (_var, _defining_expr, body) ->
self#emit_expr env body
| Cassign(v, e1) ->
let rv =
try
@ -1037,6 +1041,8 @@ method emit_tail (env:environment) exp =
None -> ()
| Some r1 -> self#emit_tail (self#bind_let env v r1) e2
end
| Cphantom_let (_var, _defining_expr, body) ->
self#emit_tail env body
| Cop((Capply ty) as op, args, dbg) ->
begin match self#emit_parts_list env args with
None -> ()