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, 55 insertions, 50 deletions

diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index aef03db..81154f9 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -1009,10 +1009,29 @@ Proof.
   destruct (Int.lt n1 n2); auto.
 Qed.
 
-Lemma testcond_for_signed_comparison_correct_pi:
+Lemma testcond_for_unsigned_comparison_correct_ii:
+  forall c n1 n2 rs,
+  eval_testcond (testcond_for_unsigned_comparison c)
+                (nextinstr (compare_ints (Vint n1) (Vint n2) rs)) =
+  Some(Int.cmpu c n1 n2).
+Proof.
+  intros. generalize (compare_ints_spec rs (Vint n1) (Vint n2)).
+  set (rs' := nextinstr (compare_ints (Vint n1) (Vint n2) rs)). 
+  intros [A [B [C D]]].
+  unfold eval_testcond. rewrite A; rewrite B; rewrite C.
+  destruct c; simpl.
+  destruct (Int.eq n1 n2); auto.
+  destruct (Int.eq n1 n2); auto.
+  destruct (Int.ltu n1 n2); auto.
+  rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
+  rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
+  destruct (Int.ltu n1 n2); auto.
+Qed.
+
+Lemma testcond_for_unsigned_comparison_correct_pi:
   forall c blk n1 n2 rs b,
   eval_compare_null c n2 = Some b ->
-  eval_testcond (testcond_for_signed_comparison c)
+  eval_testcond (testcond_for_unsigned_comparison c)
                 (nextinstr (compare_ints (Vptr blk n1) (Vint n2) rs)) = Some b.
 Proof.
   intros.
@@ -1028,10 +1047,10 @@ Proof.
   rewrite <- H0; auto.
 Qed.
 
-Lemma testcond_for_signed_comparison_correct_ip:
+Lemma testcond_for_unsigned_comparison_correct_ip:
   forall c blk n1 n2 rs b,
   eval_compare_null c n1 = Some b ->
-  eval_testcond (testcond_for_signed_comparison c)
+  eval_testcond (testcond_for_unsigned_comparison c)
                 (nextinstr (compare_ints (Vint n1) (Vptr blk n2) rs)) = Some b.
 Proof.
   intros.
@@ -1047,14 +1066,18 @@ Proof.
   rewrite <- H0; auto.
 Qed.
 
-Lemma testcond_for_signed_comparison_correct_pp:
-  forall c b1 n1 b2 n2 rs b,
-  (if eq_block b1 b2 then Some (Int.cmp c n1 n2) else eval_compare_mismatch c) = Some b ->
-  eval_testcond (testcond_for_signed_comparison c)
+Lemma testcond_for_unsigned_comparison_correct_pp:
+  forall c b1 n1 b2 n2 rs m b,
+  (if Mem.valid_pointer m b1 (Int.unsigned n1) && Mem.valid_pointer m b2 (Int.unsigned n2) 
+   then if eq_block b1 b2 then Some (Int.cmpu c n1 n2) else eval_compare_mismatch c
+   else None) = Some b ->
+  eval_testcond (testcond_for_unsigned_comparison c)
                 (nextinstr (compare_ints (Vptr b1 n1) (Vptr b2 n2) rs)) =
   Some b.
 Proof.
-  intros. generalize (compare_ints_spec rs (Vptr b1 n1) (Vptr b2 n2)).
+  intros.
+  destruct (Mem.valid_pointer m b1 (Int.unsigned n1) && Mem.valid_pointer m b2 (Int.unsigned n2)); try discriminate.
+  generalize (compare_ints_spec rs (Vptr b1 n1) (Vptr b2 n2)).
   set (rs' := nextinstr (compare_ints (Vptr b1 n1) (Vptr b2 n2) rs)). 
   intros [A [B [C D]]]. unfold eq_block in H.
   unfold eval_testcond. rewrite A; rewrite B; rewrite C.
@@ -1063,37 +1086,18 @@ Proof.
   rewrite <- H; auto.
   destruct (zeq b1 b2). inversion H. destruct (Int.eq n1 n2); auto.
   rewrite <- H; auto.
-  destruct (zeq b1 b2). inversion H. destruct (Int.lt n1 n2); auto.
+  destruct (zeq b1 b2). inversion H. destruct (Int.ltu n1 n2); auto.
   discriminate.
   destruct (zeq b1 b2). inversion H. 
-  rewrite int_not_lt. destruct (Int.lt n1 n2); destruct (Int.eq n1 n2); auto.
+  rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
   discriminate.
   destruct (zeq b1 b2). inversion H. 
-  rewrite (int_lt_not n1 n2). destruct (Int.lt n1 n2); destruct (Int.eq n1 n2); auto.
+  rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
   discriminate.
-  destruct (zeq b1 b2). inversion H. destruct (Int.lt n1 n2); auto.
+  destruct (zeq b1 b2). inversion H. destruct (Int.ltu n1 n2); auto.
   discriminate.
 Qed.
 
-Lemma testcond_for_unsigned_comparison_correct:
-  forall c n1 n2 rs,
-  eval_testcond (testcond_for_unsigned_comparison c)
-                (nextinstr (compare_ints (Vint n1) (Vint n2) rs)) =
-  Some(Int.cmpu c n1 n2).
-Proof.
-  intros. generalize (compare_ints_spec rs (Vint n1) (Vint n2)).
-  set (rs' := nextinstr (compare_ints (Vint n1) (Vint n2) rs)). 
-  intros [A [B [C D]]].
-  unfold eval_testcond. rewrite A; rewrite B; rewrite C.
-  destruct c; simpl.
-  destruct (Int.eq n1 n2); auto.
-  destruct (Int.eq n1 n2); auto.
-  destruct (Int.ltu n1 n2); auto.
-  rewrite int_not_ltu. destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
-  rewrite (int_ltu_not n1 n2). destruct (Int.ltu n1 n2); destruct (Int.eq n1 n2); auto.
-  destruct (Int.ltu n1 n2); auto.
-Qed.
-
 Lemma compare_floats_spec:
   forall rs n1 n2,
   let rs' := nextinstr (compare_floats (Vfloat n1) (Vfloat n2) rs) in
@@ -1214,7 +1218,7 @@ Qed.
 Lemma transl_cond_correct:
   forall cond args k c rs m b,
   transl_cond cond args k = OK c ->
-  eval_condition cond (map rs (map preg_of args)) = Some b ->
+  eval_condition cond (map rs (map preg_of args)) m = Some b ->
   exists rs',
      exec_straight c rs m k rs' m
   /\ eval_testcond (testcond_for_condition cond) rs' = Some b
@@ -1227,32 +1231,33 @@ Proof.
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. simpl in H0. FuncInv.
   subst b. apply testcond_for_signed_comparison_correct_ii. 
-  apply testcond_for_signed_comparison_correct_ip; auto. 
-  apply testcond_for_signed_comparison_correct_pi; auto.
-  apply testcond_for_signed_comparison_correct_pp; auto.
   intros. unfold compare_ints. repeat SOther.
 (* compu *)
-  simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0.
+  simpl map in H0. 
+  rewrite (ireg_of_eq _ _ EQ) in H0. rewrite (ireg_of_eq _ _ EQ1) in H0.
   econstructor. split. apply exec_straight_one. simpl. eauto. auto.
   split. simpl in H0. FuncInv.
-  subst b. apply testcond_for_unsigned_comparison_correct. 
+  subst b. apply testcond_for_unsigned_comparison_correct_ii. 
+  apply testcond_for_unsigned_comparison_correct_ip; auto. 
+  apply testcond_for_unsigned_comparison_correct_pi; auto.
+  eapply testcond_for_unsigned_comparison_correct_pp; eauto.
   intros. unfold compare_ints. repeat SOther.
 (* compimm *)
   simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0.
-  econstructor. split. apply exec_straight_one. simpl; eauto. auto.
-  split. simpl in H0. FuncInv. 
-  subst b. apply testcond_for_signed_comparison_correct_ii. 
-  apply testcond_for_signed_comparison_correct_pi; auto.
-  intros. unfold compare_ints. repeat SOther.
-(* compuimm *)
-  simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0.
   exists (nextinstr (compare_ints (rs x) (Vint i) rs)).
   split. destruct (Int.eq_dec i Int.zero). 
   apply exec_straight_one. subst i. simpl.
   simpl in H0. FuncInv. simpl. rewrite Int.and_idem. auto. auto.
   apply exec_straight_one; auto.
   split. simpl in H0. FuncInv.
-  subst b. apply testcond_for_unsigned_comparison_correct.
+  subst b. apply testcond_for_signed_comparison_correct_ii.
+  intros. unfold compare_ints. repeat SOther.
+(* compuimm *)
+  simpl map in H0. rewrite (ireg_of_eq _ _ EQ) in H0.
+  econstructor. split. apply exec_straight_one. simpl; eauto. auto.
+  split. simpl in H0. FuncInv. 
+  subst b. apply testcond_for_unsigned_comparison_correct_ii. 
+  apply testcond_for_unsigned_comparison_correct_pi; auto.
   intros. unfold compare_ints. repeat SOther.
 (* compf *)
   simpl map in H0. rewrite (freg_of_eq _ _ EQ) in H0. rewrite (freg_of_eq _ _ EQ1) in H0.
@@ -1333,7 +1338,7 @@ Ltac TranslOp :=
 Lemma transl_op_correct:
   forall op args res k c (rs: regset) m v,
   transl_op op args res k = OK c ->
-  eval_operation ge (rs#ESP) op (map rs (map preg_of args)) = Some v ->
+  eval_operation ge (rs#ESP) op (map rs (map preg_of args)) m = Some v ->
   exists rs',
      exec_straight c rs m k rs' m
   /\ rs'#(preg_of res) = v
@@ -1342,7 +1347,7 @@ Lemma transl_op_correct:
      r <> preg_of res -> rs' r = rs r.
 Proof.
   intros until v; intros TR EV.
-  rewrite <- (eval_operation_weaken _ _ _ _ EV).
+  rewrite <- (eval_operation_weaken _ _ _ _ _ EV).
   destruct op; simpl in TR; ArgsInv; try (TranslOp; fail).
 (* move *)
   exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. 
@@ -1383,8 +1388,8 @@ Proof.
   rewrite (eval_addressing_weaken _ _ _ _ EV). rewrite <- EA. 
   TranslOp.
 (* condition *)
-  remember (eval_condition c0 rs ## (preg_of ## args)) as ob. destruct ob; inv EV. 
-  rewrite (eval_condition_weaken _ _ (sym_equal Heqob)). 
+  remember (eval_condition c0 rs ## (preg_of ## args) m) as ob. destruct ob; inv EV. 
+  rewrite (eval_condition_weaken _ _ _ (sym_equal Heqob)). 
   exploit transl_cond_correct; eauto. intros [rs2 [P [Q R]]].
   exists (nextinstr (rs2#ECX <- Vundef #EDX <- Vundef #x <- v)).
   split. eapply exec_straight_trans. eauto.