From 95205e72ca536907fa89c7c884f0e22fc605063d Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 26 Mar 2021 12:49:02 +0100
Subject: Adding more expansions, improving miniCSE, and tuning prepass

---
 riscV/ValueAOp.v | 65 ++++++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 56 insertions(+), 9 deletions(-)

(limited to 'riscV/ValueAOp.v')

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index d50bd00f..fe519921 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -39,6 +39,32 @@ Definition may_undef_int (is_long: bool) (v1 v2: aval): aval :=
     | _ => Ifptr Ptop
     end.
 
+Definition shrx_imm_undef (v1 v2: aval): aval :=
+  match v1 with
+  | I n1 =>
+      match v2 with
+      | I n2 =>
+          if Int.ltu n2 (Int.repr 31)
+          then I n1
+          else Ifptr Ptop
+      | _ => Ifptr Ptop
+      end
+  | _ => Ifptr Ptop
+  end.
+
+Definition shrxl_imm_undef (v1 v2: aval): aval :=
+  match v1 with
+  | L n1 =>
+      match v2 with
+      | I n2 =>
+          if Int.ltu n2 (Int.repr 63)
+          then L n1
+          else Ifptr Ptop
+      | _ => Ifptr Ptop
+      end
+  | _ => Ifptr Ptop
+  end.
+
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
@@ -218,7 +244,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
   | OExoriw n, v1::nil => xor v1 (I n)
   | OEluiw n, nil => shl (I n) (I (Int.repr 12))
+  | OEaddiw n, v1::nil => add (I n) v1
   | OEaddiwr0 n, nil => add (I n) zero32
+  | OEandiw n, v1::nil => and (I n) v1
+  | OEoriw n, v1::nil => or (I n) v1
   | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
   | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64)
   | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64)
@@ -227,11 +256,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64)
   | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
   | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
+  | OEandil n, v1::nil => andl (L n) v1
+  | OEoril n, v1::nil => orl (L n) v1
   | OExoril n, v1::nil => xorl v1 (L n)
   | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
+  | OEaddil n, v1::nil => addl (L n) v1
   | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
   | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2
+  | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n)
+  | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I n)
   | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
   | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2)
   | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2)
@@ -460,22 +494,35 @@ Proof.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
   unfold Val.cmpu; apply of_optbool_sound; eauto with va.
   
-  simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
-  try apply vmatch_ifptr_undef.
-  10:
-    simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
-    apply vmatch_ifptr_l.
+  { fold (Val.add (Vint n) a1); eauto with va. }
+  { unfold zero32; simpl; eauto with va. }
+  { fold (Val.and (Vint n) a1); eauto with va. }
+  { fold (Val.or (Vint n) a1); eauto with va. }
+  { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
+  try apply vmatch_ifptr_undef. }
+  9: { fold (Val.addl (Vlong n) a1); eauto with va. }
+  10: { fold (Val.andl (Vlong n) a1); eauto with va. }
+  10: { fold (Val.orl (Vlong n) a1); eauto with va. }
+  10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
+  apply vmatch_ifptr_l. }
+  
   1,10: simpl; eauto with va.
-  9:
+  2:
     unfold Op.may_undef_int, may_undef_int; destruct is_long;
     simpl; inv H0; inv H1; eauto with va; inv H;
     apply vmatch_ifptr_p; eauto with va.
   
   3,4,6: apply eval_cmplu_sound; auto.
   1,2,3: apply eval_cmpl_sound; auto.
-  unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va.
-  unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va.
-  unfold zero64; simpl; eauto with va.
+  { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. }
+  { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. }
+  { unfold zero64; simpl; eauto with va. }
+  { unfold Op.shrx_imm_undef, shrx_imm_undef.
+    simpl; inv H1; eauto with va;
+    destruct (Int.ltu _ _); simpl; eauto with va. }
+  { unfold Op.shrxl_imm_undef, shrxl_imm_undef.
+    simpl; inv H1; eauto with va;
+    destruct (Int.ltu _ _); simpl; eauto with va. }
   all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.
 
-- 
cgit