Adding a mini CSE pass in the expansion oracle

1 files changed, 27 insertions, 36 deletions

diff --git a/riscV/Op.v b/riscV/Op.v
index 8b4d444d..d902c907 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -181,8 +181,8 @@ Inductive operation : Type :=
   | OEsltiw (n: int)                             (**r set-less-than immediate *)
   | OEsltiuw (n: int)                            (**r set-less-than unsigned immediate *)
   | OExoriw (n: int)                             (**r xor immediate *)
-  | OEluiw (n: int) (is_long: bool)              (**r load upper-immediate *)
-  | OEaddiwr0 (n: int) (is_long: bool)           (**r add immediate *)
+  | OEluiw (n: int)                              (**r load upper-immediate *)
+  | OEaddiwr0 (n: int)                           (**r add immediate *)
   | OEseql (optR0: option bool)                  (**r [rd <- rs1 == rs2] signed *)
   | OEsnel (optR0: option bool)                  (**r [rd <- rs1 != rs2] signed *)
   | OEsequl (optR0: option bool)                 (**r [rd <- rs1 == rs2] unsigned *)
@@ -195,6 +195,7 @@ Inductive operation : Type :=
   | OEluil (n: int64)                            (**r load upper-immediate *)
   | OEaddilr0 (n: int64)                         (**r add immediate *)
   | OEloadli (n: int64)                          (**r load an immediate int64 *)
+  | OEmayundef (is_long: bool)
   | OEfeqd                                       (**r compare equal *)
   | OEfltd                                       (**r compare less-than *)
   | OEfled                                       (**r compare less-than/equal *)
@@ -269,24 +270,18 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: val -> val -> B) (v1 v2 v
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (sem: val -> val -> val) (v1 vimm vz: val): val :=
+Definition may_undef_int (is_long: bool) (v1 v2: val): val :=
   if negb is_long then
     match v1 with
-    | Vint _ => sem vimm vz
+    | Vint _ => v2
     | _ => Vundef
     end
   else
     match v1 with
-    | Vlong _ => sem vimm vz
+    | Vlong _ => v2
     | _ => Vundef
     end.
 
-Definition may_undef_luil (v1: val) (n: int64): val :=
-  match v1 with
-  | Vlong _ => Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))
-  | _ => Vundef
-  end.
-
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -432,8 +427,8 @@ Definition eval_operation
   | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
   | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
   | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
-  | OEluiw n is_long, v1::nil => Some (may_undef_int is_long Val.shl v1 (Vint n) (Vint (Int.repr 12)))
-  | OEaddiwr0 n is_long, v1::nil => Some (may_undef_int is_long Val.add v1 (Vint n) zero32)
+  | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
+  | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32)
   | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64))
   | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64))
   | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
@@ -443,9 +438,10 @@ Definition eval_operation
   | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
   | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
   | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
-  | OEluil n, v1::nil => Some (may_undef_luil v1 n)
-  | OEaddilr0 n, v1::nil => Some (may_undef_int true Val.addl v1 (Vlong n) zero64)
+  | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
+  | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64)
   | OEloadli n, nil => Some (Vlong n)
+  | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2)
   | OEfeqd, v1::v2::nil => Some (Val.cmpf Ceq v1 v2)
   | OEfltd, v1::v2::nil => Some (Val.cmpf Clt v1 v2)
   | OEfled, v1::v2::nil => Some (Val.cmpf Cle v1 v2)
@@ -634,8 +630,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltiw _ => (Tint :: nil, Tint)
   | OEsltiuw _ => (Tint :: nil, Tint)
   | OExoriw _ => (Tint :: nil, Tint)
-  | OEluiw _ _ => (Tint :: nil, Tint)
-  | OEaddiwr0 _ _ => (Tint :: nil, Tint)
+  | OEluiw _ => (nil, Tint)
+  | OEaddiwr0 _ => (nil, Tint)
   | OEseql _ => (Tlong :: Tlong :: nil, Tint)
   | OEsnel _ => (Tlong :: Tlong :: nil, Tint)
   | OEsequl _ => (Tlong :: Tlong :: nil, Tint)
@@ -645,9 +641,10 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | OEsltil _ => (Tlong :: nil, Tint)
   | OEsltiul _ => (Tlong :: nil, Tint)
   | OExoril _ => (Tlong :: nil, Tlong)
-  | OEluil _ => (Tlong :: nil, Tlong)
-  | OEaddilr0 _ => (Tlong :: nil, Tlong)
+  | OEluil _ => (nil, Tlong)
+  | OEaddilr0 _ => (nil, Tlong)
   | OEloadli _ => (nil, Tlong)
+  | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64)
   | OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfltd => (Tfloat :: Tfloat :: nil, Tint)
   | OEfled => (Tfloat :: Tfloat :: nil, Tint)
@@ -892,10 +889,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - destruct v0...
   (* OEluiw *)
   - unfold may_undef_int;
-    destruct v0, is_long; simpl; trivial;
     destruct (Int.ltu _ _); cbn; trivial.
   (* OEaddiwr0 *)
-  - destruct v0, is_long; simpl; trivial.
+  - simpl; trivial.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold Val.cmpl;
     destruct Val.cmpl_bool... all: destruct b...
@@ -922,11 +918,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* OExoril *)
   - destruct v0...
   (* OEluil *)
-  - destruct v0; simpl; trivial.
+  - simpl; trivial.
   (* OEaddilr0 *)
-  - destruct v0; simpl; trivial.
+  - simpl; trivial.
   (* OEloadli *)
   - trivial.
+  (* OEmayundef *)
+  - unfold may_undef_int;
+    destruct is_long, v0, v1; simpl; trivial.
   (* OEfeqd *)
   - destruct v0; destruct v1; cbn; auto.
     destruct Float.cmp; cbn; auto.
@@ -1740,14 +1739,7 @@ Proof.
   (* OExoriw *)
   - inv H4; simpl; auto.
   (* OEluiw *)
-  - unfold may_undef_int;
-    destruct is_long;
-    inv H4; simpl; auto;
-    destruct (Int.ltu _ _); auto.
-  (* OEaddiwr0 *)
-  - unfold may_undef_int;
-    destruct is_long;
-    inv H4; simpl; auto.
+  - destruct (Int.ltu _ _); auto.
   (* OEseql *)
   - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl;
     inv H4; inv H2; simpl; try destruct (Int64.eq _ _); simpl; cbn; auto;
@@ -1772,11 +1764,10 @@ Proof.
   - apply eval_cmplu_bool_inj; auto.
   (* OExoril *)
   - inv H4; simpl; auto.
-  (* OEluil *)
-  - inv H4; simpl; auto.
-  (* OEaddilr0 *)
-  - unfold may_undef_int;
-    inv H4; simpl; auto.
+  (* OEmayundef *)
+  - destruct is_long; inv H4; inv H2;
+    unfold may_undef_int; simpl; auto;
+    eapply Val.inject_ptr; eauto.
   (* OEfeqd *)
   - inv H4; inv H2; cbn; simpl; auto.
     destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto.