diff options
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 20 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 161 |
2 files changed, 145 insertions, 36 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index dc55715a..f2292f9a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -135,10 +135,18 @@ Definition transl_comp (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := Pcompw (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k. +Definition transl_compi + (c: comparison) (s: signedness) (r: ireg) (imm: int) (lbl: label) (k: code) : list instruction := + Pcompiw (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k. + Definition transl_compl (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction := Pcompl (itest_for_cmp c s) RTMP r1 r2 ::g Pcb BTwnez RTMP lbl ::g k. +Definition transl_compil + (c: comparison) (s: signedness) (r: ireg) (imm: int64) (lbl: label) (k: code) : list instruction := + Pcompil (itest_for_cmp c s) RTMP r imm ::g Pcb BTwnez RTMP lbl ::g k. + Definition select_comp (n: int) (c: comparison) : option comparison := if Int.eq n Int.zero then match c with @@ -156,10 +164,10 @@ Definition transl_opt_compuimm match c with | Ceq => Pcbu BTweqz r1 lbl ::g k | Cne => Pcbu BTwnez r1 lbl ::g k - | _ => loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k) + | _ => transl_compi c Unsigned r1 n lbl k end else - loadimm32 RTMP n ::g (transl_comp c Unsigned r1 RTMP lbl k) + transl_compi c Unsigned r1 n lbl k . (* Definition transl_opt_compuimm @@ -192,10 +200,10 @@ Definition transl_opt_compluimm match c with | Ceq => Pcbu BTdeqz r1 lbl ::g k | Cne => Pcbu BTdnez r1 lbl ::g k - | _ => loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) + | _ => transl_compil c Unsigned r1 n lbl k end else - loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) + transl_compil c Unsigned r1 n lbl k . Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := @@ -239,7 +247,7 @@ Definition transl_cbranch OK (if Int.eq n Int.zero then Pcb (btest_for_cmpswz c) r1 lbl ::g k else - loadimm32 RTMP n ::g (transl_comp c Signed r1 RTMP lbl k) + transl_compi c Signed r1 n lbl k ) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; @@ -255,7 +263,7 @@ Definition transl_cbranch OK (if Int64.eq n Int64.zero then Pcb (btest_for_cmpsdz c) r1 lbl ::g k else - loadimm64 RTMP n ::g (transl_compl c Signed r1 RTMP lbl k) + transl_compil c Signed r1 n lbl k ) | Ccompf c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 19b1b1f1..86a0ff88 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -340,6 +340,35 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compi_correct: + forall cmp r1 n lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_compi cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmp_bool cmp rs#r1 (Vint n) = 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. + intros. esplit. split. +- unfold transl_compi. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Signed) rs # r1 (Vint n))) as rs'. + simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). + { + assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Signed) rs # r1 (Vint n))). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmp_bool cmp rs#r1 (Vint n)) as cmpbool. + destruct cmp; simpl; + unfold Val.cmp; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + Lemma transl_compu_correct: forall cmp r1 r2 lbl k rs m tbb b, exists rs', @@ -369,6 +398,35 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compui_correct: + forall cmp r1 n lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_compi cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ (Val_cmpu_bool cmp rs#r1 (Vint n) = 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. + intros. esplit. split. +- unfold transl_compi. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (rs # RTMP <- (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))) as rs'. + simpl. assert (Val.cmp_bool Cne (nextblock tbb rs') # RTMP (Vint (Int.repr 0)) = Some b). + { + assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val_cmpu_bool cmp rs#r1 (Vint n)) as cmpubool. + destruct cmp; simpl; unfold Val_cmpu; + rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + Lemma transl_compl_correct: forall cmp r1 r2 lbl k rs m tbb b, exists rs', @@ -399,6 +457,36 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compil_correct: + forall cmp r1 n lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_compil cmp Signed r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val.cmpl_bool cmp rs#r1 (Vlong n) = 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. + intros. esplit. split. +- unfold transl_compil. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Signed) rs # r1 (Vlong n))) 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 (Vlong n))). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val.cmpl_bool cmp rs#r1 (Vlong n)) as cmpbool. + destruct cmp; simpl; + unfold compare_long, Val.cmpl; + rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + Lemma swap_comparison_cmpf_eq: forall v1 v2 cmp, (Val.cmpf cmp v1 v2) = (Val.cmpf (swap_comparison cmp) v2 v1). @@ -710,6 +798,35 @@ Proof. rewrite H0. simpl; auto. Qed. +Lemma transl_compilu_correct: + forall cmp r1 n lbl k rs m tbb b, + exists rs', + exec_straight ge (transl_compil cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m + /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) + /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = 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. + intros. esplit. split. +- unfold transl_compil. apply exec_straight_one; simpl; eauto. +- split. + + intros; Simpl. + + intros. + remember (rs # RTMP <- (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))) 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 Unsigned) rs # r1 (Vlong n))). + { rewrite Heqrs'. auto. } + rewrite H0. rewrite <- H. + remember (Val_cmplu_bool cmp rs#r1 (Vlong n)) as cmpbool. + destruct cmp; simpl; + unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + destruct b0; simpl; auto. + } + rewrite H0. simpl; auto. +Qed. + Lemma transl_opt_compuimm_correct: forall n cmp r1 lbl k rs m b tbb c, select_comp n cmp = Some c -> @@ -907,16 +1024,12 @@ Proof. unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. - + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C). - exploit (transl_comp_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C'). + + exploit (transl_compi_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C'). exists rs'2, (Pcb BTwnez RTMP lbl). split. - * constructor. apply exec_straight_trans - with (c2 := (transl_comp c0 Signed x RTMP lbl k)) (rs2 := rs') (m2 := m'). - eexact A. eexact A'. + * constructor. eexact A'. * split; auto. - { apply C'; auto. rewrite B, C; eauto with asmgen. } - { intros. rewrite B'; eauto with asmgen. } + { apply C'; auto. } (* Ccompuimm *) - remember (select_comp n c0) as selcomp. destruct selcomp. @@ -926,22 +1039,18 @@ Proof. split. * apply A. * split; auto. apply C. apply EVAL'. - + assert (transl_opt_compuimm n c0 x lbl k = loadimm32 RTMP n ::g transl_comp c0 Unsigned x RTMP lbl k). + + assert (transl_opt_compuimm n c0 x lbl k = transl_compi c0 Unsigned x n lbl k). { unfold transl_opt_compuimm. destruct (Int.eq n Int.zero) eqn:EQN. all: unfold select_comp in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto. all: discriminate. } rewrite H. clear H. - exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C). - exploit (transl_compu_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C'). + exploit (transl_compui_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C'). exists rs'2, (Pcb BTwnez RTMP lbl). split. - * constructor. apply exec_straight_trans - with (c2 := (transl_comp c0 Unsigned x RTMP lbl k)) (rs2 := rs') (m2 := m'). - eexact A. eexact A'. + * constructor. eexact A'. * split; auto. - { apply C'; auto. rewrite B, C; eauto with asmgen. } - { intros. rewrite B'; eauto with asmgen. } + { apply C'; auto. } (* Ccompl *) - exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). exists rs', (Pcb BTwnez RTMP lbl). @@ -970,16 +1079,12 @@ Proof. unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. - + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C). - exploit (transl_compl_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C'). + + exploit (transl_compil_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C'). exists rs'2, (Pcb BTwnez RTMP lbl). split. - * constructor. apply exec_straight_trans - with (c2 := (transl_compl c0 Signed x RTMP lbl k)) (rs2 := rs') (m2 := m'). - eexact A. eexact A'. + * constructor. eexact A'. * split; auto. - { apply C'; auto. rewrite B, C; eauto with asmgen. } - { intros. rewrite B'; eauto with asmgen. } + { apply C'; auto. } (* Ccompluimm *) - remember (select_compl n c0) as selcomp. @@ -990,22 +1095,18 @@ Proof. split. * apply A. * split; eauto. (* apply C. apply EVAL'. *) - + assert (transl_opt_compluimm n c0 x lbl k = loadimm64 RTMP n ::g transl_compl c0 Unsigned x RTMP lbl k). + + assert (transl_opt_compluimm n c0 x lbl k = transl_compil c0 Unsigned x n lbl k). { unfold transl_opt_compluimm. destruct (Int64.eq n Int64.zero) eqn:EQN. all: unfold select_compl in Heqselcomp; rewrite EQN in Heqselcomp; destruct c0; simpl in *; auto. all: discriminate. } rewrite H. clear H. - exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C). - exploit (transl_complu_correct c0 x RTMP lbl); eauto. intros (rs'2 & A' & B' & C'). + exploit (transl_compilu_correct c0 x n lbl); eauto. intros (rs'2 & A' & B' & C'). exists rs'2, (Pcb BTwnez RTMP lbl). split. - * constructor. apply exec_straight_trans - with (c2 := (transl_compl c0 Unsigned x RTMP lbl k)) (rs2 := rs') (m2 := m'). - eexact A. eexact A'. + * constructor. eexact A'. * split; auto. - { apply C'; auto. rewrite B, C; eauto with asmgen. } - { intros. rewrite B'; eauto with asmgen. } + { apply C'; auto. eapply Val_cmplu_bool_correct; eauto. } (* Ccompf *) - exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). |