Pointers one past

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

4 files changed, 60 insertions, 91 deletions

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index b78dfb6..05e7010 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -57,9 +57,9 @@ Definition is_immed_mem_float (x: int) : bool :=
 Fixpoint decompose_int_rec (N: nat) (n p: int) : list int :=
   match N with
   | Datatypes.O =>
-      if Int.eq_dec n Int.zero then nil else n :: nil
+      if Int.eq n Int.zero then nil else n :: nil
   | Datatypes.S M =>
-      if Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
+      if Int.eq (Int.and n (Int.shl (Int.repr 3) p)) Int.zero then
         decompose_int_rec M n (Int.add p (Int.repr 2))
       else
         let m := Int.shl (Int.repr 255) p in
@@ -86,14 +86,14 @@ Definition iterate_op (op1 op2: shift_op -> instruction) (l: list int) (k: code)
 Definition loadimm (r: ireg) (n: int) (k: code) :=
   let d1 := decompose_int n in
   let d2 := decompose_int (Int.not n) in
-  if le_dec (List.length d1) (List.length d2)
+  if NPeano.leb (List.length d1) (List.length d2)
   then iterate_op (Pmov r) (Porr r r) d1 k
   else iterate_op (Pmvn r) (Pbic r r) d2 k.
 
 Definition addimm (r1 r2: ireg) (n: int) (k: code) :=
   let d1 := decompose_int n in
   let d2 := decompose_int (Int.neg n) in
-  if le_dec (List.length d1) (List.length d2)
+  if NPeano.leb (List.length d1) (List.length d2)
   then iterate_op (Padd r1 r2) (Padd r1 r1) d1 k
   else iterate_op (Psub r1 r2) (Psub r1 r1) d2 k.
 
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index b0598e9..365917c 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -348,7 +348,7 @@ Remark loadimm_label:
   forall r n k, find_label lbl (loadimm r n k) = find_label lbl k.
 Proof.
   intros. unfold loadimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n))));
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n))));
   auto with labels.
 Qed.
 Hint Rewrite loadimm_label: labels.
@@ -357,7 +357,7 @@ Remark addimm_label:
   forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k.
 Proof.
   intros; unfold addimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n))));
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n))));
   auto with labels.
 Qed.
 Hint Rewrite addimm_label: labels.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 19edcd9..658fc98 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -480,10 +480,10 @@ Lemma decompose_int_rec_or:
   forall N n p x, List.fold_left Int.or (decompose_int_rec N n p) x = Int.or x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.or_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.or_assoc. decEq. rewrite <- Int.and_or_distrib.
   rewrite Int.or_not_self. apply Int.and_mone.
@@ -493,10 +493,10 @@ Lemma decompose_int_rec_xor:
   forall N n p x, List.fold_left Int.xor (decompose_int_rec N n p) x = Int.xor x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.xor_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.xor_assoc. decEq. rewrite <- Int.and_xor_distrib.
   rewrite Int.xor_not_self. apply Int.and_mone.
@@ -506,10 +506,10 @@ Lemma decompose_int_rec_add:
   forall N n p x, List.fold_left Int.add (decompose_int_rec N n p) x = Int.add x n.
 Proof.
   induction N; intros; simpl.
-  destruct (Int.eq_dec n Int.zero); simpl. 
+  predSpec Int.eq Int.eq_spec n Int.zero; simpl.
   subst n. rewrite Int.add_zero. auto.
   auto.
-  destruct (Int.eq_dec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero).
+  predSpec Int.eq Int.eq_spec (Int.and n (Int.shl (Int.repr 3) p)) Int.zero.
   auto.
   simpl. rewrite IHN. rewrite Int.add_assoc. decEq. rewrite Int.add_and. 
   rewrite Int.or_not_self. apply Int.and_mone. apply Int.and_not_self.
@@ -647,7 +647,7 @@ Lemma loadimm_correct:
   /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold loadimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.not n)))).
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))).
   (* mov - orr* *)
   replace (Vint n) with (List.fold_left (fun v i => Val.or v (Vint i)) (decompose_int n) Vzero).
   apply iterate_op_correct.
@@ -672,7 +672,7 @@ Lemma addimm_correct:
   /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
 Proof.
   intros. unfold addimm.
-  destruct (le_dec (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
+  destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))).
   (* add - add* *)
   replace (Val.add (rs r2) (Vint n))
      with (List.fold_left (fun v i => Val.add v (Vint i)) (decompose_int n) (rs r2)).
diff --git a/arm/Op.v b/arm/Op.v
index f26bccc..291d64f 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -697,10 +697,16 @@ Hypothesis valid_pointer_inj:
   Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
 
-Hypothesis valid_pointer_no_overflow:
+Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
@@ -728,25 +734,6 @@ Ltac InvInject :=
   | _ => idtac
   end.
 
