From fb8c244726595b0e7a4db8c0f8e6aa3f3549cc14 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 5 Apr 2019 18:14:07 +0200 Subject: relecture sylvain avec TODOs pour refactoring #90 --- mppa_k1c/Asmblock.v | 412 +++++++++++++++++++++-------------- mppa_k1c/Asmblockdeps.v | 34 +-- mppa_k1c/Asmblockgenproof.v | 20 +- mppa_k1c/Asmblockgenproof1.v | 12 +- mppa_k1c/Asmvliw.v | 367 ++++++------------------------- mppa_k1c/PostpassSchedulingOracle.ml | 1 + mppa_k1c/PostpassSchedulingproof.v | 10 +- mppa_k1c/lib/Asmblockgenproof0.v | 2 +- 8 files changed, 353 insertions(+), 505 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 3bcb321d..0f65b1d0 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -33,13 +33,234 @@ Require Import Conventions. Require Import Errors. Require Export Asmvliw. + +(** * Auxiliary utilies on basic blocks *) + +(** ** A unified view of Kalray instructions *) + +Inductive instruction : Type := + | PBasic (i: basic) + | PControl (i: control) +. + +Coercion PBasic: basic >-> instruction. +Coercion PControl: control >-> instruction. + +Definition code := list instruction. +Definition bcode := list basic. + +Fixpoint basics_to_code (l: list basic) := + match l with + | nil => nil + | bi::l => (PBasic bi)::(basics_to_code l) + end. + +Fixpoint code_to_basics (c: code) := + match c with + | (PBasic i)::c => + match code_to_basics c with + | None => None + | Some l => Some (i::l) + end + | _::c => None + | nil => Some nil + end. + +Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. +Proof. + intros. induction c as [|i c]; simpl; auto. + rewrite IHc. auto. +Qed. + +Lemma code_to_basics_dist: + forall c c' l l', + code_to_basics c = Some l -> + code_to_basics c' = Some l' -> + code_to_basics (c ++ c') = Some (l ++ l'). +Proof. + induction c as [|i c]; simpl; auto. + - intros. inv H. simpl. auto. + - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. + inv H. erewrite IHc; eauto. auto. +Qed. + +(** + Asmblockgen will have to translate a Mach control into a list of instructions of the form + i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction + These functions provide way to extract the basic / control instructions +*) + +Fixpoint extract_basic (c: code) := + match c with + | nil => nil + | PBasic i :: c => i :: (extract_basic c) + | PControl i :: c => nil + end. + +Fixpoint extract_ctl (c: code) := + match c with + | nil => None + | PBasic i :: c => extract_ctl c + | PControl i :: nil => Some i + | PControl i :: _ => None (* if the first found control instruction isn't the last *) + end. + +(** ** Wellformness of basic blocks *) + +Ltac exploreInst := + repeat match goal with + | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var + | [ H : OK _ = OK _ |- _ ] => monadInv H + | [ |- context[if ?b then _ else _] ] => destruct b + | [ |- context[match ?m with | _ => _ end] ] => destruct m + | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m + | [ H : bind _ _ = OK _ |- _ ] => monadInv H + | [ H : Error _ = OK _ |- _ ] => inversion H + end. + +Definition non_empty_bblock (body: list basic) (exit: option control): Prop + := body <> nil \/ exit <> None. + +Lemma non_empty_bblock_refl: + forall body exit, + non_empty_bblock body exit <-> + Is_true (non_empty_bblockb body exit). +Proof. + intros. split. + - destruct body; destruct exit. + all: simpl; auto. intros. inversion H; contradiction. + - destruct body; destruct exit. + all: simpl; auto. + all: intros; try (right; discriminate); try (left; discriminate). + contradiction. +Qed. + +Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, + exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. + + +Lemma builtin_alone_refl: + forall body exit, + builtin_alone body exit <-> Is_true (builtin_aloneb body exit). +Proof. + intros. split. + - destruct body; destruct exit. + all: simpl; auto. + all: exploreInst; simpl; auto. + unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto. + assert (b :: body = nil). eapply H; eauto. discriminate. + - destruct body; destruct exit. + all: simpl; auto; try constructor. + + exploreInst; try discriminate. + simpl. contradiction. + + intros. discriminate. +Qed. + +Definition wf_bblock (body: list basic) (exit: option control) := + non_empty_bblock body exit /\ builtin_alone body exit. + +Lemma wf_bblock_refl: + forall body exit, + wf_bblock body exit <-> Is_true (wf_bblockb body exit). +Proof. + intros. split. + - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. + apply andb_prop_intro. auto. + - intros. apply andb_prop_elim in H. inv H. + apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. + unfold wf_bblock. split; auto. +Qed. + +Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)). +(* Local Obligation Tactic := bblock_auto_correct. *) + +Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. +Proof. + destruct b; simpl; auto. + - destruct p1, p2; auto. + - destruct p1. +Qed. + +Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. +Proof. + destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl. + intros; subst. + rewrite (Istrue_proof_irrelevant _ c1 c2). + auto. +Qed. + +Program Definition bblock_single_inst (i: instruction) := + match i with + | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |} + | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |} + end. +Next Obligation. + apply wf_bblock_refl. constructor. + right. discriminate. + constructor. +Qed. + +Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. +Proof. + intros. destruct l; try (contradict H; auto; fail). + simpl. omega. +Qed. + +Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. +Proof. + intros. destruct z; auto. + - contradict H. simpl. apply gt_irrefl. + - apply Zgt_pos_0. + - contradict H. simpl. apply gt_irrefl. +Qed. + +Lemma size_positive (b:bblock): size b > 0. +Proof. + unfold size. destruct b as [hd bdy ex cor]. simpl. + destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega). + inversion cor; contradict H; simpl; auto. +Qed. + + +Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma no_header_size: + forall bb, size (no_header bb) = size bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. +Qed. + +Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. +Next Obligation. + destruct bb; simpl. assumption. +Defined. + +Lemma stick_header_size: + forall h bb, size (stick_header h bb) = size bb. +Proof. + intros. destruct bb. unfold stick_header. simpl. reflexivity. +Qed. + +Lemma stick_header_no_header: + forall bb, stick_header (header bb) (no_header bb) = bb. +Proof. + intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. +Qed. + + + + +(** * Sequential Semantics of basic blocks *) Section RELSEM. (** Execution of arith instructions *) Variable ge: genv. - +(* TODO: delete this or define it as [parexec_arith_instr ge ai rs rs] *) Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := match ai with | PArithR n d => rs#d <- (arith_eval_r ge n) @@ -68,7 +289,7 @@ Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := (** Auxiliaries for memory accesses *) - +(* TODO: delete this or define it as [parexec_load_offset ge chunk rs rs m m d a ofs] *) Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := match (eval_offset ge ofs) with | OK ptr => match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with @@ -78,12 +299,14 @@ Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ir | _ => Stuck end. +(* TODO: delete this or define it as [parexec_load_reg ge chunk rs rs m m d a ro] *) Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := match Mem.loadv chunk m (Val.addl (rs a) (rs ro)) with | None => Stuck | Some v => Next (rs#d <- v) m end. +(* TODO: delete this as define it as ... *) Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := match (eval_offset ge ofs) with | OK ptr => match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with @@ -93,6 +316,7 @@ Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: i | _ => Stuck end. +(* TODO: delete this as define it as ... *) Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := match Mem.storev chunk m (Val.addl (rs a) (rs ro)) (rs s) with | None => Stuck @@ -103,6 +327,7 @@ Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: i (** * basic instructions *) +(* TODO: define this [parexec_basic_instr ge bi rs rs m m] *) Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := match bi with | PArith ai => Next (exec_arith_instr ai rs) m @@ -157,12 +382,9 @@ Fixpoint exec_body (body: list basic) (rs: regset) (m: mem): outcome := end end. +(** * control-flow instructions *) - -(** Position corresponding to a label *) - - - +(* TODO: delete this or define it as [par_goto_label ge f lbl rs rs m] *) Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome := match label_pos lbl 0 (fn_blocks f) with | None => Stuck @@ -173,11 +395,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) : outcome end end. -(** Evaluating a branch - -Warning: in m PC is assumed to be already pointing on the next instruction ! - -*) +(* TODO: delete this or define it as [par_eval_branch ge f l rs rs m res] *) Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: option bool) : outcome := match res with | Some true => goto_label f l rs m @@ -185,23 +403,7 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti | None => Stuck end. - -(** Execution of a single control-flow instruction [i] in initial state [rs] and - [m]. Return updated state. - - As above: PC is assumed to be incremented on the next block before the control-flow instruction - - For instructions that correspond tobuiltin - actual RISC-V instructions, the cases are straightforward - transliterations of the informal descriptions given in the RISC-V - user-mode specification. For pseudo-instructions, refer to the - informal descriptions given above. - - Note that we set to [Vundef] the registers used as temporaries by - the expansions of the pseudo-instructions, so that the RISC-V code - we generate cannot use those registers to hold values that must - survive the execution of the pseudo-instruction. *) - +(* TODO: delete this or define it as [parexec_control ge f oc rs rs m] *) Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) : outcome := match oc with | Some ic => @@ -252,32 +454,30 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) | None => Next rs m end. +(* TODO: change [exec_bblock] for a definition like this one: + +Definition exec_exit (f: function) ext size_b (rs: regset) (m: mem) + := parexec_exit ge f ext size_b rs rs m. + Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome := match exec_body (body b) rs0 m with - | Next rs' m' => - let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m' + | Next rs' m' => exec_exit f (exit b) (Ptrofs.repr (size b)) rs' m' | Stuck => Stuck end. -(** Translation of the LTL/Linear/Mach view of machine registers to - the RISC-V view. Note that no LTL register maps to [X31]. This - register is reserved as temporary, to be used by the generated RV32G - code. *) - - - - +*) +Definition exec_bblock (f: function) (b: bblock) (rs0: regset) (m: mem) : outcome := + match exec_body (body b) rs0 m with + | Next rs' m' => + let rs1 := nextblock b rs' in exec_control f (exit b) rs1 m' + | Stuck => Stuck + end. (** Execution of the instruction at [rs PC]. *) -(** TODO - * For now, we consider a builtin is alone in a basic block. - * Perhaps there is a way to avoid that ? - *) - Inductive step: state -> trace -> state -> Prop := | exec_step_internal: forall b ofs f bi rs m rs' m', @@ -318,68 +518,6 @@ End RELSEM. Definition semantics (p: program) := Semantics step (initial_state p) final_state (Genv.globalenv p). -(* Useless - -Remark extcall_arguments_determ: - forall rs m sg args1 args2, - extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. -Proof. - intros until m. - assert (A: forall l v1 v2, - extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2). - { intros. inv H; inv H0; congruence. } - assert (B: forall p v1 v2, - extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). - { intros. inv H; inv H0. - eapply A; eauto. - f_equal; eapply A; eauto. } - assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> - forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2). - { - induction 1; intros vl2 EA; inv EA. - auto. - f_equal; eauto. } - intros. eapply C; eauto. -Qed. - -Lemma semantics_determinate: forall p, determinate (semantics p). -Proof. -Ltac Equalities := - match goal with - | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => - rewrite H1 in H2; inv H2; Equalities - | _ => idtac - end. - intros; constructor; simpl; intros. -- (* determ *) - inv H; inv H0; Equalities. - + split. constructor. auto. - + unfold exec_bblock in H4. destruct (exec_body _ _ _ _); try discriminate. - rewrite H9 in H4. discriminate. - + unfold exec_bblock in H13. destruct (exec_body _ _ _ _); try discriminate. - rewrite H4 in H13. discriminate. - + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H6. eexact H13. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. - + assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. - exploit external_call_determ. eexact H3. eexact H8. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. -- (* trace length *) - red; intros. inv H; simpl. - omega. - eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. -- (* initial states *) - inv H; inv H0. f_equal. congruence. -- (* final no step *) - assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs). - { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. } - inv H. unfold Vzero in H0. red; intros; red; intros. - inv H; rewrite H0 in *; eelim NOTNULL; eauto. -- (* final states *) - inv H; inv H0. congruence. -Qed. -*) Definition data_preg (r: preg) : bool := match r with @@ -390,65 +528,3 @@ Definition data_preg (r: preg) : bool := | PC => false end. -(** Determinacy of the [Asm] semantics. *) - -(* Useless. - -Remark extcall_arguments_determ: - forall rs m sg args1 args2, - extcall_arguments rs m sg args1 -> extcall_arguments rs m sg args2 -> args1 = args2. -Proof. - intros until m. - assert (A: forall l v1 v2, - extcall_arg rs m l v1 -> extcall_arg rs m l v2 -> v1 = v2). - { intros. inv H; inv H0; congruence. } - assert (B: forall p v1 v2, - extcall_arg_pair rs m p v1 -> extcall_arg_pair rs m p v2 -> v1 = v2). - { intros. inv H; inv H0. - eapply A; eauto. - f_equal; eapply A; eauto. } - assert (C: forall ll vl1, list_forall2 (extcall_arg_pair rs m) ll vl1 -> - forall vl2, list_forall2 (extcall_arg_pair rs m) ll vl2 -> vl1 = vl2). - { - induction 1; intros vl2 EA; inv EA. - auto. - f_equal; eauto. } - intros. eapply C; eauto. -Qed. - -Lemma semantics_determinate: forall p, determinate (semantics p). -Proof. -Ltac Equalities := - match goal with - | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => - rewrite H1 in H2; inv H2; Equalities - | _ => idtac - end. - intros; constructor; simpl; intros. -- (* determ *) - inv H; inv H0; Equalities. - split. constructor. auto. - discriminate. - discriminate. - assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0. - exploit external_call_determ. eexact H5. eexact H11. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. - assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0. - exploit external_call_determ. eexact H3. eexact H8. intros [A B]. - split. auto. intros. destruct B; auto. subst. auto. -- (* trace length *) - red; intros. inv H; simpl. - omega. - eapply external_call_trace_length; eauto. - eapply external_call_trace_length; eauto. -- (* initial states *) - inv H; inv H0. f_equal. congruence. -- (* final no step *) - assert (NOTNULL: forall b ofs, Vnullptr <> Vptr b ofs). - { intros; unfold Vnullptr; destruct Archi.ptr64; congruence. } - inv H. unfold Vzero in H0. red; intros; red; intros. - inv H; rewrite H0 in *; eelim NOTNULL; eauto. -- (* final states *) - inv H; inv H0. congruence. -Qed. -*) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 32e5e5bb..01f5ca20 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -910,7 +910,7 @@ Theorem forward_simu_control_gen ge fn ex b rs m s: Proof. intros. destruct ex; simpl; inv H0. - destruct c; destruct i; simpl; rewrite (H2 PC); auto. - all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock; Simpl). + all: try (eexists; split; try split; Simpl; intros rr; destruct rr; unfold nextblock, incrPC; Simpl). (* Pjumptable *) + Simpl. rewrite (H2 r). destruct (rs r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. @@ -922,18 +922,18 @@ Proof. (* Pj_l *) + Simpl. unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. - unfold nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. + unfold nextblock, incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. (* Pcb *) + Simpl. destruct (cmp_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps. ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b0. - +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl. + +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. ++ destruct (Val.cmpl_bool _ _ _); simpl; auto. destruct b0. - +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl. + +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. @@ -941,12 +941,12 @@ Proof. (* Pcbu *) + Simpl. destruct (cmpu_for_btest _); simpl; auto. rewrite (H2 r). destruct o; simpl; auto. destruct i; unfold eval_branch; unfold eval_branch_deps. ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b0. - +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl. + +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b0. - +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock; Simpl. + +++ unfold goto_label; unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. unfold nextblock, incrPC; Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ simpl. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. @@ -1813,31 +1813,31 @@ Theorem forward_simu_par_control_gen 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 -> - match_outcome (parexec_control ge fn ex (par_nextblock (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). + match_outcome (parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw) (inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr). Proof. intros GENV MSR MSW. simpl in *. inv MSR. inv MSW. destruct ex. - destruct c; destruct i; try discriminate; simpl. - all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold par_nextblock; Simpl). + all: try (rewrite (H0 PC); eexists; split; try split; Simpl; intros rr; destruct rr; unfold incrPC; Simpl). (* Pjumptable *) - + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold par_nextblock. Simpl. + + rewrite (H0 PC). Simpl. rewrite (H0 r). unfold incrPC. Simpl. destruct (rsr r); simpl; auto. destruct (list_nth_z _ _); simpl; auto. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. destruct (preg_eq g GPR62). rewrite e. Simpl. destruct (preg_eq g GPR63). rewrite e. Simpl. Simpl. (* Pj_l *) + rewrite (H0 PC). Simpl. unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. - unfold par_nextblock. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. - eexists; split; try split; Simpl. intros rr; destruct rr; unfold par_nextblock; Simpl. + unfold incrPC. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. + eexists; split; try split; Simpl. intros rr; destruct rr; unfold incrPC; Simpl. (* Pcb *) + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmp_for_btest _); simpl; auto. destruct o; simpl; auto. - unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. ++ destruct (Val.cmp_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. @@ -1851,7 +1851,7 @@ Proof. (* Pcbu *) + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. - unfold par_eval_branch. unfold eval_branch_deps. unfold par_nextblock. Simpl. destruct i. + unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. @@ -1864,14 +1864,14 @@ Proof. +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - simpl in *. rewrite (H0 PC). eexists; split; try split; Simpl. - intros rr; destruct rr; unfold par_nextblock; Simpl. + intros rr; destruct rr; unfold incrPC; Simpl. Qed. 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) rsw mw = Next rs' m' -> + parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Next rs' m' -> exists s', inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = Some s' /\ match_states (State rs' m') s'. @@ -1885,7 +1885,7 @@ 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) rsw mw = Stuck -> + parexec_control ge fn ex (incrPC (Ptrofs.repr sz) rsr) rsw mw = Stuck -> inst_prun Ge (trans_pcincr sz (trans_exit ex)) sw sr sr = None. Proof. intros. exploit forward_simu_par_control_gen. 3: eapply H1. 2: eapply H0. all: eauto. diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v index a071a9f8..d93afba5 100644 --- a/mppa_k1c/Asmblockgenproof.v +++ b/mppa_k1c/Asmblockgenproof.v @@ -839,7 +839,7 @@ Proof. exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs2'). - { subst. unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. } + { subst. unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. eauto. } eauto. intros (tc' & rs' & GOTO & AT2 & INV). @@ -847,7 +847,7 @@ Proof. rewrite H6. simpl extract_basic. simpl. eauto. rewrite H7. simpl extract_ctl. simpl. rewrite <- Heqrs2'. eauto. econstructor; eauto. - rewrite Heqrs2' in INV. unfold nextblock in INV. + rewrite Heqrs2' in INV. unfold nextblock, incrPC in INV. eapply agree_exten; eauto with asmgen. assert (forall r : preg, r <> PC -> rs' r = rs2 r). { intros. destruct r. @@ -886,7 +886,7 @@ Proof. econstructor; eauto. eapply agree_exten with rs2; eauto with asmgen. { intros. destruct r; try destruct g; try discriminate. - all: rewrite Hrs3; try discriminate; unfold nextblock; Simpl. } + all: rewrite Hrs3; try discriminate; unfold nextblock, incrPC; Simpl. } intros. discriminate. * (* MBcond false *) @@ -912,10 +912,10 @@ Proof. rewrite H7. rewrite <- BTC. rewrite extract_ctl_basics_to_code. simpl extract_ctl. rewrite B. eauto. econstructor; eauto. - unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. eapply agree_exten with rs2; eauto with asmgen. { intros. destruct r; try destruct g; try discriminate. - all: rewrite <- C; try discriminate; unfold nextblock; Simpl. } + all: rewrite <- C; try discriminate; unfold nextblock, incrPC; Simpl. } intros. discriminate. + (* MBjumptable *) destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. @@ -926,7 +926,7 @@ Proof. generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV. assert (f1 = f) by congruence. subst f1. exploit find_label_goto_label. 4: eapply H16. 1-2: eauto. instantiate (2 := (nextblock tbb rs2) # GPR62 <- Vundef # GPR63 <- Vundef). - unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn. intros [tc' [rs' [A [B C]]]]. @@ -959,7 +959,7 @@ Proof. rewrite H6. simpl extract_basic. eauto. rewrite H7. simpl extract_ctl. simpl. reflexivity. econstructor; eauto. - unfold nextblock. repeat apply agree_set_other; auto with asmgen. + unfold nextblock, incrPC. repeat apply agree_set_other; auto with asmgen. - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. inv Hcur. (* exploit transl_blocks_distrib; eauto. (* rewrite <- H2. discriminate. *) @@ -969,7 +969,7 @@ Proof. monadInv TBC. monadInv TIC. simpl in *. rewrite H5. rewrite H6. simpl. repeat eexists. econstructor. 4: instantiate (3 := false). all:eauto. - unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite PCeq. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. assert (f = f0) by congruence. subst f0. econstructor; eauto. @@ -1398,7 +1398,7 @@ Proof. eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto. unfold exec_bblock. simpl. eauto. econstructor. eauto. eauto. eauto. - unfold nextblock. Simpl. unfold Val.offset_ptr. rewrite <- H. + unfold nextblock, incrPC. Simpl. unfold Val.offset_ptr. rewrite <- H. assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. econstructor; eauto. @@ -1581,7 +1581,7 @@ Proof. eauto. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x0). - unfold nextblock. rewrite Pregmap.gss. + unfold nextblock, incrPC. rewrite Pregmap.gss. rewrite set_res_other. rewrite undef_regs_other_2. rewrite Pregmap.gso by congruence. rewrite <- H. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 5ccea246..a43b228e 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -745,7 +745,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. (*assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S. { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }*) auto; @@ -772,7 +772,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0. auto. - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero); @@ -821,7 +821,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0; auto. - (* c = Cne *) @@ -846,7 +846,7 @@ Proof. * constructor. * split; auto. simpl. intros. assert (rs r1 = (nextblock tbb rs) r1). - unfold nextblock. Simpl. rewrite H1 in H0. + unfold nextblock, incrPC. Simpl. rewrite H1 in H0. auto; unfold eval_branch. rewrite H0; auto. - (* c = Clt *) contradict H; unfold select_compl; destruct (Int64.eq n Int64.zero); @@ -903,7 +903,7 @@ Proof. * constructor. * split; auto. assert (rs x = (nextblock tbb rs) x). - unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0. + unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. + exploit (loadimm32_correct RTMP n); eauto. intros (rs' & A & B & C). @@ -966,7 +966,7 @@ Proof. * constructor. * split; auto. assert (rs x = (nextblock tbb rs) x). - unfold nextblock. Simpl. rewrite H0 in EVAL'. clear H0. + unfold nextblock, incrPC. Simpl. rewrite H0 in EVAL'. clear H0. destruct c0; simpl; auto; unfold eval_branch; rewrite <- H; rewrite EVAL'; auto. + exploit (loadimm64_correct RTMP n); eauto. intros (rs' & A & B & C). diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index d56a7a84..6c18ac32 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -15,7 +15,9 @@ (* *) (* *********************************************************************) -(** Abstract syntax and semantics for K1c assembly language. *) +(** Abstract syntax and semantics for VLIW semantics of K1c assembly language. *) + +(* FIXME: develop/fix the comments in this file *) Require Import Coqlib. Require Import Maps. @@ -35,6 +37,12 @@ Require Import Sorting.Permutation. (** * Abstract syntax *) +(** A K1c program is syntactically given as a list of functions. + Each function is associated to a list of bundles of type [bblock] below. + Hence, syntactically, we view each bundle as a basic block: + this view induces our sequential semantics of bundles defined in [Asmblock]. +*) + (** General Purpose registers. *) @@ -481,21 +489,7 @@ Coercion PExpand: ex_instruction >-> control. Coercion PCtlFlow: cf_instruction >-> control. -(** * Definition of a bblock *) - -Ltac exploreInst := - repeat match goal with - | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var - | [ H : OK _ = OK _ |- _ ] => monadInv H - | [ |- context[if ?b then _ else _] ] => destruct b - | [ |- context[match ?m with | _ => _ end] ] => destruct m - | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m - | [ H : bind _ _ = OK _ |- _ ] => monadInv H - | [ H : Error _ = OK _ |- _ ] => inversion H - end. - -Definition non_empty_bblock (body: list basic) (exit: option control): Prop - := body <> nil \/ exit <> None. +(** * Definition of a bblock (ie a bundle) *) Definition non_empty_body (body: list basic): bool := match body with @@ -511,23 +505,11 @@ Definition non_empty_exit (exit: option control): bool := Definition non_empty_bblockb (body: list basic) (exit: option control): bool := non_empty_body body || non_empty_exit exit. -Lemma non_empty_bblock_refl: - forall body exit, - non_empty_bblock body exit <-> - Is_true (non_empty_bblockb body exit). -Proof. - intros. split. - - destruct body; destruct exit. - all: simpl; auto. intros. inversion H; contradiction. - - destruct body; destruct exit. - all: simpl; auto. - all: intros; try (right; discriminate); try (left; discriminate). - contradiction. -Qed. - -Definition builtin_alone (body: list basic) (exit: option control) := forall ef args res, - exit = Some (PExpand (Pbuiltin ef args res)) -> body = nil. +(** TODO + * For now, we consider a builtin is alone in a bundle (and a basic block). + * Is there a way to avoid that ? + *) Definition builtin_aloneb (body: list basic) (exit: option control) := match exit with | Some (PExpand (Pbuiltin _ _ _)) => @@ -538,41 +520,9 @@ Definition builtin_aloneb (body: list basic) (exit: option control) := | _ => true end. -Lemma builtin_alone_refl: - forall body exit, - builtin_alone body exit <-> Is_true (builtin_aloneb body exit). -Proof. - intros. split. - - destruct body; destruct exit. - all: simpl; auto. - all: exploreInst; simpl; auto. - unfold builtin_alone. intros. assert (Some (Pbuiltin e l b0) = Some (Pbuiltin e l b0)); auto. - assert (b :: body = nil). eapply H; eauto. discriminate. - - destruct body; destruct exit. - all: simpl; auto; try constructor. - + exploreInst; try discriminate. - simpl. contradiction. - + intros. discriminate. -Qed. - Definition wf_bblockb (body: list basic) (exit: option control) := (non_empty_bblockb body exit) && (builtin_aloneb body exit). -Definition wf_bblock (body: list basic) (exit: option control) := - non_empty_bblock body exit /\ builtin_alone body exit. - -Lemma wf_bblock_refl: - forall body exit, - wf_bblock body exit <-> Is_true (wf_bblockb body exit). -Proof. - intros. split. - - intros. inv H. apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. - apply andb_prop_intro. auto. - - intros. apply andb_prop_elim in H. inv H. - apply non_empty_bblock_refl in H0. apply builtin_alone_refl in H1. - unfold wf_bblock. split; auto. -Qed. - (** A bblock is well-formed if he contains at least one instruction, and if there is a builtin then it must be alone in this bblock. *) @@ -583,26 +533,7 @@ Record bblock := mk_bblock { correct: Is_true (wf_bblockb body exit) }. -Ltac bblock_auto_correct := (apply non_empty_bblock_refl; try discriminate; try (left; discriminate); try (right; discriminate)). -(* Local Obligation Tactic := bblock_auto_correct. *) - -Lemma Istrue_proof_irrelevant (b: bool): forall (p1 p2:Is_true b), p1=p2. -Proof. - destruct b; simpl; auto. - - destruct p1, p2; auto. - - destruct p1. -Qed. - -Lemma bblock_equality bb1 bb2: header bb1=header bb2 -> body bb1 = body bb2 -> exit bb1 = exit bb2 -> bb1 = bb2. -Proof. - destruct bb1 as [h1 b1 e1 c1], bb2 as [h2 b2 e2 c2]; simpl. - intros; subst. - rewrite (Istrue_proof_irrelevant _ c1 c2). - auto. -Qed. - - -(* FIXME: redundant with definition in Machblock *) +(* FIXME? redundant with definition in Machblock *) Definition length_opt {A} (o: option A) : nat := match o with | Some o => 1 @@ -614,66 +545,6 @@ Definition length_opt {A} (o: option A) : nat := The result is in Z to be compatible with operations on PC *) Definition size (b:bblock): Z := Z.of_nat (length (body b) + length_opt (exit b)). -(* match (body b, exit b) with - | (nil, None) => 1 - | _ => - end. - *) - -Lemma length_nonil {A: Type} : forall l:(list A), l <> nil -> (length l > 0)%nat. -Proof. - intros. destruct l; try (contradict H; auto; fail). - simpl. omega. -Qed. - -Lemma to_nat_pos : forall z:Z, (Z.to_nat z > 0)%nat -> z > 0. -Proof. - intros. destruct z; auto. - - contradict H. simpl. apply gt_irrefl. - - apply Zgt_pos_0. - - contradict H. simpl. apply gt_irrefl. -Qed. - -Lemma size_positive (b:bblock): size b > 0. -Proof. - unfold size. destruct b as [hd bdy ex cor]. simpl. - destruct ex; destruct bdy; try (apply to_nat_pos; rewrite Nat2Z.id; simpl; omega). - inversion cor; contradict H; simpl; auto. -(* rewrite eq. (* inversion COR. *) (* inversion H. *) - - assert ((length b > 0)%nat). apply length_nonil. auto. - omega. - - destruct e; simpl; try omega. contradict H; simpl; auto. - *)Qed. - - -Program Definition no_header (bb : bblock) := {| header := nil; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Lemma no_header_size: - forall bb, size (no_header bb) = size bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. unfold no_header. simpl. reflexivity. -Qed. - -Program Definition stick_header (h : list label) (bb : bblock) := {| header := h; body := body bb; exit := exit bb |}. -Next Obligation. - destruct bb; simpl. assumption. -Defined. - -Lemma stick_header_size: - forall h bb, size (stick_header h bb) = size bb. -Proof. - intros. destruct bb. unfold stick_header. simpl. reflexivity. -Qed. - -Lemma stick_header_no_header: - forall bb, stick_header (header bb) (no_header bb) = bb. -Proof. - intros. destruct bb as [hd bdy ex COR]. simpl. unfold no_header; unfold stick_header; simpl. reflexivity. -Qed. - Definition bblocks := list bblock. @@ -689,103 +560,6 @@ Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }. Definition fundef := AST.fundef function. Definition program := AST.program fundef unit. -Inductive instruction : Type := - | PBasic (i: basic) - | PControl (i: control) -. - -Coercion PBasic: basic >-> instruction. -Coercion PControl: control >-> instruction. - -Definition code := list instruction. -Definition bcode := list basic. - -Fixpoint basics_to_code (l: list basic) := - match l with - | nil => nil - | bi::l => (PBasic bi)::(basics_to_code l) - end. - -Fixpoint code_to_basics (c: code) := - match c with - | (PBasic i)::c => - match code_to_basics c with - | None => None - | Some l => Some (i::l) - end - | _::c => None - | nil => Some nil - end. - -Lemma code_to_basics_id: forall c, code_to_basics (basics_to_code c) = Some c. -Proof. - intros. induction c as [|i c]; simpl; auto. - rewrite IHc. auto. -Qed. - -Lemma code_to_basics_dist: - forall c c' l l', - code_to_basics c = Some l -> - code_to_basics c' = Some l' -> - code_to_basics (c ++ c') = Some (l ++ l'). -Proof. - induction c as [|i c]; simpl; auto. - - intros. inv H. simpl. auto. - - intros. destruct i; try discriminate. destruct (code_to_basics c) eqn:CTB; try discriminate. - inv H. erewrite IHc; eauto. auto. -Qed. - -(** - Asmblockgen will have to translate a Mach control into a list of instructions of the form - i1 :: i2 :: i3 :: ctl :: nil ; where i1..i3 are basic instructions, ctl is a control instruction - These functions provide way to extract the basic / control instructions -*) - -Fixpoint extract_basic (c: code) := - match c with - | nil => nil - | PBasic i :: c => i :: (extract_basic c) - | PControl i :: c => nil - end. - -Fixpoint extract_ctl (c: code) := - match c with - | nil => None - | PBasic i :: c => extract_ctl c - | PControl i :: nil => Some i - | PControl i :: _ => None (* if the first found control instruction isn't the last *) - end. - -(** * Utility for Asmblockgen *) - -Program Definition bblock_single_inst (i: instruction) := - match i with - | PBasic b => {| header:=nil; body:=(b::nil); exit:=None |} - | PControl ctl => {| header:=nil; body:=nil; exit:=(Some ctl) |} - end. -Next Obligation. - apply wf_bblock_refl. constructor. - right. discriminate. - constructor. -Qed. - -(** This definition is not used anymore *) -(* Program Definition bblock_basic_ctl (c: list basic) (i: option control) := - match i with - | Some i => {| header:=nil; body:=c; exit:=Some i |} - | None => - match c with - | _::_ => {| header:=nil; body:=c; exit:=None |} - | nil => {| header:=nil; body:=Pnop::nil; exit:=None |} - end - end. -Next Obligation. - bblock_auto_correct. -Qed. Next Obligation. - bblock_auto_correct. -Qed. *) - - (** * Operational semantics *) (** The semantics operates over a single mapping from registers @@ -841,6 +615,8 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset := Local Open Scope asm. +(** * Parallel Semantics of bundles *) + Section RELSEM. (** Execution of arith instructions *) @@ -855,10 +631,8 @@ Variable ge: genv. Inductive outcome: Type := | Next (rs:regset) (m:mem) - | Stuck. -(* Arguments outcome: clear implicits. *) - - + | Stuck +. (** ** Arithmetic Expressions (including comparisons) *) @@ -1216,22 +990,18 @@ Definition arith_eval_arrr n v1 v2 v3 := match n with | Pmaddw => Val.add v1 (Val.mul v2 v3) | Pmaddl => Val.addl v1 (Val.mull v2 v3) - end. + end. Definition arith_eval_arri32 n v1 v2 v3 := match n with | Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3)) - end. + end. Definition arith_eval_arri64 n v1 v2 v3 := match n with | Pmaddil => Val.addl v1 (Val.mull v2 (Vlong v3)) - end. + end. -(* TODO: on pourrait mettre ça dans Asmblock pour factoriser le code - en définissant - exec_arith_instr ai rs := parexec_arith_instr ai rs rs -*) Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset := match ai with | PArithR n d => rsw#d <- (arith_eval_r n) @@ -1264,7 +1034,6 @@ Definition eval_offset (ofs: offset) : res ptrofs := (** * load/store *) -(* TODO: factoriser ? *) Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a: ireg) (ofs: offset) := match (eval_offset ofs) with | OK ptr => match Mem.loadv chunk mr (Val.offset_ptr (rsr a) ptr) with @@ -1321,11 +1090,8 @@ Definition store_chunk n := | Pfsd => Mfloat64 end. -(* rem: parexec_store = exec_store *) - (** * basic instructions *) -(* TODO: factoriser ? *) Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) := match bi with | PArith ai => Next (parexec_arith_instr ai rsr rsw) mw @@ -1381,15 +1147,7 @@ Fixpoint parexec_wio_body (body: list basic) (rsr rsw: regset) (mr mw: mem) := end end. -(** Manipulations over the [PC] register: continuing with the next - instruction ([nextblock]) or branching to a label ([goto_label]). *) - -(* TODO: factoriser ? *) -Definition par_nextblock size_b (rs: regset) := - rs#PC <- (Val.offset_ptr rs#PC size_b). - - -(** TODO: redundant w.r.t Machblock *) +(** TODO: redundant w.r.t Machblock ?? *) Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. Proof. apply List.in_dec. @@ -1423,7 +1181,6 @@ Fixpoint label_pos (lbl: label) (pos: Z) (lb: bblocks) {struct lb} : option Z := | b :: lb' => if is_label lbl b then Some pos else label_pos lbl (pos + (size b)) lb' end. -(* TODO: factoriser ? *) Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) := match label_pos lbl 0 (fn_blocks f) with | None => Stuck @@ -1439,7 +1196,7 @@ Definition par_goto_label (f: function) (lbl: label) (rsr rsw: regset) (mw: mem) Warning: in m PC is assumed to be already pointing on the next instruction ! *) -(* TODO: factoriser ? *) + Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) (res: option bool) := match res with | Some true => par_goto_label f l rsr rsw mw @@ -1448,6 +1205,8 @@ Definition par_eval_branch (f: function) (l: label) (rsr rsw: regset) (mw: mem) end. +(* FIXME: comment not up-to-date for parallel semantics *) + (** Execution of a single control-flow instruction [i] in initial state [rs] and [m]. Return updated state. @@ -1514,18 +1273,19 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) end. -Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome := +Definition incrPC size_b (rs: regset) := + rs#PC <- (Val.offset_ptr rs#PC size_b). + +(** parallel execution of the exit instruction of a bundle *) +Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) + := parexec_control f ext (incrPC size_b rsr) rsw mw. + +Definition parexec_wio_bblock_aux f bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome := match parexec_wio_body bdy rsr rsw mr mw with - | Next rsw mw => - let rsr := par_nextblock size_b rsr in - parexec_control f ext rsr rsw mw + | Next rsw mw => parexec_exit f ext size_b rsr rsw mw | Stuck => Stuck end. -(** parallel in-order writes execution of bundles *) -Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := - parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m. - (** non-deterministic (out-of-order writes) parallel execution of bundles *) Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop := exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ @@ -1534,30 +1294,19 @@ Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) ( | Stuck => Stuck end. -Lemma parexec_bblock_write_in_order f b rs m: - parexec_bblock f b rs m (parexec_wio_bblock f b rs m). -Proof. - exists (body b). exists nil. - constructor 1. - - rewrite app_nil_r; auto. - - unfold parexec_wio_bblock. - destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto. -Qed. - (** deterministic parallel (out-of-order writes) execution of bundles *) Definition det_parexec (f: function) (bundle: bblock) (rs: regset) (m: mem) rs' m': Prop := forall o, parexec_bblock f bundle rs m o -> o = Next rs' m'. -Local Hint Resolve parexec_bblock_write_in_order. +(* FIXME: comment not up-to-date *) +(** Translation of the LTL/Linear/Mach view of machine registers to + the RISC-V view. Note that no LTL register maps to [X31]. This + register is reserved as temporary, to be used by the generated RV32G + code. *) -Lemma det_parexec_write_in_order f b rs m rs' m': - det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'. -Proof. - unfold det_parexec; auto. -Qed. - (* FIXME - R16 and R32 are excluded *) +(* FIXME - R16 and R32 are excluded *) Definition preg_of (r: mreg) : preg := match r with | R0 => GPR0 | R1 => GPR1 | R2 => GPR2 | R3 => GPR3 | R4 => GPR4 @@ -1584,7 +1333,7 @@ Definition undef_caller_save_regs (rs: regset) : regset := then rs r else Vundef. - +(* FIXME: comment not up-to-date *) (** Extract the values of the arguments of an external call. We exploit the calling conventions from module [Conventions], except that we use RISC-V registers instead of locations. *) @@ -1615,11 +1364,6 @@ Definition extcall_arguments Definition loc_external_result (sg: signature) : rpair preg := map_rpair preg_of (loc_result sg). -(** Manipulations over the [PC] register: continuing with the next - instruction ([nextblock]) or branching to a label ([goto_label]). *) - -Definition nextblock (b:bblock) (rs: regset) := - rs#PC <- (Val.offset_ptr rs#PC (Ptrofs.repr (size b))). (** Looking up bblocks in a code sequence by position. *) Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := @@ -1635,6 +1379,8 @@ Fixpoint find_bblock (pos: Z) (lb: bblocks) {struct lb} : option bblock := Inductive state: Type := | State: regset -> mem -> state. +Definition nextblock (b:bblock) (rs: regset) := + incrPC (Ptrofs.repr (size b)) rs. Inductive step: state -> trace -> state -> Prop := | exec_step_internal: @@ -1667,6 +1413,31 @@ Inductive step: state -> trace -> state -> Prop := step (State rs m) t (State rs' m') . + +(** parallel in-order writes execution of bundles *) +Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome := + parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m. + + +Lemma parexec_bblock_write_in_order f b rs m: + parexec_bblock f b rs m (parexec_wio_bblock f b rs m). +Proof. + exists (body b). exists nil. + constructor 1. + - rewrite app_nil_r; auto. + - unfold parexec_wio_bblock. + destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto. +Qed. + + +Local Hint Resolve parexec_bblock_write_in_order. + +Lemma det_parexec_write_in_order f b rs m rs' m': + det_parexec f b rs m rs' m' -> parexec_wio_bblock f b rs m = Next rs' m'. +Proof. + unfold det_parexec; auto. +Qed. + End RELSEM. (** Execution of whole programs. *) diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 6e2539e3..8c68deea 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -1,4 +1,5 @@ open Asmvliw +open Asmblock open Printf open Camlcoq open InstructionScheduler diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 599a4024..f7ada92b 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -226,7 +226,7 @@ Proof. repeat eexists. unfold exec_bblock. rewrite EXEB1. rewrite EXA. simpl. eauto. exploit exec_body_pc. eapply EXEB1. intros. rewrite <- H. auto. - unfold exec_bblock. unfold nextblock. erewrite exec_body_pc_var; eauto. + unfold exec_bblock. unfold nextblock, incrPC. erewrite exec_body_pc_var; eauto. rewrite <- H1. unfold nextblock in EXEB. rewrite regset_double_set_id. assert (size bb = size a + size b). { unfold size. rewrite H0. rewrite H1. rewrite app_length. rewrite EXA. simpl. rewrite Nat.add_0_r. @@ -234,8 +234,8 @@ Proof. clear EXA H0 H1. rewrite H in EXEB. assert (rs1 PC = rs0 PC). { apply exec_body_pc in EXEB2. auto. } rewrite H0. rewrite <- pc_set_add; auto. - exploit AB.size_positive. instantiate (1 := a). intro. omega. - exploit AB.size_positive. instantiate (1 := b). intro. omega. + exploit size_positive. instantiate (1 := a). intro. omega. + exploit size_positive. instantiate (1 := b). intro. omega. Qed. Lemma concat_all_exec_bblock (ge: Genv.t fundef unit) (f: function) : @@ -731,9 +731,9 @@ Proof. destruct bb as [h bdy ext H]; simpl. intros; subst. destruct i. generalize H. - rewrite <- AB.wf_bblock_refl in H. + rewrite <- wf_bblock_refl in H. destruct H as [H H0]. - unfold AB.builtin_alone in H0. erewrite H0; eauto. + unfold builtin_alone in H0. erewrite H0; eauto. Qed. Local Hint Resolve verified_schedule_nob_checks_alls_bundles. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index 8a83521c..fa920a8c 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -1006,7 +1006,7 @@ Lemma exec_straight_through_singleinst: Proof. intros. subst. constructor 1. unfold exec_bblock. simpl body. erewrite exec_straight_body; eauto. simpl. auto. - simpl; auto. unfold nextblock; simpl. Simpl. erewrite exec_straight_pc; eauto. + simpl; auto. unfold nextblock, incrPC; simpl. Simpl. erewrite exec_straight_pc; eauto. Qed. (** The following lemmas show that straight-line executions -- cgit