diff options
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 156 |
1 files changed, 70 insertions, 86 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 5b44caba..c453dfb8 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -30,9 +30,9 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := Definition make_lhsv_single (hvs: hsval) : list_hsval := fScons hvs fSnil. -(** Expansion functions *) +(** * Expansion functions *) -(* Immediate loads *) +(** ** Immediate loads *) Definition load_hilo32 (hi lo: int) := if Int.eq lo Int.zero then @@ -40,7 +40,7 @@ Definition load_hilo32 (hi lo: int) := else let hvs := fSop (OEluiw hi) fSnil in let hl := make_lhsv_single hvs in - fSop (OEaddiw lo) hl. + fSop (OEaddiw None lo) hl. Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then @@ -48,19 +48,19 @@ Definition load_hilo64 (hi lo: int64) := else let hvs := fSop (OEluil hi) fSnil in let hl := make_lhsv_single hvs in - fSop (OEaddil lo) hl. + fSop (OEaddil None lo) hl. Definition loadimm32 (n: int) := match make_immed32 n with | Imm32_single imm => - fSop (OEimmR0 (OPimmADD imm)) fSnil + fSop (OEaddiw (Some X0_R) imm) fSnil | Imm32_pair hi lo => load_hilo32 hi lo end. Definition loadimm64 (n: int64) := match make_immed64 n with | Imm64_single imm => - fSop (OEimmR0 (OPimmADDL imm)) fSnil + fSop (OEaddil (Some X0_R) imm) fSnil | Imm64_pair hi lo => load_hilo64 hi lo | Imm64_large imm => fSop (OEloadli imm) fSnil end. @@ -91,20 +91,20 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper fSop op hl end. -Definition addimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oadd OEaddiw. +Definition addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw. Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw. 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 addimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oaddl OEaddil. +Definition addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil. Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril. 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. -(* Comparisons intructions *) +(** ** Comparisons intructions *) Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with @@ -260,7 +260,7 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := let hl := make_lhsv_single hvs in if normal' then hvs else fSop (OExoriw Int.one) hl. -(* Branches instructions *) +(** ** Branches instructions *) Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := match cmp with @@ -309,18 +309,37 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con let hl := make_lhsv_cmp false hvs hvs in if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl). -(** Add pointer expansion *) +(** ** Add pointer expansion *) -(*Definition addptrofs (hv1: hsval) (n: ptrofs) :=*) - (*if Ptrofs.eq_dec n Ptrofs.zero then*) - (*let lhsv := make_lhsv_single hv1 in*) - (*fSop Omove lhsv*) - (*else*) - (*if Archi.ptr64*) - (*then addimm64 hv1 (Ptrofs.to_int64 n)*) - (*else addimm32 hv1 (Ptrofs.to_int n).*) - -(** Target op simplifications using "fake" values *) +Definition addptrofs (n: ptrofs) := + if Ptrofs.eq_dec n Ptrofs.zero then + fSop OEmoveSP fSnil + else + if Archi.ptr64 + then ( + match make_immed64 (Ptrofs.to_int64 n) with + | Imm64_single imm => + fSop (OEaddil (Some SP_S) imm) fSnil + | Imm64_pair hi lo => + let hvs := load_hilo64 hi lo in + let hl := make_lhsv_single hvs in + fSop (OEaddil (Some SP_S) Int64.zero) hl + | Imm64_large imm => + let hvs := fSop (OEloadli imm) fSnil in + let hl := make_lhsv_single hvs in + fSop (OEaddil (Some SP_S) Int64.zero) hl + end) + else ( + match make_immed32 (Ptrofs.to_int n) with + | Imm32_single imm => + fSop (OEaddiw (Some SP_S) imm) fSnil + | Imm32_pair hi lo => + let hvs := load_hilo32 hi lo in + let hl := make_lhsv_single hvs in + fSop (OEaddiw (Some SP_S) Int.zero) hl + end). + +(** * Target simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := match op, lr with @@ -402,10 +421,10 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca Some (loadimm64 n) | Oaddimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in - Some (addimm32 hv1 n) + Some (addimm32 hv1 n None) | Oaddlimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in - Some (addimm64 hv1 n) + Some (addimm64 hv1 n None) | Oandimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in Some (andimm32 hv1 n) @@ -442,9 +461,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then - let move_s := fSop Omove hl in - let move_l := make_lhsv_cmp false move_s move_s in - Some (fSop (OEmayundef (MUshrx n)) move_l) + let lhl := make_lhsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrx n)) lhl) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in @@ -468,9 +486,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then - let move_s := fSop Omove hl in - let move_l := make_lhsv_cmp false move_s move_s in - Some (fSop (OEmayundef (MUshrxl n)) move_l) + let lhl := make_lhsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrxl n)) lhl) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in @@ -490,9 +507,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let srail_s' := fSop (Oshrlimm n) addl_l in let srail_l' := make_lhsv_cmp false srail_s' srail_s' in Some (fSop (OEmayundef (MUshrxl n)) srail_l') - (*| Oaddrstack n, nil =>*) - (*let hv1 := fsi_sreg_get hst a1 in*) - (*OK (addptrofs hv1 n)*) + (* TODO gourdinl | Oaddrstack n, nil =>*) + (*Some (addptrofs n)*) | _, _ => None end. @@ -601,9 +617,9 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args | _, _ => None end. -(** Auxiliary lemmas on comparisons *) +(** * Auxiliary lemmas on comparisons *) -(* Signed ints *) +(** ** Signed ints *) Lemma xor_neg_ltle_cmp: forall v1 v2, Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = @@ -618,7 +634,7 @@ Proof. auto. Qed. -(* Unsigned ints *) +(** ** Unsigned ints *) Lemma xor_neg_ltle_cmpu: forall mptr v1 v2, Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = @@ -652,7 +668,7 @@ Proof. rewrite !Int.unsigned_repr; try cbn; try omega. Qed. -(* Signed longs *) +(** ** Signed longs *) Lemma xor_neg_ltle_cmpl: forall v1 v2, Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = @@ -748,7 +764,7 @@ Proof. apply Z.le_ge. trivial. Qed. -(* Unsigned longs *) +(** ** Unsigned longs *) 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)) = @@ -794,7 +810,7 @@ Proof. repeat destruct (_ && _); simpl; auto. Qed. -(* Floats *) +(** ** Floats *) Lemma xor_neg_eqne_cmpf: forall v1 v2, Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = @@ -807,7 +823,7 @@ Proof. destruct (Float.cmp _ _ _); simpl; auto. Qed. -(* Singles *) +(** ** Singles *) Lemma xor_neg_eqne_cmpfs: forall v1 v2, Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = @@ -820,7 +836,7 @@ Proof. destruct (Float32.cmp _ _ _); simpl; auto. Qed. -(* More useful lemmas *) +(** ** More useful lemmas *) Lemma xor_neg_optb: forall v, Some (Val.xor (Val.of_optbool (option_map negb v)) @@ -863,7 +879,7 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. -(* Intermediates lemmas on each expansed instruction *) +(** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall (SREG: forall r: positive, @@ -1026,7 +1042,6 @@ Proof. try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; try rewrite Int.add_commut, Int.add_zero_l in *; - try rewrite Int.add_commut; try rewrite Int.add_zero_l; try destruct (Int.ltu _ _) eqn:EQLTU; simpl; try rewrite EQLTU; simpl; try rewrite EQIMM; @@ -1149,25 +1164,21 @@ Proof. 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; try rewrite Int64.add_commut, Int64.add_zero_l in *; - try rewrite Int64.add_commut; - try rewrite Int64.add_zero_l; try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); try rewrite xor_neg_ltge_cmpl; trivial; try rewrite xor_neg_ltle_cmpl; trivial. 6: - try rewrite Int64.add_commut; rewrite <- H; try apply cmpl_ltle_add_one; auto. all: try rewrite <- H; try apply cmpl_ltle_add_one; auto; + try rewrite <- cmpl_ltle_add_one; auto; try rewrite ltu_12_wordsize; try rewrite Int.add_commut, Int.add_zero_l in *; try rewrite Int64.add_commut, Int64.add_zero_l in *; - try rewrite Int.add_commut; - try rewrite Int64.add_commut; try rewrite Int64.add_zero_l; simpl; try rewrite lt_maxsgn_false_long; try (rewrite <- H; trivial; fail); @@ -1216,7 +1227,6 @@ Proof. unfold Val.cmplu, eval_may_undef, zero64, Val.addl; try apply Int64.same_if_eq in EQLO; subst; try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; - try rewrite Int64.add_commut; try rewrite Int64.add_zero_l; try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; trivial; fail); @@ -1362,8 +1372,7 @@ Proof. - apply Int64.same_if_eq in EQLO; subst. try rewrite Int64.add_commut, Int64.add_zero_l in H. rewrite <- H; try rewrite Float.of_to_bits; trivial. - - try rewrite Int64.add_commut; - rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. - rewrite <- H; try rewrite Float.of_to_bits; trivial. Qed. @@ -1392,7 +1401,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l in H; simpl; - try rewrite Int.add_commut in H; rewrite ltu_12_wordsize; simpl; try rewrite <- H; try rewrite Float32.of_to_bits; trivial. Qed. @@ -1403,7 +1411,7 @@ Lemma simplify_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with | nil => None - | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n) + | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), @@ -1423,7 +1431,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1433,7 +1440,7 @@ Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with | nil => None - | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n) + | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), @@ -1483,7 +1490,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1543,7 +1549,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1595,7 +1600,6 @@ Proof. try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; try rewrite H; trivial. Qed. @@ -1690,9 +1694,8 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall then Some (fSop (OEmayundef (MUshrx n)) - (make_lhsv_cmp false - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) else if Int.eq n Int.one then @@ -1794,9 +1797,8 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall then Some (fSop (OEmayundef (MUshrxl n)) - (make_lhsv_cmp false - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) else if Int.eq n Int.one then @@ -1885,7 +1887,7 @@ Proof. destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. rewrite !EQN2. rewrite EQN0. reflexivity. - Qed. +Qed. Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall (SREG: forall r: positive, @@ -1924,7 +1926,7 @@ Proof. rewrite Int64.shru'_zero. reflexivity. Qed. -(* Main proof of simplification *) +(** * 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) @@ -1937,28 +1939,22 @@ Proof. unfold target_op_simplify; simpl. intros H (LREF & SREF & SREG & SMEM) ? ? ?. destruct op; try congruence. - (* int and long constants *) eapply simplify_intconst_correct; eauto. eapply simplify_longconst_correct; eauto. - (* FP const expansions *) eapply simplify_floatconst_correct; eauto. eapply simplify_singleconst_correct; eauto. - (* cast 8/16 operations *) + (* TODO gourdinl*) + (*admit.*) eapply simplify_cast8signed_correct; eauto. eapply simplify_cast16signed_correct; eauto. - (* Immediate int operations *) eapply simplify_addimm_correct; eauto. eapply simplify_andimm_correct; eauto. eapply simplify_orimm_correct; eauto. - (* Shrx imm int operation *) eapply simplify_shrximm_correct; eauto. - (* cast 32u operation *) eapply simplify_cast32unsigned_correct; eauto. - (* Immediate long operations *) eapply simplify_addlimm_correct; eauto. eapply simplify_andlimm_correct; eauto. eapply simplify_orlimm_correct; eauto. - (* Shrx imm long operation *) eapply simplify_shrxlimm_correct; eauto. (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); @@ -1966,31 +1962,20 @@ Proof. 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 *) - eapply simplify_ccompimm_correct; eauto. - (* Ccompuimm *) - eapply simplify_ccompuimm_correct; eauto. - (* Ccompl *) - eapply simplify_ccompl_correct; eauto. - (* Ccomplu *) - eapply simplify_ccomplu_correct; eauto. - (* Ccomplimm *) - eapply simplify_ccomplimm_correct; eauto. - (* 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. Qed. +(*Admitted.*) Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall (TARGET: target_cbranch_expanse hst c l = Some (c', l')) @@ -2042,7 +2027,6 @@ Proof. try destruct v; try rewrite H; try rewrite ltu_12_wordsize; try rewrite EQLO; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite Int64.add_commut, Int64.add_zero_l; try rewrite Int64.add_commut; try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l; |