-Remark val_add_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.add v1 v2) (Val.add v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; econstructor; eauto. 
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-Qed.
-
-Remark val_sub_inj:
-  forall v1 v1' v2 v2',
-  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.sub v1 v2) (Val.sub v1' v2').
-Proof.
-  intros. inv H; inv H0; simpl; auto.
-  econstructor; eauto. rewrite Int.sub_add_l. auto.
-  destruct (zeq b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite zeq_true. 
-  rewrite Int.sub_shifted. auto.
-Qed.
-
 Remark eval_shift_inj:
   forall s v v', val_inject f v v' -> val_inject f (eval_shift s v) (eval_shift s v').
 Proof.
@@ -759,45 +746,13 @@ Lemma eval_condition_inj:
   eval_condition cond vl1 m1 = Some b ->
   eval_condition cond vl2 m2 = Some b.
 Proof.
-Opaque Int.add.
-  assert (CMP:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmp_bool c v1 v2 = Some b ->
-    Val.cmp_bool c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-
-  assert (CMPU:
-    forall c v1 v2 v1' v2' b,
-    val_inject f v1 v1' ->
-    val_inject f v2 v2' ->
-    Val.cmpu_bool (Mem.valid_pointer m1) c v1 v2 = Some b ->
-    Val.cmpu_bool (Mem.valid_pointer m2) c v1' v2' = Some b).
-  intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto.
-  destruct (Mem.valid_pointer m1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  rewrite (valid_pointer_inj _ H2 Heqb4).
-  rewrite (valid_pointer_inj _ H Heqb0). simpl.
-  destruct (zeq b1 b0); simpl in H1.
-  inv H1. rewrite H in H2; inv H2. rewrite zeq_true. 
-  decEq. apply Int.translate_cmpu.
-  eapply valid_pointer_no_overflow; eauto.
-  eapply valid_pointer_no_overflow; eauto.
-  exploit valid_different_pointers_inj; eauto. intros P.
-  destruct (zeq b2 b3); auto.
-  destruct P. congruence. 
-  destruct c; simpl in H1; inv H1.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-  simpl; decEq. rewrite Int.eq_false; auto. congruence.
-
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl.
-  eapply CMP; eauto.
-  eapply CMPU; eauto.
-  eapply CMP. eauto. eapply eval_shift_inj. eauto. auto.
-  eapply CMPU. eauto. eapply eval_shift_inj. eauto. auto.
-  eapply CMP; try eassumption; eauto.
-  eapply CMPU; try eassumption; eauto.
+  eauto 4 using val_cmp_bool_inject.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
+  eauto using val_cmp_bool_inject, eval_shift_inj.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies, eval_shift_inj.
+  eauto 4 using val_cmp_bool_inject.
+  eauto 4 using val_cmpu_bool_inject, Mem.valid_pointer_implies.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; inv H2; simpl in H0; inv H0; auto.
   inv H3; simpl in H0; inv H0; auto.
@@ -819,15 +774,15 @@ Lemma eval_operation_inj:
   exists v2, eval_operation genv sp2 op vl2 m2 = Some v2 /\ val_inject f v1 v2.
 Proof.
   intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply eval_shift_inj; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_add_inject; auto.
 
-  apply val_sub_inj; auto.
-  apply val_sub_inj; auto. apply eval_shift_inj; auto.
-  apply val_sub_inj; auto. apply eval_shift_inj; auto.
-  apply (@val_sub_inj (Vint i) (Vint i) v v'); auto.
+  apply Values.val_sub_inject; auto.
+  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_sub_inject; auto. apply eval_shift_inj; auto.
+  apply (@Values.val_sub_inject f (Vint i) (Vint i) v v'); auto.
 
   inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
@@ -888,10 +843,10 @@ Proof.
             val_inject f (symbol_address genv id ofs) (symbol_address genv id ofs)).
   exact symbol_address_inj.
   intros. destruct addr; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto.
-  apply val_add_inj; auto. apply eval_shift_inj; auto.
-  apply val_add_inj; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto.
+  apply Values.val_add_inject; auto. apply eval_shift_inj; auto.
+  apply Values.val_add_inject; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -913,10 +868,20 @@ Proof.
   intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. 
 Qed.
 
-Remark valid_pointer_no_overflow_extends:
+Remark weak_valid_pointer_extends:
+  forall m1 m2, Mem.extends m1 m2 ->
+  forall b1 ofs b2 delta,
+  Some(b1, 0) = Some(b2, delta) ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+Proof.
+  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+Qed.
+
+Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
   0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
 Proof.
   intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
@@ -944,7 +909,8 @@ Lemma eval_condition_lessdef:
 Proof.
   intros. eapply eval_condition_inj with (f := fun b => Some(b, 0)) (m1 := m1).
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_list_inject_lessdef. eauto. auto.
 Qed.
@@ -963,7 +929,8 @@ Proof.
   eapply eval_operation_inj with (m1 := m1) (sp1 := sp).
   intros. rewrite <- val_inject_lessdef; auto.
   apply valid_pointer_extends; auto.
-  apply valid_pointer_no_overflow_extends; auto. 
+  apply weak_valid_pointer_extends; auto.
+  apply weak_valid_pointer_no_overflow_extends.
   apply valid_different_pointers_extends; auto.
   rewrite <- val_inject_lessdef; auto.
   eauto. auto. 
@@ -1019,7 +986,8 @@ Lemma eval_condition_inject:
 Proof.
   intros. eapply eval_condition_inj with (f := f) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.
 
@@ -1051,7 +1019,8 @@ Proof.
   eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
   exact symbol_address_inject.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
-  intros; eapply Mem.valid_pointer_inject_no_overflow; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
+  intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
 Qed.