Merge branch 'v3.7-velus' of github.com:inria-parkas/CompCert into kvx-work-velus

11 files changed, 368 insertions, 140 deletions

diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v
index 462d83ad..8e91f14b 100644
--- a/arm/Stacklayout.v
+++ b/arm/Stacklayout.v
@@ -64,7 +64,7 @@ Lemma frame_env_separated:
        ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe))
        ** P.
 Proof.
-Local Opaque Z.add Z.mul sepconj range.
+Local Opaque Z.add Z.mul sepconj range'.
   intros; simpl.
   set (olink := 4 * b.(bound_outgoing));
   set (ora := olink + 4);
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index d3fcdb91..1ede0194 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -149,7 +149,7 @@ Lemma contains_get_stack:
 Proof.
   intros. unfold load_stack.
   replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
-  eapply loadv_rule; eauto.
+  eapply loadv_rule; eauto using perm_F_any.
   simpl. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
@@ -171,7 +171,7 @@ Lemma contains_set_stack:
 Proof.
   intros. unfold store_stack.
   replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
-  eapply storev_rule; eauto.
+  eapply storev_rule; eauto using perm_F_any.
   simpl. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
@@ -936,7 +936,7 @@ Local Opaque mreg_type.
   apply range_drop_left with (mid := pos1) in SEP; [ | omega ].
   apply range_split with (mid := pos1 + sz) in SEP; [ | omega ].
   unfold sz at 1 in SEP. rewrite <- size_type_chunk in SEP.
-  apply range_contains in SEP; auto.
+  apply range_contains in SEP; auto with mem.
   exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)).
   eexact SEP.
   apply load_result_inject; auto. apply wt_ls.
@@ -1087,14 +1087,14 @@ Local Opaque b fe.
   apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto.
   (* Store of parent *)
   rewrite sep_swap3 in SEP.
-  apply (range_contains Mptr) in SEP; [|tauto].
+  apply range_contains in SEP;[|apply perm_F_any|tauto].
   exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr).
   rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
   clear SEP; intros (m3' & STORE_PARENT & SEP).
   rewrite sep_swap3 in SEP.
   (* Store of return address *)
   rewrite sep_swap4 in SEP.
-  apply (range_contains Mptr) in SEP; [|tauto].
+  apply range_contains in SEP; [|apply perm_F_any|tauto].
   exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr).
   rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
   clear SEP; intros (m4' & STORE_RETADDR & SEP).
diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 92457586..2bccf60a 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -74,6 +74,8 @@ Definition outcome_result_value (out: outcome) (t: type) (v: val) (m: mem): Prop
   [t] is the trace of input/output events performed during this
   evaluation. *)
 
+Variable function_entry: function -> list val -> mem -> env -> temp_env -> mem -> Prop.
+
 Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env -> mem -> outcome -> Prop :=
   | exec_Sskip:   forall e le m,
       exec_stmt e le m Sskip
@@ -163,14 +165,12 @@ Inductive exec_stmt: env -> temp_env -> mem -> statement -> trace -> temp_env ->
   by the call.  *)
 
 with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
-  | eval_funcall_internal: forall le m f vargs t e m1 m2 m3 out vres m4,
-      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
-      exec_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t le m3 out ->
-      outcome_result_value out f.(fn_return) vres m3 ->
-      Mem.free_list m3 (blocks_of_env ge e) = Some m4 ->
-      eval_funcall m (Internal f) vargs t m4 vres
+  | eval_funcall_internal: forall m f vargs t e le1 le2 m1 m2 out vres m3,
+      function_entry f vargs m e le1 m1 ->
+      exec_stmt e le1 m1 f.(fn_body) t le2 m2 out ->
+      outcome_result_value out f.(fn_return) vres m2 ->
+      Mem.free_list m2 (blocks_of_env ge e) = Some m3 ->
+      eval_funcall m (Internal f) vargs t m3 vres
   | eval_funcall_external: forall m ef targs tres cconv vargs t vres m',
       external_call ef ge vargs m t vres m' ->
       eval_funcall m (External ef targs tres cconv) vargs t m' vres.
@@ -231,17 +231,19 @@ CoInductive execinf_stmt: env -> temp_env -> mem -> statement -> traceinf -> Pro
     [fd] on arguments [args] diverges, with observable trace [t]. *)
 
 with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop :=
