From c3bebbcc12b5e7a4930aaba6b401ee5f06b7aafe Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 25 Feb 2021 16:30:25 +0100 Subject: some more proof for fake hsval checker expansions --- scheduling/RTLpathSE_impl.v | 325 +------------------------------------------- 1 file changed, 1 insertion(+), 324 deletions(-) (limited to 'scheduling') diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index f42a3492..7e41b5b0 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -7,7 +7,6 @@ Require Import RTL RTLpath. Require Import Errors. Require Import RTLpathSE_theory RTLpathLivegenproof. Require Import Axioms RTLpathSE_simu_specs. -Require Import Asmgen Asmgenproof1. Require Import RTLpathSE_simplify. Local Open Scope error_monad_scope. @@ -659,214 +658,14 @@ Qed. end.*) (* -Definition load_hilo32 (hi lo: int) := - DO hnil <~ hSnil();; - if Int.eq lo Int.zero then - hSop (OEluiw hi) hnil - else - DO hvs <~ hSop (OEluiw hi) hnil;; - DO hl <~ make_lhsv_single hvs;; - hSop (Oaddimm lo) hl. - -Definition load_hilo64 (hi lo: int64) := - DO hnil <~ hSnil();; - if Int64.eq lo Int64.zero then - hSop (OEluil hi) hnil - else - DO hvs <~ hSop (OEluil hi) hnil;; - DO hl <~ make_lhsv_single hvs;; - hSop (Oaddlimm lo) hl. - -Definition loadimm32 (n: int) := - match make_immed32 n with - | Imm32_single imm => - DO hnil <~ hSnil();; - hSop (OEaddiwr0 imm) hnil - | Imm32_pair hi lo => load_hilo32 hi lo - end. - -Definition loadimm64 (n: int64) := - DO hnil <~ hSnil();; - match make_immed64 n with - | Imm64_single imm => - hSop (OEaddilr0 imm) hnil - | Imm64_pair hi lo => load_hilo64 hi lo - | Imm64_large imm => hSop (OEloadli imm) hnil - end. - -Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) := - match make_immed32 n with - | Imm32_single imm => - DO hl <~ make_lhsv_single hv1;; - hSop (opimm imm) hl - | Imm32_pair hi lo => - DO hvs <~ load_hilo32 hi lo;; - DO hl <~ make_lhsv_cmp false hv1 hvs;; - hSop op hl - end. - -Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) := - match make_immed64 n with - | Imm64_single imm => - DO hl <~ make_lhsv_single hv1;; - hSop (opimm imm) hl - | Imm64_pair hi lo => - DO hvs <~ load_hilo64 hi lo;; - DO hl <~ make_lhsv_cmp false hv1 hvs;; - hSop op hl - | Imm64_large imm => - DO hnil <~ hSnil();; - DO hvs <~ hSop (OEloadli imm) hnil;; - DO hl <~ make_lhsv_cmp false hv1 hvs;; - hSop op hl - end. - -Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw. -Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. -Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. -Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. -Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. -Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. - - -Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := - match cmp with - | Ceq => hSop (OEsequw optR0) lhsv - | Cne => hSop (OEsneuw optR0) lhsv - | Clt | Cgt => hSop (OEsltuw optR0) lhsv - | Cle | Cge => - DO hvs <~ (hSop (OEsltuw optR0) lhsv);; - DO hl <~ make_lhsv_single hvs;; - hSop (OExoriw Int.one) hl - end. - -Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := - match cmp with - | Ceq => hSop (OEseql optR0) lhsv - | Cne => hSop (OEsnel optR0) lhsv - | Clt | Cgt => hSop (OEsltl optR0) lhsv - | Cle | Cge => - DO hvs <~ (hSop (OEsltl optR0) lhsv);; - DO hl <~ make_lhsv_single hvs;; - hSop (OExoriw Int.one) hl - end. -Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := - match cmp with - | Ceq => hSop (OEsequl optR0) lhsv - | Cne => hSop (OEsneul optR0) lhsv - | Clt | Cgt => hSop (OEsltul optR0) lhsv - | Cle | Cge => - DO hvs <~ (hSop (OEsltul optR0) lhsv);; - DO hl <~ make_lhsv_single hvs;; - hSop (OExoriw Int.one) hl - end. -Definition cond_float (cmp: comparison) (lhsv: list_hsval) := - match cmp with - | Ceq | Cne => hSop OEfeqd lhsv - | Clt | Cgt => hSop OEfltd lhsv - | Cle | Cge => hSop OEfled lhsv - end. -Definition cond_single (cmp: comparison) (lhsv: list_hsval) := - match cmp with - | Ceq | Cne => hSop OEfeqs lhsv - | Clt | Cgt => hSop OEflts lhsv - | Cle | Cge => hSop OEfles lhsv - end. -Definition is_normal_cmp cmp := - match cmp with | Cne => false | _ => true end. -Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: 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_single hvs;; - if normal' then RET hvs else hSop (OExoriw Int.one) hl. - -Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := - let is_inv := is_inv_cmp_int cmp in - if Int.eq n Int.zero then - let optR0 := make_optR0 true is_inv in - DO hl <~ make_lhsv_cmp is_inv hv1 hv1;; - cond_int32s cmp hl optR0 - else - match cmp with - | Ceq | Cne => - let optR0 := make_optR0 true is_inv in - DO hvs <~ xorimm32 hv1 n;; - DO hl <~ make_lhsv_cmp false hvs hvs;; - cond_int32s cmp hl optR0 - | Clt => sltimm32 hv1 n - | Cle => - if Int.eq n (Int.repr Int.max_signed) then - loadimm32 Int.one - else sltimm32 hv1 (Int.add n Int.one) - | _ => - let optR0 := make_optR0 false is_inv in - DO hvs <~ loadimm32 n;; - DO hl <~ make_lhsv_cmp is_inv hv1 hvs;; - cond_int32s cmp hl optR0 - end. -Definition expanse_condimm_int32u (cmp: comparison) (hv1: hsval) (n: int) := - let is_inv := is_inv_cmp_int cmp in - if Int.eq n Int.zero then - let optR0 := make_optR0 true is_inv in - DO hl <~ make_lhsv_cmp is_inv hv1 hv1;; - cond_int32u cmp hl optR0 - else - match cmp with - | Clt => sltuimm32 hv1 n - | _ => - let optR0 := make_optR0 false is_inv in - DO hvs <~ loadimm32 n;; - DO hl <~ make_lhsv_cmp is_inv hv1 hvs;; - cond_int32u cmp hl optR0 - end. -Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := - let is_inv := is_inv_cmp_int cmp in - if Int64.eq n Int64.zero then - let optR0 := make_optR0 true is_inv in - DO hl <~ make_lhsv_cmp is_inv hv1 hv1;; - cond_int64s cmp hl optR0 - else - match cmp with - | Ceq | Cne => - let optR0 := make_optR0 true is_inv in - DO hvs <~ xorimm64 hv1 n;; - DO hl <~ make_lhsv_cmp false hvs hvs;; - cond_int64s cmp hl optR0 - | Clt => sltimm64 hv1 n - | Cle => - if Int64.eq n (Int64.repr Int64.max_signed) then - loadimm32 Int.one - else sltimm64 hv1 (Int64.add n Int64.one) - | _ => - let optR0 := make_optR0 false is_inv in - DO hvs <~ loadimm64 n;; - DO hl <~ make_lhsv_cmp is_inv hv1 hvs;; - cond_int64s cmp hl optR0 - end. -Definition expanse_condimm_int64u (cmp: comparison) (hv1: hsval) (n: int64) := - let is_inv := is_inv_cmp_int cmp in - if Int64.eq n Int64.zero then - let optR0 := make_optR0 true is_inv in - DO hl <~ make_lhsv_cmp is_inv hv1 hv1;; - cond_int64u cmp hl optR0 - else - match cmp with - | Clt => sltuimm64 hv1 n - | _ => - let optR0 := make_optR0 false is_inv in - DO hvs <~ loadimm64 n;; - DO hl <~ make_lhsv_cmp is_inv hv1 hvs;; - cond_int64u cmp hl optR0 - end. *) (** simplify a symbolic value before assignment to a register *) @@ -911,27 +710,6 @@ Proof. intro H0; clear H0; simplify_SOME z; congruence. Qed. -Lemma xor_neg_ltle_cmp: forall v1 v2, - Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmp; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. -Qed. - -Lemma xor_neg_optb: forall v, - Some (Val.xor (Val.of_optbool (option_map negb v)) - (Vint Int.one)) = Some (Val.of_optbool v). -Proof. - intros. - destruct v; simpl; trivial. - destruct b; simpl; auto. -Qed. Lemma xor_ceq_zero: forall v n cmp, cmp = Ceq \/ cmp = Cne -> @@ -966,29 +744,6 @@ Proof. unfold Val.cmp; simpl; auto. Qed.*) -Lemma xor_neg_ltle_cmpu: forall mptr v1 v2, - Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence. - unfold Val.cmpu; simpl; - try rewrite Int.eq_sym; - try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl; - try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; - auto. - 1,2: - unfold Val.cmpu, Val.cmpu_bool; - destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _); - try destruct (eq_block _ _); auto. - unfold Val.cmpu, Val.cmpu_bool; 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. (* TODO gourdinl Lemma xor_neg_ltge_cmpu: forall mptr v1 v2, Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = @@ -1143,16 +898,7 @@ Proof. repeat destruct (_ && _); simpl; auto. Qed. -Lemma xor_neg_eqne_cmpf: forall v1 v2, - Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = - Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)). -Proof. - intros. eapply f_equal. - destruct v1, v2; simpl; try congruence; - unfold Val.cmpf; simpl. - rewrite Float.cmp_ne_eq. - destruct (Float.cmp _ _ _); simpl; auto. -Qed. + Lemma xor_neg_eqne_cmpfs: forall v1 v2, Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = @@ -1443,62 +1189,6 @@ Proof. Admitted. (*Qed.*) -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), - 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])) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompuimm c n)) 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])) rs0 m0 - IN SOME m <- seval_smem ge sp (si_smem st) rs0 m0 - IN eval_operation ge sp (Ocmp (Ccompuimm c n)) args m)). -Proof. - unfold expanse_condimm_int32u, cond_int32u in *; destruct c; - intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; - unfold loadimm32, sltuimm32, opimm32, load_hilo32. - 1,3,5,7,9,11: - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence; - 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. - 4: rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu. - 5: intros; replace (Clt) with (swap_comparison Cgt) by auto; - rewrite Val.swap_cmpu_bool; trivial. - 6: intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb. - 1,2,3,4,5,6: apply Int.same_if_eq in EQIMM; subst; trivial. - all: - specialize make_immed32_sound with n; - destruct (make_immed32 n) eqn:EQMKI; - try destruct (Int.eq lo Int.zero) eqn:EQLO. - all: - wlp_simplify; - destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence. - all: try (simplify_SOME z; contradiction; fail). - all: - try erewrite H11; eauto; - try erewrite H10; eauto; 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. - all: try apply Int.same_if_eq in H1; subst. - all: try apply Int.same_if_eq in EQLO; subst. - all: try rewrite Int.add_commut, Int.add_zero_l; trivial. - all: try rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; trivial. - all: intros; replace (Clt) with (negate_comparison Cge) by auto; - rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial. -Qed. Lemma simplify_ccompl_correct: forall c r r0 (hst: hsistate_local), WHEN DO hv1 <~ hsi_sreg_get hst r;; @@ -1576,20 +1266,7 @@ Proof. - intros; apply xor_neg_ltge_cmplu. Qed. -(* TODO gourdinl move to common/Values ? *) -Theorem swap_cmpf_bool: - forall c x y, - Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. -Qed. -Theorem swap_cmpfs_bool: - forall c x y, - Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. -Qed. Lemma simplify_ccompf_correct: forall c r r0 (hst: hsistate_local), WHEN DO hv1 <~ hsi_sreg_get hst r;; -- cgit