Refactorisation des load et des store

3 files changed, 40 insertions, 62 deletions

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: