Merge of branch "unsigned-offsets":

- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int.
  (Fixes issue with wrong comparison of pointers across 0x8000_0000)
- Revised Stacking pass to not use negative SP offsets.
- Add pointer validity checks to Cminor ... Mach
  to support the use of memory injections in Stacking.
- Cleaned up Stacklayout modules.
- IA32: improved code generation for Mgetparam.
- ARM: improved code generation for op-immediate instructions.


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

1 files changed, 56 insertions, 55 deletions

diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 3f98b881..25758cc8 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -88,10 +88,10 @@ Ltac InvVLMA :=
   approximations returned by [eval_static_operation]. *)
 
 Lemma eval_static_condition_correct:
-  forall cond al vl b,
+  forall cond al vl m b,
   val_list_match_approx al vl ->
   eval_static_condition cond al = Some b ->
-  eval_condition cond vl = Some b.
+  eval_condition cond vl m = Some b.
 Proof.
   intros until b.
   unfold eval_static_condition. 
@@ -100,9 +100,9 @@ Proof.
 Qed.
 
 Lemma eval_static_operation_correct:
-  forall op sp al vl v,
+  forall op sp al vl m v,
   val_list_match_approx al vl ->
-  eval_operation ge sp op vl = Some v ->
+  eval_operation ge sp op vl m = Some v ->
   val_match_approx (eval_static_operation op al) v.
 Proof.
   intros until v.
@@ -144,7 +144,7 @@ Proof.
   inv H4. destruct (Float.intoffloat f); simpl in H0; inv H0. red; auto.
 
   caseEq (eval_static_condition c vl0).
-  intros. generalize (eval_static_condition_correct _ _ _ _ H H1).
+  intros. generalize (eval_static_condition_correct _ _ _ m _ H H1).
   intro. rewrite H2 in H0. 
   destruct b; injection H0; intro; subst v; simpl; auto.
   intros; simpl; auto.
@@ -168,6 +168,7 @@ Section STRENGTH_REDUCTION.
 Variable app: reg -> approx.
 Variable sp: val.
 Variable rs: regset.
+Variable m: mem.
 Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.
 
 Lemma intval_correct:
@@ -183,7 +184,7 @@ Qed.
 Lemma cond_strength_reduction_correct:
   forall cond args,
   let (cond', args') := cond_strength_reduction app cond args in
-  eval_condition cond' rs##args' = eval_condition cond rs##args.
+  eval_condition cond' rs##args' m = eval_condition cond rs##args m.
 Proof.
   intros. unfold cond_strength_reduction.
   case (cond_strength_reduction_match cond args); intros.
@@ -191,7 +192,6 @@ Proof.
   caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmp. auto.
-  destruct c; reflexivity.
   caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
