From d4e023d87ec851ca3b670b45327c95600f4afee4 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 7 Mar 2019 16:26:28 +0100 Subject: Fix minor proof --- mppa_k1c/Asmblockgen.v | 62 ++++++++++++++++++------------ mppa_k1c/Asmblockgenproof.v | 16 +++++++- mppa_k1c/Asmblockgenproof1.v | 91 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 142 insertions(+), 27 deletions(-) diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index edffd879..8c6457a6 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -190,14 +190,29 @@ Definition transl_opt_compluimm loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) . -(* match select_compl n c with - | Some Ceq => Pcbu BTdeqz r1 lbl ::g k - | Some Cne => Pcbu BTdnez r1 lbl ::g k - | Some _ => nil (* Never happens *) - | None => loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) - end - . - *) +Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_float64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := @@ -234,23 +249,19 @@ Definition transl_cbranch else loadimm64 RTMP n ::g (transl_compl c Signed r1 RTMP lbl k) ) -(*| Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) -*)| _, _ => + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float64 c r1 r2 lbl k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat64 c r1 r2 lbl k) + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float32 c r1 r2 lbl k) + | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat32 c r1 r2 lbl k) + | _, _ => Error(msg "Asmgenblock.transl_cbranch") end. @@ -282,6 +293,7 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k. + Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := match ftest_for_cmp cmp with | Normal ft => Pfcompw ft rd r1 r2 ::i k diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index 1ac9a211..84877488 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -891,6 +891,10 @@ Proof. + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; simpl; eauto. * unfold transl_opt_compuimm. exploreInst; simpl; eauto. * unfold transl_opt_compluimm. exploreInst; simpl; eauto. + * unfold transl_comp_float64. exploreInst; simpl; eauto. + * unfold transl_comp_notfloat64. exploreInst; simpl; eauto. + * unfold transl_comp_float32. exploreInst; simpl; eauto. + * unfold transl_comp_notfloat32. exploreInst; simpl; eauto. + simpl in TIC. inv TIC. + simpl in TIC. monadInv TIC. simpl. eauto. - monadInv TIC. simpl; auto. @@ -990,6 +994,10 @@ Proof. + simpl in TIC. unfold transl_cbranch in TIC. exploreInst; try discriminate. * unfold transl_opt_compuimm. exploreInst; try discriminate. * unfold transl_opt_compluimm. exploreInst; try discriminate. + * unfold transl_comp_float64. exploreInst; try discriminate. + * unfold transl_comp_notfloat64. exploreInst; try discriminate. + * unfold transl_comp_float32. exploreInst; try discriminate. + * unfold transl_comp_notfloat32. exploreInst; try discriminate. - contradict Hnonil; auto. Qed. @@ -1005,8 +1013,12 @@ Proof. - assert False. eapply Hnobuiltin; eauto. destruct H. - unfold transl_cbranch in TIC. exploreInst. all: try discriminate. - + unfold transl_opt_compuimm. exploreInst. all: try discriminate. - + unfold transl_opt_compluimm. exploreInst. all: try discriminate. + * unfold transl_opt_compuimm. exploreInst. all: try discriminate. + * unfold transl_opt_compluimm. exploreInst. all: try discriminate. + * unfold transl_comp_float64. exploreInst; try discriminate. + * unfold transl_comp_notfloat64. exploreInst; try discriminate. + * unfold transl_comp_float32. exploreInst; try discriminate. + * unfold transl_comp_notfloat32. exploreInst; try discriminate. Qed. Theorem match_state_codestate: diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 76404257..b3519064 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -427,6 +427,69 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compf_correct: + forall cmp r1 r2 lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_comp_float64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmpf_bool cmp rs#r1 rs#r2 = Some b -> + exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m + = eval_branch fn lbl (nextblock tbb rs') m (Some b)) + . +Proof. Admitted. +(* intros. esplit. split. +- unfold transl_compl. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)) as rs'. + simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). + { + assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Signed) rs # r1 rs # r2 m)). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmpl_bool cmp rs#r1 rs#r2) as cmpbool. + destruct cmp; simpl; + unfold compare_long; + unfold Val.cmpl; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. *) + +Lemma transl_compnotf_correct: + forall cmp r1 r2 lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_comp_notfloat64 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ (option_map negb (Val.cmpf_bool cmp rs#r1 rs#r2) = Some b -> + exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m + = eval_branch fn lbl (nextblock tbb rs') m (Some b)) + . +Proof. Admitted. + +Lemma transl_compfs_correct: + forall cmp r1 r2 lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_comp_float32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmpfs_bool cmp rs#r1 rs#r2 = Some b -> + exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m + = eval_branch fn lbl (nextblock tbb rs') m (Some b)) + . +Proof. Admitted. + +Lemma transl_compnotfs_correct: + forall cmp r1 r2 lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_comp_notfloat32 cmp r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ (option_map negb (Val.cmpfs_bool cmp rs#r1 rs#r2) = Some b -> + exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m + = eval_branch fn lbl (nextblock tbb rs') m (Some b)) + . +Proof. Admitted. + Lemma transl_complu_correct: forall cmp r1 r2 lbl k rs m tbb b, exists rs', @@ -751,6 +814,34 @@ Proof. * split; auto. { apply C'; auto. rewrite B, C; eauto with asmgen. } { intros. rewrite B'; eauto with asmgen. } + +(* Ccompf *) +- exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez RTMP lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. + +(* Cnotcompf *) +- exploit (transl_compnotf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez RTMP lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. + +(* Ccompfs *) +- exploit (transl_compfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez RTMP lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. + +(* Cnotcompfs *) +- exploit (transl_compnotfs_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). + exists rs', (Pcb BTwnez RTMP lbl). + split. + + constructor. eexact A. + + split; auto. apply C; auto. Qed. Lemma transl_cbranch_correct_true: -- cgit