-  | evalinf_funcall_internal: forall m f vargs t e m1 m2,
-      alloc_variables ge empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 ->
-      list_norepet (var_names f.(fn_params) ++ var_names f.(fn_vars)) ->
-      bind_parameters ge e m1 f.(fn_params) vargs m2 ->
-      execinf_stmt e (create_undef_temps f.(fn_temps)) m2 f.(fn_body) t ->
+  | evalinf_funcall_internal: forall m f vargs t e m1 le1,
+      function_entry f vargs m e le1 m1 ->
+      execinf_stmt e le1 m1 f.(fn_body) t ->
       evalinf_funcall m (Internal f) vargs t.
 
 End BIGSTEP.
 
 (** Big-step execution of a whole program.  *)
 
+Section ENTRY.
+
+Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop.
+
 Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
   | bigstep_program_terminates_intro: forall b f m0 m1 t r,
       let ge := globalenv p in
@@ -249,7 +251,7 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop :=
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
-      eval_funcall ge m0 f nil t m1 (Vint r) ->
+      eval_funcall ge (function_entry ge) m0 f nil t m1 (Vint r) ->
       bigstep_program_terminates p t r.
 
 Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
@@ -259,12 +261,14 @@ Inductive bigstep_program_diverges (p: program): traceinf -> Prop :=
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       type_of_fundef f = Tfunction Tnil type_int32s cc_default ->
-      evalinf_funcall ge m0 f nil t ->
+      evalinf_funcall ge (function_entry ge) m0 f nil t ->
       bigstep_program_diverges p t.
 
 Definition bigstep_semantics (p: program) :=
   Bigstep_semantics (bigstep_program_terminates p) (bigstep_program_diverges p).
 
+End ENTRY.
+
 (** * Implication from big-step semantics to transition semantics *)
 
 Section BIGSTEP_TO_TRANSITIONS.
@@ -296,18 +300,31 @@ Proof.
   destruct k; simpl; intros; contradiction || auto.
 Qed.
 
