Removing from Asmblockgenproof0 architecture specific definitions

9 files changed, 153 insertions, 130 deletions

diff --git a/configure b/configure
index 9d5bfcf9..f13d1af3 100755
--- a/configure
+++ b/configure
@@ -845,7 +845,7 @@ EXECUTE=k1-cluster --syscall=libstd_scalls.so --
 CFLAGS= -D __K1C_COS__
 SIMU=k1-cluster -- 
 BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\
-    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v\\
+    Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\
     ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\
     Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\
     AbstractBasicBlocksDef.v SeqSimuTheory.v ImpSimuTest.v Parallelizability.v\\
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index cce180ac..a05d4726 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -33,6 +33,19 @@ Require Import Conventions.
 Require Import Errors.
 Require Export Asmvliw.
 
+(* Notations necessary to hook Asmvliw definitions *)
+Notation undef_caller_save_regs := Asmvliw.undef_caller_save_regs.
+Notation regset := Asmvliw.regset.
+Notation extcall_arg := Asmvliw.extcall_arg.
+Notation extcall_arg_pair := Asmvliw.extcall_arg_pair.
+Notation extcall_arguments := Asmvliw.extcall_arguments.
+Notation set_res := Asmvliw.set_res.
+Notation function := Asmvliw.function.
+Notation bblocks := Asmvliw.bblocks.
+Notation header := Asmvliw.header.
+Notation body := Asmvliw.body.
+Notation exit := Asmvliw.exit.
+Notation correct := Asmvliw.correct.
 
 (** * Auxiliary utilies on basic blocks *)
 
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 584f2339..02f9141b 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -7,7 +7,7 @@
 
 Require Import AST.
 Require Import Asmblock.
-Require Import Asmblockgenproof0.
+Require Import Asmblockgenproof0 Asmblockprops.
 Require Import Values.
 Require Import Globalenvs.
 Require Import Memory.
@@ -1429,7 +1429,7 @@ Lemma bblock_simu_reduce:
   forall p1 p2 ge fn,
   Ge = Genv ge fn ->
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
-  Asmblockgenproof0.bblock_simu ge fn p1 p2.
+  Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
   unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK.
   generalize (H2 (trans_state (State rs m))); clear H2.
@@ -1787,7 +1787,7 @@ Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool :=
 Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp.
 
 Theorem bblock_simu_test_correct verb p1 p2 :
-  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockgenproof0.bblock_simu ge fn p1 p2.
+  WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
   wlp_simplify.
 Qed.
@@ -1803,7 +1803,7 @@ Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool :=
   | None => false
   end.
 
-Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
    unfold pure_bblock_simu_test. 
    destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate.
@@ -1813,7 +1813,7 @@ Qed.
 
 Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true.
 
-Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2.
+Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2.
 Proof.
  eapply (pure_bblock_simu_test_correct true).
 Qed.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index 220ae08b..1a427112 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -16,7 +16,7 @@ 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 Asmblockgen Asmblockgenproof0 Asmblockgenproof1.
+Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops.
 Require Import Axioms.
 
 Module MB := Machblock.
diff --git a/mppa_k1c/Asmblockgenproof0.v b/mppa_k1c/Asmblockgenproof0.v
index d2450a9a..940c6563 100644
--- a/mppa_k1c/Asmblockgenproof0.v
+++ b/mppa_k1c/Asmblockgenproof0.v
@@ -22,16 +22,10 @@ Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
 Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
+Require Import Asmblockprops.
 
 Module MB:=Machblock.
-Module AB:=Asmvliw.
-
-Hint Extern 2 (_ <> _) => congruence: asmgen.
-
-Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
-  forall rs m,
-    exec_bblock ge f bb rs m <> Stuck ->
-    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.
+Module AB:=Asmblock.
 
 Lemma ireg_of_eq:
   forall r r', ireg_of r = OK r' -> preg_of r = IR r'.
@@ -51,53 +45,6 @@ Proof.
   destruct r1; destruct r2; simpl; intros; reflexivity || discriminate.
 Qed.
 
