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/Selectionproof.v | 93 ++++++++++++++++++++---------------------------- 1 file changed, 38 insertions(+), 55 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d7b1e675..1d2f2b3a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -598,45 +598,47 @@ Proof. exists (v1' :: vl'); split; auto. constructor; eauto. Qed. -Lemma sel_annot_arg_correct: - forall sp e e' m m', +Lemma sel_builtin_arg_correct: + forall sp e e' m m' a v c, env_lessdef e e' -> Mem.extends m m' -> - forall a v, Cminor.eval_expr ge sp e m a v -> exists v', - CminorSel.eval_annot_arg tge sp e' m' (sel_annot_arg a) v' + CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v' /\ Val.lessdef v v'. Proof. - intros until v. functional induction (sel_annot_arg a); intros EV. -- inv EV. simpl in H2; inv H2. econstructor; split. constructor. - unfold Genv.symbol_address. rewrite symbols_preserved. auto. -- inv EV. simpl in H2; inv H2. econstructor; split. constructor. auto. -- inv EV. inv H3. exploit Mem.loadv_extends; eauto. intros (v' & A & B). - exists v'; split; auto. constructor. - replace (Genv.symbol_address tge id ofs) with vaddr; auto. - simpl in H2; inv H2. unfold Genv.symbol_address. rewrite symbols_preserved. auto. -- inv EV. inv H3. simpl in H2; inv H2. exploit Mem.loadv_extends; eauto. intros (v' & A & B). - exists v'; split; auto. constructor; auto. -- exploit sel_expr_correct; eauto. intros (v1 & A & B). - exists v1; split; auto. eapply eval_annot_arg; eauto. -Qed. - -Lemma sel_annot_args_correct: + intros. unfold sel_builtin_arg. + exploit sel_expr_correct; eauto. intros (v1 & A & B). + exists v1; split; auto. + destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c). + apply eval_builtin_arg; eauto. + constructor; auto. +Qed. + +Lemma sel_builtin_args_correct: forall sp e e' m m', env_lessdef e e' -> Mem.extends m m' -> forall al vl, Cminor.eval_exprlist ge sp e m al vl -> + forall cl, exists vl', - list_forall2 (CminorSel.eval_annot_arg tge sp e' m') - (List.map sel_annot_arg al) + list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') + (sel_builtin_args al cl) vl' /\ Val.lessdef_list vl vl'. Proof. - induction 3; simpl. + induction 3; intros; simpl. - exists (@nil val); split; constructor. -- exploit sel_annot_arg_correct; eauto. intros (v1' & A & B). - destruct IHeval_exprlist as (vl' & C & D). - exists (v1' :: vl'); split; auto. constructor; auto. +- exploit sel_builtin_arg_correct; eauto. intros (v1' & A & B). + edestruct IHeval_exprlist as (vl' & C & D). + exists (v1' :: vl'); split; auto. constructor; eauto. +Qed. + +Lemma sel_builtin_res_correct: + forall oid v e v' e', + env_lessdef e e' -> Val.lessdef v v' -> + env_lessdef (set_optvar oid v e) (set_builtin_res (sel_builtin_res oid) v' e'). +Proof. + intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. Qed. (** Semantic preservation for functions and statements. *) @@ -687,10 +689,10 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (LDA: Val.lessdef_list args args') (LDE: env_lessdef e e') (ME: Mem.extends m m') - (EA: eval_exprlist tge sp e' m' nil al args'), + (EA: list_forall2 (CminorSel.eval_builtin_arg tge sp e' m') al args'), match_states (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m) - (State f' (Sbuiltin optid ef al) k' sp e' m') + (State f' (Sbuiltin (sel_builtin_res optid) ef al) k' sp e' m') | match_builtin_2: forall v v' optid f sp e k m f' e' m' k' (TF: sel_function ge f = OK f') (MC: match_cont k k') @@ -699,7 +701,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop := (ME: Mem.extends m m'), match_states (Cminor.Returnstate v (Cminor.Kcall optid f sp e k) m) - (State f' Sskip k' sp (set_optvar optid v' e') m'). + (State f' Sskip k' sp (set_builtin_res (sel_builtin_res optid) v' e') m'). Remark call_cont_commut: forall k k', match_cont k k' -> match_cont (Cminor.call_cont k) (call_cont k'). @@ -724,8 +726,6 @@ Proof. destruct (classify_call ge e); simpl; auto. (* tailcall *) destruct (classify_call ge e); simpl; auto. -(* builtin *) - destruct (builtin_is_annot e); simpl; auto. (* seq *) exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; @@ -790,11 +790,11 @@ Proof. eapply eval_store; eauto. constructor; auto. - (* Scall *) - exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit classify_call_correct; eauto. destruct (classify_call ge a) as [ | id | ef]. + (* indirect *) exploit sel_expr_correct; eauto. intros [vf' [A B]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & U & V). left; econstructor; split. econstructor; eauto. econstructor; eauto. @@ -802,6 +802,7 @@ Proof. constructor; auto. constructor; auto. + (* direct *) intros [b [U V]]. + exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & X & Y). left; econstructor; split. econstructor; eauto. @@ -809,7 +810,8 @@ Proof. apply sig_function_translated; auto. constructor; auto. constructor; auto. + (* turned into Sbuiltin *) - intros EQ. subst fd. + intros EQ. subst fd. + exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. right; split. simpl. omega. split. auto. econstructor; eauto. - (* Stailcall *) @@ -827,32 +829,13 @@ Proof. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) - destruct (builtin_is_annot ef optid) eqn:ISANNOT. -+ (* annotation *) - assert (X: exists text targs, ef = EF_annot text targs). - { destruct ef; try discriminate. econstructor; econstructor; eauto. } - destruct X as (text & targs & EQ). - assert (Y: optid = None). - { destruct ef; try discriminate. destruct optid; try discriminate. auto. } - exploit sel_annot_args_correct; eauto. - intros (vargs' & P & Q). - exploit external_call_mem_extends; eauto. - intros [vres' [m2 [A [B [C D]]]]]. - left; econstructor; split. - econstructor. - rewrite EQ; auto. - eauto. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - rewrite Y. constructor; auto. -+ (* other builtin *) - exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]]. + exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]]. exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. apply set_optvar_lessdef; auto. + constructor; auto. apply sel_builtin_res_correct; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. @@ -942,8 +925,8 @@ Proof. econstructor. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) - right; split. simpl; omega. split. auto. constructor; auto. - destruct optid; simpl; auto. apply set_var_lessdef; auto. + right; split. simpl; omega. split. auto. constructor; auto. + apply sel_builtin_res_correct; auto. Qed. Lemma sel_initial_states: -- cgit