From a57a83d632afb029c1e12c9851a8631ace7ded01 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 8 Mar 2019 11:52:10 +0100 Subject: Refactorisation des load et des store --- mppa_k1c/Asmblock.v | 64 +++++++++++++++++++------------------- mppa_k1c/Asmblockdeps.v | 32 +++---------------- mppa_k1c/PostpassSchedulingproof.v | 6 ++-- 3 files changed, 40 insertions(+), 62 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index f2ad60e6..9938b386 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -1022,11 +1022,7 @@ Definition compare_float (t: ftest) (v1 v2: val): val := | FTult => Val.notbool (Val.cmpf Cge v1 v2) end. -(** Execution of arith instructions - -TODO: subsplitting by instruction type ? Could be useful for expressing auxiliary lemma... - -*) +(** Execution of arith instructions *) Variable ge: genv. @@ -1197,37 +1193,41 @@ Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) | _ => Stuck end. +Definition load_chunk n := + match n with + | Plb => Mint8signed + | Plbu => Mint8unsigned + | Plh => Mint16signed + | Plhu => Mint16unsigned + | Plw => Mint32 + | Plw_a => Many32 + | Pld => Mint64 + | Pld_a => Many64 + | Pfls => Mfloat32 + | Pfld => Mfloat64 + end. + +Definition store_chunk n := + match n with + | Psb => Mint8unsigned + | Psh => Mint16unsigned + | Psw => Mint32 + | Psw_a => Many32 + | Psd => Mint64 + | Psd_a => Many64 + | Pfss => Mfloat32 + | Pfsd => Mfloat64 + end. + (** * basic instructions *) Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome regset := - match bi with - | PArith ai => Next (exec_arith_instr ai rs) m - - | PLoadRRO n d a ofs => - match n with - | Plb => exec_load Mint8signed rs m d a ofs - | Plbu => exec_load Mint8unsigned rs m d a ofs - | Plh => exec_load Mint16signed rs m d a ofs - | Plhu => exec_load Mint16unsigned rs m d a ofs - | Plw => exec_load Mint32 rs m d a ofs - | Plw_a => exec_load Many32 rs m d a ofs - | Pld => exec_load Mint64 rs m d a ofs - | Pld_a => exec_load Many64 rs m d a ofs - | Pfls => exec_load Mfloat32 rs m d a ofs - | Pfld => exec_load Mfloat64 rs m d a ofs - end + match bi with + | PArith ai => Next (exec_arith_instr ai rs) m - | PStoreRRO n s a ofs => - match n with - | Psb => exec_store Mint8unsigned rs m s a ofs - | Psh => exec_store Mint16unsigned rs m s a ofs - | Psw => exec_store Mint32 rs m s a ofs - | Psw_a => exec_store Many32 rs m s a ofs - | Psd => exec_store Mint64 rs m s a ofs - | Psd_a => exec_store Many64 rs m s a ofs - | Pfss => exec_store Mfloat32 rs m s a ofs - | Pfsd => exec_store Mfloat64 rs m s a ofs - end + | PLoadRRO n d a ofs => exec_load (load_chunk n) rs m d a ofs + + | PStoreRRO n s a ofs => exec_store (store_chunk n) rs m s a ofs | 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 b7e7b87c..14355d32 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -129,19 +129,7 @@ Definition exec_load_deps (chunk: memory_chunk) (m: mem) Definition load_eval (lo: load_op) (l: list value) := match lo, l with - | OLoadRRO n ofs, [Val v; Memstate m] => - match n with - | Plb => exec_load_deps Mint8signed m v ofs - | Plbu => exec_load_deps Mint8unsigned m v ofs - | Plh => exec_load_deps Mint16signed m v ofs - | Plhu => exec_load_deps Mint16unsigned m v ofs - | Plw => exec_load_deps Mint32 m v ofs - | Plw_a => exec_load_deps Many32 m v ofs - | Pld => exec_load_deps Mint64 m v ofs - | Pld_a => exec_load_deps Many64 m v ofs - | Pfls => exec_load_deps Mfloat32 m v ofs - | Pfld => exec_load_deps Mfloat64 m v ofs - end + | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps (load_chunk n) m v ofs | _, _ => None end. @@ -159,17 +147,7 @@ Definition exec_store_deps (chunk: memory_chunk) (m: mem) Definition store_eval (so: store_op) (l: list value) := match so, l with - | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => - match n with - | Psb => exec_store_deps Mint8unsigned m vs va ofs - | Psh => exec_store_deps Mint16unsigned m vs va ofs - | Psw => exec_store_deps Mint32 m vs va ofs - | Psw_a => exec_store_deps Many32 m vs va ofs - | Psd => exec_store_deps Mint64 m vs va ofs - | Psd_a => exec_store_deps Many64 m vs va ofs - | Pfss => exec_store_deps Mfloat32 m vs va ofs - | Pfsd => exec_store_deps Mfloat64 m vs va ofs - end + | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps (store_chunk n) m vs va ofs | _, _ => None end. @@ -748,8 +726,8 @@ Proof. (* Arith *) - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto. (* Load *) - - simpl in H. destruct i; destruct i. - all: unfold exec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; + - 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| @@ -759,7 +737,7 @@ Proof. subst; Simpl| Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]]. (* Store *) - - simpl in H. destruct i; destruct i. + - 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; diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 8ad30e81..2de49faa 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -575,9 +575,9 @@ Lemma transf_exec_basic_instr: Proof. intros. pose symbol_address_preserved. unfold exec_basic_instr. exploreInst; simpl; auto; try congruence. - 1: unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. - 1-10: apply transf_exec_load. - all: apply transf_exec_store. + - unfold exec_arith_instr; unfold arith_eval_r; exploreInst; simpl; auto; try congruence. + - apply transf_exec_load. + - apply transf_exec_store. Qed. Lemma transf_exec_body: -- cgit