Commit d472be24 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

xorimm

parent b9e034e7
Pipeline #68318 waiting for manual action with stage
......@@ -886,6 +886,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
......
......@@ -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
......@@ -1550,6 +1556,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)
......@@ -1916,11 +1981,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);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment