Postpass scheduling OK

- Modifying Asmblockdeps to adapt to Pfmovimm new specification
- Changing the Asmgenproof to adapt PArith in consequence
- Modifying the oracle to specify correct wlocs
- Cleaning everywhere

1 files changed, 29 insertions, 164 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index bd460209..0427d1c4 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -13,13 +13,12 @@
 (*                                                             *)
 (* *************************************************************)
 
-(** * Translation from [Asmvliw] to [AbstractBB] *)
+(** * Translation from [Asmblock] to [AbstractBB] *)
 
-(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L].
-    [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one.
-    We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW].
-    We also prove a bisimulation between the sequential semantics of [L] and [Asmblock].
-    Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L].
+(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmblock] into [L].
+    [AbstractBB] will then define a sequential semantics for [L].
+    We prove a bisimulation between the sequential semantics of [L] and [Asmblock].
+    Then, the checker on [Asmblock] is deduced from those of [L].
  *)
 
 Require Import AST.
@@ -114,7 +113,6 @@ Definition value := value_wrap.
 Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }.
 
 Inductive control_op :=
-  (*| Oj_l (l: label)*)
   | Ob (l: label)
   | Obc (c: testcond) (l: label)
   | Obl (id: ident)
@@ -327,6 +325,10 @@ Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) :=
       end
   end.
 
+(* The is argument is used to identify the source inst and avoid rewriting some code
+  0 -> Ocset
+  1 -> Ocsel
+  2 -> Obc *)
 Definition cond_eval_is (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is: Z) :=
   let res := flags_testcond_value c vCN vCZ vCC vCV in
   match is, res with
@@ -355,7 +357,6 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) :=
   end.
 
 Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is: Z) :=
-
   match c, l with
   | TCeq, [Val vCZ] => cond_eval_is TCeq v1 v2 Vundef vCZ Vundef Vundef is
   | TCne, [Val vCZ] => cond_eval_is TCne v1 v2 Vundef vCZ Vundef Vundef is
@@ -646,65 +647,6 @@ Proof.
 Qed.
 Hint Resolve is_eq_correct: wlp.
 
-(*Definition testcond_eq (c1 c2: testcond) : ?? bool :=*)
-  (*RET (match c1 with*)
-       (*| TCeq => match c2 with*)
-                 (*| TCeq => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCne => match c2 with*)
-                 (*| TCne => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TChs => match c2 with*)
-                 (*| TChs => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TClo => match c2 with*)
-                 (*| TClo => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCmi => match c2 with*)
-                 (*| TCmi => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCpl => match c2 with*)
-                 (*| TCpl => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TChi => match c2 with*)
-                 (*| TChi => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCls => match c2 with*)
-                 (*| TCls => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCge => match c2 with*)
-                 (*| TCge => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TClt => match c2 with*)
-                 (*| TClt => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCgt => match c2 with*)
-                 (*| TCgt => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*| TCle => match c2 with*)
-                 (*| TCle => true*)
-                 (*| _ => false*)
-                 (*end*)
-       (*end).*)
-
-(*Lemma testcond_eq_correct c1 c2:*)
-  (*WHEN testcond_eq c1 c2 ~> b THEN b = true -> c1 = c2.*)
-(*Proof.*)
-  (*wlp_simplify; destruct c1; destruct c2; trivial; try discriminate.*)
-(*Qed.*)
-(*Hint Resolve testcond_eq_correct: wlp.*)
-
 Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
   match o1 with
   | OArithP n1 =>
@@ -802,14 +744,6 @@ Definition control_op_eq (c1 c2: control_op): ?? bool :=
      match c2 with Otbz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end
   | Obtbl tbl1 =>
      match c2 with Obtbl tbl2 => (phys_eq tbl1 tbl2) | _ => RET false end
-  (*| Ocbu bt1 l1 =>*)
-     (*match c2 with Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end*)
-  (*| Ojumptable tbl1 =>*)
-     (*match c2 with Ojumptable tbl2 => phys_eq tbl1 tbl2 | _ => RET false end*)
-  (*| Odiv =>*)
-     (*match c2 with Odiv => RET true | _ => RET false end*)
-  (*| Odivu =>*)
-     (*match c2 with Odivu => RET true | _ => RET false end*)
   | OIncremPC sz1 =>
       match c2 with OIncremPC sz2 => RET (Z.eqb sz1 sz2) | _ => RET false end
   | OError =>
