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/RTLgen.v | 89 ++++++++++++++++++++++++++++++-------------------------- 1 file changed, 47 insertions(+), 42 deletions(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index b1c36513..45ad8e19 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -381,6 +381,47 @@ Definition add_move (rs rd: reg) (nd: node) : mon node := then ret nd else add_instr (Iop Omove (rs::nil) rd nd). +(** Translation of arguments and results of builtins. *) + +Definition exprlist_of_expr_list (l: list expr) : exprlist := + List.fold_right Econs Enil l. + +Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : builtin_arg A * list A := + match a with + | BA a => + match rl with + | r :: rs => (BA r, rs) + | nil => (BA_int Int.zero, nil) (**r never happens *) + end + | BA_int n => (BA_int n, rl) + | BA_long n => (BA_long n, rl) + | BA_float n => (BA_float n, rl) + | BA_single n => (BA_single n, rl) + | BA_loadstack chunk ofs => (BA_loadstack chunk ofs, rl) + | BA_addrstack ofs => (BA_addrstack ofs, rl) + | BA_loadglobal chunk id ofs => (BA_loadglobal chunk id ofs, rl) + | BA_addrglobal id ofs => (BA_addrglobal id ofs, rl) + | BA_longofwords hi lo => + let (hi', rl1) := convert_builtin_arg hi rl in + let (lo', rl2) := convert_builtin_arg lo rl1 in + (BA_longofwords hi' lo', rl2) + end. + +Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) := + match al with + | nil => nil + | a1 :: al => + let (a1', rl1) := convert_builtin_arg a1 rl in + a1' :: convert_builtin_args al rl1 + end. + +Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) := + match r with + | BR id => do r <- find_var map id; ret (BR r) + | BR_none => ret BR_none + | _ => error (Errors.msg "RTLgen: bad builtin_res") + end. + (** Translation of an expression. [transl_expr map a rd nd] enriches the current CFG with the RTL instructions necessary to compute the value of CminorSel expression [a], leave its result @@ -413,7 +454,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) do r <- find_letvar map n; add_move r rd nd | Ebuiltin ef al => do rl <- alloc_regs map al; - do no <- add_instr (Ibuiltin ef rl rd nd); + do no <- add_instr (Ibuiltin ef (List.map (@BA reg) rl) (BR rd) nd); transl_exprlist map al rl no | Eexternal id sg al => do rl <- alloc_regs map al; @@ -455,39 +496,6 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node) transl_expr map b r nc end. -(** Translation of arguments to annotations. *) - -Definition exprlist_of_expr_list (l: list expr) : exprlist := - List.fold_right Econs Enil l. - -Fixpoint convert_annot_arg {A: Type} (a: annot_arg expr) (rl: list A) : annot_arg A * list A := - match a with - | AA_base a => - match rl with - | r :: rs => (AA_base r, rs) - | nil => (AA_int Int.zero, nil) (**r never happens *) - end - | AA_int n => (AA_int n, rl) - | AA_long n => (AA_long n, rl) - | AA_float n => (AA_float n, rl) - | AA_single n => (AA_single n, rl) - | AA_loadstack chunk ofs => (AA_loadstack chunk ofs, rl) - | AA_addrstack ofs => (AA_addrstack ofs, rl) - | AA_loadglobal chunk id ofs => (AA_loadglobal chunk id ofs, rl) - | AA_addrglobal id ofs => (AA_addrglobal id ofs, rl) - | AA_longofwords hi lo => - let (hi', rl1) := convert_annot_arg hi rl in - let (lo', rl2) := convert_annot_arg lo rl1 in - (AA_longofwords hi' lo', rl2) - end. - -Fixpoint convert_annot_args {A: Type} (al: list (annot_arg expr)) (rl: list A) : list (annot_arg A) := - match al with - | nil => nil - | a1 :: al => - let (a1', rl1) := convert_annot_arg a1 rl in a1' :: convert_annot_args al rl1 - end. - (** Auxiliary for translating exit expressions. *) Definition transl_exit (nexits: list node) (n: nat) : mon node := @@ -586,15 +594,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) do rargs <- alloc_regs map cl; do n1 <- add_instr (Itailcall sig (inr _ id) rargs); transl_exprlist map cl rargs n1 - | Sbuiltin optid ef al => - do rargs <- alloc_regs map al; - do r <- alloc_optreg map optid; - do n1 <- add_instr (Ibuiltin ef rargs r nd); - transl_exprlist map al rargs n1 - | Sannot ef args => - let al := exprlist_of_expr_list (params_of_annot_args args) in + | Sbuiltin res ef args => + let al := exprlist_of_expr_list (params_of_builtin_args args) in do rargs <- alloc_regs map al; - do n1 <- add_instr (Iannot ef (convert_annot_args args rargs) nd); + let args' := convert_builtin_args args rargs in + do res' <- convert_builtin_res map res; + do n1 <- add_instr (Ibuiltin ef args' res' nd); transl_exprlist map al rargs n1 | Sseq s1 s2 => do ns <- transl_stmt map s2 nd nexits ngoto nret rret; -- cgit