Adding a mini CSE pass in the expansion oracle

1 files changed, 20 insertions, 21 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 97f3ff61..d50bd00f 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -27,24 +27,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval :=
+Definition may_undef_int (is_long: bool) (v1 v2: aval): aval :=
   if negb is_long then
     match v1 with
-    | I _ => sem vimm vz
+    | I _ => v2
     | _ => Ifptr Ptop
     end
   else
     match v1 with
-    | L _ => sem vimm vz
+    | L _ => v2
     | _ => Ifptr Ptop
     end.
 
-Definition may_undef_luil (v1: aval) (n: int64): aval :=
-  match v1 with
-  | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
-  | _ => 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
@@ -223,8 +217,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
   | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
   | OExoriw n, v1::nil => xor v1 (I n)
-  | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12))
-  | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32
+  | OEluiw n, nil => shl (I n) (I (Int.repr 12))
+  | OEaddiwr0 n, nil => add (I n) zero32
   | 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)
@@ -234,9 +228,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
   | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
   | OExoril n, v1::nil => xorl v1 (L n)
-  | OEluil n, v1::nil => may_undef_luil v1 n
-  | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64
+  | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
+  | 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
   | 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)
@@ -464,14 +459,18 @@ Proof.
   1,2,3: apply eval_cmp_sound; auto.
   unfold Val.cmp; apply of_optbool_sound; eauto with va.
   unfold Val.cmpu; apply of_optbool_sound; eauto with va.
-  unfold zero32; simpl; eauto with va.
-
-  1,2,11,12:
-    try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64;
-    try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1;
-    inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va;
-    try apply vmatch_ifptr_i; try apply vmatch_ifptr_l.
-
+  
+  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.
+  1,10: simpl; eauto with va.
+  9:
+    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.