@@ -921,7 +855,6 @@ Definition op_eq (o1 o2: op): ?? bool :=
     match o2 with Cvtx2w => RET true | _ => RET false end
   | Constant c1 =>
     match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end
-  (*| _ => RET false*)
   end.
 
 Lemma op_eq_correct o1 o2: 
@@ -947,7 +880,7 @@ Module IST := ImpSimu L ImpPosDict.
 Import L.
 Import P.
 
-(** Compilation from [Asmvliw] to [L] *)
+(** Compilation from [Asmblock] to [L] *)
 
 Local Open Scope positive_scope.
 
@@ -981,11 +914,6 @@ Proof.
   destruct r; destruct r'; try contradiction; discriminate.
 Qed.
 
-(*Lemma creg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'.*)
-(*Proof.*)
-  (*destruct r; destruct r'; try contradiction; discriminate.*)
-(*Qed.*)
-
 Definition ppos (r: preg) : R.t :=
   match r with
   | CR c => match c with
@@ -1005,13 +933,6 @@ Definition ppos (r: preg) : R.t :=
   end
 .
 
-(*Definition ppos_ireg0 (r: ireg0) : R.t :=*)
-  (*match r with*)
-  (*| RR0 p => ppos p*)
-  (*| XZR => 71*)
-  (*end*)
-(*.*)
-
 Notation "# r" := (ppos r) (at level 100, right associativity). 
 
 Lemma not_eq_add:
@@ -1147,7 +1068,9 @@ Definition trans_exit (ex: option control) : L.inst :=
 
 Definition trans_arith (ai: ar_instruction) : inst :=
   match ai with
-  | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)]
+  | PArithP n rd => 
+      if destroy_X16 n then [(#rd, Op(Arith (OArithP n)) Enil); (#X16, Op (Constant Vundef) Enil)]
+      else [(#rd, Op(Arith (OArithP n)) Enil)]
   | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))]
   | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))]
   | PArithRR0R n rd r1 r2 =>
@@ -1306,14 +1229,6 @@ Proof.
   intros. congruence.
 Qed.
 
-(*Lemma inv_ppos_from_ireg: forall (ir: ireg),*)
-  (*exists x,*)
-  (*inv_ppos (x) = Some (DR (IR ir)).*)
-(*Proof.*)
-  (*intros. unfold inv_ppos.*)
-  (*eexists (ireg_to_pos ir). destruct ir; simpl; reflexivity.*)
-(*Qed.*)
-
 Lemma ireg_pos_ppos: forall (sr: state) r,
   sr (ireg_to_pos r) = sr (# r).
 Proof.
@@ -1466,19 +1381,6 @@ Proof.
   destruct (R.eq_dec pos x); reflexivity.
 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)*)
-  (*|| (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); *)
-                                    (*try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))*)
-  (*|| (rewrite assign_eq)*)
-  (*); auto with asmgen.*)
-
-(*Ltac Simpl := repeat Simplif.*)
-
 Ltac sr_val_rwrt :=
   repeat match goal with
   | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ]
@@ -1501,7 +1403,7 @@ Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl
 
 Ltac DDRM dr :=
   destruct dr as [irsDDRF|frDDRF]; 
-      [destruct irsDDRF as [irsDDRF|]
+      [destruct irsDDRF
       | idtac ].
 
 Ltac DDRF dr :=
@@ -1575,7 +1477,7 @@ Ltac Simpl_update :=
   try eapply sr_xsp_update_both; eauto;
   try eapply sr_pc_update_both; eauto.
 
-Ltac Simpl sr := Simpl_exists sr; intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr; Simpl_update.
+Ltac Simpl sr := Simpl_exists sr; try (intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr); Simpl_update.
 
 Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity.
 
@@ -1596,6 +1498,10 @@ Ltac validate_crbit_flags c :=
     rewrite sr_gss; rewrite Pregmap.gss; reflexivity
   ].
 
+Ltac destruct_reg_neq r1 r2 :=
+  destruct (PregEq.eq r1 r2); subst;
+   [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity |
+     rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto].
 
 Lemma reg_update_overwrite: forall rsr sr r rd v1 v2
   (HEQV: forall r : preg, sr (# r) = Val (rsr r)),
@@ -1757,29 +1663,12 @@ Proof.
       discriminate_preg_flags ]).
 Qed.
 
-(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *)
-
-(*Module PChk := ParallelChecks L PosPseudoRegSet.*)
-
-(*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*)
-  (*PChk.is_parallelizable (trans_block p).*)
-
 Section SECT_SEQ.
 