-Lemma preg_of_data:
-  forall r, data_preg (preg_of r) = true.
-Proof.
-  intros. destruct r; reflexivity.
-Qed.
-Hint Resolve preg_of_data: asmgen.
-
-Lemma data_diff:
-  forall r r',
-  data_preg r = true -> data_preg r' = false -> r <> r'.
-Proof.
-  congruence.
-Qed.
-Hint Resolve data_diff: asmgen.
-
-Lemma preg_of_not_SP:
-  forall r, preg_of r <> SP.
-Proof.
-  intros. unfold preg_of; destruct r; simpl; congruence.
-Qed.
-
-Lemma preg_of_not_PC:
-  forall r, preg_of r <> PC.
-Proof.
-  intros. apply data_diff; auto with asmgen.
-Qed.
-
-Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
-
-Lemma nextblock_pc:
-  forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).
-Proof.
-  intros. apply Pregmap.gss.
-Qed.
-
-Lemma nextblock_inv:
-  forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.
-Proof.
-  intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
-Qed.
-
-Lemma nextblock_inv1:
-  forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
-Proof.
-  intros. apply nextblock_inv. red; intro; subst; discriminate.
-Qed.
-
 Lemma undef_regs_other:
   forall r rl rs,
   (forall r', In r' rl -> r <> r') ->
@@ -294,9 +241,9 @@ Qed.
 Lemma agree_undef_caller_save_regs:
   forall ms sp rs,
   agree ms sp rs ->
-  agree (Mach.undef_caller_save_regs ms) sp (Asmvliw.undef_caller_save_regs rs).
+  agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs).
 Proof.
-  intros. destruct H. unfold Mach.undef_caller_save_regs, Asmvliw.undef_caller_save_regs; split.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split.
 - unfold proj_sumbool; rewrite dec_eq_true. auto.
 - auto.
 - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
@@ -752,69 +699,6 @@ Proof.
   intros. destruct H. auto.
 Qed.
 
