From c4877832826fa26aea9c236f16bdc2de16c98150 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 15 Jan 2012 08:57:09 +0000 Subject: Added volatile_read_global and volatile_store_global builtins. Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cexec.v | 90 +++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 71 insertions(+), 19 deletions(-) (limited to 'cfrontend/Cexec.v') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index e3b57c51..4bce5355 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -1270,6 +1270,20 @@ Definition do_ef_volatile_store (chunk: memory_chunk) | _ => None end. +Definition do_ef_volatile_load_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match Genv.find_symbol genv id with + | Some b => do_ef_volatile_load chunk w (Vptr b ofs :: vargs) m + | None => None + end. + +Definition do_ef_volatile_store_global (chunk: memory_chunk) (id: ident) (ofs: int) + (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := + match Genv.find_symbol genv id with + | Some b => do_ef_volatile_store chunk w (Vptr b ofs :: vargs) m + | None => None + end. + Definition do_ef_malloc (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) := match vargs with @@ -1358,6 +1372,8 @@ Definition do_external (ef: external_function): | EF_builtin name sg => do_ef_external name sg | 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 @@ -1389,25 +1405,45 @@ Proof with try congruence. apply val_of_eventval_sound; auto. econstructor. constructor; eauto. constructor. - destruct ef; simpl. -(* EF_external *) - auto. -(* EF_builtin *) - auto. -(* EF_vload *) - unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs... + assert (VLOAD: forall chunk vargs, + do_ef_volatile_load chunk w vargs m = Some (w', t, vres, m') -> + volatile_load_sem chunk genv 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 [res w'']; mydestr. split. constructor. apply Genv.invert_find_symbol; auto. auto. apply val_of_eventval_sound; auto. econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. -(* EF_vstore *) - unfold do_ef_volatile_store. destruct vargs... destruct v... destruct vargs... destruct vargs... + + assert (VSTORE: forall chunk vargs, + do_ef_volatile_store chunk w vargs m = Some (w', t, vres, m') -> + volatile_store_sem chunk genv 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. split. constructor. apply Genv.invert_find_symbol; auto. auto. apply eventval_of_val_sound; auto. econstructor. constructor; eauto. constructor. split. constructor; auto. constructor. + + destruct ef; simpl. +(* EF_external *) + auto. +(* EF_builtin *) + auto. +(* EF_vload *) + auto. +(* EF_vstore *) + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact. + unfold do_ef_volatile_load_global. destruct (Genv.find_symbol genv)... + intros. exploit VLOAD; eauto. intros [A B]. split; auto. exists b; auto. +(* EF_vstore_global *) + rewrite volatile_store_global_charact. + unfold do_ef_volatile_store_global. destruct (Genv.find_symbol genv)... + 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. @@ -1443,23 +1479,39 @@ Proof. unfold do_ef_external. rewrite (list_eventval_of_val_complete _ _ _ H2). rewrite H8. rewrite (val_of_eventval_complete _ _ _ H3). auto. + assert (VLOAD: forall chunk vargs, + volatile_load_sem chunk genv 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. + inv H0. inv H9. inv H7. + rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). rewrite H10. + rewrite (val_of_eventval_complete _ _ _ H4). auto. + inv H0. rewrite H2. rewrite H3. auto. + + assert (VSTORE: forall chunk vargs, + volatile_store_sem chunk genv 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. + inv H0. inv H9. inv H7. + rewrite H3. rewrite (Genv.find_invert_symbol _ _ H2). + rewrite (eventval_of_val_complete _ _ _ H4). rewrite H10. auto. + inv H0. rewrite H2. rewrite H3. auto. + destruct ef; simpl in *. (* EF_external *) auto. (* EF_builtin *) auto. (* EF_vload *) - inv H; unfold do_ef_volatile_load. - inv H0. inv H8. inv H6. - rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). rewrite H9. - rewrite (val_of_eventval_complete _ _ _ H3). auto. - inv H0. rewrite H1. rewrite H2. auto. + auto. (* EF_vstore *) - inv H; unfold do_ef_volatile_store. - inv H0. inv H8. inv H6. - rewrite H2. rewrite (Genv.find_invert_symbol _ _ H1). - rewrite (eventval_of_val_complete _ _ _ H3). rewrite H9. auto. - inv H0. rewrite H1. rewrite H2. auto. + auto. +(* EF_vload_global *) + rewrite volatile_load_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_load_global. rewrite P. auto. +(* EF_vstore *) + rewrite volatile_store_global_charact in H. destruct H as [b [P Q]]. + unfold do_ef_volatile_store_global. rewrite P. auto. (* EF_malloc *) inv H; unfold do_ef_malloc. inv H0. rewrite H1. rewrite H2. auto. -- cgit