-(*Import PChk.*)
-
-(*Arguments Pos.add: simpl never.*)
-(*Arguments ppos: simpl never.*)
-
 Variable Ge: genv.
 
 Lemma trans_arith_correct rsr mr sr rsw' old i:
-  (*Ge = Genv ge fn ->*)
-  (*match_states (State rs m) m' ->*)
-  (*exists em,*)
-  (*L.inst_run Ge (trans_arith o) m' old = Some em /\ match_states .*)
   match_states (State rsr mr) sr ->
-  (*match_states (State rsw mw) sw ->*)
   exec_arith_instr Ge.(_lk) i rsr = rsw' ->
   exists sw,
      inst_run Ge (trans_arith i) sr old = Some sw
@@ -1788,7 +1677,16 @@ Proof.
   induction i.
   all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr.
   - (* PArithP *)
-    DIRN1 rd; Simpl sr.
+    destruct i.
+    1,2,3: DIRN1 rd; Simpl sr.
+    (* Special case for Pmovimms/Pmovimmd *)
+    all: DIRN1 rd; Simpl sr;
+         try (rewrite assign_diff; discriminate_ppos; reflexivity);
+         try replace 24 with (#X16) by auto;
+         try replace 7 with (#XSP) by auto;
+         try (Simpl_update; intros rr; destruct_reg_neq r rr);
+         try (Simpl_update; intros rr; destruct_reg_neq XSP rr);
+         try (Simpl_update; intros rr; destruct_reg_neq f0 rr).
   - (* PArithPP *)
     DIRN1 rs; DIRN1 rd; Simpl sr.
   - (* PArithPPP *)
@@ -1860,7 +1758,6 @@ Theorem bisimu_basic rsr mr sr bi:
   match_states (State rsr mr) sr ->
   match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr).
 Proof.
-
 (* a little tactic to automate reasoning on preg_eq *)
 Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core.
 Local Ltac preg_eq_discr r rd :=
@@ -2253,32 +2150,6 @@ Proof.
   - congruence.
 Qed.
 
-(*Lemma bblock_para_check_correct ge fn bb rs m rs' m':*)
-  (*Ge = Genv ge fn ->*)
-  (*exec_bblock ge fn bb rs m = Next rs' m' ->*)
-  (*bblock_para_check bb = true ->*)
-  (*det_parexec ge fn bb rs m rs' m'.*)
-(*Proof.*)
-  (*intros H H0 H1 o H2. unfold bblock_para_check in H1.*)
-  (*exploit (bisimu rs m bb ge fn); eauto. eapply trans_state_match.*)
-  (*rewrite H0; simpl.*)
-  (*intros (s2' & EXEC & MS).*)
-  (*exploit bisimu_par. 2: apply (trans_state_match (State rs m)). all: eauto.*)
-  (*intros (o2' & PRUN & MO).*)
-  (*exploit parallelizable_correct. apply is_para_correct_aux. eassumption.*)
-  (*intro. eapply H3 in PRUN. clear H3. destruct o2'.*)
-  (*- inv PRUN. inv H3. unfold exec in EXEC; unfold trans_state in H.*)
-    (*assert (x = s2') by congruence. subst. clear H.*)
-    (*assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4.*)
-    (*destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst.*)
-    (*exploit (state_equiv (State rs' m') (State rs0 m0)).*)
-    (*2: eapply H4. eapply MS. intro H. inv H. reflexivity.*)
-  (*- unfold match_outcome in MO. destruct o.*)
-    (*+ inv MO. inv H3. discriminate.*)
-    (*+ clear MO. unfold exec in EXEC.*)
-      (*unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate.*)
-(*Qed.*)
-
 End SECT_SEQ.
 
 Section SECT_BBLOCK_EQUIV.
@@ -2644,13 +2515,7 @@ Definition string_of_control (op: control_op) : pstring :=
   | Otbz _ _ _ => "Otbz"
   | Obtbl _ => "Obtbl"
   | OIncremPC _ => "OIncremPC"
-  (*| Oj_l _ => "Oj_l"*)
-  (*| Ocbu _ _ => "Ocbu"*)
-  (*| Odiv => "Odiv"*)
-  (*| Odivu => "Odivu"*)
-  (*| Ojumptable _ => "Ojumptable"*)
   | OError => "OError"
-  (*| OIncremPC _ => "OIncremPC"*)
   end.
 
 Definition string_of_allocf (op: allocf_op) : pstring :=