From c19ecc9326d0278989d7651bf8c8cf0d1c387235 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Mar 2021 12:36:11 +0100 Subject: Adding a mini CSE pass in the expansion oracle --- riscV/Op.v | 63 +++++++++++++++++++++++++++----------------------------------- 1 file changed, 27 insertions(+), 36 deletions(-) (limited to 'riscV/Op.v') 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. -- cgit