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, 39 insertions, 35 deletions

diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 3d6a667..82bca26 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -64,13 +64,13 @@ Ltac InvEval1 :=
 
 Ltac InvEval2 :=
   match goal with
-  | [ H: (eval_operation _ _ _ nil = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
       simpl in H; inv H
-  | [ H: (eval_operation _ _ _ (_ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
-  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
-  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) = Some _) |- _ ] =>
+  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
       simpl in H; FuncInv
   | _ =>
       idtac
@@ -150,12 +150,12 @@ Proof.
   eapply eval_notbool_base; eauto.
 
   inv H. eapply eval_Eop; eauto.
-  simpl. assert (eval_condition c vl = Some b).
+  simpl. assert (eval_condition c vl m = Some b).
   generalize H6. simpl. 
   case (eval_condition c vl); intros.
   destruct b0; inv H1; inversion H0; auto; congruence.
   congruence.
-  rewrite (Op.eval_negate_condition _ _ H). 
+  rewrite (Op.eval_negate_condition _ _ _ H). 
   destruct b; reflexivity.
 
   inv H. eapply eval_Econdition; eauto. 
@@ -667,7 +667,7 @@ Proof.
   EvalOp. simpl. rewrite H1. auto.
 Qed.
 
-Theorem eval_comp_int:
+Theorem eval_comp:
   forall le c a x b y,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vint y) ->
@@ -680,6 +680,19 @@ Proof.
   EvalOp. simpl. destruct (Int.cmp c x y); reflexivity.
 Qed.
 
+Theorem eval_compu_int:
+  forall le c a x b y,
+  eval_expr ge sp e m le a (Vint x) ->
+  eval_expr ge sp e m le b (Vint y) ->
+  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
+Proof.
+  intros until y.
+  unfold compu; case (comp_match a b); intros; InvEval.
+  EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+Qed.
+
 Remark eval_compare_null_transf:
   forall c x v,
   Cminor.eval_compare_null c x = Some v ->
@@ -694,15 +707,15 @@ Proof.
   destruct c; try discriminate; auto.
 Qed.
 
-Theorem eval_comp_ptr_int:
+Theorem eval_compu_ptr_int:
   forall le c a x1 x2 b y v,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vint y) ->
   Cminor.eval_compare_null c y = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until v.
-  unfold comp; case (comp_match a b); intros; InvEval.
+  unfold compu; case (comp_match a b); intros; InvEval.
   EvalOp. simpl. apply eval_compare_null_transf; auto.
   EvalOp. simpl. apply eval_compare_null_transf; auto.
 Qed.
@@ -716,58 +729,49 @@ Proof.
   destruct (Int.eq x Int.zero). destruct c; auto. auto.
 Qed.
 
-Theorem eval_comp_int_ptr:
+Theorem eval_compu_int_ptr:
   forall le c a x b y1 y2 v,
   eval_expr ge sp e m le a (Vint x) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
   Cminor.eval_compare_null c x = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until v.
-  unfold comp; case (comp_match a b); intros; InvEval.
+  unfold compu; case (comp_match a b); intros; InvEval.
   EvalOp. simpl. apply eval_compare_null_transf. 
   rewrite eval_compare_null_swap; auto.
   EvalOp. simpl. apply eval_compare_null_transf. auto.
 Qed.
 
-Theorem eval_comp_ptr_ptr:
+Theorem eval_compu_ptr_ptr:
   forall le c a x1 x2 b y1 y2,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
+  Mem.valid_pointer m x1 (Int.unsigned x2)
+  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
   x1 = y1 ->
-  eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x2 y2)).
+  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)).
 Proof.
   intros until y2.
-  unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. subst y1. rewrite dec_eq_true. 
-  destruct (Int.cmp c x2 y2); reflexivity.
+  unfold compu; case (comp_match a b); intros; InvEval.
+  EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. 
+  destruct (Int.cmpu c x2 y2); reflexivity.
 Qed.
 
-Theorem eval_comp_ptr_ptr_2:
+Theorem eval_compu_ptr_ptr_2:
   forall le c a x1 x2 b y1 y2 v,
   eval_expr ge sp e m le a (Vptr x1 x2) ->
   eval_expr ge sp e m le b (Vptr y1 y2) ->
+  Mem.valid_pointer m x1 (Int.unsigned x2)
+  && Mem.valid_pointer m y1 (Int.unsigned y2) = true ->
   x1 <> y1 ->
   Cminor.eval_compare_mismatch c = Some v ->
-  eval_expr ge sp e m le (comp c a b) v.
+  eval_expr ge sp e m le (compu c a b) v.
 Proof.
   intros until y2.
-  unfold comp; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite dec_eq_false; auto.
-  destruct c; simpl in H2; inv H2; auto.
-Qed.
-
-Theorem eval_compu:
-  forall le c a x b y,
-  eval_expr ge sp e m le a (Vint x) ->
-  eval_expr ge sp e m le b (Vint y) ->
-  eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)).
-Proof.
-  intros until y.
   unfold compu; case (comp_match a b); intros; InvEval.
-  EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
-  EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity.
+  EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto.
+  destruct c; simpl in H3; inv H3; auto.
 Qed.
 
 Theorem eval_compf: