From dd4767e17235adb5de922626ed1fea15f4eb9e3b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Apr 2021 23:37:22 +0200 Subject: Important commit on expansions' mini CSE, and a draft for addptrofs --- riscV/Asm.v | 2 +- riscV/Asmgen.v | 58 ++- riscV/Asmgenproof.v | 3 +- riscV/Asmgenproof1.v | 56 ++- riscV/ExpansionOracle.ml | 1106 ++++++++++++++++++++++++++------------------ riscV/NeedOp.v | 6 +- riscV/Op.v | 296 +++++++----- riscV/PrintOp.ml | 17 +- riscV/RTLpathSE_simplify.v | 156 +++---- riscV/ValueAOp.v | 133 +++--- 10 files changed, 1077 insertions(+), 756 deletions(-) (limited to 'riscV') diff --git a/riscV/Asm.v b/riscV/Asm.v index 5d3518f2..a16f57b5 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -982,6 +982,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pbuiltin ef args res => Stuck (**r treated specially below *) + | Pnop => Next (nextinstr rs) m (**r Pnop is used by an oracle during expansion *) (** The following instructions and directives are not generated directly by Asmgen, so we do not model them. *) @@ -1002,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfmsubd _ _ _ _ | Pfnmaddd _ _ _ _ | Pfnmsubd _ _ _ _ - | Pnop => Stuck end. diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 88d4f73f..ff5d1a6e 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -204,19 +204,23 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := | Cgt => (Pflts rd fs2 fs1, true) | Cge => (Pfles rd fs2 fs1, true) end. - + +(** Functions to select a special register according to the op "oreg" argument from RTL *) + Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) := match optR with | None => (r1, r2) | Some X0_L => (X0, r1) | Some X0_R => (r1, X0) + | Some SP_S => (X SP, r1) end. -Definition get_opimmR0 (rd: ireg) (opi: opimm) := - match opi with - | OPimmADD i => Paddiw rd X0 i - | OPimmADDL i => Paddil rd X0 i - end. +Definition get_oreg (optR: option oreg) (r: ireg0) := + match optR with + | Some SP_S => X SP + | Some X0_L | Some X0_R => X0 + | _ => r + end. Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := @@ -785,9 +789,8 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k - | OEimmR0 opi, nil => - do rd <- ireg_of res; - OK (get_opimmR0 rd opi :: k) + + (* Instructions expanded in RTL *) | OEseqw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -839,10 +842,21 @@ Definition transl_op | OEluiw n, nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) - | OEaddiw n, a1 :: nil => + | OEaddiw optR n, nil => do rd <- ireg_of res; - do rs <- ireg_of a1; + let rs := get_oreg optR X0 in OK (Paddiw rd rs n :: k) + | OEaddiw (Some SP_S) n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + if Int.eq n Int.zero then + OK (Paddw rd SP rs :: k) + else Error (msg "Asmgen.transl_op") + | OEaddiw optR n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + let rs' := get_oreg optR rs in + OK (Paddiw rd rs' n :: k) | OEandiw n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -902,10 +916,21 @@ Definition transl_op | OEluil n, nil => do rd <- ireg_of res; OK (Pluil rd n :: k) - | OEaddil n, a1 :: nil => + | OEaddil optR n, nil => do rd <- ireg_of res; - do rs <- ireg_of a1; + let rs := get_oreg optR X0 in OK (Paddil rd rs n :: k) + | OEaddil (Some SP_S) n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + if Int64.eq n Int64.zero then + OK (Paddl rd SP rs :: k) + else Error (msg "Asmgen.transl_op") + | OEaddil optR n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + let rs' := get_oreg optR rs in + OK (Paddil rd rs' n :: k) | OEandil n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -947,6 +972,13 @@ Definition transl_op do r1 <- freg_of f1; do r2 <- freg_of f2; OK (Pfles rd r1 r2 :: k) + | OEmayundef _, a1 :: a2 :: nil => + do rd <- ireg_of res; + do r2 <- ireg_of a2; + if ireg_eq rd r2 then + OK (Pnop :: k) + else + OK (Pmv rd r2 :: k) | Obits_of_single, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 101bfa9c..bf9ede7f 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -308,7 +308,8 @@ Opaque Int.eq. - apply opimm64_label; intros; exact I. - destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. - eapply transl_cond_op_label; eauto. -- destruct opi; simpl; TailNoLabel. +- destruct optR as [[]|]; simpl in *; TailNoLabel. +- destruct optR as [[]|]; simpl in *; TailNoLabel. - destruct optR as [[]|]; simpl in *; TailNoLabel. - destruct optR as [[]|]; simpl in *; TailNoLabel. - destruct optR as [[]|]; simpl in *; TailNoLabel. diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 1e17c4e2..cbe68577 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -529,31 +529,37 @@ Proof. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; @@ -591,31 +597,37 @@ Proof. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2; + try (destruct (rs x); simpl in EVAL'; discriminate; fail); eexists; eexists; eauto; split; constructor; simpl in *; try rewrite EVAL'; auto. Qed. @@ -1262,12 +1274,7 @@ Opaque Int.eq. { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) - { unfold get_opimmR0; destruct opi; simpl; - econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl. - try rewrite Int.add_commut; auto. - try rewrite Int64.add_commut; auto. } - 7,8,9,16,17,18: + 8,9,17,18: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; try destruct (rs x0); try rewrite Int64.add_commut; @@ -1276,12 +1283,41 @@ Opaque Int.eq. try rewrite Int.and_commut; auto; try rewrite Int64.or_commut; try rewrite Int.or_commut; auto. - 1-12: - destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3; + 1-14: + destruct optR as [[]|]; try discriminate; + try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl); + unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2; + try destruct (Int.eq _ _) eqn:A; try inv H0; + try destruct (Int64.eq _ _) eqn:A; try inv H1; econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; - destruct (rs x0); auto; - destruct (rs x1); auto. + try apply Int.same_if_eq in A; subst; + try apply Int64.same_if_eq in A; subst; + unfold get_sp; + try destruct (rs x0); auto; + try destruct (rs x1); auto; + try destruct (rs X2); auto; + try destruct Archi.ptr64 eqn:B; + try fold (Val.add (Vint Int.zero) (get_sp (rs X2))); + try fold (Val.addl (Vlong Int64.zero) (get_sp (rs X2))); + try rewrite Val.add_commut; auto; + try rewrite Val.addl_commut; auto; + try rewrite Int.add_commut; auto; + try rewrite Int64.add_commut; auto; + replace (Ptrofs.of_int Int.zero) with (Ptrofs.zero) by auto; + replace (Ptrofs.of_int64 Int64.zero) with (Ptrofs.zero) by auto; + try rewrite Ptrofs.add_zero; auto. + (* mayundef *) + { destruct (ireg_eq x x0); inv EQ2; + econstructor; split; + try apply exec_straight_one; simpl; eauto; + split; unfold eval_may_undef; + destruct mu eqn:EQMU; simpl; intros; Simpl; auto. + all: + destruct (rs (preg_of m0)) eqn:EQM0; simpl; auto; + destruct (rs x0); simpl; auto; Simpl; + try destruct (Int.ltu _ _); simpl; + Simpl; auto. } (* select *) { econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 16f1ee4b..e0c9b9b2 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -17,15 +17,19 @@ open Maps open RTL open Op open Asmgen -open DebugPrint open RTLpath open! Integers open Camlcoq open Option +open AST +open Printf -type sop = Sop of operation * P.t list +(** Mini CSE (a dynamic numbering is applied during expansion. + The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) -type sval = Si of RTL.instruction | Sr of P.t +let exp_debug = false + +(** Managing virtual registers and node index *) let reg = ref 1 @@ -45,6 +49,181 @@ 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 = + if exp_debug then eprintf "["; + List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l; + if exp_debug then eprintf "]\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 -> + if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v; + v + | None -> + let n = !vn.nnext in + if exp_debug then eprintf "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 -> + if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; + let old_regs = get_nval_ornil vn v in + if exp_debug then eprintf "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 -> + if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd) + +let update_reg vn rd v = + if exp_debug then eprintf "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 = + if exp_debug then eprintf "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 -> + if exp_debug then eprintf "addrhs: Some v=%d\n" vres; + Hashtbl.replace !vn.nreg rd vres; + update_reg vn rd vres + | None -> + let n = !vn.nnext in + if exp_debug then eprintf "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 = + if exp_debug then eprintf "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 = + if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v; + match Hashtbl.find !vn.nval v with + | [] -> None + | r :: rs -> + if exp_debug then eprintf "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 -> + if exp_debug then eprintf "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 @@ -59,152 +238,109 @@ type immt = | Sltil | Sltiul -let find_or_addnmove op args rd succ map_consts not_final = - let sop = Sop (op, args) in - match Hashtbl.find_opt map_consts sop with - | Some r -> - if not_final then node := !node - 1; - Sr (P.of_int r) - | None -> - if (not (List.exists (fun a -> a = rd) args)) && not_final then - Hashtbl.add map_consts sop (p2i rd); - Si (Iop (op, args, rd, succ)) - -let build_head_tuple head sv = - match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r) - -let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r - -let unzip_head_tuple_move ht r succ = - match ht with - | l, Some r' -> - if r' != r then [ Iop (Omove, [ r' ], r, succ) ] else [ Inop succ ] - | l, None -> l - -let build_full_ilist op args dest succ hd k map_consts = - let sv = find_or_addnmove op args dest succ map_consts false in - let ht = build_head_tuple hd sv in - unzip_head_tuple_move ht dest succ @ k - -let load_hilo32 dest hi lo succ map_consts not_final = +let load_hilo32 vn dest hi lo = let op1 = OEluiw hi in - if Int.eq lo Int.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts not_final in - build_head_tuple [] sv + if Int.eq lo Int.zero then [ addinst vn op1 [] dest ] else let r = r2pi () in - let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in - let ht1 = build_head_tuple [] sv1 in - let r' = unzip_head_tuple ht1 r in - let op2 = OEaddiw lo in - let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in - build_head_tuple (fst ht1) sv2 - -let load_hilo64 dest hi lo succ map_consts not_final = + 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 - let sv = find_or_addnmove op1 [] dest succ map_consts not_final in - build_head_tuple [] sv + if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ] else let r = r2pi () in - let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in - let ht1 = build_head_tuple [] sv1 in - let r' = unzip_head_tuple ht1 r in - let op2 = OEaddil lo in - let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in - build_head_tuple (fst ht1) sv2 - -let loadimm32 dest n succ map_consts not_final = + 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 = OEimmR0 (OPimmADD imm) in - let sv = find_or_addnmove op1 [] dest succ map_consts not_final in - build_head_tuple [] sv - | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final + let op1 = OEaddiw (Some X0_R, imm) in + [ addinst vn op1 [] dest ] + | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo -let loadimm64 dest n succ map_consts not_final = +let loadimm64 vn dest n = match make_immed64 n with | Imm64_single imm -> - let op1 = OEimmR0 (OPimmADDL imm) in - let sv = find_or_addnmove op1 [] dest succ map_consts not_final in - build_head_tuple [] sv - | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final + 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 - let sv = find_or_addnmove op1 [] dest succ map_consts not_final in - build_head_tuple [] sv + [ addinst vn op1 [] dest ] -let get_opimm imm = function - | Addiw -> OEaddiw imm +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 imm + | Addil -> OEaddil (optR, imm) | Andil -> OEandil imm | Oril -> OEoril imm | Xoril -> OExoril imm | Sltil -> OEsltil imm | Sltiul -> OEsltiul imm -let opimm32 a1 dest n succ k op opimm map_consts = +let opimm32 vn a1 dest n optR op opimm = match make_immed32 n with - | Imm32_single imm -> - build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts + | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] | Imm32_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo32 r hi lo (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts + 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 a1 dest n succ k op opimm map_consts = +let opimm64 vn a1 dest n optR op opimm = match make_immed64 n with - | Imm64_single imm -> - build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts + | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] | Imm64_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo64 r hi lo (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts + 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 inode = n2pi () in - let sv = find_or_addnmove op1 [] r inode map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts + 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 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k Oadd Addiw map_consts +let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw -let andimm32 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k Oand Andiw map_consts +let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw -let orimm32 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k Oor Oriw map_consts +let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw -let xorimm32 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k Oxor Xoriw map_consts +let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw -let sltimm32 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts +let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw -let sltuimm32 a1 dest n succ k map_consts = - opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts +let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw -let addimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oaddl Addil +let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil -let andimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oandl Andil +let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil -let orimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oorl Oril +let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril -let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril +let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril -let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil +let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil -let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul +let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul let is_inv_cmp = function Cle | Cgt -> true | _ -> false @@ -214,276 +350,288 @@ let make_optR is_x0 is_inv = 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 -> Icond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k + | 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 -> Icond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k + | 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 -> Icond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k + | 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 -> Icond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Icond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Icond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Icond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Icond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Icond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = + | 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 -> [ Iop (OEseqw optR, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnew optR, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltw optR, [ a1; a2 ], dest, succ) ] + | 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 sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltw optR, [ a2; a1 ], dest, succ) ] + 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 sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + let 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 is_x0 cmp a1 a2 dest tmp_reg succ map_consts = +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 -> [ Iop (OEsequw optR, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneuw optR, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltuw optR, [ a1; a2 ], dest, succ) ] + | 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 sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltuw optR, [ a2; a1 ], dest, succ) ] + 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 sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + let 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 is_x0 cmp a1 a2 dest tmp_reg succ map_consts = +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 -> [ Iop (OEseql optR, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsnel optR, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltl optR, [ a1; a2 ], dest, succ) ] + | 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 sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltl optR, [ a2; a1 ], dest, succ) ] + 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 sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + let 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 is_x0 cmp a1 a2 dest tmp_reg succ map_consts = +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 -> [ Iop (OEsequl optR, [ a1; a2 ], dest, succ) ] - | Cne -> [ Iop (OEsneul optR, [ a1; a2 ], dest, succ) ] - | Clt -> [ Iop (OEsltul optR, [ a1; a2 ], dest, succ) ] + | 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 sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] - | Cgt -> [ Iop (OEsltul optR, [ a2; a1 ], dest, succ) ] + 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 sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in - fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + let 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 cmp f1 f2 dest succ map_consts = +let cond_float vn cmp f1 f2 dest = match cmp with - | Ceq -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ] - | Cne -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ] - | Clt -> [ Iop (OEfltd, [ f1; f2 ], dest, succ) ] - | Cle -> [ Iop (OEfled, [ f1; f2 ], dest, succ) ] - | Cgt -> [ Iop (OEfltd, [ f2; f1 ], dest, succ) ] - | Cge -> [ Iop (OEfled, [ f2; f1 ], dest, succ) ] - -let cond_single cmp f1 f2 dest succ map_consts = + | 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 -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ] - | Cne -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ] - | Clt -> [ Iop (OEflts, [ f1; f2 ], dest, succ) ] - | Cle -> [ Iop (OEfles, [ f1; f2 ], dest, succ) ] - | Cgt -> [ Iop (OEflts, [ f2; f1 ], dest, succ) ] - | Cge -> [ Iop (OEfles, [ f2; f1 ], dest, succ) ] - -let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts = - if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k + | 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 ht = loadimm32 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k + 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 cmp a1 n info succ1 succ2 k map_consts = - if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k +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 ht = loadimm32 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k + 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 cmp a1 n info succ1 succ2 k map_consts = - if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k +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 ht = loadimm64 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k + 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 cmp a1 n info succ1 succ2 k map_consts = - if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k +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 ht = loadimm64 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k - -let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None + let 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 cmp a1 n dest succ map_consts = - if Int.eq n Int.zero then - let tmp_reg = get_tmp_reg cmp in - cond_int32s true cmp a1 a1 dest tmp_reg succ map_consts +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 - xorimm32 a1 r n (n2pi ()) - (cond_int32s true cmp r r dest None succ map_consts) - map_consts - | Clt -> sltimm32 a1 dest n succ [] map_consts + 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 ht = loadimm32 dest Int.one succ map_consts false in - fst ht - else sltimm32 a1 dest (Int.add n Int.one) succ [] map_consts + let 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 tmp_reg = get_tmp_reg cmp in - let ht = loadimm32 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ map_consts - -let expanse_condimm_int32u cmp a1 n dest succ map_consts = - let tmp_reg = get_tmp_reg cmp in - if Int.eq n Int.zero then - cond_int32u true cmp a1 a1 dest tmp_reg succ map_consts + 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 a1 dest n succ [] map_consts + | Clt -> sltuimm32 vn a1 dest n | _ -> let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ map_consts + 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 cmp a1 n dest succ map_consts = - if Int64.eq n Int64.zero then - let tmp_reg = get_tmp_reg cmp in - cond_int64s true cmp a1 a1 dest tmp_reg succ map_consts +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 - xorimm64 a1 r n (n2pi ()) - (cond_int64s true cmp r r dest None succ map_consts) - map_consts - | Clt -> sltimm64 a1 dest n succ [] map_consts + 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 ht = loadimm32 dest Int.one succ map_consts false in - fst ht - else sltimm64 a1 dest (Int64.add n Int64.one) succ [] map_consts + let 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 tmp_reg = get_tmp_reg cmp in - let ht = loadimm64 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ map_consts + 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 cmp a1 n dest succ map_consts = - let tmp_reg = get_tmp_reg cmp in - if Int64.eq n Int64.zero then - cond_int64u true cmp a1 a1 dest tmp_reg succ map_consts +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 a1 dest n succ [] map_consts + | Clt -> sltuimm64 vn a1 dest n | _ -> let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts true in - let r' = unzip_head_tuple ht r in - fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ map_consts + 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 cnot fn_cond cmp f1 f2 dest succ map_consts = +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 succ' = if normal' then succ else n2pi () in - let insn = fn_cond cmp f1 f2 dest succ' map_consts in + let insn = fn_cond vn cmp f1 f2 dest in if normal' then insn - else build_full_ilist (OExoriw Int.one) [ dest ] dest succ insn [] map_consts + else + let r', l = extract_arg insn in + addinst vn (OExoriw Int.one) [ r' ] dest :: l -let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts = +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 = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in - insn - :: - (if normal' then [ Icond (CEbnew (Some X0_R), [ r; r ], succ1, succ2, info) ] - else [ Icond (CEbeqw (Some X0_R), [ r; r ], succ1, succ2, info) ]) + let 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 + +let addptrofs vn n dest = + if Ptrofs.eq_dec n Ptrofs.zero then [ addinst vn OEmoveSP [] dest ] + else if Archi.ptr64 then + match make_immed64 (Ptrofs.to_int64 n) with + | Imm64_single imm -> [ addinst vn (OEaddil (Some SP_S, imm)) [] 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 + addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: 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 + addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l + else + match make_immed32 (Ptrofs.to_int n) with + | Imm32_single imm -> [ addinst vn (OEaddiw (Some SP_S, imm)) [] 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 + addinst vn (OEaddiw (Some SP_S, Int.zero)) [ r' ] dest :: l' + +(** Form a list containing both sources and destination regs of an instruction *) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -501,11 +649,11 @@ let get_regs_inst = function | Ireturn (Some r) -> [ r ] | _ -> [] -let write_initial_node initial code' new_order = - code' := PTree.set initial (Inop (n2p ())) !code'; - new_order := initial :: !new_order +(** Modify pathmap according to the size of the expansion list *) let write_pathmap initial esize pm' = + if exp_debug then + eprintf "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' = @@ -518,22 +666,51 @@ let write_pathmap initial esize pm' = in pm' := PTree.set initial path' !pm' -let rec write_tree exp initial current code' new_order fturn = - (*Printf.eprintf "wt: node is %d\n" !node;*) +(** 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 = + if exp_debug then eprintf "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 - | inst :: k -> - (*let open PrintRTL in*) - (*print_instruction stderr (target_node, inst);*) - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order; - write_tree k initial next_node code' new_order false + | 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_flag := true;*) + if exp_debug then eprintf "#### New superblock for expansion oracle\n"; let new_order = ref [] in let liveins = ref sb.liveins in let exp = ref [] in @@ -541,336 +718,342 @@ let expanse (sb : superblock) code pm = let was_exp = ref false in let code' = ref code in let pm' = ref pm in - let map_consts = Hashtbl.create 100 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 exp_debug then eprintf "We are checking node %d\n" (p2i n); (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"; - let tmp_reg = get_tmp_reg c in - exp := cond_int32s false c a1 a2 dest tmp_reg succ map_consts; + if exp_debug then eprintf "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"; - let tmp_reg = get_tmp_reg c in - exp := cond_int32u false c a1 a2 dest tmp_reg succ map_consts; + if exp_debug then eprintf "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 c a1 imm dest succ map_consts; + if exp_debug then eprintf "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 c a1 imm dest succ map_consts; + if exp_debug then eprintf "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"; - let tmp_reg = get_tmp_reg c in - exp := cond_int64s false c a1 a2 dest tmp_reg succ map_consts; + if exp_debug then eprintf "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"; - let tmp_reg = get_tmp_reg c in - exp := cond_int64u false c a1 a2 dest tmp_reg succ map_consts; + if exp_debug then eprintf "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 c a1 imm dest succ map_consts; + if exp_debug then eprintf "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 c a1 imm dest succ map_consts; + if exp_debug then eprintf "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 false cond_float c f1 f2 dest succ map_consts; + if exp_debug then eprintf "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 true cond_float c f1 f2 dest succ map_consts; + if exp_debug then eprintf "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 false cond_single c f1 f2 dest succ map_consts; + if exp_debug then eprintf "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 true cond_single c f1 f2 dest succ map_consts; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "Icond/Ccompu\n"; exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompimm\n"; - exp := - expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [] map_consts; + if exp_debug then eprintf "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 c a1 imm info succ1 succ2 [] map_consts; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "Icond/Ccomplu\n"; exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; was_branch := true; was_exp := true | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplimm\n"; - exp := - expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [] map_consts; + if exp_debug then eprintf "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 c a1 imm info succ1 succ2 [] map_consts; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "Icond/Ccompf\n"; exp := - expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 - map_consts; + 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 true cond_float c f1 f2 info succ1 succ2 - map_consts; + if exp_debug then eprintf "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"; + if exp_debug then eprintf "Icond/Ccompfs\n"; exp := - expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 - map_consts; + 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"; + if exp_debug then eprintf "Icond/Cnotcompfs\n"; exp := - expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 - map_consts; + 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 - (* Expansion of fp constants *) | Iop (Ofloatconst f, nil, dest, succ) -> - debug "Iop/Ofloatconst\n"; + if exp_debug then eprintf "Iop/Ofloatconst\n"; let r = r2pi () in - let ht = - loadimm64 r (Floats.Float.to_bits f) (n2pi ()) map_consts true - in - let r' = unzip_head_tuple ht r in - exp := - build_full_ilist Ofloat_of_bits [ r' ] dest succ (fst ht) [] - map_consts; + let l = loadimm64 vn r (Floats.Float.to_bits f) 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) -> - debug "Iop/Osingleconst\n"; + if exp_debug then eprintf "Iop/Osingleconst\n"; let r = r2pi () in - let ht = - loadimm32 r (Floats.Float32.to_bits f) (n2pi ()) map_consts true - in - let r' = unzip_head_tuple ht r in - exp := - build_full_ilist Osingle_of_bits [ r' ] dest succ (fst ht) [] - map_consts; + let l = loadimm32 vn r (Floats.Float32.to_bits f) 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"; - let ht = loadimm32 dest n succ map_consts false in - exp := unzip_head_tuple_move ht dest succ; + if exp_debug then eprintf "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"; - let ht = loadimm64 dest n succ map_consts false in - exp := unzip_head_tuple_move ht dest succ; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "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 a1 dest n succ [] map_consts; + if exp_debug then eprintf "Iop/Oorlimm\n"; + exp := orimm64 vn a1 dest n; + exp := extract_final vn !exp dest succ; was_exp := true | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - debug "Iop/cast8signed"; + if exp_debug then eprintf "Iop/cast8signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 24)) in let r = r2pi () in - let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in + let i1 = addinst vn op [ a1 ] r in + let r', l = extract_arg [ i1 ] in exp := - build_full_ilist - (Oshrimm (Int.repr (Z.of_sint 24))) - [ r' ] dest succ (fst ht) [] map_consts; + 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/cast8signed"; + if exp_debug then eprintf "Iop/cast16signed\n"; let op = Oshlimm (Int.repr (Z.of_sint 16)) in let r = r2pi () in - let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in - let ht = build_head_tuple [] sv in - let r' = unzip_head_tuple ht r in + let i1 = addinst vn op [ a1 ] r in + let r', l = extract_arg [ i1 ] in exp := - build_full_ilist - (Oshrimm (Int.repr (Z.of_sint 16))) - [ r' ] dest succ (fst ht) [] map_consts; + 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"; - let n2 = n2pi () in - let n1 = n2pi () in + if exp_debug then eprintf "Iop/Ocast32unsigned\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Ocast32signed in - let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in - let ht1 = build_head_tuple [] sv1 in - let r1' = unzip_head_tuple ht1 r1 in + let 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 sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in - let ht2 = build_head_tuple (fst ht1) sv2 in - let r2' = unzip_head_tuple ht2 r2 in + let 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 := build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + exp := addinst vn op3 [ r2' ] dest :: l2; + exp := extract_final vn !exp dest succ; + was_exp := true | Iop (Oshrximm n, a1 :: nil, dest, succ) -> - debug "Iop/Oshrximm"; - if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] - else if Int.eq n Int.one then - let n2 = n2pi () in - let n1 = n2pi () in + if Int.eq n Int.zero then ( + if exp_debug then eprintf "Iop/Oshrximm1\n"; + exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + if exp_debug then eprintf "Iop/Oshrximm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in - let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in - let ht1 = build_head_tuple [] sv1 in - let r1' = unzip_head_tuple ht1 r1 in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in let op2 = Oadd in - let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in - let ht2 = build_head_tuple (fst ht1) sv2 in - let r2' = unzip_head_tuple ht2 r2 in + let i2 = addinst vn op2 [ a1; r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in let op3 = Oshrimm Int.one in - exp := - build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts - else - let n3 = n2pi () in - let n2 = n2pi () in - let n1 = n2pi () in + let 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 ( + if exp_debug then eprintf "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 sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in - let ht1 = build_head_tuple [] sv1 in - let r1' = unzip_head_tuple ht1 r1 in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in let op2 = Oshruimm (Int.sub Int.iwordsize n) in - let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in - let ht2 = build_head_tuple (fst ht1) sv2 in - let r2' = unzip_head_tuple ht2 r2 in + let i2 = addinst vn op2 [ r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in let op3 = Oadd in - let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in - let ht3 = build_head_tuple (fst ht2) sv3 in - let r3' = unzip_head_tuple ht3 r3 in + let i3 = addinst vn op3 [ a1; r2' ] r3 in + let r3', l3 = extract_arg (i3 :: l2) in let op4 = Oshrimm n in - exp := - build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + 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) -> - debug "Iop/Oshrxlimm"; - if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] - else if Int.eq n Int.one then - let n2 = n2pi () in - let n1 = n2pi () in + if Int.eq n Int.zero then ( + if exp_debug then eprintf "Iop/Oshrxlimm1\n"; + exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + if exp_debug then eprintf "Iop/Oshrxlimm2\n"; let r1 = r2pi () in let r2 = r2pi () in let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in - let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in - let ht1 = build_head_tuple [] sv1 in - let r1' = unzip_head_tuple ht1 r1 in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in let op2 = Oaddl in - let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in - let ht2 = build_head_tuple (fst ht1) sv2 in - let r2' = unzip_head_tuple ht2 r2 in + let i2 = addinst vn op2 [ a1; r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in let op3 = Oshrlimm Int.one in - exp := - build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts - else - let n3 = n2pi () in - let n2 = n2pi () in - let n1 = n2pi () in + let 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 ( + if exp_debug then eprintf "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 sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in - let ht1 = build_head_tuple [] sv1 in - let r1' = unzip_head_tuple ht1 r1 in + let i1 = addinst vn op1 [ a1 ] r1 in + let r1', l1 = extract_arg [ i1 ] in let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in - let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in - let ht2 = build_head_tuple (fst ht1) sv2 in - let r2' = unzip_head_tuple ht2 r2 in + let i2 = addinst vn op2 [ r1' ] r2 in + let r2', l2 = extract_arg (i2 :: l1) in let op3 = Oaddl in - let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in - let ht3 = build_head_tuple (fst ht2) sv3 in - let r3' = unzip_head_tuple ht3 r3 in + let i3 = addinst vn op3 [ a1; r2' ] r3 in + let r3', l3 = extract_arg (i3 :: l2) in let op4 = Oshrlimm n in - exp := - build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + 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 + (*| Iop (Oaddrstack n, nil, dest, succ) ->*) + (*if exp_debug then eprintf "Iop/Oaddrstack\n";*) + (*exp := addptrofs vn n dest;*) + (*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 ( + node := !node + List.length !exp - 1; (if !was_branch && List.length !exp > 1 then let lives = PTree.get n !liveins in match lives with @@ -880,14 +1063,15 @@ let expanse (sb : superblock) code pm = liveins := PTree.remove n !liveins | _ -> ()); write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree !exp n !node code' new_order true) + 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; - (*debug_flag := false;*) (!code', !pm') +(** Compute the last used node and reg indexs *) + let rec find_last_node_reg = function | [] -> () | (pc, i) :: k -> diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v index 715951a0..d0ca5bb2 100644 --- a/riscV/NeedOp.v +++ b/riscV/NeedOp.v @@ -87,7 +87,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv) | Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv) | Ocmp c => needs_of_condition c - | OEimmR0 _ => op1 (default nv) + | OEmoveSP => nil | OEseqw _ => op2 (default nv) | OEsnew _ => op2 (default nv) | OEsequw _ => op2 (default nv) @@ -98,7 +98,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiuw _ => op1 (default nv) | OExoriw _ => op1 (bitwise nv) | OEluiw _ => op1 (default nv) - | OEaddiw _ => op1 (default nv) + | OEaddiw _ _ => op1 (default nv) | OEandiw n => op1 (andimm nv n) | OEoriw n => op1 (orimm nv n) | OEseql _ => op2 (default nv) @@ -111,7 +111,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | OEsltiul _ => op1 (default nv) | OExoril _ => op1 (default nv) | OEluil _ => op1 (default nv) - | OEaddil _ => op1 (default nv) + | OEaddil _ _ => op1 (default nv) | OEandil _ => op1 (default nv) | OEoril _ => op1 (default nv) | OEloadli _ => op1 (default nv) diff --git a/riscV/Op.v b/riscV/Op.v index a8ff3666..9d1826ac 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -38,10 +38,12 @@ Set Implicit Arguments. (** Conditions (boolean-valued operators). *) -(* Type to modelize the use of a special register in arith operations *) +(** Type to modelize the use of a special register in arith operations *) + Inductive oreg: Type := | X0_L: oreg - | X0_R: oreg. + | X0_R: oreg + | SP_S: oreg. Inductive condition : Type := | Ccomp (c: comparison) (**r signed integer comparison *) @@ -75,17 +77,13 @@ Inductive condition : Type := | CEbgeul (optR: option oreg). (**r branch-if-greater-or-equal unsigned *) (* This type will define the eval function of a OEmayundef operation. *) + Inductive mayundef: Type := | MUint: mayundef | MUlong: mayundef | MUshrx: int -> mayundef | MUshrxl: int -> mayundef. -(* Type for allowing a single RTL constructor to perform an arith operation between an immediate and X0 *) -Inductive opimm: Type := - | OPimmADD: int -> opimm - | OPimmADDL: int64 -> opimm. - (** Arithmetic and logical operations. In the descriptions, [rd] is the result of the operation and [r1], [r2], etc, are the arguments. *) @@ -189,41 +187,41 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) (* Expansed conditions *) - | OEimmR0 (opi: opimm) + | OEmoveSP | OEseqw (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) | OEsnew (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) | OEsequw (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) | OEsneuw (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) | OEsltw (optR: option oreg) (**r set-less-than *) | OEsltuw (optR: option oreg) (**r set-less-than unsigned *) - | OEsltiw (n: int) (**r set-less-than immediate *) - | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) - | OEaddiw (n: int) (**r add immediate *) - | OEandiw (n: int) (**r and immediate *) - | OEoriw (n: int) (**r or immediate *) - | OExoriw (n: int) (**r xor immediate *) - | OEluiw (n: int) (**r load upper-immediate *) + | OEsltiw (n: int) (**r set-less-than immediate *) + | OEsltiuw (n: int) (**r set-less-than unsigned immediate *) + | OEaddiw (optR: option oreg) (n: int) (**r add immediate *) + | OEandiw (n: int) (**r and immediate *) + | OEoriw (n: int) (**r or immediate *) + | OExoriw (n: int) (**r xor immediate *) + | OEluiw (n: int) (**r load upper-immediate *) | OEseql (optR: option oreg) (**r [rd <- rs1 == rs2] signed *) | OEsnel (optR: option oreg) (**r [rd <- rs1 != rs2] signed *) | OEsequl (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *) | OEsneul (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *) | OEsltl (optR: option oreg) (**r set-less-than *) | OEsltul (optR: option oreg) (**r set-less-than unsigned *) - | OEsltil (n: int64) (**r set-less-than immediate *) - | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) - | OEaddil (n: int64) (**r add immediate *) - | OEandil (n: int64) (**r and immediate *) - | OEoril (n: int64) (**r or immediate *) - | OExoril (n: int64) (**r xor immediate *) - | OEluil (n: int64) (**r load upper-immediate *) - | OEloadli (n: int64) (**r load an immediate int64 *) + | OEsltil (n: int64) (**r set-less-than immediate *) + | OEsltiul (n: int64) (**r set-less-than unsigned immediate *) + | OEaddil (optR: option oreg) (n: int64) (**r add immediate *) + | OEandil (n: int64) (**r and immediate *) + | OEoril (n: int64) (**r or immediate *) + | OExoril (n: int64) (**r xor immediate *) + | OEluil (n: int64) (**r load upper-immediate *) + | OEloadli (n: int64) (**r load an immediate int64 *) | OEmayundef (mu: mayundef) - | OEfeqd (**r compare equal *) - | OEfltd (**r compare less-than *) - | OEfled (**r compare less-than/equal *) - | OEfeqs (**r compare equal *) - | OEflts (**r compare less-than *) - | OEfles (**r compare less-than/equal *) + | OEfeqd (**r compare equal *) + | OEfltd (**r compare less-than *) + | OEfled (**r compare less-than/equal *) + | OEfeqs (**r compare equal *) + | OEflts (**r compare less-than *) + | OEfles (**r compare less-than/equal *) | Obits_of_single | Obits_of_float | Osingle_of_bits @@ -277,47 +275,46 @@ Defined. *) Global Opaque eq_condition eq_addressing eq_operation. + +(** Generic function to evaluate an instruction according to the given specific register *) Definition zero32 := (Vint Int.zero). Definition zero64 := (Vlong Int64.zero). -Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B := +Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz sp: val): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz + | Some SP_S => sem v1 sp end. +(** Mayundef evaluation according to the above defined type *) + Definition eval_may_undef (mu: mayundef) (v1 v2: val): val := match mu with - | MUint => match v1 with - | Vint _ => v2 - | _ => Vundef + | MUint => match v1, v2 with + | Vint _, Vint _ => v2 + | _, _ => Vundef end - | MUlong => match v1 with - | Vlong _ => v2 - | _ => Vundef + | MUlong => match v1, v2 with + | Vlong _, Vint _ => v2 + | _, _ => Vundef end | MUshrx i => - match v1 with - | Vint _ => - if Int.ltu i (Int.repr 31) then v1 else Vundef - | _ => Vundef + match v1, v2 with + | Vint _, Vint _ => + if Int.ltu i (Int.repr 31) then v2 else Vundef + | _, _ => Vundef end | MUshrxl i => - match v1 with - | Vlong _ => - if Int.ltu i (Int.repr 63) then v1 else Vundef - | _ => Vundef + match v1, v2 with + | Vlong _, Vlong _ => + if Int.ltu i (Int.repr 63) then v2 else Vundef + | _, _ => Vundef end end. -Definition eval_opimmR0 (opi: opimm): val := - match opi with - | OPimmADD i => Val.add (Vint i) zero32 - | OPimmADDL i => Val.addl (Vlong i) zero64 - end. - (** * Evaluation functions *) (** Evaluation of conditions, operators and addressing modes applied @@ -340,25 +337,33 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2) (* Expansed branches *) - | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 Vundef + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 Vundef + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 Vundef + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 Vundef + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 Vundef + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 Vundef + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 Vundef + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 Vundef + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 Vundef + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 Vundef | _, _ => None end. +(** Assert sp is a pointer *) + +Definition get_sp sp := + match sp with + | Vptr _ _ => sp + | _ => Vundef + end. + Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val) (m: mem): option val := @@ -461,31 +466,41 @@ Definition eval_operation | Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1) | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) (* Expansed conditions *) - | OEimmR0 opi, nil => Some (eval_opimmR0 opi) - | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32) - | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32) - | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32) - | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32) - | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32) - | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32) + | OEmoveSP, nil => Some (get_sp sp) + | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32 Vundef) + | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32 Vundef) + | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef) + | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef) + | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32 Vundef) + | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef) | OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n)) | OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n)) | OExoriw n, v1::nil => Some (Val.xor v1 (Vint n)) | OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12))) - | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1) + | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32 Vundef) + | OEaddiw ((Some SP_S) as optR) n, v1::nil => + let sp' := Val.add (Vint n) (get_sp sp) in + Some (apply_bin_oreg optR Val.add v1 Vundef Vundef sp') + | OEaddiw optR n, v1::nil => + Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef (get_sp sp)) | OEandiw n, v1::nil => Some (Val.and (Vint n) v1) | OEoriw n, v1::nil => Some (Val.or (Vint n) v1) - | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64)) - | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64)) - | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64)) - | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64)) - | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64)) - | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64)) + | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64 Vundef)) + | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64 Vundef)) + | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef)) + | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef)) + | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64 Vundef)) + | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef)) | OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n))) | OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n))) | OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n)) | OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12)))) - | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1) + | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64 Vundef) + | OEaddil ((Some SP_S) as optR) n, v1::nil => + let sp' := Val.addl (Vlong n) (get_sp sp) in + Some (apply_bin_oreg optR Val.addl v1 Vundef Vundef sp') + | OEaddil optR n, v1::nil => + Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef (get_sp sp)) | OEandil n, v1::nil => Some (Val.andl (Vlong n) v1) | OEoril n, v1::nil => Some (Val.orl (Vlong n) v1) | OEloadli n, nil => Some (Vlong n) @@ -574,12 +589,23 @@ Definition type_of_condition (c: condition) : list typ := | CEbgeul _ => Tlong :: Tlong :: nil end. -Definition type_of_opimmR0 (opi: opimm) : typ := - match opi with - | OPimmADD _ => Tint - | OPimmADDL _ => Tlong +(** The type of mayundef and addsp is dynamic *) + +Definition type_of_mayundef mu := + match mu with + | MUint | MUshrx _ => (Tint :: Tint :: nil, Tint) + | MUlong => (Tlong :: Tint :: nil, Tint) + | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong) end. +Definition type_addsp (is_long: bool): list typ * typ := + if Archi.ptr64 then ( + if is_long then (Tlong :: nil, Tptr) + else (nil, Tint)) + else ( + if is_long then (nil, Tlong) + else (Tint :: nil, Tptr)). + Definition type_of_operation (op: operation) : list typ * typ := match op with | Omove => (nil, Tint) (* treated specially *) @@ -675,7 +701,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoflong => (Tlong :: nil, Tsingle) | Osingleoflongu => (Tlong :: nil, Tsingle) | Ocmp c => (type_of_condition c, Tint) - | OEimmR0 opi => (nil, type_of_opimmR0 opi) + | OEmoveSP => (nil, Tptr) | OEseqw _ => (Tint :: Tint :: nil, Tint) | OEsnew _ => (Tint :: Tint :: nil, Tint) | OEsequw _ => (Tint :: Tint :: nil, Tint) @@ -686,7 +712,9 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEsltiuw _ => (Tint :: nil, Tint) | OExoriw _ => (Tint :: nil, Tint) | OEluiw _ => (nil, Tint) - | OEaddiw _ => (Tint :: nil, Tint) + | OEaddiw None _ => (Tint :: nil, Tint) + | OEaddiw (Some SP_S) _ => type_addsp false + | OEaddiw (Some _) _ => (nil, Tint) | OEandiw _ => (Tint :: nil, Tint) | OEoriw _ => (Tint :: nil, Tint) | OEseql _ => (Tlong :: Tlong :: nil, Tint) @@ -701,9 +729,11 @@ Definition type_of_operation (op: operation) : list typ * typ := | OEoril _ => (Tlong :: nil, Tlong) | OExoril _ => (Tlong :: nil, Tlong) | OEluil _ => (nil, Tlong) - | OEaddil _ => (Tlong :: nil, Tlong) + | OEaddil None _ => (Tlong :: nil, Tlong) + | OEaddil (Some SP_S) _ => type_addsp true + | OEaddil (Some _) _ => (nil, Tlong) | OEloadli _ => (nil, Tlong) - | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64) + | OEmayundef mu => type_of_mayundef mu | OEfeqd => (Tfloat :: Tfloat :: nil, Tint) | OEfltd => (Tfloat :: Tfloat :: nil, Tint) | OEfled => (Tfloat :: Tfloat :: nil, Tint) @@ -746,7 +776,7 @@ Proof. Qed. Remark type_mayundef: - forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64. + forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) (snd (type_of_mayundef mu)). Proof. intros. unfold eval_may_undef. destruct mu eqn:EQMU, v1, v2; simpl; auto. @@ -762,7 +792,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). intros. destruct op; simpl; simpl in H0; FuncInv; subst; simpl. (* move *) - - congruence. + - simpl in H; congruence. (* intconst, longconst, floatconst, singleconst *) - exact I. - exact I. @@ -929,8 +959,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; cbn; trivial. (* cmp *) - destruct (eval_condition cond vl m)... destruct b... - (* OEimmR0 *) - - destruct opi; unfold eval_opimmR0; simpl; auto. + (* OEmoveSP *) + - destruct sp; unfold Tptr; destruct Archi.ptr64 eqn:?; + simpl; trivial. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold Val.cmp; destruct Val.cmp_bool... all: destruct b... @@ -955,7 +986,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiuw *) - unfold Val.cmpu; destruct Val.cmpu_bool... destruct b... (* OEaddiw *) - - fold (Val.add (Vint n) v0); apply type_add. + - destruct optR as [[]|]; simpl in *; trivial; + destruct vl; inv H0; simpl; trivial; + destruct vl; inv H2; simpl; trivial; + destruct v0; simpl; trivial; + destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; + unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. (* OEandiw *) - destruct v0... (* OEoriw *) @@ -988,7 +1024,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). (* OEsltiul *) - unfold Val.cmplu; destruct Val.cmplu_bool... destruct b... (* OEaddil *) - - fold (Val.addl (Vlong n) v0); apply type_addl. + - destruct optR as [[]|]; simpl in *; trivial; + destruct vl; inv H0; simpl; trivial; + destruct vl; inv H2; simpl; trivial; + destruct v0; simpl; trivial; + destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial; + unfold type_addsp, Tptr; try rewrite HA; simpl; trivial. (* OEandil *) - destruct v0... (* OEoril *) @@ -1052,11 +1093,15 @@ Lemma is_trapping_op_sound: eval_operation genv sp op vl m <> None. Proof. unfold args_of_operation. - destruct op; destruct eq_operation; intros; simpl in *; try congruence. + destruct op eqn:E; destruct eq_operation; intros; simpl in *; try congruence. all: try (destruct vl as [ | vh1 vl1]; try discriminate). all: try (destruct vl1 as [ | vh2 vl2]; try discriminate). all: try (destruct vl2 as [ | vh3 vl3]; try discriminate). all: try (destruct vl3 as [ | vh4 vl4]; try discriminate). + all: try destruct optR as [[]|]; simpl in H0; try discriminate. + all: unfold type_addsp in *; simpl in *. + all: try destruct Archi.ptr64; simpl in *; try discriminate. + all: try destruct mu; simpl in *; try discriminate. Qed. End SOUNDNESS. @@ -1181,6 +1226,9 @@ Definition shift_stack_addressing (delta: Z) (addr: addressing) := Definition shift_stack_operation (delta: Z) (op: operation) := match op with | Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta)) + | OEmoveSP => Oaddrstack (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta)) + | OEaddiw (Some SP_S) n => OEaddiw (Some SP_S) (Ptrofs.to_int (Ptrofs.add (Ptrofs.of_int n) (Ptrofs.repr delta))) + | OEaddil (Some SP_S) n => OEaddil (Some SP_S) (Ptrofs.to_int64 (Ptrofs.add (Ptrofs.of_int64 n) (Ptrofs.repr delta))) | _ => op end. @@ -1193,7 +1241,8 @@ Qed. Lemma type_shift_stack_operation: forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op. Proof. - intros. destruct op; auto. + intros. destruct op; auto; + try destruct optR as [[]|]; simpl; auto. Qed. Lemma eval_shift_stack_addressing: @@ -1210,8 +1259,21 @@ Lemma eval_shift_stack_operation: eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. - intros. destruct op; simpl; auto. destruct vl; auto. - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. + intros. destruct op eqn:E; simpl; auto; destruct vl; auto. + - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto. + - rewrite !Ptrofs.add_zero_l; auto. + - destruct optR as [[]|]; simpl; auto. + - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. + destruct v, Archi.ptr64 eqn:EA; simpl; try rewrite EA; simpl; auto. + rewrite Ptrofs.add_zero_l; auto. + rewrite Ptrofs.of_int_to_int; auto. + rewrite (Ptrofs.add_commut (Ptrofs.of_int n) (Ptrofs.repr delta)); reflexivity. + - destruct optR as [[]|]; simpl; auto. + - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto. + destruct Archi.ptr64 eqn:EA; auto. + rewrite Ptrofs.add_zero_l; auto. + rewrite Ptrofs.of_int64_to_int64; auto. + rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n) (Ptrofs.repr delta)); reflexivity. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that @@ -1471,8 +1533,8 @@ Qed. Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32) - (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32). + Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32 Vundef) + (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu; @@ -1482,6 +1544,9 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmpu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef). + eauto. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1512,8 +1577,8 @@ Qed. Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR, Val.inject f v v' -> Val.inject f v0 v'0 -> - Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64)) - (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)). + Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64 Vundef)) + (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)). Proof. intros until optR. intros HV1 HV2. destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu; @@ -1523,6 +1588,9 @@ Proof. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + + exploit eval_cmplu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef). + eauto. eapply Heqo. + intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. + exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo. intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto. Qed. @@ -1789,8 +1857,9 @@ Proof. exploit eval_condition_inj; eauto. intros EQ; rewrite EQ. destruct b; simpl; constructor. simpl; constructor. - (* OEimmR0 *) - - destruct opi; unfold eval_opimmR0; simpl; auto. + (* moveSP *) + - unfold get_sp; inv H; auto. + econstructor; eauto. (* OEseqw *) - destruct optR as [[]|]; simpl; unfold zero32, Val.cmp; inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto; @@ -1814,9 +1883,14 @@ Proof. (* OEsltiuw *) - apply eval_cmpu_bool_inj; auto. (* OEaddiw *) - - fold (Val.add (Vint n) v); - fold (Val.add (Vint n) v'); + - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; + try fold (Val.add (Vint n) (get_sp sp1)); + try fold (Val.add (Vint n) (get_sp sp2)); + (*try destruct (get_sp sp1), (get_sp sp2);*) apply Val.add_inject; auto. + apply Val.add_inject; auto. + destruct sp1, sp2; simpl; auto; + inv H. (* OEandiw *) - inv H4; cbn; auto. (* OEoriw *) @@ -1848,9 +1922,13 @@ Proof. (* OEsltiul *) - apply eval_cmplu_bool_inj; auto. (* OEaddil *) - - fold (Val.addl (Vlong n) v); - fold (Val.addl (Vlong n) v'); + - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists; + try fold (Val.addl (Vlong n) (get_sp sp1)); + try fold (Val.addl (Vlong n) (get_sp sp2)); + apply Val.addl_inject; auto. apply Val.addl_inject; auto. + destruct sp1, sp2; simpl; auto; + inv H. (* OEandil *) - inv H4; cbn; auto. (* OEoril *) diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index e18d31f6..53730a1b 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -36,14 +36,16 @@ let mu_name pp = function | MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i) | MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i) -let get_immR0 pp = function - | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i) - | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i) - let get_optR_s c reg pp r1 r2 = function | None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2 | Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1 | Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c) + | Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)" + +let get_optR_a pp = function + | None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)" + | Some X0_L | Some X0_R -> fprintf pp "X0" + | Some SP_S -> fprintf pp "SP" let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> @@ -203,7 +205,6 @@ let print_operation reg pp = function | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1 | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) - | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi | OEseqw optR, [r1;r2] -> fprintf pp "OEseqw"; (get_optR_s Ceq reg pp r1 r2 optR) | OEsnew optR, [r1;r2] -> fprintf pp "OEsnew"; (get_optR_s Cne reg pp r1 r2 optR) | OEsequw optR, [r1;r2] -> fprintf pp "OEsequw"; (get_optR_s Ceq reg pp r1 r2 optR) @@ -214,7 +215,8 @@ let print_operation reg pp = function | OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n) - | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddiw (optR, n), [] -> fprintf pp "OEaddiw(%a,%ld)" get_optR_a optR (camlint_of_coqint n) + | OEaddiw (optR, n), [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n) | OEseql optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR) @@ -227,7 +229,8 @@ let print_operation reg pp = function | OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n) | OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n) - | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) + | OEaddil (optR, n), [] -> fprintf pp "OEaddil(%a,%ld)" get_optR_a optR (camlint_of_coqint n) + | OEaddil (optR, n), [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n) | OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n) | OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n) diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v index 5b44caba..c453dfb8 100644 --- a/riscV/RTLpathSE_simplify.v +++ b/riscV/RTLpathSE_simplify.v @@ -30,9 +30,9 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval := Definition make_lhsv_single (hvs: hsval) : list_hsval := fScons hvs fSnil. -(** Expansion functions *) +(** * Expansion functions *) -(* Immediate loads *) +(** ** Immediate loads *) Definition load_hilo32 (hi lo: int) := if Int.eq lo Int.zero then @@ -40,7 +40,7 @@ Definition load_hilo32 (hi lo: int) := else let hvs := fSop (OEluiw hi) fSnil in let hl := make_lhsv_single hvs in - fSop (OEaddiw lo) hl. + fSop (OEaddiw None lo) hl. Definition load_hilo64 (hi lo: int64) := if Int64.eq lo Int64.zero then @@ -48,19 +48,19 @@ Definition load_hilo64 (hi lo: int64) := else let hvs := fSop (OEluil hi) fSnil in let hl := make_lhsv_single hvs in - fSop (OEaddil lo) hl. + fSop (OEaddil None lo) hl. Definition loadimm32 (n: int) := match make_immed32 n with | Imm32_single imm => - fSop (OEimmR0 (OPimmADD imm)) fSnil + 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 (OEimmR0 (OPimmADDL imm)) fSnil + fSop (OEaddil (Some X0_R) imm) fSnil | Imm64_pair hi lo => load_hilo64 hi lo | Imm64_large imm => fSop (OEloadli imm) fSnil end. @@ -91,20 +91,20 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper fSop op hl end. -Definition addimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oadd OEaddiw. +Definition addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or). Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw. Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw. Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw. Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw. Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw. -Definition addimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oaddl OEaddil. +Definition addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or). Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil. Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril. Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril. Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil. Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul. -(* Comparisons intructions *) +(** ** Comparisons intructions *) Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) := match cmp with @@ -260,7 +260,7 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) := let hl := make_lhsv_single hvs in if normal' then hvs else fSop (OExoriw Int.one) hl. -(* Branches instructions *) +(** ** Branches instructions *) Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) := match cmp with @@ -309,18 +309,37 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con let hl := make_lhsv_cmp false hvs hvs in if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl). -(** Add pointer expansion *) +(** ** Add pointer expansion *) -(*Definition addptrofs (hv1: hsval) (n: ptrofs) :=*) - (*if Ptrofs.eq_dec n Ptrofs.zero then*) - (*let lhsv := make_lhsv_single hv1 in*) - (*fSop Omove lhsv*) - (*else*) - (*if Archi.ptr64*) - (*then addimm64 hv1 (Ptrofs.to_int64 n)*) - (*else addimm32 hv1 (Ptrofs.to_int n).*) - -(** Target op simplifications using "fake" values *) +Definition addptrofs (n: ptrofs) := + if Ptrofs.eq_dec n Ptrofs.zero then + fSop OEmoveSP fSnil + else + if Archi.ptr64 + then ( + match make_immed64 (Ptrofs.to_int64 n) with + | Imm64_single imm => + fSop (OEaddil (Some SP_S) imm) fSnil + | Imm64_pair hi lo => + let hvs := load_hilo64 hi lo in + let hl := make_lhsv_single hvs in + fSop (OEaddil (Some SP_S) Int64.zero) hl + | Imm64_large imm => + let hvs := fSop (OEloadli imm) fSnil in + let hl := make_lhsv_single hvs in + fSop (OEaddil (Some SP_S) Int64.zero) hl + end) + else ( + match make_immed32 (Ptrofs.to_int n) with + | Imm32_single imm => + fSop (OEaddiw (Some SP_S) imm) fSnil + | Imm32_pair hi lo => + let hvs := load_hilo32 hi lo in + let hl := make_lhsv_single hvs in + fSop (OEaddiw (Some SP_S) Int.zero) hl + end). + +(** * Target simplifications using "fake" values *) Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := match op, lr with @@ -402,10 +421,10 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca Some (loadimm64 n) | Oaddimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in - Some (addimm32 hv1 n) + Some (addimm32 hv1 n None) | Oaddlimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in - Some (addimm64 hv1 n) + Some (addimm64 hv1 n None) | Oandimm n, a1 :: nil => let hv1 := fsi_sreg_get hst a1 in Some (andimm32 hv1 n) @@ -442,9 +461,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then - let move_s := fSop Omove hl in - let move_l := make_lhsv_cmp false move_s move_s in - Some (fSop (OEmayundef (MUshrx n)) move_l) + let lhl := make_lhsv_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)) hl in @@ -468,9 +486,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let hv1 := fsi_sreg_get hst a1 in let hl := make_lhsv_single hv1 in if Int.eq n Int.zero then - let move_s := fSop Omove hl in - let move_l := make_lhsv_cmp false move_s move_s in - Some (fSop (OEmayundef (MUshrxl n)) move_l) + let lhl := make_lhsv_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)) hl in @@ -490,9 +507,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca let srail_s' := fSop (Oshrlimm n) addl_l in let srail_l' := make_lhsv_cmp false srail_s' srail_s' in Some (fSop (OEmayundef (MUshrxl n)) srail_l') - (*| Oaddrstack n, nil =>*) - (*let hv1 := fsi_sreg_get hst a1 in*) - (*OK (addptrofs hv1 n)*) + (* TODO gourdinl | Oaddrstack n, nil =>*) + (*Some (addptrofs n)*) | _, _ => None end. @@ -601,9 +617,9 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args | _, _ => None end. -(** Auxiliary lemmas on comparisons *) +(** * Auxiliary lemmas on comparisons *) -(* Signed ints *) +(** ** Signed ints *) Lemma xor_neg_ltle_cmp: forall v1 v2, Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) = @@ -618,7 +634,7 @@ Proof. auto. Qed. -(* Unsigned ints *) +(** ** 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)) = @@ -652,7 +668,7 @@ Proof. rewrite !Int.unsigned_repr; try cbn; try omega. Qed. -(* Signed longs *) +(** ** Signed longs *) Lemma xor_neg_ltle_cmpl: forall v1 v2, Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) = @@ -748,7 +764,7 @@ Proof. apply Z.le_ge. trivial. Qed. -(* Unsigned longs *) +(** ** 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)) = @@ -794,7 +810,7 @@ Proof. repeat destruct (_ && _); simpl; auto. Qed. -(* Floats *) +(** ** Floats *) Lemma xor_neg_eqne_cmpf: forall v1 v2, Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) = @@ -807,7 +823,7 @@ Proof. destruct (Float.cmp _ _ _); simpl; auto. Qed. -(* Singles *) +(** ** Singles *) Lemma xor_neg_eqne_cmpfs: forall v1 v2, Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) = @@ -820,7 +836,7 @@ Proof. destruct (Float32.cmp _ _ _); simpl; auto. Qed. -(* More useful lemmas *) +(** ** More useful lemmas *) Lemma xor_neg_optb: forall v, Some (Val.xor (Val.of_optbool (option_map negb v)) @@ -863,7 +879,7 @@ Proof. destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto. Qed. -(* Intermediates lemmas on each expansed instruction *) +(** * Intermediates lemmas on each expanded instruction *) Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall (SREG: forall r: positive, @@ -1026,7 +1042,6 @@ Proof. try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl; try rewrite ltu_12_wordsize; trivial; try rewrite Int.add_commut, Int.add_zero_l in *; - try rewrite Int.add_commut; try rewrite Int.add_zero_l; try destruct (Int.ltu _ _) eqn:EQLTU; simpl; try rewrite EQLTU; simpl; try rewrite EQIMM; @@ -1149,25 +1164,21 @@ Proof. 1,2,3,4,5,6,7,8,9,10,11,12: try rewrite <- optbool_mktotal; trivial; try rewrite Int64.add_commut, Int64.add_zero_l in *; - try rewrite Int64.add_commut; - try rewrite Int64.add_zero_l; try fold (Val.cmpl Clt (Vlong i) (Vlong imm)); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))))); try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo))); try rewrite xor_neg_ltge_cmpl; trivial; try rewrite xor_neg_ltle_cmpl; trivial. 6: - try rewrite Int64.add_commut; rewrite <- H; try apply cmpl_ltle_add_one; auto. all: try rewrite <- H; try apply cmpl_ltle_add_one; auto; + try rewrite <- cmpl_ltle_add_one; auto; try rewrite ltu_12_wordsize; try rewrite Int.add_commut, Int.add_zero_l in *; try rewrite Int64.add_commut, Int64.add_zero_l in *; - try rewrite Int.add_commut; - try rewrite Int64.add_commut; try rewrite Int64.add_zero_l; simpl; try rewrite lt_maxsgn_false_long; try (rewrite <- H; trivial; fail); @@ -1216,7 +1227,6 @@ Proof. 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 Int64.add_commut; try rewrite Int64.add_zero_l; try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu; trivial; fail); @@ -1362,8 +1372,7 @@ Proof. - apply Int64.same_if_eq in EQLO; subst. try rewrite Int64.add_commut, Int64.add_zero_l in H. rewrite <- H; try rewrite Float.of_to_bits; trivial. - - try rewrite Int64.add_commut; - rewrite <- H; try rewrite Float.of_to_bits; trivial. + - rewrite <- H; try rewrite Float.of_to_bits; trivial. - rewrite <- H; try rewrite Float.of_to_bits; trivial. Qed. @@ -1392,7 +1401,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l in H; simpl; - try rewrite Int.add_commut in H; rewrite ltu_12_wordsize; simpl; try rewrite <- H; try rewrite Float32.of_to_bits; trivial. Qed. @@ -1403,7 +1411,7 @@ Lemma simplify_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with | nil => None - | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n) + | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), @@ -1423,7 +1431,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1433,7 +1440,7 @@ Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall seval_sval ge sp (si_sreg st r) rs0 m0) (H : match lr with | nil => None - | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n) + | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n None) | a1 :: _ :: _ => None end = Some fsv) (OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args), @@ -1483,7 +1490,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1543,7 +1549,6 @@ Proof. all: try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; trivial. Qed. @@ -1595,7 +1600,6 @@ Proof. try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl; try apply Int.same_if_eq in EQLO; subst; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite ltu_12_wordsize; try rewrite H; trivial. Qed. @@ -1690,9 +1694,8 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall then Some (fSop (OEmayundef (MUshrx n)) - (make_lhsv_cmp false - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) else if Int.eq n Int.one then @@ -1794,9 +1797,8 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall then Some (fSop (OEmayundef (MUshrxl n)) - (make_lhsv_cmp false - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))) - (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1))))) + (make_lhsv_cmp false (fsi_sreg_get hst a1) + (fsi_sreg_get hst a1))) else if Int.eq n Int.one then @@ -1885,7 +1887,7 @@ Proof. destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate. rewrite !EQN2. rewrite EQN0. reflexivity. - Qed. +Qed. Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall (SREG: forall r: positive, @@ -1924,7 +1926,7 @@ Proof. rewrite Int64.shru'_zero. reflexivity. Qed. -(* Main proof of simplification *) +(** * Main proof of simplification *) Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall (H: target_op_simplify op lr hst = Some fsv) @@ -1937,28 +1939,22 @@ Proof. unfold target_op_simplify; simpl. intros H (LREF & SREF & SREG & SMEM) ? ? ?. destruct op; try congruence. - (* int and long constants *) eapply simplify_intconst_correct; eauto. eapply simplify_longconst_correct; eauto. - (* FP const expansions *) eapply simplify_floatconst_correct; eauto. eapply simplify_singleconst_correct; eauto. - (* cast 8/16 operations *) + (* TODO gourdinl*) + (*admit.*) eapply simplify_cast8signed_correct; eauto. eapply simplify_cast16signed_correct; eauto. - (* Immediate int operations *) eapply simplify_addimm_correct; eauto. eapply simplify_andimm_correct; eauto. eapply simplify_orimm_correct; eauto. - (* Shrx imm int operation *) eapply simplify_shrximm_correct; eauto. - (* cast 32u operation *) eapply simplify_cast32unsigned_correct; eauto. - (* Immediate long operations *) eapply simplify_addlimm_correct; eauto. eapply simplify_andlimm_correct; eauto. eapply simplify_orlimm_correct; eauto. - (* Shrx imm long operation *) eapply simplify_shrxlimm_correct; eauto. (* Ocmp expansions *) destruct cond; repeat (destruct lr; simpl; try congruence); @@ -1966,31 +1962,20 @@ Proof. try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); inv H; inv OK1. - (* Ccomp *) - eapply simplify_ccomp_correct; eauto. - (* Ccompu *) - eapply simplify_ccompu_correct; eauto. - (* Ccompimm *) - eapply simplify_ccompimm_correct; eauto. - (* Ccompuimm *) - eapply simplify_ccompuimm_correct; eauto. - (* Ccompl *) - eapply simplify_ccompl_correct; eauto. - (* Ccomplu *) - eapply simplify_ccomplu_correct; eauto. - (* Ccomplimm *) - eapply simplify_ccomplimm_correct; eauto. - (* Ccompluimm *) - eapply simplify_ccompluimm_correct; eauto. - (* Ccompf *) - eapply simplify_ccompf_correct; eauto. - (* Cnotcompf *) - eapply simplify_cnotcompf_correct; eauto. - (* Ccompfs *) - eapply simplify_ccompfs_correct; eauto. - (* Cnotcompfs *) - eapply simplify_cnotcompfs_correct; eauto. Qed. +(*Admitted.*) Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall (TARGET: target_cbranch_expanse hst c l = Some (c', l')) @@ -2042,7 +2027,6 @@ Proof. try destruct v; try rewrite H; try rewrite ltu_12_wordsize; try rewrite EQLO; try rewrite Int.add_commut, Int.add_zero_l; - try rewrite Int.add_commut; try rewrite Int64.add_commut, Int64.add_zero_l; try rewrite Int64.add_commut; try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l; diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index e48c4a5b..3ba2732d 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -19,44 +19,41 @@ Require Import Zbits. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). - -Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + +(** Functions to select a special register (see Op.v) *) + +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz + | Some SP_S => sem v1 sp end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := match mu with - | MUint => match v1 with - | I _ => v2 - | _ => Ifptr Ptop + | MUint => match v1, v2 with + | I _, I _ => v2 + | _, _ => Ifptr Ptop end - | MUlong => match v1 with - | L _ => v2 - | _ => Ifptr Ptop + | MUlong => match v1, v2 with + | L _, I _ => v2 + | _, _ => Ifptr Ptop end | MUshrx i => - match v1 with - | I _ => - if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + match v1, v2 with + | I _, I _ => + if Int.ltu i (Int.repr 31) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop end | MUshrxl i => - match v1 with - | L _ => - if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + match v1, v2 with + | L _, L _ => + if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop end end. -Definition eval_opimmR0 (opi: opimm): aval := - match opi with - | OPimmADD i => add (I i) zero32 - | OPimmADDL i => addl (L i) zero64 - end. - Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -71,22 +68,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 - | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 - | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 - | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 - | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 - | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 - | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 - | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop) + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop) | _, _ => Bnone end. @@ -226,33 +223,35 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | OEimmR0 opi, nil => eval_opimmR0 opi - | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) - | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) - | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) - | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) - | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) - | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) + | OEmoveSP, nil => Ptr Stack + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) | OEluiw n, nil => shl (I n) (I (Int.repr 12)) - | OEaddiw n, v1::nil => add (I n) v1 + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop) + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | OEandiw n, v1::nil => and (I n) v1 | OEoriw n, v1::nil => or (I n) v1 - | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) - | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) - | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) - | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) - | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) - | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) | OEandil n, v1::nil => andl (L n) v1 | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | OEaddil n, v1::nil => addl (L n) v1 + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop) + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | OEloadli n, nil => L (n) | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) @@ -419,8 +418,8 @@ Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) - (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -434,8 +433,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, vmatch bc (Val.maketotal (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 - Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). + Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -445,8 +444,8 @@ Qed. Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) - (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -457,8 +456,8 @@ Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -478,19 +477,23 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64; - destruct opi; eauto with va. 3,4,6: apply eval_cmpu_sound; auto. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - { fold (Val.add (Vint n) a1); eauto with va. } + { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; eauto with va. } { fold (Val.and (Vint n) a1); eauto with va. } { fold (Val.or (Vint n) a1); eauto with va. } { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; try apply vmatch_ifptr_undef. } - 9: { fold (Val.addl (Vlong n) a1); eauto with va. } + 9: { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; eauto with va. } 9: { fold (Val.andl (Vlong n) a1); eauto with va. } 9: { fold (Val.orl (Vlong n) a1); eauto with va. } 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; -- cgit