From acb41b1af6e5e4c933e3be1b17f6e5012eca794d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Feb 2021 16:53:46 +0100 Subject: cond and branches expanded --- riscV/Asmgen.v | 88 ++++++-- riscV/Asmgenproof.v | 28 ++- riscV/Asmgenproof1.v | 81 ++++++- riscV/ExpansionOracle.ml | 432 ++++++++++++++++++++++---------------- riscV/Op.v | 295 ++++++++++++++++++++------ riscV/OpWeights.ml | 14 +- riscV/PrintOp.ml | 30 +++ riscV/ValueAOp.v | 16 +- scheduling/RTLpathCommon.ml | 2 +- scheduling/RTLpathScheduleraux.ml | 5 +- 10 files changed, 695 insertions(+), 296 deletions(-) diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index b3fb2350..4b27ee81 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -105,8 +105,8 @@ Definition addimm32 := opimm32 Paddw Paddiw. Definition andimm32 := opimm32 Pandw Pandiw. Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. -Definition sltimm32 := opimm32 Psltw Psltiw. -Definition sltuimm32 := opimm32 Psltuw Psltiuw. +(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*) +(* TODO REMOVE Definition sltuimm32 := opimm32 Psltuw Psltiuw.*) Definition load_hilo64 (r: ireg) (hi lo: int64) k := if Int64.eq lo Int64.zero then Pluil r hi :: k @@ -132,8 +132,8 @@ Definition addimm64 := opimm64 Paddl Paddil. Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. -Definition sltimm64 := opimm64 Psltl Psltil. -Definition sltuimm64 := opimm64 Psltul Psltiul. +(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*) +(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*) Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := if Ptrofs.eq_dec n Ptrofs.zero then @@ -145,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := (** Translation of conditional branches. *) -Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := +(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := match cmp with | Ceq => Pbeqw r1 r2 lbl | Cne => Pbnew r1 r2 lbl @@ -203,12 +203,26 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := | Cle => (Pfles rd fs1 fs2, true) | Cgt => (Pflts rd fs2 fs1, true) | Cge => (Pfles rd fs2 fs1, true) + end.*) + +Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) := + match optR0 with + | None => sem r1 r2 lbl + | Some true => sem X0 r1 lbl + | Some false => sem r1 X0 lbl + end. + +Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) := + match optR0 with + | None => sem r1 r2 + | Some true => sem X0 r1 + | Some false => sem r1 X0 end. - + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => +(* TODO REMOVE | Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cbranch_int32s c r1 r2 lbl :: k) | Ccompu c, a1 :: a2 :: nil => @@ -259,7 +273,44 @@ Definition transl_cbranch | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) + OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)*) + + | CEbeqw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) + | CEbnew optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k) + | CEbltw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k) + | CEbltuw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbltuw r1 r2 lbl :: k) + | CEbgew optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbgew r1 r2 lbl :: k) + | CEbgeuw optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbgeuw r1 r2 lbl :: k) + | CEbeql optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k) + | CEbnel optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k) + | CEbltl optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k) + | CEbltul optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbltul r1 r2 lbl :: k) + | CEbgel optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbgel r1 r2 lbl :: k) + | CEbgeul optR0, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k) | _, _ => Error(msg "Asmgen.transl_cond_branch") end. @@ -268,7 +319,7 @@ Definition transl_cbranch [rd] target register to 0 or 1 depending on the truth value of the condition. *) -Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := +(* TODO REMOVE Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := match cmp with | Ceq => Pseqw rd r1 r2 :: k | Cne => Psnew rd r1 r2 :: k @@ -342,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int match cmp with | Clt => sltuimm64 rd r1 n k | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) - end. + end. *) -(* TODO Definition transl_cond_op +(* TODO REMOVE Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => @@ -389,18 +440,11 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) | _, _ => Error(msg "Asmgen.transl_cond_op") - end.*) + end.*) (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) -Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) := - match optR0 with - | None => sem r1 r2 - | Some true => sem X0 r1 - | Some false => sem r1 X0 - end. - Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -711,11 +755,9 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - - (* TODO | Ocmp cmp, _ => + (* TODO REMOVE | Ocmp cmp, _ => do rd <- ireg_of res; - transl_cond_op cmp rd args k*) - + transl_cond_op cmp rd args k *) | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 6bacaa5c..52a3bf27 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -161,7 +161,7 @@ Proof. Qed. Hint Resolve addptrofs_label: labels. -Remark transl_cond_float_nolabel: +(* TODO REMOVE Remark transl_cond_float_nolabel: forall c r1 r2 r3 insn normal, transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. @@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel: transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. unfold transl_cond_single; intros. destruct c; inv H; exact I. -Qed. + Qed.*) Remark transl_cbranch_label: forall cond args lbl k c, transl_cbranch cond args lbl k = OK c -> tail_nolabel k c. Proof. intros. unfold transl_cbranch in H; destruct cond; TailNoLabel. -- destruct c0; simpl; TailNoLabel. + (* TODO REMOVE - destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct (Int.eq n Int.zero). destruct c0; simpl; TailNoLabel. @@ -211,15 +211,27 @@ Proof. destruct normal; TailNoLabel. - destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. + destruct normal; TailNoLabel.*) +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. Qed. -(* TODO Remark transl_cond_op_label: +(* TODO REMOVE Remark transl_cond_op_label: forall cond args r k c, transl_cond_op cond r args k = OK c -> tail_nolabel k c. Proof. intros. unfold transl_cond_op in H; destruct cond; TailNoLabel. - (* TODO - destruct c0; simpl; TailNoLabel. +- destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - unfold transl_condimm_int32s. destruct (Int.eq n Int.zero). @@ -254,7 +266,7 @@ Proof. + destruct c0; simpl; TailNoLabel. + destruct c0; simpl; try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]). - apply opimm64_label; intros; exact I.*) + apply opimm64_label; intros; exact I. - destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. destruct normal; TailNoLabel. @@ -291,7 +303,7 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - apply opimm64_label; intros; exact I. - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -(* TODO - eapply transl_cond_op_label; eauto.*) +(* TODO REMOVE - eapply transl_cond_op_label; eauto.*) - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 49635ebd..429c5fec 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -292,7 +292,7 @@ Qed. (** Translation of conditional branches *) -Lemma transl_cbranch_int32s_correct: +(* TODO REMOVE Lemma transl_cbranch_int32s_correct: forall cmp r1 r2 lbl (rs: regset) m b, Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = @@ -375,16 +375,16 @@ Proof. rewrite <- Float32.cmp_swap. auto. - simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. rewrite <- Float32.cmp_swap. auto. -Qed. + Qed.*) -Remark branch_on_X31: +(* TODO UNUSUED ? Remark branch_on_X31: forall normal lbl (rs: regset) m b, rs#X31 = Val.of_bool (eqb normal b) -> exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = eval_branch fn lbl rs m (Some b). Proof. intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. -Qed. + Qed.*) Ltac ArgsInv := repeat (match goal with @@ -417,7 +417,7 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. -- exists rs, (transl_cbranch_int32s c0 x x0 lbl). + (* TODO REMOVE - exists rs, (transl_cbranch_int32s c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. - exists rs, (transl_cbranch_int32u c0 x x0 lbl). intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. @@ -492,7 +492,68 @@ Proof. econstructor; econstructor. split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. + intros; Simpl.*) + +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. +- destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -528,7 +589,7 @@ Qed. (** Translation of condition operators *) -Lemma transl_cond_int32s_correct: +(* TODO REMOVE Lemma transl_cond_int32s_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m @@ -830,9 +891,9 @@ Proof. + apply DFL. + apply DFL. + apply DFL. -Qed. + Qed. -(* TODO Lemma transl_cond_op_correct: +Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> exists rs', @@ -1134,7 +1195,7 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* cond *) - (* TODO { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). + (* TODO REMOVE { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. }*) (* Expanded instructions from RTL *) 5: econstructor; split; try apply exec_straight_one; simpl; eauto; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 9e494d0a..af14811d 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -18,8 +18,6 @@ open RTL open Op open Asmgen open DebugPrint - -(*open PrintRTL*) open! Integers let reg = ref 1 @@ -102,150 +100,169 @@ let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul -let cond_int32s_x0 cmp a1 dest succ k = - match cmp with - | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltw (Some false), [ a1; a1 ], dest, succ) :: k - | Cle -> - Iop (OEsltw (Some true), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltw (Some true), [ a1; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltw (Some false), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k +let is_inv_cmp = function Cle | Cgt -> true | _ -> false -let cond_int32s_reg cmp a1 a2 dest succ k = - match cmp with - | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltw None, [ a1; a2 ], dest, succ) :: k - | Cle -> - Iop (OEsltw None, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltw None, [ a2; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltw None, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k +let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None -let cond_int32u_x0 cmp a1 dest succ k = +let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltuw (Some false), [ a1; a1 ], dest, succ) :: k - | Cle -> - Iop (OEsltuw (Some true), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltuw (Some true), [ a1; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltuw (Some false), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - -let cond_int32u_reg cmp a1 a2 dest succ k = + | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltuw None, [ a1; a2 ], dest, succ) :: k - | Cle -> - Iop (OEsltuw None, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltuw None, [ a2; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltuw None, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - -let cond_int64s_x0 cmp a1 dest succ k = + | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cond_int32s is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltl (Some false), [ a1; a1 ], dest, succ) :: k + | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltl (Some true), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64s_reg cmp a1 a2 dest succ k = +let cond_int32u is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltl None, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltl None, [ a2; a1 ], dest, n2pi ()) + Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltl None, [ a1; a2 ], dest, n2pi ()) + Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64u_x0 cmp a1 dest succ k = +let cond_int64s is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltul (Some false), [ a1; a1 ], dest, succ) :: k + | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltul (Some true), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64u_reg cmp a1 a2 dest succ k = +let cond_int64u is_x0 cmp a1 a2 dest succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltul None, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltul None, [ a2; a1 ], dest, n2pi ()) + Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltul None, [ a1; a2 ], dest, n2pi ()) + Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k +let is_normal_cmp = function Cne -> false | _ -> true + let cond_float cmp f1 f2 dest succ = match cmp with - | Ceq -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), true) - | Cne -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), false) - | Clt -> (Iop (OEfltd, [ f1; f2 ], dest, succ), true) - | Cle -> (Iop (OEfled, [ f1; f2 ], dest, succ), true) - | Cgt -> (Iop (OEfltd, [ f2; f1 ], dest, succ), true) - | Cge -> (Iop (OEfled, [ f2; f1 ], dest, succ), true) + | Ceq -> Iop (OEfeqd, [ f1; f2 ], dest, succ) + | Cne -> Iop (OEfeqd, [ f1; f2 ], dest, succ) + | Clt -> Iop (OEfltd, [ f1; f2 ], dest, succ) + | Cle -> Iop (OEfled, [ f1; f2 ], dest, succ) + | Cgt -> Iop (OEfltd, [ f2; f1 ], dest, succ) + | Cge -> Iop (OEfled, [ f2; f1 ], dest, succ) let cond_single cmp f1 f2 dest succ = match cmp with - | Ceq -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), true) - | Cne -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), false) - | Clt -> (Iop (OEflts, [ f1; f2 ], dest, succ), true) - | Cle -> (Iop (OEfles, [ f1; f2 ], dest, succ), true) - | Cgt -> (Iop (OEflts, [ f2; f1 ], dest, succ), true) - | Cge -> (Iop (OEfles, [ f2; f1 ], dest, succ), true) + | Ceq -> Iop (OEfeqs, [ f1; f2 ], dest, succ) + | Cne -> Iop (OEfeqs, [ f1; f2 ], dest, succ) + | Clt -> Iop (OEflts, [ f1; f2 ], dest, succ) + | Cle -> Iop (OEfles, [ f1; f2 ], dest, succ) + | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ) + | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ) + +let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k + else ( + reg := !reg + 1; + loadimm32 (r2p ()) n (n2pi ()) + (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k)) + +let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k = + if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k + else ( + reg := !reg + 1; + loadimm32 (r2p ()) n (n2pi ()) + (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k)) + +let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k = + if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k + else ( + reg := !reg + 1; + loadimm64 (r2p ()) n (n2pi ()) + (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k)) + +let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k = + if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k + else ( + reg := !reg + 1; + loadimm64 (r2p ()) n (n2pi ()) + (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_condimm_int32s cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int32s_x0 cmp a1 dest succ k + if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> - xorimm32 a1 dest n (n2pi ()) (cond_int32s_x0 cmp dest dest succ k) + xorimm32 a1 dest n (n2pi ()) + (cond_int32s true cmp dest dest dest succ k) | Clt -> sltimm32 a1 dest n succ k | Cle -> if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k @@ -253,26 +270,26 @@ let expanse_condimm_int32s cmp a1 n dest succ k = | _ -> reg := !reg + 1; loadimm32 (r2p ()) n (n2pi ()) - (cond_int32s_reg cmp a1 (r2p ()) dest succ k) + (cond_int32s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int32u cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k + if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k else match cmp with | Clt -> sltuimm32 a1 dest n succ k | _ -> reg := !reg + 1; loadimm32 (r2p ()) n (n2pi ()) - (cond_int32u_reg cmp a1 (r2p ()) dest succ k) + (cond_int32u false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64s cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k + if Int.eq n Int.zero then cond_int64s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> reg := !reg + 1; xorimm64 a1 (r2p ()) n (n2pi ()) - (cond_int64s_x0 cmp (r2p ()) dest succ k) + (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k) | Clt -> sltimm64 a1 dest n succ k | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then @@ -281,47 +298,36 @@ let expanse_condimm_int64s cmp a1 n dest succ k = | _ -> reg := !reg + 1; loadimm64 (r2p ()) n (n2pi ()) - (cond_int64s_reg cmp a1 (r2p ()) dest succ k) + (cond_int64s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64u cmp a1 n dest succ k = - if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k + if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k else match cmp with | Clt -> sltuimm64 a1 dest n succ k | _ -> reg := !reg + 1; loadimm64 (r2p ()) n (n2pi ()) - (cond_int64u_reg cmp a1 (r2p ()) dest succ k) - -let expanse_cond_float cmp f1 f2 dest succ k = - let insn, normal = cond_float cmp f1 f2 dest succ in - insn - :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) + (cond_int64u false cmp a1 (r2p ()) dest succ k) -let expanse_cond_not_float cmp f1 f2 dest succ k = - let insn, normal = cond_float cmp f1 f2 dest succ in +let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let succ' = if normal' then succ else n2pi () in + let insn = fn_cond cmp f1 f2 dest succ' in insn - :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k) + :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) -let expanse_cond_single cmp f1 f2 dest succ k = - let insn, normal = cond_single cmp f1 f2 dest succ in +let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = + reg := !reg + 1; + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let insn = fn_cond cmp f1 f2 (r2p ()) (n2pi ()) in insn - :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) - -let expanse_cond_not_single cmp f1 f2 dest succ k = - let insn, normal = cond_single cmp f1 f2 dest succ in - insn - :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k) - -let rec write_tree exp n code' = - match exp with - | (Iop (_, _, _, succ) as inst) :: k -> - (*print_instruction stderr (0,inst);*) - (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*) - code' := PTree.set n inst !code'; - (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*) - write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code' - | _ -> !code' + :: (if normal' then + Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) + :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -339,94 +345,158 @@ let get_regs_inst = function | Ireturn (Some r) -> [ r ] | _ -> [] -let generate_head_order n start_node new_order = - Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) - (Camlcoq.P.to_int start_node) - !node; - for i = !node downto Camlcoq.P.to_int start_node do - new_order := !new_order @ [ Camlcoq.P.of_int i ] - done; - new_order := n :: !new_order +let rec write_tree' exp current initial code' new_order = + if current = !node then ( + code' := PTree.set initial (Inop (n2p ())) !code'; + new_order := initial :: !new_order); + match exp with + | (Iop (_, _, _, succ) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree' k (current - 1) initial code' new_order + | (Icond (_, _, succ1, succ2, _) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree' k (current - 1) initial code' new_order + | [] -> () + | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code = - debug_flag := true; let new_order = ref [] in + let liveins = ref sb.liveins in let exp = ref [] in + let was_branch = ref false in let was_exp = ref false in let code' = ref code in Array.iter (fun n -> + was_branch := false; was_exp := false; let inst = get_some @@ PTree.get n code in - let start_node = Camlcoq.P.of_int (!node + 1) in (match inst with | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccomp\n"; - exp := cond_int32s_reg c a1 a2 dest succ []; + debug "Iop/Ccomp\n"; + exp := cond_int32s false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccompu\n"; - exp := cond_int32u_reg c a1 a2 dest succ []; + debug "Iop/Ccompu\n"; + exp := cond_int32u false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompimm\n"; + debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompuimm\n"; + debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccompl\n"; - exp := cond_int64s_reg c a1 a2 dest succ []; + debug "Iop/Ccompl\n"; + exp := cond_int64s false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccomplu\n"; - exp := cond_int64u_reg c a1 a2 dest succ []; + debug "Iop/Ccomplu\n"; + exp := cond_int64u false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - (*Printf.eprintf "Ccomplimm\n";*) - (*Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;*) - (*Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;*) - (*Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);*) - (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*) - (*debug "[EXPANSION] Replace this:\n";*) - (*print_instruction stderr (0,inst);*) - (*debug "[EXPANSION] With:\n";*) - (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*) - (*entry := n2p()*) + debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompluimm\n"; + debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Ccompf\n"; - exp := expanse_cond_float c f1 f2 dest succ []; + debug "Iop/Ccompf\n"; + exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Cnotcompf\n"; - exp := expanse_cond_not_float c f1 f2 dest succ []; + debug "Iop/Cnotcompf\n"; + exp := expanse_cond_fp true cond_float c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Ccompfs\n"; - exp := expanse_cond_single c f1 f2 dest succ []; + debug "Iop/Ccompfs\n"; + exp := expanse_cond_fp false cond_single c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Cnotcompfs\n"; - exp := expanse_cond_not_single c f1 f2 dest succ []; + debug "Iop/Cnotcompfs\n"; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + was_exp := true + | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompuimm\n"; + exp := expanse_cbranchimm_int32u c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompl\n"; + exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomplu\n"; + exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomplimm\n"; + exp := expanse_cbranchimm_int64s c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompluimm\n"; + exp := expanse_cbranchimm_int64u c a1 imm info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompf\n"; + exp := expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Cnotcompf\n"; + exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompfs\n"; + exp := + expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> + debug "Icond/Cnotcompfs\n"; + exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; + was_branch := true; was_exp := true - | _ -> new_order := !new_order @ [ n ]); + | _ -> new_order := n :: !new_order); if !was_exp then ( - code' := write_tree (List.rev !exp) start_node code'; - let first = Inop (n2pi ()) in - code' := PTree.set n first !code'; - generate_head_order n start_node new_order)) + node := !node + 1; + (if !was_branch then + let lives = PTree.get n !liveins in + match lives with + | Some lives -> + liveins := PTree.set (n2p ()) lives !liveins; + liveins := PTree.remove n !liveins + | _ -> ()); + write_tree' !exp !node n code' new_order)) sb.instructions; - sb.instructions <- Array.of_list !new_order; - (*print_arrayp sb.instructions;*) - debug_flag := false; + sb.instructions <- Array.of_list (List.rev !new_order); + sb.liveins <- !liveins; !code' let rec find_last_node_reg = function diff --git a/riscV/Op.v b/riscV/Op.v index 1ca6f2e9..c99c3b43 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -49,7 +49,20 @@ Inductive condition : Type := | Ccompf (c: comparison) (**r 64-bit floating-point comparison *) | Cnotcompf (c: comparison) (**r negation of a floating-point comparison *) | Ccompfs (c: comparison) (**r 32-bit floating-point comparison *) - | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *) + | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *) + (* Expansed branches *) + | CEbeqw (optR0: option bool) (**r branch-if-equal *) + | CEbnew (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbltw (optR0: option bool) (**r branch-if-less signed *) + | CEbltuw (optR0: option bool) (**r branch-if-less unsigned *) + | CEbgew (optR0: option bool) (**r branch-if-greater-or-equal signed *) + | CEbgeuw (optR0: option bool) (**r branch-if-greater-or-equal unsigned *) + | CEbeql (optR0: option bool) (**r branch-if-equal *) + | CEbnel (optR0: option bool) (**r branch-if-not-equal signed *) + | CEbltl (optR0: option bool) (**r branch-if-less signed *) + | CEbltul (optR0: option bool) (**r branch-if-less unsigned *) + | CEbgel (optR0: option bool) (**r branch-if-greater-or-equal signed *) + | CEbgeul (optR0: option bool). (**r branch-if-greater-or-equal unsigned *) (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -153,6 +166,7 @@ Inductive operation : Type := | Osingleoflongu (**r [rd = float32_of_unsigned_int(r1)] *) (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + (* Expansed conditions *) | OEseqw (optR0: option bool) (**r [rd <- rs1 == rs2] (pseudo) *) | OEsnew (optR0: option bool) (**r [rd <- rs1 != rs2] (pseudo) *) | OEsltw (optR0: option bool) (**r set-less-than *) @@ -191,9 +205,10 @@ Inductive addressing: Type := Definition eq_condition (x y: condition) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec Int64.eq_dec; intro. + generalize Int.eq_dec Int64.eq_dec bool_dec; intros. assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. decide equality. + all: destruct optR0, optR1; decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. @@ -254,6 +269,19 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) + (* Expansed branches *) + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 + | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 + | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 + | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 + | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 | _, _ => None end. @@ -354,6 +382,7 @@ Definition eval_operation | Osingleoflong, v1::nil => Some (Val.maketotal (Val.singleoflong v1)) | Osingleoflongu, v1::nil => Some (Val.maketotal (Val.singleoflongu v1)) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) + (* Expansed conditions *) | OEseqw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) | OEsnew optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) | OEsltw optR0, v1::v2::nil => Some (apply_bin_r0 optR0 (Val.cmp Clt) v1 v2 zero32) @@ -438,6 +467,18 @@ Definition type_of_condition (c: condition) : list typ := | Cnotcompf _ => Tfloat :: Tfloat :: nil | Ccompfs _ => Tsingle :: Tsingle :: nil | Cnotcompfs _ => Tsingle :: Tsingle :: nil + | CEbeqw _ => Tint :: Tint :: nil + | CEbnew _ => Tint :: Tint :: nil + | CEbltw _ => Tint :: Tint :: nil + | CEbltuw _ => Tint :: Tint :: nil + | CEbgew _ => Tint :: Tint :: nil + | CEbgeuw _ => Tint :: Tint :: nil + | CEbeql _ => Tlong :: Tlong :: nil + | CEbnel _ => Tlong :: Tlong :: nil + | CEbltl _ => Tlong :: Tlong :: nil + | CEbltul _ => Tlong :: Tlong :: nil + | CEbgel _ => Tlong :: Tlong :: nil + | CEbgeul _ => Tlong :: Tlong :: nil end. Definition type_of_operation (op: operation) : list typ * typ := @@ -766,48 +807,72 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... - -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmp; - destruct Val.cmp_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpu; - destruct Val.cmpu_bool... all: destruct b... -- unfold Val.cmp; destruct Val.cmp_bool... - all: destruct b... -- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... -- destruct v0... -- trivial. -- trivial. -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmpl; - destruct Val.cmpl_bool... all: destruct b... -- destruct optR0 as [[]|]; simpl; unfold Val.cmplu; - destruct Val.cmplu_bool... all: destruct b... -- unfold Val.cmpl; destruct Val.cmpl_bool... - all: destruct b... -- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... -- destruct v0... -- trivial. -- trivial. -- trivial. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. -- destruct v0; destruct v1; cbn; auto. - destruct Float32.cmp; cbn; auto. + (* OEseqw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsnew *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmp; + destruct Val.cmp_bool... all: destruct b... + (* OEsltuw *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpu; + destruct Val.cmpu_bool... all: destruct b... + (* OEsltiw *) + - unfold Val.cmp; destruct Val.cmp_bool... + all: destruct b... + (* OEsltiuw *) + - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... + (* OExoriw *) + - destruct v0... + (* OEluiw *) + - trivial. + (* OEaddiwr0 *) + - trivial. + (* OEseql *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsnel *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltl *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; + destruct Val.cmpl_bool... all: destruct b... + (* OEsltul *) + - destruct optR0 as [[]|]; simpl; unfold Val.cmplu; + destruct Val.cmplu_bool... all: destruct b... + (* OEsltil *) + - unfold Val.cmpl; destruct Val.cmpl_bool... + all: destruct b... + (* OEsltiul *) + - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... + (* OExoril *) + - destruct v0... + (* OEluil *) + - trivial. + (* OEaddilr0 *) + - trivial. + (* OEloadli *) + - trivial. + (* OEfeqd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfltd *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfled *) + - destruct v0; destruct v1; cbn; auto. + destruct Float.cmp; cbn; auto. + (* OEfeqs *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEflts *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. + (* OEfles *) + - destruct v0; destruct v1; cbn; auto. + destruct Float32.cmp; cbn; auto. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -877,6 +942,18 @@ Definition negate_condition (cond: condition): condition := | Cnotcompf c => Ccompf c | Ccompfs c => Cnotcompfs c | Cnotcompfs c => Ccompfs c + | CEbeqw optR0 => CEbnew optR0 + | CEbnew optR0 => CEbeqw optR0 + | CEbltw optR0 => CEbgew optR0 + | CEbltuw optR0 => CEbgeuw optR0 + | CEbgew optR0 => CEbltw optR0 + | CEbgeuw optR0 => CEbltuw optR0 + | CEbeql optR0 => CEbnel optR0 + | CEbnel optR0 => CEbeql optR0 + | CEbltl optR0 => CEbgel optR0 + | CEbltul optR0 => CEbgeul optR0 + | CEbgel optR0 => CEbltl optR0 + | CEbgeul optR0 => CEbltul optR0 end. Lemma eval_negate_condition: @@ -896,6 +973,31 @@ Proof. repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto. repeat (destruct vl; auto). repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto. + + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmp_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpu_bool. + repeat (destruct vl; auto); replace (Cne) with (negate_comparison Ceq) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Ceq) with (negate_comparison Cne) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Cge) with (negate_comparison Clt) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmpl_bool. + repeat (destruct vl; auto); replace (Clt) with (negate_comparison Cge) by auto; destruct optR0 as [[]|]; + apply Val.negate_cmplu_bool. Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) @@ -992,6 +1094,14 @@ Definition cond_depends_on_memory (cond : condition) : bool := | Ccompuimm _ _ => negb Archi.ptr64 | Ccomplu _ => Archi.ptr64 | Ccompluimm _ _ => Archi.ptr64 + | CEbeqw _ => negb Archi.ptr64 + | CEbnew _ => negb Archi.ptr64 + | CEbltuw _ => negb Archi.ptr64 + | CEbgeuw _ => negb Archi.ptr64 + | CEbeql _ => Archi.ptr64 + | CEbnel _ => Archi.ptr64 + | CEbltul _ => Archi.ptr64 + | CEbgeul _ => Archi.ptr64 | _ => false end. @@ -1043,7 +1153,9 @@ Lemma cond_valid_pointer_eq: Proof. intros until m2. intro MEM. destruct cond eqn:COND; simpl; try congruence. all: repeat (destruct args; simpl; try congruence); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + try destruct optR0 as [[]|]; simpl; + try destruct v, v0; try rewrite !MEM; auto; + try erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. Lemma op_valid_pointer_eq: @@ -1052,8 +1164,7 @@ Lemma op_valid_pointer_eq: eval_operation ge sp op args m1 = eval_operation ge sp op args m2. Proof. intros until m2. destruct op; simpl; try congruence. - intros MEM; destruct cond; repeat (destruct args; simpl; try congruence); - erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. + intro MEM; erewrite cond_valid_pointer_eq; eauto. all: intros MEM; repeat (destruct args; simpl; try congruence); try destruct optR0 as [[]|]; simpl; try destruct v, v0; try rewrite !MEM; auto; unfold Val.cmpu, Val.cmplu; @@ -1164,27 +1275,6 @@ Ltac InvInject := | _ => idtac end. -Lemma eval_condition_inj: - forall cond vl1 vl2 b, - Val.inject_list f vl1 vl2 -> - eval_condition cond vl1 m1 = Some b -> - eval_condition cond vl2 m2 = Some b. -Proof. - intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; simpl in H0; inv H0; auto. -- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -- inv H3; inv H2; simpl in H0; inv H0; auto. -Qed. - Lemma eval_cmpu_bool_inj': forall b c v v' v0 v0', Val.inject f v v' -> Val.inject f v0 v0' -> @@ -1267,6 +1357,54 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. +Lemma eval_condition_inj: + forall cond vl1 vl2 b, + Val.inject_list f vl1 vl2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto. + all: assert (HVI32: Val.inject f (Vint Int.zero) (Vint Int.zero)) by apply Val.inject_int; + assert (HVI64: Val.inject f (Vlong Int64.zero) (Vlong Int64.zero)) by apply Val.inject_long; + try unfold zero32, zero64. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; simpl in H0; inv H0; auto. +- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmpu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +- destruct optR0 as [[]|]; simpl; + inv H3; inv H2; simpl in H0; inv H0; auto. +- destruct optR0 as [[]|]; unfold apply_bin_r0 in *; + eapply eval_cmplu_bool_inj'; eauto. +Qed. + Ltac TrivialExists := match goal with | [ |- exists v2, Some ?v1 = Some v2 /\ Val.inject _ _ v2 ] => @@ -1473,35 +1611,54 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. - + (* OEseqw *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsnew *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltw *) - destruct optR0 as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.lt _ _); simpl; cbn; auto; try apply Val.inject_int. + (* OEsltuw *) - apply eval_cmpu_bool_inj_opt; auto. + (* OEsltiw *) - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. + (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. + (* OExoriw *) - inv H4; simpl; auto. + (* OEseql *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsnel *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltl *) - destruct optR0 as [[]|]; simpl; unfold zero64, Val.cmpl; inv H4; inv H2; simpl; try destruct (Int64.lt _ _); simpl; cbn; auto; try apply Val.inject_int. + (* OEsltul *) - apply eval_cmplu_bool_inj_opt; auto. + (* OEsltil *) - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. + (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. + (* OExoril *) - inv H4; simpl; auto. + (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfltd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfled *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfeqs *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEflts *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + (* OEfles *) - inv H4; inv H2; cbn; simpl; auto. destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. Qed. diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 75a913c6..09760db9 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -56,7 +56,19 @@ module Rocket = | Ccompl _ | Ccomplu _ | Ccomplimm _ - | Ccompluimm _ -> 1 + | Ccompluimm _ + | CEbeqw _ + | CEbnew _ + | CEbltw _ + | CEbltuw _ + | CEbgew _ + | CEbgeuw _ + | CEbeql _ + | CEbnel _ + | CEbltl _ + | CEbltul _ + | CEbgel _ + | CEbgeul _ -> 1 | Ccompf _ | Cnotcompf _ -> 6 | Ccompfs _ diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index c222f777..2b5ae1f5 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -60,6 +60,30 @@ let print_condition reg pp = function fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 | (Cnotcompfs c, [r1;r2]) -> fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + | (CEbeqw optR0, [r1;r2]) -> + fprintf pp "CEbeqw"; (get_optR0_s Ceq reg pp r1 r2 optR0) + | (CEbnew optR0, [r1;r2]) -> + fprintf pp "CEbnew"; (get_optR0_s Cne reg pp r1 r2 optR0) + | (CEbltw optR0, [r1;r2]) -> + fprintf pp "CEbltw"; (get_optR0_s Clt reg pp r1 r2 optR0) + | (CEbltuw optR0, [r1;r2]) -> + fprintf pp "CEbltuw"; (get_optR0_s Clt reg pp r1 r2 optR0) + | (CEbgew optR0, [r1;r2]) -> + fprintf pp "CEbgew"; (get_optR0_s Cge reg pp r1 r2 optR0) + | (CEbgeuw optR0, [r1;r2]) -> + fprintf pp "CEbgeuw"; (get_optR0_s Cge reg pp r1 r2 optR0) + | (CEbeql optR0, [r1;r2]) -> + fprintf pp "CEbeql"; (get_optR0_s Ceq reg pp r1 r2 optR0) + | (CEbnel optR0, [r1;r2]) -> + fprintf pp "CEbnel"; (get_optR0_s Cne reg pp r1 r2 optR0) + | (CEbltl optR0, [r1;r2]) -> + fprintf pp "CEbltl"; (get_optR0_s Clt reg pp r1 r2 optR0) + | (CEbltul optR0, [r1;r2]) -> + fprintf pp "CEbltul"; (get_optR0_s Clt reg pp r1 r2 optR0) + | (CEbgel optR0, [r1;r2]) -> + fprintf pp "CEbgel"; (get_optR0_s Cge reg pp r1 r2 optR0) + | (CEbgeul optR0, [r1;r2]) -> + fprintf pp "CEbgeul"; (get_optR0_s Cge reg pp r1 r2 optR0) | _ -> fprintf pp "" @@ -180,6 +204,12 @@ let print_operation reg pp = function | OEluil n, [] -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n) | OEloadli n, [] -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) + | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 + | OEfltd, [r1;r2] -> fprintf pp "OEfltd(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 + | OEfled, [r1;r2] -> fprintf pp "OEfled(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 + | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 + | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 + | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 | _ -> fprintf pp "" let print_addressing reg pp = function diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 4880a929..ece28eff 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -41,6 +41,18 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) + | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 + | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 + | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -194,7 +206,9 @@ Proof. destruct cond; simpl; eauto with va. inv H2. destruct cond; simpl; eauto with va. - destruct cond; auto with va. + 13: destruct cond; simpl; eauto with va. + all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. Lemma symbol_address_sound: diff --git a/scheduling/RTLpathCommon.ml b/scheduling/RTLpathCommon.ml index 748a02f1..3d123ba8 100644 --- a/scheduling/RTLpathCommon.ml +++ b/scheduling/RTLpathCommon.ml @@ -6,7 +6,7 @@ type superblock = { mutable instructions: P.t array; (* pointers to code instructions *) (* each predicted Pcb has its attached liveins *) (* This is indexed by the pc value *) - liveins: Regset.t PTree.t; + mutable liveins: Regset.t PTree.t; (* Union of the input_regs of the last successors *) s_output_regs: Regset.t; typing: RTLtyping.regenv diff --git a/scheduling/RTLpathScheduleraux.ml b/scheduling/RTLpathScheduleraux.ml index 00ef31fb..cdee5a5b 100644 --- a/scheduling/RTLpathScheduleraux.ml +++ b/scheduling/RTLpathScheduleraux.ml @@ -283,7 +283,9 @@ let turn_all_loads_nontrap sb code = let rec do_schedule code = function | [] -> code | sb :: lsb -> + (*debug_flag := true;*) let code_exp = expanse sb code in + (*debug_flag := false;*) (* Trick: instead of turning loads into non trap as needed.. * First, we turn them all into non-trap. * Then, we turn back those who didn't need to be turned, into TRAP again @@ -293,12 +295,11 @@ let rec do_schedule code = function let schedule = schedule_superblock sb code' in let new_code = apply_schedule code' sb schedule in begin - (*debug_flag := true; *) + (*debug_flag := true;*) debug "Old Code: "; print_code code; debug "Exp Code: "; print_code code_exp; debug "\nSchedule to apply: "; print_arrayp schedule; debug "\nNew Code: "; print_code new_code; - (*debug_flag := false;*) debug "\n"; (* debug_flag := false; *) do_schedule new_code lsb -- cgit