aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v5
-rw-r--r--mppa_k1c/Asmblock.v2
-rw-r--r--mppa_k1c/Asmblockdeps.v60
-rw-r--r--mppa_k1c/Asmvliw.v31
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml3
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v19
-rw-r--r--mppa_k1c/TargetPrinter.ml2
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v7
8 files changed, 117 insertions, 12 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 8b1c9a81..70d39168 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -112,7 +112,8 @@ Inductive instruction : Type :=
| Pld (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int64 *)
| Pld_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any64 *)
| Pfls (rd: freg) (ra: ireg) (ofs: addressing) (**r load float *)
- | Pfld (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
+ | Pfld (rd: freg) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
+ | Plq (rs: gpreg_q) (ra: ireg) (ofs: addressing) (**r load 64-bit float *)
(** Stores **)
| Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *)
@@ -436,6 +437,8 @@ Definition basic_to_instruction (b: basic) :=
| PLoadRRO Asmvliw.Pfls rd ra ofs => Pfls rd ra (AOff ofs)
| PLoadRRO Asmvliw.Pfld rd ra ofs => Pfld rd ra (AOff ofs)
+ | PLoadQRRO qrs ra ofs => Plq qrs ra (AOff ofs)
+
| PLoadRRR Asmvliw.Plb rd ra ro => Plb rd ra (AReg ro)
| PLoadRRR Asmvliw.Plbu rd ra ro => Plbu rd ra (AReg ro)
| PLoadRRR Asmvliw.Plh rd ra ro => Plh rd ra (AReg ro)
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index f2c4a382..d9fbbdaa 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -270,6 +270,8 @@ Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ir
Definition exec_load_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_regxs chunk rs rs m m 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_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.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 52af8cdf..ee4a9b51 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -650,6 +650,14 @@ Definition trans_basic (b: basic) : inst :=
| PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
| PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
| PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))]
+ | PLoadQRRO qd a ofs =>
+ let (d0, d1) := gpreg_q_expand qd in
+ if ireg_eq d0 a
+ then [(#d0, Op Fail Enil);
+ (#d1, Op Fail Enil)]
+ else
+ [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil));
+ (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#a) @ PReg pmem @ Enil))]
| PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
| PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
| PStoreQRRO qs a ofs =>
@@ -842,7 +850,7 @@ Proof.
* intros rr; destruct rr; Simpl.
destruct (ireg_eq g rd); subst; Simpl.
Qed.
-
+
Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi:
Ge = Genv ge fn ->
match_states (State rsr mr) sr ->
@@ -877,7 +885,55 @@ Proof.
destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto;
eexists; split; try split; Simpl;
intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
-
+ + unfold parexec_load_q_offset.
+ destruct (gpreg_q_expand rd) as [rd0 rd1].
+ destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ].
+ simpl. trivial.
+ unfold exec_load_deps_offset.
+ destruct Ge.
+ unfold eval_offset.
+ repeat rewrite H0.
+ destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ] eqn:MEML0; simpl.
+ ++ destruct (Mem.loadv Many64 mr
+ (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ] eqn:MEML1.
+ +++ rewrite H0.
+ rewrite H.
+ rewrite MEML0.
+ rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+ rewrite H0.
+ rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+ rewrite H.
+ rewrite MEML1.
+ eexists; split.
+ * f_equal.
+ * constructor.
+ ** repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+ assumption.
+ ** intro.
+ destruct (preg_eq r rd1).
+ *** subst r.
+ rewrite (assign_eq _ (# rd1)).
+ rewrite Pregmap.gss.
+ reflexivity.
+ *** rewrite (assign_diff _ (#rd1) (#r) _) by (apply ppos_discr; apply not_eq_sym; assumption).
+ rewrite Pregmap.gso by assumption.
+ destruct (preg_eq r rd0).
+ **** subst r.
+ rewrite (assign_eq _ (# rd0)).
+ rewrite Pregmap.gss.
+ reflexivity.
+ **** rewrite (assign_diff _ (#rd0) (#r) _) by (apply ppos_discr; apply not_eq_sym; assumption).
+ rewrite Pregmap.gso by assumption.
+ trivial.
+ +++ rewrite H0. rewrite H. rewrite MEML0.
+ rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+ rewrite H0.
+ rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+ rewrite H.
+ rewrite MEML1.
+ constructor.
+ ++ rewrite H0. rewrite H. rewrite MEML0. trivial.
+
(* Store *)
- destruct i.
(* Store Offset *)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 6ebc8340..30263b4d 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -318,6 +318,7 @@ Inductive ld_instruction : Type :=
| PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
| PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
| PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
+ | PLoadQRRO (rd: gpreg_q) (ra: ireg) (ofs: offset)
.
(** Stores **)
@@ -1152,6 +1153,20 @@ Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m
| _ => Stuck
end.
+Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a: ireg) (ofs: offset) :=
+ let (rd0, rd1) := gpreg_q_expand d in
+ if ireg_eq rd0 a
+ then Stuck
+ else
+ match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with
+ | None => Stuck
+ | Some v0 =>
+ match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with
+ | None => Stuck
+ | Some v1 => Next (rsw#rd0 <- v0 #rd1 <- v1) mw
+ end
+ end.
+
Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with
| None => Stuck
@@ -1187,17 +1202,13 @@ Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m
Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (a: ireg) (ofs: offset) :=
let (s0, s1) := gpreg_q_expand s in
- match eval_offset ofs with
- | OK eofs =>
- match Mem.storev Many64 mr (Val.offset_ptr (rsr a) eofs) (rsr s0) with
+ match Mem.storev Many64 mr (Val.offset_ptr (rsr a) ofs) (rsr s0) with
+ | None => Stuck
+ | Some m1 =>
+ match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) (rsr s1) with
| None => Stuck
- | Some m1 =>
- match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add eofs (Ptrofs.repr 8))) (rsr s1) with
- | None => Stuck
- | Some m2 => Next rsw m2
- end
+ | Some m2 => Next rsw m2
end
- | _ => Stuck
end.
@@ -1236,6 +1247,8 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
| PLoadRRO n d a ofs => parexec_load_offset (load_chunk n) rsr rsw mr mw d a ofs
| PLoadRRR n d a ro => parexec_load_reg (load_chunk n) rsr rsw mr mw d a ro
| PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro
+ | PLoadQRRO d a ofs =>
+ parexec_load_q_offset rsr rsw mr mw d a ofs
| PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs
| PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index a4dc3614..e3d43237 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -218,6 +218,9 @@ let arith_rec i =
let load_rec i = match i with
| PLoadRRO (i, rs1, rs2, imm) ->
{ inst = load_str i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false}
+ | 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}
| 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}
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index da64c41d..0ceff6e5 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -128,6 +128,24 @@ Proof.
- discriminate.
Qed.
+Lemma exec_load_offset_q_pc_var:
+ forall rs m rd ra ofs rs' m' v,
+ exec_load_q_offset rs m rd ra ofs = Next rs' m' ->
+ exec_load_q_offset rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *.
+ destruct (gpreg_q_expand rd) as [rd0 rd1].
+ destruct (ireg_eq rd0 ra); try discriminate.
+ rewrite Pregmap.gso; try discriminate.
+ destruct (Mem.loadv _ _ _); try discriminate.
+ inv H.
+ destruct (Mem.loadv _ _ _); try discriminate.
+ inv H1. f_equal.
+ rewrite (regset_double_set PC rd0) by discriminate.
+ rewrite (regset_double_set PC rd1) by discriminate.
+ reflexivity.
+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' ->
@@ -191,6 +209,7 @@ Proof.
+ exploreInst; apply exec_load_offset_pc_var; auto.
+ exploreInst; apply exec_load_reg_pc_var; auto.
+ exploreInst; apply exec_load_regxs_pc_var; auto.
+ + apply exec_load_offset_q_pc_var; auto.
- destruct i.
+ exploreInst; apply exec_store_offset_pc_var; auto.
+ exploreInst; apply exec_store_reg_pc_var; auto.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 9d42169a..326b802d 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -392,6 +392,8 @@ module Target (*: TARGET*) =
fprintf oc " lws%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Pld(rd, ra, adr) | Pfld(rd, ra, adr) | Pld_a(rd, ra, adr) -> assert Archi.ptr64;
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
| Psb(rd, ra, adr) ->
fprintf oc " sb%a %a[%a] = %a\n" xscale adr addressing adr ireg ra ireg rd
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 3bca6629..9303b780 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -950,6 +950,13 @@ Proof.
1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+ - (* PLoadQRRO *)
+ unfold parexec_load_q_offset in H1.
+ destruct (gpreg_q_expand _) as [r0 r1] in H1.
+ destruct (ireg_eq _ _) in H1; try discriminate.
+ destruct (Mem.loadv _ _ _) in H1; try discriminate.
+ destruct (Mem.loadv _ _ _) in H1; try discriminate.
+ inv H1. Simpl.
- (* PStoreQRRO *)
unfold parexec_store_q_offset in H1.
destruct (gpreg_q_expand _) as [r0 r1] in H1.
generated by cgit (git 2.34.1) at 2024-07-02 11:12:48 +0000