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 --- riscV/ExpansionOracle.ml | 4 +- riscV/RTLpathSE_simplify.v | 813 +++++++++++++++++++++++++++++++++++++++++--- scheduling/RTLpathSE_impl.v | 325 +----------------- 3 files changed, 772 insertions(+), 370 deletions(-) diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index d3805738..11a66322 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -388,7 +388,7 @@ let expanse (sb : superblock) code pm = debug "Iop/Ccomp\n"; exp := cond_int32s false c a1 a2 dest succ []; was_exp := true - (*| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> + | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompu\n"; exp := cond_int32u false c a1 a2 dest succ []; was_exp := true @@ -432,7 +432,7 @@ let expanse (sb : superblock) code pm = debug "Iop/Cnotcompfs\n"; exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; was_exp := true - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + (*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> debug "Icond/Ccomp\n"; exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; was_branch := true; diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index b9fe504e..7b20db6c 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -1,7 +1,9 @@ +Require Import Coqlib Floats Values Memory. Require Import Integers. Require Import Op Registers. Require Import RTLpathSE_theory. Require Import RTLpathSE_simu_specs. +Require Import Asmgen Asmgenproof1. (* Useful functions for conditions/branches expansion *) @@ -26,6 +28,69 @@ Definition make_lhsv_single (hvs: hsval) : list_hsval := (* Expansion functions *) +Definition load_hilo32 (hi lo: int) := + if Int.eq lo Int.zero then + fSop (OEluiw hi) fSnil + else + let hvs := fSop (OEluiw hi) fSnil in + let hl := make_lhsv_single hvs in + fSop (Oaddimm lo) hl. + +Definition load_hilo64 (hi lo: int64) := + if Int64.eq lo Int64.zero then + fSop (OEluil hi) fSnil + else + let hvs := fSop (OEluil hi) fSnil in + let hl := make_lhsv_single hvs in + fSop (Oaddlimm lo) hl. + +Definition loadimm32 (n: int) := + match make_immed32 n with + | Imm32_single imm => + fSop (OEaddiwr0 imm) fSnil + | Imm32_pair hi lo => load_hilo32 hi lo + end. + +Definition loadimm64 (n: int64) := + match make_immed64 n with + | Imm64_single imm => + fSop (OEaddilr0 imm) fSnil + | Imm64_pair hi lo => load_hilo64 hi lo + | Imm64_large imm => fSop (OEloadli imm) fSnil + end. + +Definition opimm32 (hv1: hsval) (n: int) (op: operation) (opimm: int -> operation) := + match make_immed32 n with + | Imm32_single imm => + let hl := make_lhsv_single hv1 in + fSop (opimm imm) hl + | Imm32_pair hi lo => + let hvs := load_hilo32 hi lo in + let hl := make_lhsv_cmp false hv1 hvs in + fSop op hl + end. + +Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> operation) := + match make_immed64 n with + | Imm64_single imm => + let hl := make_lhsv_single hv1 in + fSop (opimm imm) hl + | Imm64_pair hi lo => + let hvs := load_hilo64 hi lo in + let hl := make_lhsv_cmp false hv1 hvs in + fSop op hl + | Imm64_large imm => + let hvs := fSop (OEloadli imm) fSnil in + let hl := make_lhsv_cmp false hv1 hvs in + fSop 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_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := match cmp with | Ceq => fSop (OEseqw optR0) lhsv @@ -37,78 +102,706 @@ Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) fSop (OExoriw Int.one) hl end. +Definition cond_int32u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := + match cmp with + | Ceq => fSop (OEsequw optR0) lhsv + | Cne => fSop (OEsneuw optR0) lhsv + | Clt | Cgt => fSop (OEsltuw optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltuw optR0) lhsv) in + let hl := make_lhsv_single hvs in + fSop (OExoriw Int.one) hl + end. + +Definition cond_int64s (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := + match cmp with + | Ceq => fSop (OEseql optR0) lhsv + | Cne => fSop (OEsnel optR0) lhsv + | Clt | Cgt => fSop (OEsltl optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltl optR0) lhsv) in + let hl := make_lhsv_single hvs in + fSop (OExoriw Int.one) hl + end. + +Definition cond_int64u (cmp: comparison) (lhsv: list_hsval) (optR0: option bool) := + match cmp with + | Ceq => fSop (OEsequl optR0) lhsv + | Cne => fSop (OEsneul optR0) lhsv + | Clt | Cgt => fSop (OEsltul optR0) lhsv + | Cle | Cge => + let hvs := (fSop (OEsltul optR0) lhsv) in + let hl := make_lhsv_single hvs in + fSop (OExoriw Int.one) hl + end. + +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 + let hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int32s cmp hl optR0 + else + match cmp with + | Ceq | Cne => + let optR0 := make_optR0 true is_inv in + let hvs := xorimm32 hv1 n in + let hl := make_lhsv_cmp false hvs hvs in + 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 + let hvs := loadimm32 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + 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 + let hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int32u cmp hl optR0 + else + match cmp with + | Clt => sltuimm32 hv1 n + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm32 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + 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 + let hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int64s cmp hl optR0 + else + match cmp with + | Ceq | Cne => + let optR0 := make_optR0 true is_inv in + let hvs := xorimm64 hv1 n in + let hl := make_lhsv_cmp false hvs hvs in + 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 + let hvs := loadimm64 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + 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 + let hl := make_lhsv_cmp is_inv hv1 hv1 in + cond_int64u cmp hl optR0 + else + match cmp with + | Clt => sltuimm64 hv1 n + | _ => + let optR0 := make_optR0 false is_inv in + let hvs := loadimm64 n in + let hl := make_lhsv_cmp is_inv hv1 hvs in + cond_int64u cmp hl optR0 + end. + +Definition cond_float (cmp: comparison) (lhsv: list_hsval) := + match cmp with + | Ceq | Cne => fSop OEfeqd lhsv + | Clt | Cgt => fSop OEfltd lhsv + | Cle | Cge => fSop OEfled lhsv + end. + +Definition cond_single (cmp: comparison) (lhsv: list_hsval) := + match cmp with + | Ceq | Cne => fSop OEfeqs lhsv + | Clt | Cgt => fSop OEflts lhsv + | Cle | Cge => fSop 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 + let hvs := fn_cond cmp lhsv in + let hl := make_lhsv_single hvs in + if normal' then hvs else fSop (OExoriw Int.one) hl. + (* Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := match op, lr with | Ocmp (Ccomp c), a1 :: a2 :: nil => - let fv1 := fsi_sreg_get hst a1 in - let fv2 := fsi_sreg_get hst a2 in + let hv1 := fsi_sreg_get hst a1 in + let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in - let lhsv := make_lhsv_cmp is_inv fv1 fv2 in + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (cond_int32s c lhsv optR0) - - (*| Ocmp (Ccompu c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; + | Ocmp (Ccompu c), a1 :: a2 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int32u c lhsv optR0 + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int32u c lhsv optR0) | Ocmp (Ccompimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int32s c hv1 imm + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int32s c hv1 imm) | Ocmp (Ccompuimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int32u c hv1 imm + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int32u c hv1 imm) | Ocmp (Ccompl c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; + let hv1 := fsi_sreg_get hst a1 in + let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int64s c lhsv optR0 + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int64s c lhsv optR0) | Ocmp (Ccomplu c), a1 :: a2 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - DO hv2 <~ hsi_sreg_get hst a2;; + let hv1 := fsi_sreg_get hst a1 in + let hv2 := fsi_sreg_get hst a2 in let is_inv := is_inv_cmp_int c in let optR0 := make_optR0 false is_inv in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - cond_int64u c lhsv optR0 + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (cond_int64u c lhsv optR0) | Ocmp (Ccomplimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64s c hv1 imm + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int64s c hv1 imm) | Ocmp (Ccompluimm c imm), a1 :: nil => - DO hv1 <~ hsi_sreg_get hst a1;; - expanse_condimm_int64u c hv1 imm + let hv1 := fsi_sreg_get hst a1 in + Some (expanse_condimm_int64u c hv1 imm) | Ocmp (Ccompf c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp false cond_float c lhsv + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp false cond_float c lhsv) | Ocmp (Cnotcompf c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp true cond_float c lhsv + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp true cond_float c lhsv) | Ocmp (Ccompfs c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in let is_inv := is_inv_cmp_float c in - DO lhsv <~ make_lhsv_cmp is_inv hv1 hv2;; - expanse_cond_fp false cond_single c lhsv + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp false cond_single c lhsv) | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => - DO hv1 <~ hsi_sreg_get hst f1;; - DO hv2 <~ hsi_sreg_get hst f2;; + let hv1 := fsi_sreg_get hst f1 in + let hv2 := fsi_sreg_get hst f2 in 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*) + let lhsv := make_lhsv_cmp is_inv hv1 hv2 in + Some (expanse_cond_fp true cond_single c lhsv) | _, _ => None end. +(* Auxiliary lemmas on comparisons *) + +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_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. + +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 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 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 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)) = + Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmpfs; simpl. + rewrite Float32.cmp_ne_eq. + destruct (Float32.cmp _ _ _); simpl; 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_neg_optb': forall v, + Some (Val.xor (Val.of_optbool v) (Vint Int.one)) = + Some (Val.of_optbool (option_map negb v)). +Proof. + intros. + destruct v; simpl; trivial. + destruct b; simpl; auto. +Qed. + +Lemma optbool_mktotal: forall v, + Val.maketotal (option_map Val.of_bool v) = + Val.of_optbool v. +Proof. + intros. + destruct v; simpl; auto. +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. + +(* Intermediates lemmas on each expansed instruction *) + +Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (cond_int32s c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmp_bool c v v0)). +Proof. + intros. + unfold cond_int32s in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmp. + - apply xor_neg_ltle_cmp. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmp_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmp_bool. + rewrite xor_neg_optb; trivial. +Qed. + +Lemma simplify_ccompu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj + (cond_int32u c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v v0)). +Proof. + intros. + erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). + 2: eauto. + unfold cond_int32u in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpu. + - apply xor_neg_ltle_cmpu. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpu_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmpu_bool. + rewrite xor_neg_optb; trivial. +Qed. + +Lemma simplify_ccompuimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int32u c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n))). +Proof. + intros. + assert (HMEM: Val.cmpu_bool (Mem.valid_pointer m) c v (Vint n) = + Val.cmpu_bool (Mem.valid_pointer m0) c v (Vint n)). + erewrite (cmpu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. + 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; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; trivial; + unfold Val.cmpu, zero32. + (* Simplify make immediate and decompose subcases *) + all: + try (specialize make_immed32_sound with n; + destruct (make_immed32 n) eqn:EQMKI); + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + rewrite HMEM. + (* Ceq, Cne, Clt = itself *) + all: intros; try apply Int.same_if_eq in EQIMM; subst; trivial. + (* Cle = xor (Clt) *) + all: try apply xor_neg_ltle_cmpu; trivial. + (* Others subcases with swap/negation *) + all: + unfold Val.cmpu; + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l in *; trivial; + try (rewrite <- xor_neg_ltle_cmpu; unfold Val.cmpu; + trivial; fail); + try (replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpu_bool; trivial; fail); + try (replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmpu_bool; rewrite xor_neg_optb; trivial; fail). + all: rewrite HMEM; trivial. +Qed. + +Lemma simplify_ccompl_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (cond_int64s c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmpl_bool c v v0)). +Proof. + intros. + unfold cond_int64s in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpl. + 1,2,3: rewrite optbool_mktotal; trivial. + - apply xor_neg_ltle_cmpl. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpl_bool; trivial. + rewrite optbool_mktotal; trivial. + - apply xor_neg_ltge_cmpl. +Qed. + +Lemma simplify_ccomplu_correct ge sp hst st c r r0 rs0 m m0 v v0: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj + (cond_int64u c + (make_lhsv_cmp (is_inv_cmp_int c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)) None)) rs0 m0 = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v v0)). +Proof. + intros. + erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)). + 2: eauto. + unfold cond_int64u in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmplu. + 1,2,3: rewrite optbool_mktotal; trivial. + - apply xor_neg_ltle_cmplu. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmplu_bool; trivial. + rewrite optbool_mktotal; trivial. + - apply xor_neg_ltge_cmplu. +Qed. + +Lemma simplify_ccompluimm_correct ge sp hst st c r n rs0 m m0 v: forall + (SMEM : forall (m : mem) (b : Values.block) (ofs : Z), + seval_smem ge sp (si_smem st) rs0 m0 = Some m -> + Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OK2 : seval_smem ge sp (si_smem st) rs0 m0 = Some m), + seval_sval ge sp + (hsval_proj (expanse_condimm_int64u c (fsi_sreg_get hst r) n)) rs0 m0 = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n))). +Proof. + intros. + assert (HMEM: Val.cmplu_bool (Mem.valid_pointer m) c v (Vlong n) = + Val.cmplu_bool (Mem.valid_pointer m0) c v (Vlong n)). + erewrite (cmplu_bool_valid_pointer_eq (Mem.valid_pointer m) (Mem.valid_pointer m0)); eauto. + unfold expanse_condimm_int64u, cond_int64u in *; destruct c; + intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + unfold loadimm64, sltuimm64, opimm64, load_hilo64; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + unfold Val.cmplu, zero64. + (* Simplify make immediate and decompose subcases *) + all: + try (specialize make_immed64_sound with n; + destruct (make_immed64 n) eqn:EQMKI); + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try erewrite fSop_correct; eauto; simpl; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; + try rewrite OK2; + rewrite HMEM. + (* Ceq, Cne, Clt = itself *) + all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial. + (* Cle = xor (Clt) *) + all: try apply xor_neg_ltle_cmplu; trivial. + (* Others subcases with swap/negation *) + all: + unfold Val.cmplu; + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; + try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; + trivial; fail); + try (replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmplu_bool; trivial; fail); + try (replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmplu_bool; rewrite xor_neg_optb; trivial; fail); + rewrite optbool_mktotal; trivial. + all: + try rewrite HMEM; trivial; + rewrite <- xor_neg_ltge_cmplu; unfold Val.cmplu; rewrite <- optbool_mktotal; trivial. +Qed. + +Lemma simplify_ccompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp false cond_float c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (Val.cmpf_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpf. + - apply xor_neg_eqne_cmpf. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpf_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpf_bool; trivial. +Qed. + +Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp true cond_float c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpf. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl. + all: destruct (Float.cmp _ _ _); trivial. +Qed. + +Lemma simplify_ccompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp false cond_single c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (Val.cmpfs_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpfs. + - apply xor_neg_eqne_cmpfs. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpfs_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpfs_bool; trivial. +Qed. + +Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (OKv1 : seval_sval ge sp (si_sreg st r) rs0 m0 = Some v) + (OKv2 : seval_sval ge sp (si_sreg st r0) rs0 m0 = Some v0), + seval_sval ge sp + (hsval_proj + (expanse_cond_fp true cond_single c + (make_lhsv_cmp (is_inv_cmp_float c) (fsi_sreg_get hst r) + (fsi_sreg_get hst r0)))) rs0 m0 = + Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + erewrite !fsi_sreg_get_correct; eauto; + rewrite OKv1, OKv2; trivial; + unfold Val.cmpfs. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. + all: destruct (Float32.cmp _ _ _); trivial. +Qed. + +(* Main proof of simplification *) Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (H: target_op_simplify op lr hst = Some fsv) @@ -117,8 +810,40 @@ Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args) (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp op args m. -Proof. Admitted. (* - unfold target_op_simplify; simpl. congruence. - Qed.*) +Proof. + unfold target_op_simplify; simpl. + intros H (LREF & SREF & SREG & SMEM) ? ? ?. + destruct op; try congruence. + destruct cond; repeat (destruct lr; simpl; try congruence); + simpl in OK1; + try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); + try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); + inv H; inv OK1. + (* Ccomp *) + - eapply simplify_ccomp_correct; eauto. + (* Ccompu *) + - eapply simplify_ccompu_correct; eauto. + (* Ccompimm *) + - (* TODO gourdinl *) admit. + (* Ccompuimm *) + - eapply simplify_ccompuimm_correct; eauto. + (* Ccompl *) + - eapply simplify_ccompl_correct; eauto. + (* Ccomplu *) + - eapply simplify_ccomplu_correct; eauto. + (* Ccomplimm *) + - admit. + (* Ccompluimm *) + - eapply simplify_ccompluimm_correct; eauto. + (* Ccompf *) + - eapply simplify_ccompf_correct; eauto. + (* Cnotcompf *) + - eapply simplify_cnotcompf_correct; eauto. + (* Ccompfs *) + - eapply simplify_ccompfs_correct; eauto. + (* Cnotcompfs *) + - eapply simplify_cnotcompfs_correct; eauto. + Admitted. +(*Qed.*) Global Opaque target_op_simplify. 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