From 54f97d1988f623ba7422e13a504caeb5701ba93c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 21 Aug 2015 11:05:36 +0200 Subject: Refactoring of builtins and annotations in the back-end. Before, the back-end languages had distinct instructions - Iannot for annotations, taking structured expressions (annot_arg) as arguments, and producing no results' - Ibuiltin for other builtins, using simple pseudoregs/locations/registers as arguments and results. This branch enriches Ibuiltin instructions so that they take structured expressions (builtin_arg and builtin_res) as arguments and results. This way, - Annotations fit the general pattern of builtin functions, so Iannot instructions are removed. - EF_vload_global and EF_vstore_global become useless, as the same optimization can be achieved by EF_vload/vstore taking a structured argument of the "address of global" kind. - Better code can be generated for builtin_memcpy between stack locations, or volatile accesses to stack locations. Finally, this commit also introduces a new kind of external function, EF_debug, which is like EF_annot but produces no observable events. It will be used later to transport debug info through the back-end, without preventing optimizations. --- common/AST.v | 143 +++++++++++++++++++++++++++++++++++------------------------ 1 file changed, 85 insertions(+), 58 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 387eb6b2..1f393c72 100644 --- a/common/AST.v +++ b/common/AST.v @@ -560,12 +560,6 @@ Inductive external_function : Type := (** A volatile store operation. If the adress given as first argument points within a volatile global variable, generate an event. Otherwise, produce no event and behave like a regular memory store. *) - | EF_vload_global (chunk: memory_chunk) (id: ident) (ofs: int) - (** A volatile load operation from a global variable. - Specialized version of [EF_vload]. *) - | EF_vstore_global (chunk: memory_chunk) (id: ident) (ofs: int) - (** A volatile store operation in a global variable. - Specialized version of [EF_vstore]. *) | EF_malloc (** Dynamic memory allocation. Takes the requested size in bytes as argument; returns a pointer to a fresh block of the given size. @@ -585,12 +579,16 @@ Inductive external_function : Type := (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string). + | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) + | EF_debug (kind: positive) (text: ident) (targs: list typ). + (** Transport debugging information from the front-end to the generated + assembly. Takes zero, one or several arguments like [EF_annot]. + Unlike [EF_annot], produces no observable event. *) (** The type signature of an external function. *) @@ -600,14 +598,13 @@ Definition ef_sig (ef: external_function): signature := | EF_builtin name sg => sg | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default - | EF_vload_global chunk _ _ => mksignature nil (Some (type_of_chunk chunk)) cc_default - | EF_vstore_global chunk _ _ => mksignature (type_of_chunk chunk :: nil) None cc_default | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text sg clob => sg + | EF_debug kind text targs => mksignature targs None cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -618,14 +615,13 @@ Definition ef_inline (ef: external_function) : bool := | EF_builtin name sg => true | EF_vload chunk => true | EF_vstore chunk => true - | EF_vload_global chunk id ofs => true - | EF_vstore_global chunk id ofs => true | EF_malloc => false | EF_free => false | EF_memcpy sz al => true | EF_annot text targs => true | EF_annot_val text targ => true | EF_inline_asm text sg clob => true + | EF_debug kind text targs => true end. (** Whether an external function must reload its arguments. *) @@ -633,6 +629,7 @@ Definition ef_inline (ef: external_function) : bool := Definition ef_reloads (ef: external_function) : bool := match ef with | EF_annot text targs => false + | EF_debug kind text targs => false | _ => true end. @@ -640,22 +637,12 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. + generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. auto. apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. -(** Global variables referenced by an external function *) - -Definition globals_external (ef: external_function) : list ident := - match ef with - | EF_vload_global _ id _ => id :: nil - | EF_vstore_global _ id _ => id :: nil - | _ => nil - end. - (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := @@ -690,55 +677,95 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := End TRANSF_PARTIAL_FUNDEF. -(** * Arguments to annotations *) +(** * Arguments and results to builtin functions *) Set Contextual Implicit. -Inductive annot_arg (A: Type) : Type := - | AA_base (x: A) - | AA_int (n: int) - | AA_long (n: int64) - | AA_float (f: float) - | AA_single (f: float32) - | AA_loadstack (chunk: memory_chunk) (ofs: int) - | AA_addrstack (ofs: int) - | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) - | AA_addrglobal (id: ident) (ofs: int) - | AA_longofwords (hi lo: annot_arg A). - -Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := +Inductive builtin_arg (A: Type) : Type := + | BA (x: A) + | BA_int (n: int) + | BA_long (n: int64) + | BA_float (f: float) + | BA_single (f: float32) + | BA_loadstack (chunk: memory_chunk) (ofs: int) + | BA_addrstack (ofs: int) + | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | BA_addrglobal (id: ident) (ofs: int) + | BA_longofwords (hi lo: builtin_arg A). + +Inductive builtin_res (A: Type) : Type := + | BR (x: A) + | BR_none + | BR_longofwords (hi lo: builtin_res A). + +Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident := match a with - | AA_loadglobal chunk id ofs => id :: nil - | AA_addrglobal id ofs => id :: nil - | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | BA_loadglobal chunk id ofs => id :: nil + | BA_addrglobal id ofs => id :: nil + | BA_longofwords hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo | _ => nil end. -Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := - List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. +Definition globals_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list ident := + List.fold_right (fun a l => globals_of_builtin_arg a ++ l) nil al. -Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := +Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A := match a with - | AA_base x => x :: nil - | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | BA x => x :: nil + | BA_longofwords hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo | _ => nil end. -Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := - List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. +Definition params_of_builtin_args (A: Type) (al: list (builtin_arg A)) : list A := + List.fold_right (fun a l => params_of_builtin_arg a ++ l) nil al. -Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := +Fixpoint params_of_builtin_res (A: Type) (a: builtin_res A) : list A := match a with - | AA_base x => AA_base (f x) - | AA_int n => AA_int n - | AA_long n => AA_long n - | AA_float n => AA_float n - | AA_single n => AA_single n - | AA_loadstack chunk ofs => AA_loadstack chunk ofs - | AA_addrstack ofs => AA_addrstack ofs - | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs - | AA_addrglobal id ofs => AA_addrglobal id ofs - | AA_longofwords hi lo => - AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + | BR x => x :: nil + | BR_none => nil + | BR_longofwords hi lo => params_of_builtin_res hi ++ params_of_builtin_res lo end. +Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_arg B := + match a with + | BA x => BA (f x) + | BA_int n => BA_int n + | BA_long n => BA_long n + | BA_float n => BA_float n + | BA_single n => BA_single n + | BA_loadstack chunk ofs => BA_loadstack chunk ofs + | BA_addrstack ofs => BA_addrstack ofs + | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs + | BA_addrglobal id ofs => BA_addrglobal id ofs + | BA_longofwords hi lo => + BA_longofwords (map_builtin_arg f hi) (map_builtin_arg f lo) + end. + +Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B := + match a with + | BR x => BR (f x) + | BR_none => BR_none + | BR_longofwords hi lo => + BR_longofwords (map_builtin_res f hi) (map_builtin_res f lo) + end. + +(** Which kinds of builtin arguments are supported by which external function. *) + +Inductive builtin_arg_constraint : Type := + | OK_default + | OK_const + | OK_addrstack + | OK_addrglobal + | OK_addrany + | OK_all. + +Definition builtin_arg_ok + (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) := + match ba, c with + | (BA _ | BA_longofwords _ _), _ => true + | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true + | BA_addrstack _, (OK_addrstack | OK_addrany) => true + | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true + | _, OK_all => true + | _, _ => false + end. -- cgit