Skip to content

Commit 7e3e0c8

Browse files
authored
flambda-backend: Fix inclusion checks for primitives (#661)
1 parent 96c68f9 commit 7e3e0c8

File tree

15 files changed

+176
-52
lines changed

15 files changed

+176
-52
lines changed

lambda/translcore.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -298,7 +298,7 @@ let rec iter_exn_names f pat =
298298
let transl_ident loc env ty path desc kind =
299299
match desc.val_kind, kind with
300300
| Val_prim p, Id_prim pmode ->
301-
let poly_mode = transl_alloc_mode pmode in
301+
let poly_mode = Option.map transl_alloc_mode pmode in
302302
Translprim.transl_primitive loc p env ty ~poly_mode (Some path)
303303
| Val_anc _, Id_value ->
304304
raise(Error(to_location loc, Free_super_var))
@@ -373,7 +373,7 @@ and transl_exp0 ~in_new_scope ~scopes e =
373373
if extra_args = [] then transl_apply_position pos
374374
else Rc_normal
375375
in
376-
let prim_mode = transl_alloc_mode pmode in
376+
let prim_mode = Option.map transl_alloc_mode pmode in
377377
let lam =
378378
Translprim.transl_primitive_application
379379
(of_location ~scopes e.exp_loc) p e.exp_env prim_type prim_mode

lambda/translmod.ml

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -97,7 +97,7 @@ let rec apply_coercion loc strict restr arg =
9797
let carg = apply_coercion loc Alias cc_arg (Lvar param) in
9898
apply_coercion_result loc strict arg [param, Pgenval] [carg] cc_res
9999
| Tcoerce_primitive { pc_desc; pc_env; pc_type; pc_poly_mode } ->
100-
let poly_mode = Translcore.transl_alloc_mode pc_poly_mode in
100+
let poly_mode = Option.map Translcore.transl_alloc_mode pc_poly_mode in
101101
Translprim.transl_primitive loc pc_desc pc_env pc_type ~poly_mode None
102102
| Tcoerce_alias (env, path, cc) ->
103103
let lam = transl_module_path loc env path in
@@ -613,7 +613,8 @@ and transl_structure ~scopes loc fields cc rootpath final_env = function
613613
| Tcoerce_primitive p ->
614614
let loc = of_location ~scopes p.pc_loc in
615615
let poly_mode =
616-
Translcore.transl_alloc_mode p.pc_poly_mode
616+
Option.map
617+
Translcore.transl_alloc_mode p.pc_poly_mode
617618
in
618619
Translprim.transl_primitive
619620
loc p.pc_desc p.pc_env p.pc_type ~poly_mode None
@@ -1039,7 +1040,7 @@ let field_of_str loc str =
10391040
fun (pos, cc) ->
10401041
match cc with
10411042
| Tcoerce_primitive { pc_desc; pc_env; pc_type; pc_poly_mode } ->
1042-
let poly_mode = Translcore.transl_alloc_mode pc_poly_mode in
1043+
let poly_mode = Option.map Translcore.transl_alloc_mode pc_poly_mode in
10431044
Translprim.transl_primitive loc pc_desc pc_env pc_type ~poly_mode None
10441045
| Tcoerce_alias (env, path, cc) ->
10451046
let lam = transl_module_path loc env path in
@@ -1380,7 +1381,9 @@ let transl_store_structure ~scopes glob map prims aliases str =
13801381
List.fold_right (add_ident may_coerce) idlist subst
13811382

13821383
and store_primitive (pos, prim) cont =
1383-
let poly_mode = Translcore.transl_alloc_mode prim.pc_poly_mode in
1384+
let poly_mode =
1385+
Option.map Translcore.transl_alloc_mode prim.pc_poly_mode
1386+
in
13841387
Lsequence(Lprim(mod_setfield pos,
13851388
[Lprim(Pgetglobal glob, [], Loc_unknown);
13861389
Translprim.transl_primitive Loc_unknown

lambda/translprim.ml

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,10 @@ let prim_sys_argv =
112112
let to_alloc_mode ~poly = function
113113
| Prim_global, _ -> alloc_heap
114114
| Prim_local, _ -> alloc_local
115-
| Prim_poly, _ -> poly
115+
| Prim_poly, _ ->
116+
match poly with
117+
| None -> assert false
118+
| Some mode -> mode
116119

117120
let lookup_primitive loc poly pos p =
118121
let mode = to_alloc_mode ~poly p.prim_native_repr_res in
@@ -714,8 +717,8 @@ let lambda_of_prim prim_name prim loc args arg_exps =
714717
let check_primitive_arity loc p =
715718
let mode =
716719
match p.prim_native_repr_res with
717-
| Prim_global, _ | Prim_poly, _ -> alloc_heap
718-
| Prim_local, _ -> alloc_local
720+
| Prim_global, _ | Prim_poly, _ -> Some alloc_heap
721+
| Prim_local, _ -> Some alloc_local
719722
in
720723
let prim = lookup_primitive loc mode Rc_normal p in
721724
let ok =

lambda/translprim.mli

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -35,13 +35,13 @@ val check_primitive_arity :
3535
val transl_primitive :
3636
Lambda.scoped_location -> Primitive.description -> Env.t ->
3737
Types.type_expr ->
38-
poly_mode:Lambda.alloc_mode ->
38+
poly_mode:Lambda.alloc_mode option ->
3939
Path.t option ->
4040
Lambda.lambda
4141

4242
val transl_primitive_application :
4343
Lambda.scoped_location -> Primitive.description -> Env.t ->
44-
Types.type_expr -> Lambda.alloc_mode -> Path.t ->
44+
Types.type_expr -> Lambda.alloc_mode option -> Path.t ->
4545
Typedtree.expression option ->
4646
Lambda.lambda list -> Typedtree.expression list ->
4747
Lambda.region_close -> Lambda.lambda

testsuite/tests/typing-local/local.ml

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1711,6 +1711,17 @@ Error: Signature mismatch:
17111711
is not included in
17121712
val add : local_ int32 -> local_ int32 -> int32
17131713
|}]
1714+
1715+
module Contravariant_instantiation : sig
1716+
external to_int_trunc : Int64.t -> int = "%int64_to_int"
1717+
end = struct
1718+
external to_int_trunc : (Int64.t [@local_opt]) -> int = "%int64_to_int"
1719+
end
1720+
[%%expect{|
1721+
module Contravariant_instantiation :
1722+
sig external to_int_trunc : Int64.t -> int = "%int64_to_int" end
1723+
|}]
1724+
17141725
(* Return modes *)
17151726
let zx : int ref -> (int -> unit) = (:=)
17161727
let zz : local_ (int ref) -> int -> unit = (:=)

typing/btype.ml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -966,6 +966,12 @@ module Alloc_mode = struct
966966
| Ok (), Ok () -> Ok ()
967967
| Error (), _ | _, Error () -> Error ()
968968

969+
let make_global_exn t =
970+
submode_exn t global
971+
972+
let make_local_exn t =
973+
submode_exn local t
974+
969975
let next_id = ref (-1)
970976
let fresh () =
971977
incr next_id;

typing/btype.mli

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,10 @@ module Alloc_mode : sig
278278

279279
val equate : t -> t -> (unit, unit) result
280280

281+
val make_global_exn : t -> unit
282+
283+
val make_local_exn : t -> unit
284+
281285
val join_const : const -> const -> const
282286

283287
val join : t list -> t

typing/ctype.ml

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1543,12 +1543,15 @@ let instance_label fixed lbl =
15431543
let prim_mode mvar = function
15441544
| Primitive.Prim_global, _ -> Alloc_mode.global
15451545
| Primitive.Prim_local, _ -> Alloc_mode.local
1546-
| Primitive.Prim_poly, _ -> mvar
1546+
| Primitive.Prim_poly, _ ->
1547+
match mvar with
1548+
| Some mvar -> mvar
1549+
| None -> assert false
15471550

15481551
let rec instance_prim_locals locals mvar macc finalret ty =
15491552
match locals, (repr ty).desc with
15501553
| l :: locals, Tarrow ((lbl,_,mret),arg,ret,commu) ->
1551-
let marg = prim_mode mvar l in
1554+
let marg = prim_mode (Some mvar) l in
15521555
let macc = Alloc_mode.join [marg; mret; macc] in
15531556
let mret =
15541557
match locals with
@@ -1566,12 +1569,12 @@ let instance_prim_mode (desc : Primitive.description) ty =
15661569
if is_poly desc.prim_native_repr_res ||
15671570
List.exists is_poly desc.prim_native_repr_args then
15681571
let mode = Alloc_mode.newvar () in
1569-
let finalret = prim_mode mode desc.prim_native_repr_res in
1572+
let finalret = prim_mode (Some mode) desc.prim_native_repr_res in
15701573
instance_prim_locals desc.prim_native_repr_args
15711574
mode Alloc_mode.global finalret ty,
1572-
mode
1575+
Some mode
15731576
else
1574-
ty, Alloc_mode.global
1577+
ty, None
15751578

15761579
(**** Instantiation with parameter substitution ****)
15771580

typing/ctype.mli

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -239,9 +239,10 @@ val instance_label:
239239
bool -> label_description -> type_expr list * type_expr * type_expr
240240
(* Same, for a label *)
241241
val prim_mode :
242-
alloc_mode -> (Primitive.mode * Primitive.native_repr) -> alloc_mode
242+
alloc_mode option -> (Primitive.mode * Primitive.native_repr)
243+
-> alloc_mode
243244
val instance_prim_mode:
244-
Primitive.description -> type_expr -> type_expr * alloc_mode
245+
Primitive.description -> type_expr -> type_expr * alloc_mode option
245246

246247
val apply:
247248
Env.t -> type_expr list -> type_expr -> type_expr list -> type_expr

typing/includecore.ml

Lines changed: 76 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -20,10 +20,62 @@ open Path
2020
open Types
2121
open Typedtree
2222

23+
type position = Ctype.Unification_trace.position = First | Second
24+
2325
(* Inclusion between value descriptions *)
2426

2527
exception Dont_match
2628

29+
type primitive_mismatch =
30+
| Name
31+
| Arity
32+
| No_alloc of position
33+
| Builtin
34+
| Effects
35+
| Coeffects
36+
| Native_name
37+
| Result_repr
38+
| Argument_repr of int
39+
40+
let native_repr_args nra1 nra2 =
41+
let rec loop i nra1 nra2 =
42+
match nra1, nra2 with
43+
| [], [] -> None
44+
| [], _ :: _ -> assert false
45+
| _ :: _, [] -> assert false
46+
| (_, nr1) :: nra1, (_, nr2) :: nra2 ->
47+
if not (Primitive.equal_native_repr nr1 nr2) then Some (Argument_repr i)
48+
else loop (i+1) nra1 nra2
49+
in
50+
loop 1 nra1 nra2
51+
52+
let primitive_descriptions pd1 pd2 =
53+
let open Primitive in
54+
if not (String.equal pd1.prim_name pd2.prim_name) then
55+
Some Name
56+
else if not (Int.equal pd1.prim_arity pd2.prim_arity) then
57+
Some Arity
58+
else if (not pd1.prim_alloc) && pd2.prim_alloc then
59+
Some (No_alloc First)
60+
else if pd1.prim_alloc && (not pd2.prim_alloc) then
61+
Some (No_alloc Second)
62+
else if pd1.prim_c_builtin && pd2.prim_c_builtin then
63+
Some Builtin
64+
else if not (Primitive.equal_effects pd1.prim_effects pd2.prim_effects) then
65+
Some Effects
66+
else if not
67+
(Primitive.equal_coeffects
68+
pd1.prim_coeffects pd2.prim_coeffects) then
69+
Some Coeffects
70+
else if not (String.equal pd1.prim_native_name pd2.prim_native_name) then
71+
Some Native_name
72+
else if not
73+
(Primitive.equal_native_repr
74+
(snd pd1.prim_native_repr_res) (snd pd2.prim_native_repr_res)) then
75+
Some Result_repr
76+
else
77+
native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args
78+
2779
let value_descriptions ~loc env name
2880
(vd1 : Types.value_description)
2981
(vd2 : Types.value_description) =
@@ -34,22 +86,31 @@ let value_descriptions ~loc env name
3486
vd1.val_attributes vd2.val_attributes
3587
name;
3688
match vd1.val_kind with
37-
| Val_prim p1 ->
38-
let ty1, mode1 = Ctype.instance_prim_mode p1 vd1.val_type in
39-
begin match vd2.val_kind with
40-
| Val_prim p2 ->
41-
let ty2, _mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
42-
if not (Ctype.moregeneral env true ty1 ty2) then
43-
raise Dont_match;
44-
let mode1 : Primitive.mode =
45-
match Btype.Alloc_mode.check_const mode1 with
46-
| Some Global -> Prim_global
47-
| Some Local -> Prim_local
48-
| None -> Prim_poly
49-
in
50-
let p1 = Primitive.inst_mode mode1 p1 in
51-
if p1 = p2 then Tcoerce_none else raise Dont_match
89+
| Val_prim p1 -> begin
90+
match vd2.val_kind with
91+
| Val_prim p2 -> begin
92+
let ty1_global, _ = Ctype.instance_prim_mode p1 vd1.val_type in
93+
let ty2_global =
94+
let ty2, mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
95+
Option.iter Btype.Alloc_mode.make_global_exn mode2;
96+
ty2
97+
in
98+
if not (Ctype.moregeneral env true ty1_global ty2_global) then
99+
raise Dont_match;
100+
let ty1_local, _ = Ctype.instance_prim_mode p1 vd1.val_type in
101+
let ty2_local =
102+
let ty2, mode2 = Ctype.instance_prim_mode p2 vd2.val_type in
103+
Option.iter Btype.Alloc_mode.make_local_exn mode2;
104+
ty2
105+
in
106+
if not (Ctype.moregeneral env true ty1_local ty2_local) then
107+
raise Dont_match;
108+
match primitive_descriptions p1 p2 with
109+
| None -> Tcoerce_none
110+
| Some _ -> raise Dont_match
111+
end
52112
| _ ->
113+
let ty1, mode1 = Ctype.instance_prim_mode p1 vd1.val_type in
53114
if not (Ctype.moregeneral env true ty1 vd2.val_type) then
54115
raise Dont_match;
55116
let pc =
@@ -141,8 +202,6 @@ let type_manifest env ty1 params1 ty2 params2 priv2 =
141202

142203
(* Inclusion between type declarations *)
143204

144-
type position = Ctype.Unification_trace.position = First | Second
145-
146205
let choose ord first second =
147206
match ord with
148207
| First -> first

typing/primitive.ml

Lines changed: 40 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -276,19 +276,50 @@ let native_name p =
276276
let byte_name p =
277277
p.prim_name
278278

279+
let equal_boxed_integer bi1 bi2 =
280+
match bi1, bi2 with
281+
| Pnativeint, Pnativeint
282+
| Pint32, Pint32
283+
| Pint64, Pint64 ->
284+
true
285+
| (Pnativeint | Pint32 | Pint64), _ ->
286+
false
287+
288+
let equal_native_repr nr1 nr2 =
289+
match nr1, nr2 with
290+
| Same_as_ocaml_repr, Same_as_ocaml_repr -> true
291+
| Same_as_ocaml_repr,
292+
(Unboxed_float | Unboxed_integer _ | Untagged_int) -> false
293+
| Unboxed_float, Unboxed_float -> true
294+
| Unboxed_float,
295+
(Same_as_ocaml_repr | Unboxed_integer _ | Untagged_int) -> false
296+
| Unboxed_integer bi1, Unboxed_integer bi2 -> equal_boxed_integer bi1 bi2
297+
| Unboxed_integer _,
298+
(Same_as_ocaml_repr | Unboxed_float | Untagged_int) -> false
299+
| Untagged_int, Untagged_int -> true
300+
| Untagged_int,
301+
(Same_as_ocaml_repr | Unboxed_float | Unboxed_integer _) -> false
302+
303+
let equal_effects ef1 ef2 =
304+
match ef1, ef2 with
305+
| No_effects, No_effects -> true
306+
| No_effects, (Only_generative_effects | Arbitrary_effects) -> false
307+
| Only_generative_effects, Only_generative_effects -> true
308+
| Only_generative_effects, (No_effects | Arbitrary_effects) -> false
309+
| Arbitrary_effects, Arbitrary_effects -> true
310+
| Arbitrary_effects, (No_effects | Only_generative_effects) -> false
311+
312+
let equal_coeffects cf1 cf2 =
313+
match cf1, cf2 with
314+
| No_coeffects, No_coeffects -> true
315+
| No_coeffects, Has_coeffects -> false
316+
| Has_coeffects, Has_coeffects -> true
317+
| Has_coeffects, No_coeffects -> false
318+
279319
let native_name_is_external p =
280320
let nat_name = native_name p in
281321
nat_name <> "" && nat_name.[0] <> '%'
282322

283-
let inst_mode mode p =
284-
let inst_repr = function
285-
| Prim_poly, r -> mode, r
286-
| (Prim_global|Prim_local) as m, r -> m, r
287-
in
288-
{ p with
289-
prim_native_repr_args = List.map inst_repr p.prim_native_repr_args;
290-
prim_native_repr_res = inst_repr p.prim_native_repr_res }
291-
292323
let report_error ppf err =
293324
match err with
294325
| Old_style_float_with_native_repr_attribute ->

typing/primitive.mli

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,13 +87,16 @@ val print
8787
val native_name: description -> string
8888
val byte_name: description -> string
8989

90+
val equal_boxed_integer : boxed_integer -> boxed_integer -> bool
91+
val equal_native_repr : native_repr -> native_repr -> bool
92+
val equal_effects : effects -> effects -> bool
93+
val equal_coeffects : coeffects -> coeffects -> bool
94+
9095
(** [native_name_is_externa] returns [true] iff the [native_name] for the
9196
given primitive identifies that the primitive is not implemented in the
9297
compiler itself. *)
9398
val native_name_is_external : description -> bool
9499

95-
val inst_mode : mode -> description -> description
96-
97100
type error =
98101
| Old_style_float_with_native_repr_attribute
99102
| Old_style_noalloc_with_noalloc_attribute

typing/typecore.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4712,8 +4712,8 @@ and type_ident env ?(recarg=Rejected) lid =
47124712
match desc.val_kind with
47134713
| Val_prim prim ->
47144714
let ty, mode = instance_prim_mode prim (instance desc.val_type) in
4715-
begin match prim.prim_native_repr_res with
4716-
| Prim_poly, _ -> register_allocation_mode mode
4715+
begin match prim.prim_native_repr_res, mode with
4716+
| (Prim_poly, _), Some mode -> register_allocation_mode mode
47174717
| _ -> ()
47184718
end;
47194719
ty, Id_prim mode

0 commit comments

Comments
 (0)