-Ltac Simplif :=
-  ((rewrite nextblock_inv by eauto with asmgen)
-  || (rewrite nextblock_inv1 by eauto with asmgen)
-  || (rewrite Pregmap.gss)
-  || (rewrite nextblock_pc)
-  || (rewrite Pregmap.gso by eauto with asmgen)
-  ); auto with asmgen.
-
-Ltac Simpl := repeat Simplif.
-
-Theorem exec_basic_instr_pc:
-  forall ge b rs1 m1 rs2 m2,
-  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
-  rs2 PC = rs1 PC.
-Proof.
-  intros. destruct b; try destruct i; try destruct i.
-  all: try (inv H; Simpl).
-  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  { (* PLoadQRRO *)
-    unfold  parexec_load_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  { (* PLoadORRO *)
-    unfold  parexec_load_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
-  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  
-  { (* PStoreQRRO *)
-    unfold  parexec_store_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  { (* PStoreORRO *)
-    unfold  parexec_store_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  - 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_body_pc:
   forall ge l rs1 m1 rs2 m2,
   exec_body ge l rs1 m1 = Next rs2 m2 ->
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index c0a05ab3..ecb4629b 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -20,7 +20,7 @@
 Require Import Coqlib Errors Maps.
 Require Import AST Integers Floats Values Memory Globalenvs.
 Require Import Op Locations Machblock Conventions.
-Require Import Asmblock Asmblockgen Asmblockgenproof0.
+Require Import Asmblock Asmblockgen Asmblockgenproof0 Asmblockprops.
 Require Import Chunks.
 
 (** Decomposition of integer constants. *)
diff --git a/mppa_k1c/Asmblockprops.v b/mppa_k1c/Asmblockprops.v
new file mode 100644
index 00000000..7f6e33db
--- /dev/null
+++ b/mppa_k1c/Asmblockprops.v
@@ -0,0 +1,126 @@
+(** Common definition and proofs on Asmblock required by various modules *)
+
+Require Import Coqlib.
+Require Import Integers.
+Require Import Memory.
+Require Import Globalenvs.
+Require Import Values.
+Require Import Asmblock.
+
+Definition bblock_simu (ge: Genv.t fundef unit) (f: function) (bb bb': bblock) :=
+  forall rs m,
+    exec_bblock ge f bb rs m <> Stuck ->
+    exec_bblock ge f bb rs m = exec_bblock ge f bb' rs m.
+    
+Hint Extern 2 (_ <> _) => congruence: asmgen.
+
+Lemma preg_of_data:
+  forall r, data_preg (preg_of r) = true.
+Proof.
+  intros. destruct r; reflexivity.
+Qed.
+Hint Resolve preg_of_data: asmgen.
+
+Lemma data_diff:
+  forall r r',
+  data_preg r = true -> data_preg r' = false -> r <> r'.
+Proof.
+  congruence.
+Qed.
+Hint Resolve data_diff: asmgen.
+
+Lemma preg_of_not_PC:
+  forall r, preg_of r <> PC.
+Proof.
+  intros. apply data_diff; auto with asmgen.
+Qed.
+
+Lemma preg_of_not_SP:
+  forall r, preg_of r <> SP.
+Proof.
+  intros. unfold preg_of; destruct r; simpl; congruence.
+Qed.
+
+Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen.
+
+
+Lemma nextblock_pc:
+  forall b rs, (nextblock b rs)#PC = Val.offset_ptr rs#PC (Ptrofs.repr (size b)).
+Proof.
+  intros. apply Pregmap.gss.
+Qed.
+
+Lemma nextblock_inv:
+  forall b r rs, r <> PC -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. unfold nextblock. apply Pregmap.gso. red; intro; subst. auto.
+Qed.
+
+Lemma nextblock_inv1:
+  forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
+Proof.
+  intros. apply nextblock_inv. red; intro; subst; discriminate.
+Qed.
+
+Ltac Simplif :=
+  ((rewrite nextblock_inv by eauto with asmgen)
+  || (rewrite nextblock_inv1 by eauto with asmgen)
+  || (rewrite Pregmap.gss)
+  || (rewrite nextblock_pc)
+  || (rewrite Pregmap.gso by eauto with asmgen)
+  ); auto with asmgen.
+
+Ltac Simpl := repeat Simplif.
+
+Theorem exec_basic_instr_pc:
+  forall ge b rs1 m1 rs2 m2,
+  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
+  rs2 PC = rs1 PC.
+Proof.
+  intros. destruct b; try destruct i; try destruct i.
+  all: try (inv H; Simpl).
+  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
+
+  { (* PLoadQRRO *)
+    unfold  parexec_load_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  { (* PLoadORRO *)
+    unfold  parexec_load_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl. }
+  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
+  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
+  
+  { (* PStoreQRRO *)
+    unfold  parexec_store_q_offset in H1.
+    destruct (gpreg_q_expand _) as [r0 r1] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  { (* PStoreORRO *)
+    unfold  parexec_store_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity. }
+  - 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.
\ No newline at end of file
diff --git a/mppa_k1c/PostpassScheduling.v b/mppa_k1c/PostpassScheduling.v
index 8b6de1e2..31180cea 100644
--- a/mppa_k1c/PostpassScheduling.v
+++ b/mppa_k1c/PostpassScheduling.v
@@ -12,7 +12,7 @@
 
 Require Import Coqlib Errors AST Integers.
 Require Import Asmblock Axioms Memory Globalenvs.
-Require Import Asmblockdeps Asmblockgenproof0.
+Require Import Asmblockdeps Asmblockgenproof0 Asmblockprops.
 Require Peephole.
 
 Local Open Scope error_monad_scope.
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index cdf8829f..f1166a38 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -14,7 +14,7 @@ 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 Asmblockgenproof0.
+Require Import Asmblockgenproof0 Asmblockprops.
 Require Import PostpassScheduling.
 Require Import Asmblockgenproof.
 Require Import Axioms.