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, 16 insertions, 13 deletions

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index d997015..d475f26 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -86,7 +86,7 @@ Lemma eval_base_condition_of_expr:
   eval_expr ge sp e m le a v ->
   Val.bool_of_val v b ->
   eval_condexpr ge sp e m le 
-                (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))
+                (CEcond (Ccompuimm Cne Int.zero) (a ::: Enil))
                 b.
 Proof.
   intros. 
@@ -97,7 +97,7 @@ Qed.
 Lemma is_compare_neq_zero_correct:
   forall c v b,
   is_compare_neq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
+  eval_condition c (v :: nil) m = Some b ->
   Val.bool_of_val v b.
 Proof.
   intros.
@@ -107,17 +107,18 @@ Proof.
 
   simpl in H0. destruct v; inv H0. 
   generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
-  subst i; constructor. constructor; auto. constructor.
+  subst i; constructor. constructor; auto.
 
   simpl in H0. destruct v; inv H0. 
   generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
   subst i; constructor. constructor; auto.
+  constructor.
 Qed.
 
 Lemma is_compare_eq_zero_correct:
   forall c v b,
   is_compare_eq_zero c = true ->
-  eval_condition c (v :: nil) = Some b ->
+  eval_condition c (v :: nil) m = Some b ->
   Val.bool_of_val v (negb b).
 Proof.
   intros. apply is_compare_neq_zero_correct with (negate_condition c).
@@ -145,8 +146,8 @@ Proof.
   eapply eval_base_condition_of_expr; eauto.
 
   inv H0. simpl in H7.
-  assert (eval_condition c vl = Some b).
-    destruct (eval_condition c vl); try discriminate.
+  assert (eval_condition c vl m = Some b).
+    destruct (eval_condition c vl m); try discriminate.
     destruct b0; inv H7; inversion H1; congruence.
   assert (eval_condexpr ge sp e m le (CEcond c e0) b).
     eapply eval_CEcond; eauto.
@@ -230,7 +231,7 @@ Lemma eval_sel_binop:
   forall le op a1 a2 v1 v2 v,
   eval_expr ge sp e m le a1 v1 ->
   eval_expr ge sp e m le a2 v2 ->
-  eval_binop op v1 v2 = Some v ->
+  eval_binop op v1 v2 m = Some v ->
   eval_expr ge sp e m le (sel_binop op a1 a2) v.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
@@ -263,13 +264,15 @@ Proof.
   apply eval_subf; auto.
   apply eval_mulf; auto.
   apply eval_divf; auto.
-  apply eval_comp_int; auto.
-  eapply eval_comp_int_ptr; eauto.
-  eapply eval_comp_ptr_int; eauto.
+  apply eval_comp; auto.
+  eapply eval_compu_int; eauto.
+  eapply eval_compu_int_ptr; eauto.
+  eapply eval_compu_ptr_int; eauto.
+  destruct (Mem.valid_pointer m b (Int.unsigned i) &&
+            Mem.valid_pointer m b0 (Int.unsigned i0)) as [] _eqn; try congruence.
   destruct (eq_block b b0); inv H1.
-  eapply eval_comp_ptr_ptr; eauto.
-  eapply eval_comp_ptr_ptr_2; eauto.
-  eapply eval_compu; eauto.
+  eapply eval_compu_ptr_ptr; eauto.
+  eapply eval_compu_ptr_ptr_2; eauto.
   eapply eval_compf; eauto.
 Qed.