From 59948b3348964f4b16f408ffe690f2c78ca80959 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Mar 2019 17:41:27 +0100 Subject: Added double comparisons --- mppa_k1c/Asmblockgenproof1.v | 70 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) (limited to 'mppa_k1c/Asmblockgenproof1.v') diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index e6093290..76404257 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1034,6 +1034,72 @@ Proof. destruct (Float32.cmp _ _ _); auto. Qed. +Lemma swap_comparison_cmpf: + forall v1 v2 cmp, + Val.lessdef (Val.cmpf cmp v1 v2) (Val.cmpf (swap_comparison cmp) v2 v1). +Proof. + intros. unfold Val.cmpf. unfold Val.cmpf_bool. destruct v1; destruct v2; auto. + rewrite Float.cmp_swap. auto. +Qed. + +Lemma transl_cond_float64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_float64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.cmpf cmp rs#r1 rs#r2) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. apply swap_comparison_cmpf. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. +Qed. + +Lemma transl_cond_nofloat64_correct: + forall cmp rd r1 r2 k rs m, + exists rs', + exec_straight ge (basics_to_code (transl_cond_notfloat64 cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m + /\ Val.lessdef (Val.of_optbool (option_map negb (Val.cmpf_bool cmp (rs r1) (rs r2)))) rs'#rd + /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. +Proof. + intros. destruct cmp; simpl. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. + rewrite Float.cmp_ne_eq. simpl. destruct (Float.cmp Ceq f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp Clt f f0); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap. + destruct (Float.cmp _ _ _); auto. +- econstructor; split. apply exec_straight_one; [simpl; eauto]. + split; intros; Simpl. + unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. + destruct (Float.cmp _ _ _); auto. +Qed. + Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> @@ -1069,6 +1135,10 @@ Proof. exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite MKTOT; eauto. ++ (* cmpfloat *) + exploit transl_cond_float64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. ++ (* cmpnosingle *) + exploit transl_cond_nofloat64_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpsingle *) exploit transl_cond_float32_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpnosingle *) -- cgit