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

8 files changed, 56 insertions, 54 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 22c3a5a..c293efb 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -489,7 +489,7 @@ Definition transl_funbody
 Definition transl_function
          (gce: compilenv) (f: Csharpminor.function): res function :=
   let (cenv, stacksize) := build_compilenv gce f in
-  if zle stacksize Int.max_signed
+  if zle stacksize Int.max_unsigned
   then transl_funbody cenv stacksize f
   else Error(msg "Cminorgen: too many local variables, stack size exceeded").
 
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 480acbb..ba51310 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -76,7 +76,7 @@ Lemma sig_preserved:
 Proof.
   intros until tf; destruct f; simpl.
   unfold transl_function. destruct (build_compilenv gce f).
-  case (zle z Int.max_signed); simpl bind; try congruence.
+  case (zle z Int.max_unsigned); simpl bind; try congruence.
   intros. monadInv H. simpl. eapply sig_preserved_body; eauto. 
   intro. inv H. reflexivity.
 Qed.
@@ -1265,7 +1265,7 @@ Lemma eval_binop_compat:
   val_inject f v2 tv2 ->
   Mem.inject f m tm ->
   exists tv,
-     Cminor.eval_binop op tv1 tv2 = Some tv
+     Cminor.eval_binop op tv1 tv2 tm = Some tv
   /\ val_inject f v tv.
 Proof.
   destruct op; simpl; intros.
@@ -1302,19 +1302,25 @@ Proof.
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
-    exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
-    exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
-  (* cmp ptr ptr *)
-  caseEq (Mem.valid_pointer m b1 (Int.signed ofs1) && Mem.valid_pointer m b0 (Int.signed ofs0)); 
+(* cmpu *)
+  inv H0; try discriminate; inv H1; inv H; TrivialOp.
+  exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
+  exists v; split; auto. eapply val_inject_eval_compare_null; eauto.
+  (* cmpu ptr ptr *)
+  caseEq (Mem.valid_pointer m b1 (Int.unsigned ofs1) && Mem.valid_pointer m b0 (Int.unsigned ofs0)); 
   intro EQ; rewrite EQ in H4; try discriminate.
   elim (andb_prop _ _ EQ); intros.
+  exploit Mem.valid_pointer_inject_val. eauto. eexact H. econstructor; eauto. 
+  intros V1. rewrite V1.
+  exploit Mem.valid_pointer_inject_val. eauto. eexact H1. econstructor; eauto. 
+  intros V2. rewrite V2. simpl.
   destruct (eq_block b1 b0); inv H4.
   (* same blocks in source *)
   assert (b3 = b2) by congruence. subst b3.
   assert (delta0 = delta) by congruence. subst delta0.
-  exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split.
+  exists (Val.of_bool (Int.cmpu c ofs1 ofs0)); split.
   unfold eq_block; rewrite zeq_true; simpl.
-  decEq. decEq. rewrite Int.translate_cmp. auto. 
+  decEq. decEq. rewrite Int.translate_cmpu. auto. 
   eapply Mem.valid_pointer_inject_no_overflow; eauto.
   eapply Mem.valid_pointer_inject_no_overflow; eauto.
   apply val_inject_val_of_bool.
@@ -1323,13 +1329,11 @@ Proof.
   destruct (eq_block b2 b3); auto.
   exploit Mem.different_pointers_inject; eauto. intros [A|A]. 
   congruence.
-  decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp.
+  decEq. destruct c; simpl in H6; inv H6; unfold Int.cmpu.
   predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
   congruence. auto.
   predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)).
   congruence. auto.
-  (* cmpu *)
-  inv H0; try discriminate; inv H1; inv H; TrivialOp.
   (* cmpf *)
   inv H0; try discriminate; inv H1; inv H; TrivialOp.
 Qed.
@@ -1831,7 +1835,7 @@ Lemma match_callstack_alloc_variable:
   Mem.valid_block tm sp ->
   Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
   Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
