diff options
-rw-r--r-- | mppa_k1c/Asm.v | 97 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 58 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 212 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 115 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof.v | 450 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 306 | ||||
-rw-r--r-- | mppa_k1c/Asmexpand.ml | 44 | ||||
-rw-r--r-- | mppa_k1c/Asmvliw.v | 42 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 11 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 4 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 63 | ||||
-rw-r--r-- | mppa_k1c/PrintOp.ml | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectLong.vp | 5 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 16 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 1 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 1 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 44 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 1 | ||||
-rw-r--r-- | mppa_k1c/lib/Asmblockgenproof0.v | 18 |
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': |