Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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).