@@ -199,6 +199,7 @@ Proof.
   caseEq (intval app r1); intros.
   simpl. rewrite (intval_correct _ _ H). 
   destruct (rs#r2); auto. rewrite Int.swap_cmpu. auto.
+  destruct c; reflexivity.
   caseEq (intval app r2); intros.
   simpl. rewrite (intval_correct _ _ H0). auto.
   auto.
@@ -217,8 +218,8 @@ Qed.
 Lemma make_addimm_correct:
   forall n r v,
   let (op, args) := make_addimm n r in
-  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oadd (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_addimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -230,8 +231,8 @@ Qed.
 Lemma make_shlimm_correct:
   forall n r v,
   let (op, args) := make_shlimm n r in
-  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shlimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -244,8 +245,8 @@ Qed.
 Lemma make_shrimm_correct:
   forall n r v,
   let (op, args) := make_shrimm n r in
-  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shrimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -258,8 +259,8 @@ Qed.
 Lemma make_shruimm_correct:
   forall n r v,
   let (op, args) := make_shruimm n r in
-  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_shruimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -273,8 +274,8 @@ Lemma make_mulimm_correct:
   forall n r r' v,
   rs#r' = Vint n ->
   let (op, args) := make_mulimm n r r' in
-  eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Omul (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_mulimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -282,8 +283,8 @@ Proof.
   generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intros.
   subst n. simpl in H2. simpl. FuncInv. rewrite Int.mul_one in H1. congruence.
   caseEq (Int.is_power2 n); intros.
-  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil))
-     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil)).
+  replace (eval_operation ge sp Omul (rs # r :: Vint n :: nil) m)
+     with (eval_operation ge sp Oshl (rs # r :: Vint i :: nil) m).
   apply make_shlimm_correct. 
   simpl. generalize (Int.is_power2_range _ _ H2). 
   change (Z_of_nat Int.wordsize) with 32. intro. rewrite H3.
@@ -294,8 +295,8 @@ Qed.
 Lemma make_andimm_correct:
   forall n r v,
   let (op, args) := make_andimm n r in
-  eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oand (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_andimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -308,8 +309,8 @@ Qed.
 Lemma make_orimm_correct:
   forall n r v,
   let (op, args) := make_orimm n r in
-  eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oor (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_orimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -322,8 +323,8 @@ Qed.
 Lemma make_xorimm_correct:
   forall n r v,
   let (op, args) := make_xorimm n r in
-  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->
-  eval_operation ge sp op rs##args = Some v.
+  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) m = Some v ->
+  eval_operation ge sp op rs##args m = Some v.
 Proof.
   intros; unfold make_xorimm.
   generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intros.
@@ -336,16 +337,16 @@ Qed.
 Lemma op_strength_reduction_correct:
   forall op args v,
   let (op', args') := op_strength_reduction app op args in
-  eval_operation ge sp op rs##args = Some v ->
-  eval_operation ge sp op' rs##args' = Some v.
+  eval_operation ge sp op rs##args m = Some v ->
+  eval_operation ge sp op' rs##args' m = Some v.
 Proof.
   intros; unfold op_strength_reduction;
   case (op_strength_reduction_match op args); intros; simpl List.map.
   (* Oadd *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oadd (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r2 :: Vint i :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.add_commut; auto.
   caseEq (intval app r2); intros.
@@ -354,8 +355,8 @@ Proof.
   (* Oaddshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oaddshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto.
   assumption.
@@ -365,16 +366,16 @@ Proof.
   simpl in *. destruct rs#r2; auto. 
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H0).
-  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil)).
+  replace (eval_operation ge sp Osub (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg i) :: nil) m).
   apply make_addimm_correct.
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
   (* Osubshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil)).
+  replace (eval_operation ge sp (Osubshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oadd (rs # r1 :: Vint (Int.neg (eval_shift s i)) :: nil) m).
   apply make_addimm_correct. 
   simpl. destruct rs#r1; auto; rewrite Int.sub_add_opp; auto.
   assumption.
@@ -386,8 +387,8 @@ Proof.
   (* Omul *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Omul (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Omul (rs # r2 :: Vint i :: nil) m).
   apply make_mulimm_correct. apply intval_correct; auto. 
   simpl. destruct rs#r2; auto. rewrite Int.mul_commut; auto.
   caseEq (intval app r2); intros.
@@ -398,8 +399,8 @@ Proof.
   caseEq (intval app r2); intros.
   caseEq (Int.is_power2 i); intros.
   rewrite (intval_correct _ _ H).
-  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil)).
+  replace (eval_operation ge sp Odivu (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oshru (rs # r1 :: Vint i0 :: nil) m).
   apply make_shruimm_correct. 
   simpl. destruct rs#r1; auto. 
   change 32 with (Z_of_nat Int.wordsize). 
@@ -412,8 +413,8 @@ Proof.
   (* Oand *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oand (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oand (rs # r2 :: Vint i :: nil) m).
   apply make_andimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.and_commut; auto.
   caseEq (intval app r2); intros.
@@ -422,15 +423,15 @@ Proof.
   (* Oandshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oandshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oor *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oor (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oor (rs # r2 :: Vint i :: nil) m).
   apply make_orimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.or_commut; auto.
   caseEq (intval app r2); intros.
@@ -439,15 +440,15 @@ Proof.
   (* Oorshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oorshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_orimm_correct. reflexivity.
   assumption.
   (* Oxor *)
   caseEq (intval app r1); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil))
-     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil)).
+  replace (eval_operation ge sp Oxor (Vint i :: rs # r2 :: nil) m)
+     with (eval_operation ge sp Oxor (rs # r2 :: Vint i :: nil) m).
   apply make_xorimm_correct. 
   simpl. destruct rs#r2; auto. rewrite Int.xor_commut; auto.
   caseEq (intval app r2); intros.
@@ -456,22 +457,22 @@ Proof.
   (* Oxorshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil)).
+  replace (eval_operation ge sp (Oxorshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oxor (rs # r1 :: Vint (eval_shift s i) :: nil) m).
   apply make_xorimm_correct. reflexivity.
   assumption.
   (* Obic *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil)).
+  replace (eval_operation ge sp Obic (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not i) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Obicshift *)
   caseEq (intval app r2); intros.
   rewrite (intval_correct _ _ H). 
-  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil))
-     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil)).
+  replace (eval_operation ge sp (Obicshift s) (rs # r1 :: Vint i :: nil) m)
+     with (eval_operation ge sp Oand (rs # r1 :: Vint (Int.not (eval_shift s i)) :: nil) m).
   apply make_andimm_correct. reflexivity.
   assumption.
   (* Oshl *)