aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c')
-rw-r--r--mppa_k1c/Asm.v97
-rw-r--r--mppa_k1c/Asmblock.v52
-rw-r--r--mppa_k1c/Asmblockdeps.v226
-rw-r--r--mppa_k1c/Asmblockgenproof1.v25
-rw-r--r--mppa_k1c/Asmexpand.ml44
-rw-r--r--mppa_k1c/Asmvliw.v48
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml4
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v64
-rw-r--r--mppa_k1c/TargetPrinter.ml44
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v18
10 files changed, 417 insertions, 205 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 2d708b79..115c8d6d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -38,6 +38,11 @@ Require Import Errors.
Definition label := positive.
Definition preg := preg.
+Inductive addressing : Type :=
+ | AOff (ofs: offset)
+ | AReg (ro: ireg)
+.
+
(** Syntax *)
Inductive instruction : Type :=
(** pseudo instructions *)
@@ -70,26 +75,26 @@ Inductive instruction : Type :=
| Ploopdo (count: ireg) (loopend: label)
(** Loads **)
- | Plb (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte *)
- | Plbu (rd: ireg) (ra: ireg) (ofs: offset) (**r load byte unsigned *)
- | Plh (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word *)
- | Plhu (rd: ireg) (ra: ireg) (ofs: offset) (**r load half word unsigned *)
- | Plw (rd: ireg) (ra: ireg) (ofs: offset) (**r load int32 *)
- | Plw_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any32 *)
- | Pld (rd: ireg) (ra: ireg) (ofs: offset) (**r load int64 *)
- | Pld_a (rd: ireg) (ra: ireg) (ofs: offset) (**r load any64 *)
- | Pfls (rd: freg) (ra: ireg) (ofs: offset) (**r load float *)
- | Pfld (rd: freg) (ra: ireg) (ofs: offset) (**r load 64-bit float *)
+ | Plb (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte *)
+ | Plbu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load byte unsigned *)
+ | Plh (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word *)
+ | Plhu (rd: ireg) (ra: ireg) (ofs: addressing) (**r load half word unsigned *)
+ | Plw (rd: ireg) (ra: ireg) (ofs: addressing) (**r load int32 *)
+ | Plw_a (rd: ireg) (ra: ireg) (ofs: addressing) (**r load any32 *)
+ | 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 *)
(** Stores **)
- | Psb (rs: ireg) (ra: ireg) (ofs: offset) (**r store byte *)
- | Psh (rs: ireg) (ra: ireg) (ofs: offset) (**r store half byte *)
- | Psw (rs: ireg) (ra: ireg) (ofs: offset) (**r store int32 *)
- | Psw_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any32 *)
- | Psd (rs: ireg) (ra: ireg) (ofs: offset) (**r store int64 *)
- | Psd_a (rs: ireg) (ra: ireg) (ofs: offset) (**r store any64 *)
- | Pfss (rs: freg) (ra: ireg) (ofs: offset) (**r store float *)
- | Pfsd (rd: freg) (ra: ireg) (ofs: offset) (**r store 64-bit float *)
+ | Psb (rs: ireg) (ra: ireg) (ofs: addressing) (**r store byte *)
+ | Psh (rs: ireg) (ra: ireg) (ofs: addressing) (**r store half byte *)
+ | Psw (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int32 *)
+ | Psw_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any32 *)
+ | Psd (rs: ireg) (ra: ireg) (ofs: addressing) (**r store int64 *)
+ | Psd_a (rs: ireg) (ra: ireg) (ofs: addressing) (**r store any64 *)
+ | Pfss (rs: freg) (ra: ireg) (ofs: addressing) (**r store float *)
+ | Pfsd (rd: freg) (ra: ireg) (ofs: addressing) (**r store 64-bit float *)
(** Arith RR *)
| Pmv (rd rs: ireg) (**r register move *)
@@ -364,26 +369,46 @@ Definition basic_to_instruction (b: basic) :=
| PArithARRI64 Asmblock.Pmaddil rd rs1 imm => Pmaddil rd rs1 imm
(** Load *)
- | PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs
- | PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra ofs
- | PLoadRRO Asmblock.Plh rd ra ofs => Plh rd ra ofs
- | PLoadRRO Asmblock.Plhu rd ra ofs => Plhu rd ra ofs
- | PLoadRRO Asmblock.Plw rd ra ofs => Plw rd ra ofs
- | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra ofs
- | PLoadRRO Asmblock.Pld rd ra ofs => Pld rd ra ofs
- | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra ofs
- | PLoadRRO Asmblock.Pfls rd ra ofs => Pfls rd ra ofs
- | PLoadRRO Asmblock.Pfld rd ra ofs => Pfld rd ra ofs
+ | PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Plbu rd ra ofs => Plbu rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Plh rd ra ofs => Plh rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Plhu rd ra ofs => Plhu rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Plw rd ra ofs => Plw rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Plw_a rd ra ofs => Plw_a rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Pld rd ra ofs => Pld rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Pld_a rd ra ofs => Pld_a rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Pfls rd ra ofs => Pfls rd ra (AOff ofs)
+ | PLoadRRO Asmblock.Pfld rd ra ofs => Pfld rd ra (AOff ofs)
+
+ | PLoadRRR Asmblock.Plb rd ra ro => Plb rd ra (AReg ro)
+ | PLoadRRR Asmblock.Plbu rd ra ro => Plbu rd ra (AReg ro)
+ | PLoadRRR Asmblock.Plh rd ra ro => Plh rd ra (AReg ro)
+ | PLoadRRR Asmblock.Plhu rd ra ro => Plhu rd ra (AReg ro)
+ | PLoadRRR Asmblock.Plw rd ra ro => Plw rd ra (AReg ro)
+ | PLoadRRR Asmblock.Plw_a rd ra ro => Plw_a rd ra (AReg ro)
+ | PLoadRRR Asmblock.Pld rd ra ro => Pld rd ra (AReg ro)
+ | PLoadRRR Asmblock.Pld_a rd ra ro => Pld_a rd ra (AReg ro)
+ | PLoadRRR Asmblock.Pfls rd ra ro => Pfls rd ra (AReg ro)
+ | PLoadRRR Asmblock.Pfld rd ra ro => Pfld rd ra (AReg ro)
(** Store *)
- | PStoreRRO Asmblock.Psb rd ra ofs => Psb rd ra ofs
- | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra ofs
- | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra ofs
- | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra ofs
- | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra ofs
- | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra ofs
- | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra ofs
- | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfsd rd ra ofs
+ | PStoreRRO Asmblock.Psb rd ra ofs => Psb rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Psh rd ra ofs => Psh rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Psw rd ra ofs => Psw rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Psw_a rd ra ofs => Psw_a rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Psd rd ra ofs => Psd rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Psd_a rd ra ofs => Psd_a rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Pfss rd ra ofs => Pfss rd ra (AOff ofs)
+ | PStoreRRO Asmblock.Pfsd rd ra ofs => Pfsd rd ra (AOff ofs)
+
+ | PStoreRRR Asmblock.Psb rd ra ro => Psb rd ra (AReg ro)
+ | PStoreRRR Asmblock.Psh rd ra ro => Psh rd ra (AReg ro)
+ | PStoreRRR Asmblock.Psw rd ra ro => Psw rd ra (AReg ro)
+ | PStoreRRR Asmblock.Psw_a rd ra ro => Psw_a rd ra (AReg ro)
+ | PStoreRRR Asmblock.Psd rd ra ro => Psd rd ra (AReg ro)
+ | PStoreRRR Asmblock.Psd_a rd ra ro => Psd_a rd ra (AReg ro)
+ | PStoreRRR Asmblock.Pfss rd ra ro => Pfss rd ra (AReg ro)
+ | PStoreRRR Asmblock.Pfsd rd ra ro => Pfsd rd ra (AReg ro)
end.
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index b4cf57ae..3656b91f 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -259,9 +259,11 @@ Inductive load_name_rro : Type :=
Inductive ld_instruction : Type :=
| PLoadRRO (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset)
+ | PLoadRRR (i: load_name_rro) (rd: ireg) (ra: ireg) (rofs: ireg)
.
Coercion PLoadRRO: load_name_rro >-> Funclass.
+Coercion PLoadRRR: load_name_rro >-> Funclass.
(** Stores **)
Inductive store_name_rro : Type :=
@@ -277,9 +279,11 @@ Inductive store_name_rro : Type :=
Inductive st_instruction : Type :=
| PStoreRRO (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset)
+ | PStoreRRR (i: store_name_rro) (rs: ireg) (ra: ireg) (rofs: ireg)
.
Coercion PStoreRRO: store_name_rro >-> Funclass.
+Coercion PStoreRRR: store_name_rro >-> Funclass.
(** Arithmetic instructions **)
Inductive arith_name_r : Type :=
@@ -1259,24 +1263,42 @@ Definition eval_offset (ofs: offset) : res ptrofs :=
end.
Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
- (d: ireg) (a: ireg) (ofs: offset) :=
+ (d: ireg) (a: ireg) (ptr: ptrofs) :=
+ match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
+ | None => Stuck
+ | Some v => Next (rs#d <- v) m
+ end
+.
+
+Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) :=
match (eval_offset ofs) with
- | OK ptr =>
- match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
- | None => Stuck
- | Some v => Next (rs#d <- v) m
- end
+ | OK ptr => exec_load chunk rs m d a ptr
+ | _ => Stuck
+ end.
+
+Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
+ match (rs ro) with
+ | Vptr _ ofs => exec_load chunk rs m d a ofs
| _ => Stuck
end.
Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
- (s: ireg) (a: ireg) (ofs: offset) :=
+ (s: ireg) (a: ireg) (ptr: ptrofs) :=
+ match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
+ | None => Stuck
+ | Some m' => Next rs m'
+ end
+.
+
+Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) :=
match (eval_offset ofs) with
- | OK ptr =>
- match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
- | None => Stuck
- | Some m' => Next rs m'
- end
+ | OK ptr => exec_store chunk rs m s a ptr
+ | _ => Stuck
+ end.
+
+Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
+ match (rs ro) with
+ | Vptr _ ofs => exec_store chunk rs m s a ofs
| _ => Stuck
end.
@@ -1312,9 +1334,11 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome :=
match bi with
| PArith ai => Next (exec_arith_instr ai rs) m
- | PLoadRRO n d a ofs => exec_load (load_chunk n) rs m d a ofs
+ | PLoadRRO n d a ofs => exec_load_offset (load_chunk n) rs m d a ofs
+ | PLoadRRR n d a ro => exec_load_reg (load_chunk n) rs m d a ro
- | PStoreRRO n s a ofs => exec_store (store_chunk n) rs m s a ofs
+ | PStoreRRO n s a ofs => exec_store_offset (store_chunk n) rs m s a ofs
+ | PStoreRRR n s a ro => exec_store_reg (store_chunk n) rs m s a ro
| Pallocframe sz pos =>
let (m1, stk) := Mem.alloc m 0 sz in
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index dd876485..7e332895 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -72,12 +72,14 @@ Coercion OArithRRI64: arith_name_rri64 >-> Funclass.
Inductive load_op :=
| OLoadRRO (n: load_name_rro) (ofs: offset)
+ | OLoadRRR (n: load_name_rro)
.
Coercion OLoadRRO: load_name_rro >-> Funclass.
Inductive store_op :=
| OStoreRRO (n: store_name_rro) (ofs: offset)
+ | OStoreRRR (n: store_name_rro)
.
Coercion OStoreRRO: store_name_rro >-> Funclass.
@@ -126,38 +128,58 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
end.
Definition exec_load_deps (chunk: memory_chunk) (m: mem)
- (v: val) (ofs: offset) :=
+ (v: val) (ptr: ptrofs) :=
+ match Mem.loadv chunk m (Val.offset_ptr v ptr) with
+ | None => None
+ | Some vl => Some (Val vl)
+ end
+.
+
+Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) :=
let (ge, fn) := Ge in
match (eval_offset ge ofs) with
- | OK ptr =>
- match Mem.loadv chunk m (Val.offset_ptr v ptr) with
- | None => None
- | Some vl => Some (Val vl)
- end
+ | OK ptr => exec_load_deps chunk m v ptr
+ | _ => None
+ end.
+
+Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) :=
+ match vo with
+ | Vptr _ ofs => exec_load_deps chunk m v ofs
| _ => None
end.
Definition load_eval (lo: load_op) (l: list value) :=
match lo, l with
- | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps (load_chunk n) m v ofs
+ | 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
| _, _ => None
end.
Definition exec_store_deps (chunk: memory_chunk) (m: mem)
- (vs va: val) (ofs: offset) :=
+ (vs va: val) (ptr: ptrofs) :=
+ match Mem.storev chunk m (Val.offset_ptr va ptr) vs with
+ | None => None
+ | Some m' => Some (Memstate m')
+ end
+.
+
+Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) :=
let (ge, fn) := Ge in
match (eval_offset ge ofs) with
- | OK ptr =>
- match Mem.storev chunk m (Val.offset_ptr va ptr) vs with
- | None => None
- | Some m' => Some (Memstate m')
- end
+ | OK ptr => exec_store_deps chunk m vs va ptr
+ | _ => None
+ end.
+
+Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
+ match vo with
+ | Vptr _ ofs => exec_store_deps chunk m vs va ofs
| _ => None
end.
Definition store_eval (so: store_op) (l: list value) :=
match so, l with
- | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps (store_chunk n) m vs va ofs
+ | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps_offset (store_chunk n) m vs va ofs
+ | OStoreRRR n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_reg (store_chunk n) m vs va vo
| _, _ => None
end.
@@ -337,26 +359,32 @@ Qed.
Definition load_op_eq (o1 o2: load_op): ?? bool :=
match o1, o2 with
| OLoadRRO n1 ofs1, OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2)
+ | OLoadRRR n1, OLoadRRR n2 => phys_eq n1 n2
+ | _, _ => RET false
end.
Lemma load_op_eq_correct o1 o2:
WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
Proof.
- destruct o1, o2; wlp_simplify.
- apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
+ destruct o1, o2; wlp_simplify; try discriminate.
+ - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
+ - congruence.
Qed.
Definition store_op_eq (o1 o2: store_op): ?? bool :=
match o1, o2 with
| OStoreRRO n1 ofs1, OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2)
+ | OStoreRRR n1, OStoreRRR n2 => phys_eq n1 n2
+ | _, _ => RET false
end.
Lemma store_op_eq_correct o1 o2:
WHEN store_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
Proof.
- destruct o1, o2; wlp_simplify.
- apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
+ destruct o1, o2; wlp_simplify; try discriminate.
+ - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence.
+ - congruence.
Qed.
(* TODO: rewrite control_op_eq in a robust style against the miss of a case
@@ -586,7 +614,9 @@ Definition trans_basic (b: basic) : macro :=
match b with
| PArith ai => trans_arith ai
| PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (Name (#a) @ Name pmem @ Enil))]
+ | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (Name (#a) @ Name (#ro) @ Name pmem @ Enil))]
| PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (Name (#s) @ Name (#a) @ Name pmem @ Enil))]
+ | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (Name (#s) @ Name (#a) @ Name (#ro) @ Name pmem @ Enil))]
| Pallocframe sz pos => [(#FP, Name (#SP)); (#SP, Op (Allocframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
(pmem, Op (Allocframe sz pos) (Old (Name (#SP)) @ Name pmem @ Enil))]
| Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (Name (#SP) @ Name pmem @ Enil));
@@ -799,25 +829,47 @@ Proof.
intros. destruct b.
(* Arith *)
- simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto.
+
(* Load *)
- simpl in H. destruct i.
- unfold exec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
- destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
- eexists; split; try split;
- [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; rewrite MEML; reflexivity|
- Simpl|
- intros rr; destruct rr; Simpl;
- destruct (ireg_eq g rd); [
- subst; Simpl|
- Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]].
+ (* Load Offset *)
+ + destruct i. all:
+ unfold exec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_load in H;
+ destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+ eexists; split; try split; [
+ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+ (* Load Reg *)
+ + destruct i. all:
+ unfold exec_load_reg in H; destruct (rs rofs) eqn:ROFS; try discriminate; unfold exec_load in H;
+ destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+ eexists; split; try split; [
+ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; rewrite ROFS;
+ unfold exec_load_deps; simpl in MEML; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+
(* Store *)
- simpl in H. destruct i.
- all: unfold exec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
- destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
- eexists; split; try split;
- [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; pose (H1 rs0); simpl in e0; rewrite e0; rewrite MEML; reflexivity
- | Simpl
- | intros rr; destruct rr; Simpl].
+ (* Store Offset *)
+ + destruct i. all:
+ unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; unfold exec_store in H;
+ destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+ eexists; split; try split;
+ [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl ].
+ (* Store Reg *)
+ + destruct i. all:
+ unfold exec_store_reg in H; destruct (rs rofs) eqn:ROFS; try discriminate; unfold exec_store in H;
+ destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+ eexists; split; try split;
+ [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg; rewrite ROFS;
+ unfold exec_store_deps; simpl in MEML; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl ].
+
(* Allocframe *)
- simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate.
inv H. inv H0. eexists. split; try split.
@@ -1155,13 +1207,28 @@ Lemma forward_simu_basic_instr_stuck:
Proof.
intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate.
(* PLoad *)
- - destruct i; destruct i.
- all: simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e;
- unfold exec_load in H0; destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate.
+ - destruct i.
+ (* Load Offset *)
+ + destruct i. all:
+ simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto;
+ unfold exec_load in H0; unfold exec_load_deps; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate.
+ (* Load Reg *)
+ + destruct i. all:
+ simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg;
+ destruct (rs rofs); auto; unfold exec_load in H0; simpl in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate.
+
(* PStore *)
- - destruct i; destruct i;
- simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; pose (H3 rs0); simpl in e; rewrite e; clear e;
- unfold exec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate.
+ - destruct i.
+ (* Store Offset *)
+ + destruct i. all:
+ simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto;
+ unfold exec_store in H0; simpl in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _); auto; discriminate.
+ (* Store Reg *)
+ + destruct i. all:
+ simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0;
+ unfold exec_store_deps_reg; destruct (rs rofs); auto; unfold exec_store in H0; unfold exec_store_deps;
+ destruct (Mem.storev _ _ _ _); auto; discriminate.
+
(* Pallocframe *)
- simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0.
destruct (Mem.store _ _ _ _); try discriminate. reflexivity.
@@ -1521,6 +1588,7 @@ Definition string_of_name_lrro (n: load_name_rro) : pstring :=
Definition string_of_load (op: load_op): pstring :=
match op with
| OLoadRRO n _ => string_of_name_lrro n
+ | OLoadRRR n => string_of_name_lrro n
end.
Definition string_of_name_srro (n: store_name_rro) : pstring :=
@@ -1538,6 +1606,7 @@ Definition string_of_name_srro (n: store_name_rro) : pstring :=
Definition string_of_store (op: store_op) : pstring :=
match op with
| OStoreRRO n _ => string_of_name_srro n
+ | OStoreRRR n => string_of_name_srro n
end.
Definition string_of_control (op: control_op) : pstring :=
@@ -1731,23 +1800,46 @@ Proof.
- simpl in H. inversion H. subst rsw' mw'. simpl macro_prun. eapply trans_arith_par_correct; eauto.
(* Load *)
- simpl in H. destruct i.
- unfold parexec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
- destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H. inv MSR; inv MSW;
- eexists; split; try split;
- [ simpl; rewrite EVALOFF; rewrite H; pose (H0 ra); simpl in e; rewrite e; rewrite MEML; reflexivity|
- Simpl|
- intros rr; destruct rr; Simpl;
- destruct (ireg_eq g rd); [
- subst; Simpl|
- Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]].
+ (* Load Offset *)
+ + destruct i; simpl load_chunk in H. all:
+ unfold parexec_load_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
+ unfold parexec_load in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW;
+ eexists; split; try split;
+ [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); unfold exec_load_deps; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+
+ (* Load Reg *)
+ + destruct i; simpl load_chunk in H. all:
+ unfold parexec_load_reg in H; destruct (rsr rofs) eqn:ROFS; try discriminate;
+ unfold parexec_load in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW;
+ eexists; split; try split;
+ [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); unfold exec_load_deps_reg; rewrite ROFS;
+ unfold exec_load_deps; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ].
+
(* Store *)
- simpl in H. destruct i.
- unfold parexec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate.
- destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate. inv H; inv MSR; inv MSW.
- eexists; split; try split.
- * simpl. rewrite EVALOFF. rewrite H. rewrite (H0 ra). rewrite (H0 rs). rewrite MEML. reflexivity.
- * Simpl.
- * intros rr; destruct rr; Simpl.
+ (* Store Offset *)
+ + destruct i; simpl store_chunk in H. all:
+ unfold parexec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate;
+ unfold parexec_store in H; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW;
+ eexists; split; try split;
+ [ simpl; rewrite EVALOFF; rewrite H; rewrite (H0 ra); rewrite (H0 rs); unfold exec_store_deps; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl ].
+
+ (* Store Reg *)
+ + destruct i; simpl store_chunk in H. all:
+ unfold parexec_store_reg in H; destruct (rsr rofs) eqn:ROFS; try discriminate;
+ unfold parexec_store in H; destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv MSR; inv MSW;
+ eexists; split; try split;
+ [ simpl; rewrite H; rewrite (H0 rofs); rewrite (H0 ra); rewrite (H0 rs); unfold exec_store_deps_reg; rewrite ROFS;
+ unfold exec_store_deps; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl ].
+
(* Allocframe *)
- simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate.
inv H. inv MSR. inv MSW. eexists. split; try split.
@@ -1785,13 +1877,27 @@ Proof.
intros GENV MSR MSW H0. inv MSR; inv MSW.
unfold parexec_basic_instr in H0. destruct bi; try discriminate.
(* PLoad *)
- - destruct i; destruct i.
- all: simpl; rewrite H; rewrite (H1 ra); unfold parexec_load in H0;
- destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate.
+ - destruct i.
+ (* Load Offset *)
+ + destruct i; simpl in H0. all:
+ simpl; rewrite H; rewrite (H1 ra); unfold parexec_load_offset in H0; destruct (eval_offset _ _); auto;
+ unfold parexec_load in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate.
+ (* Load Reg *)
+ + destruct i; simpl in H0. all:
+ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold parexec_load_reg in H0; unfold exec_load_deps_reg;
+ destruct (rsr rofs); auto; unfold parexec_load in H0; unfold exec_load_deps; destruct (Mem.loadv _ _ _); auto; discriminate.
+
(* PStore *)
- - destruct i; destruct i;
- simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs);
- unfold parexec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate.
+ - destruct i.
+ (* Store Offset *)
+ + destruct i; simpl in H0. all:
+ simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); unfold parexec_store_offset in H0; destruct (eval_offset _ _); auto;
+ unfold parexec_store in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _ _); auto; discriminate.
+
+ (* Store Reg *)
+ + destruct i; simpl in H0. all:
+ simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); rewrite (H1 rofs); unfold parexec_store_reg in H0; unfold exec_store_deps_reg;
+ destruct (rsr rofs); auto; unfold parexec_store in H0; unfold exec_store_deps; destruct (Mem.storev _ _ _ _); auto; discriminate.
(* Pallocframe *)
- simpl. Simpl. rewrite (H1 SP). rewrite H. destruct (Mem.alloc _ _ _). simpl in H0.
destruct (Mem.store _ _ _ _); try discriminate. reflexivity.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 5486a497..f8bbf7f4 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1763,7 +1763,7 @@ Qed.
Lemma indexed_load_access_correct:
forall chunk (mk_instr: ireg -> offset -> basic) rd m,
(forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
forall (base: ireg) ofs k (rs: regset) v,
Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v ->
base <> RTMP ->
@@ -1777,14 +1777,14 @@ Proof.
intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
econstructor; split.
eapply exec_straight_opt_right. eexact A. apply exec_straight_one. rewrite EXEC.
- unfold exec_load. rewrite PtrEq. rewrite B, LOAD. eauto. Simpl.
+ unfold exec_load_offset. rewrite PtrEq. unfold exec_load. rewrite B, LOAD. eauto. Simpl.
split; intros; Simpl. auto.
Qed.
Lemma indexed_store_access_correct:
forall chunk (mk_instr: ireg -> offset -> basic) r1 m,
(forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
forall (base: ireg) ofs k (rs: regset) m',
Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs#r1) = Some m' ->
base <> RTMP -> r1 <> RTMP ->
@@ -1797,12 +1797,11 @@ Proof.
intros (base' & ofs' & rs' & ptr' & A & PtrEq & B & C).
econstructor; split.
eapply exec_straight_opt_right. eapply A. apply exec_straight_one. rewrite EXEC.
- unfold exec_store. rewrite PtrEq. rewrite B, C, STORE.
+ unfold exec_store_offset. rewrite PtrEq. unfold exec_store. rewrite B, C, STORE.
eauto.
discriminate.
{ intro. inv H. contradiction. }
auto.
-(* intros; Simpl. rewrite C; auto. *)
Qed.
Lemma loadind_correct:
@@ -1821,7 +1820,7 @@ Proof.
/\ c = indexed_memory_access mk_instr base ofs :: k
/\ forall base' ofs' rs',
exec_basic_instr ge (mk_instr base' ofs') rs' m =
- exec_load ge (chunk_of_type ty) rs' m rd base' ofs').
+ exec_load_offset ge (chunk_of_type ty) rs' m rd base' ofs').
{ unfold loadind in TR.
destruct ty, (preg_of dst); inv TR; econstructor; esplit; eauto. }
destruct A as (mk_instr & rd & rdEq & B & C). subst c. rewrite rdEq.
@@ -1843,7 +1842,7 @@ Proof.
/\ c = indexed_memory_access mk_instr base ofs :: k
/\ forall base' ofs' rs',
exec_basic_instr ge (mk_instr base' ofs') rs' m =
- exec_store ge (chunk_of_type ty) rs' m rr base' ofs').
+ exec_store_offset ge (chunk_of_type ty) rs' m rr base' ofs').
{ unfold storeind in TR. destruct ty, (preg_of src); inv TR; econstructor; esplit; eauto. }
destruct A as (mk_instr & rr & rsEq & B & C). subst c.
eapply indexed_store_access_correct; eauto with asmgen.
@@ -1945,7 +1944,7 @@ Qed.
Lemma transl_load_access_correct:
forall chunk (mk_instr: ireg -> offset -> basic) addr args k c rd (rs: regset) m v v',
(forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs) ->
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs) ->
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.loadv chunk m v = Some v' ->
@@ -1959,14 +1958,14 @@ Proof.
intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
econstructor; split.
eapply exec_straight_opt_right. eexact A. apply exec_straight_one.
- rewrite INSTR. unfold exec_load. rewrite PtrEq, B, LOAD. reflexivity. Simpl.
+ rewrite INSTR. unfold exec_load_offset. unfold exec_load. rewrite PtrEq, B, LOAD. reflexivity. Simpl.
split; intros; Simpl. auto.
Qed.
Lemma transl_store_access_correct:
forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
(forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk rs m r1 base ofs) ->
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk rs m r1 base ofs) ->
transl_memory_access mk_instr addr args k = OK c ->
eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
Mem.storev chunk m v rs#r1 = Some m' ->
@@ -1980,7 +1979,7 @@ Proof.
intros (base & ofs & rs' & ptr & A & PtrEq & B & C).
econstructor; split.
eapply exec_straight_opt_right. eexact A. apply exec_straight_one.
- rewrite INSTR. unfold exec_store. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
+ rewrite INSTR. unfold exec_store_offset. unfold exec_store. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
intro. inv H. contradiction.
auto.
Qed.
@@ -2000,7 +1999,7 @@ Proof.
preg_of dst = IR rd
/\ transl_memory_access mk_instr addr args k = OK c
/\ forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_load ge chunk rs m rd base ofs).
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_load_offset ge chunk rs m rd base ofs).
{ unfold transl_load in TR; destruct chunk; ArgsInv; econstructor; (esplit; eauto). }
destruct A as (mk_instr & rd & rdEq & B & C). rewrite rdEq.
eapply transl_load_access_correct; eauto with asmgen.
@@ -2020,7 +2019,7 @@ Proof.
preg_of src = IR rr
/\ transl_memory_access mk_instr addr args k = OK c
/\ (forall base ofs rs,
- exec_basic_instr ge (mk_instr base ofs) rs m = exec_store ge chunk' rs m rr base ofs)
+ exec_basic_instr ge (mk_instr base ofs) rs m = exec_store_offset ge chunk' rs m rr base ofs)
/\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src)).
{ unfold transl_store in TR; destruct chunk; ArgsInv;
(econstructor; econstructor; econstructor; split; [eauto | split; [eassumption | split; [ intros; simpl; reflexivity | auto]]]).
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index f1528389..a9f17f33 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -157,10 +157,10 @@ let expand_builtin_memcpy_big sz al src dst =
let lbl = new_label() in
emit (Ploopdo (tmpbuf, lbl));
emit Psemi;
- emit (Plb (tmpbuf, srcptr, Asmblock.Ofsimm Z.zero));
+ emit (Plb (tmpbuf, srcptr, AOff (Asmblock.Ofsimm Z.zero)));
emit (Paddil (srcptr, srcptr, Z.one));
emit Psemi;
- emit (Psb (tmpbuf, dstptr, Asmblock.Ofsimm Z.zero));
+ emit (Psb (tmpbuf, dstptr, AOff (Asmblock.Ofsimm Z.zero)));
emit (Paddil (dstptr, dstptr, Z.one));
emit Psemi;
emit (Plabel lbl);;
@@ -176,30 +176,30 @@ let expand_builtin_memcpy sz al args =
let expand_builtin_vload_common chunk base ofs res =
match chunk, res with
| Mint8unsigned, BR(Asmblock.IR res) ->
- emit (Plbu (res, base, Asmblock.Ofsimm ofs))
+ emit (Plbu (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint8signed, BR(Asmblock.IR res) ->
- emit (Plb (res, base, Asmblock.Ofsimm ofs))
+ emit (Plb (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint16unsigned, BR(Asmblock.IR res) ->
- emit (Plhu (res, base, Asmblock.Ofsimm ofs))
+ emit (Plhu (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint16signed, BR(Asmblock.IR res) ->
- emit (Plh (res, base, Asmblock.Ofsimm ofs))
+ emit (Plh (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint32, BR(Asmblock.IR res) ->
- emit (Plw (res, base, Asmblock.Ofsimm ofs))
+ emit (Plw (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint64, BR(Asmblock.IR res) ->
- emit (Pld (res, base, Asmblock.Ofsimm ofs))
+ emit (Pld (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mint64, BR_splitlong(BR(Asmblock.IR res1), BR(Asmblock.IR res2)) ->
let ofs' = Ptrofs.add ofs _4 in
if base <> res2 then begin
- emit (Plw (res2, base, Asmblock.Ofsimm ofs));
- emit (Plw (res1, base, Asmblock.Ofsimm ofs'))
+ emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs)));
+ emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs')))
end else begin
- emit (Plw (res1, base, Asmblock.Ofsimm ofs'));
- emit (Plw (res2, base, Asmblock.Ofsimm ofs))
+ emit (Plw (res1, base, AOff (Asmblock.Ofsimm ofs')));
+ emit (Plw (res2, base, AOff (Asmblock.Ofsimm ofs)))
end
| Mfloat32, BR(Asmblock.IR res) ->
- emit (Pfls (res, base, Asmblock.Ofsimm ofs))
+ emit (Pfls (res, base, AOff (Asmblock.Ofsimm ofs)))
| Mfloat64, BR(Asmblock.IR res) ->
- emit (Pfld (res, base, Asmblock.Ofsimm ofs))
+ emit (Pfld (res, base, AOff (Asmblock.Ofsimm ofs)))
| _ ->
assert false
@@ -218,21 +218,21 @@ let expand_builtin_vload chunk args res =
let expand_builtin_vstore_common chunk base ofs src =
match chunk, src with
| (Mint8signed | Mint8unsigned), BA(Asmblock.IR src) ->
- emit (Psb (src, base, Asmblock.Ofsimm ofs))
+ emit (Psb (src, base, AOff (Asmblock.Ofsimm ofs)))
| (Mint16signed | Mint16unsigned), BA(Asmblock.IR src) ->
- emit (Psh (src, base, Asmblock.Ofsimm ofs))
+ emit (Psh (src, base, AOff (Asmblock.Ofsimm ofs)))
| Mint32, BA(Asmblock.IR src) ->
- emit (Psw (src, base, Asmblock.Ofsimm ofs))
+ emit (Psw (src, base, AOff (Asmblock.Ofsimm ofs)))
| Mint64, BA(Asmblock.IR src) ->
- emit (Psd (src, base, Asmblock.Ofsimm ofs))
+ emit (Psd (src, base, AOff (Asmblock.Ofsimm ofs)))
| Mint64, BA_splitlong(BA(Asmblock.IR src1), BA(Asmblock.IR src2)) ->
let ofs' = Ptrofs.add ofs _4 in
- emit (Psw (src2, base, Asmblock.Ofsimm ofs));
- emit (Psw (src1, base, Asmblock.Ofsimm ofs'))
+ emit (Psw (src2, base, AOff (Asmblock.Ofsimm ofs)));
+ emit (Psw (src1, base, AOff (Asmblock.Ofsimm ofs')))
| Mfloat32, BA(Asmblock.IR src) ->
- emit (Pfss (src, base, Asmblock.Ofsimm ofs))
+ emit (Pfss (src, base, AOff (Asmblock.Ofsimm ofs)))
| Mfloat64, BA(Asmblock.IR src) ->
- emit (Pfsd (src, base, Asmblock.Ofsimm ofs))
+ emit (Pfsd (src, base, AOff (Asmblock.Ofsimm ofs)))
| _ ->
assert false
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index d553c612..cae79287 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -70,24 +70,42 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
(* TODO: factoriser ? *)
Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
- (d: ireg) (a: ireg) (ofs: offset) :=
+ (d: ireg) (a: ireg) (ptr: ptrofs) :=
+ match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
+ | None => Stuck
+ | Some v => Next (rsw#d <- v) mw
+ end
+.
+
+Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) :=
match (eval_offset ge ofs) with
- | OK ptr =>
- match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
- | None => Stuck
- | Some v => Next (rsw#d <- v) mw
- end
+ | OK ptr => parexec_load chunk rsr rsw mr mw d a ptr
+ | _ => Stuck
+ end.
+
+Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
+ match (rsr ro) with
+ | Vptr _ ofs => parexec_load chunk rsr rsw mr mw d a ofs
| _ => Stuck
end.
Definition parexec_store (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
- (s: ireg) (a: ireg) (ofs: offset) :=
+ (s: ireg) (a: ireg) (ptr: ptrofs) :=
+ match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
+ | None => Stuck
+ | Some m' => Next rsw m'
+ end
+.
+
+Definition parexec_store_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a: ireg) (ofs: offset) :=
match (eval_offset ge ofs) with
- | OK ptr =>
- match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
- | None => Stuck
- | Some m' => Next rsw m'
- end
+ | OK ptr => parexec_store chunk rsr rsw mr mw s a ptr
+ | _ => Stuck
+ end.
+
+Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) :=
+ match (rsr ro) with
+ | Vptr _ ofs => parexec_store chunk rsr rsw mr mw s a ofs
| _ => Stuck
end.
@@ -100,9 +118,11 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
match bi with
| PArith ai => Next (parexec_arith_instr ai rsr rsw) mw
- | PLoadRRO n d a ofs => parexec_load (load_chunk n) rsr rsw mr mw d a ofs
+ | 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
- | PStoreRRO n s a ofs => parexec_store (store_chunk n) rsr rsw mr mw s 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
| Pallocframe sz pos =>
let (mw, stk) := Mem.alloc mr 0 sz in
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 62df124a..762c67fc 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -201,10 +201,14 @@ 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}
+ | 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}
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))
; is_control = false}
+ | PStoreRRR (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}
let get_rec (rd:gpreg) rs = { inst = get_str; write_locs = [Reg (IR rd)]; read_locs = [Reg rs]; imm = None; is_control = false }
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 4e33fc90..77014bdc 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -95,23 +95,47 @@ Proof.
- repeat (rewrite Pregmap.gso); auto.
Qed.
-Lemma exec_load_pc_var:
+Lemma exec_load_offset_pc_var:
forall ge t rs m rd ra ofs rs' m' v,
- exec_load ge t rs m rd ra ofs = Next rs' m' ->
- exec_load ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+ exec_load_offset ge t rs m rd ra ofs = Next rs' m' ->
+ exec_load_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
Proof.
- intros. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+ intros. unfold exec_load_offset in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); 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_pc_var:
+Lemma exec_load_reg_pc_var:
+ forall t rs m rd ra ro rs' m' v,
+ exec_load_reg t rs m rd ra ro = Next rs' m' ->
+ exec_load_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_load_reg in *. unfold exec_load in *. rewrite Pregmap.gso; try discriminate. destruct (rs ro); 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 ge t rs m rd ra ofs = Next rs' m' ->
- exec_store ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+ exec_store_offset ge t rs m rd ra ofs = Next rs' m' ->
+ exec_store_offset ge t rs # PC <- v m rd ra ofs = Next rs' # PC <- v m'.
+Proof.
+ intros. unfold exec_store_offset in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate.
+ destruct (eval_offset ge ofs); try discriminate.
+ destruct (Mem.storev _ _ _).
+ - inv H. apply next_eq; auto.
+ - discriminate.
+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' ->
+ exec_store_reg t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
Proof.
- intros. unfold exec_store in *. rewrite Pregmap.gso; try discriminate. destruct (eval_offset ge ofs); try discriminate.
+ intros. unfold exec_store_reg in *. unfold exec_store in *. rewrite Pregmap.gso; try discriminate.
+ destruct (rs ro); try discriminate.
destruct (Mem.storev _ _ _).
- inv H. apply next_eq; auto.
- discriminate.
@@ -129,8 +153,12 @@ Proof.
(* Some cases treated seperately because exploreInst destructs too much *)
all: try (inv H; apply next_eq; auto; apply functional_extensionality; intros; rewrite regset_double_set; auto; discriminate).
- - exploreInst; apply exec_load_pc_var; auto.
- - exploreInst; apply exec_store_pc_var; auto.
+ - destruct i.
+ + exploreInst; apply exec_load_offset_pc_var; auto.
+ + exploreInst; apply exec_load_reg_pc_var; auto.
+ - destruct i.
+ + exploreInst; apply exec_store_offset_pc_var; auto.
+ + exploreInst; apply exec_store_reg_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.
@@ -559,16 +587,16 @@ Proof.
intros. unfold eval_offset. destruct ofs; auto. erewrite symbol_address_preserved; eauto.
Qed.
-Lemma transf_exec_load:
- forall t rs m rd ra ofs, exec_load ge t rs m rd ra ofs = exec_load tge t rs m rd ra ofs.
+Lemma transf_exec_load_offset:
+ forall t rs m rd ra ofs, exec_load_offset ge t rs m rd ra ofs = exec_load_offset tge t rs m rd ra ofs.
Proof.
- intros. unfold exec_load. rewrite eval_offset_preserved. reflexivity.
+ intros. unfold exec_load_offset. rewrite eval_offset_preserved. reflexivity.
Qed.
-Lemma transf_exec_store:
- forall t rs m rs0 ra ofs, exec_store ge t rs m rs0 ra ofs = exec_store tge t rs m rs0 ra ofs.
+Lemma transf_exec_store_offset:
+ forall t rs m rs0 ra ofs, exec_store_offset ge t rs m rs0 ra ofs = exec_store_offset tge t rs m rs0 ra ofs.
Proof.
- intros. unfold exec_store. rewrite eval_offset_preserved. reflexivity.
+ intros. unfold exec_store_offset. rewrite eval_offset_preserved. reflexivity.
Qed.
Lemma transf_exec_basic_instr:
@@ -577,8 +605,8 @@ Proof.
intros. pose symbol_address_preserved.
unfold exec_basic_instr. exploreInst; simpl; auto; try congruence.
- unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence.
- - apply transf_exec_load.
- - apply transf_exec_store.
+ - apply transf_exec_load_offset.
+ - apply transf_exec_store_offset.
Qed.
Lemma transf_exec_body:
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 6416b65b..ef02c25a 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -164,6 +164,10 @@ module Target (*: TARGET*) =
| Ofsimm n -> ptrofs oc n
| Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
+ let addressing oc = function
+ | AOff ofs -> offset oc ofs
+ | AReg ro -> ireg oc ro
+
let icond_name = let open Asmblock in function
| ITne | ITneu -> "ne"
| ITeq | ITequ -> "eq"
@@ -287,27 +291,27 @@ module Target (*: TARGET*) =
section oc Section_text
(* Load/Store instructions *)
- | Plb(rd, ra, ofs) ->
- fprintf oc " lbs %a = %a[%a]\n" ireg rd offset ofs ireg ra
- | Plbu(rd, ra, ofs) ->
- fprintf oc " lbz %a = %a[%a]\n" ireg rd offset ofs ireg ra
- | Plh(rd, ra, ofs) ->
- fprintf oc " lhs %a = %a[%a]\n" ireg rd offset ofs ireg ra
- | Plhu(rd, ra, ofs) ->
- fprintf oc " lhz %a = %a[%a]\n" ireg rd offset ofs ireg ra
- | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
- fprintf oc " lws %a = %a[%a]\n" ireg rd offset ofs ireg ra
- | Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
- fprintf oc " ld %a = %a[%a]\n" ireg rd offset ofs ireg ra
+ | Plb(rd, ra, adr) ->
+ fprintf oc " lbs %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ | Plbu(rd, ra, adr) ->
+ fprintf oc " lbz %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ | Plh(rd, ra, adr) ->
+ fprintf oc " lhs %a = %a[%a]\n" ireg rd addressing adr ireg ra
+ | Plhu(rd, ra, adr) ->
+ fprintf oc " lhz %a = %a[%a]\n" 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
+ | 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
- | Psb(rd, ra, ofs) ->
- fprintf oc " sb %a[%a] = %a\n" offset ofs ireg ra ireg rd
- | Psh(rd, ra, ofs) ->
- fprintf oc " sh %a[%a] = %a\n" offset ofs ireg ra ireg rd
- | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
- fprintf oc " sw %a[%a] = %a\n" offset ofs ireg ra ireg rd
- | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
- fprintf oc " sd %a[%a] = %a\n" offset ofs ireg ra ireg rd
+ | Psb(rd, ra, adr) ->
+ fprintf oc " sb %a[%a] = %a\n" addressing adr ireg ra ireg rd
+ | Psh(rd, ra, adr) ->
+ fprintf oc " sh %a[%a] = %a\n" addressing adr ireg ra ireg rd
+ | Psw(rd, ra, adr) | Psw_a(rd, ra, adr) | Pfss(rd, ra, adr) ->
+ fprintf oc " sw %a[%a] = %a\n" 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\n" addressing adr ireg ra ireg rd
(* Arith R instructions *)
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 69234938..ed8edfde 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -943,14 +943,16 @@ Lemma exec_basic_instr_pc:
Proof.
intros. destruct b; try destruct i; try destruct i.
all: try (inv H; Simpl).
- all: try (unfold exec_load in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
- all: try (unfold exec_store in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
- destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
- destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
- destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
- destruct rs; try discriminate. inv H1. Simpl.
- destruct rd; try discriminate. inv H1; Simpl.
- auto.
+ 1-10: try (unfold exec_load_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+ 1-10: try (unfold exec_load_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_load in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+ 1-10: try (unfold exec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
+ 1-10: try (unfold exec_store_reg in H1; destruct (rs1 rofs); try discriminate; unfold exec_store in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+ - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
+ - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
+ destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
+ - destruct rs; try discriminate. inv H1. Simpl.
+ - destruct rd; try discriminate. inv H1; Simpl.
+ - reflexivity.
Qed.
(* Lemma exec_straight_pc':
generated by cgit (git 2.34.1) at 2024-07-14 12:00:26 +0000