From 77f3fd97849ad7daa0c6e29c1d7d511d94fb4455 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 16:57:27 +0200 Subject: adding missing xorimm exp --- riscV/ExpansionOracle.ml | 10 +++++++ riscV/RTLpathSE_simplify.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 77 insertions(+) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index b8a7f6e7..4f67b9af 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -885,6 +885,16 @@ let expanse (sb : superblock) code pm = exp := orimm64 vn a1 dest n; exp := extract_final vn !exp dest succ; was_exp := true + | Iop (Oxorimm n, a1 :: nil, dest, succ) -> + if exp_debug then eprintf "Iop/Oxorimm\n"; + exp := xorimm32 vn a1 dest n; + exp := extract_final vn !exp dest succ; + was_exp := true + | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> + if exp_debug then eprintf "Iop/Oxorlimm\n"; + exp := xorimm64 vn a1 dest n; + exp := extract_final vn !exp dest succ; + was_exp := true | Iop (Ocast8signed, a1 :: nil, dest, succ) -> if exp_debug then eprintf "Iop/cast8signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 24)) in diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 33e2db61..7aca1772 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -407,6 +407,12 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca | Oorlimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in Some (orimm64 hv1 n) + | Oxorimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (xorimm32 hv1 n) + | Oxorlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (xorimm64 hv1 n) | Ocast8signed, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in @@ -1560,6 +1566,65 @@ Proof. try rewrite ltu_12_wordsize; trivial. Qed. +Lemma simplify_xorimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + 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 => Some (xorimm32 (fsi_sreg_get hst a1) n) + | 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 (Oxorimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold xorimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.xor (Vint imm) v); rewrite Val.xor_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_xorlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + 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 => Some (xorimm64 (fsi_sreg_get hst a1) n) + | 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 (Oxorlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold xorimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.xorl (Vlong imm) v); rewrite Val.xorl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + Lemma simplify_intconst_correct ge sp rs0 m0 args m n fsv lr st: forall (H : match lr with | nil => Some (loadimm32 n) @@ -1926,11 +1991,13 @@ Proof. eapply simplify_addimm_correct; eauto. eapply simplify_andimm_correct; eauto. eapply simplify_orimm_correct; eauto. + eapply simplify_xorimm_correct; eauto. eapply simplify_shrximm_correct; eauto. eapply simplify_cast32unsigned_correct; eauto. eapply simplify_addlimm_correct; eauto. eapply simplify_andlimm_correct; eauto. eapply simplify_orlimm_correct; eauto. + eapply simplify_xorlimm_correct; eauto. eapply simplify_shrxlimm_correct; eauto. (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); -- cgit