diff options
| -rw-r--r-- | mppa_k1c/Asmblock.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Peephole.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 7 | ||||
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 14 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 43 |
5 files changed, 65 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 9abc1ca1..f2c4a382 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -272,6 +272,8 @@ Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: 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_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/Peephole.v b/mppa_k1c/Peephole.v index 2c73bb63..91936ac6 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -34,8 +34,8 @@ Fixpoint optimize_body (insns : list basic) : list basic := match t0 with | h1 :: t1 => match h0, h1 with - | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), - (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => + | (PStoreRRO Psd_a rs0 ra0 ofs0), + (PStoreRRO Psd_a rs1 ra1 ofs1) => match gpreg_q_search rs0 rs1 with | Some rs0rs1 => let zofs0 := Ptrofs.signed ofs0 in diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 033cf943..c944774a 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -222,7 +222,12 @@ let load_rec i = match i with { inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false} let store_rec i = match i with - | PStoreRRO (i, rs1, rs2, imm) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) + | PStoreRRO (i, rs1, rs2, imm) -> + { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm)) + ; is_control = false} + | PStoreQRRO (rs, ra, imm) -> + 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} | 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} diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 47248e3e..da64c41d 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -140,6 +140,19 @@ Proof. - discriminate. Qed. +Lemma exec_store_q_offset_pc_var: + forall rs m rd ra ofs rs' m' v, + exec_store_q_offset rs m rd ra ofs = Next rs' m' -> + exec_store_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_q_offset in *. unfold parexec_store_q_offset in *. rewrite Pregmap.gso; try discriminate. + simpl in *. + destruct (gpreg_q_expand _) as [s0 s1]. + destruct (Mem.storev _ _ _); try discriminate. + destruct (Mem.storev _ _ _); try discriminate. + inv H. apply next_eq; auto. +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' -> @@ -182,6 +195,7 @@ Proof. + 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. - 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 156b16d0..7eea7d15 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -41,6 +41,7 @@ module Target (*: TARGET*) = let print_label oc lbl = label oc (transl_label lbl) let int_reg_name = let open Asmvliw in function + | GPR0 -> "$r0" | GPR1 -> "$r1" | GPR2 -> "$r2" | GPR3 -> "$r3" | GPR4 -> "$r4" | GPR5 -> "$r5" | GPR6 -> "$r6" | GPR7 -> "$r7" | GPR8 -> "$r8" | GPR9 -> "$r9" | GPR10 -> "$r10" | GPR11 -> "$r11" @@ -60,7 +61,43 @@ module Target (*: TARGET*) = let ireg oc r = output_string oc (int_reg_name r) - let ireg = ireg + let int_gpreg_q_name = + let open Asmvliw in + function + | R0R1 -> "$r0r1" + | R2R3 -> "$r2r3" + | R4R5 -> "$r4r5" + | R6R7 -> "$r6r7" + | R8R9 -> "$r8r9" + | R10R11 -> "$r10r11" + | R12R13 -> "$r12r13" + | R14R15 -> "$r14r15" + | R16R17 -> "$r16r17" + | R18R19 -> "$r18r19" + | R20R21 -> "$r20r21" + | R22R23 -> "$r22r23" + | R24R25 -> "$r24r25" + | R26R27 -> "$r26r27" + | R28R29 -> "$r28r29" + | R30R31 -> "$r30r31" + | R32R33 -> "$r32r33" + | R34R35 -> "$r34r35" + | R36R37 -> "$r36r37" + | R38R39 -> "$r38r39" + | R40R41 -> "$r40r41" + | R42R43 -> "$r42r43" + | R44R45 -> "$r44r45" + | R46R47 -> "$r46r47" + | R48R49 -> "$r48r49" + | R50R51 -> "$r50r51" + | R52R53 -> "$r52r53" + | R54R55 -> "$r54r55" + | R56R57 -> "$r56r57" + | R58R59 -> "$r58r59" + | R60R61 -> "$r60r61" + | R62R63 -> "$r62r63" + + let gpreg_q oc r = output_string oc (int_gpreg_q_name r) let preg oc = let open Asmvliw in function | IR r -> ireg oc r @@ -364,7 +401,9 @@ module Target (*: TARGET*) = fprintf oc " sw%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd | Psd(rd, ra, adr) | Psd_a(rd, ra, adr) | Pfsd(rd, ra, adr) -> assert Archi.ptr64; 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 + (* Arith R instructions *) (* Arith RR instructions *) |