From cbe3f094b32077ce8d8569556d4ebc6341b09dd9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 May 2019 21:54:11 +0200 Subject: it compiles --- mppa_k1c/Asm.v | 9 ++++ mppa_k1c/Asmblock.v | 2 + mppa_k1c/Asmblockdeps.v | 20 ++++++++ mppa_k1c/Asmblockgen.v | 36 +++++++------ mppa_k1c/Asmblockgenproof.v | 2 +- mppa_k1c/Asmblockgenproof1.v | 99 ++++++++++++++++++++++++++++++++---- mppa_k1c/Asmvliw.v | 14 ++--- mppa_k1c/PostpassSchedulingOracle.ml | 2 +- mppa_k1c/PostpassSchedulingproof.v | 12 +++++ mppa_k1c/lib/Asmblockgenproof0.v | 1 + 10 files changed, 164 insertions(+), 33 deletions(-) diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 0e217d36..d73d00c7 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -475,6 +475,15 @@ Definition basic_to_instruction (b: basic) := | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro) | PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro) + | PStoreRRRXS Asmvliw.Psb rd ra ro => Psb rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Psh rd ra ro => Psh rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Psw rd ra ro => Psw rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Psw_a rd ra ro => Psw_a rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Psd rd ra ro => Psd rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Psd_a rd ra ro => Psd_a rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro) + | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro) + end. Section RELSEM. diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 3aec4e11..1988813f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -274,6 +274,8 @@ Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: i Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro. +Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_regxs chunk rs rs m m s a ro. + (** * basic instructions *) Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m. diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 32a5fa04..f6573838 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -83,6 +83,7 @@ Coercion OLoadRRO: load_name >-> Funclass. Inductive store_op := | OStoreRRO (n: store_name) (ofs: offset) | OStoreRRR (n: store_name) + | OStoreRRRXS (n: store_name) . Coercion OStoreRRO: store_name >-> Funclass. @@ -177,10 +178,17 @@ Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) := | Some m' => Some (Memstate m') end. +Definition exec_store_deps_regxs (chunk: memory_chunk) (m: mem) (vs va vo: val) := + match Mem.storev chunk m (Val.addl va (Val.shll vo (scale_of_chunk chunk))) 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_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 + | OStoreRRRXS n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_regxs (store_chunk n) m vs va vo | _, _ => None end. @@ -385,6 +393,8 @@ Definition store_op_eq (o1 o2: store_op): ?? bool := match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end | OStoreRRR n1 => match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end + | OStoreRRRXS n1 => + match o2 with OStoreRRRXS n2 => phys_eq n1 n2 | _ => RET false end end. Lemma store_op_eq_correct o1 o2: @@ -393,6 +403,7 @@ Proof. destruct o1, o2; wlp_simplify; try discriminate. - congruence. - congruence. + - congruence. Qed. Hint Resolve store_op_eq_correct: wlp. Opaque store_op_eq_correct. @@ -626,6 +637,7 @@ Definition trans_basic (b: basic) : inst := | PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] + | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS 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)); @@ -864,6 +876,13 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + (* Store Reg XS *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_regxs; simpl; unfold exec_store_deps_regxs; 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. @@ -1446,6 +1465,7 @@ Definition string_of_store (op: store_op) : pstring := match op with | OStoreRRO n _ => string_of_store_name n | OStoreRRR n => string_of_store_name n + | OStoreRRRXS n => string_of_store_name n end. Definition string_of_control (op: control_op) : pstring := diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a74aa9f6..ea99c098 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -807,31 +807,31 @@ end. Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) := match ty, preg_of dst with - | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Pld rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfld rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Plw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.loadind") end. Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) := match ty, preg_of src with - | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs ::i k) - | Tlong, IR rd => OK (indexed_memory_access (Psd rd) base ofs ::i k) - | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs ::i k) - | Tfloat, IR rd => OK (indexed_memory_access (Pfsd rd) base ofs ::i k) - | Tany32, IR rd => OK (indexed_memory_access (Psw_a rd) base ofs ::i k) - | Tany64, IR rd => OK (indexed_memory_access (Psd_a rd) base ofs ::i k) + | Tint, IR rd => OK (indexed_memory_access (PStoreRRO Psw rd) base ofs ::i k) + | Tlong, IR rd => OK (indexed_memory_access (PStoreRRO Psd rd) base ofs ::i k) + | Tsingle, IR rd => OK (indexed_memory_access (PStoreRRO Pfss rd) base ofs ::i k) + | Tfloat, IR rd => OK (indexed_memory_access (PStoreRRO Pfsd rd) base ofs ::i k) + | Tany32, IR rd => OK (indexed_memory_access (PStoreRRO Psw_a rd) base ofs ::i k) + | Tany64, IR rd => OK (indexed_memory_access (PStoreRRO Psd_a rd) base ofs ::i k) | _, _ => Error (msg "Asmblockgen.storeind") end. Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) := - indexed_memory_access (Pld dst) base ofs. + indexed_memory_access (PLoadRRO Pld dst) base ofs. Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := - indexed_memory_access (Psd src) base ofs. + indexed_memory_access (PStoreRRO Psd src) base ofs. (** Translation of memory accesses: loads, and stores. *) @@ -901,7 +901,7 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing) Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := do r <- ireg_of dst; - transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) scale args k. + transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k. Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: bcode) : res bcode := @@ -933,10 +933,16 @@ Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing) do r <- ireg_of src; transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k. +Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z) + (args: list mreg) (src: mreg) (k: bcode) : res bcode := + do r <- ireg_of src; + transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k. + Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: bcode) : res bcode := match addr with | Aindexed2 => transl_store_rrr chunk addr args src k + | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k | _ => transl_store_rro chunk addr args src k end. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index e710b5a4..0233a3dc 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -523,7 +523,7 @@ Proof. - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate. all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate. - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate. - all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate. + all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate. Qed. Lemma transl_basic_code_nonil: diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index c9d72c4d..82f3b0fc 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -2254,15 +2254,15 @@ Lemma transl_load_memory_access2XS_ok: args = mr0 :: mro :: nil /\ preg_of dst = IR rd /\ preg_of mro = IR ro - /\ transl_memory_access2XS chunk mk_instr (Aindexed2XS scale) args k = OK c + /\ transl_memory_access2XS chunk mk_instr scale 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. + exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs 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_access2XS 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; rewrite Heqb; reflexivity + | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ x)); simpl; rewrite Heqb; eauto | eauto]. Qed. @@ -2316,6 +2316,33 @@ Proof. auto. Qed. +Lemma transl_store_access2XS_correct: + forall chunk (mk_instr: ireg -> ireg -> basic) scale 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_regxs chunk rs m r1 base ro) -> + transl_memory_access2XS chunk mk_instr scale args k = OK c -> + eval_addressing ge rs#SP (Aindexed2XS scale) (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_access2XS_correct; eauto. + intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C & D). 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_regxs. unfold parexec_store_regxs. + unfold scale_of_chunk. + subst scale. + 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, @@ -2355,7 +2382,7 @@ Qed. Lemma transl_store_memory_access_ok: forall addr chunk args src k c rs a m m', - addr <> Aindexed2 -> + (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) -> 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' -> @@ -2368,7 +2395,6 @@ Lemma transl_store_memory_access_ok: Proof. intros until m'. intros ? TR ? ?. unfold transl_store in TR. destruct addr; try contradiction. - - (* Aindex2XS *) discriminate. - monadInv TR. destruct chunk. all: ArgsInv; eexists; eexists; eexists; split; try split; [ repeat (destruct args; try discriminate); eassumption @@ -2403,6 +2429,20 @@ Proof. erewrite <- Mem.store_signed_unsigned_16. reflexivity. Qed. +Remark exec_store_regxs_8_sign rs m x base ofs: + exec_store_regxs Mint8unsigned rs m x base ofs = exec_store_regxs Mint8signed rs m x base ofs. +Proof. + unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto. + erewrite <- Mem.store_signed_unsigned_8. reflexivity. +Qed. + +Remark exec_store_regxs_16_sign rs m x base ofs: + exec_store_regxs Mint16unsigned rs m x base ofs = exec_store_regxs Mint16signed rs m x base ofs. +Proof. + unfold exec_store_regxs. unfold parexec_store_regxs. 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 -> @@ -2428,6 +2468,30 @@ Proof. - simpl. intros. eapply exec_store_reg_16_sign. Qed. +Lemma transl_store_memory_access2XS_ok: + forall scale chunk args src k c rs a m m', + transl_store chunk (Aindexed2XS scale) args src k = OK c -> + eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (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_access2XS chunk' mk_instr scale args k = OK c + /\ (forall base rs, + exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs 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. monadInv TR. destruct chunk. all: + unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists; + [ ArgsInv; reflexivity + | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRRXS _ x)); simpl; rewrite Heqb; eauto + | eauto ]. + - simpl. intros. eapply exec_store_regxs_8_sign. + - simpl. intros. eapply exec_store_regxs_16_sign. +Qed. + Lemma transl_store_correct: forall chunk addr args src k c (rs: regset) m a m', transl_store chunk addr args src k = OK c -> @@ -2438,15 +2502,30 @@ Lemma transl_store_correct: /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r. Proof. intros until m'; intros TR EV STORE. destruct addr. - 1: (* AIndexed2XS *) discriminate. - 2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A; + - exploit transl_store_memory_access2XS_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C). + eapply transl_store_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence. + destruct rr; try discriminate. destruct src; simpl in srcEq; 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. + - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity). + 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_access_ok; eauto; try discriminate; try (simpl; reflexivity). + 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_access_ok; eauto; try discriminate; try (simpl; reflexivity). + 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/Asmvliw.v b/mppa_k1c/Asmvliw.v index 7a5adf5e..629d1449 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -273,9 +273,6 @@ Inductive ld_instruction : Type := | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg) . -Coercion PLoadRRO: load_name >-> Funclass. -Coercion PLoadRRR: load_name >-> Funclass. - (** Stores **) Inductive store_name : Type := | Psb (**r store byte *) @@ -291,11 +288,9 @@ Inductive store_name : Type := Inductive st_instruction : Type := | PStoreRRO (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset) | PStoreRRR (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) + | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg) . -Coercion PStoreRRO: store_name >-> Funclass. -Coercion PStoreRRR: store_name >-> Funclass. - (** Arithmetic instructions **) Inductive arith_name_r : Type := | Ploadsymbol (id: ident) (ofs: ptrofs) (**r load the address of a symbol *) @@ -1160,6 +1155,12 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem | Some m' => Next rsw m' end. +Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) := + match Mem.storev chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) (rsr s) with + | None => Stuck + | Some m' => Next rsw m' + end. + Definition load_chunk n := match n with | Plb => Mint8signed @@ -1198,6 +1199,7 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := | 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 + | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro | Pallocframe sz pos => let (mw, stk) := Mem.alloc mr 0 sz in diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index ef5e325a..e6643736 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -224,7 +224,7 @@ let load_rec i = match i with 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 + | PStoreRRR (i, rs1, rs2, rs3) | PStoreRRRXS (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 3f3cb19c..43c8acb8 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -151,6 +151,17 @@ Proof. - discriminate. Qed. +Lemma exec_store_regxs_pc_var: + forall t rs m rd ra ro rs' m' v, + exec_store_regxs t rs m rd ra ro = Next rs' m' -> + exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'. +Proof. + intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate. + destruct (Mem.storev _ _ _). + - inv H. apply next_eq; auto. + - discriminate. +Qed. + Lemma exec_basic_instr_pc_var: forall ge i rs m rs' m' v, exec_basic_instr ge i rs m = Next rs' m' -> @@ -170,6 +181,7 @@ Proof. - destruct i. + exploreInst; apply exec_store_offset_pc_var; auto. + exploreInst; apply exec_store_reg_pc_var; auto. + + exploreInst; apply exec_store_regxs_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. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index ab0d2964..0a83a903 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -949,6 +949,7 @@ Proof. 1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]). 1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]). 1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto. + 1-10: try (unfold parexec_store_regxs 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. -- cgit