-  tf.(fn_stackspace) <= Int.max_signed ->
+  tf.(fn_stackspace) <= Int.max_unsigned ->
   Mem.alloc m 0 (sizeof lv) = (m', b) ->
   match_callstack f m tm 
                   (Frame cenv tf e le te sp lo (Mem.nextblock m) :: cs)
@@ -1862,9 +1866,8 @@ Proof.
     generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS.
     exploit Mem.alloc_left_mapped_inject.
       eauto. eauto. eauto. 
-      instantiate (1 := ofs). 
-      generalize Int.min_signed_neg. omega.
-      right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega.
+      instantiate (1 := ofs). omega. 
+      right; rewrite BOUNDS; simpl. omega.
       intros. apply Mem.perm_implies with Freeable; auto with mem.
       apply PERMS. rewrite LV in H1. simpl in H1. omega.
       rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. 
@@ -1923,7 +1926,7 @@ Lemma match_callstack_alloc_variables_rec:
   Mem.valid_block tm sp ->
   Mem.bounds tm sp = (0, tf.(fn_stackspace)) ->
   Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable ->
-  tf.(fn_stackspace) <= Int.max_signed ->
+  tf.(fn_stackspace) <= Int.max_unsigned ->
   forall e m vars e' m',
   alloc_variables e m vars e' m' ->
   forall f cenv sz,
@@ -2016,7 +2019,7 @@ Qed.
 Lemma match_callstack_alloc_variables:
   forall fn cenv tf m e m' tm tm' sp f cs targs,
   build_compilenv gce fn = (cenv, tf.(fn_stackspace)) ->
-  tf.(fn_stackspace) <= Int.max_signed ->
+  tf.(fn_stackspace) <= Int.max_unsigned ->
   list_norepet (fn_params_names fn ++ fn_vars_names fn) ->
   alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' ->
   Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) ->
@@ -2200,7 +2203,7 @@ Lemma function_entry_ok:
   bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 ->
   match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) ->
   build_compilenv gce fn = (cenv, tf.(fn_stackspace)) ->
-  tf.(fn_stackspace) <= Int.max_signed ->
+  tf.(fn_stackspace) <= Int.max_unsigned ->
   Mem.alloc tm 0 tf.(fn_stackspace) = (tm1, sp) ->
   let tparams := List.map for_var (fn_params_names fn) in
   let tvars := List.map for_var (fn_vars_names fn) in
@@ -2924,7 +2927,7 @@ Proof.
 (* internal call *)
   monadInv TR. generalize EQ; clear EQ; unfold transl_function.
   caseEq (build_compilenv gce f). intros ce sz BC.
