diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/SelectLong.vp | 38 | ||||
-rw-r--r-- | backend/SelectLongproof.v | 20 | ||||
-rw-r--r-- | backend/ValueDomain.v | 14 |
3 files changed, 40 insertions, 32 deletions
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 09f29afc..0c1cbb3a 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -27,10 +27,10 @@ Open Local Scope cminorsel_scope. the names of these functions. *) Record helper_functions : Type := mk_helper_functions { - i64_dtos: ident; (**r float -> signed long *) - i64_dtou: ident; (**r float -> unsigned long *) - i64_stod: ident; (**r signed long -> float *) - i64_utod: ident; (**r unsigned long -> float *) + i64_dtos: ident; (**r float64 -> signed long *) + i64_dtou: ident; (**r float64 -> unsigned long *) + i64_stod: ident; (**r signed long -> float64 *) + i64_utod: ident; (**r unsigned long -> float64 *) i64_stof: ident; (**r signed long -> float32 *) i64_utof: ident; (**r unsigned long -> float32 *) i64_neg: ident; (**r opposite *) @@ -304,13 +304,16 @@ Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := Definition cmplu (c: comparison) (e1 e2: expr) := match c with | Ceq => - if is_longconst_zero e2 - then cmpl_eq_zero e1 - else cmpl_eq_zero (xorl e1 e2) + cmpl_eq_zero (xorl e1 e2) +(* + (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Cne => - if is_longconst_zero e2 - then cmpl_ne_zero e1 - else cmpl_ne_zero (xorl e1 e2) + cmpl_ne_zero (xorl e1 e2) +(* (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Clt => cmplu_gen Clt Clt e1 e2 | Cle => @@ -330,13 +333,16 @@ Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := Definition cmpl (c: comparison) (e1 e2: expr) := match c with | Ceq => - if is_longconst_zero e2 - then cmpl_eq_zero e1 - else cmpl_eq_zero (xorl e1 e2) + cmpl_eq_zero (xorl e1 e2) +(* + (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Cne => - if is_longconst_zero e2 - then cmpl_ne_zero e1 - else cmpl_ne_zero (xorl e1 e2) + cmpl_ne_zero (xorl e1 e2) +(* (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Clt => if is_longconst_zero e2 then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 26f33dab..ec0dd2cd 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -1024,16 +1024,10 @@ Proof. 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; inv EQ; clear H0. - apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + 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; inv EQ; clear H0. - apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B. inv B. + 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. @@ -1095,16 +1089,10 @@ Proof. 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; inv EQ; clear H0. - apply eval_cmpl_eq_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + 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; inv EQ; clear H0. - apply eval_cmpl_ne_zero; auto. -+ exploit eval_xorl. eexact H. eexact H0. intros [v1 [A B]]. simpl in B; inv B. + 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. diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index 239dd474..2ece8cdb 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -681,6 +681,14 @@ Qed. Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va. +Lemma is_uns_1: + forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one. +Proof. + intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros. + rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega. + rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega. +Qed. + (** Smart constructors for [Uns] and [Sgn]. *) Definition uns (n: Z) : aval := @@ -749,6 +757,12 @@ Qed. Hint Resolve vmatch_uns vmatch_uns_undef vmatch_sgn vmatch_sgn_undef : va. +Lemma vmatch_Uns_1: + forall v, vmatch v (Uns 1) -> v = Vundef \/ v = Vint Int.zero \/ v = Vint Int.one. +Proof. + intros. inv H; auto. right. exploit is_uns_1; eauto. intuition congruence. +Qed. + (** Ordering *) Inductive vge: aval -> aval -> Prop := |