From 6d7fdaf8484da81993958d339e411d8e3b1a38c1 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 25 Mar 2021 11:28:17 +0100 Subject: Fix assertion that checks that APPLY can only be passed 4 arguments. --- kernel/vmbytegen.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vmbytegen.ml') diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 7d3b3469b0..3dc268ccdf 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -761,7 +761,7 @@ let rec compile_lam env cenv lam sz cont = let arity = CPrimitives.arity op in let nparams = CPrimitives.nparams op in let nargs = arity - nparams in - assert (arity = Array.length args && arity <= 4); + assert (arity = Array.length args && arity + Univ.Instance.length u <= 4); let (jump, cont) = make_branch cont in let lbl_default = Label.create () in let default = -- cgit v1.2.3 From ae819deb38c3a962e3badf020705c3d0c6c84e67 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 25 Mar 2021 12:03:40 +0100 Subject: Make it more obvious when the calling convention of APPLY changes. Despite their names, APPLY1 to APPLY4 are completely different from APPLY(n) with n = 1 to 4. Indeed, the latter assumes that the return address was already pushed on the stack, before the arguments were. On the other hand, APPLY1 to APPLY4 insert the return address in the middle of the already pushed arguments. --- kernel/vmbytegen.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/vmbytegen.ml') diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 3dc268ccdf..9500b88e60 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont = | None -> if nargs <= 4 then comp_args comp_arg cenv args sz - (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont))) + (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont))) else let lbl,cont1 = label_code cont in Kpush_retaddr lbl :: @@ -765,7 +765,7 @@ let rec compile_lam env cenv lam sz cont = let (jump, cont) = make_branch cont in let lbl_default = Label.create () in let default = - let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in + let cont = [Kgetglobal kn; Kshort_apply (arity + Univ.Instance.length u); jump] in let cont = if Univ.Instance.is_empty u then cont else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) -- cgit v1.2.3 From 6a6e58ea763d3bacda86056b6e7f404bf95ad45d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 25 Mar 2021 14:32:27 +0100 Subject: Support OCaml primitives with an actual arity larger than 4. PArray.set has arity 4, but due to the polymorphic universe, its actual arity is 5. As a consequence, Kshort_apply cannot be used to invoke it (or rather its accumulating version). Using Kapply does not quite work here, because Kpush_retaddr would have to be invoked before the arguments, that is, before we even know whether the arguments are accumulators. So, to use Kapply, one would need to push the return address, push duplicates of the already computed arguments, call the accumulator, and then pop the original arguments. This commit follows a simpler approach, but more restrictive, as it is still limited to arity 4, but this time independently from universes. To do so, the call is performed in two steps. First, a closure containing the universes is created. Second, the actual application to the original arguments is performed, for which Kshort_apply is sufficient. So, this is inefficient, because a closure is created just so that it can be immediately fully applied. But since this is the accumulator slow path, this does not matter. --- kernel/vmbytegen.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'kernel/vmbytegen.ml') diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 9500b88e60..b4d97228bf 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -757,26 +757,25 @@ let rec compile_lam env cenv lam sz cont = let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in comp_args (compile_lam env) cenv args sz cont - | Lprim ((kn,u), op, args) when is_caml_prim op -> + | Lprim (kn, op, args) when is_caml_prim op -> let arity = CPrimitives.arity op in let nparams = CPrimitives.nparams op in let nargs = arity - nparams in - assert (arity = Array.length args && arity + Univ.Instance.length u <= 4); + assert (arity = Array.length args && arity <= 4 && nargs >= 1); let (jump, cont) = make_branch cont in let lbl_default = Label.create () in let default = - let cont = [Kgetglobal kn; Kshort_apply (arity + Univ.Instance.length u); jump] in + let cont = [Kshort_apply arity; jump] in + let cont = Kpush :: compile_get_global cenv kn (sz + arity) cont in let cont = - if Univ.Instance.is_empty u then cont - else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont) - in - Klabel lbl_default :: - Kpush :: - if Int.equal nparams 0 then cont - else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont) - in + if Int.equal nparams 0 then cont + else + let params = Array.sub args 0 nparams in + Kpush :: comp_args (compile_lam env) cenv params (sz + nargs) cont in + Klabel lbl_default :: cont in fun_code := Ksequence default :: !fun_code; - comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont) + let cont = Kcamlprim (op, lbl_default) :: cont in + comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz cont | Lprim (kn, op, args) -> comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont) -- cgit v1.2.3