From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 20 May 2021 11:58:40 +0200 Subject: Changing to an opaq record in BTL info, this is a broken commit --- riscV/ExpansionOracle.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 1384b9b3..735f5cf5 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -23,6 +23,7 @@ open Camlcoq open Option open AST open DebugPrint +open AuxTools (** Mini CSE (a dynamic numbering is applied during expansion. The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) @@ -33,8 +34,6 @@ let reg = ref 1 let node = ref 1 -let p2i r = P.to_int r - let r2p () = P.of_int !reg let n2p () = P.of_int !node -- cgit From 0efe7783c50d72858352fda93d30e0f52792d658 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 24 May 2021 10:07:52 +0200 Subject: Moving common tools, adding liveness input/output information to BTL generation oracle --- riscV/ExpansionOracle.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 735f5cf5..8a17217a 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -23,7 +23,7 @@ open Camlcoq open Option open AST open DebugPrint -open AuxTools +open RTLcommonaux (** Mini CSE (a dynamic numbering is applied during expansion. The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) -- cgit From c3ce32da7d431069ef355296bef66b112a302b78 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 12:32:21 +0200 Subject: op simplify BTL intro --- riscV/BTL_SEsimplify.v | 1 + 1 file changed, 1 insertion(+) create mode 120000 riscV/BTL_SEsimplify.v (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v new file mode 120000 index 00000000..f190e6d5 --- /dev/null +++ b/riscV/BTL_SEsimplify.v @@ -0,0 +1 @@ +../aarch64/BTL_SEsimplify.v \ No newline at end of file -- cgit From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- riscV/ExpansionOracle.ml | 1056 +--------------------------------------------- 1 file changed, 2 insertions(+), 1054 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index bbcc6807..0869007c 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -10,1058 +10,6 @@ (* *) (* *************************************************************) -open RTLpathLivegenaux -open RTLpathCommon -open Datatypes -open Maps -open RTL -open Op -open Asmgen -open RTLpath -open! Integers -open Camlcoq -open Option -open AST -open DebugPrint -open RTLcommonaux +let expanse n ibf btl = btl -(** Mini CSE (a dynamic numbering is applied during expansion. - The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) - -(** Managing virtual registers and node index *) - -let reg = ref 1 - -let node = ref 1 - -let r2p () = P.of_int !reg - -let n2p () = P.of_int !node - -let r2pi () = - reg := !reg + 1; - r2p () - -let n2pi () = - node := !node + 1; - n2p () - -(** Below are the types for rhs and equations *) - -type rhs = Sop of operation * int list | Smove - -type seq = Seq of int * rhs - -(** This is a mini abstraction to have a simpler representation during expansion - - Snop will be converted to Inop - - (Sr r) is inserted if the value was found in register r - - (Sexp dest rhs args succ) represent an instruction - (succesor may not be defined at this point, hence the use of type option) - - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must - always be the last instruction in expansion list *) - -type expl = - | Snop of P.t - | Sr of P.t - | Sexp of P.t * rhs * P.t list * node option - | Sfinalcond of condition * P.t list * node * node * bool option - -(** Record used during the "dynamic" value numbering *) - -type numb = { - mutable nnext : int; (** Next unusued value number *) - mutable seqs : seq list; (** equations *) - mutable nreg : (P.t, int) Hashtbl.t; (** mapping registers to values *) - mutable nval : (int, P.t list) Hashtbl.t; - (** reverse mapping values to registers containing it *) -} - -let print_list_pos l = - debug "["; - List.iter (fun i -> debug "%d;" (p2i i)) l; - debug "]\n" - -let empty_numbering () = - { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 } - -let rec get_nvalues vn = function - | [] -> [] - | r :: rs -> - let v = - match Hashtbl.find_opt !vn.nreg r with - | Some v -> - debug "getnval r=%d |-> v=%d\n" (p2i r) v; - v - | None -> - let n = !vn.nnext in - debug "getnval r=%d |-> v=%d\n" (p2i r) n; - !vn.nnext <- !vn.nnext + 1; - Hashtbl.replace !vn.nreg r n; - Hashtbl.replace !vn.nval n [ r ]; - n - in - let vs = get_nvalues vn rs in - v :: vs - -let get_nval_ornil vn v = - match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l - -let forget_reg vn rd = - match Hashtbl.find_opt !vn.nreg rd with - | Some v -> - debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; - let old_regs = get_nval_ornil vn v in - debug "forget_reg: old_regs are:\n"; - print_list_pos old_regs; - Hashtbl.replace !vn.nval v - (List.filter (fun n -> not (P.eq n rd)) old_regs) - | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd) - -let update_reg vn rd v = - debug "update_reg: update v=%d with r=%d\n" v (p2i rd); - forget_reg vn rd; - let old_regs = get_nval_ornil vn v in - Hashtbl.replace !vn.nval v (rd :: old_regs) - -let rec find_valnum_rhs rh = function - | [] -> None - | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl - -let set_unknown vn rd = - debug "set_unknown: rd=%d\n" (p2i rd); - forget_reg vn rd; - Hashtbl.remove !vn.nreg rd - -let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> () - -let addrhs vn rd rh = - match find_valnum_rhs rh !vn.seqs with - | Some vres -> - debug "addrhs: Some v=%d\n" vres; - Hashtbl.replace !vn.nreg rd vres; - update_reg vn rd vres - | None -> - let n = !vn.nnext in - debug "addrhs: None v=%d\n" n; - !vn.nnext <- !vn.nnext + 1; - !vn.seqs <- Seq (n, rh) :: !vn.seqs; - update_reg vn rd n; - Hashtbl.replace !vn.nreg rd n - -let addsop vn v op rd = - debug "addsop\n"; - if op = Omove then ( - update_reg vn rd (List.hd v); - Hashtbl.replace !vn.nreg rd (List.hd v)) - else addrhs vn rd (Sop (op, v)) - -let rec kill_mem_operations = function - | (Seq (v, Sop (op, vl)) as eq) :: tl -> - if op_depends_on_memory op then kill_mem_operations tl - else eq :: kill_mem_operations tl - | [] -> [] - | eq :: tl -> eq :: kill_mem_operations tl - -let reg_valnum vn v = - debug "reg_valnum: trying to find a mapping for v=%d\n" v; - match Hashtbl.find !vn.nval v with - | [] -> None - | r :: rs -> - debug "reg_valnum: found a mapping r=%d\n" (p2i r); - Some r - -let rec reg_valnums vn = function - | [] -> Some [] - | v :: vs -> ( - match (reg_valnum vn v, reg_valnums vn vs) with - | Some r, Some rs -> Some (r :: rs) - | _, _ -> None) - -let find_rhs vn rh = - match find_valnum_rhs rh !vn.seqs with - | None -> None - | Some vres -> reg_valnum vn vres - -(** Functions to perform the dynamic reduction during CSE *) - -let extract_arg l = - if List.length l > 0 then - match List.hd l with - | Sr r -> (r, List.tl l) - | Sexp (rd, _, _, _) -> (rd, l) - | _ -> failwith "extract_arg: final instruction arg can not be extracted" - else failwith "extract_arg: trying to extract on an empty list" - -let extract_final vn fl fdest succ = - if List.length fl > 0 then - match List.hd fl with - | Sr r -> - if not (P.eq r fdest) then ( - let v = get_nvalues vn [ r ] in - addsop vn v Omove fdest; - Sexp (fdest, Smove, [ r ], Some succ) :: List.tl fl) - else Snop succ :: List.tl fl - | Sexp (rd, rh, args, None) -> - assert (rd = fdest); - Sexp (fdest, rh, args, Some succ) :: List.tl fl - | _ -> fl - else failwith "extract_final: trying to extract on an empty list" - -let addinst vn op args rd = - let v = get_nvalues vn args in - let rh = Sop (op, v) in - match find_rhs vn rh with - | Some r -> - debug "addinst: rhs found with r=%d\n" (p2i r); - Sr r - | None -> - addsop vn v op rd; - Sexp (rd, rh, args, None) - -(** Expansion functions *) - -type immt = - | Addiw - | Addil - | Andiw - | Andil - | Oriw - | Oril - | Xoriw - | Xoril - | Sltiw - | Sltiuw - | Sltil - | Sltiul - -let load_hilo32 vn dest hi lo = - let op1 = OEluiw hi in - if Int.eq lo Int.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddiw (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let load_hilo64 vn dest hi lo = - let op1 = OEluil hi in - if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddil (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let loadimm32 vn dest n = - match make_immed32 n with - | Imm32_single imm -> - let op1 = OEaddiw (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo - -let loadimm64 vn dest n = - match make_immed64 n with - | Imm64_single imm -> - let op1 = OEaddil (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo - | Imm64_large imm -> - let op1 = OEloadli imm in - [ addinst vn op1 [] dest ] - -let get_opimm optR imm = function - | Addiw -> OEaddiw (optR, imm) - | Andiw -> OEandiw imm - | Oriw -> OEoriw imm - | Xoriw -> OExoriw imm - | Sltiw -> OEsltiw imm - | Sltiuw -> OEsltiuw imm - | Addil -> OEaddil (optR, imm) - | Andil -> OEandil imm - | Oril -> OEoril imm - | Xoril -> OExoril imm - | Sltil -> OEsltil imm - | Sltiul -> OEsltiul imm - -let opimm32 vn a1 dest n optR op opimm = - match make_immed32 n with - | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm32_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - -let opimm64 vn a1 dest n optR op opimm = - match make_immed64 n with - | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm64_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - | Imm64_large imm -> - let r = r2pi () in - let op1 = OEloadli imm in - let i1 = addinst vn op1 [] r in - let r', l' = extract_arg [ i1 ] in - let i2 = addinst vn op [ a1; r' ] dest in - i2 :: l' - -let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw - -let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw - -let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw - -let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw - -let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw - -let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw - -let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil - -let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil - -let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril - -let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril - -let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil - -let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul - -let is_inv_cmp = function Cle | Cgt -> true | _ -> false - -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 optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cond_int32s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int32u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let is_normal_cmp = function Cne -> false | _ -> true - -let cond_float vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ] - -let cond_single vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] - -let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32u false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64u false cmp a1 r' info succ1 succ2 l' - -let expanse_condimm_int32s vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm32 vn a1 r n in - let r', l' = extract_arg l in - cond_int32s vn true cmp r' r' dest @ l' - | Clt -> sltimm32 vn a1 dest n - | Cle -> - if Int.eq n (Int.repr Int.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUint) [ a1; r ] dest :: l' - else sltimm32 vn a1 dest (Int.add n Int.one) - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int32u vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm32 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32u vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64s vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm64 vn a1 r n in - let r', l' = extract_arg l in - cond_int64s vn true cmp r' r' dest @ l' - | Clt -> sltimm64 vn a1 dest n - | Cle -> - if Int64.eq n (Int64.repr Int64.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l' - else sltimm64 vn a1 dest (Int64.add n Int64.one) - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64u vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm64 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64u vn false cmp a1 r' dest @ l' - -let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = - let normal = is_normal_cmp cmp in - let normal' = if cnot then not normal else normal in - let insn = fn_cond vn cmp f1 f2 dest in - if normal' then insn - else - let r', l = extract_arg insn in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 = - 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 vn cmp f1 f2 r in - let r', l = extract_arg insn in - if normal' then - Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - -(** Form a list containing both sources and destination regs of an instruction *) - -let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] - -let get_regs_inst = function - | Inop _ -> [] - | Iop (_, args, dest, _) -> dest :: args - | Iload (_, _, _, args, dest, _) -> dest :: args - | Istore (_, _, args, src, _) -> src :: args - | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args) - | Itailcall (_, t, args) -> get_regindent t @ args - | Ibuiltin (_, args, dest, _) -> - AST.params_of_builtin_res dest @ AST.params_of_builtin_args args - | Icond (_, args, _, _, _) -> args - | Ijumptable (arg, _) -> [ arg ] - | Ireturn (Some r) -> [ r ] - | _ -> [] - -(** Modify pathmap according to the size of the expansion list *) - -let write_pathmap initial esize pm' = - debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; - let path = get_some @@ PTree.get initial !pm' in - let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in - let path' = - { - psize = npsize; - input_regs = path.input_regs; - pre_output_regs = path.pre_output_regs; - output_regs = path.output_regs; - } - in - pm' := PTree.set initial path' !pm' - -(** Write a single instruction in the tree and update order *) - -let write_inst target_node inst code' new_order = - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order - -(** Return olds args if the CSE numbering is empty *) - -let get_arguments vn vals args = - match reg_valnums vn vals with Some args' -> args' | None -> args - -(** Update the code tree with the expansion list *) - -let rec write_tree vn exp initial current code' new_order fturn = - debug "wt: node is %d\n" !node; - let target_node, next_node = - if fturn then (P.to_int initial, current) else (current, current - 1) - in - match exp with - | Sr r :: _ -> - failwith "write_tree: there are still some symbolic values in the list" - | Sexp (rd, Sop (op, vals), args, None) :: k -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, P.of_int next_node) in - write_inst target_node inst code' new_order; - write_tree vn k initial next_node code' new_order false - | [ Snop succ ] -> - let inst = Inop succ in - write_inst target_node inst code' new_order - | [ Sexp (rd, Sop (op, vals), args, Some succ) ] -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sexp (rd, Smove, args, Some succ) ] -> - let inst = Iop (Omove, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sfinalcond (cond, args, succ1, succ2, info) ] -> - let inst = Icond (cond, args, succ1, succ2, info) in - write_inst target_node inst code' new_order - | [] -> () - | _ -> failwith "write_tree: invalid list" - -(** Main expansion function - TODO gourdinl to split? *) -let expanse (sb : superblock) code pm = - debug "#### New superblock for expansion oracle\n"; - let new_order = ref [] in - let liveins = ref sb.liveins in - let exp = ref [] in - let was_branch = ref false in - let was_exp = ref false in - let code' = ref code in - let pm' = ref pm in - let vn = ref (empty_numbering ()) in - Array.iter - (fun n -> - was_branch := false; - was_exp := false; - let inst = get_some @@ PTree.get n code in - (if !Clflags.option_fexpanse_rtlcond then - match inst with - (* Expansion of conditions - Ocmp *) - | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomp\n"; - exp := cond_int32s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompu\n"; - exp := cond_int32u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompl\n"; - exp := cond_int64s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomplu\n"; - exp := cond_int64u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompf\n"; - exp := expanse_cond_fp vn false cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompf\n"; - exp := expanse_cond_fp vn true cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompfs\n"; - exp := expanse_cond_fp vn false cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp vn true cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - (* Expansion of branches - Ccomp *) - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomp\n"; - exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompu\n"; - exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompimm\n"; - exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompuimm\n"; - exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompl\n"; - exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplu\n"; - exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplimm\n"; - exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompluimm\n"; - exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompf\n"; - exp := - expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompf\n"; - exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompfs\n"; - exp := - expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompfs\n"; - exp := - expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | _ -> ()); - (if !Clflags.option_fexpanse_others && not !was_exp then - match inst with - | Iop (Ofloatconst f, nil, dest, succ) -> ( - match make_immed64 (Floats.Float.to_bits f) with - | Imm64_single _ | Imm64_large _ -> () - | Imm64_pair (hi, lo) -> - debug "Iop/Ofloatconst\n"; - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Osingleconst f, nil, dest, succ) -> ( - match make_immed32 (Floats.Float32.to_bits f) with - | Imm32_single imm -> () - | Imm32_pair (hi, lo) -> - debug "Iop/Osingleconst\n"; - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Ointconst n, nil, dest, succ) -> - debug "Iop/Ointconst\n"; - exp := loadimm32 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Olongconst n, nil, dest, succ) -> - debug "Iop/Olongconst\n"; - exp := loadimm64 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddimm\n"; - exp := addimm32 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddlimm\n"; - exp := addimm64 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandimm\n"; - exp := andimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandlimm\n"; - exp := andimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorimm\n"; - exp := orimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorlimm\n"; - exp := orimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorimm\n"; - exp := xorimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorlimm\n"; - exp := xorimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - debug "Iop/cast8signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 24)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast16signed, a1 :: nil, dest, succ) -> - debug "Iop/cast16signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 16)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> - debug "Iop/Ocast32unsigned\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Ocast32signed in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in - exp := addinst vn op3 [ r2' ] dest :: l2; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrximm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrximm1\n"; - exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrximm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oadd in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrximm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshruimm (Int.sub Int.iwordsize n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oadd in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrxlimm1\n"; - exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrxlimm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oaddl in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrlimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrxlimm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oaddl in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrlimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | _ -> ()); - (* Update the CSE numbering *) - (if not !was_exp then - match inst with - | Iop (op, args, dest, succ) -> - let v = get_nvalues vn args in - addsop vn v op dest - | Iload (_, _, _, _, dst, _) -> set_unknown vn dst - | Istore (chk, addr, args, src, s) -> - !vn.seqs <- kill_mem_operations !vn.seqs - | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) -> - vn := empty_numbering () - | _ -> ()); - (* Update code, liveins, pathmap, and order of the superblock for one expansion *) - if !was_exp then ( - (if !was_branch && List.length !exp > 1 then - let lives = PTree.get n !liveins in - match lives with - | Some lives -> - let new_branch_pc = P.of_int (!node + 1) in - liveins := PTree.set new_branch_pc lives !liveins; - liveins := PTree.remove n !liveins - | _ -> ()); - node := !node + List.length !exp - 1; - write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree vn (List.rev !exp) n !node code' new_order true) - else new_order := n :: !new_order) - sb.instructions; - sb.instructions <- Array.of_list (List.rev !new_order); - sb.liveins <- !liveins; - (!code', !pm') - -(** Compute the last used node and reg indexs *) - -let rec find_last_node_reg = function - | [] -> () - | (pc, i) :: k -> - let rec traverse_list var = function - | [] -> () - | e :: t -> - let e' = p2i e in - if e' > !var then var := e'; - traverse_list var t - in - traverse_list node [ pc ]; - traverse_list reg (get_regs_inst i); - find_last_node_reg k +let find_last_node_reg c = () -- cgit From 23c01485970efa11a7207ac2124f5922a011b0d4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 20:01:12 +0200 Subject: new expansion oracle for BTL --- riscV/ExpansionOracle.ml | 330 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 328 insertions(+), 2 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 0869007c..7950cb6a 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -10,6 +10,332 @@ (* *) (* *************************************************************) -let expanse n ibf btl = btl +open BTL +open Op +open! Integers +open Camlcoq +open DebugPrint +open RTLcommonaux +open BTLcommonaux +open AST +open Datatypes +open Maps -let find_last_node_reg c = () +(** Tools *) + +(** TODO gourdinl move to BTLcommonaux *) +let rec iblock_to_list ib = + match ib with + | Bseq (ib1, ib2) -> iblock_to_list ib1 @ iblock_to_list ib2 + | _ -> [ ib ] + +let rec list_to_iblock lib = + match lib with + | i1 :: k -> + if List.length lib > 1 then + Bseq (i1, list_to_iblock k) + else i1 + | [] -> failwith "list_to_iblock: called on empty list" + +(** Mini CSE (a dynamic numbering is applied during expansion. + The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) + +(** Managing virtual registers and node index *) + +let reg = ref 1 + +let r2p () = P.of_int !reg + +let r2pi () = + reg := !reg + 1; + r2p () + +(** Below are the types for rhs and equations *) + +type rhs = Sop of operation * int list | Smove + +type seq = Seq of int * rhs + +(** This is a mini abstraction to have a simpler representation during expansion + - (Sr r) is inserted if the value was found in register r + - (Sexp dest rhs args iinfo) represent an instruction + - (Scond cond args ib1 ib2 iinfo) represents a condition +*) + +type expl = + | Sr of P.t + | Sexp of P.t * rhs * P.t list * inst_info + | Scond of condition * P.t list * iblock * iblock * inst_info + +(** Record used during the "dynamic" value numbering *) + +type numb = { + mutable nnext : int; (** Next unusued value number *) + mutable seqs : seq list; (** equations *) + mutable nreg : (P.t, int) Hashtbl.t; (** mapping registers to values *) + mutable nval : (int, P.t list) Hashtbl.t; + (** reverse mapping values to registers containing it *) +} + +let print_list_pos l = + debug "["; + List.iter (fun i -> debug "%d;" (p2i i)) l; + debug "]\n" + +let empty_numbering () = + { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 } + +let rec get_nvalues vn = function + | [] -> [] + | r :: rs -> + let v = + match Hashtbl.find_opt !vn.nreg r with + | Some v -> + debug "getnval r=%d |-> v=%d\n" (p2i r) v; + v + | None -> + let n = !vn.nnext in + debug "getnval r=%d |-> v=%d\n" (p2i r) n; + !vn.nnext <- !vn.nnext + 1; + Hashtbl.replace !vn.nreg r n; + Hashtbl.replace !vn.nval n [ r ]; + n + in + let vs = get_nvalues vn rs in + v :: vs + +let get_nval_ornil vn v = + match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l + +let forget_reg vn rd = + match Hashtbl.find_opt !vn.nreg rd with + | Some v -> + debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; + let old_regs = get_nval_ornil vn v in + debug "forget_reg: old_regs are:\n"; + print_list_pos old_regs; + Hashtbl.replace !vn.nval v + (List.filter (fun n -> not (P.eq n rd)) old_regs) + | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd) + +let update_reg vn rd v = + debug "update_reg: update v=%d with r=%d\n" v (p2i rd); + forget_reg vn rd; + let old_regs = get_nval_ornil vn v in + Hashtbl.replace !vn.nval v (rd :: old_regs) + +let rec find_valnum_rhs rh = function + | [] -> None + | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl + +let set_unknown vn rd = + debug "set_unknown: rd=%d\n" (p2i rd); + forget_reg vn rd; + Hashtbl.remove !vn.nreg rd + +let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> () + +let addrhs vn rd rh = + match find_valnum_rhs rh !vn.seqs with + | Some vres -> + debug "addrhs: Some v=%d\n" vres; + Hashtbl.replace !vn.nreg rd vres; + update_reg vn rd vres + | None -> + let n = !vn.nnext in + debug "addrhs: None v=%d\n" n; + !vn.nnext <- !vn.nnext + 1; + !vn.seqs <- Seq (n, rh) :: !vn.seqs; + update_reg vn rd n; + Hashtbl.replace !vn.nreg rd n + +let addsop vn v op rd = + debug "addsop\n"; + if op = Omove then ( + update_reg vn rd (List.hd v); + Hashtbl.replace !vn.nreg rd (List.hd v)) + else addrhs vn rd (Sop (op, v)) + +let rec kill_mem_operations = function + | (Seq (v, Sop (op, vl)) as eq) :: tl -> + if op_depends_on_memory op then kill_mem_operations tl + else eq :: kill_mem_operations tl + | [] -> [] + | eq :: tl -> eq :: kill_mem_operations tl + +let reg_valnum vn v = + debug "reg_valnum: trying to find a mapping for v=%d\n" v; + match Hashtbl.find !vn.nval v with + | [] -> None + | r :: rs -> + debug "reg_valnum: found a mapping r=%d\n" (p2i r); + Some r + +let rec reg_valnums vn = function + | [] -> Some [] + | v :: vs -> ( + match (reg_valnum vn v, reg_valnums vn vs) with + | Some r, Some rs -> Some (r :: rs) + | _, _ -> None) + +let find_rhs vn rh = + match find_valnum_rhs rh !vn.seqs with + | None -> None + | Some vres -> reg_valnum vn vres + +(** Functions to perform the dynamic reduction during CSE *) + +let extract_arg l = + if List.length l > 0 then + match List.hd l with + | Sr r -> (r, List.tl l) + | Sexp (rd, _, _, _) -> (rd, l) + | _ -> failwith "extract_arg: final instruction arg can not be extracted" + else failwith "extract_arg: trying to extract on an empty list" + +let extract_final vn fl fdest = + if List.length fl > 0 then + match List.hd fl with + | Sr r -> + if not (P.eq r fdest) then ( + let v = get_nvalues vn [ r ] in + addsop vn v Omove fdest; + Sexp (fdest, Smove, [ r ], def_iinfo ()) :: List.tl fl) + else List.tl fl + | _ -> fl + else failwith "extract_final: trying to extract on an empty list" + +let addinst vn op args rd iinfo = + let v = get_nvalues vn args in + let rh = Sop (op, v) in + match find_rhs vn rh with + | Some r -> + debug "addinst: rhs found with r=%d\n" (p2i r); + Sr r + | None -> + addsop vn v op rd; + Sexp (rd, rh, args, iinfo) + +(** Expansion functions *) + +let is_inv_cmp = function Cle | Cgt -> true | _ -> false + +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 cond_int32s vn is_x0 cmp a1 a2 dest iinfo = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest iinfo ] + | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest iinfo ] + | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest iinfo ] + | Cle -> + let r = r2pi () in + let op = OEsltw optR in + let i1 = addinst vn op [ a2; a1 ] r iinfo in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l + | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest iinfo ] + | Cge -> + let r = r2pi () in + let op = OEsltw optR in + let i1 = addinst vn op [ a1; a2 ] r iinfo in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l + +(** Return olds args if the CSE numbering is empty *) + +let get_arguments vn vals args = + match reg_valnums vn vals with Some args' -> args' | None -> args + +let rec gen_btl_list vn exp = + match exp with + | Sr r :: _ -> + failwith "write_tree: there are still some symbolic values in the list" + | Sexp (rd, Sop (op, vals), args, iinfo) :: k -> + let args = get_arguments vn vals args in + let inst = Bop (op, args, rd, iinfo) in + inst :: gen_btl_list vn k + | [ Sexp (rd, Smove, args, iinfo) ] -> + [ Bop (Omove, args, rd, iinfo) ] + | [ Scond (cond, args, succ1, succ2, iinfo) ] -> + [ Bcond (cond, args, succ1, succ2, iinfo) ] + | [] -> [] + | _ -> failwith "write_tree: invalid list" + +let expanse_list li = + debug "#### New block for expansion oracle\n"; + let exp = ref [] in + let was_exp = ref false in + let vn = ref (empty_numbering ()) in + let rec expanse_list_rec li = + match li with + | [] -> li + | i :: li' -> + was_exp := false; + (if !Clflags.option_fexpanse_rtlcond then + match i with + | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccomp\n"; + exp := cond_int32s vn false c a1 a2 dest iinfo; + exp := extract_final vn !exp dest; + was_exp := true + | _ -> ()); + if not !was_exp then ( + (match i with + | Bop (op, args, dest, iinfo) -> + let v = get_nvalues vn args in + addsop vn v op dest + | Bload (_, _, _, _, dst, _) -> set_unknown vn dst + | Bstore (_, _, _, _, _) -> + !vn.seqs <- kill_mem_operations !vn.seqs + (* TODO gourdinl empty numb BF? vn := empty_numbering ()*) + | _ -> ()); + i :: expanse_list_rec li') + else + gen_btl_list vn !exp @ expanse_list_rec li' + in + expanse_list_rec li + +let expanse n ibf btl = + debug_flag := true; + let lib = iblock_to_list ibf.entry in + let new_lib = expanse_list lib in + let ibf' = { entry = list_to_iblock new_lib; + input_regs = ibf.input_regs; + binfo = ibf.binfo } in + debug_flag := false; + PTree.set n ibf' btl + +(** Form a list containing both sources and destination regs of a block *) +let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] + +let rec get_regs_ib = function + | Bnop _ -> [] + | Bop (_, args, dest, _) -> dest :: args + | Bload (_, _, _, args, dest, _) -> dest :: args + | Bstore (_, _, args, src, _) -> src :: args + | Bcond (_, args, ib1, ib2, _) -> + get_regs_ib ib1 @ get_regs_ib ib2 @ args + | Bseq (ib1, ib2) -> + get_regs_ib ib1 @ get_regs_ib ib2 + | BF (Breturn (Some r), _) -> [r] + | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args) + | BF (Btailcall (_, t, args), _) -> (get_regindent t @ args) + | BF (Bbuiltin (_, args, dest, _), _) -> + AST.params_of_builtin_res dest @ AST.params_of_builtin_args args + | BF (Bjumptable (arg, _), _) -> [arg] + | _ -> [] + +let rec find_last_reg = function + | [] -> () + | (pc, ibf) :: k -> + let rec traverse_list var = function + | [] -> () + | e :: t -> + let e' = p2i e in + if e' > !var then var := e'; + traverse_list var t + in + traverse_list reg (get_regs_ib ibf.entry); + find_last_reg k -- cgit From 8663f220ec0b0f10e74ae7442cdf221a83fc3943 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 22:16:11 +0200 Subject: bug fix in oracle --- riscV/ExpansionOracle.ml | 393 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 360 insertions(+), 33 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 7950cb6a..c1cf5c9c 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -20,6 +20,7 @@ open BTLcommonaux open AST open Datatypes open Maps +open Asmgen (** Tools *) @@ -31,10 +32,7 @@ let rec iblock_to_list ib = let rec list_to_iblock lib = match lib with - | i1 :: k -> - if List.length lib > 1 then - Bseq (i1, list_to_iblock k) - else i1 + | i1 :: k -> if List.length lib > 1 then Bseq (i1, list_to_iblock k) else i1 | [] -> failwith "list_to_iblock: called on empty list" (** Mini CSE (a dynamic numbering is applied during expansion. @@ -205,7 +203,7 @@ let extract_final vn fl fdest = | _ -> fl else failwith "extract_final: trying to extract on an empty list" -let addinst vn op args rd iinfo = +let addinst vn op args rd = let v = get_nvalues vn args in let rh = Sop (op, v) in match find_rhs vn rh with @@ -214,34 +212,308 @@ let addinst vn op args rd iinfo = Sr r | None -> addsop vn v op rd; - Sexp (rd, rh, args, iinfo) + Sexp (rd, rh, args, def_iinfo ()) (** Expansion functions *) +type immt = + | Addiw + | Addil + | Andiw + | Andil + | Oriw + | Oril + | Xoriw + | Xoril + | Sltiw + | Sltiuw + | Sltil + | Sltiul + +let load_hilo32 vn dest hi lo = + let op1 = OEluiw hi in + if Int.eq lo Int.zero then [ addinst vn op1 [] dest ] + else + let r = r2pi () in + let op2 = OEaddiw (None, lo) in + let i1 = addinst vn op1 [] r in + let r', l = extract_arg [ i1 ] in + let i2 = addinst vn op2 [ r' ] dest in + i2 :: l + +let load_hilo64 vn dest hi lo = + let op1 = OEluil hi in + if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ] + else + let r = r2pi () in + let op2 = OEaddil (None, lo) in + let i1 = addinst vn op1 [] r in + let r', l = extract_arg [ i1 ] in + let i2 = addinst vn op2 [ r' ] dest in + i2 :: l + +let loadimm32 vn dest n = + match make_immed32 n with + | Imm32_single imm -> + let op1 = OEaddiw (Some X0_R, imm) in + [ addinst vn op1 [] dest ] + | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo + +let loadimm64 vn dest n = + match make_immed64 n with + | Imm64_single imm -> + let op1 = OEaddil (Some X0_R, imm) in + [ addinst vn op1 [] dest ] + | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo + | Imm64_large imm -> + let op1 = OEloadli imm in + [ addinst vn op1 [] dest ] + +let get_opimm optR imm = function + | Addiw -> OEaddiw (optR, imm) + | Andiw -> OEandiw imm + | Oriw -> OEoriw imm + | Xoriw -> OExoriw imm + | Sltiw -> OEsltiw imm + | Sltiuw -> OEsltiuw imm + | Addil -> OEaddil (optR, imm) + | Andil -> OEandil imm + | Oril -> OEoril imm + | Xoril -> OExoril imm + | Sltil -> OEsltil imm + | Sltiul -> OEsltiul imm + +let opimm32 vn a1 dest n optR op opimm = + match make_immed32 n with + | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] + | Imm32_pair (hi, lo) -> + let r = r2pi () in + let l = load_hilo32 vn r hi lo in + let r', l' = extract_arg l in + let i = addinst vn op [ a1; r' ] dest in + i :: l' + +let opimm64 vn a1 dest n optR op opimm = + match make_immed64 n with + | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] + | Imm64_pair (hi, lo) -> + let r = r2pi () in + let l = load_hilo64 vn r hi lo in + let r', l' = extract_arg l in + let i = addinst vn op [ a1; r' ] dest in + i :: l' + | Imm64_large imm -> + let r = r2pi () in + let op1 = OEloadli imm in + let i1 = addinst vn op1 [] r in + let r', l' = extract_arg [ i1 ] in + let i2 = addinst vn op [ a1; r' ] dest in + i2 :: l' + +let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw + +let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw + +let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw + +let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw + +let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw + +let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw + +let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil + +let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil + +let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril + +let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril + +let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil + +let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul + let is_inv_cmp = function Cle | Cgt -> true | _ -> false 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 cond_int32s vn is_x0 cmp a1 a2 dest iinfo = +let cond_int32s vn is_x0 cmp a1 a2 dest = let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest iinfo ] - | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest iinfo ] - | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest iinfo ] + | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ] + | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ] + | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ] | Cle -> let r = r2pi () in let op = OEsltw optR in - let i1 = addinst vn op [ a2; a1 ] r iinfo in + let i1 = addinst vn op [ a2; a1 ] r in let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l - | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest iinfo ] + addinst vn (OExoriw Int.one) [ r' ] dest :: l + | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ] | Cge -> let r = r2pi () in let op = OEsltw optR in - let i1 = addinst vn op [ a1; a2 ] r iinfo in + let i1 = addinst vn op [ a1; a2 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + +let cond_int32u vn is_x0 cmp a1 a2 dest = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ] + | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ] + | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ] + | Cle -> + let r = r2pi () in + let op = OEsltuw optR in + let i1 = addinst vn op [ a2; a1 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ] + | Cge -> + let r = r2pi () in + let op = OEsltuw optR in + let i1 = addinst vn op [ a1; a2 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + +let cond_int64s vn is_x0 cmp a1 a2 dest = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ] + | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ] + | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ] + | Cle -> + let r = r2pi () in + let op = OEsltl optR in + let i1 = addinst vn op [ a2; a1 ] r in let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l + addinst vn (OExoriw Int.one) [ r' ] dest :: l + | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ] + | Cge -> + let r = r2pi () in + let op = OEsltl optR in + let i1 = addinst vn op [ a1; a2 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + +let cond_int64u vn is_x0 cmp a1 a2 dest = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ] + | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ] + | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ] + | Cle -> + let r = r2pi () in + let op = OEsltul optR in + let i1 = addinst vn op [ a2; a1 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ] + | Cge -> + let r = r2pi () in + let op = OEsltul optR in + let i1 = addinst vn op [ a1; a2 ] r in + let r', l = extract_arg [ i1 ] in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + +let is_normal_cmp = function Cne -> false | _ -> true + +let cond_float vn cmp f1 f2 dest = + match cmp with + | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ] + | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ] + | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ] + | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ] + | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ] + | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ] + +let cond_single vn cmp f1 f2 dest = + match cmp with + | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ] + | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ] + | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ] + | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ] + | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] + | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] + +let expanse_condimm_int32s vn cmp a1 n dest = + if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest + else + match cmp with + | Ceq | Cne -> + let r = r2pi () in + let l = xorimm32 vn a1 r n in + let r', l' = extract_arg l in + cond_int32s vn true cmp r' r' dest @ l' + | Clt -> sltimm32 vn a1 dest n + | Cle -> + if Int.eq n (Int.repr Int.max_signed) then + let l = loadimm32 vn dest Int.one in + let r, l' = extract_arg l in + addinst vn (OEmayundef MUint) [ a1; r ] dest :: l' + else sltimm32 vn a1 dest (Int.add n Int.one) + | _ -> + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cond_int32s vn false cmp a1 r' dest @ l' + +let expanse_condimm_int32u vn cmp a1 n dest = + if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest + else + match cmp with + | Clt -> sltuimm32 vn a1 dest n + | _ -> + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cond_int32u vn false cmp a1 r' dest @ l' + +let expanse_condimm_int64s vn cmp a1 n dest = + if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest + else + match cmp with + | Ceq | Cne -> + let r = r2pi () in + let l = xorimm64 vn a1 r n in + let r', l' = extract_arg l in + cond_int64s vn true cmp r' r' dest @ l' + | Clt -> sltimm64 vn a1 dest n + | Cle -> + if Int64.eq n (Int64.repr Int64.max_signed) then + let l = loadimm32 vn dest Int.one in + let r, l' = extract_arg l in + addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l' + else sltimm64 vn a1 dest (Int64.add n Int64.one) + | _ -> + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cond_int64s vn false cmp a1 r' dest @ l' + +let expanse_condimm_int64u vn cmp a1 n dest = + if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest + else + match cmp with + | Clt -> sltuimm64 vn a1 dest n + | _ -> + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cond_int64u vn false cmp a1 r' dest @ l' + +let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = + let normal = is_normal_cmp cmp in + let normal' = if cnot then not normal else normal in + let insn = fn_cond vn cmp f1 f2 dest in + if normal' then insn + else + let r', l = extract_arg insn in + addinst vn (OExoriw Int.one) [ r' ] dest :: l + (** Return olds args if the CSE numbering is empty *) @@ -256,8 +528,7 @@ let rec gen_btl_list vn exp = let args = get_arguments vn vals args in let inst = Bop (op, args, rd, iinfo) in inst :: gen_btl_list vn k - | [ Sexp (rd, Smove, args, iinfo) ] -> - [ Bop (Omove, args, rd, iinfo) ] + | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ] | [ Scond (cond, args, succ1, succ2, iinfo) ] -> [ Bcond (cond, args, succ1, succ2, iinfo) ] | [] -> [] @@ -277,7 +548,62 @@ let expanse_list li = match i with | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) -> debug "Bop/Ccomp\n"; - exp := cond_int32s vn false c a1 a2 dest iinfo; + exp := cond_int32s vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccompu\n"; + exp := cond_int32u vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompimm\n"; + exp := expanse_condimm_int32s vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompuimm\n"; + exp := expanse_condimm_int32u vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccompl\n"; + exp := cond_int64s vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccomplu\n"; + exp := cond_int64u vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccomplimm\n"; + exp := expanse_condimm_int64s vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompluimm\n"; + exp := expanse_condimm_int64u vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Ccompf\n"; + exp := expanse_cond_fp vn false cond_float c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Cnotcompf\n"; + exp := expanse_cond_fp vn true cond_float c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Ccompfs\n"; + exp := expanse_cond_fp vn false cond_single c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Cnotcompfs\n"; + exp := expanse_cond_fp vn true cond_single c f1 f2 dest; exp := extract_final vn !exp dest; was_exp := true | _ -> ()); @@ -292,19 +618,22 @@ let expanse_list li = (* TODO gourdinl empty numb BF? vn := empty_numbering ()*) | _ -> ()); i :: expanse_list_rec li') - else - gen_btl_list vn !exp @ expanse_list_rec li' + else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li' in expanse_list_rec li let expanse n ibf btl = - debug_flag := true; + (*debug_flag := true;*) let lib = iblock_to_list ibf.entry in let new_lib = expanse_list lib in - let ibf' = { entry = list_to_iblock new_lib; - input_regs = ibf.input_regs; - binfo = ibf.binfo } in - debug_flag := false; + let ibf' = + { + entry = list_to_iblock new_lib; + input_regs = ibf.input_regs; + binfo = ibf.binfo; + } + in + (*debug_flag := false;*) PTree.set n ibf' btl (** Form a list containing both sources and destination regs of a block *) @@ -315,16 +644,14 @@ let rec get_regs_ib = function | Bop (_, args, dest, _) -> dest :: args | Bload (_, _, _, args, dest, _) -> dest :: args | Bstore (_, _, args, src, _) -> src :: args - | Bcond (_, args, ib1, ib2, _) -> - get_regs_ib ib1 @ get_regs_ib ib2 @ args - | Bseq (ib1, ib2) -> - get_regs_ib ib1 @ get_regs_ib ib2 - | BF (Breturn (Some r), _) -> [r] + | Bcond (_, args, ib1, ib2, _) -> get_regs_ib ib1 @ get_regs_ib ib2 @ args + | Bseq (ib1, ib2) -> get_regs_ib ib1 @ get_regs_ib ib2 + | BF (Breturn (Some r), _) -> [ r ] | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args) - | BF (Btailcall (_, t, args), _) -> (get_regindent t @ args) - | BF (Bbuiltin (_, args, dest, _), _) -> + | BF (Btailcall (_, t, args), _) -> get_regindent t @ args + | BF (Bbuiltin (_, args, dest, _), _) -> AST.params_of_builtin_res dest @ AST.params_of_builtin_args args - | BF (Bjumptable (arg, _), _) -> [arg] + | BF (Bjumptable (arg, _), _) -> [ arg ] | _ -> [] let rec find_last_reg = function -- cgit From 9ce1b23f6361d8070490df1269a7bc53aa215efb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 12:16:27 +0200 Subject: expansions btl proofs --- riscV/BTL_SEsimplify.v | 999 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 998 insertions(+), 1 deletion(-) mode change 120000 => 100644 riscV/BTL_SEsimplify.v (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v deleted file mode 120000 index f190e6d5..00000000 --- a/riscV/BTL_SEsimplify.v +++ /dev/null @@ -1 +0,0 @@ -../aarch64/BTL_SEsimplify.v \ No newline at end of file diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v new file mode 100644 index 00000000..a4a2785a --- /dev/null +++ b/riscV/BTL_SEsimplify.v @@ -0,0 +1,998 @@ +Require Import Coqlib Floats Values Memory. +Require Import Integers. +Require Import Op Registers. +Require Import BTL_SEtheory. +Require Import BTL_SEsimuref. +Require Import Asmgen Asmgenproof1. + +(** Useful functions for conditions/branches expansion *) + +Definition is_inv_cmp_int (cmp: comparison) : bool := + match cmp with | Cle | Cgt => true | _ => false end. + +Definition is_inv_cmp_float (cmp: comparison) : bool := + match cmp with | Cge | Cgt => true | _ => false end. + +Definition make_optR (is_x0 is_inv: bool) : option oreg := + if is_x0 then + (if is_inv then Some (X0_L) + else Some (X0_R)) + else None. + +(** Functions to manage lists of "fake" values *) + +Definition make_lfsv_cmp (is_inv: bool) (fsv1 fsv2: sval) : list_sval := + let (fsvfirst, fsvsec) := if is_inv then (fsv1, fsv2) else (fsv2, fsv1) in + let lfsv := fScons fsvfirst fSnil in + fScons fsvsec lfsv. + +Definition make_lfsv_single (fsv: sval) : list_sval := + fScons fsv fSnil. + +(** * Expansion functions *) + +(** ** Immediate loads *) + +Definition load_hilo32 (hi lo: int) := + if Int.eq lo Int.zero then + fSop (OEluiw hi) fSnil + else + let fsv := fSop (OEluiw hi) fSnil in + let hl := make_lfsv_single fsv in + fSop (OEaddiw None lo) hl. + +Definition load_hilo64 (hi lo: int64) := + if Int64.eq lo Int64.zero then + fSop (OEluil hi) fSnil + else + let fsv := fSop (OEluil hi) fSnil in + let hl := make_lfsv_single fsv in + fSop (OEaddil None lo) hl. + +Definition loadimm32 (n: int) := + match make_immed32 n with + | Imm32_single imm => + fSop (OEaddiw (Some X0_R) imm) fSnil + | Imm32_pair hi lo => load_hilo32 hi lo + end. + +Definition loadimm64 (n: int64) := + match make_immed64 n with + | Imm64_single imm => + fSop (OEaddil (Some X0_R) imm) fSnil + | Imm64_pair hi lo => load_hilo64 hi lo + | Imm64_large imm => fSop (OEloadli imm) fSnil + end. + +Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) := + match make_immed32 n with + | Imm32_single imm => + let hl := make_lfsv_single hv1 in + fSop (opimm imm) hl + | Imm32_pair hi lo => + let fsv := load_hilo32 hi lo in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + end. + +Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := + match make_immed64 n with + | Imm64_single imm => + let hl := make_lfsv_single hv1 in + fSop (opimm imm) hl + | Imm64_pair hi lo => + let fsv := load_hilo64 hi lo in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + | Imm64_large imm => + let fsv := fSop (OEloadli imm) fSnil in + let hl := make_lfsv_cmp false hv1 fsv in + fSop op hl + end. + +Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). +Definition andimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oand OEandiw. +Definition orimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oor OEoriw. +Definition xorimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oxor OExoriw. +Definition sltimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. +Definition sltuimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. +Definition addimm64 (hv1: sval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). +Definition andimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oandl OEandil. +Definition orimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oorl OEoril. +Definition xorimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oxorl OExoril. +Definition sltimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. +Definition sltuimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. +(** ** Comparisons intructions *) + +Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := + match cmp with + | Ceq => fSop (OEseqw optR) lsv + | Cne => fSop (OEsnew optR) lsv + | Clt | Cgt => fSop (OEsltw optR) lsv + | Cle | Cge => + let fsv := (fSop (OEsltw optR) lsv) in + let lfsv := make_lfsv_single fsv in + fSop (OExoriw Int.one) lfsv + end. + +Definition cond_int32u (cmp: comparison) (lsv: list_sval) (optR: option oreg) := + match cmp with + | Ceq => fSop (OEsequw optR) lsv + | Cne => fSop (OEsneuw optR) lsv + | Clt | Cgt => fSop (OEsltuw optR) lsv + | Cle | Cge => + let fsv := (fSop (OEsltuw optR) lsv) in + let lfsv := make_lfsv_single fsv in + fSop (OExoriw Int.one) lfsv + end. + +Definition cond_int64s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := + match cmp with + | Ceq => fSop (OEseql optR) lsv + | Cne => fSop (OEsnel optR) lsv + | Clt | Cgt => fSop (OEsltl optR) lsv + | Cle | Cge => + let fsv := (fSop (OEsltl optR) lsv) in + let lfsv := make_lfsv_single fsv in + fSop (OExoriw Int.one) lfsv + end. + +Definition cond_int64u (cmp: comparison) (lsv: list_sval) (optR: option oreg) := + match cmp with + | Ceq => fSop (OEsequl optR) lsv + | Cne => fSop (OEsneul optR) lsv + | Clt | Cgt => fSop (OEsltul optR) lsv + | Cle | Cge => + let fsv := (fSop (OEsltul optR) lsv) in + let lfsv := make_lfsv_single fsv in + fSop (OExoriw Int.one) lfsv + end. + +Definition expanse_condimm_int32s (cmp: comparison) (fsv1: sval) (n: int) := + let is_inv := is_inv_cmp_int cmp in + if Int.eq n Int.zero then + let optR := make_optR true is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + cond_int32s cmp lfsv optR + else + match cmp with + | Ceq | Cne => + let optR := make_optR true is_inv in + let fsv := xorimm32 fsv1 n in + let lfsv := make_lfsv_cmp false fsv fsv in + cond_int32s cmp lfsv optR + | Clt => sltimm32 fsv1 n + | Cle => + if Int.eq n (Int.repr Int.max_signed) then + let fsv := loadimm32 Int.one in + let lfsv := make_lfsv_cmp false fsv1 fsv in + fSop (OEmayundef MUint) lfsv + else sltimm32 fsv1 (Int.add n Int.one) + | _ => + let optR := make_optR false is_inv in + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + cond_int32s cmp lfsv optR + end. + +Definition expanse_condimm_int32u (cmp: comparison) (fsv1: sval) (n: int) := + let is_inv := is_inv_cmp_int cmp in + if Int.eq n Int.zero then + let optR := make_optR true is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + cond_int32u cmp lfsv optR + else + match cmp with + | Clt => sltuimm32 fsv1 n + | _ => + let optR := make_optR false is_inv in + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + cond_int32u cmp lfsv optR + end. + +Definition expanse_condimm_int64s (cmp: comparison) (fsv1: sval) (n: int64) := + let is_inv := is_inv_cmp_int cmp in + if Int64.eq n Int64.zero then + let optR := make_optR true is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + cond_int64s cmp lfsv optR + else + match cmp with + | Ceq | Cne => + let optR := make_optR true is_inv in + let fsv := xorimm64 fsv1 n in + let lfsv := make_lfsv_cmp false fsv fsv in + cond_int64s cmp lfsv optR + | Clt => sltimm64 fsv1 n + | Cle => + if Int64.eq n (Int64.repr Int64.max_signed) then + let fsv := loadimm32 Int.one in + let lfsv := make_lfsv_cmp false fsv1 fsv in + fSop (OEmayundef MUlong) lfsv + else sltimm64 fsv1 (Int64.add n Int64.one) + | _ => + let optR := make_optR false is_inv in + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + cond_int64s cmp lfsv optR + end. + +Definition expanse_condimm_int64u (cmp: comparison) (fsv1: sval) (n: int64) := + let is_inv := is_inv_cmp_int cmp in + if Int64.eq n Int64.zero then + let optR := make_optR true is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + cond_int64u cmp lfsv optR + else + match cmp with + | Clt => sltuimm64 fsv1 n + | _ => + let optR := make_optR false is_inv in + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + cond_int64u cmp lfsv optR + end. + +Definition cond_float (cmp: comparison) (lsv: list_sval) := + match cmp with + | Ceq | Cne => fSop OEfeqd lsv + | Clt | Cgt => fSop OEfltd lsv + | Cle | Cge => fSop OEfled lsv + end. + +Definition cond_single (cmp: comparison) (lsv: list_sval) := + match cmp with + | Ceq | Cne => fSop OEfeqs lsv + | Clt | Cgt => fSop OEflts lsv + | Cle | Cge => fSop OEfles lsv + end. + +Definition is_normal_cmp cmp := + match cmp with | Cne => false | _ => true end. + +Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + let fsv := fn_cond cmp lsv in + let lfsv := make_lfsv_single fsv in + if normal' then fsv else fSop (OExoriw Int.one) lfsv. + +(** Target op simplifications using "fake" values *) + +Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval := + match op, lr with + | Ocmp (Ccomp c), a1 :: a2 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + let fsv2 := ris_sreg_get hrs a2 in + let is_inv := is_inv_cmp_int c in + let optR := make_optR false is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond_int32s c lfsv optR) + | Ocmp (Ccompu c), a1 :: a2 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + let fsv2 := ris_sreg_get hrs a2 in + let is_inv := is_inv_cmp_int c in + let optR := make_optR false is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond_int32u c lfsv optR) + | Ocmp (Ccompimm c imm), a1 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + Some (expanse_condimm_int32s c fsv1 imm) + | Ocmp (Ccompuimm c imm), a1 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + Some (expanse_condimm_int32u c fsv1 imm) + | Ocmp (Ccompl c), a1 :: a2 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + let fsv2 := ris_sreg_get hrs a2 in + let is_inv := is_inv_cmp_int c in + let optR := make_optR false is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond_int64s c lfsv optR) + | Ocmp (Ccomplu c), a1 :: a2 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + let fsv2 := ris_sreg_get hrs a2 in + let is_inv := is_inv_cmp_int c in + let optR := make_optR false is_inv in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond_int64u c lfsv optR) + | Ocmp (Ccomplimm c imm), a1 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + Some (expanse_condimm_int64s c fsv1 imm) + | Ocmp (Ccompluimm c imm), a1 :: nil => + let fsv1 := ris_sreg_get hrs a1 in + Some (expanse_condimm_int64u c fsv1 imm) + | Ocmp (Ccompf c), f1 :: f2 :: nil => + let fsv1 := ris_sreg_get hrs f1 in + let fsv2 := ris_sreg_get hrs f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cond_fp false cond_float c lfsv) + | Ocmp (Cnotcompf c), f1 :: f2 :: nil => + let fsv1 := ris_sreg_get hrs f1 in + let fsv2 := ris_sreg_get hrs f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cond_fp true cond_float c lfsv) + | Ocmp (Ccompfs c), f1 :: f2 :: nil => + let fsv1 := ris_sreg_get hrs f1 in + let fsv2 := ris_sreg_get hrs f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cond_fp false cond_single c lfsv) + | Ocmp (Cnotcompfs c), f1 :: f2 :: nil => + let fsv1 := ris_sreg_get hrs f1 in + let fsv2 := ris_sreg_get hrs f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cond_fp true cond_single c lfsv) + | _, _ => None + end. + +Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := + None. + +(** * Auxiliary lemmas on comparisons *) + +(** ** Signed ints *) + +Lemma xor_neg_ltle_cmp: forall v1 v2, + Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmp_bool Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + unfold Val.cmp; simpl; + try rewrite Int.eq_sym; + try destruct (Int.eq _ _); try destruct (Int.lt _ _) eqn:ELT ; simpl; + try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; + auto. +Qed. +Local Hint Resolve xor_neg_ltle_cmp: core. + +(** ** Unsigned ints *) + +Lemma xor_neg_ltle_cmpu: forall mptr v1 v2, + Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer mptr) Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + unfold Val.cmpu; simpl; + try rewrite Int.eq_sym; + try destruct (Int.eq _ _); try destruct (Int.ltu _ _) eqn:ELT ; simpl; + try rewrite Int.xor_one_one; try rewrite Int.xor_zero_one; + auto. + 1,2: + unfold Val.cmpu, Val.cmpu_bool; + destruct Archi.ptr64; try destruct (_ && _); try destruct (_ || _); + try destruct (eq_block _ _); auto. + unfold Val.cmpu, Val.cmpu_bool; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. +Local Hint Resolve xor_neg_ltle_cmpu: core. + +Remark ltu_12_wordsize: + Int.ltu (Int.repr 12) Int.iwordsize = true. +Proof. + unfold Int.iwordsize, Int.zwordsize. simpl. + unfold Int.ltu. apply zlt_true. + rewrite !Int.unsigned_repr; try cbn; try lia. +Qed. +Local Hint Resolve ltu_12_wordsize: core. + +(** ** Signed longs *) + +Lemma xor_neg_ltle_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. +Local Hint Resolve xor_neg_ltle_cmpl: core. + +Lemma xor_neg_ltge_cmpl: forall v1 v2, + Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpl_bool Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.lt _ _); auto. +Qed. +Local Hint Resolve xor_neg_ltge_cmpl: core. + +Lemma xorl_zero_eq_cmpl: forall c v1 v2, + c = Ceq \/ c = Cne -> + Some + (Val.maketotal + (option_map Val.of_bool + (Val.cmpl_bool c (Val.xorl v1 v2) (Vlong Int64.zero)))) = + Some (Val.of_optbool (Val.cmpl_bool c v1 v2)). +Proof. + intros. destruct c; inv H; try discriminate; + destruct v1, v2; simpl; auto; + destruct (Int64.eq i i0) eqn:EQ0. + 1,3: + apply Int64.same_if_eq in EQ0; subst; + rewrite Int64.xor_idem; + rewrite Int64.eq_true; trivial. + 1,2: + destruct (Int64.eq (Int64.xor i i0) Int64.zero) eqn:EQ1; simpl; try congruence; + rewrite Int64.xor_is_zero in EQ1; congruence. +Qed. +Local Hint Resolve xorl_zero_eq_cmpl: core. + +Lemma cmp_ltle_add_one: forall v n, + Int.eq n (Int.repr Int.max_signed) = false -> + Some (Val.of_optbool (Val.cmp_bool Clt v (Vint (Int.add n Int.one)))) = + Some (Val.of_optbool (Val.cmp_bool Cle v (Vint n))). +Proof. + intros v n EQMAX. unfold Val.cmp_bool; destruct v; simpl; auto. + unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). + destruct (zlt (Int.signed n) (Int.signed i)). + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. + rewrite Int.add_signed. symmetry; apply Int.signed_repr. + specialize (Int.eq_spec n (Int.repr Int.max_signed)). + rewrite EQMAX; simpl; intros. + assert (Int.signed n <> Int.max_signed). + { red; intros E. elim H. rewrite <- (Int.repr_signed n). rewrite E. auto. } + generalize (Int.signed_range n); lia. +Qed. +Local Hint Resolve cmp_ltle_add_one: core. + +Lemma cmpl_ltle_add_one: forall v n, + Int64.eq n (Int64.repr Int64.max_signed) = false -> + Some (Val.of_optbool (Val.cmpl_bool Clt v (Vlong (Int64.add n Int64.one)))) = + Some (Val.of_optbool (Val.cmpl_bool Cle v (Vlong n))). +Proof. + intros v n EQMAX. unfold Val.cmpl_bool; destruct v; simpl; auto. + unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). + destruct (zlt (Int64.signed n) (Int64.signed i)). + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. + rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. + specialize (Int64.eq_spec n (Int64.repr Int64.max_signed)). + rewrite EQMAX; simpl; intros. + assert (Int64.signed n <> Int64.max_signed). + { red; intros E. elim H. rewrite <- (Int64.repr_signed n). rewrite E. auto. } + generalize (Int64.signed_range n); lia. +Qed. +Local Hint Resolve cmpl_ltle_add_one: core. + +Remark lt_maxsgn_false_int: forall i, + Int.lt (Int.repr Int.max_signed) i = false. +Proof. + intros; unfold Int.lt. + specialize Int.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. +Local Hint Resolve lt_maxsgn_false_int: core. + +Remark lt_maxsgn_false_long: forall i, + Int64.lt (Int64.repr Int64.max_signed) i = false. +Proof. + intros; unfold Int64.lt. + specialize Int64.signed_range with i; intros. + rewrite zlt_false; auto. destruct H. + rewrite Int64.signed_repr; try (cbn; lia). + apply Z.le_ge. trivial. +Qed. +Local Hint Resolve lt_maxsgn_false_long: core. + +(** ** Unsigned longs *) + +Lemma xor_neg_ltle_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cle v2 v1)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. +Local Hint Resolve xor_neg_ltle_cmplu: core. + +Lemma xor_neg_ltge_cmplu: forall mptr v1 v2, + Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer mptr) Cge v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence. + destruct (Int64.ltu _ _); auto. + 1,2: unfold Val.cmplu; simpl; auto; + destruct (Archi.ptr64); simpl; + try destruct (eq_block _ _); simpl; + try destruct (_ && _); simpl; + try destruct (Ptrofs.cmpu _ _); + try destruct cmp; simpl; auto. + unfold Val.cmplu; simpl; + destruct Archi.ptr64; try destruct (_ || _); simpl; auto; + destruct (eq_block b b0); destruct (eq_block b0 b); + try congruence; + try destruct (_ || _); simpl; try destruct (Ptrofs.ltu _ _); + simpl; auto; + repeat destruct (_ && _); simpl; auto. +Qed. +Local Hint Resolve xor_neg_ltge_cmplu: core. + +(** ** Floats *) + +Lemma xor_neg_eqne_cmpf: forall v1 v2, + Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpf_bool Cne v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmpf; simpl. + rewrite Float.cmp_ne_eq. + destruct (Float.cmp _ _ _); simpl; auto. +Qed. +Local Hint Resolve xor_neg_eqne_cmpf: core. + +(** ** Singles *) + +Lemma xor_neg_eqne_cmpfs: forall v1 v2, + Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = + Some (Val.of_optbool (Val.cmpfs_bool Cne v1 v2)). +Proof. + intros. eapply f_equal. + destruct v1, v2; simpl; try congruence; + unfold Val.cmpfs; simpl. + rewrite Float32.cmp_ne_eq. + destruct (Float32.cmp _ _ _); simpl; auto. +Qed. +Local Hint Resolve xor_neg_eqne_cmpfs: core. + +(** ** More useful lemmas *) + +Lemma xor_neg_optb: forall v, + Some (Val.xor (Val.of_optbool (option_map negb v)) + (Vint Int.one)) = Some (Val.of_optbool v). +Proof. + intros. + destruct v; simpl; trivial. + destruct b; simpl; auto. +Qed. +Local Hint Resolve xor_neg_optb: core. + +Lemma xor_neg_optb': forall v, + Some (Val.xor (Val.of_optbool v) (Vint Int.one)) = + Some (Val.of_optbool (option_map negb v)). +Proof. + intros. + destruct v; simpl; trivial. + destruct b; simpl; auto. +Qed. +Local Hint Resolve xor_neg_optb': core. + +Lemma optbool_mktotal: forall v, + Val.maketotal (option_map Val.of_bool v) = + Val.of_optbool v. +Proof. + intros. + destruct v; simpl; auto. +Qed. +Local Hint Resolve optbool_mktotal: core. + +(* TODO gourdinl move to common/Values ? *) +Theorem swap_cmpf_bool: + forall c x y, + Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. +Qed. +Local Hint Resolve swap_cmpf_bool: core. + +Theorem swap_cmpfs_bool: + forall c x y, + Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. +Qed. +Local Hint Resolve swap_cmpfs_bool: core. + +(** * Intermediates lemmas on each expanded instruction *) + +Lemma simplify_ccomp_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (cond_int32s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = + Some (Val.of_optbool (Val.cmp_bool c v v0)). +Proof. + intros. + unfold cond_int32s in *; destruct c; simpl; + erewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmp. eauto. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmp_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmp_bool; eauto. +Qed. + +Lemma simplify_ccompu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (cond_int32u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)). +Proof. + intros. + unfold cond_int32u in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpu. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpu_bool; trivial. + - replace (Clt) with (negate_comparison Cge) by auto; + rewrite Val.negate_cmpu_bool; eauto. +Qed. + +Lemma simplify_ccompimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r v n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v), + eval_sval ctx (expanse_condimm_int32s c (hrs r) n) = + Some (Val.of_optbool (Val.cmp_bool c v (Vint n))). +Proof. + intros. + unfold expanse_condimm_int32s, cond_int32s in *; destruct c; + intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; + unfold loadimm32, sltimm32, xorimm32, opimm32, load_hilo32; + try rewrite !REG_EQ, OKv1; + unfold Val.cmp, zero32. + all: + try apply xor_neg_ltle_cmp; + try apply xor_neg_ltge_cmp; trivial. + 4: + try destruct (Int.eq n (Int.repr Int.max_signed)) eqn:EQMAX; subst; + try apply Int.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed32_sound with (Int.add n Int.one); + destruct (make_immed32 (Int.add n Int.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,8,9: + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl. + all: + try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; + try rewrite !REG_EQ, OKv1; + try rewrite (Int.add_commut _ Int.zero), Int.add_zero_l in H; subst; simpl; + unfold Val.cmp, eval_may_undef, zero32, Val.add; simpl; + destruct v; auto. + all: + try rewrite ltu_12_wordsize; + try rewrite <- H; + try (apply cmp_ltle_add_one; auto); + try rewrite Int.add_commut, Int.add_zero_l in *; + try ( + simpl; trivial; + try rewrite Int.xor_is_zero; + try destruct (Int.lt _ _) eqn:EQLT; trivial; + try rewrite lt_maxsgn_false_int in EQLT; + simpl; trivial; try discriminate; fail). +Qed. + +Lemma simplify_ccompuimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r v n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v), + eval_sval ctx (expanse_condimm_int32u c (hrs r) n) = + Some (Val.of_optbool (Val.cmpu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vint n))). +Proof. + intros. + unfold expanse_condimm_int32u, cond_int32u in *; destruct c; + intros; destruct (Int.eq n Int.zero) eqn:EQIMM; simpl; + try apply Int.same_if_eq in EQIMM; subst; + unfold loadimm32, sltuimm32, opimm32, load_hilo32; + try rewrite !REG_EQ, OKv1; trivial; + try rewrite xor_neg_ltle_cmpu; + unfold Val.cmpu, zero32. + all: + try (specialize make_immed32_sound with n; + destruct (make_immed32 n) eqn:EQMKI); + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; subst; + intros; subst; simpl; + try rewrite !REG_EQ, OKv1; + unfold eval_may_undef, Val.cmpu; + destruct v; simpl; auto; + 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 destruct (Int.ltu _ _) eqn:EQLTU; simpl; + try rewrite EQLTU; simpl; try rewrite EQIMM; + try rewrite EQARCH; trivial. +Qed. + +Lemma simplify_ccompl_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (cond_int64s c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = + Some (Val.of_optbool (Val.cmpl_bool c v v0)). +Proof. + intros. + unfold cond_int64s in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpl. + 1,2,3: rewrite optbool_mktotal; trivial. + replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmpl_bool; trivial. + rewrite optbool_mktotal; trivial. +Qed. + +Lemma simplify_ccomplu_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (cond_int64u c (make_lfsv_cmp (is_inv_cmp_int c) (hrs r) (hrs r0)) None) = + Some (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v v0)). +Proof. + intros. + unfold cond_int64u in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmplu. + 1,2,3: rewrite optbool_mktotal; trivial; eauto. + replace (Clt) with (swap_comparison Cgt) by auto; + rewrite Val.swap_cmplu_bool; trivial. + rewrite optbool_mktotal; trivial. +Qed. + +Lemma simplify_ccomplimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r v n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v), + eval_sval ctx (expanse_condimm_int64s c (hrs r) n) = + Some (Val.of_optbool (Val.cmpl_bool c v (Vlong n))). +Proof. + intros. + unfold expanse_condimm_int64s, cond_int64s in *; destruct c; + intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + try apply Int64.same_if_eq in EQIMM; subst; + unfold loadimm32, loadimm64, sltimm64, xorimm64, opimm64, load_hilo32, load_hilo64; + try rewrite !REG_EQ, OKv1; + unfold Val.cmpl, zero64. + all: + try apply xor_neg_ltle_cmpl; + try apply xor_neg_ltge_cmpl; + try rewrite optbool_mktotal; trivial. + 4: + try destruct (Int64.eq n (Int64.repr Int64.max_signed)) eqn:EQMAX; subst; + try apply Int64.same_if_eq in EQMAX; subst; simpl. + 4: + intros; try (specialize make_immed32_sound with (Int.one); + destruct (make_immed32 Int.one) eqn:EQMKI_A1); intros; simpl. + 6: + intros; try (specialize make_immed64_sound with (Int64.add n Int64.one); + destruct (make_immed64 (Int64.add n Int64.one)) eqn:EQMKI_A2); intros; simpl. + 1,2,3,9,10: + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl. + all: + try destruct (Int.eq lo Int.zero) eqn:EQLO32; + try apply Int.same_if_eq in EQLO32; subst; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO64; + try apply Int64.same_if_eq in EQLO64; subst; simpl; + try rewrite !REG_EQ, OKv1; + try rewrite (Int64.add_commut _ Int64.zero), Int64.add_zero_l in H; subst; + unfold Val.cmpl, Val.addl; + try rewrite optbool_mktotal; trivial; + destruct v; auto. + all: + try rewrite <- optbool_mktotal; trivial; + try rewrite Int64.add_commut, Int64.add_zero_l in *; + 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))). + all: + try rewrite <- cmpl_ltle_add_one; auto; + try rewrite ltu_12_wordsize; + try rewrite Int.add_commut, Int.add_zero_l in *; + simpl; try rewrite lt_maxsgn_false_long; + try (rewrite <- H; trivial; fail); + simpl; trivial. +Qed. + +Lemma simplify_ccompluimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r v n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v), + eval_sval ctx (expanse_condimm_int64u c (hrs r) n) = + Some (Val.of_optbool + (Val.cmplu_bool (Mem.valid_pointer (cm0 ctx)) c v (Vlong n))). +Proof. + intros. + unfold expanse_condimm_int64u, cond_int64u in *; destruct c; + intros; destruct (Int64.eq n Int64.zero) eqn:EQIMM; simpl; + unfold loadimm64, sltuimm64, opimm64, load_hilo64; + try rewrite !REG_EQ, OKv1; + unfold Val.cmplu, zero64. + (* Simplify make immediate and decompose subcases *) + all: + try (specialize make_immed64_sound with n; + destruct (make_immed64 n) eqn:EQMKI); + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; simpl; + try rewrite !REG_EQ, OKv1. + (* Ceq, Cne, Clt = itself *) + all: intros; try apply Int64.same_if_eq in EQIMM; subst; trivial. + (* Cle = xor (Clt) *) + all: try apply xor_neg_ltle_cmplu; trivial. + (* Others subcases with swap/negation *) + all: + unfold Val.cmplu, eval_may_undef, 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 <- xor_neg_ltle_cmplu; unfold Val.cmplu; + trivial; fail); + try rewrite optbool_mktotal; trivial. + all: + try destruct v; simpl; auto; + try destruct (Archi.ptr64); simpl; + try rewrite EQIMM; + try destruct (Int64.ltu _ _); + try rewrite <- optbool_mktotal; trivial. +Qed. + +Lemma simplify_ccompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (expanse_cond_fp false cond_float c + (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = + Some (Val.of_optbool (Val.cmpf_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpf. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpf_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpf_bool; trivial. +Qed. + +Lemma simplify_cnotcompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (expanse_cond_fp true cond_float c + (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = + Some (Val.of_optbool (option_map negb (Val.cmpf_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpf. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float.cmp_swap; simpl. + all: destruct (Float.cmp _ _ _); trivial. +Qed. + +Lemma simplify_ccompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), eval_sval ctx + (expanse_cond_fp false cond_single c + (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = + Some (Val.of_optbool (Val.cmpfs_bool c v v0)). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpfs. + - replace (Clt) with (swap_comparison Cgt) by auto; + rewrite swap_cmpfs_bool; trivial. + - replace (Cle) with (swap_comparison Cge) by auto; + rewrite swap_cmpfs_bool; trivial. +Qed. + +Lemma simplify_cnotcompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + c r r0 v v0: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (OKv1 : eval_sval ctx (st r) = Some v) + (OKv2 : eval_sval ctx (st r0) = Some v0), + eval_sval ctx + (expanse_cond_fp true cond_single c + (make_lfsv_cmp (is_inv_cmp_float c) (hrs r) (hrs r0))) = + Some (Val.of_optbool (option_map negb (Val.cmpfs_bool c v v0))). +Proof. + intros. + unfold expanse_cond_fp in *; destruct c; simpl; + rewrite !REG_EQ, OKv1, OKv2; trivial; + unfold Val.cmpfs. + 1,3,4: apply xor_neg_optb'. + all: destruct v, v0; simpl; trivial. + rewrite Float32.cmp_ne_eq; rewrite negb_involutive; trivial. + 1: replace (Clt) with (swap_comparison Cgt) by auto; rewrite <- Float32.cmp_swap; simpl. + 2: replace (Cle) with (swap_comparison Cge) by auto; rewrite <- Float32.cmp_swap; simpl. + all: destruct (Float32.cmp _ _ _); trivial. +Qed. + +(* Main proof of simplification *) + +Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall + (H: target_op_simplify op lr hrs = Some fsv) + (REF: ris_refines ctx hrs st) + (OK0: ris_ok ctx hrs) + (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args), + eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx). +Proof. + unfold target_op_simplify; simpl. + intros H ? ? ?; inv REF. + destruct op; try congruence. + (* Ocmp expansions *) + destruct cond; repeat (destruct lr; simpl; try congruence); + simpl in OK1; + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + inv H; inv OK1. + - eapply simplify_ccomp_correct; eauto. + - eapply simplify_ccompu_correct; eauto. + - eapply simplify_ccompimm_correct; eauto. + - eapply simplify_ccompuimm_correct; eauto. + - eapply simplify_ccompl_correct; eauto. + - eapply simplify_ccomplu_correct; eauto. + - eapply simplify_ccomplimm_correct; eauto. + - eapply simplify_ccompluimm_correct; eauto. + - eapply simplify_ccompf_correct; eauto. + - eapply simplify_cnotcompf_correct; eauto. + - eapply simplify_ccompfs_correct; eauto. + - eapply simplify_cnotcompfs_correct; eauto. +Qed. + +(* +Lemma target_cbranch_expanse_correct hrs c l ge sp rs0 m0 st c' l': forall + (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) + (LREF : hsilocal_refines ge sp rs0 m0 hrs st) + (OK: hsok_local ge sp rs0 m0 hrs), + seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = + seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Proof. + unfold target_cbranch_expanse, seval_condition; simpl. + intros H (LREF & SREF & SREG & SMEM) ?. + congruence. +Qed. +Global Opaque target_op_simplify. + Global Opaque target_cbranch_expanse.*) -- cgit From 0481f8e4c6aa3dd19219a8b196b36fcfaeb5408d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 13:35:49 +0200 Subject: new expansions --- riscV/BTL_SEsimplify.v | 752 ++++++++++++++++++++++++++++++++++++++++++++++- riscV/ExpansionOracle.ml | 198 ++++++++++++- 2 files changed, 935 insertions(+), 15 deletions(-) (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index a4a2785a..30468544 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -38,16 +38,16 @@ Definition load_hilo32 (hi lo: int) := fSop (OEluiw hi) fSnil else let fsv := fSop (OEluiw hi) fSnil in - let hl := make_lfsv_single fsv in - fSop (OEaddiw None lo) hl. + let lfsv := make_lfsv_single fsv in + fSop (OEaddiw None lo) lfsv. Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then fSop (OEluil hi) fSnil else let fsv := fSop (OEluil hi) fSnil in - let hl := make_lfsv_single fsv in - fSop (OEaddil None lo) hl. + let lfsv := make_lfsv_single fsv in + fSop (OEaddil None lo) lfsv. Definition loadimm32 (n: int) := match make_immed32 n with @@ -67,27 +67,27 @@ Definition loadimm64 (n: int64) := Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => - let hl := make_lfsv_single hv1 in - fSop (opimm imm) hl + let lfsv := make_lfsv_single hv1 in + fSop (opimm imm) lfsv | Imm32_pair hi lo => let fsv := load_hilo32 hi lo in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv end. Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := match make_immed64 n with | Imm64_single imm => - let hl := make_lfsv_single hv1 in - fSop (opimm imm) hl + let lfsv := make_lfsv_single hv1 in + fSop (opimm imm) lfsv | Imm64_pair hi lo => let fsv := load_hilo64 hi lo in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv | Imm64_large imm => let fsv := fSop (OEloadli imm) fSnil in - let hl := make_lfsv_cmp false hv1 fsv in - fSop op hl + let lfsv := make_lfsv_cmp false hv1 fsv in + fSop op lfsv end. Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). @@ -326,6 +326,113 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt let is_inv := is_inv_cmp_float c in let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in Some (expanse_cond_fp true cond_single c lfsv) + | Ofloatconst f, nil => + let fsv := loadimm64 (Float.to_bits f) in + let lfsv := make_lfsv_single fsv in + Some (fSop (Ofloat_of_bits) lfsv) + | Osingleconst f, nil => + let fsv := loadimm32 (Float32.to_bits f) in + let lfsv := make_lfsv_single fsv in + Some (fSop (Osingle_of_bits) lfsv) + | Ointconst n, nil => + Some (loadimm32 n) + | Olongconst n, nil => + Some (loadimm64 n) + | Oaddimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (addimm32 hv1 n None) + | Oaddlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (addimm64 hv1 n None) + | Oandimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (andimm32 hv1 n) + | Oandlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (andimm64 hv1 n) + | Oorimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (orimm32 hv1 n) + | Oorlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (orimm64 hv1 n) + | Oxorimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (xorimm32 hv1 n) + | Oxorlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + Some (xorimm64 hv1 n) + | Ocast8signed, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in + let hl' := make_lfsv_single fsv in + Some (fSop (Oshrimm (Int.repr 24)) hl') + | Ocast16signed, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in + let hl' := make_lfsv_single fsv in + Some (fSop (Oshrimm (Int.repr 16)) hl') + | Ocast32unsigned, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + let cast32s_s := fSop Ocast32signed lfsv in + let cast32s_l := make_lfsv_single cast32s_s in + let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in + let sllil_l := make_lfsv_single sllil_s in + Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) + | Oshrximm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lfsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrx n)) lhl) + else + if Int.eq n Int.one then + let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in + let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lfsv_single addw_s in + let sraiw_s := fSop (Oshrimm Int.one) addw_l in + let sraiw_l := make_lfsv_cmp false sraiw_s sraiw_s in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l) + else + let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in + let sraiw_l := make_lfsv_single sraiw_s in + let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in + let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let addw_s := fSop Oadd srliw_l in + let addw_l := make_lfsv_single addw_s in + let sraiw_s' := fSop (Oshrimm n) addw_l in + let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in + Some (fSop (OEmayundef (MUshrx n)) sraiw_l') + | Oshrxlimm n, a1 :: nil => + let hv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single hv1 in + if Int.eq n Int.zero then + let lhl := make_lfsv_cmp false hv1 hv1 in + Some (fSop (OEmayundef (MUshrxl n)) lhl) + else + if Int.eq n Int.one then + let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in + let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lfsv_single addl_s in + let srail_s := fSop (Oshrlimm Int.one) addl_l in + let srail_l := make_lfsv_cmp false srail_s srail_s in + Some (fSop (OEmayundef (MUshrxl n)) srail_l) + else + let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in + let srail_l := make_lfsv_single srail_s in + let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in + let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let addl_s := fSop Oaddl srlil_l in + let addl_l := make_lfsv_single addl_s in + let srail_s' := fSop (Oshrlimm n) addl_l in + let srail_l' := make_lfsv_cmp false srail_s' srail_s' in + Some (fSop (OEmayundef (MUshrxl n)) srail_l') + | _, _ => None end. @@ -950,6 +1057,606 @@ Proof. all: destruct (Float32.cmp _ _ _); trivial. Qed. +Lemma simplify_intconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (H : match lr with + | nil => Some (loadimm32 n) + | _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Ointconst n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm32, load_hilo32, make_lfsv_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 ltu_12_wordsize; try rewrite H; trivial. +Qed. + +Lemma simplify_longconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (H : match lr with + | nil => Some (loadimm64 n) + | _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Olongconst n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv OK1; inv H; simpl; + unfold loadimm64, load_hilo64, make_lfsv_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_floatconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (H : match lr with + | nil => + Some + (fSop Ofloat_of_bits + (make_lfsv_single (loadimm64 (Float.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Ofloatconst n) args (cm0 ctx). +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. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. +Qed. + +Lemma simplify_singleconst_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (H : match lr with + | nil => + Some + (fSop Osingle_of_bits + (make_lfsv_single (loadimm32 (Float32.to_bits n)))) + | _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Osingleconst n) args (cm0 ctx). +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; + rewrite ltu_12_wordsize; simpl; try rewrite <- H; + try rewrite Float32.of_to_bits; trivial. +Qed. + +Lemma simplify_cast8signed_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 24)) + (make_lfsv_single + (fSop (Oshlimm (Int.repr 24)) (make_lfsv_single (hrs a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) Ocast8signed args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + rewrite !REG_EQ. + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. + 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 (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrimm (Int.repr 16)) + (make_lfsv_single + (fSop (Oshlimm (Int.repr 16)) (make_lfsv_single (hrs a1))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) Ocast16signed args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + rewrite !REG_EQ. + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. + 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_addimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm32 (hrs a1) n None) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oaddimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl. + unfold addimm32, opimm32, load_hilo32, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + apply Int.same_if_eq in EQLO; subst; + rewrite Int.add_commut, Int.add_zero_l; + rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_andimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm32 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oandimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl. + unfold andimm32, opimm32, load_hilo32, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + fold (Val.and (Vint imm) v); rewrite Val.and_commut; trivial. + apply Int.same_if_eq in EQLO; subst; + rewrite Int.add_commut, Int.add_zero_l; + rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_orimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm32 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oorimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl. + unfold orimm32, opimm32, load_hilo32, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + fold (Val.or (Vint imm) v); rewrite Val.or_commut; trivial. + apply Int.same_if_eq in EQLO; subst; + rewrite Int.add_commut, Int.add_zero_l; + rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_xorimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (xorimm32 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oxorimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl. + unfold xorimm32, opimm32, load_hilo32, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + apply Int.same_if_eq in EQLO; subst; + rewrite Int.add_commut, Int.add_zero_l; + rewrite ltu_12_wordsize; trivial. +Qed. + +Lemma simplify_shrximm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lfsv_cmp false (hrs a1) (hrs a1))) + else + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrx n)) + (make_lfsv_cmp false + (fSop (Oshrimm Int.one) + (make_lfsv_single + (fSop Oadd + (make_lfsv_cmp false (hrs a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lfsv_single (hrs a1))))))) + (fSop (Oshrimm Int.one) + (make_lfsv_single + (fSop Oadd + (make_lfsv_cmp false (hrs a1) + (fSop (Oshruimm (Int.repr 31)) + (make_lfsv_single (hrs a1))))))))) + else + Some + (fSop (OEmayundef (MUshrx n)) + (make_lfsv_cmp false + (fSop (Oshrimm n) + (make_lfsv_single + (fSop Oadd + (make_lfsv_cmp false (hrs a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lfsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lfsv_single (hrs a1))))))))) + (fSop (Oshrimm n) + (make_lfsv_single + (fSop Oadd + (make_lfsv_cmp false (hrs a1) + (fSop (Oshruimm (Int.sub Int.iwordsize n)) + (make_lfsv_single + (fSop (Oshrimm (Int.repr 31)) + (make_lfsv_single (hrs a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oshrximm n) args (cm0 ctx). +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 H; simpl; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; + destruct (Val.shrx v (Vint n)) eqn:TOTAL; cbn; + unfold eval_may_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_cast32unsigned_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => + Some + (fSop (Oshrluimm (Int.repr 32)) + (make_lfsv_single + (fSop (Oshllimm (Int.repr 32)) + (make_lfsv_single + (fSop Ocast32signed (make_lfsv_single (hrs a1))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) Ocast32unsigned args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl. + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1. + 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. + +Lemma simplify_addlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (addimm64 (hrs a1) n None) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oaddlimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + unfold addimm64, opimm64, load_hilo64, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + apply Int64.same_if_eq in EQLO; subst. + rewrite Int64.add_commut, Int64.add_zero_l; trivial. +Qed. + +Lemma simplify_andlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (andimm64 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oandlimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + unfold andimm64, opimm64, load_hilo64, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + fold (Val.andl (Vlong imm) v); rewrite Val.andl_commut; trivial. + apply Int64.same_if_eq in EQLO; subst; + rewrite Int64.add_commut, Int64.add_zero_l; trivial. +Qed. + +Lemma simplify_orlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (orimm64 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oorlimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + unfold orimm64, opimm64, load_hilo64, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + fold (Val.orl (Vlong imm) v); rewrite Val.orl_commut; trivial. + apply Int64.same_if_eq in EQLO; subst; + rewrite Int64.add_commut, Int64.add_zero_l; trivial. +Qed. + +Lemma simplify_xorlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => Some (xorimm64 (hrs a1) n) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oxorlimm n) args (cm0 ctx). +Proof. + intros. + repeat (destruct lr; simpl; try congruence); + simpl in OK1; inv H; simpl; + unfold xorimm64, opimm64, load_hilo64, make_lfsv_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; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; trivial. + apply Int64.same_if_eq in EQLO; subst; + rewrite Int64.add_commut, Int64.add_zero_l; trivial. +Qed. + +Lemma simplify_shrxlimm_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) + args fsv lr n: forall + (REG_EQ : forall r : positive, eval_sval ctx (hrs r) = eval_sval ctx (st r)) + (H : match lr with + | nil => None + | a1 :: nil => + if Int.eq n Int.zero + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lfsv_cmp false (hrs a1) (hrs a1))) + else + if Int.eq n Int.one + then + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lfsv_cmp false + (fSop (Oshrlimm Int.one) + (make_lfsv_single + (fSop Oaddl + (make_lfsv_cmp false (hrs a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lfsv_single (hrs a1))))))) + (fSop (Oshrlimm Int.one) + (make_lfsv_single + (fSop Oaddl + (make_lfsv_cmp false (hrs a1) + (fSop (Oshrluimm (Int.repr 63)) + (make_lfsv_single (hrs a1))))))))) + else + Some + (fSop (OEmayundef (MUshrxl n)) + (make_lfsv_cmp false + (fSop (Oshrlimm n) + (make_lfsv_single + (fSop Oaddl + (make_lfsv_cmp false (hrs a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lfsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lfsv_single (hrs a1))))))))) + (fSop (Oshrlimm n) + (make_lfsv_single + (fSop Oaddl + (make_lfsv_cmp false (hrs a1) + (fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) + (make_lfsv_single + (fSop (Oshrlimm (Int.repr 63)) + (make_lfsv_single (hrs a1))))))))))) + | a1 :: _ :: _ => None + end = Some fsv) + (OK1 : eval_list_sval ctx (list_sval_inj (map st lr)) = Some args), + eval_sval ctx fsv = + eval_operation (cge ctx) (csp ctx) (Oshrxlimm n) args (cm0 ctx). +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 H; simpl; + rewrite !REG_EQ; + destruct (eval_sval ctx (st p)) eqn:OKv1; try congruence; inv OK1; + destruct (Val.shrxl v (Vint n)) eqn:TOTAL; cbn; + unfold eval_may_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. + (* Main proof of simplification *) Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall @@ -962,6 +1669,23 @@ Proof. unfold target_op_simplify; simpl. intros H ? ? ?; inv REF. destruct op; try congruence. + eapply simplify_intconst_correct; eauto. + eapply simplify_longconst_correct; eauto. + eapply simplify_floatconst_correct; eauto. + eapply simplify_singleconst_correct; eauto. + eapply simplify_cast8signed_correct; eauto. + eapply simplify_cast16signed_correct; eauto. + eapply simplify_addimm_correct; eauto. + eapply simplify_andimm_correct; eauto. + eapply simplify_orimm_correct; eauto. + eapply simplify_xorimm_correct; eauto. + eapply simplify_shrximm_correct; eauto. + eapply simplify_cast32unsigned_correct; eauto. + eapply simplify_addlimm_correct; eauto. + eapply simplify_andlimm_correct; eauto. + eapply simplify_orlimm_correct; eauto. + eapply simplify_xorlimm_correct; eauto. + eapply simplify_shrxlimm_correct; eauto. (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); simpl in OK1; diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index c1cf5c9c..2a21b7a4 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -514,7 +514,6 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = let r', l = extract_arg insn in addinst vn (OExoriw Int.one) [ r' ] dest :: l - (** Return olds args if the CSE numbering is empty *) let get_arguments vn vals args = @@ -607,6 +606,203 @@ let expanse_list li = exp := extract_final vn !exp dest; was_exp := true | _ -> ()); + (if !Clflags.option_fexpanse_others && not !was_exp then + match i with + | Bop (Ofloatconst f, nil, dest, iinfo) -> ( + match make_immed64 (Floats.Float.to_bits f) with + | Imm64_single _ | Imm64_large _ -> () + | Imm64_pair (hi, lo) -> + debug "Bop/Ofloatconst\n"; + let r = r2pi () in + let l = load_hilo64 vn r hi lo in + let r', l' = extract_arg l in + exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; + exp := extract_final vn !exp dest; + was_exp := true) + | Bop (Osingleconst f, nil, dest, iinfo) -> ( + match make_immed32 (Floats.Float32.to_bits f) with + | Imm32_single imm -> () + | Imm32_pair (hi, lo) -> + debug "Bop/Osingleconst\n"; + let r = r2pi () in + let l = load_hilo32 vn r hi lo in + let r', l' = extract_arg l in + exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; + exp := extract_final vn !exp dest; + was_exp := true) + | Bop (Ointconst n, nil, dest, iinfo) -> + debug "Bop/Ointconst\n"; + exp := loadimm32 vn dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Olongconst n, nil, dest, iinfo) -> + debug "Bop/Olongconst\n"; + exp := loadimm64 vn dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oaddimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oaddimm\n"; + exp := addimm32 vn a1 dest n None; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oaddlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oaddlimm\n"; + exp := addimm64 vn a1 dest n None; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oandimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oandimm\n"; + exp := andimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oandlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oandlimm\n"; + exp := andimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oorimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oorimm\n"; + exp := orimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oorlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oorlimm\n"; + exp := orimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oxorimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oxorimm\n"; + exp := xorimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oxorlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oxorlimm\n"; + exp := xorimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocast8signed, a1 :: nil, dest, iinfo) -> + debug "Bop/cast8signed\n"; + let op = Oshlimm (Int.repr (Z.of_sint 24)) in + let r = r2pi () in + let i1 = addinst vn op [ a1 ] r in + let r', l = extract_arg [ i1 ] in + exp := + addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocast16signed, a1 :: nil, dest, iinfo) -> + debug "Bop/cast16signed\n"; + let op = Oshlimm (Int.repr (Z.of_sint 16)) in + let r = r2pi () in + let i1 = addinst vn op [ a1 ] r in + let r', l = extract_arg [ i1 ] in + exp := + addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocast32unsigned, a1 :: nil, dest, iinfo) -> + debug "Bop/Ocast32unsigned\n"; + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Ocast32signed in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in + + let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in + let i2 = addinst vn op2 [ r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in + + let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in + exp := addinst vn op3 [ r2' ] dest :: l2; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oshrximm n, a1 :: nil, dest, iinfo) -> + if Int.eq n Int.zero then ( + debug "Bop/Oshrximm1\n"; + exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + debug "Bop/Oshrximm2\n"; + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in + + let op2 = Oadd in + let i2 = addinst vn op2 [ a1; r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in + + let op3 = Oshrimm Int.one in + let i3 = addinst vn op3 [ r2' ] dest in + let r3, l3 = extract_arg (i3 :: l2) in + exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) + else ( + debug "Bop/Oshrximm3\n"; + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in + + let op2 = Oshruimm (Int.sub Int.iwordsize n) in + let i2 = addinst vn op2 [ r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in + + let op3 = Oadd in + let i3 = addinst vn op3 [ a1; r2' ] r3 in + let r3', l3 = extract_arg (i3 :: l2) in + + let op4 = Oshrimm n in + let i4 = addinst vn op4 [ r3' ] dest in + let r4, l4 = extract_arg (i4 :: l3) in + exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4); + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oshrxlimm n, a1 :: nil, dest, iinfo) -> + if Int.eq n Int.zero then ( + debug "Bop/Oshrxlimm1\n"; + exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + debug "Bop/Oshrxlimm2\n"; + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in + + let op2 = Oaddl in + let i2 = addinst vn op2 [ a1; r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in + + let op3 = Oshrlimm Int.one in + let i3 = addinst vn op3 [ r2' ] dest in + let r3, l3 = extract_arg (i3 :: l2) in + exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) + else ( + debug "Bop/Oshrxlimm3\n"; + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in + + let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in + let i2 = addinst vn op2 [ r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in + + let op3 = Oaddl in + let i3 = addinst vn op3 [ a1; r2' ] r3 in + let r3', l3 = extract_arg (i3 :: l2) in + + let op4 = Oshrlimm n in + let i4 = addinst vn op4 [ r3' ] dest in + let r4, l4 = extract_arg (i4 :: l3) in + exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4); + exp := extract_final vn !exp dest; + was_exp := true + | _ -> ()); if not !was_exp then ( (match i with | Bop (op, args, dest, iinfo) -> -- cgit From b995d85e4df6dc505558342331e34a4487719590 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 22 Jul 2021 14:07:16 +0200 Subject: renaming --- riscV/BTL_SEsimplify.v | 102 ++++++++++++++++++++++++------------------------- 1 file changed, 51 insertions(+), 51 deletions(-) (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index 30468544..0cdea5fe 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -64,44 +64,44 @@ Definition loadimm64 (n: int64) := | Imm64_large imm => fSop (OEloadli imm) fSnil end. -Definition opimm32 (hv1: sval) (n: int) (op: operation) (opimm: int -> operation) := +Definition opimm32 (fsv1: sval) (n: int) (op: operation) (opimm: int -> operation) := match make_immed32 n with | Imm32_single imm => - let lfsv := make_lfsv_single hv1 in + let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm32_pair hi lo => let fsv := load_hilo32 hi lo in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. -Definition opimm64 (hv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := +Definition opimm64 (fsv1: sval) (n: int64) (op: operation) (opimm: int64 -> operation) := match make_immed64 n with | Imm64_single imm => - let lfsv := make_lfsv_single hv1 in + let lfsv := make_lfsv_single fsv1 in fSop (opimm imm) lfsv | Imm64_pair hi lo => let fsv := load_hilo64 hi lo in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv | Imm64_large imm => let fsv := fSop (OEloadli imm) fSnil in - let lfsv := make_lfsv_cmp false hv1 fsv in + let lfsv := make_lfsv_cmp false fsv1 fsv in fSop op lfsv end. -Definition addimm32 (hv1: sval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). -Definition andimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oand OEandiw. -Definition orimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oor OEoriw. -Definition xorimm32 (hv1: sval) (n: int) := opimm32 hv1 n Oxor OExoriw. -Definition sltimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. -Definition sltuimm32 (hv1: sval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. -Definition addimm64 (hv1: sval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). -Definition andimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oandl OEandil. -Definition orimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oorl OEoril. -Definition xorimm64 (hv1: sval) (n: int64) := opimm64 hv1 n Oxorl OExoril. -Definition sltimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. -Definition sltuimm64 (hv1: sval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. +Definition addimm32 (fsv1: sval) (n: int) (or: option oreg) := opimm32 fsv1 n Oadd (OEaddiw or). +Definition andimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oand OEandiw. +Definition orimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oor OEoriw. +Definition xorimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n Oxor OExoriw. +Definition sltimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltw None) OEsltiw. +Definition sltuimm32 (fsv1: sval) (n: int) := opimm32 fsv1 n (OEsltuw None) OEsltiuw. +Definition addimm64 (fsv1: sval) (n: int64) (or: option oreg) := opimm64 fsv1 n Oaddl (OEaddil or). +Definition andimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oandl OEandil. +Definition orimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oorl OEoril. +Definition xorimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n Oxorl OExoril. +Definition sltimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltl None) OEsltil. +Definition sltuimm64 (fsv1: sval) (n: int64) := opimm64 fsv1 n (OEsltul None) OEsltiul. (** ** Comparisons intructions *) Definition cond_int32s (cmp: comparison) (lsv: list_sval) (optR: option oreg) := @@ -339,59 +339,59 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt | Olongconst n, nil => Some (loadimm64 n) | Oaddimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (addimm32 hv1 n None) + let fsv1 := ris_sreg_get hrs a1 in + Some (addimm32 fsv1 n None) | Oaddlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (addimm64 hv1 n None) + let fsv1 := ris_sreg_get hrs a1 in + Some (addimm64 fsv1 n None) | Oandimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (andimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (andimm32 fsv1 n) | Oandlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (andimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (andimm64 fsv1 n) | Oorimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (orimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (orimm32 fsv1 n) | Oorlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (orimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (orimm64 fsv1 n) | Oxorimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (xorimm32 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (xorimm32 fsv1 n) | Oxorlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - Some (xorimm64 hv1 n) + let fsv1 := ris_sreg_get hrs a1 in + Some (xorimm64 fsv1 n) | Ocast8signed, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 24)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 24)) hl') | Ocast16signed, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let fsv := fSop (Oshlimm (Int.repr 16)) lfsv in let hl' := make_lfsv_single fsv in Some (fSop (Oshrimm (Int.repr 16)) hl') | Ocast32unsigned, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in let cast32s_s := fSop Ocast32signed lfsv in let cast32s_l := make_lfsv_single cast32s_s in let sllil_s := fSop (Oshllimm (Int.repr 32)) cast32s_l in let sllil_l := make_lfsv_single sllil_s in Some (fSop (Oshrluimm (Int.repr 32)) sllil_l) | Oshrximm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then - let lhl := make_lfsv_cmp false hv1 hv1 in + let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrx n)) lhl) else if Int.eq n Int.one then let srliw_s := fSop (Oshruimm (Int.repr 31)) lfsv in - let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s := fSop (Oshrimm Int.one) addw_l in @@ -401,22 +401,22 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt let sraiw_s := fSop (Oshrimm (Int.repr 31)) lfsv in let sraiw_l := make_lfsv_single sraiw_s in let srliw_s := fSop (Oshruimm (Int.sub Int.iwordsize n)) sraiw_l in - let srliw_l := make_lfsv_cmp false hv1 srliw_s in + let srliw_l := make_lfsv_cmp false fsv1 srliw_s in let addw_s := fSop Oadd srliw_l in let addw_l := make_lfsv_single addw_s in let sraiw_s' := fSop (Oshrimm n) addw_l in let sraiw_l' := make_lfsv_cmp false sraiw_s' sraiw_s' in Some (fSop (OEmayundef (MUshrx n)) sraiw_l') | Oshrxlimm n, a1 :: nil => - let hv1 := ris_sreg_get hrs a1 in - let lfsv := make_lfsv_single hv1 in + let fsv1 := ris_sreg_get hrs a1 in + let lfsv := make_lfsv_single fsv1 in if Int.eq n Int.zero then - let lhl := make_lfsv_cmp false hv1 hv1 in + let lhl := make_lfsv_cmp false fsv1 fsv1 in Some (fSop (OEmayundef (MUshrxl n)) lhl) else if Int.eq n Int.one then let srlil_s := fSop (Oshrluimm (Int.repr 63)) lfsv in - let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s := fSop (Oshrlimm Int.one) addl_l in @@ -426,7 +426,7 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt let srail_s := fSop (Oshrlimm (Int.repr 63)) lfsv in let srail_l := make_lfsv_single srail_s in let srlil_s := fSop (Oshrluimm (Int.sub Int64.iwordsize' n)) srail_l in - let srlil_l := make_lfsv_cmp false hv1 srlil_s in + let srlil_l := make_lfsv_cmp false fsv1 srlil_s in let addl_s := fSop Oaddl srlil_l in let addl_l := make_lfsv_single addl_s in let srail_s' := fSop (Oshrlimm n) addl_l in -- cgit From 6adfc52c130ee73cf6ee2ee8b85ed8b5e5024a4a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 22 Jul 2021 16:43:14 +0200 Subject: branches expansions support --- riscV/BTL_SEsimplify.v | 240 ++++++++++++++++++++++++++++++++++++++++++++--- riscV/ExpansionOracle.ml | 160 ++++++++++++++++++++++++++++++- 2 files changed, 387 insertions(+), 13 deletions(-) (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index 0cdea5fe..baa4edeb 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -258,6 +258,55 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lsv: list_sval) := let lfsv := make_lfsv_single fsv in if normal' then fsv else fSop (OExoriw Int.one) lfsv. +(** ** Branches instructions *) + +Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbeqw optR + | Cne => CEbnew optR + | Clt => CEbltw optR + | Cle => CEbgew optR + | Cgt => CEbltw optR + | Cge => CEbgew optR + end. + +Definition transl_cbranch_int32u (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbequw optR + | Cne => CEbneuw optR + | Clt => CEbltuw optR + | Cle => CEbgeuw optR + | Cgt => CEbltuw optR + | Cge => CEbgeuw optR + end. + +Definition transl_cbranch_int64s (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbeql optR + | Cne => CEbnel optR + | Clt => CEbltl optR + | Cle => CEbgel optR + | Cgt => CEbltl optR + | Cge => CEbgel optR + end. + +Definition transl_cbranch_int64u (cmp: comparison) (optR: option oreg) := + match cmp with + | Ceq => CEbequl optR + | Cne => CEbneul optR + | Clt => CEbltul optR + | Cle => CEbgeul optR + | Cgt => CEbltul optR + | Cge => CEbgeul optR + end. + +Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lfsv: list_sval) : (condition * list_sval) := + let normal := is_normal_cmp cmp in + let normal' := if cnot then negb normal else normal in + let fsv := fn_cond cmp lfsv in + let lfsv' := make_lfsv_cmp false fsv fsv in + if normal' then ((CEbnew (Some X0_R)), lfsv') else ((CEbeqw (Some X0_R)), lfsv'). + (** Target op simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval := @@ -437,7 +486,109 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): opt end. Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := - None. + match cond, args with + | (Ccomp c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccompu c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccompimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int.eq n Int.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int32s c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int32s c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompuimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int.eq n Int.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int32u c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm32 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int32u c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompl c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccomplu c), (a1 :: a2 :: nil) => + let is_inv := is_inv_cmp_int c in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in + let fsv1 := ris_sreg_get prev a1 in + let fsv2 := ris_sreg_get prev a2 in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (cond, lfsv) + | (Ccomplimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int64s c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int64s c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompluimm c n), (a1 :: nil) => + let is_inv := is_inv_cmp_int c in + let fsv1 := ris_sreg_get prev a1 in + (if Int64.eq n Int64.zero then + let lfsv := make_lfsv_cmp is_inv fsv1 fsv1 in + let cond := transl_cbranch_int64u c (make_optR true is_inv) in + Some (cond, lfsv) + else + let fsv := loadimm64 n in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv in + let cond := transl_cbranch_int64u c (make_optR false is_inv) in + Some (cond, lfsv)) + | (Ccompf c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp false cond_float c lfsv) + | (Cnotcompf c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp true cond_float c lfsv) + | (Ccompfs c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp false cond_single c lfsv) + | (Cnotcompfs c), (f1 :: f2 :: nil) => + let fsv1 := ris_sreg_get prev f1 in + let fsv2 := ris_sreg_get prev f2 in + let is_inv := is_inv_cmp_float c in + let lfsv := make_lfsv_cmp is_inv fsv1 fsv2 in + Some (expanse_cbranch_fp true cond_single c lfsv) + | _, _ => None + end. (** * Auxiliary lemmas on comparisons *) @@ -1706,17 +1857,84 @@ Proof. - eapply simplify_cnotcompfs_correct; eauto. Qed. -(* -Lemma target_cbranch_expanse_correct hrs c l ge sp rs0 m0 st c' l': forall +Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) - (LREF : hsilocal_refines ge sp rs0 m0 hrs st) - (OK: hsok_local ge sp rs0 m0 hrs), - seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = - seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. + (REF: ris_refines ctx hrs st) + (OK: ris_ok ctx hrs), + eval_scondition ctx c' l' = + eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). Proof. - unfold target_cbranch_expanse, seval_condition; simpl. - intros H (LREF & SREF & SREG & SMEM) ?. - congruence. + unfold target_cbranch_expanse, eval_scondition; simpl. + intros H ? ?. inversion REF. + destruct c; try congruence; + repeat (destruct l; simpl in H; try congruence). + 1,2,5,6: + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + try replace (Cle) with (swap_comparison Cge) by auto; + try replace (Clt) with (swap_comparison Cgt) by auto; + try rewrite Val.swap_cmp_bool; trivial; + try rewrite Val.swap_cmpu_bool; trivial; + try rewrite Val.swap_cmpl_bool; trivial; + try rewrite Val.swap_cmplu_bool; trivial. + 1,2,3,4: + try destruct (Int.eq n Int.zero) eqn: EQIMM; + try apply Int.same_if_eq in EQIMM; + try destruct (Int64.eq n Int64.zero) eqn: EQIMM; + try apply Int64.same_if_eq in EQIMM; + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + unfold loadimm32, load_hilo32, Val.cmp, Val.cmpu, zero32; + unfold loadimm64, load_hilo64, Val.cmpl, Val.cmplu, zero64; + intros; try (specialize make_immed32_sound with (n); + destruct (make_immed32 n) eqn:EQMKI); intros; simpl; + intros; try (specialize make_immed64_sound with (n); + destruct (make_immed64 n) eqn:EQMKI); intros; simpl; + try rewrite EQLO; simpl; + try destruct (Int.eq lo Int.zero) eqn:EQLO; + try destruct (Int64.eq lo Int64.zero) eqn:EQLO; + try apply Int.same_if_eq in EQLO; simpl; trivial; + try apply Int64.same_if_eq in EQLO; simpl; trivial; + unfold eval_may_undef; + try erewrite !fsi_sreg_get_correct; eauto; + try rewrite OKv1; simpl; trivial; + 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 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; + try rewrite Int.add_commut, Int.add_zero_l in EQIMM; + try rewrite Int64.add_commut, Int64.add_zero_l in EQIMM; + try rewrite EQIMM; simpl; + try destruct (Archi.ptr64); trivial. + + 1,2,3,4: + destruct c; inv H; simpl; + rewrite !REG_EQ; + try (destruct (eval_smem ctx (si_smem st)) eqn:OKmem; try congruence); + try (destruct (eval_sval ctx (si_sreg st r)) eqn:OKv1; try congruence); + try (destruct (eval_sval ctx (si_sreg st r0)) eqn:OKv2; try congruence); + unfold zero32, zero64, Val.cmpf, Val.cmpfs; + destruct v, v0; simpl; trivial; + try rewrite Float.cmp_ne_eq; + try rewrite Float32.cmp_ne_eq; + try rewrite <- Float.cmp_swap; simpl; + try rewrite <- Float32.cmp_swap; simpl; + try destruct (Float.cmp _ _); simpl; + try destruct (Float32.cmp _ _); simpl; + try rewrite Int.eq_true; simpl; + try rewrite Int.eq_false; try apply Int.one_not_zero; + simpl; trivial. Qed. Global Opaque target_op_simplify. - Global Opaque target_cbranch_expanse.*) +Global Opaque target_cbranch_expanse. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 2a21b7a4..7295ae0d 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -339,6 +339,46 @@ let is_inv_cmp = function Cle | Cgt -> true | _ -> false 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 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int32u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64s is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeql optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgel optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltl optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + let cond_int32s vn is_x0 cmp a1 a2 dest = let optR = make_optR is_x0 (is_inv_cmp cmp) in match cmp with @@ -439,6 +479,40 @@ let cond_single vn cmp f1 f2 dest = | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] +let expanse_cbranchimm_int32s vn cmp a1 n iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cbranch_int32s false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm32 vn r n in + let r', l' = extract_arg l in + cbranch_int32u false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64s true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cbranch_int64s false cmp a1 r' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64u true cmp a1 a1 iinfo succ1 succ2 [] + else + let r = r2pi () in + let l = loadimm64 vn r n in + let r', l' = extract_arg l in + cbranch_int64u false cmp a1 r' iinfo succ1 succ2 l' + let expanse_condimm_int32s vn cmp a1 n dest = if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest else @@ -514,6 +588,16 @@ let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = let r', l = extract_arg insn in addinst vn (OExoriw Int.one) [ r' ] dest :: l +let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 iinfo succ1 succ2 = + 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 vn cmp f1 f2 r in + let r', l = extract_arg insn in + if normal' then + Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l + else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l + (** Return olds args if the CSE numbering is empty *) let get_arguments vn vals args = @@ -529,22 +613,26 @@ let rec gen_btl_list vn exp = inst :: gen_btl_list vn k | [ Sexp (rd, Smove, args, iinfo) ] -> [ Bop (Omove, args, rd, iinfo) ] | [ Scond (cond, args, succ1, succ2, iinfo) ] -> - [ Bcond (cond, args, succ1, succ2, iinfo) ] + let ib = Bcond (cond, args, succ1, succ2, iinfo) in + [ ib ] | [] -> [] | _ -> failwith "write_tree: invalid list" let expanse_list li = debug "#### New block for expansion oracle\n"; let exp = ref [] in + let was_branch = ref false in let was_exp = ref false in let vn = ref (empty_numbering ()) in let rec expanse_list_rec li = match li with | [] -> li | i :: li' -> + was_branch := false; was_exp := false; (if !Clflags.option_fexpanse_rtlcond then match i with + (* Expansion of conditions - Ocmp *) | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) -> debug "Bop/Ccomp\n"; exp := cond_int32s vn false c a1 a2 dest; @@ -605,9 +693,75 @@ let expanse_list li = exp := expanse_cond_fp vn true cond_single c f1 f2 dest; exp := extract_final vn !exp dest; was_exp := true + (* Expansion of branches - Ccomp *) + | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompuimm\n"; + exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompl\n"; + exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplu\n"; + exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplimm\n"; + exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompluimm\n"; + exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompf\n"; + exp := + expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompf\n"; + exp := + expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompfs\n"; + exp := + expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompfs\n"; + exp := + expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true | _ -> ()); (if !Clflags.option_fexpanse_others && not !was_exp then match i with + (* Others expansions *) | Bop (Ofloatconst f, nil, dest, iinfo) -> ( match make_immed64 (Floats.Float.to_bits f) with | Imm64_single _ | Imm64_large _ -> () @@ -814,7 +968,9 @@ let expanse_list li = (* TODO gourdinl empty numb BF? vn := empty_numbering ()*) | _ -> ()); i :: expanse_list_rec li') - else gen_btl_list vn (List.rev !exp) @ expanse_list_rec li' + else + let hd = gen_btl_list vn (List.rev !exp) in + hd @ expanse_list_rec li' in expanse_list_rec li -- cgit From 056658bd2986d9e12ac07a54d25c08eb8a62ff60 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 28 Jul 2021 10:32:09 +0200 Subject: remove todos, clean --- riscV/BTL_SEsimplify.v | 25 ++++--------------------- riscV/ExpansionOracle.ml | 1 - riscV/RTLpathSE_simplify.v | 23 ++++------------------- 3 files changed, 8 insertions(+), 41 deletions(-) (limited to 'riscV') diff --git a/riscV/BTL_SEsimplify.v b/riscV/BTL_SEsimplify.v index baa4edeb..ab01f7ac 100644 --- a/riscV/BTL_SEsimplify.v +++ b/riscV/BTL_SEsimplify.v @@ -854,23 +854,6 @@ Proof. Qed. Local Hint Resolve optbool_mktotal: core. -(* TODO gourdinl move to common/Values ? *) -Theorem swap_cmpf_bool: - forall c x y, - Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. -Qed. -Local Hint Resolve swap_cmpf_bool: core. - -Theorem swap_cmpfs_bool: - forall c x y, - Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. -Qed. -Local Hint Resolve swap_cmpfs_bool: core. - (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) @@ -1140,9 +1123,9 @@ Proof. rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.cmpf. - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpf_bool; trivial. + rewrite Val.swap_cmpf_bool; trivial. - replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpf_bool; trivial. + rewrite Val.swap_cmpf_bool; trivial. Qed. Lemma simplify_cnotcompf_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) @@ -1181,9 +1164,9 @@ Proof. rewrite !REG_EQ, OKv1, OKv2; trivial; unfold Val.cmpfs. - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpfs_bool; trivial. + rewrite Val.swap_cmpfs_bool; trivial. - replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpfs_bool; trivial. + rewrite Val.swap_cmpfs_bool; trivial. Qed. Lemma simplify_cnotcompfs_correct (ctx: iblock_exec_context) (hrs: ristate) (st: sistate) diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 7295ae0d..49ca7e96 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -24,7 +24,6 @@ open Asmgen (** Tools *) -(** TODO gourdinl move to BTLcommonaux *) let rec iblock_to_list ib = match ib with | Bseq (ib1, ib2) -> iblock_to_list ib1 @ iblock_to_list ib2 diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 2739bc5d..2370ad66 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -838,21 +838,6 @@ Proof. destruct v; simpl; auto. Qed. -(* TODO gourdinl move to common/Values ? *) -Theorem swap_cmpf_bool: - forall c x y, - Val.cmpf_bool (swap_comparison c) x y = Val.cmpf_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float.cmp_swap. auto. -Qed. - -Theorem swap_cmpfs_bool: - forall c x y, - Val.cmpfs_bool (swap_comparison c) x y = Val.cmpfs_bool c y x. -Proof. - destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. -Qed. - (** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall @@ -1239,9 +1224,9 @@ Proof. unfold Val.cmpf. - apply xor_neg_eqne_cmpf. - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpf_bool; trivial. + rewrite Val.swap_cmpf_bool; trivial. - replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpf_bool; trivial. + rewrite Val.swap_cmpf_bool; trivial. Qed. Lemma simplify_cnotcompf_correct ge sp hst st c r r0 rs0 m0 v v0: forall @@ -1290,9 +1275,9 @@ Proof. unfold Val.cmpfs. - apply xor_neg_eqne_cmpfs. - replace (Clt) with (swap_comparison Cgt) by auto; - rewrite swap_cmpfs_bool; trivial. + rewrite Val.swap_cmpfs_bool; trivial. - replace (Cle) with (swap_comparison Cge) by auto; - rewrite swap_cmpfs_bool; trivial. + rewrite Val.swap_cmpfs_bool; trivial. Qed. Lemma simplify_cnotcompfs_correct ge sp hst st c r r0 rs0 m0 v v0: forall -- cgit