+Variable function_entry: genv -> function -> list val -> mem -> env -> temp_env -> mem -> Prop.
+
+Definition exec_stmt_fe (ge: genv) := exec_stmt ge (function_entry ge).
+Definition eval_funcall_fe (ge: genv) := eval_funcall ge (function_entry ge).
+Definition execinf_stmt_fe (ge: genv) := execinf_stmt ge (function_entry ge).
+Definition evalinf_funcall_fe (ge: genv) := evalinf_funcall ge (function_entry ge).
+Definition bigstep_semantics_fe := bigstep_semantics function_entry.
+
+Definition step_fe (ge: genv) := step ge (function_entry ge).
+Definition semantics_fe (p: program) :=
+  let ge := globalenv p in
+  Semantics_gen step_fe (initial_state p) final_state ge ge.
+
 Lemma exec_stmt_eval_funcall_steps:
   (forall e le m s t le' m' out,
-   exec_stmt ge e le m s t le' m' out ->
+   exec_stmt_fe ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step1 ge (State f s k e le m) t S
+   star step_fe ge (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S)
 /\
   (forall m fd args t m' res,
-   eval_funcall ge m fd args t m' res ->
+   eval_funcall_fe ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step1 ge (Callstate fd args k m) t (Returnstate res k m')).
+   star step_fe ge (Callstate fd args k m) t (Returnstate res k m')).
 Proof.
   apply exec_stmt_funcall_ind; intros.
 
@@ -450,23 +467,23 @@ Proof.
   unfold S2. inv B1; simpl; econstructor; eauto.
 
 (* call internal *)
-  destruct (H3 f k) as [S1 [A1 B1]].
-  eapply star_left. eapply step_internal_function; eauto. econstructor; eauto.
+  destruct (H1 f k) as [S1 [A1 B1]].
+  eapply star_left. eapply step_internal_function; eauto.
   eapply star_right. eexact A1.
    inv B1; simpl in H4; try contradiction.
   (* Out_normal *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H7. subst vres. apply step_skip_call; auto.
+  destruct H5. subst vres. apply step_skip_call; auto.
   (* Out_return None *)
   assert (fn_return f = Tvoid /\ vres = Vundef).
     destruct (fn_return f); auto || contradiction.
-  destruct H8. subst vres.
-  rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7.
+  destruct H6. subst vres.
+  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
   apply step_return_0; auto.
   (* Out_return Some *)
-  destruct H4.
-  rewrite <- (is_call_cont_call_cont k H6). rewrite <- H7.
+  destruct H2.
+  rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5.
   eapply step_return_1; eauto.
   reflexivity. traceEq.
 
@@ -476,31 +493,31 @@ Qed.
 
 Lemma exec_stmt_steps:
    forall e le m s t le' m' out,
-   exec_stmt ge e le m s t le' m' out ->
+   exec_stmt_fe ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step1 ge (State f s k e le m) t S
+   star step_fe ge (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S.
 Proof (proj1 exec_stmt_eval_funcall_steps).
 
 Lemma eval_funcall_steps:
    forall m fd args t m' res,
-   eval_funcall ge m fd args t m' res ->
+   eval_funcall_fe ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step1 ge (Callstate fd args k m) t (Returnstate res k m').
+   star step_fe ge (Callstate fd args k m) t (Returnstate res k m').
 Proof (proj2 exec_stmt_eval_funcall_steps).
 
 Definition order (x y: unit) := False.
 
 Lemma evalinf_funcall_forever:
   forall m fd args T k,
-  evalinf_funcall ge m fd args T ->
-  forever_N step1 order ge tt (Callstate fd args k m) T.
+  evalinf_funcall_fe ge m fd args T ->
+  forever_N step_fe order ge tt (Callstate fd args k m) T.
 Proof.
   cofix CIH_FUN.
   assert (forall e le m s T f k,
-          execinf_stmt ge e le m s T ->
-          forever_N step1 order ge tt (State f s k e le m) T).
+          execinf_stmt_fe ge e le m s T ->
+          forever_N step_fe order ge tt (State f s k e le m) T).
   cofix CIH_STMT.
   intros. inv H.
 
@@ -559,13 +576,13 @@ Proof.
 (* call internal *)
   intros. inv H0.
   eapply forever_N_plus.
-  eapply plus_one. econstructor; eauto. econstructor; eauto.
+  eapply plus_one. econstructor; eauto.
   apply H; eauto.
   traceEq.
 Qed.
 
 Theorem bigstep_semantics_sound:
-  bigstep_sound (bigstep_semantics prog) (semantics1 prog).
+  bigstep_sound (bigstep_semantics_fe prog) (semantics_fe prog).
 Proof.
   constructor; simpl; intros.
 (* termination *)
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0aefde31..8190e35a 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -30,11 +30,7 @@ open Clight
    not in the table of atoms.  We print them as "$NNN" (a unique
    integer). *)
 
-let temp_name (id: AST.ident) =
-  try
-    "$" ^ Hashtbl.find string_of_atom id
-  with Not_found ->
-    Printf.sprintf "$%d" (P.to_int id)
+let temp_name (id: AST.ident) = (* "$" ^ Z.to_string (Z.Zpos id) *)extern_atom id
 
 (* Declarator (identifier + type) -- reuse from PrintCsyntax *)
 
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index d37fbd46..462a4ec1 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -22,10 +22,8 @@
   Global environments, along with the initial memory state at the beginning
   of program execution, are built from the program of interest, as follows:
 - A distinct memory address is assigned to each function of the program.
-  These function addresses use negative numbers to distinguish them from
-  addresses of memory blocks.  The associations of function name to function
-  address and function address to function description are recorded in
-  the global environment.
+  The associations of function name to function address and function address
+  to function description are recorded in the global environment.
 - For each global variable, a memory block is allocated and associated to
   the name of the variable.
 
diff --git a/common/Separation.v b/common/Separation.v
index 27065d1f..9aee633f 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -29,7 +29,7 @@
   frame rule; instead, a weak form of the frame rule is provided
   by the lemmas that help us reason about the logical assertions. *)
 
-Require Import Setoid Program.Basics.
+Require Import Setoid Morphisms Program.Basics.
 Require Import Coqlib Decidableplus.
 Require Import AST Integers Values Memory Events Globalenvs.
 
@@ -113,8 +113,37 @@ Proof.
   intros P Q [[A B] [C D]]. split; auto.
 Qed.
 
+Instance massert_imp_eqv_Proper:
+  Proper (massert_eqv ==> massert_eqv ==> iff) massert_imp.
+Proof.
+  intros p q Hpq r s Hrs.
+  split; destruct 1 as [HR1 HR2];
+    constructor; intros;
+      apply Hrs || apply Hpq;
+      apply HR1 || apply HR2;
+      apply Hpq || apply Hrs;
+      assumption.
+Qed.
+
 Hint Resolve massert_imp_refl massert_eqv_refl : core.
 
+Instance footprint_massert_imp_Proper:
+  Proper (massert_imp --> eq ==> eq ==> Basics.impl) m_footprint.
+Proof.
+  destruct 1. repeat intro. subst. intuition.
+Qed.
+
+Instance footprint_massert_eqv_Proper:
+  Proper (massert_eqv ==> eq ==> eq ==> iff) m_footprint.
+Proof.
+  intros P Q HPQ b' b Hbeq ofs' ofs Hoeq.
+  subst.
+  destruct HPQ as [HPQ HQP].
+  split; intro HH.
+  now rewrite HQP.
+  now rewrite HPQ.
+Qed.
+
 (** * Separating conjunction *)
 
 Definition disjoint_footprint (P Q: massert) : Prop :=
@@ -143,6 +172,21 @@ Proof.
 - intuition auto.
 Qed.
 
+Add Morphism disjoint_footprint
+    with signature massert_eqv ==> massert_eqv ==> iff
+    as disjoint_footprint_morph_1.
+Proof.
+  intros p q Hpq r s Hrs.
+  unfold disjoint_footprint.
+  split; intro HH; intros b ofs Hf1 Hf2.
+  - rewrite <-Hpq in Hf1.
+    rewrite <-Hrs in Hf2.
+    now specialize (HH _ _ Hf1 Hf2).
+  - rewrite Hpq in Hf1.
+    rewrite Hrs in Hf2.
+    now specialize (HH _ _ Hf1 Hf2).
+Qed.
+
 Add Morphism sepconj
   with signature massert_eqv ==> massert_eqv ==> massert_eqv
   as sepconj_morph_2.
@@ -161,6 +205,15 @@ Proof.
   intros. rewrite <- H0, <- H1; auto.
 Qed.
 
+Lemma sep_imp':
+  forall P P' Q Q',
+    massert_imp P P' ->
+    massert_imp Q Q' ->
+    massert_imp (P ** Q) (P' ** Q').
+Proof.
+  intros * HP HQ. rewrite HP, HQ. reflexivity.
+Qed.
+
 Lemma sep_comm_1:
   forall P Q,  massert_imp (P ** Q) (Q ** P).
 Proof.
@@ -240,15 +293,17 @@ Proof.
 Qed.
 
 Lemma sep_drop:
-  forall P Q m, m |= P ** Q -> m |= Q.
+  forall P Q, massert_imp (P ** Q) Q.
 Proof.
-  simpl; intros. tauto.
+  constructor.
+  - simpl; intros. tauto.
+  - intros. now constructor 2.
 Qed.
 
 Lemma sep_drop2:
-  forall P Q R m, m |= P ** Q ** R -> m |= P ** R.
+  forall P Q R, massert_imp (P ** Q ** R) (P ** R).
 Proof.
-  intros. rewrite sep_swap in H. eapply sep_drop; eauto.
+  intros. rewrite sep_swap, sep_drop. reflexivity.
 Qed.
 
 Lemma sep_proj1:
@@ -259,7 +314,9 @@ Qed.
 
 Lemma sep_proj2:
   forall P Q m, m |= P ** Q -> m |= Q.
-Proof sep_drop.
+Proof.
+  apply sep_drop.
+Qed.
 
 Definition sep_pick1 := sep_proj1.
 
@@ -315,19 +372,40 @@ Proof.
   simpl; intros. intuition auto. red; simpl; tauto.
 Qed.
 
-(** A range of bytes, with full permissions and unspecified contents. *)
+Lemma sep_pure':
+  forall P m, m |= pure P <-> P.
+Proof.
+  simpl; intros. intuition auto. 
+Qed.
+
+(** A range of bytes with given permissions unspecified contents *)
 
-Program Definition range (b: block) (lo hi: Z) : massert := {|
+Program Definition range' (p: permission) (b: block) (lo hi: Z) : massert := {|
   m_pred := fun m =>
        0 <= lo /\ hi <= Ptrofs.modulus
-    /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p);
+    /\ (forall i k, lo <= i < hi -> Mem.perm m b i k p);
   m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi
 |}.
 Next Obligation.
   split; auto. split; auto. intros. eapply Mem.perm_unchanged_on; eauto. simpl; auto.
 Qed.
 Next Obligation.
-  apply Mem.perm_valid_block with ofs Cur Freeable; auto.
+  eapply Mem.perm_valid_block with ofs Cur _; auto.
+Qed.
+
+Notation range := (range' Freeable).
+Notation range_w := (range' Writable).
+
+Lemma range'_imp:
+  forall p p' b lo hi,
+    perm_order p p' ->
+    massert_imp (range' p b lo hi) (range' p' b lo hi).
+Proof.
+  constructor; auto.
+  destruct 1 as (Hlo & Hhi & Hperm).
+  repeat split; auto.
+  intros i k Hoff.
+  eapply Mem.perm_implies; eauto.
 Qed.
 
 Lemma alloc_rule:
@@ -346,47 +424,95 @@ Proof.
   eelim Mem.fresh_block_alloc; eauto. eapply (m_valid P); eauto.
 Qed.
 
+Lemma free_rule:
+forall P m b lo hi,
+  m |= range b lo hi ** P ->
+  exists m',
+    Mem.free m b lo hi = Some m' /\ m' |= P.
+Proof.
+  intros P m b lo hi Hr.
+  destruct Hr as ((Hlo & Hhi & Hperm) & HP & Hdj).
+  assert (Mem.range_perm m b lo hi Cur Freeable) as Hrp
+    by (intros ? ?; now apply Hperm).
+  apply Mem.range_perm_free in Hrp.
+  destruct Hrp as (m2 & Hfree).
+  exists m2.
+  split; [assumption|].
+  apply Mem.free_unchanged_on with (P:=m_footprint P) in Hfree.
+  now apply m_invar with (1:=HP) (2:=Hfree).
+  intros i Hr HfP.
+  apply Hdj with (2:=HfP).
+  now split.
+Qed.
+
+Lemma range_split':
+  forall p b lo hi mid,
+    lo <= mid <= hi ->
+    massert_eqv (range' p b lo hi)
+                (range' p b lo mid ** range' p b mid hi).
+Proof.
+  intros * HR.
+  constructor; constructor.
+  - intros m HH.
+    inversion HH as [Hlo [Hhi Hperm]].
+    split; constructor; repeat split.
+    + assumption.
+    + omega.
+    + intros. apply Hperm. omega.
+    + omega.
+    + exact Hhi.
+    + intros. apply Hperm. omega.
+    + red; simpl; intros; omega.
+  - intros. simpl in *. intuition.
+  - intros m HH.
+    inversion_clear HH as [Hlm [Hmh Hdisj]].
+    inversion_clear Hlm as [Hlo [Hmid Hperm]].
+    inversion_clear Hmh as [Hmid' [Hhi Hperm']].
+    constructor; repeat split.
+    + assumption.
+    + assumption.
+    + intros i k Hi.
+      destruct (Z.lt_ge_cases i mid); intuition.
+  - intros * Hfoot. simpl in *.
+    destruct (Z.lt_ge_cases ofs mid); intuition.
+Qed.
+
 Lemma range_split:
-  forall b lo hi P mid m,
+  forall p b lo hi P mid m,
   lo <= mid <= hi ->
-  m |= range b lo hi ** P ->
-  m |= range b lo mid ** range b mid hi ** P.
+  m |= range' p b lo hi ** P ->
+  m |= range' p b lo mid ** range' p b mid hi ** P.
 Proof.
-  intros. rewrite <- sep_assoc. eapply sep_imp; eauto.
-  split; simpl; intros.
-- intuition auto.
-+ omega.
-+ apply H5; omega.
-+ omega.
-+ apply H5; omega.
-+ red; simpl; intros; omega.
-- intuition omega.
+  intros.
+  rewrite <-sep_assoc.
+  rewrite range_split' with (1:=H) in H0.
+  assumption.
 Qed.
 
 Lemma range_drop_left:
-  forall b lo hi P mid m,
+  forall p b lo hi P mid m,
   lo <= mid <= hi ->
-  m |= range b lo hi ** P ->
-  m |= range b mid hi ** P.
+  m |= range' p b lo hi ** P ->
+  m |= range' p b mid hi ** P.
 Proof.
-  intros. apply sep_drop with (range b lo mid). apply range_split; auto.
+  intros. apply sep_drop with (range' p b lo mid). apply range_split; auto.
 Qed.
 
 Lemma range_drop_right:
-  forall b lo hi P mid m,
+  forall p b lo hi P mid m,
   lo <= mid <= hi ->
-  m |= range b lo hi ** P ->
-  m |= range b lo mid ** P.
+  m |= range' p b lo hi ** P ->
+  m |= range' p b lo mid ** P.
 Proof.
-  intros. apply sep_drop2 with (range b mid hi). apply range_split; auto.
+  intros. apply sep_drop2 with (range' p b mid hi). apply range_split; auto.
 Qed.
 
 Lemma range_split_2:
-  forall b lo hi P mid al m,
+  forall p b lo hi P mid al m,
   lo <= align mid al <= hi ->
   al > 0 ->
-  m |= range b lo hi ** P ->
-  m |= range b lo mid ** range b (align mid al) hi ** P.
+  m |= range' p b lo hi ** P ->
+  m |= range' p b lo mid ** range' p b (align mid al) hi ** P.
 Proof.
   intros. rewrite <- sep_assoc. eapply sep_imp; eauto.
   assert (mid <= align mid al) by (apply align_le; auto).
@@ -401,67 +527,89 @@ Proof.
 Qed.
 
 Lemma range_preserved:
-  forall m m' b lo hi,
-  m |= range b lo hi ->
+  forall p m m' b lo hi,
+  m |= range' p b lo hi ->
   (forall i k p, lo <= i < hi -> Mem.perm m b i k p -> Mem.perm m' b i k p) ->
-  m' |= range b lo hi.
+  m' |= range' p b lo hi.
 Proof.
   intros. destruct H as (A & B & C). simpl; intuition auto.
 Qed.
 
-(** A memory area that contains a value sastifying a given predicate *)
+(** A memory area that contains a value satisfying a given predicate. *)
 
-Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {|
+Program Definition contains' (p: permission) (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {|
   m_pred := fun m =>
-       0 <= ofs <= Ptrofs.max_unsigned
-    /\ Mem.valid_access m chunk b ofs Freeable
+       0 <= ofs /\ ofs + size_chunk chunk <= Ptrofs.modulus
+    /\ Mem.valid_access m chunk b ofs p
     /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v;
   m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk
 |}.
 Next Obligation.
-  rename H2 into v. split;[|split].
+  rename H3 into v. split;[|split;[|split]].
+- auto.
 - auto.
-- destruct H1; split; auto. red; intros; eapply Mem.perm_unchanged_on; eauto. simpl; auto.
+- destruct H2; split; auto. red; intros; eapply Mem.perm_unchanged_on; eauto. simpl; auto.
 - exists v. split; auto. eapply Mem.load_unchanged_on; eauto. simpl; auto.
 Qed.
 Next Obligation.
   eauto with mem.
 Qed.
 
+Notation contains := (contains' Freeable).
+Notation contains_w := (contains' Writable).
+
+Lemma contains'_imp:
+  forall p p' chunk b ofs spec,
+    perm_order p p' ->
+    massert_imp (contains' p chunk b ofs spec) (contains' p' chunk b ofs spec).
+Proof.
+  constructor; auto.
+  inversion 1 as (Hlo & Hhi & Hac & v & Hload & Hspec).
+  eapply Mem.valid_access_implies in Hac; eauto.
+  repeat (split; eauto).
+Qed.
+  
 Lemma contains_no_overflow:
-  forall spec m chunk b ofs,
-  m |= contains chunk b ofs spec ->
+  forall p spec m chunk b ofs,
+  m |= contains' p chunk b ofs spec ->
   0 <= ofs <= Ptrofs.max_unsigned.
 Proof.
-  intros. simpl in H. tauto.
+  intros. simpl in H.
+  destruct H as (H1 & H2 & H3).
+  split; [assumption|].
+  generalize (size_chunk_pos chunk).
+  unfold Ptrofs.max_unsigned. omega.
 Qed.
 
 Lemma load_rule:
-  forall spec m chunk b ofs,
-  m |= contains chunk b ofs spec ->
+  forall p spec m chunk b ofs,
+  perm_order p Readable ->
+  m |= contains' p chunk b ofs spec ->
   exists v, Mem.load chunk m b ofs = Some v /\ spec v.
 Proof.
-  intros. destruct H as (D & E & v & F & G).
+  intros * Hp Hc. destruct Hc as (D & E & F & v & G & H).
   exists v; auto.
 Qed.
 
 Lemma loadv_rule:
-  forall spec m chunk b ofs,
-  m |= contains chunk b ofs spec ->
+  forall p spec m chunk b ofs,
+  perm_order p Readable ->
+  m |= contains' p chunk b ofs spec ->
   exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v.
 Proof.
-  intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto.
+  intros. exploit load_rule; eauto with mem. intros (v & A & B). exists v; split; auto.
   simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto.
 Qed.
 
 Lemma store_rule:
-  forall chunk m b ofs v (spec1 spec: val -> Prop) P,
-  m |= contains chunk b ofs spec1 ** P ->
+  forall p chunk m b ofs v (spec1 spec: val -> Prop) P,
+  perm_order p Writable ->
+  m |= contains' p chunk b ofs spec1 ** P ->
   spec (Val.load_result chunk v) ->
   exists m',
-  Mem.store chunk m b ofs v = Some m' /\ m' |= contains chunk b ofs spec ** P.
+  Mem.store chunk m b ofs v = Some m' /\ m' |= contains' p chunk b ofs spec ** P.
 Proof.
-  intros. destruct H as (A & B & C). destruct A as (D & E & v0 & F & G).
+  intros * Hp Hc Hs. destruct Hc as (A & B & C). destruct A as (D & E & v0 & F & G).
   assert (H: Mem.valid_access m chunk b ofs Writable) by eauto with mem.
   destruct (Mem.valid_access_store _ _ _ _ v H) as [m' STORE].
   exists m'; split; auto. simpl. intuition auto.
@@ -473,64 +621,132 @@ Proof.
 Qed.
 
 Lemma storev_rule:
-  forall chunk m b ofs v (spec1 spec: val -> Prop) P,
-  m |= contains chunk b ofs spec1 ** P ->
+  forall p chunk m b ofs v (spec1 spec: val -> Prop) P,
+  perm_order p Writable ->
+  m |= contains' p chunk b ofs spec1 ** P ->
   spec (Val.load_result chunk v) ->
   exists m',
-  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P.
+  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains' p chunk b ofs spec ** P.
 Proof.
   intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto.
   simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto.
 Qed.
 
-Lemma range_contains:
-  forall chunk b ofs P m,
-  m |= range b ofs (ofs + size_chunk chunk) ** P ->
-  (align_chunk chunk | ofs) ->
-  m |= contains chunk b ofs (fun v => True) ** P.
+Lemma storev_rule2:
+  forall p chunk m m' b ofs v (spec1 spec: val -> Prop) P,
+    perm_order p Writable ->
+    m |= contains' p chunk b ofs spec1 ** P ->
+    spec (Val.load_result chunk v) ->
+    Memory.Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' ->
+    m' |= contains' p chunk b ofs spec ** P.
 Proof.
-  intros. destruct H as (A & B & C). destruct A as (D & E & F).
-  split; [|split].
-- assert (Mem.valid_access m chunk b ofs Freeable).
+  intros * Hp Hm Hspec Hstore.
+  eapply storev_rule with (2:=Hm) in Hspec; eauto.
+  destruct Hspec as [m'' [Hmem Hspec]].
+  rewrite Hmem in Hstore. injection Hstore.
+  intro; subst. assumption.
+Qed.
+
+Lemma range_contains':
+  forall p chunk b ofs,
+    perm_order p Readable ->
+    (align_chunk chunk | ofs) ->
+    massert_imp (range' p b ofs (ofs + size_chunk chunk))
+                (contains' p chunk b ofs (fun v => True)).
+Proof.
+  intros. constructor.
+  intros * Hr. destruct Hr as (D & E & F).
+  assert (Mem.valid_access m chunk b ofs p).
   { split; auto. red; auto. }
-  split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega.
-  split. auto.
-+ destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD].
+  split; [|split].
+- generalize (size_chunk_pos chunk). omega.
+- assumption.
+- split; [assumption|].
+  destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD].
   eauto with mem.
   exists v; auto.
 - auto.
-- auto.
+Qed.
+
+Lemma range_contains:
+  forall p chunk b ofs P m,
+  perm_order p Readable ->
+  m |= range' p b ofs (ofs + size_chunk chunk) ** P ->
+  (align_chunk chunk | ofs) ->
+  m |= contains' p chunk b ofs (fun v => True) ** P.
+Proof.
+  intros * Hp Hr Hc.
+  rewrite range_contains' in Hr; assumption.
+Qed.
+
+Lemma contains_range':
+  forall p chunk b ofs spec,
+    massert_imp (contains' p chunk b ofs spec)
+                (range' p b ofs (ofs + size_chunk chunk)).
+Proof.
+  intros.
+  split.
+- intros. destruct H as (A & B & C & D).
+  split; [|split]; try assumption.
+  destruct C as (C1 & C2).
+  intros i k Hr.
+  specialize (C1 _ Hr).
+  eauto with mem.
+- trivial.
+Qed.
+
+Lemma contains_range:
+  forall p chunk b ofs spec P m,
+  m |= contains' p chunk b ofs spec ** P ->
+  m |= range' p b ofs (ofs + size_chunk chunk) ** P.
+Proof.
+  intros.
+  rewrite contains_range' in H; assumption.
 Qed.
 
 Lemma contains_imp:
-  forall (spec1 spec2: val -> Prop) chunk b ofs,
+  forall p (spec1 spec2: val -> Prop) chunk b ofs,
   (forall v, spec1 v -> spec2 v) ->
-  massert_imp (contains chunk b ofs spec1) (contains chunk b ofs spec2).
+  massert_imp (contains' p chunk b ofs spec1) (contains' p chunk b ofs spec2).
 Proof.
   intros; split; simpl; intros.
 - intuition auto. destruct H4 as (v & A & B). exists v; auto.
 - auto.
 Qed.
 
-(** A memory area that contains a given value *)
+(** A memory area that contains a given value. *)
 
-Definition hasvalue (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert :=
-  contains chunk b ofs (fun v' => v' = v).
+Definition hasvalue' (p: permission) (chunk: memory_chunk) (b: block) (ofs: Z) (v: val) : massert :=
+  contains' p chunk b ofs (fun v' => v' = v).
+
+Notation hasvalue := (hasvalue' Freeable).
+Notation hasvalue_w := (hasvalue' Writable).
+
+Lemma hasvalue'_imp:
+  forall p p' chunk b ofs v,
+    perm_order p p' ->
+    massert_imp (hasvalue' p chunk b ofs v) (hasvalue' p' chunk b ofs v).
+Proof.
+  constructor; auto.
+  now apply contains'_imp.
+Qed.
 
 Lemma store_rule':
-  forall chunk m b ofs v (spec1: val -> Prop) P,
-  m |= contains chunk b ofs spec1 ** P ->
+  forall p chunk m b ofs v (spec1: val -> Prop) P,
+  perm_order p Writable ->
+  m |= contains' p chunk b ofs spec1 ** P ->
   exists m',
-  Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P.
+  Mem.store chunk m b ofs v = Some m' /\ m' |= hasvalue' p chunk b ofs (Val.load_result chunk v) ** P.
 Proof.
   intros. eapply store_rule; eauto.
 Qed.
 
 Lemma storev_rule':
-  forall chunk m b ofs v (spec1: val -> Prop) P,
-  m |= contains chunk b ofs spec1 ** P ->
+  forall p chunk m b ofs v (spec1: val -> Prop) P,
+  perm_order p Writable ->
+  m |= contains' p chunk b ofs spec1 ** P ->
   exists m',
-  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P.
+  Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue' p chunk b ofs (Val.load_result chunk v) ** P.
 Proof.
   intros. eapply storev_rule; eauto.
 Qed.
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 0504ad0b..8e24e29f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -437,11 +437,12 @@ let elab_char_constant loc wide chars =
     warning loc Unnamed "character constant too long for its type";
   (* C99 6.4.4.4 item 10: single character -> represent at type char
      or wchar_t *)
-  Ceval.normalize_int v
+  let k =
     (if List.length chars = 1 then
        if wide then wchar_ikind() else IChar
      else
-       IInt)
+       IInt) in
+  (Ceval.normalize_int v k, k)
 
 let elab_string_literal loc wide chars =
   let nbits = if wide then 8 * !config.sizeof_wchar else 8 in
@@ -469,8 +470,7 @@ let elab_constant loc = function
       let (v, fk) = elab_float_constant f in
       CFloat(v, fk)
   | CONST_CHAR(wide, s) ->
-      let ikind = if wide then wchar_ikind () else IInt in
-      CInt(elab_char_constant loc wide s, ikind, "")
+      CInt(fst (elab_char_constant loc wide s), IInt, "")
   | CONST_STRING(wide, s) ->
       elab_string_literal loc wide s
 
diff --git a/cparser/Elab.mli b/cparser/Elab.mli
index 59c5efc1..68e33d06 100644
--- a/cparser/Elab.mli
+++ b/cparser/Elab.mli
@@ -20,6 +20,6 @@ val elab_file : Cabs.definition list -> C.program
 
 val elab_int_constant : Cabs.loc -> string -> int64 * C.ikind
 val elab_float_constant : Cabs.floatInfo -> C.float_cst * C.fkind
-val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64
+val elab_char_constant : Cabs.loc -> bool -> int64 list -> int64 * C.ikind
   (* These auxiliary functions are exported so that they can be reused
      in other projects that deal with C-style source languages. *)
diff --git a/doc/index.html b/doc/index.html
index 631c5d99..5f4ac5e1 100644
--- a/doc/index.html
+++ b/doc/index.html
@@ -341,7 +341,8 @@ See also: <A HREF="html/compcert.powerpc.NeedOp.html"><I>NeedOp</I></A>: process
 
 The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
 <UL>
-<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions.
+<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for 
+        CompCert C + type-checking functions.
 <LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
 reconstruction.
 <LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v
index cb3806bd..d5539b70 100644
--- a/powerpc/Stacklayout.v
+++ b/powerpc/Stacklayout.v
@@ -68,7 +68,7 @@ Lemma frame_env_separated:
        ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe))
        ** P.
 Proof.
-Local Opaque Z.add Z.mul sepconj range.
+Local Opaque Z.add Z.mul sepconj range'.
   intros; simpl.
   set (ol := align (8 + 4 * b.(bound_outgoing)) 8).
   set (ora := ol + 4 * b.(bound_local)).
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v
index d375febf..96b0c8ef 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -58,7 +58,7 @@ Lemma frame_env_separated:
        ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe))
        ** P.
 Proof.
-Local Opaque Z.add Z.mul sepconj range.
+Local Opaque Z.add Z.mul sepconj range'.
   intros; simpl.
   set (w := if Archi.ptr64 then 8 else 4).
   set (olink := align (4 * b.(bound_outgoing)) w).