diff options
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 532 |
1 files changed, 298 insertions, 234 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index af2cd46d..a7c9bb6a 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -71,16 +71,18 @@ Coercion OArithRRI32: arith_name_rri32 >-> Funclass. Coercion OArithRRI64: arith_name_rri64 >-> Funclass. Inductive load_op := - | OLoadRRO (n: load_name_rro) (ofs: offset) + | OLoadRRO (n: load_name) (ofs: offset) + | OLoadRRR (n: load_name) . -Coercion OLoadRRO: load_name_rro >-> Funclass. +Coercion OLoadRRO: load_name >-> Funclass. Inductive store_op := - | OStoreRRO (n: store_name_rro) (ofs: offset) + | OStoreRRO (n: store_name) (ofs: offset) + | OStoreRRR (n: store_name) . -Coercion OStoreRRO: store_name_rro >-> Funclass. +Coercion OStoreRRO: store_name >-> Funclass. Inductive op_wrap := | Arith (ao: arith_op) @@ -125,39 +127,49 @@ Definition arith_eval (ao: arith_op) (l: list value) := | _, _ => None end. -Definition exec_load_deps (chunk: memory_chunk) (m: mem) - (v: val) (ofs: offset) := +Definition exec_load_deps_offset (chunk: memory_chunk) (m: mem) (v: val) (ofs: offset) := let (ge, fn) := Ge in match (eval_offset ge ofs) with - | OK ptr => - match Mem.loadv chunk m (Val.offset_ptr v ptr) with - | None => None - | Some vl => Some (Val vl) - end + | OK ptr => match Mem.loadv chunk m (Val.offset_ptr v ptr) with + | None => None + | Some vl => Some (Val vl) + end | _ => None end. +Definition exec_load_deps_reg (chunk: memory_chunk) (m: mem) (v vo: val) := + match Mem.loadv chunk m (Val.addl v vo) with + | None => None + | Some vl => Some (Val vl) + end. + Definition load_eval (lo: load_op) (l: list value) := match lo, l with - | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps (load_chunk n) m v ofs + | OLoadRRO n ofs, [Val v; Memstate m] => exec_load_deps_offset (load_chunk n) m v ofs + | OLoadRRR n, [Val v; Val vo; Memstate m] => exec_load_deps_reg (load_chunk n) m v vo | _, _ => None end. -Definition exec_store_deps (chunk: memory_chunk) (m: mem) - (vs va: val) (ofs: offset) := +Definition exec_store_deps_offset (chunk: memory_chunk) (m: mem) (vs va: val) (ofs: offset) := let (ge, fn) := Ge in match (eval_offset ge ofs) with - | OK ptr => - match Mem.storev chunk m (Val.offset_ptr va ptr) vs with - | None => None - | Some m' => Some (Memstate m') - end + | OK ptr => match Mem.storev chunk m (Val.offset_ptr va ptr) vs with + | None => None + | Some m' => Some (Memstate m') + end | _ => None end. +Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) := + match Mem.storev chunk m (Val.addl va vo) 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 (store_chunk n) m vs va ofs + | 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 | _, _ => None end. @@ -270,33 +282,30 @@ Definition op_eval (o: op) (l: list value) := end. -Definition is_constant (o: op): bool := - (* FIXME - - => répondre "true" autant que possible mais en satisfaisant [is_constant_correct] ci-dessous. + (** Function [is_constant] is used for a small optimization inside the scheduling verifier. + It is good that it answers [true] as much as possible while satisfying [is_constant_correct] below. - ATTENTION, is_constant ne doit pas dépendre de [ge]. - Sinon, on aurait une implémentation facile: [match op_eval o nil with Some _ => true | _ => false end] + BE CAREFUL that, [is_constant] must not depend on [ge]. + Otherwise, we would have an easy implementation: [match op_eval o nil with Some _ => true | _ => false end] - => REM: il n'est pas sûr que ce soit utile de faire qqchose de très exhaustif en pratique... - (ça sert juste à une petite optimisation du vérificateur de scheduling). + => REM: when [is_constant] is not complete w.r.t [is_constant_correct], this should have only a very little impact + on the performance of the scheduling verifier... *) + +Definition is_constant (o: op): bool := match o with - | Constant _ => true + | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true | _ => false end. Lemma is_constant_correct o: is_constant o = true -> op_eval o nil <> None. Proof. destruct o; simpl; try congruence. + destruct ao; simpl; try congruence; + destruct n; simpl; try congruence; + unfold arith_eval; destruct Ge; simpl; try congruence. Qed. - -Definition iandb (ib1 ib2: ?? bool): ?? bool := - DO b1 <~ ib1;; - DO b2 <~ ib2;; - RET (andb b1 b2). - Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o1 with | OArithR n1 => @@ -325,99 +334,110 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end end. +Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; congruence || intuition eauto with wlp). + Lemma arith_op_eq_correct o1 o2: WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. - destruct o1, o2; wlp_simplify; try discriminate. - all: try congruence. - all: apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + destruct o1, o2; my_wlp_simplify; try congruence. Qed. - +Hint Resolve arith_op_eq_correct: wlp. +Opaque arith_op_eq_correct. Definition load_op_eq (o1 o2: load_op): ?? bool := match o1, o2 with | OLoadRRO n1 ofs1, OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) + | OLoadRRR n1, OLoadRRR n2 => phys_eq n1 n2 + | _, _ => RET false end. Lemma load_op_eq_correct o1 o2: WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. - destruct o1, o2; wlp_simplify. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + destruct o1, o2; wlp_simplify; try discriminate. + - congruence. + - congruence. Qed. +Hint Resolve load_op_eq_correct: wlp. +Opaque load_op_eq_correct. Definition store_op_eq (o1 o2: store_op): ?? bool := match o1, o2 with | OStoreRRO n1 ofs1, OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) + | OStoreRRR n1, OStoreRRR n2 => phys_eq n1 n2 + | _, _ => RET false end. Lemma store_op_eq_correct o1 o2: WHEN store_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. - destruct o1, o2; wlp_simplify. - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. + destruct o1, o2; wlp_simplify; try discriminate. + - congruence. + - congruence. Qed. +Hint Resolve store_op_eq_correct: wlp. +Opaque store_op_eq_correct. -(* TODO: rewrite control_op_eq in a robust style against the miss of a case - cf. arith_op_eq above *) Definition control_op_eq (c1 c2: control_op): ?? bool := - match c1, c2 with - | Oj_l l1, Oj_l l2 => phys_eq l1 l2 - | Ocb bt1 l1, Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) - | Ocbu bt1 l1, Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) - | Ojumptable tbl1, Ojumptable tbl2 => phys_eq tbl1 tbl2 - | Odiv, Odiv => RET true - | Odivu, Odivu => RET true - | OIncremPC sz1, OIncremPC sz2 => RET (Z.eqb sz1 sz2) - | OError, OError => RET true - | _, _ => RET false + match c1 with + | Oj_l l1 => + match c2 with Oj_l l2 => phys_eq l1 l2 | _ => RET false end + | Ocb bt1 l1 => + match c2 with Ocb bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => 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 => + match c2 with OError => RET true | _ => RET false end end. Lemma control_op_eq_correct c1 c2: WHEN control_op_eq c1 c2 ~> b THEN b = true -> c1 = c2. Proof. - destruct c1, c2; wlp_simplify; try discriminate. - - congruence. - - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - - apply andb_prop in H1; inversion H1; apply H in H2; apply H0 in H3; congruence. - - rewrite Z.eqb_eq in * |-. congruence. - - congruence. + destruct c1, c2; wlp_simplify; try rewrite Z.eqb_eq in * |-; try congruence. Qed. +Hint Resolve control_op_eq_correct: wlp. +Opaque control_op_eq_correct. - -(* TODO: rewrite op_eq in a robust style against the miss of a case - cf. arith_op_eq above *) Definition op_eq (o1 o2: op): ?? bool := - match o1, o2 with - | Arith i1, Arith i2 => arith_op_eq i1 i2 - | Load i1, Load i2 => load_op_eq i1 i2 - | Store i1, Store i2 => store_op_eq i1 i2 - | Control i1, Control i2 => control_op_eq i1 i2 - | Allocframe sz1 pos1, Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) - | Allocframe2 sz1 pos1, Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) - | Freeframe sz1 pos1, Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) - | Freeframe2 sz1 pos1, Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) - | Constant c1, Constant c2 => phys_eq c1 c2 - | Fail, Fail => RET true - | _, _ => RET false + match o1 with + | Arith i1 => + match o2 with Arith i2 => arith_op_eq i1 i2 | _ => RET false end + | Load i1 => + match o2 with Load i2 => load_op_eq i1 i2 | _ => RET false end + | Store i1 => + match o2 with Store i2 => store_op_eq i1 i2 | _ => RET false end + | Control i1 => + match o2 with Control i2 => control_op_eq i1 i2 | _ => RET false end + | Allocframe sz1 pos1 => + match o2 with Allocframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Allocframe2 sz1 pos1 => + match o2 with Allocframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Freeframe sz1 pos1 => + match o2 with Freeframe sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Freeframe2 sz1 pos1 => + match o2 with Freeframe2 sz2 pos2 => iandb (RET (Z.eqb sz1 sz2)) (phys_eq pos1 pos2) | _ => RET false end + | Constant c1 => + match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end + | Fail => + match o2 with Fail => RET true | _ => RET false end end. - Theorem op_eq_correct o1 o2: WHEN op_eq o1 o2 ~> b THEN b=true -> o1 = o2. Proof. - destruct o1, o2; wlp_simplify; try discriminate. - - simpl in Hexta. exploit arith_op_eq_correct. eassumption. eauto. congruence. - - simpl in Hexta. exploit load_op_eq_correct. eassumption. eauto. congruence. - - simpl in Hexta. exploit store_op_eq_correct. eassumption. eauto. congruence. - - simpl in Hexta. exploit control_op_eq_correct. eassumption. eauto. congruence. - - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. - - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. - - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. - - apply andb_prop in H0; inversion_clear H0. apply H in H2. apply Z.eqb_eq in H1. congruence. - - congruence. + destruct o1, o2; wlp_simplify; try rewrite Z.eqb_eq in * |- ; try congruence. Qed. +Hint Resolve op_eq_correct: wlp. +Global Opaque op_eq_correct. (* QUICK FIX WITH struct_eq *) @@ -542,74 +562,76 @@ Definition inv_ppos (p: R.t) : option preg := Notation "a @ b" := (Econs a b) (at level 102, right associativity). -Definition trans_control (ctl: control) : macro := +Definition trans_control (ctl: control) : inst := match ctl with - | Pret => [(#PC, Name (#RA))] - | Pcall s => [(#RA, Name (#PC)); (#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)] - | Picall r => [(#RA, Name (#PC)); (#PC, Name (#r))] + | Pret => [(#PC, PReg(#RA))] + | Pcall s => [(#RA, PReg(#PC)); (#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)] + | Picall r => [(#RA, PReg(#PC)); (#PC, PReg(#r))] | Pgoto s => [(#PC, Op (Arith (OArithR (Ploadsymbol s Ptrofs.zero))) Enil)] - | Pigoto r => [(#PC, Name (#r))] - | Pj_l l => [(#PC, Op (Control (Oj_l l)) (Name (#PC) @ Enil))] - | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (Name (#r) @ Name (#PC) @ Enil))] - | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (Name (#r) @ Name (#PC) @ Enil))] - | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (Name (#r) @ Name (#PC) @ Enil)); + | Pigoto r => [(#PC, PReg(#r))] + | Pj_l l => [(#PC, Op (Control (Oj_l l)) (PReg(#PC) @ Enil))] + | Pcb bt r l => [(#PC, Op (Control (Ocb bt l)) (PReg(#r) @ PReg(#PC) @ Enil))] + | Pcbu bt r l => [(#PC, Op (Control (Ocbu bt l)) (PReg(#r) @ PReg(#PC) @ Enil))] + | Pjumptable r labels => [(#PC, Op (Control (Ojumptable labels)) (PReg(#r) @ PReg(#PC) @ Enil)); (#GPR62, Op (Constant Vundef) Enil); (#GPR63, Op (Constant Vundef) Enil) ] | Pbuiltin ef args res => [(#PC, Op (Control (OError)) Enil)] end. -Definition trans_exit (ex: option control) : L.macro := +Definition trans_exit (ex: option control) : L.inst := match ex with | None => [] | Some ctl => trans_control ctl end . -Definition trans_arith (ai: ar_instruction) : macro := +Definition trans_arith (ai: ar_instruction) : inst := match ai with | PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)] - | PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (Name (#s) @ Enil))] + | PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))] | PArithRI32 n d i => [(#d, Op (Arith (OArithRI32 n i)) Enil)] | PArithRI64 n d i => [(#d, Op (Arith (OArithRI64 n i)) Enil)] | PArithRF32 n d i => [(#d, Op (Arith (OArithRF32 n i)) Enil)] | PArithRF64 n d i => [(#d, Op (Arith (OArithRF64 n i)) Enil)] - | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (Name (#s1) @ Name (#s2) @ Enil))] - | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (Name (#s) @ Enil))] - | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (Name (#s) @ Enil))] - | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (Name(#d) @ Name (#s1) @ Name (#s2) @ Enil))] - | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (Name(#d) @ Name (#s) @ Enil))] - | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (Name(#d) @ Name (#s) @ Enil))] + | PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (PReg(#s1) @ PReg(#s2) @ Enil))] + | PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (PReg(#s) @ Enil))] + | PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (PReg(#s) @ Enil))] + | PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (PReg(#d) @ PReg(#s1) @ PReg(#s2) @ Enil))] + | PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (PReg(#d) @ PReg(#s) @ Enil))] + | PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (PReg(#d) @ PReg(#s) @ Enil))] end. -Definition trans_basic (b: basic) : macro := +Definition trans_basic (b: basic) : inst := match b with | PArith ai => trans_arith ai - | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (Name (#a) @ Name pmem @ Enil))] - | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (Name (#s) @ Name (#a) @ Name pmem @ Enil))] - | Pallocframe sz pos => [(#FP, Name (#SP)); (#SP, Op (Allocframe2 sz pos) (Name (#SP) @ Name pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); - (pmem, Op (Allocframe sz pos) (Old (Name (#SP)) @ Name pmem @ Enil))] - | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (Name (#SP) @ Name pmem @ Enil)); - (#SP, Op (Freeframe2 sz pos) (Name (#SP) @ Old (Name pmem) @ Enil)); + | PLoadRRO n d a ofs => [(#d, Op (Load (OLoadRRO n ofs)) (PReg (#a) @ PReg pmem @ Enil))] + | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR 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))] + | 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)); + (#SP, Op (Freeframe2 sz pos) (PReg (#SP) @ Old (PReg pmem) @ Enil)); (#RTMP, Op (Constant Vundef) Enil)] | Pget rd ra => match ra with - | RA => [(#rd, Name (#ra))] + | RA => [(#rd, PReg(#ra))] | _ => [(#rd, Op Fail Enil)] end | Pset ra rd => match ra with - | RA => [(#ra, Name (#rd))] + | RA => [(#ra, PReg(#rd))] | _ => [(#rd, Op Fail Enil)] end | Pnop => [] end. -Fixpoint trans_body (b: list basic) : list L.macro := +Fixpoint trans_body (b: list basic) : list L.inst := match b with | nil => nil | b :: lb => (trans_basic b) :: (trans_body lb) end. -Definition trans_pcincr (sz: Z) (k: L.macro) := (#PC, Op (Control (OIncremPC sz)) (Name (#PC) @ Enil)) :: k. +Definition trans_pcincr (sz: Z) (k: L.inst) := (#PC, Op (Control (OIncremPC sz)) (PReg(#PC) @ Enil)) :: k. Definition trans_block (b: Asmblock.bblock) : L.bblock := trans_body (body b) ++ (trans_pcincr (size b) (trans_exit (exit b)) :: nil). @@ -686,7 +708,7 @@ Lemma exec_app_some: Proof. induction c. - simpl. intros. congruence. - - intros. simpl in *. destruct (macro_run _ _ _ _); auto. eapply IHc; eauto. discriminate. + - intros. simpl in *. destruct (inst_run _ _ _ _); auto. eapply IHc; eauto. discriminate. Qed. Lemma exec_app_none: @@ -696,7 +718,7 @@ Lemma exec_app_none: Proof. induction c. - simpl. discriminate. - - intros. simpl. simpl in H. destruct (macro_run _ _ _ _); auto. + - intros. simpl. simpl in H. destruct (inst_run _ _ _ _); auto. Qed. Lemma trans_arith_correct: @@ -704,7 +726,7 @@ Lemma trans_arith_correct: exec_arith_instr ge i rs = rs' -> match_states (State rs m) s -> exists s', - macro_run (Genv ge fn) (trans_arith i) s s = Some s' + inst_run (Genv ge fn) (trans_arith i) s s = Some s' /\ match_states (State rs' m) s'. Proof. intros. unfold exec_arith_instr in H. destruct i. @@ -793,31 +815,50 @@ Lemma forward_simu_basic: exec_basic_instr ge b rs m = Next rs' m' -> match_states (State rs m) s -> exists s', - macro_run (Genv ge fn) (trans_basic b) s s = Some s' + inst_run (Genv ge fn) (trans_basic b) s s = Some s' /\ match_states (State rs' m') s'. Proof. intros. destruct b. (* Arith *) - - simpl in H. inv H. simpl macro_run. eapply trans_arith_correct; eauto. + - simpl in H. inv H. simpl inst_run. eapply trans_arith_correct; eauto. (* Load *) - 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| - Simpl| - intros rr; destruct rr; Simpl; - destruct (ireg_eq g rd); [ - subst; Simpl| - Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]]. + (* Load Offset *) + + destruct i. all: + unfold exec_load_offset 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; rewrite (H1 ra); simpl in MEML; rewrite MEML; reflexivity + | Simpl + | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. + (* Load Reg *) + + destruct i. all: + unfold exec_load_reg in H; destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); unfold exec_load_deps_reg; simpl in MEML; rewrite MEML; reflexivity + | Simpl + | intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl ]. + (* Store *) - 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; - [ simpl; rewrite EVALOFF; rewrite H; pose (H1 ra); simpl in e; rewrite e; pose (H1 rs0); simpl in e0; rewrite e0; rewrite MEML; reflexivity - | Simpl - | intros rr; destruct rr; Simpl]. + (* Store Offset *) + + destruct i. all: + unfold exec_store_offset in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite EVALOFF; rewrite H; rewrite (H1 ra); rewrite (H1 rs0); simpl in MEML; rewrite MEML; reflexivity + | Simpl + | intros rr; destruct rr; Simpl ]. + (* Store Reg *) + + destruct i. all: + unfold exec_store_reg in H; + destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate; inv H; inv H0; + eexists; split; try split; + [ simpl; rewrite H; rewrite (H1 rofs); rewrite (H1 ra); rewrite (H1 rs0); unfold exec_store_deps_reg; + simpl in MEML; rewrite MEML; reflexivity + | Simpl + | intros rr; destruct rr; Simpl ]. + (* Allocframe *) - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. inv H. inv H0. eexists. split; try split. @@ -842,7 +883,7 @@ Proof. - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv H0. eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. (* Pnop *) - - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. + - simpl in H. inv H. inv H0. eexists. split; try split. assumption. assumption. Qed. Lemma forward_simu_body: @@ -1040,11 +1081,11 @@ Proof. eapply IHc; eauto. Qed. -Lemma exec_trans_pcincr_exec_macrorun: +Lemma exec_trans_pcincr_exec_instrun: forall rs m s b k, match_states (State rs m) s -> exists s', - macro_run Ge ((# PC, Op (OIncremPC (size b)) (Name (# PC) @ Enil)) :: k) s s = macro_run Ge k s' s + inst_run Ge ((# PC, Op (OIncremPC (size b)) (PReg(# PC) @ Enil)) :: k) s s = inst_run Ge k s' s /\ match_states (State (nextblock b rs) m) s'. Proof. intros. inv H. eexists. split. simpl. pose (H1 PC); simpl in e; rewrite e. destruct Ge. simpl. eapply eq_refl. @@ -1053,9 +1094,9 @@ Proof. - intros rr; destruct rr; Simpl. Qed. -Lemma macro_run_trans_exit_noold: +Lemma inst_run_trans_exit_noold: forall ex s s' s'', - macro_run Ge (trans_exit ex) s s' = macro_run Ge (trans_exit ex) s s''. + inst_run Ge (trans_exit ex) s s' = inst_run Ge (trans_exit ex) s s''. Proof. intros. destruct ex. - destruct c; destruct i; reflexivity. @@ -1070,10 +1111,10 @@ Lemma exec_trans_pcincr_exec: /\ match_states (State (nextblock b rs) m) s'. Proof. intros. - exploit exec_trans_pcincr_exec_macrorun; eauto. + exploit exec_trans_pcincr_exec_instrun; eauto. intros (s' & MRUN & MS). eexists. split. unfold exec. unfold trans_pcincr. unfold run. rewrite MRUN. - erewrite macro_run_trans_exit_noold; eauto. + erewrite inst_run_trans_exit_noold; eauto. assumption. Qed. @@ -1155,13 +1196,28 @@ Lemma forward_simu_basic_instr_stuck: Proof. intros. inv H1. unfold exec_basic_instr in H0. destruct i; try discriminate. (* PLoad *) - - destruct i; destruct i. - all: simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; - unfold exec_load in H0; destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate. + - destruct i. + (* Load Offset *) + + destruct i. all: + simpl; rewrite H2; rewrite (H3 ra); unfold exec_load_offset in H0; destruct (eval_offset _ _); auto; + simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. + (* Load Reg *) + + destruct i. all: + simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); unfold exec_load_reg in H0; unfold exec_load_deps_reg; + destruct (rs rofs); auto; simpl in H0; destruct (Mem.loadv _ _ _); auto; discriminate. + (* PStore *) - - destruct i; destruct i; - simpl; rewrite H2; pose (H3 ra); simpl in e; rewrite e; clear e; pose (H3 rs0); simpl in e; rewrite e; clear e; - unfold exec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate. + - destruct i. + (* Store Offset *) + + destruct i. all: + simpl; rewrite H2; rewrite (H3 ra); rewrite (H3 rs0); unfold exec_store_offset in H0; destruct (eval_offset _ _); auto; + simpl in H0; destruct (Mem.storev _ _ _); auto; discriminate. + (* Store Reg *) + + destruct i. all: + simpl; rewrite H2; rewrite (H3 rofs); rewrite (H3 ra); rewrite (H3 rs0); simpl in H0; unfold exec_store_reg in H0; + unfold exec_store_deps_reg; destruct (rs rofs); auto; + destruct (Mem.storev _ _ _ _); auto; discriminate. + (* Pallocframe *) - simpl. Simpl. pose (H3 SP); simpl in e; rewrite e; clear e. rewrite H2. destruct (Mem.alloc _ _ _). simpl in H0. destruct (Mem.store _ _ _ _); try discriminate. reflexivity. @@ -1505,7 +1561,7 @@ Definition string_of_arith (op: arith_op): pstring := | OArithARRI64 n _ => string_of_name_arri64 n end. -Definition string_of_name_lrro (n: load_name_rro) : pstring := +Definition string_of_load_name (n: load_name) : pstring := match n with Plb => "Plb" | Plbu => "Plbu" @@ -1521,10 +1577,11 @@ Definition string_of_name_lrro (n: load_name_rro) : pstring := Definition string_of_load (op: load_op): pstring := match op with - | OLoadRRO n _ => string_of_name_lrro n + | OLoadRRO n _ => string_of_load_name n + | OLoadRRR n => string_of_load_name n end. -Definition string_of_name_srro (n: store_name_rro) : pstring := +Definition string_of_store_name (n: store_name) : pstring := match n with Psb => "Psb" | Psh => "Psh" @@ -1538,7 +1595,8 @@ Definition string_of_name_srro (n: store_name_rro) : pstring := Definition string_of_store (op: store_op) : pstring := match op with - | OStoreRRO n _ => string_of_name_srro n + | OStoreRRO n _ => string_of_store_name n + | OStoreRRR n => string_of_store_name n end. Definition string_of_control (op: control_op) : pstring := @@ -1604,7 +1662,7 @@ End SECT. (** Parallelizability of a bblock *) -Module PChk := ParallelChecks L PosResourceSet. +Module PChk := ParallelChecks L PosPseudoRegSet. Definition bblock_para_check (p: Asmblock.bblock) : bool := PChk.is_parallelizable (trans_block p). @@ -1632,16 +1690,16 @@ Arguments ppos: simpl never. Variable Ge: genv. -Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' mw' i: +Lemma trans_arith_par_correct ge fn rsr mr sr rsw mw sw rsw' i: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_arith_instr ge i rsr rsw = rsw' -> mw = mw' -> + parexec_arith_instr ge i rsr rsw = rsw' -> exists sw', - macro_prun Ge (trans_arith i) sw sr sr = Some sw' - /\ match_states (State rsw' mw') sw'. + inst_prun Ge (trans_arith i) sw sr sr = Some sw' + /\ match_states (State rsw' mw) sw'. Proof. - intros GENV MSR MSW PARARITH MWEQ. subst. inv MSR. inv MSW. + intros GENV MSR MSW PARARITH. subst. inv MSR. inv MSW. unfold parexec_arith_instr. destruct i. (* Ploadsymbol *) - destruct i. eexists; split; [| split]. @@ -1717,63 +1775,91 @@ Proof. destruct (ireg_eq g rd); subst; Simpl. Qed. -Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi rsw' mw': +Theorem forward_simu_par_wio_basic_gen ge fn rsr rsw mr mw sr sw bi: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_basic_instr ge bi rsr rsw mr mw = Next rsw' mw' -> - exists sw', - macro_prun Ge (trans_basic bi) sw sr sr = Some sw' - /\ match_states (State rsw' mw') sw'. + match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). Proof. - intros GENV MSR MSW H. - destruct bi. + intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2). + destruct bi; simpl. (* Arith *) - - simpl in H. inversion H. subst rsw' mw'. simpl macro_prun. eapply trans_arith_par_correct; eauto. + - exploit trans_arith_par_correct. 5: eauto. all: eauto. (* Load *) - - simpl in H. destruct i. - unfold parexec_load in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate; - destruct (Mem.loadv _ _ _) eqn:MEML; try discriminate; inv H. inv MSR; inv MSW; - eexists; split; try split; - [ simpl; rewrite EVALOFF; rewrite H; pose (H0 ra); simpl in e; rewrite e; rewrite MEML; reflexivity| - Simpl| - intros rr; destruct rr; Simpl; - destruct (ireg_eq g rd); [ - subst; Simpl| - Simpl; rewrite assign_diff; pose (H1 g); simpl in e; try assumption; Simpl; unfold ppos; apply not_eq_ireg_to_pos; assumption]]. + - destruct i. + (* Load Offset *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_offset; simpl; unfold exec_load_deps_offset; erewrite GENV, H, H0; + destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Reg *) + + destruct i; simpl load_chunk. all: + unfold parexec_load_reg; simpl; unfold exec_load_deps_reg; rewrite H, H0; rewrite (H0 rofs); + destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + (* Store *) - - simpl in H. destruct i. - unfold parexec_store in H; destruct (eval_offset _ _) eqn:EVALOFF; try discriminate. - destruct (Mem.storev _ _ _ _) eqn:MEML; try discriminate. inv H; inv MSR; inv MSW. - eexists; split; try split. - * simpl. rewrite EVALOFF. rewrite H. rewrite (H0 ra). rewrite (H0 rs). rewrite MEML. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. + - destruct i. + (* Store Offset *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_offset; simpl; unfold exec_store_deps_offset; erewrite GENV, H, H0; rewrite (H0 ra); + destruct (eval_offset _ _) eqn:EVALOFF; simpl; auto; + destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto; + eexists; split; try split; Simpl; + intros rr; destruct rr; Simpl. + + (* Store Reg *) + + destruct i; simpl store_chunk. all: + unfold parexec_store_reg; simpl; unfold exec_store_deps_reg; 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 *) - - simpl in H. destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS; try discriminate. - inv H. inv MSR. inv MSW. eexists. split; try split. - * simpl. Simpl. rewrite (H0 GPR12). rewrite H. rewrite MEMAL. rewrite MEMS. Simpl. - rewrite H. rewrite MEMAL. rewrite MEMS. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. -(* Freeframe *) - - simpl in H. destruct (Mem.loadv _ _ _) eqn:MLOAD; try discriminate. destruct (rsr GPR12) eqn:SPeq; try discriminate. - destruct (Mem.free _ _ _ _) eqn:MFREE; try discriminate. inv H. inv MSR. inv MSW. - eexists. split; try split. - * simpl. rewrite (H0 GPR12). rewrite H. rewrite SPeq. rewrite MLOAD. rewrite MFREE. - Simpl. rewrite (H0 GPR12). rewrite SPeq. rewrite MLOAD. rewrite MFREE. reflexivity. + - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. + * eexists; repeat split. + { Simpl. erewrite !H0, H, MEMAL, MEMS. Simpl. + rewrite H, MEMAL. rewrite MEMS. reflexivity. } + { Simpl. } + { intros rr; destruct rr; Simpl. + destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. } + * simpl; Simpl; erewrite !H0, H, MEMAL, MEMS; auto. + (* Freeframe *) + - erewrite !H0, H. + destruct (Mem.loadv _ _ _) eqn:MLOAD; simpl; auto. + destruct (rsr GPR12) eqn:SPeq; simpl; auto. + destruct (Mem.free _ _ _ _) eqn:MFREE; simpl; auto. + eexists; repeat split. + * simpl. Simpl. erewrite H0, SPeq, MLOAD, MFREE. reflexivity. * Simpl. * intros rr; destruct rr; Simpl. destruct (ireg_eq g GPR32); [| destruct (ireg_eq g GPR12); [| destruct (ireg_eq g GPR17)]]; subst; Simpl. (* Pget *) - - simpl in H. destruct rs eqn:rseq; try discriminate. inv H. inv MSR. inv MSW. - eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. + - destruct rs eqn:rseq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. (* Pset *) - - simpl in H. destruct rd eqn:rdeq; try discriminate. inv H. inv MSR; inv MSW. - eexists. split; try split. Simpl. intros rr; destruct rr; Simpl. + - destruct rd eqn:rdeq; simpl; auto. + eexists. repeat split. Simpl. intros rr; destruct rr; Simpl. (* Pnop *) - - simpl in H. inv H. inv MSR. inv MSW. eexists. split; try split. assumption. assumption. + - eexists. repeat split; assumption. +Qed. + + +Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi rsw' mw': + Ge = Genv ge fn -> + match_states (State rsr mr) sr -> + match_states (State rsw mw) sw -> + parexec_basic_instr ge bi rsr rsw mr mw = Next rsw' mw' -> + exists sw', + inst_prun Ge (trans_basic bi) sw sr sr = Some sw' + /\ match_states (State rsw' mw') sw'. +Proof. + intros H H0 H1 H2; exploit forward_simu_par_wio_basic_gen; [ eapply H | eapply H0 | eapply H1 | erewrite H2 ]. + simpl; auto. Qed. Theorem forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi: @@ -1781,30 +1867,10 @@ Theorem forward_simu_par_wio_basic_Stuck ge fn rsr rsw mr mw sr sw bi: match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> parexec_basic_instr ge bi rsr rsw mr mw = Stuck -> - macro_prun Ge (trans_basic bi) sw sr sr = None. + inst_prun Ge (trans_basic bi) sw sr sr = None. Proof. - intros GENV MSR MSW H0. inv MSR; inv MSW. - unfold parexec_basic_instr in H0. destruct bi; try discriminate. -(* PLoad *) - - destruct i; destruct i. - all: simpl; rewrite H; rewrite (H1 ra); unfold parexec_load in H0; - destruct (eval_offset _ _); auto; destruct (Mem.loadv _ _ _); auto; discriminate. -(* PStore *) - - destruct i; destruct i; - simpl; rewrite H; rewrite (H1 ra); rewrite (H1 rs); - unfold parexec_store in H0; destruct (eval_offset _ _); auto; destruct (Mem.storev _ _ _); auto; discriminate. -(* Pallocframe *) - - simpl. Simpl. rewrite (H1 SP). rewrite H. destruct (Mem.alloc _ _ _). simpl in H0. - destruct (Mem.store _ _ _ _); try discriminate. reflexivity. -(* Pfreeframe *) - - simpl. Simpl. rewrite (H1 SP). rewrite H. - destruct (Mem.loadv _ _ _); auto. destruct (rsr GPR12); auto. destruct (Mem.free _ _ _ _); auto. - discriminate. -(* Pget *) - - simpl. destruct rs; subst; try discriminate. - all: simpl; auto. - - simpl. destruct rd; subst; try discriminate. - all: simpl; auto. + intros H H0 H1 H2; exploit forward_simu_par_wio_basic_gen; [ eapply H | eapply H0 | eapply H1 | erewrite H2 ]. + simpl; auto. Qed. Theorem forward_simu_par_body: @@ -1835,9 +1901,9 @@ Theorem forward_simu_par_control ge fn rsr rsw mr mw sr sw sz rs' ex m': Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Next rs' m' -> + parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' -> exists s', - macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s' + inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s' /\ match_states (State rs' m') s'. Proof. intros GENV MSR MSW H0. @@ -1947,8 +2013,8 @@ Lemma forward_simu_par_control_Stuck ge fn rsr rsw mr mw sr sw sz ex: Ge = Genv ge fn -> match_states (State rsr mr) sr -> match_states (State rsw mw) sw -> - parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) (par_nextblock (Ptrofs.repr sz) rsw) mw = Stuck -> - macro_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. + parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw = Stuck -> + inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. Proof. intros GENV MSR MSW H0. inv MSR; inv MSW. destruct ex as [ctl|]; try discriminate. destruct ctl; destruct i; try discriminate; try (simpl; reflexivity). @@ -2159,15 +2225,13 @@ Proof. constructor; auto. Qed. -Lemma bblock_para_check_correct: - forall ge fn bb rs m rs' m' o, +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 -> - parexec_bblock ge fn bb rs m o -> - o = Next rs' m'. + det_parexec ge fn bb rs m rs' m'. Proof. - intros. unfold bblock_para_check in H1. + intros H H0 H1 o H2. unfold bblock_para_check in H1. exploit forward_simu; eauto. eapply trans_state_match. intros (s2' & EXEC & MS). exploit forward_simu_par_alt. 2: apply (trans_state_match (State rs m)). all: eauto. |