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. --- cfrontend/Cexec.v | 70 ++++++++++++++++--------------------------------------- 1 file changed, 20 insertions(+), 50 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index aba3c094..16d5823b 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -527,6 +527,10 @@ Definition do_ef_annot_val (text: ident) (targ: typ) | _ => None end. +Definition do_ef_debug (kind: positive) (text: ident) (targs: list typ) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + Some(w, E0, Vundef, m). + Definition do_external (ef: external_function): world -> list val -> mem -> option (world * trace * val * mem) := match ef with @@ -534,14 +538,13 @@ Definition do_external (ef: external_function): | EF_builtin name sg => do_external_function name sg ge | EF_vload chunk => do_ef_volatile_load chunk | EF_vstore chunk => do_ef_volatile_store chunk - | EF_vload_global chunk id ofs => do_ef_volatile_load_global chunk id ofs - | EF_vstore_global chunk id ofs => do_ef_volatile_store_global chunk id ofs | EF_malloc => do_ef_malloc | EF_free => do_ef_free | EF_memcpy sz al => do_ef_memcpy sz al | EF_annot text targs => do_ef_annot text targs | EF_annot_val text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge + | EF_debug kind text targs => do_ef_debug kind text targs end. Lemma do_ef_external_sound: @@ -550,40 +553,21 @@ Lemma do_ef_external_sound: external_call ef ge vargs m t vres m' /\ possible_trace w t w'. Proof with try congruence. intros until m'. - - assert (VLOAD: forall chunk vargs, - do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> - volatile_load_sem chunk ge vargs m t vres m' /\ possible_trace w t w'). - intros chunk vargs'. - unfold do_ef_volatile_load. destruct vargs'... destruct v... destruct vargs'... - mydestr. destruct p as [[w'' t''] v]; mydestr. - exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. - - assert (VSTORE: forall chunk vargs, - do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') -> - volatile_store_sem chunk ge vargs m t vres m' /\ possible_trace w t w'). - intros chunk vargs'. - unfold do_ef_volatile_store. destruct vargs'... destruct v... destruct vargs'... destruct vargs'... - mydestr. destruct p as [[w'' t''] m'']. mydestr. - exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. - destruct ef; simpl. (* EF_external *) eapply do_external_function_sound; eauto. (* EF_builtin *) eapply do_external_function_sound; eauto. (* EF_vload *) + unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... + mydestr. destruct p as [[w'' t''] v]; mydestr. + exploit do_volatile_load_sound; eauto. intuition. econstructor; eauto. auto. (* EF_vstore *) + unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... + mydestr. destruct p as [[w'' t''] m'']. mydestr. + exploit do_volatile_store_sound; eauto. intuition. econstructor; eauto. auto. -(* EF_vload_global *) - rewrite volatile_load_global_charact; simpl. - unfold do_ef_volatile_load_global. destruct (Genv.find_symbol ge)... - intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. -(* EF_vstore_global *) - rewrite volatile_store_global_charact; simpl. - unfold do_ef_volatile_store_global. destruct (Genv.find_symbol ge)... - intros. exploit VSTORE; eauto. intros [A B]. split; auto. exists b; auto. (* EF_malloc *) unfold do_ef_malloc. destruct vargs... destruct v... destruct vargs... destruct (Mem.alloc m (-4) (Int.unsigned i)) as [m1 b] eqn:?. mydestr. @@ -606,6 +590,8 @@ Proof with try congruence. econstructor. constructor; eauto. constructor. (* EF_inline_asm *) eapply do_inline_assembly_sound; eauto. +(* EF_debug *) + unfold do_ef_debug. mydestr. split; constructor. Qed. Lemma do_ef_external_complete: @@ -613,35 +599,17 @@ Lemma do_ef_external_complete: external_call ef ge vargs m t vres m' -> possible_trace w t w' -> do_external ef w vargs m = Some(w', t, vres, m'). Proof. - intros. - - assert (VLOAD: forall chunk vargs, - volatile_load_sem chunk ge vargs m t vres m' -> - do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m')). - intros. inv H1; unfold do_ef_volatile_load. - exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. - - assert (VSTORE: forall chunk vargs, - volatile_store_sem chunk ge vargs m t vres m' -> - do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m')). - intros. inv H1; unfold do_ef_volatile_store. - exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. - - destruct ef; simpl in *. + intros. destruct ef; simpl in *. (* EF_external *) eapply do_external_function_complete; eauto. (* EF_builtin *) eapply do_external_function_complete; eauto. (* EF_vload *) - auto. -(* EF_vstore *) - auto. -(* EF_vload_global *) - rewrite volatile_load_global_charact in H; simpl in H. destruct H as [b [P Q]]. - unfold do_ef_volatile_load_global. rewrite P. auto. + inv H; unfold do_ef_volatile_load. + exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto. (* EF_vstore *) - rewrite volatile_store_global_charact in H; simpl in H. destruct H as [b [P Q]]. - unfold do_ef_volatile_store_global. rewrite P. auto. + inv H; unfold do_ef_volatile_store. + exploit do_volatile_store_complete; eauto. intros EQ; rewrite EQ; auto. (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. rewrite H1. rewrite H2. auto. @@ -660,6 +628,8 @@ Proof. rewrite (eventval_of_val_complete _ _ _ H1). auto. (* EF_inline_asm *) eapply do_inline_assembly_complete; eauto. +(* EF_debug *) + inv H. inv H0. reflexivity. Qed. (** * Reduction of expressions *) -- cgit