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. --- backend/Allocation.v | 107 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 65 insertions(+), 42 deletions(-) (limited to 'backend/Allocation.v') diff --git a/backend/Allocation.v b/backend/Allocation.v index 37b79a1a..5499c1c5 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -93,12 +93,10 @@ Inductive block_shape: Type := (mv1: moves) (ros': mreg + ident) (mv2: moves) (s: node) | BStailcall (sg: signature) (ros: reg + ident) (args: list reg) (mv1: moves) (ros': mreg + ident) - | BSbuiltin (ef: external_function) (args: list reg) (res: reg) - (mv1: moves) (args': list mreg) (res': list mreg) + | BSbuiltin (ef: external_function) + (args: list (builtin_arg reg)) (res: builtin_res reg) + (mv1: moves) (args': list (builtin_arg loc)) (res': builtin_res mreg) (mv2: moves) (s: node) - | BSannot (ef: external_function) - (args: list (annot_arg reg)) (args': list (annot_arg loc)) - (s: node) | BScond (cond: condition) (args: list reg) (mv: moves) (args': list mreg) (s1 s2: node) | BSjumptable (arg: reg) @@ -280,14 +278,6 @@ Definition pair_instr_block Some(BSbuiltin ef args res mv1 args' res' mv2 s) | _ => None end - | Iannot ef args s => - match b with - | Lannot ef' args' :: b1 => - assertion (external_function_eq ef ef'); - assertion (check_succ s b1); - Some(BSannot ef args args' s) - | _ => None - end | Icond cond args s1 s2 => let (mv1, b1) := extract_moves nil b in match b1 with @@ -699,54 +689,86 @@ Definition add_equation_ros (ros: reg + ident) (ros': mreg + ident) (e: eqs) : o | _, _ => None end. -(** [add_equations_annot_arg] adds the needed equations for annotation - arguments. *) +(** [add_equations_builtin_arg] adds the needed equations for arguments + to builtin functions. *) -Fixpoint add_equations_annot_arg (env: regenv) (arg: annot_arg reg) (arg': annot_arg loc) (e: eqs) : option eqs := +Fixpoint add_equations_builtin_arg + (env: regenv) (arg: builtin_arg reg) (arg': builtin_arg loc) (e: eqs) : option eqs := match arg, arg' with - | AA_base r, AA_base l => + | BA r, BA l => Some (add_equation (Eq Full r l) e) - | AA_base r, AA_longofwords (AA_base lhi) (AA_base llo) => + | BA r, BA_longofwords (BA lhi) (BA llo) => assertion (typ_eq (env r) Tlong); Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e)) - | AA_int n, AA_int n' => + | BA_int n, BA_int n' => assertion (Int.eq_dec n n'); Some e - | AA_long n, AA_long n' => + | BA_long n, BA_long n' => assertion (Int64.eq_dec n n'); Some e - | AA_float f, AA_float f' => + | BA_float f, BA_float f' => assertion (Float.eq_dec f f'); Some e - | AA_single f, AA_single f' => + | BA_single f, BA_single f' => assertion (Float32.eq_dec f f'); Some e - | AA_loadstack chunk ofs, AA_loadstack chunk' ofs' => + | BA_loadstack chunk ofs, BA_loadstack chunk' ofs' => assertion (chunk_eq chunk chunk'); assertion (Int.eq_dec ofs ofs'); Some e - | AA_addrstack ofs, AA_addrstack ofs' => + | BA_addrstack ofs, BA_addrstack ofs' => assertion (Int.eq_dec ofs ofs'); Some e - | AA_loadglobal chunk id ofs, AA_loadglobal chunk' id' ofs' => + | BA_loadglobal chunk id ofs, BA_loadglobal chunk' id' ofs' => assertion (chunk_eq chunk chunk'); assertion (ident_eq id id'); assertion (Int.eq_dec ofs ofs'); Some e - | AA_addrglobal id ofs, AA_addrglobal id' ofs' => + | BA_addrglobal id ofs, BA_addrglobal id' ofs' => assertion (ident_eq id id'); assertion (Int.eq_dec ofs ofs'); Some e - | AA_longofwords hi lo, AA_longofwords hi' lo' => - do e1 <- add_equations_annot_arg env hi hi' e; - add_equations_annot_arg env lo lo' e1 + | BA_longofwords hi lo, BA_longofwords hi' lo' => + do e1 <- add_equations_builtin_arg env hi hi' e; + add_equations_builtin_arg env lo lo' e1 | _, _ => None end. -Fixpoint add_equations_annot_args (env: regenv) - (args: list(annot_arg reg)) (args': list(annot_arg loc)) (e: eqs) : option eqs := +Fixpoint add_equations_builtin_args + (env: regenv) (args: list (builtin_arg reg)) + (args': list (builtin_arg loc)) (e: eqs) : option eqs := match args, args' with | nil, nil => Some e | a1 :: al, a1' :: al' => - do e1 <- add_equations_annot_arg env a1 a1' e; - add_equations_annot_args env al al' e1 + do e1 <- add_equations_builtin_arg env a1 a1' e; + add_equations_builtin_args env al al' e1 + | _, _ => None + end. + +(** For [EF_debug] builtins, some arguments can be removed. *) + +Fixpoint add_equations_debug_args + (env: regenv) (args: list (builtin_arg reg)) + (args': list (builtin_arg loc)) (e: eqs) : option eqs := + match args, args' with + | _, nil => Some e + | a1 :: al, a1' :: al' => + match add_equations_builtin_arg env a1 a1' e with + | None => add_equations_debug_args env al args' e + | Some e1 => add_equations_debug_args env al al' e1 + end + | _, _ => None + end. + +(** Checking of the result of a builtin *) + +Definition remove_equations_builtin_res + (env: regenv) (res: builtin_res reg) (res': builtin_res mreg) (e: eqs) : option eqs := + match res, res' with + | BR r, BR r' => Some (remove_equation (Eq Full r (R r')) e) + | BR r, BR_longofwords (BR rhi) (BR rlo) => + assertion (typ_eq (env r) Tlong); + if mreg_eq rhi rlo then None else + Some (remove_equation (Eq Low r (R rlo)) + (remove_equation (Eq High r (R rhi)) e)) + | BR_none, BR_none => Some e | _, _ => None end. @@ -972,16 +994,18 @@ Definition transfer_aux (f: RTL.function) (env: regenv) track_moves env mv1 e2 | BSbuiltin ef args res mv1 args' res' mv2 s => do e1 <- track_moves env mv2 e; - let args' := map R args' in - let res' := map R res' in - do e2 <- remove_equations_res res (sig_res (ef_sig ef)) res' e1; - assertion (reg_unconstrained res e2); - assertion (forallb (fun l => loc_unconstrained l e2) res'); + do e2 <- remove_equations_builtin_res env res res' e1; + assertion (forallb (fun r => reg_unconstrained r e2) + (params_of_builtin_res res)); + assertion (forallb (fun mr => loc_unconstrained (R mr) e2) + (params_of_builtin_res res')); assertion (can_undef (destroyed_by_builtin ef) e2); - do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2; + do e3 <- + match ef with + | EF_debug _ _ _ => add_equations_debug_args env args args' e2 + | _ => add_equations_builtin_args env args args' e2 + end; track_moves env mv1 e3 - | BSannot ef args args' s => - add_equations_annot_args env args args' e | BScond cond args mv args' s1 s2 => assertion (can_undef (destroyed_by_cond cond) e); do e1 <- add_equations args args' e; @@ -1152,7 +1176,6 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BScall sg ros args res mv1 ros' mv2 s => s :: nil | BStailcall sg ros args mv1 ros' => nil | BSbuiltin ef args res mv1 args' res' mv2 s => s :: nil - | BSannot ef args args' s => s :: nil | BScond cond args mv args' s1 s2 => s1 :: s2 :: nil | BSjumptable arg mv arg' tbl => tbl | BSreturn optarg mv => nil -- cgit