From df9aab806ae8d20393b56e4175e210ed6cff1ef1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 12:48:51 +0200 Subject: a more general way to manage special registers before introducing SP --- riscV/ExpansionOracle.ml | 121 ++++++++++++++++++++++++----------------------- 1 file changed, 61 insertions(+), 60 deletions(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index c03e0d03..16f1ee4b 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -66,7 +66,7 @@ let find_or_addnmove op args rd succ map_consts not_final = if not_final then node := !node - 1; Sr (P.of_int r) | None -> - if not (List.exists (fun a -> a = rd) args) && not_final then + if (not (List.exists (fun a -> a = rd) args)) && not_final then Hashtbl.add map_consts sop (p2i rd); Si (Iop (op, args, rd, succ)) @@ -208,131 +208,132 @@ let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul let is_inv_cmp = function Cle | Cgt -> true | _ -> false -let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None +let make_optR is_x0 is_inv = + if is_x0 then if is_inv then Some X0_L else Some X0_R else None let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbequw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneuw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Icond (CEbequl optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneul optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Ceq -> Icond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: 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 + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEseqw optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnew optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltw optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltw optR0 in + let op = OEsltw optR 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) ] + | Cgt -> [ Iop (OEsltw optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltw optR0 in + let op = OEsltw optR 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 map_consts = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEsequw optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneuw optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltuw optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltuw optR0 in + let op = OEsltuw optR 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) ] + | Cgt -> [ Iop (OEsltuw optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltuw optR0 in + let op = OEsltuw optR 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 map_consts = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEseql optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnel optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltl optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltl optR0 in + let op = OEsltl optR 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) ] + | Cgt -> [ Iop (OEsltl optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltl optR0 in + let op = OEsltl optR 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 map_consts = - let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ] + | Ceq -> [ Iop (OEsequl optR, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneul optR, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltul optR, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - let op = OEsltul optR0 in + let op = OEsltul optR 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) ] + | Cgt -> [ Iop (OEsltul optR, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - let op = OEsltul optR0 in + let op = OEsltul optR 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 @@ -481,8 +482,8 @@ let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts = 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) ]) + (if normal' then [ Icond (CEbnew (Some X0_R), [ r; r ], succ1, succ2, info) ] + else [ Icond (CEbeqw (Some X0_R), [ r; r ], succ1, succ2, info) ]) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] -- cgit