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/RTLgenspec.v | 41 +++++++++++++++++++++++++++-------------- 1 file changed, 27 insertions(+), 14 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 1ca9faa0..41b5016f 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -727,7 +727,7 @@ Inductive tr_expr (c: code): tr_expr c map pr (Eletvar n) ns nd rd dst | tr_Ebuiltin: forall map pr ef al ns nd rd dst n1 rl, tr_exprlist c map pr al ns n1 rl -> - c!n1 = Some (Ibuiltin ef rl rd nd) -> + c!n1 = Some (Ibuiltin ef (List.map (@BA reg) rl) (BR rd) nd) -> reg_map_ok map rd dst -> ~In rd pr -> tr_expr c map pr (Ebuiltin ef al) ns nd rd dst | tr_Eexternal: forall map pr id sg al ns nd rd dst n1 rl, @@ -807,6 +807,15 @@ Inductive tr_exitexpr (c: code): tr_exitexpr c (add_letvar map r) b n1 nexits -> tr_exitexpr c map (XElet a b) ns nexits. +(** Auxiliary for the compilation of [builtin] statements. *) + +Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Prop := + | tr_builtin_res_var: forall map id r, + map.(map_vars)!id = Some r -> + tr_builtin_res map (BR id) (BR r) + | tr_builtin_res_none: forall map, + tr_builtin_res map BR_none BR_none. + (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c], starting at node [ns], contains instructions that perform the Cminor statement [stmt]. These instructions branch to node [ncont] if @@ -849,15 +858,11 @@ Inductive tr_stmt (c: code) (map: mapping): tr_exprlist c map nil cl ns n2 rargs -> c!n2 = Some (Itailcall sig (inr _ id) rargs) -> tr_stmt c map (Stailcall sig (inr _ id) cl) ns nd nexits ngoto nret rret - | tr_Sbuiltin: forall optid ef al ns nd nexits ngoto nret rret rd n1 rargs, - tr_exprlist c map nil al ns n1 rargs -> - c!n1 = Some (Ibuiltin ef rargs rd nd) -> - reg_map_ok map rd optid -> - tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret - | tr_Sannot: forall ef al ns nd nexits ngoto nret rret n1 rargs, - tr_exprlist c map nil (exprlist_of_expr_list (params_of_annot_args al)) ns n1 rargs -> - c!n1 = Some (Iannot ef (convert_annot_args al rargs) nd) -> - tr_stmt c map (Sannot ef al) ns nd nexits ngoto nret rret + | tr_Sbuiltin: forall res ef args ns nd nexits ngoto nret rret res' n1 rargs, + tr_exprlist c map nil (exprlist_of_expr_list (params_of_builtin_args args)) ns n1 rargs -> + c!n1 = Some (Ibuiltin ef (convert_builtin_args args rargs) res' nd) -> + tr_builtin_res map res res' -> + tr_stmt c map (Sbuiltin res ef args) ns nd nexits ngoto nret rret | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, tr_stmt c map s2 n nd nexits ngoto nret rret -> tr_stmt c map s1 ns n nexits ngoto nret rret -> @@ -1208,6 +1213,17 @@ Proof. apply add_letvar_valid; eauto with rtlg. Qed. +Lemma convert_builtin_res_charact: + forall map res s res' s' INCR + (TR: convert_builtin_res map res s = OK res' s' INCR) + (WF: map_valid map s), + tr_builtin_res map res res'. +Proof. + destruct res; simpl; intros; monadInv TR. +- constructor. unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto. +- constructor. +Qed. + Lemma transl_stmt_charact: forall map stmt nd nexits ngoto nret rret s ns s' INCR (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR) @@ -1260,10 +1276,7 @@ Proof. (* Sbuiltin *) econstructor; eauto 4 with rtlg. eapply transl_exprlist_charact; eauto 3 with rtlg. - eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg. - (* Sannot *) - econstructor; eauto 4 with rtlg. - eapply transl_exprlist_charact; eauto 3 with rtlg. + eapply convert_builtin_res_charact; eauto with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. -- cgit