diff options
-rw-r--r-- | riscV/Asmgen.v | 44 | ||||
-rw-r--r-- | riscV/Asmgenproof.v | 6 | ||||
-rw-r--r-- | riscV/Asmgenproof1.v | 12 | ||||
-rw-r--r-- | riscV/ExpansionOracle.ml | 500 | ||||
-rw-r--r-- | riscV/NeedOp.v | 6 | ||||
-rw-r--r-- | riscV/Op.v | 44 | ||||
-rw-r--r-- | riscV/ValueAOp.v | 7 |
7 files changed, 417 insertions, 202 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index f702d11a..b3fb2350 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -344,10 +344,10 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) end. -Definition transl_cond_op +(* TODO Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := match cond, args with - (* TODO | Ccomp c, a1 :: a2 :: nil => + | Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cond_int32s c rd r1 r2 k) | Ccompu c, a1 :: a2 :: nil => @@ -370,7 +370,7 @@ Definition transl_cond_op OK (transl_condimm_int64s c rd r1 n k) | Ccompluimm c n, a1 :: nil => do r1 <- ireg_of a1; - OK (transl_condimm_int64u c rd r1 n k)*) + OK (transl_condimm_int64u c rd r1 n k) | Ccompf c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_float c rd r1 r2 in @@ -386,10 +386,10 @@ Definition transl_cond_op | Cnotcompfs c, f1 :: f2 :: nil => do r1 <- freg_of f1; do r2 <- freg_of f2; let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) + 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]. *) @@ -712,9 +712,9 @@ Definition transl_op do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - | Ocmp cmp, _ => + (* TODO | 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; @@ -795,6 +795,36 @@ Definition transl_op | OEloadli n, nil => do rd <- ireg_of res; OK (Ploadli rd n :: k) + | OEfeqd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqd rd r1 r2 :: k) + | OEfltd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfltd rd r1 r2 :: k) + | OEfled, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfled rd r1 r2 :: k) + | OEfeqs, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqs rd r1 r2 :: k) + | OEflts, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pflts rd r1 r2 :: k) + | OEfles, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfles rd r1 r2 :: k) | _, _ => Error(msg "Asmgen.transl_op") end. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 63ceed0d..6bacaa5c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -214,7 +214,7 @@ Proof. destruct normal; TailNoLabel. Qed. -Remark transl_cond_op_label: +(* TODO 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. @@ -267,7 +267,7 @@ Proof. - destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. destruct normal; TailNoLabel. -Qed. + Qed.*) Remark transl_op_label: forall op args r k c, @@ -291,7 +291,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. -- eapply transl_cond_op_label; eauto. +(* TODO - 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 ee203da4..49635ebd 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -832,7 +832,7 @@ Proof. + apply DFL. Qed. -Lemma transl_cond_op_correct: +(* TODO Lemma transl_cond_op_correct: forall cond rd args k c rs m, transl_cond_op cond rd args k = OK c -> exists rs', @@ -844,7 +844,7 @@ Proof. { destruct ob as [[]|]; reflexivity. } intros until m; intros TR. destruct cond; simpl in TR; ArgsInv. -(* TODO + (* cmp *) ++ (* cmp *) exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpu *) exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). @@ -866,7 +866,7 @@ Proof. + (* cmpluimm *) exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto.*) + exists rs'; repeat split; eauto. rewrite MKTOT; eauto. + (* cmpf *) destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. fold (Val.cmpf c0 (rs x) (rs x0)). @@ -923,7 +923,7 @@ Proof. * econstructor; split. apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. split; intros; Simpl. -Qed. + Qed.*) (** Some arithmetic properties. *) @@ -1134,8 +1134,8 @@ Opaque Int.eq. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } (* cond *) - { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. } + (* TODO { 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; split; intros; Simpl; rewrite Int.add_commut; auto. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index c3f2cb3f..9e494d0a 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -18,40 +18,46 @@ open RTL open Op open Asmgen open DebugPrint + (*open PrintRTL*) open! Integers let reg = ref 1 + let node = ref 1 let r2p () = Camlcoq.P.of_int !reg + let n2p () = Camlcoq.P.of_int !node -let n2pi () = node := !node + 1; n2p() + +let n2pi () = + node := !node + 1; + n2p () type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul let load_hilo32 dest hi lo succ k = - if Int.eq lo Int.zero then - Iop (OEluiw hi, [], dest, succ) :: k - else ( - Iop (OEluiw hi, [], dest, n2pi()) :: (Iop (Oaddimm lo, [dest], dest, succ)) :: k) + if Int.eq lo Int.zero then Iop (OEluiw hi, [], dest, succ) :: k + else + Iop (OEluiw hi, [], dest, n2pi ()) + :: Iop (Oaddimm lo, [ dest ], dest, succ) + :: k let load_hilo64 dest hi lo succ k = - if Int64.eq lo Int64.zero then - Iop (OEluil hi, [], dest, succ) :: k - else ( - Iop (OEluil hi, [], dest, n2pi()) :: (Iop (Oaddlimm lo, [dest], dest, succ)) :: k) + if Int64.eq lo Int64.zero then Iop (OEluil hi, [], dest, succ) :: k + else + Iop (OEluil hi, [], dest, n2pi ()) + :: Iop (Oaddlimm lo, [ dest ], dest, succ) + :: k let loadimm32 dest n succ k = match make_immed32 n with - | Imm32_single imm -> - Iop (OEaddiwr0 imm, [], dest, succ) :: k + | Imm32_single imm -> Iop (OEaddiwr0 imm, [], dest, succ) :: k | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ k let loadimm64 dest n succ k = match make_immed64 n with - | Imm64_single imm -> - Iop (OEaddilr0 imm, [], dest, succ) :: k + | Imm64_single imm -> Iop (OEaddilr0 imm, [], dest, succ) :: k | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ k | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k @@ -65,236 +71,359 @@ let get_opimm imm = function let opimm32 a1 dest n succ k op opimm = match make_immed32 n with - | Imm32_single imm -> - Iop (get_opimm imm opimm, [a1], dest, succ) :: k + | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm32_pair (hi, lo) -> reg := !reg + 1; - load_hilo32 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k) + load_hilo32 (r2p ()) hi lo (n2pi ()) + (Iop (op, [ a1; r2p () ], dest, succ) :: k) let opimm64 a1 dest n succ k op opimm = match make_immed64 n with - | Imm64_single imm -> - Iop (get_opimm imm opimm, [a1], dest, succ) :: k + | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm64_pair (hi, lo) -> reg := !reg + 1; - load_hilo64 (r2p()) hi lo (n2pi()) (Iop (op, [a1;r2p()], dest, succ) :: k) - | Imm64_large imm -> + load_hilo64 (r2p ()) hi lo (n2pi ()) + (Iop (op, [ a1; r2p () ], dest, succ) :: k) + | Imm64_large imm -> reg := !reg + 1; - Iop (OEloadli imm, [], r2p(), n2pi()) :: Iop (op, [a1;r2p()], dest, succ) :: k + Iop (OEloadli imm, [], r2p (), n2pi ()) + :: Iop (op, [ a1; r2p () ], dest, succ) + :: k let xorimm32 a1 dest n succ k = opimm32 a1 dest n succ k Oxor Xoriw + let sltimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltw None) Sltiw + let sltuimm32 a1 dest n succ k = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw + let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril + 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 + | 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 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 + | 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 cond_int32u_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 (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 + | 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 = 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 + | 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 = 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 - | Cle -> Iop (OEsltl (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k - | Cgt -> Iop (OEsltl (Some true), [a1;a1], dest, succ) :: k - | Cge -> Iop (OEsltl (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | 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 + | Cle -> + Iop (OEsltl (Some true), [ a1; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k + | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k + | Cge -> + Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k let cond_int64s_reg cmp a1 a2 dest succ k = 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 - | Cle -> Iop (OEsltl None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k - | Cgt -> Iop (OEsltl None, [a2;a1], dest, succ) :: k - | Cge -> Iop (OEsltl None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | 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 + | Cle -> + Iop (OEsltl None, [ a2; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k + | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k + | Cge -> + Iop (OEsltl None, [ a1; a2 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k let cond_int64u_x0 cmp a1 dest succ k = 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 - | Cle -> Iop (OEsltul (Some true), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k - | Cgt -> Iop (OEsltul (Some true), [a1;a1], dest, succ) :: k - | Cge -> Iop (OEsltul (Some false), [a1;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | 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 + | Cle -> + Iop (OEsltul (Some true), [ a1; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k + | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k + | Cge -> + Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k let cond_int64u_reg cmp a1 a2 dest succ k = 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 - | Cle -> Iop (OEsltul None, [a2;a1], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k - | Cgt -> Iop (OEsltul None, [a2;a1], dest, succ) :: k - | Cge -> Iop (OEsltul None, [a1;a2], dest, n2pi()) :: Iop (OExoriw Int.one, [dest], dest, succ) :: k + | 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 + | Cle -> + Iop (OEsltul None, [ a2; a1 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: k + | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k + | Cge -> + Iop (OEsltul None, [ a1; a2 ], dest, n2pi ()) + :: Iop (OExoriw Int.one, [ dest ], dest, succ) + :: 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 else +let cond_float cmp f1 f2 dest succ = match cmp with - | Ceq | Cne -> - xorimm32 a1 dest n (n2pi()) (cond_int32s_x0 cmp 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 - else sltimm32 a1 dest (Int.add n Int.one) succ k - | _ -> reg := !reg + 1; - loadimm32 (r2p()) n (n2pi()) (cond_int32s_reg cmp a1 (r2p()) dest succ k) + | 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) -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 else +let cond_single cmp f1 f2 dest succ = 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) + | 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) + +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 + else + match cmp with + | Ceq | Cne -> + xorimm32 a1 dest n (n2pi ()) (cond_int32s_x0 cmp 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 + else sltimm32 a1 dest (Int.add n Int.one) succ k + | _ -> + reg := !reg + 1; + loadimm32 (r2p ()) n (n2pi ()) + (cond_int32s_reg 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 + 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) 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 else - match cmp with - | Ceq | Cne -> - reg := !reg + 1; - xorimm64 a1 (r2p()) n (n2pi()) (cond_int64s_x0 cmp (r2p()) dest succ k) - | Clt -> sltimm64 a1 dest n succ k - | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) - then loadimm32 dest Int.one succ k - else sltimm64 a1 dest (Int64.add n Int64.one) succ k - | _ -> reg := !reg + 1; - loadimm64 (r2p()) n (n2pi()) (cond_int64s_reg cmp a1 (r2p()) dest succ k) - + if Int.eq n Int.zero then cond_int64s_x0 cmp 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) + | Clt -> sltimm64 a1 dest n succ k + | Cle -> + if Int64.eq n (Int64.repr Int64.max_signed) then + loadimm32 dest Int.one succ k + else sltimm64 a1 dest (Int64.add n Int64.one) succ k + | _ -> + reg := !reg + 1; + loadimm64 (r2p ()) n (n2pi ()) + (cond_int64s_reg 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 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) + if Int64.eq n Int64.zero then cond_int64u_x0 cmp 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) + +let expanse_cond_not_float cmp f1 f2 dest succ k = + let insn, normal = cond_float cmp f1 f2 dest succ in + insn + :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k) + +let expanse_cond_single cmp f1 f2 dest succ k = + let insn, normal = cond_single cmp f1 f2 dest succ 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 -> + | (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' + write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code' | _ -> !code' -let get_regindent = function - | Coq_inr _ -> [] - | Coq_inl r -> [r] - +let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] + let get_regs_inst = function - | Inop (_) -> [] - | Iop (_,args,dest,_) -> dest :: args - | Iload (_,_,_,args,dest,_) -> dest :: args - | Istore (_,_,args,src,_) -> src :: args - | Icall (_,t,args,dest,_) -> dest :: ((get_regindent t) @ args) - | Itailcall (_,t,args) -> (get_regindent t) @ args - | Ibuiltin (_,args,dest,_) -> - (AST.params_of_builtin_res dest) @ - AST.params_of_builtin_args args - | Icond (_,args,_,_,_) -> args - | Ijumptable (arg,_) -> [arg] - | Ireturn (Some r) -> [r] + | Inop _ -> [] + | Iop (_, args, dest, _) -> dest :: args + | Iload (_, _, _, args, dest, _) -> dest :: args + | Istore (_, _, args, src, _) -> src :: args + | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args) + | Itailcall (_, t, args) -> get_regindent t @ args + | Ibuiltin (_, args, dest, _) -> + AST.params_of_builtin_res dest @ AST.params_of_builtin_args args + | Icond (_, args, _, _, _) -> args + | Ijumptable (arg, _) -> [ arg ] + | 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]; + 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 expanse (sb: superblock) code = +let expanse (sb : superblock) code = debug_flag := true; let new_order = ref [] in let exp = ref [] in let was_exp = ref false in let code' = ref code in - Array.iter (fun n -> - 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 []; - 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 []; - was_exp := true) - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> ( - Printf.eprintf "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"; - 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 []; - 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 []; - 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()*) - 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"; - exp := expanse_condimm_int64u c a1 imm dest succ []; - was_exp := true) - | _ -> new_order := !new_order @ [n]); - 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) - ) sb.instructions; + Array.iter + (fun n -> + 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 []; + 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 []; + was_exp := true + | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> + Printf.eprintf "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"; + 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 []; + 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 []; + 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()*) + 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"; + 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 []; + 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 []; + 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 []; + 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 []; + was_exp := true + | _ -> new_order := !new_order @ [ n ]); + 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)) + sb.instructions; sb.instructions <- Array.of_list !new_order; (*print_arrayp sb.instructions;*) debug_flag := false; @@ -303,12 +432,13 @@ let expanse (sb: superblock) code = let rec find_last_node_reg = function | [] -> () | (pc, i) :: k -> - let rec traverse_list var = function - | [] -> () - | e :: t -> - (let e' = Camlcoq.P.to_int e in - if e' > !var then var := e'; - traverse_list var t) in - traverse_list node [pc]; - traverse_list reg (get_regs_inst i); - find_last_node_reg k + let rec traverse_list var = function + | [] -> () + | e :: t -> + let e' = Camlcoq.P.to_int e in + if e' > !var then var := e'; + traverse_list var t + in + traverse_list node [ pc ]; + traverse_list reg (get_regs_inst i); + find_last_node_reg k diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 67940c47..db8b68ef 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -106,6 +106,12 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEluil n => op1 (default nv) | OEaddilr0 n => op1 (modarith nv) | OEloadli n => op1 (default nv) + | OEfeqd => op2 (default nv) + | OEfltd => op2 (default nv) + | OEfled => op2 (default nv) + | OEfeqs => op2 (default nv) + | OEflts => op2 (default nv) + | OEfles => op2 (default nv) end. Definition operation_is_redundant (op: operation) (nv: nval): bool := @@ -171,7 +171,13 @@ Inductive operation : Type := | OExoril (n: int64) (**r xor immediate *) | OEluil (n: int64) (**r load upper-immediate *) | OEaddilr0 (n: int64) (**r add immediate *) - | OEloadli (n: int64). (**r load an immediate int64 *) + | OEloadli (n: int64) (**r load an immediate int64 *) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles. (**r compare less-than/equal *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -367,6 +373,12 @@ Definition eval_operation | 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) + | 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) + | OEfeqs, v1::v2::nil => Some (Val.cmpfs Ceq v1 v2) + | OEflts, v1::v2::nil => Some (Val.cmpfs Clt v1 v2) + | OEfles, v1::v2::nil => Some (Val.cmpfs Cle v1 v2) | _, _ => None end. @@ -542,6 +554,12 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEluil _ => (nil, Tlong) | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) + | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) + | OEfltd => (Tfloat :: Tfloat :: nil, Tint) + | OEfled => (Tfloat :: Tfloat :: nil, Tint) + | OEfeqs => (Tsingle :: Tsingle :: nil, Tint) + | OEflts => (Tsingle :: Tsingle :: nil, Tint) + | OEfles => (Tsingle :: Tsingle :: nil, Tint) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -778,6 +796,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - 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. Qed. (* This should not be simplified to "false" because it breaks proofs elsewhere. *) @@ -1462,6 +1492,18 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. - apply eval_cmplu_bool_inj; auto. - inv H4; simpl; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. + - inv H4; inv H2; cbn; simpl; auto. + destruct Float32.cmp; unfold Vtrue, Vfalse; cbn; auto. Qed. Lemma eval_addressing_inj: diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index 9218d80d..4880a929 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -166,6 +166,12 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEluil n, nil => L (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))) | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (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) + | OEfeqs, v1::v2::nil => of_optbool (cmpfs_bool Ceq v1 v2) + | OEflts, v1::v2::nil => of_optbool (cmpfs_bool Clt v1 v2) + | OEfles, v1::v2::nil => of_optbool (cmpfs_bool Cle v1 v2) | _, _ => Vbot end. @@ -317,6 +323,7 @@ Proof. 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. + all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. End SOUNDNESS. |