From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: 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 --- ia32/Asmgenproof1.v | 105 +++++++++++++++++++++++++++------------------------- 1 file changed, 55 insertions(+), 50 deletions(-) (limited to 'ia32/Asmgenproof1.v') diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index aef03dbd..81154f9c 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,24 +1231,18 @@ 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). @@ -1252,7 +1250,14 @@ Proof. 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. -- cgit