aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v12
-rw-r--r--mppa_k1c/Asmblock.v2
-rw-r--r--mppa_k1c/Asmblockdeps.v20
-rw-r--r--mppa_k1c/Asmvliw.v23
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml8
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v12
-rw-r--r--mppa_k1c/TargetPrinter.ml18
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v1
8 files changed, 85 insertions, 11 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d1ac8a67..0e217d36 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -42,6 +42,7 @@ Definition preg := preg.
Inductive addressing : Type :=
| AOff (ofs: offset)
| AReg (ro: ireg)
+ | ARegXS (ro: ireg)
.
(** Syntax *)
@@ -444,6 +445,17 @@ Definition basic_to_instruction (b: basic) :=
| PLoadRRR Asmvliw.Pfls rd ra ro => Pfls rd ra (AReg ro)
| PLoadRRR Asmvliw.Pfld rd ra ro => Pfld rd ra (AReg ro)
+ | PLoadRRRXS Asmvliw.Plb rd ra ro => Plb rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plbu rd ra ro => Plbu rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plh rd ra ro => Plh rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plhu rd ra ro => Plhu rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plw rd ra ro => Plw rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Plw_a rd ra ro => Plw_a rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pld rd ra ro => Pld rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pld_a rd ra ro => Pld_a rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pfls rd ra ro => Pfls rd ra (ARegXS ro)
+ | PLoadRRRXS Asmvliw.Pfld rd ra ro => Pfld rd ra (ARegXS ro)
+
(** Store *)
| PStoreRRO Asmvliw.Psb rd ra ofs => Psb rd ra (AOff ofs)
| PStoreRRO Asmvliw.Psh rd ra ofs => Psh rd ra (AOff ofs)
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index ed145f21..3aec4e11 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -268,6 +268,8 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir
Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := parexec_load_reg chunk rs rs m m d a ro.
+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_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := parexec_store_offset ge chunk 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.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 2e83fb44..32a5fa04 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -75,6 +75,7 @@ Coercion OArithRRI64: arith_name_rri64 >-> Funclass.
Inductive load_op :=
| OLoadRRO (n: load_name) (ofs: offset)
| OLoadRRR (n: load_name)
+ | OLoadRRRXS (n: load_name)
.
Coercion OLoadRRO: load_name >-> Funclass.
@@ -146,10 +147,17 @@ Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) :=
| Some vl => Some (Val vl)
end.
+Definition exec_load_deps_regxs (chunk: memory_chunk) (m: mem) (v vo: val) :=
+ match Mem.loadv chunk m (Val.addl v (Val.shll vo (scale_of_chunk chunk))) with
+ | None => None
+ | Some vl => Some (Val vl)
+ end.
+
Definition load_eval (lo: load_op) (l: list value) :=
match lo, l with
| OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps_offset (load_chunk n) m v ofs
| OLoadRRR n, [Val v; Val vo; Memstate m] => exec_load_deps_reg (load_chunk n) m v vo
+ | OLoadRRRXS n, [Val v; Val vo; Memstate m] => exec_load_deps_regxs (load_chunk n) m v vo
| _, _ => None
end.
@@ -355,6 +363,8 @@ Definition load_op_eq (o1 o2: load_op): ?? bool :=
match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end
| OLoadRRR n1 =>
match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end
+ | OLoadRRRXS n1 =>
+ match o2 with OLoadRRRXS n2 => phys_eq n1 n2 | _ => RET false end
end.
Lemma load_op_eq_correct o1 o2:
@@ -363,6 +373,7 @@ Proof.
destruct o1, o2; wlp_simplify; try discriminate.
- congruence.
- congruence.
+ - congruence.
Qed.
Hint Resolve load_op_eq_correct: wlp.
Opaque load_op_eq_correct.
@@ -612,6 +623,7 @@ Definition trans_basic (b: basic) : inst :=
| PArith ai => trans_arith ai
| PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg (#a) @ PReg pmem @ Enil))]
| 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))]
| PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
| Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
@@ -828,6 +840,13 @@ Proof.
eexists; split; try split; Simpl;
intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+ (* Load Reg XS *)
+ + destruct i; simpl load_chunk. all:
+ unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs);
+ destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto;
+ eexists; split; try split; Simpl;
+ intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+
(* Store *)
- destruct i.
(* Store Offset *)
@@ -1408,6 +1427,7 @@ Definition string_of_load (op: load_op): pstring :=
match op with
| OLoadRRO n _ => string_of_load_name n
| OLoadRRR n => string_of_load_name n
+ | OLoadRRRXS n => string_of_load_name n
end.
Definition string_of_store_name (n: store_name) : pstring :=
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index cf827818..d7311272 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -270,6 +270,7 @@ Inductive load_name : Type :=
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)
.
Coercion PLoadRRO: load_name >-> Funclass.
@@ -1123,6 +1124,27 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
| Some v => Next (rsw#d <- v) mw
end.
+Definition scale_of_chunk (chunk: memory_chunk) :=
+ Vint (Int.repr
+ (match chunk with
+ | Mint8signed => 0
+ | Mint8unsigned => 0
+ | Mint16signed => 1
+ | Mint16unsigned => 1
+ | Mint32 => 2
+ | Mint64 => 3
+ | Mfloat32 => 2
+ | Mfloat64 => 3
+ | Many32 => 2
+ | Many64 => 3
+ end)).
+
+Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
+ match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with
+ | None => Stuck
+ | Some v => Next (rsw#d <- v) mw
+ end.
+
Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) :=
match (eval_offset ofs) with
| OK ptr => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
@@ -1172,6 +1194,7 @@ 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
| 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 f931b64b..ef5e325a 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -216,10 +216,10 @@ let arith_rec i =
| PArithR (i, rd) -> arith_r_rec i (IR rd)
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}
- | PLoadRRR (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}
+ | 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}
+ | 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}
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))
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index bc90dd4c..3f3cb19c 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -117,6 +117,17 @@ Proof.
- discriminate.
Qed.
+Lemma exec_load_regxs_pc_var:
+ forall t rs m rd ra ro rs' m' v,
+ exec_load_regxs t rs m rd ra ro = Next rs' m' ->
+ exec_load_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_load_regxs in *. unfold parexec_load_regxs in *. rewrite Pregmap.gso; try discriminate.
+ destruct (Mem.loadv _ _ _).
+ - inv H. apply next_eq; auto. apply functional_extensionality. intros. rewrite regset_double_set; auto. discriminate.
+ - discriminate.
+Qed.
+
Lemma exec_store_offset_pc_var:
forall ge t rs m rd ra ofs rs' m' v,
exec_store_offset ge t rs m rd ra ofs = Next rs' m' ->
@@ -155,6 +166,7 @@ Proof.
- destruct i.
+ exploreInst; apply exec_load_offset_pc_var; auto.
+ exploreInst; apply exec_load_reg_pc_var; auto.
+ + exploreInst; apply exec_load_regxs_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 506faa1c..47927364 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -166,7 +166,11 @@ module Target (*: TARGET*) =
let addressing oc = function
| AOff ofs -> offset oc ofs
- | AReg ro -> ireg oc ro
+ | AReg ro | ARegXS ro -> ireg oc ro
+
+ let xscale oc = function
+ | ARegXS _ -> fprintf oc ".xs"
+ | _ -> ()
let icond_name = let open Asmvliw in function
| ITne | ITneu -> "ne"
@@ -342,17 +346,17 @@ module Target (*: TARGET*) =
(* Load/Store instructions *)
| Plb(rd, ra, adr) ->
- fprintf oc " lbs %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ fprintf oc " lbs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Plbu(rd, ra, adr) ->
- fprintf oc " lbz %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ fprintf oc " lbz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Plh(rd, ra, adr) ->
- fprintf oc " lhs %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ fprintf oc " lhs%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Plhu(rd, ra, adr) ->
- fprintf oc " lhz %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ fprintf oc " lhz%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Plw(rd, ra, adr) | Plw_a(rd, ra, adr) | Pfls(rd, ra, adr) ->
- fprintf oc " lws %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ 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]\n" ireg rd addressing adr ireg ra
+ fprintf oc " ld%a %a = %a[%a]\n" xscale adr ireg rd addressing adr ireg ra
| Psb(rd, ra, adr) ->
fprintf oc " sb %a[%a] = %a\n" addressing adr ireg ra ireg rd
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index eb336edc..ab0d2964 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -946,6 +946,7 @@ Proof.
all: try (inv H; Simpl).
1-10: try (unfold parexec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
1-10: try (unfold parexec_load_reg in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+ 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge 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.
- destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
generated by cgit (git 2.34.1) at 2024-07-04 13:10:47 +0000