diff options
| -rw-r--r-- | scheduling/RTLpathSE_impl.v | 369 |
1 files changed, 272 insertions, 97 deletions
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index 7a90fd3a..1e36a558 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -972,6 +972,122 @@ Proof. - repeat destruct (_ && _); simpl; auto. Qed. +Lemma cmpl_optbool_mktotal: forall cmp v1 v2, + Some (Val.maketotal (Val.cmpl cmp v1 v2)) = + Some (Val.of_optbool (Val.cmpl_bool cmp v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.cmp _ _); auto. +Qed. + +Lemma cmplu_optbool_mktotal: forall mptr cmp v1 v2, + Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) cmp v1 v2)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) cmp v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. +Qed. + +Lemma xor_neg_ltle_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. + +Lemma cmp_neg_ltgt_cmpl: forall v1 v2, + Some (Val.maketotal (Val.cmpl Clt v1 v2)) = + Some (Val.of_optbool (Val.cmpl_bool Cgt v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. + +Lemma xor_neg_ltge_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. + +Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + +Lemma cmp_neg_ltgt_cmplu: forall mptr v1 v2, + Some (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cgt v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + +Lemma xor_neg_ltge_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. + Lemma simplify_ccomp_correct: forall c r r0 (hst: hsistate_local), WHEN DO hv1 <~ hsi_sreg_get hst r;; DO hv2 <~ hsi_sreg_get hst r0;; @@ -1002,9 +1118,9 @@ Proof. erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; simplify_SOME z. - simplify_SOME z; intros; apply xor_neg_ltle_cmp. - simplify_SOME z; intros; apply cmp_neg_ltgt_cmp. - simplify_SOME z; intros; apply xor_neg_ltge_cmp. + intros; apply xor_neg_ltle_cmp. + intros; apply cmp_neg_ltgt_cmp. + intros; apply xor_neg_ltge_cmp. Qed. Lemma simplify_ccompu_correct: forall c r r0 (hst: hsistate_local), @@ -1037,9 +1153,81 @@ Proof. erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; simplify_SOME z. - simplify_SOME z; intros; apply xor_neg_ltle_cmpu. - simplify_SOME z; intros; apply cmp_neg_ltgt_cmpu. - simplify_SOME z; intros; apply xor_neg_ltge_cmpu. + intros; apply xor_neg_ltle_cmpu. + intros; apply cmp_neg_ltgt_cmpu. + intros; apply xor_neg_ltge_cmpu. +Qed. + +Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local), + WHEN DO hv1 <~ hsi_sreg_get hst r;; + DO hv2 <~ hsi_sreg_get hst r0;; + DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; + cond_int64s c lhsv None ~> hv + THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) + (m0 : mem) (st : sistate_local), + hsilocal_refines ge sp rs0 m0 hst st -> + hsok_local ge sp rs0 m0 hst -> + (SOME args <- + seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 + m0 + IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 + IN eval_operation ge sp (Ocmp (Ccompl c)) args m) <> None -> + seval_sval ge sp (hsval_proj hv) rs0 m0 = + (SOME args <- + seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 + m0 + IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 + IN eval_operation ge sp (Ocmp (Ccompl c)) args m)). +Proof. + unfold cond_int64s in *; destruct c; + wlp_simplify; + destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. + all: try (simplify_SOME z; contradiction; fail). + all: + try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); + erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; + erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; + simplify_SOME z. + 1,2,3: intros; apply cmpl_optbool_mktotal. + intros; apply xor_neg_ltle_cmpl. + intros; apply cmp_neg_ltgt_cmpl. + intros; apply xor_neg_ltge_cmpl. +Qed. + +Lemma simplify_ccomplu_correct: forall c r r0 (hst: hsistate_local), + WHEN DO hv1 <~ hsi_sreg_get hst r;; + DO hv2 <~ hsi_sreg_get hst r0;; + DO lhsv <~ make_lhsv_cmp (is_inv_cmp_int c) hv1 hv2;; + cond_int64u c lhsv None ~> hv + THEN (forall (ge : RTL.genv) (sp : val) (rs0 : regset) + (m0 : mem) (st : sistate_local), + hsilocal_refines ge sp rs0 m0 hst st -> + hsok_local ge sp rs0 m0 hst -> + (SOME args <- + seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 + m0 + IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 + IN eval_operation ge sp (Ocmp (Ccomplu c)) args m) <> None -> + seval_sval ge sp (hsval_proj hv) rs0 m0 = + (SOME args <- + seval_list_sval ge sp (list_sval_inj (map (si_sreg st) [r; r0])) rs0 + m0 + IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 + IN eval_operation ge sp (Ocmp (Ccomplu c)) args m)). +Proof. + unfold cond_int64u in *; destruct c; + wlp_simplify; + destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. + all: try (simplify_SOME z; contradiction; fail). + all: + try (erewrite H7; eauto; erewrite H6; eauto; erewrite H5; eauto); + erewrite H4; eauto; erewrite H3; eauto; erewrite H2; eauto; + erewrite H1; eauto; erewrite H0; eauto; erewrite H; eauto; + simplify_SOME z. + 1,2,3: intros; apply cmplu_optbool_mktotal. + intros; apply xor_neg_ltle_cmplu. + intros; apply cmp_neg_ltgt_cmplu. + intros; apply xor_neg_ltge_cmplu. Qed. Lemma simplify_correct rsv lr hst: @@ -1063,8 +1251,8 @@ Proof. { destruct cond; repeat (destruct lr; try apply simplify_nothing). + apply simplify_ccomp_correct. + apply simplify_ccompu_correct. - + admit. - + admit. + + apply simplify_ccompl_correct. + + apply simplify_ccomplu_correct. + admit. + admit. + admit. @@ -1202,8 +1390,8 @@ Definition transl_cbranch_int32s (cmp: comparison) (optR0: option bool) := Definition transl_cbranch_int32u (cmp: comparison) (optR0: option bool) := match cmp with - | Ceq => CEbeqw optR0 - | Cne => CEbnew optR0 + | Ceq => CEbequw optR0 + | Cne => CEbneuw optR0 | Clt => CEbltuw optR0 | Cle => CEbgeuw optR0 | Cgt => CEbltuw optR0 @@ -1222,8 +1410,8 @@ Definition transl_cbranch_int64s (cmp: comparison) (optR0: option bool) := Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := match cmp with - | Ceq => CEbeql optR0 - | Cne => CEbnel optR0 + | Ceq => CEbequl optR0 + | Cne => CEbneul optR0 | Clt => CEbltul optR0 | Cle => CEbgeul optR0 | Cgt => CEbltul optR0 @@ -1319,14 +1507,60 @@ Qed. Local Hint Resolve hsist_set_local_correct_stat: core. +Lemma hsiexec_cond_noexp (hst: hsistate): forall l c0 n n0, + WHEN DO res <~ + (DO vargs <~ hlist_args (hsi_local hst) l;; RET ((c0, vargs)));; + (let (cond, vargs) := res in + RET (Some + {| + hsi_pc := n0; + hsi_exits := {| + hsi_cond := cond; + hsi_scondargs := vargs; + hsi_elocal := hsi_local hst; + hsi_ifso := n |} :: hsi_exits hst; + hsi_local := hsi_local hst |})) ~> o0 + THEN (forall (hst' : hsistate) (st : sistate), + o0 = Some hst' -> + exists st' : sistate, + Some + {| + si_pc := n0; + si_exits := {| + si_cond := c0; + si_scondargs := list_sval_inj + (map (si_sreg (si_local st)) l); + si_elocal := si_local st; + si_ifso := n |} :: si_exits st; + si_local := si_local st |} = Some st' /\ + (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st') /\ + (forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem), + hsistate_refines_dyn ge sp rs0 m0 hst st -> + hsistate_refines_dyn ge sp rs0 m0 hst' st')). +Proof. + intros. + wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. + - unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. + constructor; simpl; eauto. + constructor. + - destruct H0 as (EXREF & LREF & NEST). + split. + + constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. + Lemma hsiexec_inst_correct i hst: WHEN hsiexec_inst i hst ~> o THEN forall hst' st, o = Some 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. Admitted. - (* TODO destruct i; simpl; +Proof. + destruct i; simpl; try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail). - (* refines_dyn Iop *) wlp_simplify; try_simplify_someHyps; eexists; intuition eauto. @@ -1341,89 +1575,30 @@ Proof. Admitted. eapply hsist_set_local_correct_dyn; eauto. unfold sok_local; simpl; intuition. - (* refines_stat Icond *) - unfold cbranch_expanse; destruct c eqn:EQC; simpl in *. - destruct l. - 2: { - destruct l. - 2: { - destruct l. - { 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). - (*eapply hsist_set_local_correct_dyn; eauto.*) - split. - + constructor; simpl; auto. - constructor; simpl; auto. - intros; erewrite seval_condition_refines; eauto. - destruct c0; simpl. - unfold seval_condition. - erewrite H3; eauto. - erewrite H2; eauto. - erewrite H1; eauto. - erewrite H0; eauto. - erewrite H; eauto. - simplify_SOME args. - { - intros. destruct args0, args2; auto; - unfold Val.cmpu_bool, Val.cmp_bool; - destruct Archi.ptr64; auto. simpl. - destruct (_ && _). - try destruct (Int.eq _ _); auto. - try destruct (Mem.valid_pointer _ _ _ || Mem.valid_pointer _ _ _); - simpl. congruence. - - - - - - - destruct args, args1; try congruence; auto. - destruct args1; try congruence; auto. - destruct args1; try congruence; auto. - destruct v1. - unfold Val.cmpu_bool, Val.cmp_bool. - erewrite H3. - - destruct c eqn:EQC; simpl; eauto. - 8: { destruct (hlist_args (hsi_local hst) l) in Hexta. - destruct in Hexta. - - - destruct exta; simpl in *. - destruct Hexta. - + split; simpl; auto. - destruct NEST as [|st0 se lse TOP NEST]; - econstructor; simpl; auto; constructor; auto. - - - wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; - - unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition. - constructor; simpl; eauto. - constructor. - - (* refines_dyn Icond *) - destruct REF as (EXREF & LREF & NEST). - destruct exta. simpl. - split. - + constructor; simpl; auto. - constructor; simpl; auto. - intros; erewrite seval_condition_refines; eauto. - - destruct c eqn:EQC; simpl; eauto. - 8: { destruct (hlist_args (hsi_local hst) l) in Hexta. - destruct in Hexta. - - - destruct exta; simpl in *. - destruct Hexta. - + split; simpl; auto. - destruct NEST as [|st0 se lse TOP NEST]; - econstructor; simpl; auto; constructor; auto. - Qed.*) + unfold cbranch_expanse; destruct c eqn:EQC; + try apply hsiexec_cond_noexp. + + repeat (destruct l; try apply hsiexec_cond_noexp). + 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; + erewrite H3; eauto; erewrite H2; eauto; + erewrite H1; eauto; erewrite H0; eauto; + erewrite H; eauto; simplify_SOME z. + all: intros; destruct z0, z2; auto. + -- split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. + + admit. + + admit. + + admit. +Admitted. +(*Qed.*) Global Opaque hsiexec_inst. Local Hint Resolve hsiexec_inst_correct: wlp. |