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. --- ia32/Asmgenproof.v | 40 ++++++++++------------------------------ 1 file changed, 10 insertions(+), 30 deletions(-) (limited to 'ia32/Asmgenproof.v') diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 3570da2e..d91e17a2 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -671,53 +671,33 @@ Opaque loadind. rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) - inv AT. monadInv H3. + inv AT. monadInv H4. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H2); intro NOOV. - exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto. + generalize (transf_function_no_overflow _ _ H3); intro NOOV. + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. intros [vres' [m2' [A [B [C D]]]]]. left. econstructor; split. apply plus_one. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. - eapply external_call_symbols_preserved'; eauto. + erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr_nf, nextinstr. rewrite Pregmap.gss. - rewrite undef_regs_other. rewrite set_pregs_other_2. rewrite undef_regs_other_2. - rewrite <- H0. simpl. econstructor; eauto. + rewrite undef_regs_other. rewrite set_res_other. rewrite undef_regs_other_2. + rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. - rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. simpl; intros. intuition congruence. - apply agree_nextinstr_nf. eapply agree_set_mregs; auto. + apply agree_nextinstr_nf. eapply agree_set_res; auto. eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. congruence. -- (* Mannot *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit annot_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. - eapply exec_step_annot. eauto. eauto. - eapply find_instr_tail; eauto. eauto. - erewrite <- sp_val by eauto. - eapply eval_annot_args_preserved with (ge1 := ge); eauto. - exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - eapply match_states_intro with (ep := false); eauto with coqlib. - unfold nextinstr. rewrite Pregmap.gss. - rewrite <- H1; simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - apply agree_nextinstr. auto. - congruence. - - (* Mgoto *) assert (f0 = f) by congruence. subst f0. inv AT. monadInv H4. -- cgit