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.v58
-rw-r--r--mppa_k1c/Asmblockdeps.v212
-rw-r--r--mppa_k1c/Asmblockgen.v115
-rw-r--r--mppa_k1c/Asmblockgenproof.v450
-rw-r--r--mppa_k1c/Asmblockgenproof1.v306
-rw-r--r--mppa_k1c/Asmexpand.ml44
-rw-r--r--mppa_k1c/Asmvliw.v42
-rw-r--r--mppa_k1c/Op.v11
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml4
-rw-r--r--mppa_k1c/PostpassSchedulingproof.v63
-rw-r--r--mppa_k1c/PrintOp.ml1
-rw-r--r--mppa_k1c/SelectLong.vp5
-rw-r--r--mppa_k1c/SelectLongproof.v16
-rw-r--r--mppa_k1c/SelectOp.vp1
-rw-r--r--mppa_k1c/SelectOpproof.v1
-rw-r--r--mppa_k1c/TargetPrinter.ml44
-rw-r--r--mppa_k1c/ValueAOp.v1
-rw-r--r--mppa_k1c/lib/Asmblockgenproof0.v18
19 files changed, 694 insertions, 795 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 f3f59f7d..e612576f 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -244,7 +244,7 @@ Inductive cf_instruction : Type :=
.
(** Loads **)
-Inductive load_name_rro : Type :=
+Inductive load_name : Type :=
| Plb (**r load byte *)
| Plbu (**r load byte unsigned *)
| Plh (**r load half word *)
@@ -258,13 +258,15 @@ Inductive load_name_rro : Type :=
.
Inductive ld_instruction : Type :=
- | PLoadRRO (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset)
+ | PLoadRRO (i: load_name) (rd: ireg) (ra: ireg) (ofs: offset)
+ | PLoadRRR (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
.
-Coercion PLoadRRO: load_name_rro >-> Funclass.
+Coercion PLoadRRO: load_name >-> Funclass.
+Coercion PLoadRRR: load_name >-> Funclass.
(** Stores **)
-Inductive store_name_rro : Type :=
+Inductive store_name : Type :=
| Psb (**r store byte *)
| Psh (**r store half byte *)
| Psw (**r store int32 *)
@@ -276,10 +278,12 @@ Inductive store_name_rro : Type :=
.
Inductive st_instruction : Type :=
- | PStoreRRO (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset)
+ | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
+ | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
.
-Coercion PStoreRRO: store_name_rro >-> Funclass.
+Coercion PStoreRRO: store_name >-> Funclass.
+Coercion PStoreRRR: store_name >-> Funclass.
(** Arithmetic instructions **)
Inductive arith_name_r : Type :=
@@ -1258,28 +1262,36 @@ Definition eval_offset (ofs: offset) : res ptrofs :=
end
end.
-Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem)
- (d: ireg) (a: ireg) (ofs: offset) :=
+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 => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with
+ | None => Stuck
+ | Some v => Next (rs#d <- v) m
+ end
| _ => Stuck
end.
-Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem)
- (s: ireg) (a: ireg) (ofs: offset) :=
+Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) :=
+ match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with
+ | None => Stuck
+ | Some v => Next (rs#d <- v) 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 => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with
+ | None => Stuck
+ | Some m' => Next rs m'
+ end
| _ => Stuck
end.
+Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) :=
+ match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with
+ | None => Stuck
+ | Some m' => Next rs m'
+ end.
+
Definition load_chunk n :=
match n with
| Plb => Mint8signed
@@ -1312,9 +1324,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 6d87a34d..9180eabb 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -71,16 +71,18 @@ Coercion OArithRRI32: arith_name_rri32 >-> Funclass.
Coercion OArithRRI64: arith_name_rri64 >-> Funclass.
Inductive load_op :=
- | OLoadRRO (n: load_name_rro) (ofs: offset)
+ | OLoadRRO (n: load_name) (ofs: offset)
+ | OLoadRRR (n: load_name)
.
-Coercion OLoadRRO: load_name_rro >-> Funclass.
+Coercion OLoadRRO: load_name >-> Funclass.
Inductive store_op :=
- | OStoreRRO (n: store_name_rro) (ofs: offset)
+ | OStoreRRO (n: store_name) (ofs: offset)
+ | OStoreRRR (n: store_name)
.
-Coercion OStoreRRO: store_name_rro >-> Funclass.
+Coercion OStoreRRO: store_name >-> Funclass.
Inductive op_wrap :=
| Arith (ao: arith_op)
@@ -125,39 +127,49 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
| _, _ => None
end.
-Definition exec_load_deps (chunk: memory_chunk) (m: mem)
- (v: val) (ofs: offset) :=
+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 => match Mem.loadv chunk m (Val.offset_ptr v ptr) with
+ | None => None
+ | Some vl => Some (Val vl)
+ end
| _ => None
end.
+Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) :=
+ match Mem.loadv chunk m (Val.addl v vo) 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 (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) :=
+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 => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with
+ | None => None
+ | Some m' => Some (Memstate m')
+ end
| _ => None
end.
+Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
+ match Mem.storev chunk m (Val.addl va vo) vs with
+ | None => None
+ | Some m' => Some (Memstate m')
+ 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.
@@ -335,12 +347,16 @@ Opaque arith_op_eq_correct.
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; try congruence.
+ destruct o1, o2; wlp_simplify; try discriminate.
+ - congruence.
+ - congruence.
Qed.
Hint Resolve load_op_eq_correct: wlp.
Opaque load_op_eq_correct.
@@ -349,12 +365,16 @@ Opaque load_op_eq_correct.
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; try congruence.
+ destruct o1, o2; wlp_simplify; try discriminate.
+ - congruence.
+ - congruence.
Qed.
Hint Resolve store_op_eq_correct: wlp.
Opaque store_op_eq_correct.
@@ -585,12 +605,14 @@ Definition trans_arith (ai: ar_instruction) : inst :=
Definition trans_basic (b: basic) : inst :=
match b with
| PArith ai => trans_arith ai
- | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg(#a) @ PReg pmem @ Enil))]
- | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg(#s) @ PReg(#a) @ PReg pmem @ Enil))]
- | Pallocframe sz pos => [(#FP, PReg(#SP)); (#SP, Op (Allocframe2 sz pos) (PReg(#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
- (pmem, Op (Allocframe sz pos) (Old (PReg(#SP)) @ PReg pmem @ Enil))]
- | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg(#SP) @ PReg pmem @ Enil));
- (#SP, Op (Freeframe2 sz pos) (PReg(#SP) @ Old (PReg pmem) @ Enil));
+ | 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))]
+ | 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);
+ (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))]
+ | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil));
+ (#SP, Op (Freeframe2 sz pos) (PReg (#SP) @ Old (PReg pmem) @ Enil));
(#RTMP, Op (Constant Vundef) Enil)]
| Pget rd ra => match ra with
| RA => [(#rd, PReg(#ra))]
@@ -801,23 +823,42 @@ Proof.
- simpl in H. inv H. simpl inst_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;
+ destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0;
+ eexists; split; try split; [
+ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); 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 (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; 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;
+ 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); simpl in MEML; rewrite MEML; reflexivity
+ | Simpl
+ | intros rr; destruct rr; Simpl ].
+ (* Store Reg *)
+ + destruct i. all:
+ unfold exec_store_reg 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;
+ 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.
@@ -842,7 +883,7 @@ Proof.
- simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0.
eexists. split; try split. Simpl. intros rr; destruct rr; Simpl.
(* Pnop *)
- - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption.
+ - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption.
Qed.
Lemma forward_simu_body:
@@ -1155,13 +1196,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;
+ 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; simpl in H0; 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;
+ simpl in H0; 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;
+ 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.
@@ -1504,7 +1560,7 @@ Definition string_of_arith (op: arith_op): pstring :=
| OArithARRI64 n _ => string_of_name_arri64 n
end.
-Definition string_of_name_lrro (n: load_name_rro) : pstring :=
+Definition string_of_load_name (n: load_name) : pstring :=
match n with
Plb => "Plb"
| Plbu => "Plbu"
@@ -1520,10 +1576,11 @@ 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
+ | OLoadRRO n _ => string_of_load_name n
+ | OLoadRRR n => string_of_load_name n
end.
-Definition string_of_name_srro (n: store_name_rro) : pstring :=
+Definition string_of_store_name (n: store_name) : pstring :=
match n with
Psb => "Psb"
| Psh => "Psh"
@@ -1537,7 +1594,8 @@ 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
+ | OStoreRRO n _ => string_of_store_name n
+ | OStoreRRR n => string_of_store_name n
end.
Definition string_of_control (op: control_op) : pstring :=
@@ -1727,21 +1785,39 @@ Proof.
(* Arith *)
- exploit trans_arith_par_correct. 5: eauto. all: eauto.
(* Load *)
- - destruct i; unfold parexec_load; simpl; unfold exec_load_deps.
- erewrite GENV, H, H0.
- destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto.
- destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto.
- eexists; intuition eauto; Simpl.
- destruct r; 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].
+ - destruct i.
+ (* Load Offset *)
+ + destruct i; simpl load_chunk. all:
+ unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0;
+ destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto;
+ destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto;
+ eexists; split; try split; Simpl;
+ intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+
+ (* Load Reg *)
+ + destruct i; simpl load_chunk. all:
+ unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; 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; unfold parexec_store; simpl; unfold exec_store_deps.
- erewrite GENV, H, ! H0.
- destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto.
- destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto.
- eexists; intuition eauto; Simpl.
+ - destruct i.
+ (* Store Offset *)
+ + destruct i; simpl store_chunk. all:
+ unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra);
+ destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto;
+ destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
+ eexists; split; try split; Simpl;
+ intros rr; destruct rr; Simpl.
+
+ (* Store Reg *)
+ + destruct i; simpl store_chunk. all:
+ unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs);
+ destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
+ eexists; split; try split; Simpl;
+ intros rr; destruct rr; Simpl.
+
(* Allocframe *)
- destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
* eexists; repeat split.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 1afb627a..3260312d 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -741,11 +741,7 @@ Definition indexed_memory_access
match make_immed64 (Ptrofs.to_int64 ofs) with
| Imm64_single imm =>
mk_instr base (Ofsimm (Ptrofs.of_int64 imm))
-(*| Imm64_pair hi lo =>
- Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
- | Imm64_large imm =>
- Pmake GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k
-*)end.
+end.
Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
match ty, preg_of dst with
@@ -777,6 +773,17 @@ Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) :=
(** Translation of memory accesses: loads, and stores. *)
+Definition transl_memory_access2
+ (mk_instr: ireg -> ireg -> basic)
+ (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
+ match addr, args with
+ | Aindexed2, a1 :: a2 :: nil =>
+ do rs1 <- ireg_of a1;
+ do rs2 <- ireg_of a2;
+ OK (mk_instr rs1 rs2 ::i k)
+ | _, _ => Error (msg "Asmblockgen.transl_memory_access2")
+ end.
+
Definition transl_memory_access
(mk_instr: ireg -> offset -> basic)
(addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
@@ -792,60 +799,64 @@ Definition transl_memory_access
Error(msg "Asmblockgen.transl_memory_access")
end.
+Definition chunk2load (chunk: memory_chunk) :=
+ match chunk with
+ | Mint8signed => Plb
+ | Mint8unsigned => Plbu
+ | Mint16signed => Plh
+ | Mint16unsigned => Plhu
+ | Mint32 => Plw
+ | Mint64 => Pld
+ | Mfloat32 => Pfls
+ | Mfloat64 => Pfld
+ | Many32 => Plw_a
+ | Many64 => Pld_a
+ end.
+
+Definition transl_load_rro (chunk: memory_chunk) (addr: addressing)
+ (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+ do r <- ireg_of dst;
+ transl_memory_access (PLoadRRO (chunk2load chunk) r) addr args k.
+
+Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing)
+ (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+ do r <- ireg_of dst;
+ transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k.
+
Definition transl_load (chunk: memory_chunk) (addr: addressing)
(args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+ match addr with
+ | Aindexed2 => transl_load_rrr chunk addr args dst k
+ | _ => transl_load_rro chunk addr args dst k
+ end.
+
+Definition chunk2store (chunk: memory_chunk) :=
match chunk with
- | Mint8signed =>
- do r <- ireg_of dst;
- transl_memory_access (Plb r) addr args k
- | Mint8unsigned =>
- do r <- ireg_of dst;
- transl_memory_access (Plbu r) addr args k
- | Mint16signed =>
- do r <- ireg_of dst;
- transl_memory_access (Plh r) addr args k
- | Mint16unsigned =>
- do r <- ireg_of dst;
- transl_memory_access (Plhu r) addr args k
- | Mint32 =>
- do r <- ireg_of dst;
- transl_memory_access (Plw r) addr args k
- | Mint64 =>
- do r <- ireg_of dst;
- transl_memory_access (Pld r) addr args k
- | Mfloat32 =>
- do r <- freg_of dst;
- transl_memory_access (Pfls r) addr args k
- | Mfloat64 =>
- do r <- freg_of dst;
- transl_memory_access (Pfld r) addr args k
- | _ =>
- Error (msg "Asmblockgen.transl_load")
+ | Mint8signed | Mint8unsigned => Psb
+ | Mint16signed | Mint16unsigned => Psh
+ | Mint32 => Psw
+ | Mint64 => Psd
+ | Mfloat32 => Pfss
+ | Mfloat64 => Pfsd
+ | Many32 => Psw_a
+ | Many64 => Psd_a
end.
+Definition transl_store_rro (chunk: memory_chunk) (addr: addressing)
+ (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+ do r <- ireg_of src;
+ transl_memory_access (PStoreRRO (chunk2store chunk) r) addr args k.
+
+Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing)
+ (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+ do r <- ireg_of src;
+ transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k.
+
Definition transl_store (chunk: memory_chunk) (addr: addressing)
(args: list mreg) (src: mreg) (k: bcode) : res bcode :=
- match chunk with
- | Mint8signed | Mint8unsigned =>
- do r <- ireg_of src;
- transl_memory_access (Psb r) addr args k
- | Mint16signed | Mint16unsigned =>
- do r <- ireg_of src;
- transl_memory_access (Psh r) addr args k
- | Mint32 =>
- do r <- ireg_of src;
- transl_memory_access (Psw r) addr args k
- | Mint64 =>
- do r <- ireg_of src;
- transl_memory_access (Psd r) addr args k
- | Mfloat32 =>
- do r <- freg_of src;
- transl_memory_access (Pfss r) addr args k
- | Mfloat64 =>
- do r <- freg_of src;
- transl_memory_access (Pfsd r) addr args k
- | _ =>
- Error (msg "Asmblockgen.transl_store")
+ match addr with
+ | Aindexed2 => transl_store_rrr chunk addr args src k
+ | _ => transl_store_rro chunk addr args src k
end.
(** Function epilogue *)
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 63f4c136..70f188ec 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -16,7 +16,6 @@ Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock.
-(* Require Import Asmgen Asmgenproof0 Asmgenproof1. *)
Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1.
Module MB := Machblock.
@@ -75,34 +74,6 @@ Proof.
omega.
Qed.
-(*
-Lemma exec_straight_exec:
- forall fb f c ep tf tc c' rs m rs' m',
- transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
- exec_straight tge tf tc rs m c' rs' m' ->
- plus step tge (State rs m) E0 (State rs' m').
-Proof.
- intros. inv H.
- eapply exec_straight_steps_1; eauto.
- eapply transf_function_no_overflow; eauto.
- eapply functions_transl; eauto.
-Qed.
-
-Lemma exec_straight_at:
- forall fb f c ep tf tc c' ep' tc' rs m rs' m',
- transl_code_at_pc ge (rs PC) fb f c ep tf tc ->
- transl_code f c' ep' = OK tc' ->
- exec_straight tge tf tc rs m tc' rs' m' ->
- transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'.
-Proof.
- intros. inv H.
- exploit exec_straight_steps_2; eauto.
- eapply transf_function_no_overflow; eauto.
- eapply functions_transl; eauto.
- intros [ofs' [PC' CT']].
- rewrite PC'. constructor; auto.
-Qed.
- *)
(** The following lemmas show that the translation from Mach to Asm
preserves labels, in the sense that the following diagram commutes:
<<
@@ -121,314 +92,6 @@ Qed.
Section TRANSL_LABEL.
-(* Remark loadimm32_label:
- forall r n k, tail_nolabel k (loadimm32 r n k).
-Proof.
- intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel.
-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
-Qed.
-Hint Resolve loadimm32_label: labels.
-
-Remark opimm32_label:
- forall (op: arith_name_rrr) (opimm: arith_name_rri32) r1 r2 n k,
- (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
- (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
- tail_nolabel k (opimm32 op opimm r1 r2 n k).
-Proof.
- intros; unfold opimm32. destruct (make_immed32 n); TailNoLabel.
-(*unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel.*)
-Qed.
-Hint Resolve opimm32_label: labels.
-
-Remark loadimm64_label:
- forall r n k, tail_nolabel k (loadimm64 r n k).
-Proof.
- intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel.
-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
-Qed.
-Hint Resolve loadimm64_label: labels.
-
-Remark cast32signed_label:
- forall rd rs k, tail_nolabel k (cast32signed rd rs k).
-Proof.
- intros; unfold cast32signed. destruct (ireg_eq rd rs); TailNoLabel.
-Qed.
-Hint Resolve cast32signed_label: labels.
-
-Remark opimm64_label:
- forall (op: arith_name_rrr) (opimm: arith_name_rri64) r1 r2 n k,
- (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
- (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
- tail_nolabel k (opimm64 op opimm r1 r2 n k).
-Proof.
- intros; unfold opimm64. destruct (make_immed64 n); TailNoLabel.
-(*unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel.*)
-Qed.
-Hint Resolve opimm64_label: labels.
-
-Remark addptrofs_label:
- forall r1 r2 n k, tail_nolabel k (addptrofs r1 r2 n k).
-Proof.
- unfold addptrofs; intros. destruct (Ptrofs.eq_dec n Ptrofs.zero). TailNoLabel.
- apply opimm64_label; TailNoLabel.
-Qed.
-Hint Resolve addptrofs_label: labels.
-(*
-Remark transl_cond_float_nolabel:
- forall c r1 r2 r3 insn normal,
- transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
- unfold transl_cond_float; intros. destruct c; inv H; exact I.
-Qed.
-
-Remark transl_cond_single_nolabel:
- forall c r1 r2 r3 insn normal,
- transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn.
-Proof.
- unfold transl_cond_single; intros. destruct c; inv H; exact I.
-Qed.
-*)
-Remark transl_cbranch_label:
- forall cond args lbl k c,
- transl_cbranch cond args lbl k = OK c -> tail_nolabel k c.
-Proof.
- intros. unfold transl_cbranch in H. destruct cond; TailNoLabel.
-(* Ccomp *)
- - unfold transl_comp; TailNoLabel.
-(* Ccompu *)
- - unfold transl_comp; TailNoLabel.
-(* Ccompimm *)
- - destruct (Int.eq n Int.zero); TailNoLabel.
- unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
-(* Ccompuimm *)
- - unfold transl_opt_compuimm.
- remember (select_comp n c0) as selcomp; destruct selcomp.
- + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp;
- destruct (Int.eq n Int.zero); destruct c0; discriminate.
- + unfold loadimm32;
- destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel.
-(* Ccompl *)
- - unfold transl_compl; TailNoLabel.
-(* Ccomplu *)
- - unfold transl_compl; TailNoLabel.
-(* Ccomplimm *)
- - destruct (Int64.eq n Int64.zero); TailNoLabel.
- unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
-(* Ccompluimm *)
- - unfold transl_opt_compluimm.
- remember (select_compl n c0) as selcomp; destruct selcomp.
- + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_compl;
- destruct (Int64.eq n Int64.zero); destruct c0; discriminate.
- + unfold loadimm64;
- destruct (make_immed64 n); TailNoLabel; unfold transl_compl; TailNoLabel.
-Qed.
-
-(*
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
- destruct c0; simpl; TailNoLabel.
- apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k).
- auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int.eq n Int.zero).
- destruct c0; simpl; TailNoLabel.
- apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k).
- auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
- destruct c0; simpl; TailNoLabel.
- apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k).
- auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (Int64.eq n Int64.zero).
- destruct c0; simpl; TailNoLabel.
- apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k).
- auto with labels. destruct c0; simpl; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
- apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto.
- destruct normal; TailNoLabel.
-- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
- apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto.
- destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
- apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto.
- destruct normal; TailNoLabel.
-- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2.
- apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto.
- destruct normal; TailNoLabel.
-*)
-
-Remark transl_cond_op_label:
- forall cond args r k c,
- transl_cond_op cond r args k = OK c -> tail_nolabel k c.
-Proof.
- intros. unfold transl_cond_op in H; destruct cond; TailNoLabel.
-- unfold transl_cond_int32s; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int32u; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int32s; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int32u; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int64s; destruct c0; simpl; TailNoLabel.
-- unfold transl_cond_int64u; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64s; destruct c0; simpl; TailNoLabel.
-- unfold transl_condimm_int64u; destruct c0; simpl; TailNoLabel.
-Qed.
-
-Remark transl_op_label:
- forall op args r k c,
- transl_op op args r k = OK c -> tail_nolabel k c.
-Proof.
-Opaque Int.eq.
- unfold transl_op; intros; destruct op; TailNoLabel.
-(* Omove *)
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-(* Oaddrsymbol *)
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)); TailNoLabel.
-(* Oaddimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oandimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oorimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oxorimm32 *)
-- apply opimm32_label; intros; exact I.
-(* Oshrximm *)
-- destruct (Int.eq n Int.zero); TailNoLabel.
-(* Oaddimm64 *)
-- apply opimm64_label; intros; exact I.
-(* Oandimm64 *)
-- apply opimm64_label; intros; exact I.
-(* Oorimm64 *)
-- apply opimm64_label; intros; exact I.
-(* Oxorimm64 *)
-- apply opimm64_label; intros; exact I.
-(* Ocmp *)
-- eapply transl_cond_op_label; eauto.
-Qed.
-
-(*
-- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
-- destruct (Float.eq_dec n Float.zero); TailNoLabel.
-- destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
-+ TailNoLabel.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- apply opimm32_label; intros; exact I.
-- destruct (Int.eq n Int.zero); TailNoLabel.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- apply opimm64_label; intros; exact I.
-- destruct (Int.eq n Int.zero); TailNoLabel.
-- eapply transl_cond_op_label; eauto.
-*)
-*)
-
-(* Remark indexed_memory_access_label:
- forall (mk_instr: ireg -> offset -> instruction) base ofs k,
- (forall r o, nolabel (mk_instr r o)) ->
- tail_nolabel k (indexed_memory_access mk_instr base ofs k).
-Proof.
- unfold indexed_memory_access; intros.
- (* destruct Archi.ptr64. *)
- destruct (make_immed64 (Ptrofs.to_int64 ofs)); TailNoLabel.
- (* destruct (make_immed32 (Ptrofs.to_int ofs)); TailNoLabel. *)
-Qed. *)
-
-(*
-Remark loadind_label:
- forall base ofs ty dst k c,
- loadind base ofs ty dst k = OK c -> tail_nolabel k c.
-Proof.
- unfold loadind; intros.
- destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark storeind_label:
- forall src base ofs ty k c,
- storeind src base ofs ty k = OK c -> tail_nolabel k c.
-Proof.
- unfold storeind; intros.
- destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I.
-Qed.
-
-Remark loadind_ptr_label:
- forall base ofs dst k, tail_nolabel k (loadind_ptr base ofs dst k).
-Proof.
- intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.
-Qed.
-*)
-
-(* Remark storeind_ptr_label:
- forall src base ofs k, tail_nolabel k (storeind_ptr src base ofs k).
-Proof.
- intros. apply indexed_memory_access_label. intros; destruct Archi.ptr64; exact I.
-Qed. *)
-
-(*
-Remark transl_memory_access_label:
- forall (mk_instr: ireg -> offset -> instruction) addr args k c,
- (forall r o, nolabel (mk_instr r o)) ->
- transl_memory_access mk_instr addr args k = OK c ->
- tail_nolabel k c.
-Proof.
- unfold transl_memory_access; intros; destruct addr; TailNoLabel; apply indexed_memory_access_label; auto.
-Qed.
-
-Remark make_epilogue_label:
- forall f k, tail_nolabel k (make_epilogue f k).
-Proof.
- unfold make_epilogue; intros. eapply tail_nolabel_trans. apply loadind_ptr_label. TailNoLabel.
-Qed.
-
-Lemma transl_instr_label:
- forall f i ep k c,
- transl_instr f i ep k = OK c ->
- match i with Mlabel lbl => c = Plabel lbl ::i k | _ => tail_nolabel k c end.
-Proof.
- unfold transl_instr; intros; destruct i; TailNoLabel.
-(* loadind *)
-- eapply loadind_label; eauto.
-(* storeind *)
-- eapply storeind_label; eauto.
-(* Mgetparam *)
-- destruct ep. eapply loadind_label; eauto.
- eapply tail_nolabel_trans. apply loadind_ptr_label. eapply loadind_label; eauto.
-(* transl_op *)
-- eapply transl_op_label; eauto.
-(* transl_load *)
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-(* transl store *)
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct s0; monadInv H; TailNoLabel.
-- destruct s0; monadInv H; eapply tail_nolabel_trans
- ; [eapply make_epilogue_label|TailNoLabel].
-- eapply transl_cbranch_label; eauto.
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-Qed.
-(*
-
-
-- eapply transl_op_label; eauto.
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
-- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
-*)
-
-Lemma transl_instr_label':
- forall lbl f i ep k c,
- transl_instr f i ep k = OK c ->
- find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k.
-Proof.
- intros. exploit transl_instr_label; eauto.
- destruct i; try (intros [A B]; apply B).
- intros. subst c. simpl. auto.
-Qed.
-*)
-
Lemma gen_bblocks_label:
forall hd bdy ex tbb tc,
gen_bblocks hd bdy ex = tbb::tc ->
@@ -640,115 +303,6 @@ Qed.
- Mach register values and Asm register values agree.
*)
-(*
-Lemma exec_straight_steps:
- forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2,
- match_stack ge s ->
- Mem.extends m2 m2' ->
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
- (forall k c (TR: transl_instr f i ep k = OK c),
- exists rs2,
- exec_straight tge tf c rs1 m1' k rs2 m2'
- /\ agree ms2 sp rs2
- /\ (fp_is_parent ep i = true -> rs2#FP = parent_sp s)) ->
- exists st',
- plus step tge (State rs1 m1') E0 st' /\
- match_states (Mach.State s fb sp c ms2 m2) st'.
-Proof.
- intros. inversion H2. subst. monadInv H7.
- exploit H3; eauto. intros [rs2 [A [B C]]].
- exists (State rs2 m2'); split.
- eapply exec_straight_exec; eauto.
- econstructor; eauto. eapply exec_straight_at; eauto.
-Qed.
-*)
-
-(*
-Lemma exec_straight_steps_goto:
- forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
- match_stack ge s ->
- Mem.extends m2 m2' ->
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
- transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
- fp_is_parent ep i = false ->
- (forall k c (TR: transl_instr f i ep k = OK c),
- exists jmp, exists k', exists rs2,
- exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
- /\ agree ms2 sp rs2
- /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
- exists st',
- plus step tge (State rs1 m1') E0 st' /\
- match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
- intros. inversion H3. subst. monadInv H9.
- exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
- generalize (functions_transl _ _ _ H7 H8); intro FN.
- generalize (transf_function_no_overflow _ _ H8); intro NOOV.
- exploit exec_straight_steps_2; eauto.
- intros [ofs' [PC2 CT2]].
- exploit find_label_goto_label; eauto.
- intros [tc' [rs3 [GOTO [AT' OTH]]]].
- exists (State rs3 m2'); split.
- eapply plus_right'.
- eapply exec_straight_steps_1; eauto.
- econstructor; eauto.
- eapply find_instr_tail. eauto.
- rewrite C. eexact GOTO.
- traceEq.
- econstructor; eauto.
- apply agree_exten with rs2; auto with asmgen.
- congruence.
-Qed.
-
-Lemma exec_straight_opt_steps_goto:
- forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c',
- match_stack ge s ->
- Mem.extends m2 m2' ->
- Genv.find_funct_ptr ge fb = Some (Internal f) ->
- Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
- transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
- fp_is_parent ep i = false ->
- (forall k c (TR: transl_instr f i ep k = OK c),
- exists jmp, exists k', exists rs2,
- exec_straight_opt tge tf c rs1 m1' (jmp :: k') rs2 m2'
- /\ agree ms2 sp rs2
- /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
- exists st',
- plus step tge (State rs1 m1') E0 st' /\
- match_states (Mach.State s fb sp c' ms2 m2) st'.
-Proof.
- intros. inversion H3. subst. monadInv H9.
- exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
- generalize (functions_transl _ _ _ H7 H8); intro FN.
- generalize (transf_function_no_overflow _ _ H8); intro NOOV.
- inv A.
-- exploit find_label_goto_label; eauto.
- intros [tc' [rs3 [GOTO [AT' OTH]]]].
- exists (State rs3 m2'); split.
- apply plus_one. econstructor; eauto.
- eapply find_instr_tail. eauto.
- rewrite C. eexact GOTO.
- econstructor; eauto.
- apply agree_exten with rs2; auto with asmgen.
- congruence.
-- exploit exec_straight_steps_2; eauto.
- intros [ofs' [PC2 CT2]].
- exploit find_label_goto_label; eauto.
- intros [tc' [rs3 [GOTO [AT' OTH]]]].
- exists (State rs3 m2'); split.
- eapply plus_right'.
- eapply exec_straight_steps_1; eauto.
- econstructor; eauto.
- eapply find_instr_tail. eauto.
- rewrite C. eexact GOTO.
- traceEq.
- econstructor; eauto.
- apply agree_exten with rs2; auto with asmgen.
- congruence.
-Qed. *)
-
(** We need to show that, in the simulation diagram, we cannot
take infinitely many Mach transitions that correspond to zero
transitions on the Asm side. Actually, all Mach transitions
@@ -967,9 +521,9 @@ Proof.
unfold transl_cond_float32. exploreInst; try discriminate.
unfold transl_cond_notfloat32. exploreInst; try discriminate.
- simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.
- all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.
+ all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
- simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.
- all: unfold transl_memory_access in EQ0; exploreInst; try discriminate.
+ all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
Qed.
Lemma transl_basic_code_nonil:
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 5486a497..5ccea246 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -30,40 +30,13 @@ Lemma make_immed32_sound:
Proof.
intros; unfold make_immed32. set (lo := Int.sign_ext 12 n).
predSpec Int.eq Int.eq_spec n lo; auto.
-(*
-- auto.
-- set (m := Int.sub n lo).
- assert (A: Int.eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto).
- assert (B: Int.eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0).
- { replace 0 with (Int.unsigned n - Int.unsigned n) by omega.
- auto using Int.eqmod_sub, Int.eqmod_refl. }
- assert (C: Int.eqmod (two_p 12) (Int.unsigned m) 0).
- { apply Int.eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto.
- apply Int.eqmod_divides with Int.modulus. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
- exists (two_p (32-12)); auto. }
- assert (D: Int.modu m (Int.repr 4096) = Int.zero).
- { apply Int.eqmod_mod_eq in C. unfold Int.modu.
- change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C.
- reflexivity.
- apply two_p_gt_ZERO; omega. }
- rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto.
- rewrite Int.shl_mul_two_p.
- change (two_p (Int.unsigned (Int.repr 12))) with 4096.
- replace (Int.mul (Int.divu m (Int.repr 4096)) (Int.repr 4096)) with m.
- unfold m. rewrite Int.sub_add_opp. rewrite Int.add_assoc. rewrite <- (Int.add_commut lo).
- rewrite Int.add_neg_zero. rewrite Int.add_zero. auto.
- rewrite (Int.modu_divu_Euclid m (Int.repr 4096)) at 1 by (vm_compute; congruence).
- rewrite D. apply Int.add_zero.
-*)
Qed.
Lemma make_immed64_sound:
forall n,
match make_immed64 n with
| Imm64_single imm => n = imm
-(*| Imm64_pair hi lo => n = Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo
- | Imm64_large imm => n = imm
-*)end.
+ end.
Proof.
intros; unfold make_immed64. set (lo := Int64.sign_ext 12 n).
predSpec Int64.eq Int64.eq_spec n lo.
@@ -76,7 +49,6 @@ Proof.
Qed.
-
(** Properties of registers *)
Lemma ireg_of_not_RTMP:
@@ -1763,7 +1735,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 +1749,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. 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 +1769,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. rewrite B, C, STORE.
eauto.
discriminate.
{ intro. inv H. contradiction. }
auto.
-(* intros; Simpl. rewrite C; auto. *)
Qed.
Lemma loadind_correct:
@@ -1821,7 +1792,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 +1814,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.
@@ -1942,10 +1913,49 @@ Proof.
inv TR. inv EV. apply indexed_memory_access_correct; eauto with asmgen.
Qed.
+Lemma transl_memory_access2_correct:
+ forall mk_instr addr args k c (rs: regset) m v,
+ transl_memory_access2 mk_instr addr args k = OK c ->
+ eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some v ->
+ exists base ro mro mr1 rs',
+ args = mr1 :: mro :: nil
+ /\ ireg_of mro = OK ro
+ /\ exec_straight_opt (basics_to_code c) rs m (mk_instr base ro ::g (basics_to_code k)) rs' m
+ /\ Val.addl rs'#base rs'#ro = v
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+ intros until v; intros TR EV.
+ unfold transl_memory_access2 in TR; destruct addr; ArgsInv.
+ inv EV. repeat eexists. eassumption. econstructor; eauto.
+Qed.
+
+Lemma transl_load_access2_correct:
+ forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c rd (rs: regset) m v mro mr1 ro v',
+ args = mr1 :: mro :: nil ->
+ ireg_of mro = OK ro ->
+ (forall base rs,
+ exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro) ->
+ transl_memory_access2 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' ->
+ exists rs',
+ exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+ /\ rs'#rd = v'
+ /\ forall r, r <> PC -> r <> RTMP -> r <> rd -> rs'#r = rs#r.
+Proof.
+ intros until v'; intros ARGS IREGE INSTR TR EV LOAD.
+ exploit transl_memory_access2_correct; eauto.
+ intros (base & ro2 & mro2 & mr2 & rs' & ARGSS & IREGEQ & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mr2 mro2. clear ARGS.
+ econstructor; split.
+ eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+ rewrite INSTR. unfold exec_load_reg. rewrite B, LOAD. reflexivity. Simpl.
+ split; intros; Simpl. auto.
+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 +1969,101 @@ 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. rewrite PtrEq, B, LOAD. reflexivity. Simpl.
split; intros; Simpl. auto.
Qed.
+Lemma transl_load_memory_access_ok:
+ forall addr chunk args dst k c rs a v m,
+ addr <> Aindexed2 ->
+ transl_load chunk addr args dst k = OK c ->
+ eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+ Mem.loadv chunk m a = Some v ->
+ exists mk_instr rd,
+ 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_offset ge chunk rs m rd base ofs.
+Proof.
+ intros until m. intros ADDR TR ? ?.
+ unfold transl_load in TR. destruct addr; try contradiction.
+ - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
+ - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+ [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity
+ | eauto ].
+ - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
+ [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity
+ | eauto ].
+Qed.
+
+Lemma transl_load_memory_access2_ok:
+ forall addr chunk args dst k c rs a v m,
+ addr = Aindexed2 ->
+ transl_load chunk addr args dst k = OK c ->
+ eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+ Mem.loadv chunk m a = Some v ->
+ exists mk_instr mr0 mro rd ro,
+ args = mr0 :: mro :: nil
+ /\ preg_of dst = IR rd
+ /\ preg_of mro = IR ro
+ /\ transl_memory_access2 mk_instr addr args k = OK c
+ /\ forall base rs,
+ exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro.
+Proof.
+ intros until m. intros ? TR ? ?.
+ unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
+ unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+ [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
+ | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; reflexivity
+ | eauto].
+Qed.
+
+Lemma transl_load_correct:
+ forall chunk addr args dst k c (rs: regset) m a v,
+ transl_load chunk addr args dst k = OK c ->
+ eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
+ Mem.loadv chunk m a = Some v ->
+ exists rs',
+ exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
+ /\ rs'#(preg_of dst) = v
+ /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
+Proof.
+ intros until v; intros TR EV LOAD. destruct addr.
+ 2-4: exploit transl_load_memory_access_ok; eauto; try discriminate;
+ intros A; destruct A as (mk_instr & rd & rdEq & B & C); rewrite rdEq;
+ eapply transl_load_access_correct; eauto with asmgen.
+ - exploit transl_load_memory_access2_ok; eauto. intros (mk_instr & mr0 & mro & rd & ro & argsEq & rdEq & roEq & B & C).
+ rewrite rdEq. eapply transl_load_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity.
+Qed.
+
+Lemma transl_store_access2_correct:
+ forall chunk (mk_instr: ireg -> ireg -> basic) addr args k c r1 (rs: regset) m v mr1 mro ro m',
+ args = mr1 :: mro :: nil ->
+ ireg_of mro = OK ro ->
+ (forall base rs,
+ exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk rs m r1 base ro) ->
+ transl_memory_access2 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' ->
+ r1 <> RTMP ->
+ exists rs',
+ exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+ /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+ intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31.
+ exploit transl_memory_access2_correct; eauto.
+ intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
+ econstructor; split.
+ eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+ rewrite INSTR. unfold exec_store_reg. rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+ intro. inv H. contradiction.
+ 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,30 +2077,98 @@ 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. rewrite PtrEq, B. rewrite C; try discriminate. rewrite STORE. auto.
intro. inv H. contradiction.
auto.
Qed.
-Lemma transl_load_correct:
- forall chunk addr args dst k c (rs: regset) m a v,
- transl_load chunk addr args dst k = OK c ->
- eval_addressing ge rs#SP addr (map rs (map preg_of args)) = Some a ->
- Mem.loadv chunk m a = Some v ->
- exists rs',
- exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m
- /\ rs'#(preg_of dst) = v
- /\ forall r, r <> PC -> r <> RTMP -> r <> preg_of dst -> rs'#r = rs#r.
+
+Remark exec_store_offset_8_sign rs m x base ofs:
+ exec_store_offset ge Mint8unsigned rs m x base ofs = exec_store_offset ge Mint8signed rs m x base ofs.
Proof.
- intros until v; intros TR EV LOAD.
- assert (A: exists mk_instr rd,
- 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).
- { 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.
+ unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+ destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_offset_16_sign rs m x base ofs:
+ exec_store_offset ge Mint16unsigned rs m x base ofs = exec_store_offset ge Mint16signed rs m x base ofs.
+Proof.
+ unfold exec_store_offset. destruct (eval_offset _ _); auto. unfold Mem.storev.
+ destruct (Val.offset_ptr _ _); auto. erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Lemma transl_store_memory_access_ok:
+ forall addr chunk args src k c rs a m m',
+ addr <> Aindexed2 ->
+ transl_store chunk addr args src k = OK c ->
+ eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+ Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+ exists mk_instr chunk' rr,
+ 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_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).
+Proof.
+ intros until m'. intros ? TR ? ?.
+ unfold transl_store in TR. destruct addr; try contradiction.
+ - monadInv TR. destruct chunk. all:
+ ArgsInv; eexists; eexists; eexists; split; try split; [
+ repeat (destruct args; try discriminate); eassumption
+ | split; eauto; intros; simpl; try reflexivity].
+ eapply exec_store_offset_8_sign.
+ eapply exec_store_offset_16_sign.
+ - monadInv TR. destruct chunk. all:
+ ArgsInv; eexists; eexists; eexists; split; try split;
+ [ repeat (destruct args; try discriminate); instantiate (1 := PStoreRRO _ x); simpl; eassumption
+ | split; eauto; intros; simpl; try reflexivity].
+ eapply exec_store_offset_8_sign.
+ eapply exec_store_offset_16_sign.
+ - monadInv TR. destruct chunk. all:
+ ArgsInv; eexists; eexists; eexists; split; try split;
+ [ repeat (destruct args; try discriminate); instantiate (1 := PStoreRRO _ x); simpl; eassumption
+ | split; eauto; intros; simpl; try reflexivity].
+ eapply exec_store_offset_8_sign.
+ eapply exec_store_offset_16_sign.
+Qed.
+
+Remark exec_store_reg_8_sign rs m x base ofs:
+ exec_store_reg Mint8unsigned rs m x base ofs = exec_store_reg Mint8signed rs m x base ofs.
+Proof.
+ unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+ erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_reg_16_sign rs m x base ofs:
+ exec_store_reg Mint16unsigned rs m x base ofs = exec_store_reg Mint16signed rs m x base ofs.
+Proof.
+ unfold exec_store_reg. unfold Mem.storev. destruct (Val.addl _ _); auto.
+ erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
+Lemma transl_store_memory_access2_ok:
+ forall addr chunk args src k c rs a m m',
+ addr = Aindexed2 ->
+ transl_store chunk addr args src k = OK c ->
+ eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
+ Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+ exists mk_instr chunk' rr mr0 mro ro,
+ args = mr0 :: mro :: nil
+ /\ preg_of mro = IR ro
+ /\ preg_of src = IR rr
+ /\ transl_memory_access2 mk_instr addr args k = OK c
+ /\ (forall base rs,
+ exec_basic_instr ge (mk_instr base ro) rs m = exec_store_reg chunk' rs m rr base ro)
+ /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+ intros until m'. intros ? TR ? ?.
+ unfold transl_store in TR. subst addr. monadInv TR. destruct chunk. all:
+ unfold transl_memory_access2 in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+ [ ArgsInv; reflexivity
+ | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRR _ x)); simpl; reflexivity
+ | eauto ].
+ - simpl. intros. eapply exec_store_reg_8_sign.
+ - simpl. intros. eapply exec_store_reg_16_sign.
Qed.
Lemma transl_store_correct:
@@ -2015,22 +2180,15 @@ Lemma transl_store_correct:
exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
/\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
Proof.
- intros until m'; intros TR EV STORE.
- assert (A: exists mk_instr chunk' rr,
- 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)
- /\ 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]]]).
- destruct a; auto. apply Mem.store_signed_unsigned_8.
- destruct a; auto. apply Mem.store_signed_unsigned_16.
- }
- destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D).
- rewrite D in STORE; clear D.
- eapply transl_store_access_correct; eauto with asmgen. congruence.
- destruct rr; try discriminate. destruct src; try discriminate.
+ intros until m'; intros TR EV STORE. destruct addr.
+ 2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A;
+ destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+ rewrite D in STORE; clear D;
+ eapply transl_store_access_correct; eauto with asmgen; try congruence;
+ destruct rr; try discriminate; destruct src; try discriminate.
+ - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+ eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+ destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
Qed.
Lemma make_epilogue_correct:
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 ac73853d..c15a33af 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -69,28 +69,36 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
(** * load/store *)
(* TODO: factoriser ? *)
-Definition parexec_load (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
- (d: ireg) (a: ireg) (ofs: offset) :=
+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 => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with
+ | None => Stuck
+ | Some v => Next (rsw#d <- v) mw
+ end
| _ => Stuck
end.
-Definition parexec_store (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
- (s: ireg) (a: ireg) (ofs: offset) :=
+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
+ | 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 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 => match Mem.storev chunk mr (Val.offset_ptr (rsr a) ptr) (rsr s) with
+ | None => Stuck
+ | Some m' => Next rsw m'
+ end
| _ => Stuck
end.
+Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) :=
+ match Mem.storev chunk mr (Val.addl (rsr a) (rsr ro)) (rsr s) with
+ | None => Stuck
+ | Some m' => Next rsw m'
+ end.
+
(* rem: parexec_store = exec_store *)
(** * basic instructions *)
@@ -100,9 +108,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/Op.v b/mppa_k1c/Op.v
index c4338857..d533a504 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -187,6 +187,7 @@ Inductive operation : Type :=
addressing. *)
Inductive addressing: Type :=
+ | Aindexed2: addressing (**r Address is [r1 + r2] *)
| Aindexed: ptrofs -> addressing (**r Address is [r1 + offset] *)
| Aglobal: ident -> ptrofs -> addressing (**r Address is global plus offset *)
| Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *)
@@ -385,6 +386,7 @@ Definition eval_addressing
(F V: Type) (genv: Genv.t F V) (sp: val)
(addr: addressing) (vl: list val) : option val :=
match addr, vl with
+ | Aindexed2, v1 :: v2 :: nil => Some (Val.addl v1 v2)
| Aindexed n, v1 :: nil => Some (Val.offset_ptr v1 n)
| Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs)
| Ainstack n, nil => Some (Val.offset_ptr sp n)
@@ -569,6 +571,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
Definition type_of_addressing (addr: addressing) : list typ :=
match addr with
+ | Aindexed2 => Tptr :: Tptr :: nil
| Aindexed _ => Tptr :: nil
| Aglobal _ _ => nil
| Ainstack _ => nil
@@ -914,6 +917,7 @@ Qed.
Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
match addr with
+ | Aindexed2 => None
| Aindexed n => Some(Aindexed (Ptrofs.add n (Ptrofs.repr delta)))
| Aglobal id n => Some(Aglobal id (Ptrofs.add n (Ptrofs.repr delta)))
| Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta)))
@@ -1337,9 +1341,10 @@ Lemma eval_addressing_inj:
exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
Proof.
intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
- apply Val.offset_ptr_inject; auto.
- apply H; simpl; auto.
- apply Val.offset_ptr_inject; auto.
+ - apply Val.addl_inject; auto.
+ - apply Val.offset_ptr_inject; auto.
+ - apply H; simpl; auto.
+ - apply Val.offset_ptr_inject; auto.
Qed.
End EVAL_COMPAT.
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 4433bb1d..e0890a09 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -95,23 +95,46 @@ 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 *. 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 *. 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 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 *. 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 *. rewrite Pregmap.gso; try discriminate.
destruct (Mem.storev _ _ _).
- inv H. apply next_eq; auto.
- discriminate.
@@ -129,8 +152,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 +586,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 +604,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/PrintOp.ml b/mppa_k1c/PrintOp.ml
index 9ec474b3..5ac00404 100644
--- a/mppa_k1c/PrintOp.ml
+++ b/mppa_k1c/PrintOp.ml
@@ -160,6 +160,7 @@ let print_operation reg pp = function
let print_addressing reg pp = function
| Aindexed n, [r1] -> fprintf pp "%a + %Ld" reg r1 (camlint64_of_ptrofs n)
+ | Aindexed2, [r1;r2] -> fprintf pp "%a + %a" reg r1 reg r2
| Aglobal(id, ofs), [] ->
fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs)
| Ainstack ofs, [] -> fprintf pp "stack(%Ld)" (camlint64_of_ptrofs ofs)
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 0c3618d7..31112dca 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -364,10 +364,9 @@ Definition floatoflongu (e: expr) :=
if Archi.splitlong then SplitLong.floatoflongu e else
Eop Ofloatoflongu (e:::Enil).
-(* SplitLong.longofsingle splits the operation into (longoffloat (floatofsingle e)) *)
-Definition longofsingle (e: expr) := SplitLong.longofsingle e.
+Definition longofsingle (e: expr) := longoffloat (floatofsingle e).
-Definition longuofsingle (e: expr) := SplitLong.longuofsingle e.
+Definition longuofsingle (e: expr) := longuoffloat (floatofsingle e).
Definition singleoflong (e: expr) := SplitLong.singleoflong e.
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 79187338..51b989d6 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -600,16 +600,22 @@ Qed.
Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle.
Proof.
- unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
- eapply SplitLongproof.eval_longofsingle; eauto.
-(* TrivialExists. *)
+ unfold longofsingle; red; intros.
+ destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
+ exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+ apply Float32.to_long_double in EQ.
+ eapply eval_longoffloat; eauto. simpl.
+ change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
Qed.
Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle.
Proof.
unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *)
- eapply SplitLongproof.eval_longuofsingle; eauto.
-(* TrivialExists. *)
+ destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
+ exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+ apply Float32.to_longu_double in EQ.
+ eapply eval_longuoffloat; eauto. simpl.
+ change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
Qed.
Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index f6605c11..d82fe238 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -481,6 +481,7 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
| Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)
| Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
| Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
+ | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil)
| _ => (Aindexed Ptrofs.zero, e:::Enil)
end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 89af39ee..d426e4f1 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -991,6 +991,7 @@ Proof.
- exists (v1 :: nil); split. eauto with evalexpr. simpl.
destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H.
simpl. auto.
+ - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
- exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
Qed.
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/ValueAOp.v b/mppa_k1c/ValueAOp.v
index fb1977ea..a54dbd8f 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -36,6 +36,7 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
Definition eval_static_addressing (addr: addressing) (vl: list aval): aval :=
match addr, vl with
| Aindexed n, v1::nil => offset_ptr v1 n
+ | Aindexed2, v1::v2::nil => addl v1 v2
| Aglobal s ofs, nil => Ptr (Gl s ofs)
| Ainstack ofs, nil => Ptr (Stk ofs)
| _, _ => Vbot
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 69234938..d0e05389 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; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
+ 1-10: try (unfold exec_load_reg 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; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
+ 1-10: try (unfold exec_store_reg 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 03:47:44 +0000