From 21e8f7a5644c3e61b926d51b458f4b9465eaba22 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 4 May 2019 08:34:40 +0200 Subject: it compiles! --- mppa_k1c/Asmblock.v | 4 ++++ mppa_k1c/PostpassSchedulingOracle.ml | 21 ++++++++++++------ mppa_k1c/PostpassSchedulingproof.v | 42 ++++++++++++++++++++++++++++++++++++ mppa_k1c/TargetPrinter.ml | 27 ++++++++++++++++++++++- 4 files changed, 87 insertions(+), 7 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d9fbbdaa..ddb7ce7d 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -272,10 +272,14 @@ Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: Definition exec_load_q_offset (rs: regset) (m: mem) (d : gpreg_q) (a: ireg) (ofs: offset) := parexec_load_q_offset rs rs m m d a ofs. +Definition exec_load_o_offset (rs: regset) (m: mem) (d : gpreg_o) (a: ireg) (ofs: offset) := parexec_load_o_offset rs rs m m d a ofs. + Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset chunk rs rs m m s a ofs. Definition exec_store_q_offset (rs: regset) (m: mem) (s : gpreg_q) (a: ireg) (ofs: offset) := parexec_store_q_offset rs rs m m s a ofs. +Definition exec_store_o_offset (rs: regset) (m: mem) (s : gpreg_o) (a: ireg) (ofs: offset) := parexec_store_o_offset rs rs m m s a ofs. + Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro. Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_regxs chunk rs rs m m s a ro. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index bdf72ec5..5523752f 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -221,6 +221,9 @@ let load_rec i = match i with | PLoadQRRO(rs, ra, imm) -> let (rs0, rs1) = gpreg_q_expand rs in { inst = "Plq"; write_locs = [Reg (IR rs0); Reg (IR rs1)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false} + | PLoadORRO(rs, ra, imm) -> + let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in + { inst = "Plo"; write_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false} | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} @@ -232,6 +235,10 @@ let store_rec i = match i with let (rs0, rs1) = gpreg_q_expand rs in { inst = "Psq"; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false} + | PStoreORRO (rs, ra, imm) -> + let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in + { inst = "Pso"; write_locs = [Mem]; read_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3); Reg (IR ra)]; imm = (Some (Off imm)) + ; is_control = false} | PStoreRRR (i, rs1, rs2, rs3) | PStoreRRRXS (i, rs1, rs2, rs3) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} @@ -448,8 +455,8 @@ type real_instruction = | Maddw | Maddd | Cmoved | Make | Nop | Extfz | Extfs | Insf (* LSU *) - | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq - | Sb | Sh | Sw | Sd | Sq + | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo + | Sb | Sh | Sw | Sd | Sq | So (* BCU *) | Icall | Call | Cb | Igoto | Goto | Ret | Get | Set (* FPU *) @@ -522,12 +529,14 @@ let ab_inst_to_real = function | "Plw" | "Plw_a" | "Pfls" -> Lws | "Pld" | "Pfld" | "Pld_a" -> Ld | "Plq" -> Lq + | "Plo" -> Lo | "Psb" -> Sb | "Psh" -> Sh | "Psw" | "Psw_a" | "Pfss" -> Sw | "Psd" | "Psd_a" | "Pfsd" -> Sd | "Psq" -> Sq + | "Pso" -> So | "Pcb" | "Pcbu" -> Cb | "Pcall" | "Pdiv" | "Pdivu" -> Call @@ -599,11 +608,11 @@ let rec_to_usage r = | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding) | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau - | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq -> + | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> (match encoding with None | Some U6 | Some S10 -> lsu_data | Some U27L5 | Some U27L10 -> lsu_data_x | Some E27U27L10 -> lsu_data_y) - | Sb | Sh | Sw | Sd | Sq -> + | Sb | Sh | Sw | Sd | Sq | So -> (match encoding with None | Some U6 | Some S10 -> lsu_acc | Some U27L5 | Some U27L10 -> lsu_acc_x | Some E27U27L10 -> lsu_acc_y) @@ -624,8 +633,8 @@ let real_inst_to_latency = function -> 1 | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4 | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *) - | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq -> 3 - | Sb | Sh | Sw | Sd | Sq -> 1 (* See k1c-Optimization.pdf page 19 *) + | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3 + | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See k1c-Optimization.pdf page 19 *) | Get -> 1 | Set -> 4 (* According to the manual should be 3, but I measured 4 *) | Icall | Call | Cb | Igoto | Goto | Ret -> 42 (* Should not matter since it's the final instruction of the basic block *) diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 0ceff6e5..7ade517a 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -146,6 +146,30 @@ Proof. reflexivity. Qed. +Lemma exec_load_offset_o_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_load_o_offset rs m rd ra ofs = Next rs' m' -> + exec_load_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *. + destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]. + destruct (ireg_eq rd0 ra); try discriminate. + destruct (ireg_eq rd1 ra); try discriminate. + destruct (ireg_eq rd2 ra); try discriminate. + rewrite Pregmap.gso; try discriminate. + simpl in *. + destruct (Mem.loadv _ _ _); try discriminate. + destruct (Mem.loadv _ _ _); try discriminate. + destruct (Mem.loadv _ _ _); try discriminate. + destruct (Mem.loadv _ _ _); try discriminate. + rewrite (regset_double_set PC rd0) by discriminate. + rewrite (regset_double_set PC rd1) by discriminate. + rewrite (regset_double_set PC rd2) by discriminate. + rewrite (regset_double_set PC rd3) by discriminate. + inv H. + trivial. +Qed. + Lemma exec_store_offset_pc_var: forall t rs m rd ra ofs rs' m' v, exec_store_offset t rs m rd ra ofs = Next rs' m' -> @@ -171,6 +195,22 @@ Proof. inv H. apply next_eq; auto. Qed. +Lemma exec_store_o_offset_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_store_o_offset rs m rd ra ofs = Next rs' m' -> + exec_store_o_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. + unfold exec_store_o_offset in *. unfold parexec_store_o_offset in *. + destruct (gpreg_o_expand _) as [[[s0 s1] s2] s3]. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + inv H. + trivial. +Qed. + Lemma exec_store_reg_pc_var: forall t rs m rd ra ro rs' m' v, exec_store_reg t rs m rd ra ro = Next rs' m' -> @@ -210,11 +250,13 @@ Proof. + exploreInst; apply exec_load_reg_pc_var; auto. + exploreInst; apply exec_load_regxs_pc_var; auto. + apply exec_load_offset_q_pc_var; auto. + + apply exec_load_offset_o_pc_var; auto. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. + exploreInst; apply exec_store_regxs_pc_var; auto. + apply exec_store_q_offset_pc_var; auto. + + apply exec_store_o_offset_pc_var; auto. - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate). destruct (Mem.storev _ _ _ _); try discriminate. inv H. apply next_eq; auto. apply functional_extensionality. intros. diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 326b802d..a2318469 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -96,8 +96,29 @@ module Target (*: TARGET*) = | R58R59 -> "$r58r59" | R60R61 -> "$r60r61" | R62R63 -> "$r62r63" - + + let int_gpreg_o_name = + let open Asmvliw in + function + | R0R1R2R3 -> "$r0r1r2r3" + | R4R5R6R7 -> "$r4r5r6r7" + | R8R9R10R11 -> "$r8r9r10r11" + | R12R13R14R15 -> "$r12r13r14r15" + | R16R17R18R19 -> "$r16r17r18r19" + | R20R21R22R23 -> "$r20r21r22r23" + | R24R25R26R27 -> "$r24r25r26r27" + | R28R29R30R31 -> "$r28r29r30r31" + | R32R33R34R35 -> "$r32r33r34r35" + | R36R37R38R39 -> "$r36r37r38r39" + | R40R41R42R43 -> "$r40r41r42r43" + | R44R45R46R47 -> "$r44r45r46r47" + | R48R49R50R51 -> "$r48r49r50r51" + | R52R53R54R55 -> "$r52r53r54r55" + | R56R57R58R59 -> "$r56r57r58r59" + | R60R61R62R63 -> "$r60r61r62r63";; + let gpreg_q oc r = output_string oc (int_gpreg_q_name r) + let gpreg_o oc r = output_string oc (int_gpreg_o_name r) let preg oc = let open Asmvliw in function | IR r -> ireg oc r @@ -394,6 +415,8 @@ module Target (*: TARGET*) = fprintf oc " ld%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra | Plq(rd, ra, adr) -> fprintf oc " lq%a %a = %a[%a]\n" xscale adr gpreg_q rd addressing adr ireg ra + | Plo(rd, ra, adr) -> + fprintf oc " lo%a %a = %a[%a]\n" xscale adr gpreg_o rd addressing adr ireg ra | Psb(rd, ra, adr) -> fprintf oc " sb%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd @@ -405,6 +428,8 @@ module Target (*: TARGET*) = fprintf oc " sd%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd | Psq(rd, ra, adr) -> fprintf oc " sq%a %a[%a] = %a\n" xscale adr addressing adr ireg ra gpreg_q rd + | Pso(rd, ra, adr) -> + fprintf oc " so%a %a[%a] = %a\n" xscale adr addressing adr ireg ra gpreg_o rd (* Arith R instructions *) -- cgit