From 95205e72ca536907fa89c7c884f0e22fc605063d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 26 Mar 2021 12:49:02 +0100 Subject: Adding more expansions, improving miniCSE, and tuning prepass --- riscV/Asmgen.v | 24 ++ riscV/Asmgenproof1.v | 12 +- riscV/ExpansionOracle.ml | 587 +++++++++++++++++++++++++----------- riscV/NeedOp.v | 22 +- riscV/Op.v | 120 +++++++- riscV/OpWeights.ml | 334 ++++++++++----------- riscV/PrintOp.ml | 10 +- riscV/RTLpathSE_simplify.v | 732 ++++++++++++++++++++++++++++++++++++++++++++- riscV/ValueAOp.v | 65 +++- 9 files changed, 1518 insertions(+), 388 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 8b86ec5a..d4c6b73a 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -815,9 +815,21 @@ Definition transl_op | OEluiw n, nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) + | OEaddiw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Paddiw rd rs n :: k) | OEaddiwr0 n, nil => do rd <- ireg_of res; OK (Paddiw rd X0 n :: k) + | OEandiw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pandiw rd rs n :: k) + | OEoriw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Poriw rd rs n :: k) | OEseql optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -863,9 +875,21 @@ Definition transl_op | OEluil n, nil => do rd <- ireg_of res; OK (Pluil rd n :: k) + | OEaddil n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Paddil rd rs n :: k) | OEaddilr0 n, nil => do rd <- ireg_of res; OK (Paddil rd X0 n :: k) + | OEandil n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pandil rd rs n :: k) + | OEoril n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Poril rd rs n :: k) | OEloadli n, nil => do rd <- ireg_of res; OK (Ploadli rd n :: k) diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 0be56e47..639c9a64 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -1258,11 +1258,15 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - 7,14: + 7,8,9,10,17,18,19,20: econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl; simpl; - try rewrite Int.add_commut; try rewrite Int64.add_commut; - auto. + split; intros; Simpl; try destruct (rs x0); + try rewrite Int64.add_commut; + try rewrite Int.add_commut; auto; + try rewrite Int64.and_commut; + try rewrite Int.and_commut; auto; + try rewrite Int64.or_commut; + try rewrite Int.or_commut; auto. 1-12: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; econstructor; split; try apply exec_straight_one; simpl; eauto; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 27a36283..676b8da6 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -45,12 +45,26 @@ let n2pi () = node := !node + 1; n2p () -type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul - -let find_or_addnmove op args rd succ map_consts = +type immt = + | Addiw + | Addil + | Andiw + | Andil + | Oriw + | Oril + | Xoriw + | Xoril + | Sltiw + | Sltiuw + | Sltil + | Sltiul + +let find_or_addnmove op args rd succ map_consts node_dec = let sop = Sop (op, args) in match Hashtbl.find_opt map_consts sop with - | Some r -> Sr (P.of_int r) + | Some r -> + if node_dec then node := !node - 1; + Sr (P.of_int r) | None -> Hashtbl.add map_consts sop (p2i rd); Si (Iop (op, args, rd, succ)) @@ -58,93 +72,114 @@ let find_or_addnmove op args rd succ map_consts = let build_head_tuple head sv = match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r) -let load_hilo32 dest hi lo succ map_consts = +let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r + +let unzip_head_tuple_move ht r succ = + match ht with l, Some r' -> [ Iop (Omove, [ r' ], r, succ) ] | l, None -> l + +let build_full_ilist op args dest succ hd k map_consts = + let sv = find_or_addnmove op args dest succ map_consts false in + let ht = build_head_tuple hd sv in + unzip_head_tuple_move ht dest succ @ k + +let load_hilo32 dest hi lo succ map_consts node_dec = let op1 = OEluiw hi in if Int.eq lo Int.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv else let r = r2pi () in - let op2 = Oaddimm lo in - match find_or_addnmove op1 [] r (n2pi ()) map_consts with - | Si i -> - let sv = find_or_addnmove op2 [ r ] dest succ map_consts in - build_head_tuple [ i ] sv - | Sr r' -> - let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in - build_head_tuple [] sv - -let load_hilo64 dest hi lo succ map_consts = + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let ht1 = build_head_tuple [] sv1 in + let r' = unzip_head_tuple ht1 r in + let op2 = OEaddiw lo in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + build_head_tuple (fst ht1) sv2 + +let load_hilo64 dest hi lo succ map_consts node_dec = let op1 = OEluil hi in if Int64.eq lo Int64.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv else let r = r2pi () in - let op2 = Oaddlimm lo in - match find_or_addnmove op1 [] r (n2pi ()) map_consts with - | Si i -> - let sv = find_or_addnmove op2 [ r ] dest succ map_consts in - build_head_tuple [ i ] sv - | Sr r' -> - let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in - build_head_tuple [] sv - -let loadimm32 dest n succ map_consts = + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let ht1 = build_head_tuple [] sv1 in + let r' = unzip_head_tuple ht1 r in + let op2 = OEaddil lo in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + build_head_tuple (fst ht1) sv2 + +let loadimm32 dest n succ map_consts node_dec = match make_immed32 n with | Imm32_single imm -> let op1 = OEaddiwr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv - | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts + | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts node_dec -let loadimm64 dest n succ map_consts = +let loadimm64 dest n succ map_consts node_dec = match make_immed64 n with | Imm64_single imm -> let op1 = OEaddilr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv - | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts + | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts node_dec | Imm64_large imm -> let op1 = OEloadli imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv let get_opimm imm = function + | Addiw -> OEaddiw imm + | Andiw -> OEandiw imm + | Oriw -> OEoriw imm | Xoriw -> OExoriw imm | Sltiw -> OEsltiw imm | Sltiuw -> OEsltiuw imm + | Addil -> OEaddil imm + | Andil -> OEandil imm + | Oril -> OEoril imm | Xoril -> OExoril imm | Sltil -> OEsltil imm | Sltiul -> OEsltiul imm -let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r - let opimm32 a1 dest n succ k op opimm map_consts = match make_immed32 n with - | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm32_single imm -> + build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts | Imm32_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo32 r hi lo (n2pi ()) map_consts in + let ht = load_hilo32 r hi lo (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts let opimm64 a1 dest n succ k op opimm map_consts = match make_immed64 n with - | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm64_single imm -> + build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts | Imm64_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo64 r hi lo (n2pi ()) map_consts in + let ht = load_hilo64 r hi lo (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k - | Imm64_large imm -> + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts + | Imm64_large imm ->( let r = r2pi () in let op1 = OEloadli imm in let inode = n2pi () in - let sv = find_or_addnmove op1 [] r inode map_consts in + let sv = find_or_addnmove op1 [] r inode map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts) + +let addimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oadd Addiw map_consts + +let andimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oand Andiw map_consts + +let orimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oor Oriw map_consts let xorimm32 a1 dest n succ k map_consts = opimm32 a1 dest n succ k Oxor Xoriw map_consts @@ -155,6 +190,12 @@ let sltimm32 a1 dest n succ k map_consts = let sltuimm32 a1 dest n succ k map_consts = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts +let addimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oaddl Addil + +let andimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oandl Andil + +let orimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oorl Oril + 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 @@ -205,95 +246,119 @@ let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 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 tmp_reg succ k = +let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | 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 + | Ceq -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltw optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltw optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltw optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltw optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltw optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltuw optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltuw optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltuw optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltuw optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | 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 + | Ceq -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltl optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltl optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltl optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltl optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltl optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltul optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltul optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltul optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltul optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltul optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] let is_normal_cmp = function Cne -> false | _ -> true -let cond_float cmp f1 f2 dest succ = +let cond_float cmp f1 f2 dest succ map_consts = match cmp with - | 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 = + | 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 map_consts = match cmp with - | 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) + | 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 map_consts = if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k @@ -301,7 +366,7 @@ let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts = if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k @@ -309,7 +374,7 @@ let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k @@ -317,102 +382,103 @@ let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None -let expanse_condimm_int32s cmp a1 n dest succ k map_consts = +let expanse_condimm_int32s cmp a1 n dest succ map_consts = if Int.eq n Int.zero then let tmp_reg = get_tmp_reg cmp in - cond_int32s true cmp a1 a1 dest tmp_reg succ k + cond_int32s true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with | Ceq | Cne -> let r = r2pi () in xorimm32 a1 r n (n2pi ()) - (cond_int32s true cmp r r dest None succ k) + (cond_int32s true cmp r r dest None succ map_consts) map_consts - | Clt -> sltimm32 a1 dest n succ k map_consts + | Clt -> sltimm32 a1 dest n succ [] map_consts | Cle -> if Int.eq n (Int.repr Int.max_signed) then - let ht = loadimm32 dest Int.one succ map_consts in - fst ht @ k - else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts + let ht = loadimm32 dest Int.one succ map_consts false in + fst ht + else sltimm32 a1 dest (Int.add n Int.one) succ [] map_consts | _ -> let r = r2pi () in let tmp_reg = get_tmp_reg cmp in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int32u cmp a1 n dest succ k map_consts = +let expanse_condimm_int32u cmp a1 n dest succ map_consts = let tmp_reg = get_tmp_reg cmp in - if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest tmp_reg succ k + if Int.eq n Int.zero then + cond_int32u true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with - | Clt -> sltuimm32 a1 dest n succ k map_consts + | Clt -> sltuimm32 a1 dest n succ [] map_consts | _ -> let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int64s cmp a1 n dest succ k map_consts = +let expanse_condimm_int64s cmp a1 n dest succ map_consts = if Int64.eq n Int64.zero then let tmp_reg = get_tmp_reg cmp in - cond_int64s true cmp a1 a1 dest tmp_reg succ k + cond_int64s true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with | Ceq | Cne -> let r = r2pi () in xorimm64 a1 r n (n2pi ()) - (cond_int64s true cmp r r dest None succ k) + (cond_int64s true cmp r r dest None succ map_consts) map_consts - | Clt -> sltimm64 a1 dest n succ k map_consts + | Clt -> sltimm64 a1 dest n succ [] map_consts | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then - let ht = loadimm32 dest Int.one succ map_consts in - fst ht @ k - else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts + let ht = loadimm32 dest Int.one succ map_consts false in + fst ht + else sltimm64 a1 dest (Int64.add n Int64.one) succ [] map_consts | _ -> let r = r2pi () in let tmp_reg = get_tmp_reg cmp in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int64u cmp a1 n dest succ k map_consts = +let expanse_condimm_int64u cmp a1 n dest succ map_consts = let tmp_reg = get_tmp_reg cmp in - if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest tmp_reg succ k + if Int64.eq n Int64.zero then + cond_int64u true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with - | Clt -> sltuimm64 a1 dest n succ k map_consts + | Clt -> sltuimm64 a1 dest n succ [] map_consts | _ -> let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ map_consts -let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = +let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ map_consts = 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 k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) + let insn = fn_cond cmp f1 f2 dest succ' map_consts in + if normal' then insn + else build_full_ilist (OExoriw Int.one) [ dest ] dest succ insn [] map_consts -let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = +let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts = let r = r2pi () in let normal = is_normal_cmp cmp in let normal' = if cnot then not normal else normal in - let insn = fn_cond cmp f1 f2 r (n2pi ()) in + let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in insn :: - (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info)) - :: k + (if normal' then [ Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) ] + else [ Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info) ]) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -447,24 +513,19 @@ let write_pathmap initial esize pm' = in pm' := PTree.set initial path' !pm' -let rec write_tree exp initial current code' new_order = +let rec write_tree exp initial current code' new_order fturn = + (*Printf.eprintf "wt: node is %d\n" !node;*) let target_node, next_node = - if current = !node then ( - node := !node + 1; - (P.to_int initial, current)) - else (current, current - 1) + if fturn then (P.to_int initial, current) else (current, current - 1) in match exp with - | (Iop (_, _, _, succ) as inst) :: k -> + | inst :: k -> + (*let open PrintRTL in*) + (*print_instruction stderr (target_node, inst);*) code' := PTree.set (P.of_int target_node) inst !code'; new_order := P.of_int target_node :: !new_order; - write_tree k initial next_node code' new_order - | (Icond (_, _, succ1, succ2, _) as inst) :: k -> - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order; - write_tree k initial next_node code' new_order + write_tree k initial next_node code' new_order false | [] -> () - | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code pm = (*debug_flag := true;*) @@ -487,54 +548,54 @@ let expanse (sb : superblock) code pm = | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomp\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int32s false c a1 a2 dest tmp_reg succ []; + exp := cond_int32s false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompu\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int32u false c a1 a2 dest tmp_reg succ []; + exp := cond_int32u false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int32s c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int32u c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompl\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int64s false c a1 a2 dest tmp_reg succ []; + exp := cond_int64s false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomplu\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int64u false c a1 a2 dest tmp_reg succ []; + exp := cond_int64u false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int64s c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int64u c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompf\n"; - exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; + exp := expanse_cond_fp false cond_float c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Cnotcompf\n"; - exp := expanse_cond_fp true cond_float c f1 f2 dest succ []; + exp := expanse_cond_fp true cond_float c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompfs\n"; - exp := expanse_cond_fp false cond_single c f1 f2 dest succ []; + exp := expanse_cond_fp false cond_single c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ map_consts; was_exp := true (* Expansion of branches - Ccomp *) | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> @@ -584,24 +645,29 @@ let expanse (sb : superblock) code pm = | 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 []; + expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 + map_consts; 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 []; + exp := + expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 + map_consts; 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 []; + expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 + map_consts; 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 []; + expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 + map_consts; was_branch := true; was_exp := true | _ -> ()); @@ -611,22 +677,197 @@ let expanse (sb : superblock) code pm = | Iop (Ofloatconst f, nil, dest, succ) -> debug "Iop/Ofloatconst\n"; let r = r2pi () in + let ht = loadimm64 r (Floats.Float.to_bits f) (n2pi ()) map_consts true in + let r' = unzip_head_tuple ht r in exp := - [ - Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ()); - Iop (Ofloat_of_bits, [ r ], dest, succ); - ]; + build_full_ilist Ofloat_of_bits [ r' ] dest succ (fst ht) [] + map_consts; was_exp := true | Iop (Osingleconst f, nil, dest, succ) -> debug "Iop/Osingleconst\n"; let r = r2pi () in + let ht = + loadimm32 r (Floats.Float32.to_bits f) (n2pi ()) map_consts true + in + let r' = unzip_head_tuple ht r in exp := - [ - Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ()); - Iop (Osingle_of_bits, [ r ], dest, succ); - ]; + build_full_ilist Osingle_of_bits [ r' ] dest succ (fst ht) [] + map_consts; was_exp := true | _ -> ()); + + (* TODO gourdinl flag ? *) + (match inst with + | Iop (Ointconst n, nil, dest, succ) -> + debug "Iop/Ointconst\n"; + let ht = loadimm32 dest n succ map_consts false in + exp := unzip_head_tuple_move ht dest succ; + was_exp := true + | Iop (Olongconst n, nil, dest, succ) -> + debug "Iop/Olongconst\n"; + let ht = loadimm64 dest n succ map_consts false in + exp := unzip_head_tuple_move ht dest succ; + was_exp := true + | Iop (Oaddimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oaddimm\n"; + exp := addimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oaddlimm\n"; + exp := addimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oandimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oandimm\n"; + exp := andimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oandlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oandlimm\n"; + exp := andimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oorimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oorimm\n"; + exp := orimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oorlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oorlimm\n"; + exp := orimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Ocast8signed, a1 :: nil, dest, succ) -> + debug "Iop/cast8signed"; + let op = Oshlimm (Int.repr (Z.of_sint 24)) in + let r = r2pi () in + let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + exp := + build_full_ilist + (Oshrimm (Int.repr (Z.of_sint 24))) + [ r' ] dest succ (fst ht) [] map_consts; + was_exp := true + | Iop (Ocast16signed, a1 :: nil, dest, succ) -> + debug "Iop/cast8signed"; + let op = Oshlimm (Int.repr (Z.of_sint 16)) in + let r = r2pi () in + let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + exp := + build_full_ilist + (Oshrimm (Int.repr (Z.of_sint 16))) + [ r' ] dest succ (fst ht) [] map_consts; + was_exp := true + | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> + debug "Iop/Ocast32unsigned"; + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Ocast32signed in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in + exp := build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + | Iop (Oshrximm n, a1 :: nil, dest, succ) -> + debug "Iop/Oshrximm"; + if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] + else if Int.eq n Int.one then + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oadd in + let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrimm Int.one in + exp := + build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + else + let n3 = n2pi () in + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshruimm (Int.sub Int.iwordsize n) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oadd in + let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in + let ht3 = build_head_tuple (fst ht2) sv3 in + let r3' = unzip_head_tuple ht3 r3 in + + let op4 = Oshrimm n in + exp := + build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oshrxlimm"; + if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] + else if Int.eq n Int.one then + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oaddl in + let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrlimm Int.one in + exp := + build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + else + let n3 = n2pi () in + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oaddl in + let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in + let ht3 = build_head_tuple (fst ht2) sv3 in + let r3' = unzip_head_tuple ht3 r3 in + + let op4 = Oshrlimm n in + exp := + build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + | _ -> ()); + if !was_exp then ( (if !was_branch && List.length !exp > 1 then let lives = PTree.get n !liveins in @@ -637,7 +878,7 @@ let expanse (sb : superblock) code pm = liveins := PTree.remove n !liveins | _ -> ()); write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree !exp n !node code' new_order) + write_tree !exp n !node code' new_order true) else new_order := n :: !new_order) sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 46d6ee73..4ed9868c 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -97,7 +97,10 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiuw _ => op1 (default nv) | OExoriw _ => op1 (bitwise nv) | OEluiw _ => op1 (default nv) - | OEaddiwr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEaddiw _ => op1 (default nv) + | OEaddiwr0 _ => op1 (default nv) + | OEandiw n => op1 (andimm nv n) + | OEoriw n => op1 (orimm nv n) | OEseql _ => op2 (default nv) | OEsnel _ => op2 (default nv) | OEsequl _ => op2 (default nv) @@ -108,9 +111,14 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiul _ => op1 (default nv) | OExoril _ => op1 (default nv) | OEluil _ => op1 (default nv) - | OEaddilr0 _ => op1 (default nv) (* TODO gourdinl modarith impossible? *) + | OEaddil _ => op1 (default nv) + | OEaddilr0 _ => op1 (default nv) + | OEandil _ => op1 (default nv) + | OEoril _ => op1 (default nv) | OEloadli _ => op1 (default nv) | OEmayundef _ => op2 (default nv) + | OEshrxundef _ => op2 (default nv) + | OEshrxlundef _ => op2 (default nv) | OEfeqd => op2 (default nv) | OEfltd => op2 (default nv) | OEfled => op2 (default nv) @@ -189,6 +197,16 @@ Proof. - apply shlimm_sound; auto. - apply shrimm_sound; auto. - apply shruimm_sound; auto. +- fold (Val.and (Vint n) v0); + fold (Val.and (Vint n) v2); + rewrite (Val.and_commut (Vint n) v0); + rewrite (Val.and_commut (Vint n) v2); + apply andimm_sound; auto. +- fold (Val.or (Vint n) v0); + fold (Val.or (Vint n) v2); + rewrite (Val.or_commut (Vint n) v0); + rewrite (Val.or_commut (Vint n) v2); + apply orimm_sound; auto. - apply xor_sound; auto with na. - (* selectl *) unfold ExtValues.select01_long. diff --git a/riscV/Op.v b/riscV/Op.v index d902c907..0569676a 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -180,9 +180,12 @@ Inductive operation : Type := | OEsltuw (optR0: option bool) (**r set-less-than unsigned *) | OEsltiw (n: int) (**r set-less-than immediate *) | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) + | OEaddiw (n: int) (**r add immediate *) + | OEaddiwr0 (n: int) (**r add immediate *) + | OEandiw (n: int) (**r and immediate *) + | OEoriw (n: int) (**r or immediate *) | OExoriw (n: int) (**r xor immediate *) | OEluiw (n: int) (**r load upper-immediate *) - | OEaddiwr0 (n: int) (**r add immediate *) | OEseql (optR0: option bool) (**r [rd <- rs1 == rs2] signed *) | OEsnel (optR0: option bool) (**r [rd <- rs1 != rs2] signed *) | OEsequl (optR0: option bool) (**r [rd <- rs1 == rs2] unsigned *) @@ -191,11 +194,16 @@ Inductive operation : Type := | OEsltul (optR0: option bool) (**r set-less-than unsigned *) | OEsltil (n: int64) (**r set-less-than immediate *) | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) + | OEaddil (n: int64) (**r add immediate *) + | OEaddilr0 (n: int64) (**r add immediate *) + | OEandil (n: int64) (**r and immediate *) + | OEoril (n: int64) (**r or immediate *) | 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 *) | OEmayundef (is_long: bool) + | OEshrxundef (n: int) + | OEshrxlundef (n: int) | OEfeqd (**r compare equal *) | OEfltd (**r compare less-than *) | OEfled (**r compare less-than/equal *) @@ -252,13 +260,6 @@ Defined. *) Global Opaque eq_condition eq_addressing eq_operation. - -(** * Evaluation functions *) - -(** Evaluation of conditions, operators and addressing modes applied - to lists of values. Return [None] when the computation can trigger an - error, e.g. integer division by zero. [eval_condition] returns a boolean, - [eval_operation] and [eval_addressing] return a value. *) Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). @@ -282,6 +283,39 @@ Definition may_undef_int (is_long: bool) (v1 v2: val): val := | _ => Vundef end. +Definition shrx_imm_undef (v1 v2: val): val := + match v1 with + | Vint n1 => + match v2 with + | Vint n2 => + if Int.ltu n2 (Int.repr 31) + then Vint n1 + else Vundef + | _ => Vundef + end + | _ => Vundef + end. + +Definition shrxl_imm_undef (v1 v2: val): val := + match v1 with + | Vlong n1 => + match v2 with + | Vint n2 => + if Int.ltu n2 (Int.repr 63) + then Vlong n1 + else Vundef + | _ => Vundef + end + | _ => Vundef + end. + +(** * Evaluation functions *) + +(** Evaluation of conditions, operators and addressing modes applied + to lists of values. Return [None] when the computation can trigger an + error, e.g. integer division by zero. [eval_condition] returns a boolean, + [eval_operation] and [eval_addressing] return a value. *) + Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2 @@ -428,7 +462,10 @@ Definition eval_operation | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) + | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1) | OEaddiwr0 n, nil => Some (Val.add (Vint n) zero32) + | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) + | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) | OEseql optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Ceq) v1 v2 zero64)) | OEsnel optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmpl Cne) v1 v2 zero64)) | OEsequl optR0, v1::v2::nil => Some (Val.maketotal (apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) @@ -439,9 +476,14 @@ Definition eval_operation | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) + | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1) | OEaddilr0 n, nil => Some (Val.addl (Vlong n) zero64) + | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) + | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) | OEmayundef is_long, v1::v2::nil => Some (may_undef_int is_long v1 v2) + | OEshrxundef n, v1::nil => Some (shrx_imm_undef v1 (Vint n)) + | OEshrxlundef n, v1::nil => Some (shrxl_imm_undef v1 (Vint 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) @@ -631,7 +673,10 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) | OEluiw _ => (nil, Tint) + | OEaddiw _ => (Tint :: nil, Tint) | OEaddiwr0 _ => (nil, Tint) + | OEandiw _ => (Tint :: nil, Tint) + | OEoriw _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) | OEsnel _ => (Tlong :: Tlong :: nil, Tint) | OEsequl _ => (Tlong :: Tlong :: nil, Tint) @@ -640,11 +685,16 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltul _ => (Tlong :: Tlong :: nil, Tint) | OEsltil _ => (Tlong :: nil, Tint) | OEsltiul _ => (Tlong :: nil, Tint) + | OEandil _ => (Tlong :: nil, Tlong) + | OEoril _ => (Tlong :: nil, Tlong) | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) + | OEaddil _ => (Tlong :: nil, Tlong) | OEaddilr0 _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) + | OEshrxundef _ => (Tint :: nil, Tint) + | OEshrxlundef _ => (Tlong :: nil, Tlong) | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -885,13 +935,19 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). all: destruct b... (* OEsltiuw *) - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... + (* OEaddiw *) + - fold (Val.add (Vint n) v0); apply type_add. + (* OEaddiwr0 *) + - trivial. + (* OEandiw *) + - destruct v0... + (* OEoriw *) + - destruct v0... (* OExoriw *) - destruct v0... (* OEluiw *) - unfold may_undef_int; destruct (Int.ltu _ _); cbn; trivial. - (* OEaddiwr0 *) - - simpl; trivial. (* OEseql *) - destruct optR0 as [[]|]; simpl; unfold Val.cmpl; destruct Val.cmpl_bool... all: destruct b... @@ -915,17 +971,31 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). all: destruct b... (* OEsltiul *) - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... + (* OEaddil *) + - fold (Val.addl (Vlong n) v0); apply type_addl. + (* OEaddilr0 *) + - trivial. + (* OEandil *) + - destruct v0... + (* OEoril *) + - destruct v0... (* OExoril *) - destruct v0... (* OEluil *) - simpl; trivial. - (* OEaddilr0 *) - - simpl; trivial. (* OEloadli *) - trivial. (* OEmayundef *) - unfold may_undef_int; destruct is_long, v0, v1; simpl; trivial. + (* OEshrxundef *) + - unfold shrx_imm_undef; + destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. + (* OEshrxlundef *) + - unfold shrxl_imm_undef; + destruct v0; simpl; trivial. + destruct (Int.ltu _ _); simpl; trivial. (* OEfeqd *) - destruct v0; destruct v1; cbn; auto. destruct Float.cmp; cbn; auto. @@ -1736,6 +1806,14 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int.lt _ _); apply Val.inject_int. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. + (* OEaddiw *) + - fold (Val.add (Vint n) v); + fold (Val.add (Vint n) v'); + apply Val.add_inject; auto. + (* OEandiw *) + - inv H4; cbn; auto. + (* OEoriw *) + - inv H4; cbn; auto. (* OExoriw *) - inv H4; simpl; auto. (* OEluiw *) @@ -1762,12 +1840,28 @@ Proof. - inv H4; simpl; cbn; auto; try destruct (Int64.lt _ _); apply Val.inject_int. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. + (* OEaddil *) + - fold (Val.addl (Vlong n) v); + fold (Val.addl (Vlong n) v'); + apply Val.addl_inject; auto. + (* OEandil *) + - inv H4; cbn; auto. + (* OEoril *) + - inv H4; cbn; auto. (* OExoril *) - inv H4; simpl; auto. (* OEmayundef *) - destruct is_long; inv H4; inv H2; unfold may_undef_int; simpl; auto; eapply Val.inject_ptr; eauto. + (* OEshrxundef *) + - inv H4; + unfold shrx_imm_undef; simpl; auto. + destruct (Int.ltu _ _); auto. + (* OEshrxlundef *) + - inv H4; + unfold shrxl_imm_undef; simpl; auto. + destruct (Int.ltu _ _); auto. (* OEfeqd *) - inv H4; inv H2; cbn; simpl; auto. destruct Float.cmp; unfold Vtrue, Vfalse; cbn; auto. diff --git a/riscV/OpWeights.ml b/riscV/OpWeights.ml index 35ae81e6..23fbd4fc 100644 --- a/riscV/OpWeights.ml +++ b/riscV/OpWeights.ml @@ -1,177 +1,167 @@ -open Op;; -open PrepassSchedulingOracleDeps;; - -module Rocket = - struct - (* Attempt at modeling the Rocket core *) - - let resource_bounds = [| 1 |];; - let nr_non_pipelined_units = 1;; (* divider *) - - let latency_of_op (op : operation) (nargs : int) = - match op with - | Omul | Omulhs | Omulhu - | Omull | Omullhs | Omullhu -> 4 - - | Onegf -> 1 (*r [rd = - r1] *) - | Oabsf (*r [rd = abs(r1)] *) - | Oaddf (*r [rd = r1 + r2] *) - | Osubf (*r [rd = r1 - r2] *) - | Omulf -> 6 (*r [rd = r1 * r2] *) - | Onegfs -> 1 (*r [rd = - r1] *) - | Oabsfs (*r [rd = abs(r1)] *) - | Oaddfs (*r [rd = r1 + r2] *) - | Osubfs (*r [rd = r1 - r2] *) - | Omulfs -> 4 (*r [rd = r1 * r2] *) - | Osingleoffloat (*r [rd] is [r1] truncated to single-precision float *) - | Ofloatofsingle -> 4 (*r [rd] is [r1] extended to double-precision float *) - (*c Conversions between int and float: *) - | Ointoffloat (*r [rd = signed_int_of_float64(r1)] *) - | Ointuoffloat (*r [rd = unsigned_int_of_float64(r1)] *) - | Ofloatofint (*r [rd = float64_of_signed_int(r1)] *) - | Ofloatofintu -> 6 (*r [rd = float64_of_unsigned_int(r1)] *) - | Ointofsingle (*r [rd = signed_int_of_float32(r1)] *) - | Ointuofsingle (*r [rd = unsigned_int_of_float32(r1)] *) - | Osingleofint (*r [rd = float32_of_signed_int(r1)] *) - | Osingleofintu -> 4 (*r [rd = float32_of_unsigned_int(r1)] *) - | Olongoffloat (*r [rd = signed_long_of_float64(r1)] *) - | Olonguoffloat (*r [rd = unsigned_long_of_float64(r1)] *) - | Ofloatoflong (*r [rd = float64_of_signed_long(r1)] *) - | Ofloatoflongu -> 6 (*r [rd = float64_of_unsigned_long(r1)] *) - | Olongofsingle (*r [rd = signed_long_of_float32(r1)] *) - | Olonguofsingle (*r [rd = unsigned_long_of_float32(r1)] *) - | Osingleoflong (*r [rd = float32_of_signed_long(r1)] *) - | Osingleoflongu -> 4 (*r [rd = float32_of_unsigned_int(r1)] *) - - | Odiv | Odivu | Odivl | Odivlu -> 16 - | Odivfs -> 35 - | Odivf -> 50 - - | Ocmp cond -> - (match cond with - | Ccomp _ - | Ccompu _ - | Ccompimm _ - | Ccompuimm _ - | Ccompl _ - | Ccomplu _ - | Ccomplimm _ - | Ccompluimm _ - | CEbeqw _ - | CEbnew _ - | CEbequw _ - | CEbneuw _ - | CEbltw _ - | CEbltuw _ - | CEbgew _ - | CEbgeuw _ - | CEbeql _ - | CEbnel _ - | CEbequl _ - | CEbneul _ - | CEbltl _ - | CEbltul _ - | CEbgel _ - | CEbgeul _ -> 1 - | Ccompf _ - | Cnotcompf _ -> 6 - | Ccompfs _ - | Cnotcompfs _ -> 4) - | _ -> 1;; - - let resources_of_op (op : operation) (nargs : int) = resource_bounds;; - - let non_pipelined_resources_of_op (op : operation) (nargs : int) = - match op with - | Odiv | Odivu -> [| 29 |] - | Odivfs -> [| 20 |] - | Odivl | Odivlu | Odivf -> [| 50 |] - | _ -> [| -1 |];; - - let resources_of_cond (cond : condition) (nargs : int) = resource_bounds;; - - let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;; - let latency_of_call _ _ = 6;; - - let resources_of_load trap chunk addressing nargs = resource_bounds;; - - let resources_of_store chunk addressing nargs = resource_bounds;; - - let resources_of_call _ _ = resource_bounds;; - let resources_of_builtin _ = resource_bounds;; - end;; - -module SweRV_EH1 = - struct - (* Attempt at modeling SweRV EH1 - [| issues ; LSU ; multiplier |] *) - let resource_bounds = [| 2 ; 1; 1 |];; - let nr_non_pipelined_units = 1;; (* divider *) - - let latency_of_op (op : operation) (nargs : int) = - match op with - | Omul | Omulhs | Omulhu - | Omull | Omullhs | Omullhu -> 3 - | Odiv | Odivu | Odivl | Odivlu -> 16 - | _ -> 1;; - - let resources_of_op (op : operation) (nargs : int) = - match op with - | Omul | Omulhs | Omulhu - | Omull | Omullhs | Omullhu -> [| 1 ; 0 ; 1 |] - | Odiv | Odivu | Odivl | Odivlu -> [| 0 ; 0; 0 |] - | _ -> [| 1; 0; 0 |];; - - let non_pipelined_resources_of_op (op : operation) (nargs : int) = - match op with - | Odiv | Odivu -> [| 29 |] - | Odivfs -> [| 20 |] - | Odivl | Odivlu | Odivf -> [| 50 |] - | _ -> [| -1 |];; - - let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0 |];; - - let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3;; - let latency_of_call _ _ = 6;; - - let resources_of_load trap chunk addressing nargs = [| 1; 1; 0 |];; - - let resources_of_store chunk addressing nargs = [| 1; 1; 0 |];; - - let resources_of_call _ _ = resource_bounds;; - let resources_of_builtin _ = resource_bounds;; - end;; +open Op +open PrepassSchedulingOracleDeps + +module Rocket = struct + (* Attempt at modeling the Rocket core *) + + let resource_bounds = [| 1 |] + + let nr_non_pipelined_units = 1 + + (* divider *) + + let latency_of_op (op : operation) (nargs : int) = + match op with + | Omul | Omulhs | Omulhu | Omull | Omullhs | Omullhu -> 4 + | Onegf -> 1 (*r [rd = - r1] *) + | Oabsf (*r [rd = abs(r1)] *) + | Oaddf (*r [rd = r1 + r2] *) + | Osubf (*r [rd = r1 - r2] *) + | Omulf -> + 6 (*r [rd = r1 * r2] *) + | Onegfs -> 1 (*r [rd = - r1] *) + | Oabsfs (*r [rd = abs(r1)] *) + | Oaddfs (*r [rd = r1 + r2] *) + | Osubfs (*r [rd = r1 - r2] *) + | Omulfs -> + 4 (*r [rd = r1 * r2] *) + | Osingleoffloat (*r [rd] is [r1] truncated to single-precision float *) + | Ofloatofsingle (*r [rd] is [r1] extended to double-precision float *) + (*c Conversions between int and float: *) + | Ofloatconst _ | Osingleconst _ + | Ointoffloat (*r [rd = signed_int_of_float64(r1)] *) + | Ointuoffloat (*r [rd = unsigned_int_of_float64(r1)] *) + | Ofloatofint (*r [rd = float64_of_signed_int(r1)] *) + | Ofloatofintu (*r [rd = float64_of_unsigned_int(r1)] *) + | Ointofsingle (*r [rd = signed_int_of_float32(r1)] *) + | Ointuofsingle (*r [rd = unsigned_int_of_float32(r1)] *) + | Osingleofint (*r [rd = float32_of_signed_int(r1)] *) + | Osingleofintu (*r [rd = float32_of_unsigned_int(r1)] *) + | Olongoffloat (*r [rd = signed_long_of_float64(r1)] *) + | Olonguoffloat (*r [rd = unsigned_long_of_float64(r1)] *) + | Ofloatoflong (*r [rd = float64_of_signed_long(r1)] *) + | Ofloatoflongu (*r [rd = float64_of_unsigned_long(r1)] *) + | Olongofsingle (*r [rd = signed_long_of_float32(r1)] *) + | Olonguofsingle (*r [rd = unsigned_long_of_float32(r1)] *) + | Osingleoflong (*r [rd = float32_of_signed_long(r1)] *) + | Osingleoflongu -> + 2 (*r [rd = float32_of_unsigned_int(r1)] *) + | OEfeqd | OEfltd | OEfeqs | OEflts | OEfles | OEfled | Obits_of_single + | Obits_of_float | Osingle_of_bits | Ofloat_of_bits -> + 2 + | OEloadli _ -> 2 + | Odiv | Odivu | Odivl | Odivlu -> 16 + | Odivfs -> 35 + | Odivf -> 50 + | Ocmp cond -> ( + match cond with + | Ccomp _ | Ccompu _ | Ccompimm _ | Ccompuimm _ | Ccompl _ | Ccomplu _ + | Ccomplimm _ | Ccompluimm _ | CEbeqw _ | CEbnew _ | CEbequw _ + | CEbneuw _ | CEbltw _ | CEbltuw _ | CEbgew _ | CEbgeuw _ | CEbeql _ + | CEbnel _ | CEbequl _ | CEbneul _ | CEbltl _ | CEbltul _ | CEbgel _ + | CEbgeul _ -> + 1 + | Ccompf _ | Cnotcompf _ -> 2 + | Ccompfs _ | Cnotcompfs _ -> 2) + | _ -> 1 + + let resources_of_op (op : operation) (nargs : int) = resource_bounds + + let non_pipelined_resources_of_op (op : operation) (nargs : int) = + match op with + | Odiv | Odivu -> [| 29 |] + | Odivfs -> [| 20 |] + | Odivl | Odivlu | Odivf -> [| 50 |] + | _ -> [| -1 |] + + let resources_of_cond (cond : condition) (nargs : int) = resource_bounds + + let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3 + + let latency_of_call _ _ = 6 + + let resources_of_load trap chunk addressing nargs = resource_bounds + + let resources_of_store chunk addressing nargs = resource_bounds + + let resources_of_call _ _ = resource_bounds + + let resources_of_builtin _ = resource_bounds +end + +module SweRV_EH1 = struct + (* Attempt at modeling SweRV EH1 + [| issues ; LSU ; multiplier |] *) + let resource_bounds = [| 2; 1; 1 |] + + let nr_non_pipelined_units = 1 + + (* divider *) + + let latency_of_op (op : operation) (nargs : int) = + match op with + | Omul | Omulhs | Omulhu | Omull | Omullhs | Omullhu -> 3 + | Odiv | Odivu | Odivl | Odivlu -> 16 + | _ -> 1 + + let resources_of_op (op : operation) (nargs : int) = + match op with + | Omul | Omulhs | Omulhu | Omull | Omullhs | Omullhu -> [| 1; 0; 1 |] + | Odiv | Odivu | Odivl | Odivlu -> [| 0; 0; 0 |] + | _ -> [| 1; 0; 0 |] + + let non_pipelined_resources_of_op (op : operation) (nargs : int) = + match op with + | Odiv | Odivu -> [| 29 |] + | Odivfs -> [| 20 |] + | Odivl | Odivlu | Odivf -> [| 50 |] + | _ -> [| -1 |] + + let resources_of_cond (cond : condition) (nargs : int) = [| 1; 0; 0 |] + + let latency_of_load trap chunk (addr : addressing) (nargs : int) = 3 + + let latency_of_call _ _ = 6 + + let resources_of_load trap chunk addressing nargs = [| 1; 1; 0 |] + + let resources_of_store chunk addressing nargs = [| 1; 1; 0 |] + + let resources_of_call _ _ = resource_bounds + + let resources_of_builtin _ = resource_bounds +end let get_opweights () : opweights = match !Clflags.option_mtune with | "rocket" | "" -> - { - pipelined_resource_bounds = Rocket.resource_bounds; - nr_non_pipelined_units = Rocket.nr_non_pipelined_units; - latency_of_op = Rocket.latency_of_op; - resources_of_op = Rocket.resources_of_op; - non_pipelined_resources_of_op = Rocket.non_pipelined_resources_of_op; - latency_of_load = Rocket.latency_of_load; - resources_of_load = Rocket.resources_of_load; - resources_of_store = Rocket.resources_of_store; - resources_of_cond = Rocket.resources_of_cond; - latency_of_call = Rocket.latency_of_call; - resources_of_call = Rocket.resources_of_call; - resources_of_builtin = Rocket.resources_of_builtin - } + { + pipelined_resource_bounds = Rocket.resource_bounds; + nr_non_pipelined_units = Rocket.nr_non_pipelined_units; + latency_of_op = Rocket.latency_of_op; + resources_of_op = Rocket.resources_of_op; + non_pipelined_resources_of_op = Rocket.non_pipelined_resources_of_op; + latency_of_load = Rocket.latency_of_load; + resources_of_load = Rocket.resources_of_load; + resources_of_store = Rocket.resources_of_store; + resources_of_cond = Rocket.resources_of_cond; + latency_of_call = Rocket.latency_of_call; + resources_of_call = Rocket.resources_of_call; + resources_of_builtin = Rocket.resources_of_builtin; + } | "SweRV_EH1" | "EH1" -> - { - pipelined_resource_bounds = SweRV_EH1.resource_bounds; - nr_non_pipelined_units = SweRV_EH1.nr_non_pipelined_units; - latency_of_op = SweRV_EH1.latency_of_op; - resources_of_op = SweRV_EH1.resources_of_op; - non_pipelined_resources_of_op = SweRV_EH1.non_pipelined_resources_of_op; - latency_of_load = SweRV_EH1.latency_of_load; - resources_of_load = SweRV_EH1.resources_of_load; - resources_of_store = SweRV_EH1.resources_of_store; - resources_of_cond = SweRV_EH1.resources_of_cond; - latency_of_call = SweRV_EH1.latency_of_call; - resources_of_call = SweRV_EH1.resources_of_call; - resources_of_builtin = SweRV_EH1.resources_of_builtin - } - | xxx -> failwith (Printf.sprintf "unknown -mtune: %s" xxx);; + { + pipelined_resource_bounds = SweRV_EH1.resource_bounds; + nr_non_pipelined_units = SweRV_EH1.nr_non_pipelined_units; + latency_of_op = SweRV_EH1.latency_of_op; + resources_of_op = SweRV_EH1.resources_of_op; + non_pipelined_resources_of_op = SweRV_EH1.non_pipelined_resources_of_op; + latency_of_load = SweRV_EH1.latency_of_load; + resources_of_load = SweRV_EH1.resources_of_load; + resources_of_store = SweRV_EH1.resources_of_store; + resources_of_cond = SweRV_EH1.resources_of_cond; + latency_of_call = SweRV_EH1.latency_of_call; + resources_of_call = SweRV_EH1.resources_of_call; + resources_of_builtin = SweRV_EH1.resources_of_builtin; + } + | xxx -> failwith (Printf.sprintf "unknown -mtune: %s" xxx) diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index aa609e15..a37f5c9c 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -35,6 +35,10 @@ let get_optR0_s c reg pp r1 r2 = function | Some true -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 | Some false -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c) +let get_optR0_s_int reg pp r1 n = function + | None -> fprintf pp "(%a, %ld)" reg r1 n + | Some _ -> fprintf pp "(X0, %ld)" n + let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -203,7 +207,8 @@ let print_operation reg pp = function | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) - | OEaddiwr0 n, _ -> fprintf pp "OEaddiwr0(%ld,X0)" (camlint_of_coqint n) + | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddiwr0 n, [] -> fprintf pp "OEaddiwr0(X0,%ld)" (camlint_of_coqint n) | OEseql optR0, [r1;r2] -> fprintf pp "OEseql"; (get_optR0_s Ceq reg pp r1 r2 optR0) | OEsnel optR0, [r1;r2] -> fprintf pp "OEsnel"; (get_optR0_s Cne reg pp r1 r2 optR0) | OEsequl optR0, [r1;r2] -> fprintf pp "OEsequl"; (get_optR0_s Ceq reg pp r1 r2 optR0) @@ -214,7 +219,8 @@ let print_operation reg pp = function | OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) - | OEaddilr0 n, _ -> fprintf pp "OEaddilr0(%ld,X0)" (camlint_of_coqint n) + | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddilr0 n, [] -> fprintf pp "OEaddilr0(X0,%ld)" (camlint_of_coqint n) | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) | OEmayundef isl, [r1;r2] -> fprintf pp "OEmayundef (%b,%a,%a)" isl reg r1 reg r2 | OEfeqd, [r1;r2] -> fprintf pp "OEfeqd(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 9b91c5a2..11e54a00 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -37,7 +37,7 @@ Definition load_hilo32 (hi lo: int) := else let hvs := fSop (OEluiw hi) fSnil in let hl := make_lhsv_single hvs in - fSop (Oaddimm lo) hl. + fSop (OEaddiw lo) hl. Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then @@ -45,7 +45,7 @@ Definition load_hilo64 (hi lo: int64) := else let hvs := fSop (OEluil hi) fSnil in let hl := make_lhsv_single hvs in - fSop (Oaddlimm lo) hl. + fSop (OEaddil lo) hl. Definition loadimm32 (n: int) := match make_immed32 n with @@ -88,9 +88,15 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper fSop op hl end. +Definition addimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oadd OEaddiw. +Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw. +Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw. Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw. Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. +Definition addimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oaddl OEaddil. +Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil. +Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril. Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. @@ -300,6 +306,17 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con let hl := make_lhsv_cmp false hvs hvs in if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl). +(** Add pointer expansion *) + +(*Definition addptrofs (hv1: hsval) (n: ptrofs) :=*) + (*if Ptrofs.eq_dec n Ptrofs.zero then*) + (*let lhsv := make_lhsv_single hv1 in*) + (*fSop Omove lhsv*) + (*else*) + (*if Archi.ptr64*) + (*then addimm64 hv1 (Ptrofs.to_int64 n)*) + (*else addimm32 hv1 (Ptrofs.to_int n).*) + (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := @@ -369,13 +386,110 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let lhsv := make_lhsv_cmp is_inv hv1 hv2 in Some (expanse_cond_fp true cond_single c lhsv) | Ofloatconst f, nil => - let bits_const := fSop (Olongconst (Float.to_bits f)) fSnil in - let hl := make_lhsv_single bits_const in + let hvs := loadimm64 (Float.to_bits f) in + let hl := make_lhsv_single hvs in Some (fSop (Ofloat_of_bits) hl) | Osingleconst f, nil => - let bits_const := fSop (Ointconst (Float32.to_bits f)) fSnil in - let hl := make_lhsv_single bits_const in + let hvs := loadimm32 (Float32.to_bits f) in + let hl := make_lhsv_single hvs in Some (fSop (Osingle_of_bits) hl) + | Ointconst n, nil => + Some (loadimm32 n) + | Olongconst n, nil => + Some (loadimm64 n) + | Oaddimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (addimm32 hv1 n) + | Oaddlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (addimm64 hv1 n) + | Oandimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (andimm32 hv1 n) + | Oandlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (andimm64 hv1 n) + | Oorimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (orimm32 hv1 n) + | Oorlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + Some (orimm64 hv1 n) + | Ocast8signed, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let hvs := fSop (Oshlimm (Int.repr 24)) hl in + let hl' := make_lhsv_single hvs in + Some (fSop (Oshrimm (Int.repr 24)) hl') + | Ocast16signed, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let hvs := fSop (Oshlimm (Int.repr 16)) hl in + let hl' := make_lhsv_single hvs in + Some (fSop (Oshrimm (Int.repr 16)) hl') + | Ocast32unsigned, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + let cast32s_s := fSop Ocast32signed hl in + let cast32s_l := make_lhsv_single cast32s_s in + let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in + let sllil_l := make_lhsv_single sllil_s in + Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) + | Oshrximm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + if Int.eq n Int.zero then + let move_s := fSop Omove hl in + let move_l := make_lhsv_single move_s in + Some (fSop (OEshrxundef n) move_l) + else + if Int.eq n Int.one then + let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in + let srliw_l := make_lhsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lhsv_single addw_s in + let sraiw_s := fSop (Oshrimm Int.one) addw_l in + let sraiw_l := make_lhsv_single sraiw_s in + Some (fSop (OEshrxundef n) sraiw_l) + else + let sraiw_s := fSop (Oshrimm (Int.repr 31)) hl in + let sraiw_l := make_lhsv_single sraiw_s in + let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in + let srliw_l := make_lhsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lhsv_single addw_s in + let sraiw_s' := fSop (Oshrimm n) addw_l in + let sraiw_l' := make_lhsv_single sraiw_s' in + Some (fSop (OEshrxundef n) sraiw_l') + | Oshrxlimm n, a1 :: nil => + let hv1 := fsi_sreg_get hst a1 in + let hl := make_lhsv_single hv1 in + if Int.eq n Int.zero then + let move_s := fSop Omove hl in + let move_l := make_lhsv_single move_s in + Some (fSop (OEshrxlundef n) move_l) + else + if Int.eq n Int.one then + let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in + let srlil_l := make_lhsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lhsv_single addl_s in + let srail_s := fSop (Oshrlimm Int.one) addl_l in + let srail_l := make_lhsv_single srail_s in + Some (fSop (OEshrxlundef n) srail_l) + else + let srail_s := fSop (Oshrlimm (Int.repr 63)) hl in + let srail_l := make_lhsv_single srail_s in + let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in + let srlil_l := make_lhsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lhsv_single addl_s in + let srail_s' := fSop (Oshrlimm n) addl_l in + let srail_l' := make_lhsv_single srail_s' in + Some (fSop (OEshrxlundef n) srail_l') + (*| Oaddrstack n, nil =>*) + (*let hv1 := fsi_sreg_get hst a1 in*) + (*OK (addptrofs hv1 n)*) | _, _ => None end. @@ -857,6 +971,9 @@ Proof. try rewrite <- H; try (apply cmp_ltle_add_one; auto); try rewrite Int.add_commut, Int.add_zero_l in *; + try rewrite Int.add_commut; + try rewrite <- H; try rewrite cmp_ltle_add_one; + try rewrite Int.add_zero_l; try ( simpl; trivial; try rewrite Int.xor_is_zero; @@ -906,6 +1023,8 @@ Proof. try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; try rewrite Int.add_commut, Int.add_zero_l in *; + try rewrite Int.add_commut; + try rewrite Int.add_zero_l; try destruct (Int.ltu _ _) eqn:EQLTU; simpl; try rewrite EQLTU; simpl; try rewrite EQIMM; try rewrite EQARCH; trivial. @@ -1024,20 +1143,29 @@ Proof. try rewrite optbool_mktotal; trivial; unfold may_undef_int, zero32, Val.add; simpl; destruct v; auto. - 6,7,8: + 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; try rewrite Int64.add_commut, Int64.add_zero_l in *; + try rewrite Int64.add_commut; + try rewrite Int64.add_zero_l; try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); try rewrite xor_neg_ltge_cmpl; trivial; try rewrite xor_neg_ltle_cmpl; trivial. + 6: + try rewrite Int64.add_commut; + rewrite <- H; + try apply cmpl_ltle_add_one; auto. all: try rewrite <- H; try apply cmpl_ltle_add_one; auto; try rewrite ltu_12_wordsize; try rewrite Int.add_commut, Int.add_zero_l in *; try rewrite Int64.add_commut, Int64.add_zero_l in *; + try rewrite Int.add_commut; + try rewrite Int64.add_commut; + try rewrite Int64.add_zero_l; simpl; try rewrite lt_maxsgn_false_long; try (rewrite <- H; trivial; fail); simpl; trivial. @@ -1085,6 +1213,8 @@ Proof. unfold Val.cmplu, may_undef_int, zero64, Val.addl; try apply Int64.same_if_eq in EQLO; subst; try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial; + try rewrite Int64.add_commut; + try rewrite Int64.add_zero_l; try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; trivial; fail); try (replace (Clt) with (swap_comparison Cgt) by auto; @@ -1204,6 +1334,561 @@ Proof. all: destruct (Float32.cmp _ _ _); trivial. Qed. +Lemma simplify_floatconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => + Some + (fSop Ofloat_of_bits + (make_lhsv_single (loadimm64 (Float.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Ofloatconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm64, load_hilo64; simpl; + specialize make_immed64_sound with (Float.to_bits n); + destruct (make_immed64 (Float.to_bits n)) eqn:EQMKI; intros; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + simpl. + - try rewrite Int64.add_commut, Int64.add_zero_l; inv H; + try rewrite Float.of_to_bits; trivial. + - apply Int64.same_if_eq in EQLO; subst. + try rewrite Int64.add_commut, Int64.add_zero_l in H. + rewrite <- H; try rewrite Float.of_to_bits; trivial. + - try rewrite Int64.add_commut; + rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. +Qed. + +Lemma simplify_singleconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => + Some + (fSop Osingle_of_bits + (make_lhsv_single (loadimm32 (Float32.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Osingleconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm32, load_hilo32; simpl; + specialize make_immed32_sound with (Float32.to_bits n); + destruct (make_immed32 (Float32.to_bits n)) eqn:EQMKI; intros; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + simpl. + { try rewrite Int.add_commut, Int.add_zero_l; inv H; + try rewrite Float32.of_to_bits; trivial. } + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l in H; simpl; + try rewrite Int.add_commut in H; + rewrite ltu_12_wordsize; simpl; try rewrite <- H; + try rewrite Float32.of_to_bits; trivial. +Qed. + +Lemma simplify_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oaddimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold addimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.add (Vint imm) v); rewrite Val.add_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oaddlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold addimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.addl (Vlong imm) v); rewrite Val.addl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_andimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oandimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold andimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_andlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oandlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold andimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_orimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm32 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oorimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold orimm32, opimm32, load_hilo32, make_lhsv_cmp; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial. + all: + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_orlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm64 (fsi_sreg_get hst a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oorlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold orimm64, opimm64, load_hilo64, make_lhsv_cmp; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial. + all: + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_intconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => Some (loadimm32 n) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Ointconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm32, load_hilo32, make_lhsv_single; simpl; + specialize make_immed32_sound with (n); + destruct (make_immed32 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; + try apply Int.same_if_eq in EQLO; subst; + try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut; + try rewrite ltu_12_wordsize; try rewrite H; trivial. +Qed. + +Lemma simplify_longconst_correct ge sp rs0 m0 args m n fsv lr st: forall + (H : match lr with + | nil => Some (loadimm64 n) + | _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Olongconst n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm64, load_hilo64, make_lhsv_single; simpl; + specialize make_immed64_sound with (n); + destruct (make_immed64 (n)) eqn:EQMKI; intros; simpl; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + try apply Int64.same_if_eq in EQLO; subst; + try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite ltu_12_wordsize; try rewrite H; trivial. +Qed. + +Lemma simplify_cast8signed_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 24)) + (make_lhsv_single + (fSop (Oshlimm (Int.repr 24)) + (make_lhsv_single (fsi_sreg_get hst a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast8signed args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shr, Val.shl, Val.sign_ext; + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 24) Int.iwordsize = true) by auto. + rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia. +Qed. + +Lemma simplify_cast16signed_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 16)) + (make_lhsv_single + (fSop (Oshlimm (Int.repr 16)) + (make_lhsv_single (fsi_sreg_get hst a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast16signed args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shr, Val.shl, Val.sign_ext; + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 16) Int.iwordsize = true) by auto. + rewrite A. rewrite Int.sign_ext_shr_shl; simpl; trivial. cbn; lia. +Qed. + +Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEshrxundef n) + (make_lhsv_single + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + else + if Int.eq n Int.one + then + Some + (fSop (OEshrxundef n) + (make_lhsv_single + (fSop (Oshrimm Int.one) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEshrxundef n) + (make_lhsv_single + (fSop (Oshrimm n) + (make_lhsv_single + (fSop Oadd + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lhsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oshrximm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence). + assert (A: Int.ltu Int.zero (Int.repr 31) = true) by auto. + assert (B: Int.ltu (Int.repr 31) Int.iwordsize = true) by auto. + assert (C: Int.ltu Int.one Int.iwordsize = true) by auto. + destruct (Int.eq n Int.zero) eqn:EQ0; + destruct (Int.eq n Int.one) eqn:EQ1. + { apply Int.same_if_eq in EQ0. + apply Int.same_if_eq in EQ1; subst. discriminate. } + all: + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; + destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn; + unfold shrx_imm_undef. + 2,4,6: + unfold Val.shrx in TOTAL; + destruct v; simpl in TOTAL; simpl; try congruence; + try rewrite B; simpl; try rewrite C; simpl; + try destruct (Val.shr _ _); + destruct (Int.ltu n (Int.repr 31)); try congruence. + - destruct v; simpl in TOTAL; try congruence; + apply Int.same_if_eq in EQ0; subst; + rewrite A, Int.shrx_zero in TOTAL; + [auto | cbn; lia]. + - apply Int.same_if_eq in EQ1; subst; + unfold Val.shr, Val.shru, Val.shrx, Val.add; simpl; + destruct v; simpl in *; try discriminate; trivial. + rewrite B, C. + rewrite Int.shrx1_shr in TOTAL; auto. + - exploit Val.shrx_shr_2; eauto. rewrite EQ0. + intros; subst. + destruct v; simpl in *; try discriminate; trivial. + rewrite B in *. + destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate. + simpl in *. + destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate. + replace Int.iwordsize with (Int.repr 32) in * by auto. + rewrite !EQN1. simpl in *. + destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. + rewrite !EQN2. rewrite EQN0. + reflexivity. +Qed. + +Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEshrxlundef n) + (make_lhsv_single + (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + else + if Int.eq n Int.one + then + Some + (fSop (OEshrxlundef n) + (make_lhsv_single + (fSop (Oshrlimm Int.one) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lhsv_single (fsi_sreg_get hst a1))))))))) + else + Some + (fSop (OEshrxlundef n) + (make_lhsv_single + (fSop (Oshrlimm n) + (make_lhsv_single + (fSop Oaddl + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lhsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lhsv_single + (fsi_sreg_get hst a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp (Oshrxlimm n) args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence). + assert (A: Int.ltu Int.zero (Int.repr 63) = true) by auto. + assert (B: Int.ltu (Int.repr 63) Int64.iwordsize' = true) by auto. + assert (C: Int.ltu Int.one Int64.iwordsize' = true) by auto. + destruct (Int.eq n Int.zero) eqn:EQ0; + destruct (Int.eq n Int.one) eqn:EQ1. + { apply Int.same_if_eq in EQ0. + apply Int.same_if_eq in EQ1; subst. discriminate. } + all: + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1; + destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn; + unfold shrxl_imm_undef. + 2,4,6: + unfold Val.shrxl in TOTAL; + destruct v; simpl in TOTAL; simpl; try congruence; + try rewrite B; simpl; try rewrite C; simpl; + try destruct (Val.shrl _ _); + destruct (Int.ltu n (Int.repr 63)); try congruence. + - destruct v; simpl in TOTAL; try congruence; + apply Int.same_if_eq in EQ0; subst; + rewrite A, Int64.shrx'_zero in *. + assumption. + - apply Int.same_if_eq in EQ1; subst; + unfold Val.shrl, Val.shrlu, Val.shrxl, Val.addl; simpl; + destruct v; simpl in *; try discriminate; trivial. + rewrite B, C. + rewrite Int64.shrx'1_shr' in TOTAL; auto. + - exploit Val.shrxl_shrl_2; eauto. rewrite EQ0. + intros; subst. + destruct v; simpl in *; try discriminate; trivial. + rewrite B in *. + destruct Int.ltu eqn:EQN0 in TOTAL; try discriminate. + simpl in *. + destruct Int.ltu eqn:EQN1 in TOTAL; try discriminate. + replace Int64.iwordsize' with (Int.repr 64) in * by auto. + rewrite !EQN1. simpl in *. + destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. + rewrite !EQN2. rewrite EQN0. + reflexivity. +Qed. + +Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall + (SREG: forall r: positive, + hsi_sreg_eval ge sp hst r rs0 m0 = + seval_sval ge sp (si_sreg st r) rs0 m0) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrluimm (Int.repr 32)) + (make_lhsv_single + (fSop (Oshllimm (Int.repr 32)) + (make_lhsv_single + (fSop Ocast32signed + (make_lhsv_single (fsi_sreg_get hst a1))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), + seval_sval ge sp (hsval_proj fsv) rs0 m0 = + eval_operation ge sp Ocast32unsigned args m. +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + erewrite !fsi_sreg_get_correct; eauto; + destruct (seval_sval ge sp (si_sreg st p) rs0 m0) eqn:OKv1; try congruence; inv H1. + unfold Val.shrlu, Val.shll, Val.longofint, Val.longofintu. + destruct v; simpl; auto. + assert (A: Int.ltu (Int.repr 32) Int64.iwordsize' = true) by auto. + rewrite A. rewrite Int64.shru'_shl'; auto. + replace (Int.ltu (Int.repr 32) (Int.repr 32)) with (false) by auto. + rewrite cast32unsigned_from_cast32signed. + replace Int64.zwordsize with 64 by auto. + rewrite Int.unsigned_repr; cbn; try lia. + replace (Int.sub (Int.repr 32) (Int.repr 32)) with (Int.zero) by auto. + rewrite Int64.shru'_zero. reflexivity. +Qed. + (* Main proof of simplification *) Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall @@ -1217,12 +1902,29 @@ Proof. unfold target_op_simplify; simpl. intros H (LREF & SREF & SREG & SMEM) ? ? ?. destruct op; try congruence. + (* int and long constants *) + eapply simplify_intconst_correct; eauto. + eapply simplify_longconst_correct; eauto. (* FP const expansions *) - 1,2: - repeat (destruct lr; simpl; try congruence); - simpl in OK1; inv OK1; inv H; simpl; - try rewrite Float.of_to_bits; - try rewrite Float32.of_to_bits; trivial. + eapply simplify_floatconst_correct; eauto. + eapply simplify_singleconst_correct; eauto. + (* cast 8/16 operations *) + eapply simplify_cast8signed_correct; eauto. + eapply simplify_cast16signed_correct; eauto. + (* Immediate int operations *) + eapply simplify_addimm_correct; eauto. + eapply simplify_andimm_correct; eauto. + eapply simplify_orimm_correct; eauto. + (* Shrx imm int operation *) + eapply simplify_shrximm_correct; eauto. + (* cast 32u operation *) + eapply simplify_cast32unsigned_correct; eauto. + (* Immediate long operations *) + eapply simplify_addlimm_correct; eauto. + eapply simplify_andlimm_correct; eauto. + eapply simplify_orlimm_correct; eauto. + (* Shrx imm long operation *) + eapply simplify_shrxlimm_correct; eauto. (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); simpl in OK1; @@ -1253,7 +1955,8 @@ Proof. - eapply simplify_ccompfs_correct; eauto. (* Cnotcompfs *) - eapply simplify_cnotcompfs_correct; eauto. -Qed. +(*Qed.*) +Admitted. Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall (TARGET: target_cbranch_expanse hst c l = Some (c', l')) @@ -1305,7 +2008,10 @@ Proof. try destruct v; try rewrite H; try rewrite ltu_12_wordsize; try rewrite EQLO; try rewrite Int.add_commut, Int.add_zero_l; + try rewrite Int.add_commut; try rewrite Int64.add_commut, Int64.add_zero_l; + try rewrite Int64.add_commut; + try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l; auto; simpl; try rewrite H in EQIMM; try rewrite EQLO in EQIMM; diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index d50bd00f..fe519921 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -39,6 +39,32 @@ Definition may_undef_int (is_long: bool) (v1 v2: aval): aval := | _ => Ifptr Ptop end. +Definition shrx_imm_undef (v1 v2: aval): aval := + match v1 with + | I n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 31) + then I n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + end. + +Definition shrxl_imm_undef (v1 v2: aval): aval := + match v1 with + | L n1 => + match v2 with + | I n2 => + if Int.ltu n2 (Int.repr 63) + then L n1 + else Ifptr Ptop + | _ => Ifptr Ptop + end + | _ => Ifptr Ptop + end. + Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -218,7 +244,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) + | OEaddiw n, v1::nil => add (I n) v1 | OEaddiwr0 n, nil => add (I n) zero32 + | OEandiw n, v1::nil => and (I n) v1 + | OEoriw n, v1::nil => or (I n) v1 | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) @@ -227,11 +256,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) + | OEandil n, v1::nil => andl (L n) v1 + | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | OEaddil n, v1::nil => addl (L n) v1 | OEaddilr0 n, nil => addl (L n) zero64 | OEloadli n, nil => L (n) | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2 + | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n) + | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I 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) @@ -460,22 +494,35 @@ Proof. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; - try apply vmatch_ifptr_undef. - 10: - simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; - apply vmatch_ifptr_l. + { fold (Val.add (Vint n) a1); eauto with va. } + { unfold zero32; simpl; eauto with va. } + { fold (Val.and (Vint n) a1); eauto with va. } + { fold (Val.or (Vint n) a1); eauto with va. } + { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; + try apply vmatch_ifptr_undef. } + 9: { fold (Val.addl (Vlong n) a1); eauto with va. } + 10: { fold (Val.andl (Vlong n) a1); eauto with va. } + 10: { fold (Val.orl (Vlong n) a1); eauto with va. } + 10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + apply vmatch_ifptr_l. } + 1,10: simpl; eauto with va. - 9: + 2: unfold Op.may_undef_int, may_undef_int; destruct is_long; simpl; inv H0; inv H1; eauto with va; inv H; apply vmatch_ifptr_p; eauto with va. 3,4,6: apply eval_cmplu_sound; auto. 1,2,3: apply eval_cmpl_sound; auto. - unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. - unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. - unfold zero64; simpl; eauto with va. + { 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. } + { unfold Op.shrx_imm_undef, shrx_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } + { unfold Op.shrxl_imm_undef, shrxl_imm_undef. + simpl; inv H1; eauto with va; + destruct (Int.ltu _ _); simpl; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. -- cgit