it compiles!

4 files changed, 87 insertions, 7 deletions

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 *)