diff options
Diffstat (limited to 'riscV/RTLpathSE_simplify.v')
| -rw-r--r-- | riscV/RTLpathSE_simplify.v | 204 |
1 files changed, 118 insertions, 86 deletions
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 5804e67e..6066c7f5 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -165,7 +165,7 @@ Definition expanse_condimm_int32s (cmp: comparison) (hv1: hsval) (n: int) := if Int.eq n (Int.repr Int.max_signed) then let hvs := loadimm32 Int.one in let hl := make_lhsv_cmp false hv1 hvs in - fSop (OEmayundef false) hl + fSop (OEmayundef MUint) hl else sltimm32 hv1 (Int.add n Int.one) | _ => let optR0 := make_optR0 false is_inv in @@ -208,7 +208,7 @@ Definition expanse_condimm_int64s (cmp: comparison) (hv1: hsval) (n: int64) := if Int64.eq n (Int64.repr Int64.max_signed) then let hvs := loadimm32 Int.one in let hl := make_lhsv_cmp false hv1 hvs in - fSop (OEmayundef true) hl + fSop (OEmayundef MUlong) hl else sltimm64 hv1 (Int64.add n Int64.one) | _ => let optR0 := make_optR0 false is_inv in @@ -440,8 +440,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca 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_single move_s in - Some (fSop (OEshrxundef n) move_l) + let move_l := make_lhsv_cmp false move_s move_s in + Some (fSop (OEmayundef (MUshrx n)) move_l) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in @@ -449,8 +449,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addw_s := fSop Oadd srliw_l in let addw_l := make_lhsv_single addw_s in let sraiw_s := fSop (Oshrimm Int.one) addw_l in - let sraiw_l := make_lhsv_single sraiw_s in - Some (fSop (OEshrxundef n) sraiw_l) + let sraiw_l := make_lhsv_cmp false sraiw_s sraiw_s in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l) else let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in let sraiw_l := make_lhsv_single sraiw_s in @@ -459,15 +459,15 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addw_s := fSop Oadd srliw_l in let addw_l := make_lhsv_single addw_s in let sraiw_s' := fSop (Oshrimm n) addw_l in - let sraiw_l' := make_lhsv_single sraiw_s' in - Some (fSop (OEshrxundef n) sraiw_l') + let sraiw_l' := make_lhsv_cmp false sraiw_s' sraiw_s' in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l') | Oshrxlimm n, a1 :: nil => 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_single move_s in - Some (fSop (OEshrxlundef n) move_l) + let move_l := make_lhsv_cmp false move_s move_s in + Some (fSop (OEmayundef (MUshrxl n)) move_l) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in @@ -475,8 +475,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addl_s := fSop Oaddl srlil_l in let addl_l := make_lhsv_single addl_s in let srail_s := fSop (Oshrlimm Int.one) addl_l in - let srail_l := make_lhsv_single srail_s in - Some (fSop (OEshrxlundef n) srail_l) + let srail_l := make_lhsv_cmp false srail_s srail_s in + Some (fSop (OEmayundef (MUshrxl n)) srail_l) else let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in let srail_l := make_lhsv_single srail_s in @@ -485,8 +485,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let addl_s := fSop Oaddl srlil_l in let addl_l := make_lhsv_single addl_s in let srail_s' := fSop (Oshrlimm n) addl_l in - let srail_l' := make_lhsv_single srail_s' in - Some (fSop (OEshrxlundef n) srail_l') + 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)*) @@ -964,7 +964,7 @@ Proof. try rewrite OKv1; try rewrite OK2; try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; - unfold Val.cmp, may_undef_int, zero32, Val.add; simpl; + unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl; destruct v; auto. all: try rewrite ltu_12_wordsize; @@ -1018,7 +1018,7 @@ Proof. try rewrite OKv1; try rewrite OK2; rewrite HMEM; - unfold may_undef_int, Val.cmpu; + unfold eval_may_undef, Val.cmpu; destruct v; simpl; auto; try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; @@ -1141,7 +1141,7 @@ Proof. unfold Val.cmpl, Val.addl; try rewrite xorl_zero_eq_cmpl; trivial; try rewrite optbool_mktotal; trivial; - unfold may_undef_int, zero32, Val.add; simpl; + unfold eval_may_undef, zero32, Val.add; simpl; destruct v; auto. 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; @@ -1210,7 +1210,7 @@ Proof. all: try apply xor_neg_ltle_cmplu; trivial. (* Others subcases with swap/negation *) all: - unfold Val.cmplu, may_undef_int, zero64, Val.addl; + 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; @@ -1681,41 +1681,57 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with - | nil => None - | a1 :: nil => - if Int.eq n Int.zero - then - Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) - else - if Int.eq n Int.one + | nil => None + | a1 :: nil => + if Int.eq n Int.zero then Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop (Oshrimm Int.one) - (make_lhsv_single - (fSop Oadd - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshruimm (Int.repr 31)) - (make_lhsv_single (fsi_sreg_get hst a1))))))))) + (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))))) else - Some - (fSop (OEshrxundef n) - (make_lhsv_single - (fSop (Oshrimm n) - (make_lhsv_single - (fSop Oadd - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshruimm (Int.sub Int.iwordsize n)) - (make_lhsv_single - (fSop (Oshrimm (Int.repr 31)) - (make_lhsv_single - (fsi_sreg_get hst a1))))))))))) - | a1 :: _ :: _ => None - end = Some fsv) + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrx n)) + (make_lhsv_cmp false + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp (Oshrximm n) args m. @@ -1734,7 +1750,7 @@ Proof. erewrite !fsi_sreg_get_correct; eauto; destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn; - unfold shrx_imm_undef. + unfold eval_may_undef. 2,4,6: unfold Val.shrx in TOTAL; destruct v; simpl in TOTAL; simpl; try congruence; @@ -1769,41 +1785,57 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with - | nil => None - | a1 :: nil => - if Int.eq n Int.zero - then - Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) - else - if Int.eq n Int.one + | nil => None + | a1 :: nil => + if Int.eq n Int.zero then Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop (Oshrlimm Int.one) - (make_lhsv_single - (fSop Oaddl - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshrluimm (Int.repr 63)) - (make_lhsv_single (fsi_sreg_get hst a1))))))))) + (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))))) else - Some - (fSop (OEshrxlundef n) - (make_lhsv_single - (fSop (Oshrlimm n) - (make_lhsv_single - (fSop Oaddl - (make_lhsv_cmp false (fsi_sreg_get hst a1) - (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) - (make_lhsv_single - (fSop (Oshrlimm (Int.repr 63)) - (make_lhsv_single - (fsi_sreg_get hst a1))))))))))) - | a1 :: _ :: _ => None - end = Some fsv) + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))) + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lhsv_cmp false + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))) + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), seval_sval ge sp (hsval_proj fsv) rs0 m0 = eval_operation ge sp (Oshrxlimm n) args m. @@ -1822,7 +1854,7 @@ Proof. erewrite !fsi_sreg_get_correct; eauto; destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn; - unfold shrxl_imm_undef. + unfold eval_may_undef. 2,4,6: unfold Val.shrxl in TOTAL; destruct v; simpl in TOTAL; simpl; try congruence; @@ -1850,7 +1882,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, @@ -2001,7 +2033,7 @@ Proof. try destruct (Int64.eq lo Int64.zero) eqn:EQLO; try apply Int.same_if_eq in EQLO; simpl; trivial; try apply Int64.same_if_eq in EQLO; simpl; trivial; - unfold may_undef_int; + unfold eval_may_undef; try erewrite !fsi_sreg_get_correct; eauto; try rewrite OKv1; simpl; trivial; try destruct v; try rewrite H; |