From 726c815f2070e9ae40bdf6df1d4e63b4a60b6e09 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 18 Nov 2013 10:01:21 +0000 Subject: Revised semantics of external functions, continued: - Also axiomatize the semantics of inline asm - In Cexec, revised parameterization over do_external_function - In Interp.ml, matching changes + suppression of Interp_ext.ml git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2370 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cexec.v | 71 ++++++++++++++++++++++++++++--------------------------- 1 file changed, 36 insertions(+), 35 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 699c29e..36a62a8 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -387,19 +387,33 @@ Qed. (** External calls *) -Parameter do_external_function: ident -> signature -> list val -> mem -> option val. - -Axiom do_external_function_correct: - forall id sg (ge: genv) vargs m t vres m', - external_functions_sem id sg ge vargs m t vres m' <-> - do_external_function id sg vargs m = Some vres /\ t = E0 /\ m' = m. - -Definition do_ef_external (name: ident) (sg: signature) - (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := - match do_external_function name sg vargs m with - | None => None - | Some vres => Some(w, E0, vres, m) - end. +Variable do_external_function: + ident -> signature -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + +Hypothesis do_external_function_sound: + forall id sg ge vargs m t vres m' w w', + do_external_function id sg ge w vargs m = Some(w', t, vres, m') -> + external_functions_sem id sg ge vargs m t vres m' /\ possible_trace w t w'. + +Hypothesis do_external_function_complete: + forall id sg ge vargs m t vres m' w w', + external_functions_sem id sg ge vargs m t vres m' -> + possible_trace w t w' -> + do_external_function id sg ge w vargs m = Some(w', t, vres, m'). + +Variable do_inline_assembly: + ident -> genv -> world -> list val -> mem -> option (world * trace * val * mem). + +Hypothesis do_inline_assembly_sound: + forall txt ge vargs m t vres m' w w', + do_inline_assembly txt ge w vargs m = Some(w', t, vres, m') -> + inline_assembly_sem txt ge vargs m t vres m' /\ possible_trace w t w'. + +Hypothesis do_inline_assembly_complete: + forall txt ge vargs m t vres m' w w', + inline_assembly_sem txt ge vargs m t vres m' -> + possible_trace w t w' -> + do_inline_assembly txt ge w vargs m = Some(w', t, vres, m'). Definition do_ef_volatile_load (chunk: memory_chunk) (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := @@ -508,8 +522,8 @@ Definition do_ef_annot_val (text: ident) (targ: typ) Definition do_external (ef: external_function): world -> list val -> mem -> option (world * trace * val * mem) := match ef with - | EF_external name sg => do_ef_external name sg - | EF_builtin name sg => do_ef_external name sg + | EF_external name sg => do_external_function name sg ge + | 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 @@ -519,7 +533,7 @@ Definition do_external (ef: external_function): | 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 => do_ef_annot text nil + | EF_inline_asm text => do_inline_assembly text ge end. Lemma do_ef_external_sound: @@ -528,11 +542,6 @@ 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 (EXT: forall name sg, - do_ef_external name sg w vargs m = Some(w', t, vres, m') -> - external_functions_sem name sg ge vargs m t vres m' /\ possible_trace w t w'). - intros until sg. unfold do_ef_external. mydestr. - split. rewrite do_external_function_correct. auto. constructor. assert (VLOAD: forall chunk vargs, do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> @@ -552,9 +561,9 @@ Proof with try congruence. destruct ef; simpl. (* EF_external *) - auto. + eapply do_external_function_sound; eauto. (* EF_builtin *) - auto. + eapply do_external_function_sound; eauto. (* EF_vload *) auto. (* EF_vstore *) @@ -588,10 +597,7 @@ Proof with try congruence. split. constructor. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. (* EF_inline_asm *) - unfold do_ef_annot. destruct vargs; simpl... mydestr. - split. change (Event_annot text nil) with (Event_annot text (annot_eventvals nil nil)). - constructor. constructor. - econstructor. constructor; eauto. constructor. + eapply do_inline_assembly_sound; eauto. Qed. Lemma do_ef_external_complete: @@ -600,11 +606,6 @@ Lemma do_ef_external_complete: do_external ef w vargs m = Some(w', t, vres, m'). Proof. intros. - assert (EXT: forall name sg, - external_functions_sem name sg ge vargs m t vres m' -> - do_ef_external name sg w vargs m = Some (w', t, vres, m')). - intros. rewrite do_external_function_correct in H1. destruct H1 as (A & B & C). - subst. unfold do_ef_external. rewrite A. inv H0. auto. assert (VLOAD: forall chunk vargs, volatile_load_sem chunk ge vargs m t vres m' -> @@ -620,9 +621,9 @@ Proof. destruct ef; simpl in *. (* EF_external *) - auto. + eapply do_external_function_complete; eauto. (* EF_builtin *) - auto. + eapply do_external_function_complete; eauto. (* EF_vload *) auto. (* EF_vstore *) @@ -650,7 +651,7 @@ Proof. inv H; unfold do_ef_annot_val. inv H0. inv H6. inv H4. rewrite (eventval_of_val_complete _ _ _ H1). auto. (* EF_inline_asm *) - inv H; unfold do_ef_annot. inv H0. inv H6. inv H4. inv H1. simpl. auto. + eapply do_inline_assembly_complete; eauto. Qed. (** * Reduction of expressions *) -- cgit v1.2.3