diff options
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 755 |
1 files changed, 626 insertions, 129 deletions
diff --git a/common/Events.v b/common/Events.v index 855c013..ad1fc51 100644 --- a/common/Events.v +++ b/common/Events.v @@ -13,34 +13,44 @@ (* *) (* *********************************************************************) -(** Representation of observable events and execution traces. *) +(** Observable events, execution traces, and semantics of external calls. *) Require Import Coqlib. +Require Intv. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. +Require Import Memory. + +(** * Events and traces *) (** The observable behaviour of programs is stated in terms of - input/output events, which can also be thought of as system calls - to the operating system. An event is generated each time an - external function (see module AST) is invoked. The event records - the name of the external function, the arguments to the function - invocation provided by the program, and the return value provided by - the outside world (e.g. the operating system). Arguments and values - are either integers or floating-point numbers. We currently do not - allow pointers to be exchanged between the program and the outside - world. *) + input/output events, which represent the actions of the program + that the external world can observe. CompCert leaves much flexibility as to + the exact content of events: the only requirement is that they + do not expose pointer values nor memory states, because these + are not preserved literally during compilation. For concreteness, + we use the following type for events. Each event represents either: + +- A system call (e.g. an input/output operation), recording the + name of the system call, its int-or-float parameters, + and its int-or-float result. + +- A volatile load from a memory location, recording a label + associated with the read (e.g. a global variable name or a source code position). + +- A volatile store to a memory location, also recording a label. +*) Inductive eventval: Type := | EVint: int -> eventval | EVfloat: float -> eventval. -Record event : Type := mkevent { - ev_name: ident; - ev_args: list eventval; - ev_res: eventval -}. +Inductive event: Type := + | Event_syscall: ident -> list eventval -> eventval -> event + | Event_load: ident -> event + | Event_store: ident -> event. (** The dynamic semantics for programs collect traces of events. Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *) @@ -49,10 +59,6 @@ Definition trace := list event. Definition E0 : trace := nil. -Definition Eextcall - (name: ident) (args: list eventval) (res: eventval) : trace := - mkevent name args res :: nil. - Definition Eapp (t1 t2: trace) : trace := t1 ++ t2. CoInductive traceinf : Type := @@ -93,7 +99,7 @@ Qed. Hint Rewrite E0_left E0_right Eapp_assoc E0_left_inf Eappinf_assoc: trace_rewrite. -Opaque trace E0 Eextcall Eapp Eappinf. +Opaque trace E0 Eapp Eappinf. (** The following [traceEq] tactic proves equalities between traces or infinite traces. *) @@ -115,115 +121,6 @@ Ltac decomposeTraceEq := Ltac traceEq := repeat substTraceHyp; autorewrite with trace_rewrite; decomposeTraceEq. -(** The predicate [event_match ef vargs t vres] expresses that - the event [t] is generated when invoking external function [ef] - with arguments [vargs], and obtaining [vres] as a return value - from the operating system. *) - -Inductive eventval_match: eventval -> typ -> val -> Prop := - | ev_match_int: - forall i, eventval_match (EVint i) Tint (Vint i) - | ev_match_float: - forall f, eventval_match (EVfloat f) Tfloat (Vfloat f). - -Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop := - | evl_match_nil: - eventval_list_match nil nil nil - | evl_match_cons: - forall ev1 evl ty1 tyl v1 vl, - eventval_match ev1 ty1 v1 -> - eventval_list_match evl tyl vl -> - eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl). - -Inductive event_match: - external_function -> list val -> trace -> val -> Prop := - event_match_intro: - forall ef vargs vres eargs eres, - eventval_list_match eargs (sig_args ef.(ef_sig)) vargs -> - eventval_match eres (proj_sig_res ef.(ef_sig)) vres -> - event_match ef vargs (Eextcall ef.(ef_id) eargs eres) vres. - -(** The following section shows that [event_match] is stable under - relocation of pointer values, as performed by memory injections - (see module [Mem]). *) - -Require Import Mem. - -Section EVENT_MATCH_INJECT. - -Variable f: meminj. - -Remark eventval_match_inject: - forall ev ty v1, eventval_match ev ty v1 -> - forall v2, val_inject f v1 v2 -> - eventval_match ev ty v2. -Proof. - induction 1; intros; inversion H; constructor. -Qed. - -Remark eventval_list_match_inject: - forall evl tyl vl1, eventval_list_match evl tyl vl1 -> - forall vl2, val_list_inject f vl1 vl2 -> - eventval_list_match evl tyl vl2. -Proof. - induction 1; intros. - inversion H; constructor. - inversion H1; constructor. - eapply eventval_match_inject; eauto. - eauto. -Qed. - -Lemma event_match_inject: - forall ef args1 t res args2, - event_match ef args1 t res -> - val_list_inject f args1 args2 -> - event_match ef args2 t res /\ val_inject f res res. -Proof. - intros. inversion H; subst. - split. constructor. eapply eventval_list_match_inject; eauto. auto. - inversion H2; constructor. -Qed. - -End EVENT_MATCH_INJECT. - -(** The following section shows that [event_match] is stable under - replacement of [Vundef] values by more defined values. *) - -Section EVENT_MATCH_LESSDEF. - -Remark eventval_match_lessdef: - forall ev ty v1, eventval_match ev ty v1 -> - forall v2, Val.lessdef v1 v2 -> - eventval_match ev ty v2. -Proof. - induction 1; intros; inv H; constructor. -Qed. - -Remark eventval_list_match_moredef: - forall evl tyl vl1, eventval_list_match evl tyl vl1 -> - forall vl2, Val.lessdef_list vl1 vl2 -> - eventval_list_match evl tyl vl2. -Proof. - induction 1; intros. - inversion H; constructor. - inversion H1; constructor. - eapply eventval_match_lessdef; eauto. - eauto. -Qed. - -Lemma event_match_lessdef: - forall ef args1 t res1 args2, - event_match ef args1 t res1 -> - Val.lessdef_list args1 args2 -> - exists res2, event_match ef args2 t res2 /\ Val.lessdef res1 res2. -Proof. - intros. inversion H; subst. exists res1; split. - constructor. eapply eventval_list_match_moredef; eauto. auto. - auto. -Qed. - -End EVENT_MATCH_LESSDEF. - (** Bisimilarity between infinite traces. *) CoInductive traceinf_sim: traceinf -> traceinf -> Prop := @@ -251,6 +148,23 @@ Proof. cofix COINDHYP;intros. inv H; inv H0; constructor; eauto. Qed. +CoInductive traceinf_sim': traceinf -> traceinf -> Prop := + | traceinf_sim'_cons: forall t T1 T2, + t <> E0 -> traceinf_sim' T1 T2 -> traceinf_sim' (t *** T1) (t *** T2). + +Lemma traceinf_sim'_sim: + forall T1 T2, traceinf_sim' T1 T2 -> traceinf_sim T1 T2. +Proof. + cofix COINDHYP; intros. inv H. + destruct t. elim H0; auto. +Transparent Eappinf. +Transparent E0. + simpl. + destruct t. simpl. constructor. apply COINDHYP; auto. + constructor. apply COINDHYP. + constructor. unfold E0; congruence. auto. +Qed. + (** The "is prefix of" relation between a finite and an infinite trace. *) Inductive traceinf_prefix: trace -> traceinf -> Prop := @@ -321,3 +235,586 @@ Proof. Transparent Eappinf. simpl. f_equal. apply IHt. Qed. + +(** * Semantics of external functions *) + +(** Each external function is of one of the following kinds: *) + +Inductive extfun_kind: signature -> Type := + | EF_syscall (sg: signature) (name: ident): extfun_kind sg + (** A system call. Takes integer-or-float arguments, produces a + result that is an integer or a float, does not modify + the memory, and produces an [Event_syscall] event in the trace. *) + | EF_load (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: nil) (Some (type_of_chunk chunk))) + (** A volatile read operation. Reads and returns the given memory + chunk from the address given as first argument. + Produces an [Event_load] event containing the given label. *) + | EF_store (label: ident) (chunk: memory_chunk): extfun_kind (mksignature (Tint :: type_of_chunk chunk :: nil) None) + (** A volatile store operation. Store the value given as second + argument at the address given as first argument, using the + given memory chunk. + Produces an [Event_store] event containing the given label. *) + | EF_malloc: extfun_kind (mksignature (Tint :: nil) (Some Tint)) + (** Dynamic memory allocation. Takes the requested size in bytes + as argument; returns a pointer to a fresh block of the given size. + Produces no observable event. *) + | EF_free: extfun_kind (mksignature (Tint :: nil) None). + (** Dynamic memory deallocation. Takes a pointer to a block + allocated by an [EF_malloc] external call and frees the + corresponding block. + Produces no observable event. *) + +Parameter classify_external_function: + forall (ef: external_function), extfun_kind (ef.(ef_sig)). + +(** For each external function, its behavior is defined by a predicate relating: +- the values of the arguments passed to this function +- the memory state before the call +- the result value of the call +- the memory state after the call +- the trace generated by the call (can be empty). + +We now specify the expected properties of this predicate. +*) + +Definition mem_unchanged_on (P: block -> Z -> Prop) (m_before m_after: mem): Prop := + (forall b ofs p, + P b ofs -> Mem.perm m_before b ofs p -> Mem.perm m_after b ofs p) +/\(forall chunk b ofs v, + (forall i, ofs <= i < ofs + size_chunk chunk -> P b i) -> + Mem.load chunk m_before b ofs = Some v -> + Mem.load chunk m_after b ofs = Some v). + +Definition loc_out_of_bounds (m: mem) (b: block) (ofs: Z) : Prop := + ofs < Mem.low_bound m b \/ ofs > Mem.high_bound m b. + +Definition loc_unmapped (f: meminj) (b: block) (ofs: Z): Prop := + f b = None. + +Definition loc_out_of_reach (f: meminj) (m: mem) (b: block) (ofs: Z): Prop := + forall b0 delta, + f b0 = Some(b, delta) -> + ofs < Mem.low_bound m b0 + delta \/ ofs >= Mem.high_bound m b0 + delta. + +Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := + forall b1 b2 delta, + f b1 = None -> f' b1 = Some(b2, delta) -> + ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. + +Fixpoint matching_traces (t1 t2: trace) {struct t1} : Prop := + match t1, t2 with + | Event_syscall name1 args1 res1 :: t1', Event_syscall name2 args2 res2 :: t2' => + name1 = name2 -> args1 = args2 -> res1 = res2 /\ matching_traces t1' t2' + | Event_load name1 :: t1', Event_load name2 :: t2' => + name1 = name2 -> matching_traces t1' t2' + | Event_store name1 :: t1', Event_store name2 :: t2' => + name1 = name2 -> matching_traces t1' t2' + | _, _ => + True + end. + +Record extcall_properties (sem: list val -> mem -> trace -> val -> mem -> Prop) + (sg: signature) : Prop := mk_extcall_properties { + +(** The return value of an external call must agree with its signature. *) + ec_well_typed: + forall vargs m1 t vres m2, + sem vargs m1 t vres m2 -> + Val.has_type vres (proj_sig_res sg); + +(** The number of arguments of an external call must agree with its signature. *) + ec_arity: + forall vargs m1 t vres m2, + sem vargs m1 t vres m2 -> + List.length vargs = List.length sg.(sig_args); + +(** External calls cannot invalidate memory blocks. (Remember that + freeing a block does not invalidate its block identifier.) *) + ec_valid_block: + forall vargs m1 t vres m2 b, + sem vargs m1 t vres m2 -> + Mem.valid_block m1 b -> Mem.valid_block m2 b; + +(** External calls preserve the bounds of valid blocks. *) + ec_bounds: + forall vargs m1 t vres m2 b, + sem vargs m1 t vres m2 -> + Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b; + +(** External calls must commute with memory extensions, in the + following sense. *) + ec_mem_extends: + forall vargs m1 t vres m2 m1' vargs', + sem vargs m1 t vres m2 -> + Mem.extends m1 m1' -> + Val.lessdef_list vargs vargs' -> + exists vres', exists m2', + sem vargs' m1' t vres' m2' + /\ Val.lessdef vres vres' + /\ Mem.extends m2 m2' + /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'; + +(** External calls must commute with memory injections, + in the following sense. *) + ec_mem_inject: + forall vargs m1 t vres m2 f m1' vargs', + sem vargs m1 t vres m2 -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f', exists vres', exists m2', + sem vargs' m1' t vres' m2' + /\ val_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ mem_unchanged_on (loc_unmapped f) m1 m2 + /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'; + +(** External calls must be internally deterministic: + if the observable traces match, the return states must be + identical. *) + ec_determ: + forall vargs m t1 vres1 m1 t2 vres2 m2, + sem vargs m t1 vres1 m1 -> sem vargs m t2 vres2 m2 -> + matching_traces t1 t2 -> t1 = t2 /\ vres1 = vres2 /\ m1 = m2 +}. + +(** ** Semantics of volatile loads *) + +Inductive extcall_load_sem (label: ident) (chunk: memory_chunk): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_load_sem_intro: forall b ofs m vres, + Mem.load chunk m b (Int.signed ofs) = Some vres -> + extcall_load_sem label chunk (Vptr b ofs :: nil) m (Event_load label :: nil) vres m. + +Lemma extcall_load_ok: + forall label chunk, + extcall_properties (extcall_load_sem label chunk) + (mksignature (Tint :: nil) (Some (type_of_chunk chunk))). +Proof. + intros; constructor; intros. + + inv H. unfold proj_sig_res. simpl. eapply Mem.load_type; eauto. + + inv H. simpl. auto. + + inv H. auto. + + inv H. auto. + + inv H. inv H1. inv H6. inv H4. + exploit Mem.load_extends; eauto. intros [v2 [A B]]. + exists v2; exists m1'; intuition. + constructor; auto. + red. auto. + + inv H. inv H1. inv H6. + assert (Mem.loadv chunk m2 (Vptr b ofs) = Some vres). auto. + exploit Mem.loadv_inject; eauto. intros [v2 [A B]]. + inv H4. + exists f; exists v2; exists m1'; intuition. + constructor. auto. + red; auto. + red; auto. + red; intros. congruence. + + inv H; inv H0. intuition congruence. +Qed. + +(** ** Semantics of volatile stores *) + +Inductive extcall_store_sem (label: ident) (chunk: memory_chunk): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_store_sem_intro: forall b ofs v m m', + Mem.store chunk m b (Int.signed ofs) v = Some m' -> + extcall_store_sem label chunk (Vptr b ofs :: v :: nil) m (Event_store label :: nil) Vundef m'. + +Lemma extcall_store_ok: + forall label chunk, + extcall_properties (extcall_store_sem label chunk) + (mksignature (Tint :: type_of_chunk chunk :: nil) None). +Proof. + intros; constructor; intros. + + inv H. unfold proj_sig_res. simpl. auto. + + inv H. simpl. auto. + + inv H. eauto with mem. + + inv H. eapply Mem.bounds_store; eauto. + + inv H. inv H1. inv H6. inv H7. inv H4. + exploit Mem.store_within_extends; eauto. intros [m' [A B]]. + exists Vundef; exists m'; intuition. + constructor; auto. + red; split; intros. + eapply Mem.perm_store_1; eauto. + rewrite <- H1. eapply Mem.load_store_other; eauto. + destruct (eq_block b0 b); auto. subst b0; right. + exploit Mem.valid_access_in_bounds. + eapply Mem.store_valid_access_3. eexact H2. + intros [C D]. + generalize (size_chunk_pos chunk0). intro E. + generalize (size_chunk_pos chunk). intro F. + apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) + (Int.signed ofs, Int.signed ofs + size_chunk chunk)). + red; intros. generalize (H x H4). unfold loc_out_of_bounds, Intv.In; simpl. omega. + simpl; omega. simpl; omega. + + inv H. inv H1. inv H6. inv H7. + assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. + exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. + inv H4. + exists f; exists Vundef; exists m2'; intuition. + constructor; auto. + split; intros. eapply Mem.perm_store_1; eauto. + rewrite <- H4. eapply Mem.load_store_other; eauto. + left. exploit (H1 ofs0). generalize (size_chunk_pos chunk0). omega. + unfold loc_unmapped. congruence. + split; intros. eapply Mem.perm_store_1; eauto. + rewrite <- H4. eapply Mem.load_store_other; eauto. + destruct (eq_block b0 b2); auto. subst b0; right. + assert (EQ: Int.signed (Int.add ofs (Int.repr delta)) = Int.signed ofs + delta). + eapply Mem.address_inject; eauto with mem. + simpl in A. rewrite EQ in A. rewrite EQ. + exploit Mem.valid_access_in_bounds. + eapply Mem.store_valid_access_3. eexact H2. + intros [C D]. + generalize (size_chunk_pos chunk0). intro E. + generalize (size_chunk_pos chunk). intro F. + apply (Intv.range_disjoint' (ofs0, ofs0 + size_chunk chunk0) + (Int.signed ofs + delta, Int.signed ofs + delta + size_chunk chunk)). + red; intros. exploit (H1 x H5). eauto. unfold Intv.In; simpl. omega. + simpl; omega. simpl; omega. + + red; intros. congruence. + + inv H; inv H0. intuition congruence. +Qed. + +(** ** Semantics of dynamic memory allocation (malloc) *) + +Inductive extcall_malloc_sem: + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_malloc_sem_intro: forall n m m' b m'', + Mem.alloc m (-4) (Int.signed n) = (m', b) -> + Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> + extcall_malloc_sem (Vint n :: nil) m E0 (Vptr b Int.zero) m''. + +Lemma extcall_malloc_ok: + extcall_properties extcall_malloc_sem + (mksignature (Tint :: nil) (Some Tint)). +Proof. + assert (UNCHANGED: + forall (P: block -> Z -> Prop) m n m' b m'', + Mem.alloc m (-4) (Int.signed n) = (m', b) -> + Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> + mem_unchanged_on P m m''). + intros; split; intros. + eauto with mem. + transitivity (Mem.load chunk m' b0 ofs). + eapply Mem.load_store_other; eauto. left. + apply Mem.valid_not_valid_diff with m; eauto with mem. + eapply Mem.load_alloc_other; eauto. + + constructor; intros. + + inv H. unfold proj_sig_res; simpl. auto. + + inv H. auto. + + inv H. eauto with mem. + + inv H. transitivity (Mem.bounds m' b). + eapply Mem.bounds_store; eauto. + eapply Mem.bounds_alloc_other; eauto. + apply Mem.valid_not_valid_diff with m1; eauto with mem. + + inv H. inv H1. inv H5. inv H7. + exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + intros [m3' [A B]]. + exploit Mem.store_within_extends. eexact B. eauto. + instantiate (1 := Vint n). auto. + intros [m2' [C D]]. + exists (Vptr b Int.zero); exists m2'; intuition. + econstructor; eauto. + eapply UNCHANGED; eauto. + + inv H. inv H1. inv H5. inv H7. + exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. + intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. + exploit Mem.store_mapped_inject. eexact A. eauto. eauto. + instantiate (1 := Vint n). auto. + intros [m2' [E F]]. + exists f'; exists (Vptr b' Int.zero); exists m2'; intuition. + econstructor; eauto. + econstructor. eauto. auto. + eapply UNCHANGED; eauto. + eapply UNCHANGED; eauto. + red; intros. destruct (eq_block b1 b). + subst b1. rewrite C in H1. inv H1. eauto with mem. + rewrite D in H1. congruence. auto. + + inv H; inv H0. intuition congruence. +Qed. + +(** ** Semantics of dynamic memory deallocation (free) *) + +Inductive extcall_free_sem: + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_free_sem_intro: forall b lo sz m m', + Mem.load Mint32 m b (Int.signed lo - 4) = Some (Vint sz) -> + Int.signed sz > 0 -> + Mem.free m b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) = Some m' -> + extcall_free_sem (Vptr b lo :: nil) m E0 Vundef m'. + +Lemma extcall_free_ok: + extcall_properties extcall_free_sem + (mksignature (Tint :: nil) None). +Proof. + assert (UNCHANGED: + forall (P: block -> Z -> Prop) m b lo hi m', + Mem.free m b lo hi = Some m' -> + lo < hi -> + (forall b' ofs, P b' ofs -> b' <> b \/ ofs < lo \/ hi <= ofs) -> + mem_unchanged_on P m m'). + intros; split; intros. + eapply Mem.perm_free_1; eauto. + rewrite <- H3. eapply Mem.load_free; eauto. + destruct (eq_block b0 b); auto. right. right. + apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) (lo, hi)). + red; intros. apply Intv.notin_range. simpl. exploit H1; eauto. intuition. + simpl; generalize (size_chunk_pos chunk); omega. + simpl; omega. + + constructor; intros. + + inv H. unfold proj_sig_res. simpl. auto. + + inv H. auto. + + inv H. eauto with mem. + + inv H. eapply Mem.bounds_free; eauto. + + inv H. inv H1. inv H8. inv H6. + exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. + exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. + exists Vundef; exists m2'; intuition. + econstructor; eauto. + eapply UNCHANGED; eauto. omega. + intros. destruct (eq_block b' b); auto. subst b; right. + red in H. + exploit Mem.range_perm_in_bounds. + eapply Mem.free_range_perm. eexact H4. omega. omega. + + inv H. inv H1. inv H8. inv H6. + exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. + assert (Mem.range_perm m1 b (Int.signed lo - 4) (Int.signed lo + Int.signed sz) Freeable). + eapply Mem.free_range_perm; eauto. + exploit Mem.address_inject; eauto. + apply Mem.perm_implies with Freeable; auto with mem. + apply H. instantiate (1 := lo). omega. + intro EQ. + assert (Mem.range_perm m1' b2 (Int.signed lo + delta - 4) (Int.signed lo + delta + Int.signed sz) Freeable). + red; intros. + replace ofs with ((ofs - delta) + delta) by omega. + eapply Mem.perm_inject; eauto. apply H. omega. + destruct (Mem.range_perm_free _ _ _ _ H1) as [m2' FREE]. + exists f; exists Vundef; exists m2'; intuition. + + econstructor. + rewrite EQ. replace (Int.signed lo + delta - 4) with (Int.signed lo - 4 + delta) by omega. + eauto. auto. + rewrite EQ. auto. + + assert (Mem.free_list m1 ((b, Int.signed lo - 4, Int.signed lo + Int.signed sz) :: nil) = Some m2). + simpl. rewrite H4. auto. + eapply Mem.free_inject; eauto. + intros. destruct (eq_block b b1). + subst b. assert (delta0 = delta) by congruence. subst delta0. + exists (Int.signed lo - 4); exists (Int.signed lo + Int.signed sz); split. + simpl; auto. omega. + elimtype False. + exploit Mem.inject_no_overlap. eauto. eauto. eauto. eauto. + instantiate (1 := ofs + delta0 - delta). + apply Mem.perm_implies with Freeable; auto with mem. + apply H. omega. eauto with mem. + unfold block; omega. + + eapply UNCHANGED; eauto. omega. intros. + red in H6. left. congruence. + + eapply UNCHANGED; eauto. omega. intros. + destruct (eq_block b' b2); auto. subst b'. right. + red in H6. generalize (H6 _ _ H5). intros. + exploit Mem.range_perm_in_bounds. eexact H. omega. intros. omega. + + red; intros. congruence. + + inv H; inv H0. intuition congruence. +Qed. + +(** ** Semantics of system calls. *) + +Inductive eventval_match: eventval -> typ -> val -> Prop := + | ev_match_int: + forall i, eventval_match (EVint i) Tint (Vint i) + | ev_match_float: + forall f, eventval_match (EVfloat f) Tfloat (Vfloat f). + +Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop := + | evl_match_nil: + eventval_list_match nil nil nil + | evl_match_cons: + forall ev1 evl ty1 tyl v1 vl, + eventval_match ev1 ty1 v1 -> + eventval_list_match evl tyl vl -> + eventval_list_match (ev1::evl) (ty1::tyl) (v1::vl). + +Inductive extcall_io_sem (name: ident) (sg: signature): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_io_sem_intro: forall vargs m args res vres, + eventval_list_match args (sig_args sg) vargs -> + eventval_match res (proj_sig_res sg) vres -> + extcall_io_sem name sg vargs m (Event_syscall name args res :: E0) vres m. + +Remark eventval_match_lessdef: + forall ev ty v1 v2, + eventval_match ev ty v1 -> Val.lessdef v1 v2 -> eventval_match ev ty v2. +Proof. + intros. inv H; inv H0; constructor. +Qed. + +Remark eventval_list_match_lessdef: + forall evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, Val.lessdef_list vl1 vl2 -> eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto. +Qed. + +Remark eventval_match_inject: + forall f ev ty v1 v2, + eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. +Proof. + intros. inv H; inv H0; constructor. +Qed. + +Remark eventval_match_inject_2: + forall f ev ty v, + eventval_match ev ty v -> val_inject f v v. +Proof. + induction 1; constructor. +Qed. + +Remark eventval_list_match_inject: + forall f evl tyl vl1, eventval_list_match evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_inject; eauto. eauto. +Qed. + +Remark eventval_list_match_length: + forall evl tyl vl, eventval_list_match evl tyl vl -> List.length vl = List.length tyl. +Proof. + induction 1; simpl; eauto. +Qed. + +Remark eventval_match_determ_1: + forall ev ty v1 v2, eventval_match ev ty v1 -> eventval_match ev ty v2 -> v1 = v2. +Proof. + intros. inv H; inv H0; auto. +Qed. + +Remark eventval_match_determ_2: + forall ev1 ev2 ty v, eventval_match ev1 ty v -> eventval_match ev2 ty v -> ev1 = ev2. +Proof. + intros. inv H; inv H0; auto. +Qed. + +Remark eventval_list_match_determ_2: + forall evl1 tyl vl, eventval_list_match evl1 tyl vl -> + forall evl2, eventval_list_match evl2 tyl vl -> evl1 = evl2. +Proof. + induction 1; intros. inv H. auto. inv H1. f_equal; eauto. + eapply eventval_match_determ_2; eauto. +Qed. + +Lemma extcall_io_ok: + forall name sg, + extcall_properties (extcall_io_sem name sg) sg. +Proof. + intros; constructor; intros. + + inv H. inv H1; constructor. + + inv H. eapply eventval_list_match_length; eauto. + + inv H; auto. + + inv H; auto. + + inv H. + exists vres; exists m1'; intuition. + econstructor; eauto. eapply eventval_list_match_lessdef; eauto. + red; auto. + + inv H. + exists f; exists vres; exists m1'; intuition. + econstructor; eauto. eapply eventval_list_match_inject; eauto. + eapply eventval_match_inject_2; eauto. + red; auto. + red; auto. + red; intros; congruence. + + inv H; inv H0. simpl in H1. + assert (args = args0) by (eapply eventval_list_match_determ_2; eauto). + destruct H1; auto. subst. + intuition. eapply eventval_match_determ_1; eauto. +Qed. + +(** ** Combined semantics of external calls *) + +(** Combining the semantics given above for the various kinds of external calls, + we define the predicate [external_call] that relates: +- the external function being invoked +- the values of the arguments passed to this function +- the memory state before the call +- the result value of the call +- the memory state after the call +- the trace generated by the call (can be empty). + +This predicate is used in the semantics of all CompCert languages. *) + +Definition external_call (ef: external_function): + list val -> mem -> trace -> val -> mem -> Prop := + match classify_external_function ef with + | EF_syscall sg name => extcall_io_sem name sg + | EF_load label chunk => extcall_load_sem label chunk + | EF_store label chunk => extcall_store_sem label chunk + | EF_malloc => extcall_malloc_sem + | EF_free => extcall_free_sem + end. + +Theorem external_call_spec: + forall ef, + extcall_properties (external_call ef) (ef.(ef_sig)). +Proof. + intros. unfold external_call. destruct (classify_external_function ef). + apply extcall_io_ok. + apply extcall_load_ok. + apply extcall_store_ok. + apply extcall_malloc_ok. + apply extcall_free_ok. +Qed. + +Definition external_call_well_typed ef := ec_well_typed _ _ (external_call_spec ef). +Definition external_call_arity ef := ec_arity _ _ (external_call_spec ef). +Definition external_call_valid_block ef := ec_valid_block _ _ (external_call_spec ef). +Definition external_call_bounds ef := ec_bounds _ _ (external_call_spec ef). +Definition external_call_mem_extends ef := ec_mem_extends _ _ (external_call_spec ef). +Definition external_call_mem_inject ef := ec_mem_inject _ _ (external_call_spec ef). +Definition external_call_determ ef := ec_determ _ _ (external_call_spec ef). |