xorimmsubmission_OOPSLA2021_RISCV

2 files changed, 77 insertions, 0 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 092bf0d1..def90a6a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -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
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index d55d94ad..ca049962 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
@@ -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);