From 5f6e788e0f404755d6cd1494e18e38758865188f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 25 Mar 2021 11:27:05 +0100 Subject: Split the return type away from the signature of primitive operations. This avoids having to drop the last element of the signature in the common case. --- kernel/cPrimitives.ml | 76 ++++++++++++++++++++++++++++++++------------------ kernel/cPrimitives.mli | 4 +-- kernel/nativecode.ml | 5 ++-- kernel/typeops.ml | 13 +++++---- 4 files changed, 60 insertions(+), 38 deletions(-) (limited to 'kernel') diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 6ef0e9fa15..9e0f574fa3 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -295,38 +295,57 @@ let types = PITT_param 1)) in function - | Int63head0 | Int63tail0 -> [int_ty; int_ty] + | Int63head0 | Int63tail0 -> + [int_ty], int_ty | Int63add | Int63sub | Int63mul | Int63div | Int63mod | Int63divs | Int63mods | Int63lsr | Int63lsl | Int63asr - | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] + | Int63land | Int63lor | Int63lxor -> + [int_ty; int_ty], int_ty | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> - [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] + [int_ty; int_ty], PITT_ind (PIT_carry, int_ty) | Int63mulc | Int63diveucl -> - [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] - | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) + | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> + [int_ty; int_ty], PITT_ind (PIT_bool, ()) + | Int63compare | Int63compares -> + [int_ty; int_ty], PITT_ind (PIT_cmp, ()) | Int63div21 -> - [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] + [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty)) + | Int63addMulDiv -> + [int_ty; int_ty; int_ty], int_ty | Float64opp | Float64abs | Float64sqrt - | Float64next_up | Float64next_down -> [float_ty; float_ty] - | Float64ofInt63 -> [int_ty; float_ty] - | Float64normfr_mantissa -> [float_ty; int_ty] - | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))] - | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())] - | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())] - | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())] - | Float64add | Float64sub | Float64mul - | Float64div -> [float_ty; float_ty; float_ty] - | Float64ldshiftexp -> [float_ty; int_ty; float_ty] - | Arraymake -> [int_ty; PITT_param 1; array_ty] - | Arrayget -> [array_ty; int_ty; PITT_param 1] - | Arraydefault -> [array_ty; PITT_param 1] - | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] - | Arraycopy -> [array_ty; array_ty] - | Arraylength -> [array_ty; int_ty] + | Float64next_up | Float64next_down -> + [float_ty], float_ty + | Float64ofInt63 -> + [int_ty], float_ty + | Float64normfr_mantissa -> + [float_ty], int_ty + | Float64frshiftexp -> + [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty)) + | Float64eq | Float64lt | Float64le -> + [float_ty; float_ty], PITT_ind (PIT_bool, ()) + | Float64compare -> + [float_ty; float_ty], PITT_ind (PIT_f_cmp, ()) + | Float64classify -> + [float_ty], PITT_ind (PIT_f_class, ()) + | Float64add | Float64sub | Float64mul | Float64div -> + [float_ty; float_ty], float_ty + | Float64ldshiftexp -> + [float_ty; int_ty], float_ty + | Arraymake -> + [int_ty; PITT_param 1], array_ty + | Arrayget -> + [array_ty; int_ty], PITT_param 1 + | Arraydefault -> + [array_ty], PITT_param 1 + | Arrayset -> + [array_ty; int_ty; PITT_param 1], array_ty + | Arraycopy -> + [array_ty], array_ty + | Arraylength -> + [array_ty], int_ty let one_param = (* currently if there's a parameter it's always this *) @@ -460,14 +479,17 @@ type args_red = arg_kind list (* Invariant only argument of type int63, float or an inductive can have kind Kwhnf *) -let arity t = let sign = types t in nparams t + List.length sign - 1 +let arity t = + nparams t + List.length (fst (types t)) let kind t = let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in - params (nparams t) @ List.map args (CList.drop_last (types t)) + params (nparams t) @ List.map args (fst (types t)) -let types t = params t, types t +let types t = + let args_ty, ret_ty = types t in + params t, args_ty, ret_ty (** Special Entries for Register **) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index de90179726..6661851d53 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -140,8 +140,8 @@ val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type val univs : t -> Univ.AUContext.t -val types : t -> Constr.rel_context * ind_or_type list -(** Parameters * Reduction relevant arguments and output type +val types : t -> Constr.rel_context * ind_or_type list * ind_or_type +(** Parameters * Reduction relevant arguments * output type XXX we could reify universes in ind_or_type (currently polymorphic types like array are assumed to use universe 0). *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9ce388929c..22bbcb8a65 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -994,9 +994,8 @@ let extract_prim ml_of l = let decl = ref [] in let cond = ref [] in let type_args p = - let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in - let params, sign = CPrimitives.types p in - List.length params, Array.of_list (aux sign) in + let params, args_ty, _ = CPrimitives.types p in + List.length params, Array.of_list args_ty in let rec aux l = match l with | Lprim(prefix,kn,p,args) -> diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 741491c917..1b1aa84e6b 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -785,15 +785,16 @@ let type_of_prim env u t = | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t | PITT_param i -> Constr.mkRel (n+i) in - let rec nary_op n = function - | [] -> assert false - | [ret_ty] -> tr_type n ret_ty + let rec nary_op n ret_ty = function + | [] -> tr_type n ret_ty | arg_ty :: r -> - Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r) + Constr.mkProd (Context.nameR (Id.of_string "x"), + tr_type n arg_ty, nary_op (n + 1) ret_ty r) in - let params, sign = types t in + let params, args_ty, ret_ty = types t in assert (AUContext.size (univs t) = Instance.length u); - Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params) + Vars.subst_instance_constr u + (Term.it_mkProd_or_LetIn (nary_op 0 ret_ty args_ty) params) let type_of_prim_or_type env u = let open CPrimitives in function -- cgit v1.2.3 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') 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/vmbytecodes.ml | 2 ++ kernel/vmbytecodes.mli | 1 + kernel/vmbytegen.ml | 4 ++-- kernel/vmemitcodes.ml | 5 ++++- 4 files changed, 9 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index c2b087f061..1783560694 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -35,6 +35,7 @@ type instruction = | Kpush | Kpop of int | Kpush_retaddr of Label.t + | Kshort_apply of int | Kapply of int | Kappterm of int * int | Kreturn of int @@ -93,6 +94,7 @@ let rec pp_instr i = | Kpush -> str "push" | Kpop n -> str "pop " ++ int n | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl + | Kshort_apply n -> str "short_apply " ++ int n | Kapply n -> str "apply " ++ int n | Kappterm(n, m) -> str "appterm " ++ int n ++ str ", " ++ int m diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index eeca0d2ad1..d9e2d91177 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -30,6 +30,7 @@ type instruction = | Kpush (** sp = accu :: sp *) | Kpop of int (** sp = skipn n sp *) | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *) + | Kshort_apply of int (** number of arguments (arguments on top of stack) *) | Kapply of int (** number of arguments (arguments on top of stack) *) | Kappterm of int * int (** number of arguments, slot size *) | Kreturn of int (** slot size *) 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) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index caa263432e..44e933ef26 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -300,8 +300,11 @@ let emit_instr env = function out env opPOP; out_int env n | Kpush_retaddr lbl -> out env opPUSH_RETADDR; out_label env lbl + | Kshort_apply n -> + assert (1 <= n && n <= 4); + out env(opAPPLY1 + n - 1) | Kapply n -> - if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) + out env opAPPLY; out_int env n | Kappterm(n, sz) -> if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) else (out env opAPPTERM; out_int env n; out_int env sz) -- 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') 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 From 682a3f473d318e549ed8cf61f3690573e32c00be Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 25 Mar 2021 14:58:39 +0100 Subject: Improve dump of primitive OCaml operations. --- kernel/vmbytecodes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index 1783560694..b5604d0593 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -148,8 +148,8 @@ let rec pp_instr i = (Constant.print (fst id)) | Kcamlprim (op, lbl) -> - str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ - pp_lbl lbl + str "camlcall " ++ str (CPrimitives.to_string op) ++ str ", branch " ++ + pp_lbl lbl ++ str " on accu" and pp_bytecodes c = match c with -- cgit v1.2.3