From 5c84fd4adbcd8a63cc29fb0286cb46f18abde55c Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Apr 2013 17:11:47 +0000 Subject: Expand 64-bit integer comparisons into 32-bit integer comparisons. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/SelectLongproof.v | 273 ++++++++++++++++++++++++++++------------------ 1 file changed, 165 insertions(+), 108 deletions(-) (limited to 'backend/SelectLongproof.v') diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index aca05bf..3eeeeb5 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -61,11 +61,7 @@ Definition i64_helpers_correct (hf: helper_functions) : Prop := /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z) /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y)) /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y)) - /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)) - /\(forall c x y, exists z, helper_implements hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - /\(forall c x y, exists z, helper_implements hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero). + /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)). End HELPERS. @@ -180,6 +176,22 @@ Proof. destruct v; try (rewrite UNDEF; auto). erewrite B; simpl; eauto. rewrite Int64.ofwords_recompose. auto. Qed. +Lemma eval_splitlong_strict: + forall le a f va v, + eval_expr ge sp e m le a (Vlong va) -> + (forall le a1 a2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le (f a1 a2) v) -> + eval_expr ge sp e m le (splitlong a f) v. +Proof. + intros until v. + unfold splitlong. case (splitlong_match a); intros. +- InvEval. destruct v1; simpl in H; try discriminate. destruct v0; inv H. + apply H0. rewrite Int64.hi_ofwords; auto. rewrite Int64.lo_ofwords; auto. +- EvalOp. apply H0; EvalOp. +Qed. + Lemma eval_splitlong2: forall le a b f va vb sem, (forall le a1 a2 b1 b2 x1 x2 y1 y2, @@ -198,7 +210,7 @@ Lemma eval_splitlong2: exists v, eval_expr ge sp e m le (splitlong2 a b f) v /\ Val.lessdef (sem va vb) v. Proof. intros until sem; intros EXEC UNDEF. - unfold splitlong2. case (splitlong2_match a); intros. + unfold splitlong2. case (splitlong2_match a b); intros. - InvEval. subst va vb. exploit (EXEC le h1 l1 h2 l2); eauto. intros [v [A B]]. exists v; split; auto. @@ -240,6 +252,35 @@ Proof. erewrite B; simpl; eauto. rewrite ! Int64.ofwords_recompose; auto. Qed. +Lemma eval_splitlong2_strict: + forall le a b f va vb v, + eval_expr ge sp e m le a (Vlong va) -> + eval_expr ge sp e m le b (Vlong vb) -> + (forall le a1 a2 b1 b2, + eval_expr ge sp e m le a1 (Vint (Int64.hiword va)) -> + eval_expr ge sp e m le a2 (Vint (Int64.loword va)) -> + eval_expr ge sp e m le b1 (Vint (Int64.hiword vb)) -> + eval_expr ge sp e m le b2 (Vint (Int64.loword vb)) -> + eval_expr ge sp e m le (f a1 a2 b1 b2) v) -> + eval_expr ge sp e m le (splitlong2 a b f) v. +Proof. + assert (INV: forall v1 v2 n, + Val.longofwords v1 v2 = Vlong n -> v1 = Vint(Int64.hiword n) /\ v2 = Vint(Int64.loword n)). + { + intros. destruct v1; simpl in H; try discriminate. destruct v2; inv H. + rewrite Int64.hi_ofwords; rewrite Int64.lo_ofwords; auto. + } + intros until v. + unfold splitlong2. case (splitlong2_match a b); intros. +- InvEval. exploit INV. eexact H. intros [EQ1 EQ2]. exploit INV. eexact H0. intros [EQ3 EQ4]. + subst. auto. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- InvEval. exploit INV; eauto. intros [EQ1 EQ2]. subst. + econstructor. eauto. apply H1; EvalOp. +- EvalOp. apply H1; EvalOp. +Qed. + Lemma is_longconst_sound: forall le a x n, is_longconst a = Some n -> @@ -891,35 +932,49 @@ Proof. Qed. Lemma eval_cmpl_eq_zero: - unary_constructor_sound cmpl_eq_zero (fun v => Val.cmpl Ceq v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_eq_zero a) (Val.of_bool (Int64.eq x Int64.zero)). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Ceq x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_eq_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Ceq). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Ceq). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (Int64.eq x Int64.zero); inv B2; auto. Qed. Lemma eval_cmpl_ne_zero: - unary_constructor_sound cmpl_ne_zero (fun v => Val.cmpl Cne v (Vlong Int64.zero)). + forall le a x, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le (cmpl_ne_zero a) (Val.of_bool (negb (Int64.eq x Int64.zero))). Proof. - red; intros. unfold cmpl_eq_zero. - apply eval_splitlong with (sem := fun x => Val.cmpl Cne x (Vlong Int64.zero)); auto. -- intros. - exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. + intros. unfold cmpl_ne_zero. + eapply eval_splitlong_strict; eauto. intros. + exploit eval_or. eexact H0. eexact H1. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := Cne). intros [v2 [A2 B2]]. - exists v2; split. auto. intros; subst. - simpl in B1; inv B1. unfold Val.cmp in B2; simpl in B2. - unfold Val.cmpl; simpl. rewrite decompose_cmpl_eq_zero. - destruct (Int.eq (Int.or p q)); inv B2; auto. -- destruct x; auto. + instantiate (1 := Cne). intros [v2 [A2 B2]]. + unfold Val.cmp in B2; simpl in B2. + rewrite <- decompose_cmpl_eq_zero in B2. + rewrite Int64.ofwords_recompose in B2. + destruct (negb (Int64.eq x Int64.zero)); inv B2; auto. +Qed. + +Lemma eval_cmplu_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmplu_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmpu ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmplu_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark int64_eq_xor: @@ -933,44 +988,57 @@ Proof. auto. Qed. -Theorem eval_cmplu: forall c, binary_constructor_sound (cmplu hf c) (Val.cmplu c). +Theorem eval_cmplu: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmplu c x y = Some v -> + eval_expr ge sp e m le (cmplu c a b) v. Proof. - intros; red; intros. unfold cmplu. - set (default := comp c (Eexternal (i64_ucmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmplu c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_ucmp) sig_ll_i (x::y::nil) z - /\ Val.cmplu c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmplu in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmplu, Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. +- (* Clt *) + exploit (eval_cmplu_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmplu_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. auto. +- (* Cgt *) + exploit (eval_cmplu_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_ltu. rewrite ! Int64.ofwords_recompose. auto. +- (* Cge *) + exploit (eval_cmplu_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_leu. rewrite Int.eq_sym. auto. +Qed. + +Lemma eval_cmpl_gen: + forall ch cl a b le x y, + eval_expr ge sp e m le a (Vlong x) -> + eval_expr ge sp e m le b (Vlong y) -> + eval_expr ge sp e m le (cmpl_gen ch cl a b) + (Val.of_bool (if Int.eq (Int64.hiword x) (Int64.hiword y) + then Int.cmpu cl (Int64.loword x) (Int64.loword y) + else Int.cmp ch (Int64.hiword x) (Int64.hiword y))). +Proof. + intros. unfold cmpl_gen. eapply eval_splitlong2_strict; eauto. intros. + econstructor. econstructor. EvalOp. simpl. eauto. + destruct (Int.eq (Int64.hiword x) (Int64.hiword y)); EvalOp. Qed. Remark decompose_cmpl_lt_zero: @@ -991,72 +1059,61 @@ Proof. vm_compute. intuition congruence. Qed. -Theorem eval_cmpl: forall c, binary_constructor_sound (cmpl hf c) (Val.cmpl c). +Theorem eval_cmpl: + forall c le a x b y v, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.cmpl c x y = Some v -> + eval_expr ge sp e m le (cmpl c a b) v. Proof. - intros; red; intros. unfold cmpl. - set (default := comp c (Eexternal (i64_scmp hf) sig_ll_i (a ::: b ::: Enil)) - (Eop (Ointconst Int.zero) Enil)). - assert (DEFAULT: - exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.cmpl c x y) v). - { - assert (HELP: exists z, helper_implements ge hf.(i64_scmp) sig_ll_i (x::y::nil) z - /\ Val.cmpl c x y = Val.cmp c z Vzero) - by UseHelper. - destruct HELP as [z [A B]]. - exploit eval_comp. eapply eval_helper_2. eexact H. eexact H0. eauto. - instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. - instantiate (1 := c). fold Vzero. intros [v [C D]]. - econstructor; split; eauto. congruence. - } - destruct c; auto. + intros. unfold Val.cmpl in H1. + destruct x; simpl in H1; try discriminate. destruct y; inv H1. + rename i into x. rename i0 into y. + destruct c; simpl. - (* Ceq *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_eq_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_eq_zero; auto. - (* Cne *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v [A B]]. - exploit eval_cmpl_ne_zero. eexact A. intros [v' [C D]]. - exists v'; split; auto. - eapply Val.lessdef_trans; [idtac|eexact D]. - destruct x; auto. destruct y; auto. simpl in B; inv B. - unfold Val.cmpl; simpl. rewrite int64_eq_xor; auto. ++ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + rewrite int64_eq_xor. apply eval_cmpl_ne_zero; auto. - (* Clt *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1. inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Clt). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2. simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (Int.lt (Int64.hiword x) Int.zero); inv B2; auto. ++ exploit (eval_cmpl_gen Clt Clt). eexact H. eexact H0. simpl. + rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. +- (* Cle *) + exploit (eval_cmpl_gen Clt Cle). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. auto. +- (* Cgt *) + exploit (eval_cmpl_gen Cgt Cgt). eexact H. eexact H0. simpl. + rewrite Int.eq_sym. rewrite <- Int64.decompose_lt. rewrite ! Int64.ofwords_recompose. auto. - (* Cge *) destruct (is_longconst_zero b) eqn:LC. -+ exploit is_longconst_zero_sound; eauto. intros EQ; subst; clear H0. - exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. ++ exploit is_longconst_zero_sound; eauto. intros EQ; inv EQ; clear H0. + exploit eval_highlong. eexact H. intros [v1 [A1 B1]]. simpl in B1; inv B1. exploit eval_comp. eexact A1. instantiate (2 := Eop (Ointconst Int.zero) Enil). EvalOp. instantiate (1 := Cge). intros [v2 [A2 B2]]. - econstructor; split. eauto. - destruct x; simpl in *; auto. inv B1. - unfold Val.cmp, Val.cmp_bool, Val.of_optbool, Int.cmp in B2. - unfold Val.cmpl, Val.cmpl_bool, Val.of_optbool, Int64.cmp. - rewrite <- (Int64.ofwords_recompose i). rewrite decompose_cmpl_lt_zero. - auto. -+ apply DEFAULT. + unfold Val.cmp in B2; simpl in B2. + rewrite <- (Int64.ofwords_recompose x). rewrite decompose_cmpl_lt_zero. + destruct (negb (Int.lt (Int64.hiword x) Int.zero)); inv B2; auto. ++ exploit (eval_cmpl_gen Cgt Cge). eexact H. eexact H0. intros. + rewrite <- (Int64.ofwords_recompose x). rewrite <- (Int64.ofwords_recompose y). + rewrite Int64.decompose_le. rewrite Int.eq_sym. auto. Qed. End CMCONSTR. -- cgit v1.2.3