From fb6325b46ff522a9120f4a101f095908b1ab38c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 19 Feb 2021 18:19:24 +0100 Subject: Branch expansions activated and configured in the checker (but admitted) and bugfix in the expansion liveness modification --- scheduling/RTLpathSE_impl.v | 195 +++++++++++++++++++++++++++++++++----------- 1 file changed, 146 insertions(+), 49 deletions(-) (limited to 'scheduling') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index b7b58ae5..32761c6e 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -893,6 +893,12 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs let optR0 := make_optR0 false is_inv in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; cond_int64u c lhsv optR0 + | (Ccomplimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int64s c hv1 imm + | (Ccompluimm c imm), a1 :: nil => + DO hv1 <~ hsi_sreg_get hst a1;; + expanse_condimm_int64u c hv1 imm | (Ccompf c), f1 :: f2 :: nil => DO hv1 <~ hsi_sreg_get hst f1;; DO hv2 <~ hsi_sreg_get hst f2;; @@ -917,12 +923,6 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hs let is_inv := is_inv_cmp_float c in DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; expanse_cond_fp true cond_single c lhsv - | (Ccomplimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64s c hv1 imm - | (Ccompluimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64u c hv1 imm | _, _ => DO lhsv <~ hlist_args hst lr;; hSop op lhsv @@ -1317,7 +1317,7 @@ Proof. rewrite Int.sub_zero_l. unfold Int.shru, Int.shl. *) -(* TODO gourdinl Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local), +Lemma simplify_ccompuimm_correct: forall c n r (hst: hsistate_local), WHEN DO hv1 <~ hsi_sreg_get hst r;; expanse_condimm_int32u c hv1 n ~> hv THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem) (st : sistate_local), @@ -1355,51 +1355,37 @@ Proof. simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction. + apply mkimm_single_equal in EQMKI; subst. rewrite Int.add_commut, Int.add_zero_l. trivial. - + - - 2: { intros. destruct (Int.eq n Int.zero) eqn:EQIMM; simpl. - 2: { unfold loadimm32. destruct (make_immed32 n) eqn:EQMKI. - 2: { - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail); + + admit. + + admit. + - (* TODO gourdinl same as first goal *) + wlp_simplify; + destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. + all: try (simplify_SOME z; contradiction; fail). try erewrite H9; eauto; try erewrite H8; eauto; try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto; try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto; try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto; simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction. - 2: { - apply mkimm_single_equal in EQMKI; subst. - rewrite Int.add_commut, Int.add_zero_l. trivial. - - - 2: { + apply Int.same_if_eq in EQIMM; subst. trivial. + - admit. + - (* TODO gourdinl same as first goal *) wlp_simplify; destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - - 2: { - - all: - try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); + all: try (simplify_SOME z; contradiction; fail). + try erewrite H9; eauto; try erewrite H8; eauto; + try erewrite H7; eauto; try erewrite H6; eauto; try erewrite H5; eauto; try erewrite H4; eauto; try erewrite H3; eauto; try erewrite H2; eauto; try erewrite H1; eauto; try erewrite H0; eauto; try erewrite H; eauto; - simplify_SOME z; unfold Val.cmp, zero32. - all: - try apply Int.same_if_eq in H0; subst; trivial. - - erewrite H0. - - - - intros; apply xor_neg_ltle_cmpu. - - intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpu_bool; trivial. - - intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool. - rewrite xor_neg_optb; trivial. -Qed. - - *) + simplify_SOME z; unfold Val.cmpu, zero32; intros; try contradiction. + apply Int.same_if_eq in EQIMM; subst. trivial. + - (* same *) admit. + - (* same *) admit. + - (* same *) admit. + - (* same *) admit. + - (* same *) admit. + - (* same *) admit. + - (* same *) admit. +Admitted. Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local), WHEN DO hv1 <~ hsi_sreg_get hst r;; @@ -1791,7 +1777,7 @@ Proof. rewrite <- X, sok_local_set_sreg. intuition eauto. - destruct REF; intuition eauto. - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto. -Qed. + Qed. Global Opaque hslocal_set_sreg. Local Hint Resolve hslocal_set_sreg_correct: wlp. @@ -1843,6 +1829,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := | Cge => CEbgeul optR0 end. +Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * list_hsval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + DO hvs <~ fn_cond cmp lhsv;; + DO hl <~ make_lhsv_cmp false hvs hvs;; + if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl). + Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) := match cond, args with | (Ccomp c), (a1 :: a2 :: nil) => @@ -1859,6 +1852,30 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list DO hv2 <~ hsi_sreg_get prev a2;; DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; RET (cond, lhsv) + | (Ccompimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + DO hv1 <~ hsi_sreg_get prev a1;; + (if Int.eq n Int.zero then + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; + let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in + RET (cond, lhsv) + else + DO hvs <~ loadimm32 n;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; + let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in + RET (cond, lhsv)) + | (Ccompuimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + DO hv1 <~ hsi_sreg_get prev a1;; + (if Int.eq n Int.zero then + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; + let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in + RET (cond, lhsv) + else + DO hvs <~ loadimm32 n;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; + let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in + RET (cond, lhsv)) | (Ccompl c), (a1 :: a2 :: nil) => let is_inv := is_inv_cmp_int c in let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in @@ -1873,9 +1890,54 @@ Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list DO hv2 <~ hsi_sreg_get prev a2;; DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; RET (cond, lhsv) - (* | Icond (Ccompimm c n) (a1 :: nil) _ _ _ => - let cond := transl_cbranch_int32s c (make_optR0 c) in - RET (cond, a1 :: a1 :: nil)*) + | (Ccomplimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + DO hv1 <~ hsi_sreg_get prev a1;; + (if Int64.eq n Int64.zero then + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; + let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in + RET (cond, lhsv) + else + DO hvs <~ loadimm64 n;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; + let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in + RET (cond, lhsv)) + | (Ccompluimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + DO hv1 <~ hsi_sreg_get prev a1;; + (if Int64.eq n Int64.zero then + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv1;; + let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in + RET (cond, lhsv) + else + DO hvs <~ loadimm64 n;; + DO lhsv <~ make_lhsv_cmp is_inv hv1 hvs;; + let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in + RET (cond, lhsv)) + | (Ccompf c), (f1 :: f2 :: nil) => + DO hv1 <~ hsi_sreg_get prev f1;; + DO hv2 <~ hsi_sreg_get prev f2;; + let is_inv := is_inv_cmp_float c in + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + expanse_cbranch_fp false cond_float c lhsv + | (Cnotcompf c), (f1 :: f2 :: nil) => + DO hv1 <~ hsi_sreg_get prev f1;; + DO hv2 <~ hsi_sreg_get prev f2;; + let is_inv := is_inv_cmp_float c in + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + expanse_cbranch_fp true cond_float c lhsv + | (Ccompfs c), (f1 :: f2 :: nil) => + DO hv1 <~ hsi_sreg_get prev f1;; + DO hv2 <~ hsi_sreg_get prev f2;; + let is_inv := is_inv_cmp_float c in + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + expanse_cbranch_fp false cond_single c lhsv + | (Cnotcompfs c), (f1 :: f2 :: nil) => + DO hv1 <~ hsi_sreg_get prev f1;; + DO hv2 <~ hsi_sreg_get prev f2;; + let is_inv := is_inv_cmp_float c in + DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; + expanse_cbranch_fp true cond_single c lhsv | _, _ => DO vargs <~ hlist_args prev args;; RET (cond, vargs) @@ -1984,7 +2046,7 @@ Lemma hsiexec_inst_correct i hst: exists st', siexec_inst i st = Some st' /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st') /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st'). -Proof. +Proof. Admitted. (* destruct i; simpl; try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail). - (* refines_dyn Iop *) @@ -2020,9 +2082,44 @@ Proof. destruct NEST as [|st0 se lse TOP NEST]; econstructor; simpl; auto; constructor; auto. + admit. + + repeat (destruct l; try apply hsiexec_cond_noexp). + destruct (Int.eq _ _) eqn:EQIMM; simpl. + 1: admit. + + unfold loadimm32; destruct make_immed32. + { + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + * unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. + constructor; simpl; eauto. + constructor. + * destruct REF as (EXREF & LREF & NEST). + split. + -- do 2 (constructor; simpl; auto). + intros; erewrite seval_condition_refines; eauto. + destruct c0; simpl; unfold seval_condition. + + { simpl in *. + erewrite H4; eauto. + erewrite H3; eauto; erewrite H2; eauto. + simpl. + + erewrite H1; eauto. try erewrite H0; eauto; + try erewrite H; eauto; simplify_SOME z. + 2: { + generalize (sok_local_set_sreg_simp (Rop (OEaddiwr0 imm))); simpl; eauto. + intros.j + apply hsilocal_refines_smem_refines in LREF; auto. + + rewrite <- LREF. auto. + 2: { eauto. + all: intros; destruct z0, z2; auto. + -- split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. + + admit. + admit. -Admitted. + *) (*Qed.*) Global Opaque hsiexec_inst. Local Hint Resolve hsiexec_inst_correct: wlp. -- cgit