-  destruct (zle sz Int.max_signed); try congruence.
+  destruct (zle sz Int.max_unsigned); try congruence.
   intro TRBODY.
   generalize TRBODY; intro TMP. monadInv TMP.
   set (tf := mkfunction (Csharpminor.fn_sig f) 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index dff5fa2..3a3ba3b 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -413,19 +413,24 @@ Function sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
   match classify_cmp t1 t2 with
-  | cmp_case_iiu =>
+  | cmp_case_ii Signed =>
+      match v1,v2 with
+      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
+      | _,  _ => None
+      end
+  | cmp_case_ii Unsigned =>
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | _,  _ => None
       end
-  | cmp_case_ipip =>
+  | cmp_case_pp =>
       match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
+      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
-          if Mem.valid_pointer m b1 (Int.signed ofs1)
-          && Mem.valid_pointer m b2 (Int.signed ofs2) then
+          if Mem.valid_pointer m b1 (Int.unsigned ofs1)
+          && Mem.valid_pointer m b2 (Int.unsigned ofs2) then
             if zeq b1 b2
-            then Some (Val.of_bool (Int.cmp c ofs1 ofs2))
+            then Some (Val.of_bool (Int.cmpu c ofs1 ofs2))
             else sem_cmp_mismatch c
           else None
       | Vptr b ofs, Vint n =>
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 2f05678..d2eb3c1 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -267,17 +267,7 @@ Definition eval_constant (cst: constant) : option val :=
 
 Definition eval_unop := Cminor.eval_unop.
 
-Definition eval_binop (op: binary_operation)
-                      (arg1 arg2: val) (m: mem): option val :=
-  match op, arg1, arg2 with
-  | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 =>
-      if Mem.valid_pointer m b1 (Int.signed n1)
-      && Mem.valid_pointer m b2 (Int.signed n2)
-      then Cminor.eval_binop op arg1 arg2
-      else None
-  | _, _, _ =>
-      Cminor.eval_binop op arg1 arg2
-  end.
+Definition eval_binop := Cminor.eval_binop.
 
 (** Allocation of local variables at function entry.  Each variable is
   bound to the reference to a fresh block of the appropriate size. *)
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 87dfc87..f1f7c0a 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -199,8 +199,9 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
 
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
-  | cmp_case_iiu => OK (Ebinop (Ocmpu c) e1 e2)
-  | cmp_case_ipip => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_case_ii Signed => OK (Ebinop (Ocmp c) e1 e2)
+  | cmp_case_ii Unsigned => OK (Ebinop (Ocmpu c) e1 e2)
+  | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
   | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
   | cmp_case_if sg => OK (Ebinop (Ocmpf c) (make_floatofint e1 sg) e2)
   | cmp_case_fi sg => OK (Ebinop (Ocmpf c) e1 (make_floatofint e2 sg))
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 3f6aa62..457f0d1 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -585,19 +585,21 @@ Lemma make_cmp_correct:
 Proof.
   intros until m. intro SEM. unfold make_cmp.
   functional inversion SEM; rewrite H0; intros.
-  (* iiu *) 
+  (** ii Signed *)
+  inversion H8; eauto with cshm.
+  (* ii Unsigned *) 
   inversion H8. eauto with cshm.
-  (* ipip int int *)
+  (* pp int int *)
   inversion H8. eauto with cshm.
-  (* ipip ptr ptr *)
+  (* pp ptr ptr *)
   inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
   inversion H10. eapply eval_Ebinop; eauto with cshm.
   simpl. rewrite H3. unfold eq_block. rewrite H9. auto.
-  (* ipip ptr int *)
+  (* pp ptr int *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
   simpl. unfold eval_compare_null. rewrite H8. auto.
-  (* ipip int ptr *)
+  (* pp int ptr *)
   inversion H9. eapply eval_Ebinop; eauto with cshm.
   simpl. unfold eval_compare_null. rewrite H8. auto.
   (* ff *)
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 8560d5e..a199f33 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -893,8 +893,8 @@ Definition classify_shift (ty1: type) (ty2: type) :=
 end.
 
 Inductive classify_cmp_cases : Type:=
-  | cmp_case_iiu               (**r unsigned int, unsigned int *)
-  | cmp_case_ipip              (**r int-or-pointer, int-or-pointer *)
+  | cmp_case_ii(s: signedness) (**r int, int *)
+  | cmp_case_pp                (**r pointer, pointer *)
   | cmp_case_ff                (**r float , float *)
   | cmp_case_if(s: signedness) (**r int, float *)
   | cmp_case_fi(s: signedness) (**r float, int *)
@@ -902,15 +902,15 @@ Inductive classify_cmp_cases : Type:=
 
 Definition classify_cmp (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with 
-  | Tint I32 Unsigned , Tint _ _ => cmp_case_iiu
-  | Tint _ _ , Tint I32 Unsigned => cmp_case_iiu
-  | Tint _ _ , Tint _ _ => cmp_case_ipip
+  | Tint I32 Unsigned , Tint _ _ => cmp_case_ii Unsigned
+  | Tint _ _ , Tint I32 Unsigned => cmp_case_ii Unsigned
+  | Tint _ _ , Tint _ _ => cmp_case_ii Signed
   | Tfloat _ , Tfloat _ => cmp_case_ff
   | Tint _ sg, Tfloat _ => cmp_case_if sg
   | Tfloat _, Tint _ sg => cmp_case_fi sg
-  | Tpointer _ , Tpointer _ => cmp_case_ipip
-  | Tpointer _ , Tint _ _ => cmp_case_ipip
-  | Tint _ _, Tpointer _ => cmp_case_ipip
+  | Tpointer _ , Tpointer _ => cmp_case_pp
+  | Tpointer _ , Tint _ _ => cmp_case_pp
+  | Tint _ _, Tpointer _ => cmp_case_pp
   | _ , _ => cmp_default
   end.
 
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index e8f1f9f..10206af 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -336,13 +336,14 @@ Lemma sem_cmp_match:
   match_val v1 v1' -> match_val v2 v2' ->
   match_val v v'.
 Proof.
+Opaque zeq.
   intros. unfold sem_cmp in *.
-  destruct (classify_cmp ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
+  destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
   destruct (Int.eq n Int.zero); try discriminate. 
   unfold sem_cmp_mismatch in *. destruct c; inv H3; inv H2; constructor.
   destruct (Int.eq n Int.zero); try discriminate. 
   unfold sem_cmp_mismatch in *. destruct c; inv H2; inv H1; constructor.
-  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.signed ofs)) in H4. discriminate.
+  rewrite (mem_empty_not_valid_pointer (Zpos id) (Int.unsigned ofs)) in H4. discriminate.
 Qed.
 
 Lemma sem_binary_match: