From c3034c18bff34350a7c0d386cd01651622912eb6 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Feb 2019 14:58:59 +0100 Subject: Proof of transf_blocks_verified --- mppa_k1c/PostpassSchedulingproof.v | 55 +++++++++++++++++++++++++++++++------- 1 file changed, 46 insertions(+), 9 deletions(-) diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index c95a8917..a1d7b977 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -113,6 +113,11 @@ Axiom verified_schedule_correct: concat_all lbb = OK tbb /\ bblock_equiv ge f bb tbb. +Axiom verified_schedule_size: + forall bb lbb, + verified_schedule bb = OK lbb -> + size bb = size_blocks lbb. + Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil). Remark builtin_body_nil: @@ -468,21 +473,53 @@ Proof. Qed. Lemma tail_find_bblock: - forall f ofs bb, - find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb -> - exists c, code_tail (Ptrofs.unsigned ofs) (fn_blocks f) (bb::c). + forall lbb pos bb, + find_bblock pos lbb = Some bb -> + exists c, code_tail pos lbb (bb::c). Proof. -Admitted. + induction lbb. + - intros. simpl in H. inv H. + - intros. simpl in H. + destruct (zlt pos 0); try (inv H; fail). + destruct (zeq pos 0). + + inv H. exists lbb. constructor; auto. + + apply IHlbb in H. destruct H as (c & TAIL). exists c. + cutrewrite (pos = pos - size a + size a). apply code_tail_S; auto. + omega. +Qed. + +Lemma code_tail_head_app: + forall l pos c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + size_blocks l) (l++c1) c2. +Proof. + induction l. + - intros. simpl. rewrite Z.add_0_r. auto. + - intros. apply IHl in H. simpl. rewrite (Z.add_comm (size a)). rewrite Z.add_assoc. apply code_tail_S. assumption. +Qed. Lemma transf_blocks_verified: - forall c tc ofs bb c', + forall c tc pos bb c', transf_blocks c = OK tc -> - code_tail (Ptrofs.unsigned ofs) c (bb::c') -> + code_tail pos c (bb::c') -> exists lbb, verified_schedule bb = OK lbb - /\ exists tc', code_tail (Ptrofs.unsigned ofs) tc (lbb ++ tc'). -Proof. -Admitted. + /\ exists tc', code_tail pos tc (lbb ++ tc'). +Proof. + induction c; intros. + - simpl in H. inv H. inv H0. + - inv H0. + + monadInv H. exists (schedule bb). + split; simpl; auto. eexists; eauto. econstructor; eauto. + + unfold transf_blocks in H. fold transf_blocks in H. monadInv H. + exploit IHc; eauto. + intros (lbb & TRANS & tc' & TAIL). + monadInv TRANS. + repeat eexists; eauto. + erewrite verified_schedule_size; eauto. + apply code_tail_head_app. + eauto. +Qed. Lemma transf_find_bblock: forall ofs f bb tf, -- cgit From ae31128c5ca6437d77b29d31fb1441f51a073095 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 1 Feb 2019 17:44:27 +0100 Subject: Encore de la tuyauterie --- mppa_k1c/PostpassSchedulingproof.v | 92 +++++++++++++++++++++++++++++++++++++- 1 file changed, 91 insertions(+), 1 deletion(-) diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index a1d7b977..ad423fb0 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -120,6 +120,11 @@ Axiom verified_schedule_size: Axiom verified_schedule_single_inst: forall bb, size bb = 1 -> verified_schedule bb = OK (bb::nil). +Axiom verified_schedule_header: + forall bb tbb lbb, + verified_schedule bb = OK (tbb :: lbb) -> + header bb = header tbb. + Remark builtin_body_nil: forall bb ef args res, exit bb = Some (PExpand (Pbuiltin ef args res)) -> body bb = nil. Proof. @@ -535,12 +540,97 @@ Proof. eapply transf_blocks_verified; eauto. Qed. +Lemma transf_exec_body: + forall bdy rs m, exec_body ge bdy rs m = exec_body tge bdy rs m. +Proof. +Admitted. + +Lemma symbol_address_preserved: + forall l, Genv.symbol_address ge l Ptrofs.zero = Genv.symbol_address tge l Ptrofs.zero. +Proof. + intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity. +Qed. + +Lemma head_tail {A: Type}: + forall (l: list A) hd, hd::l = hd :: (tail (hd::l)). +Proof. + intros. simpl. auto. +Qed. + +Lemma verified_schedule_not_empty: + forall bb lbb, + verified_schedule bb = OK lbb -> lbb <> nil. +Proof. + intros. apply verified_schedule_size in H. + pose (size_positive bb). assert (size_blocks lbb > 0) by omega. clear H g. + destruct lbb; simpl in *; discriminate. +Qed. + +Lemma verified_schedule_label: + forall bb tbb lbb l, + verified_schedule bb = OK (tbb :: lbb) -> + is_label l bb = is_label l tbb. +Proof. +Admitted. + +Lemma label_pos_head_app: + forall c bb lbb l tc, + verified_schedule bb = OK lbb -> + label_pos l 0 c = label_pos l 0 tc -> + label_pos l 0 (bb :: c) = label_pos l 0 (lbb ++ tc). +Proof. + induction c. + - intros. simpl in H0. destruct lbb. + + apply verified_schedule_not_empty in H. contradiction. + + rewrite (head_tail lbb). simpl tl. + simpl. erewrite verified_schedule_label; eauto. + destruct (is_label l b) eqn:ISLBL; simpl; auto. + (* TODO - finish *) +Admitted. + + +Lemma label_pos_preserved: + forall c tc l, + transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc. +Proof. + induction c. + - intros. simpl in *. inv H. reflexivity. + - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H. eapply IHc in EQ. + eapply label_pos_head_app; eauto. +Qed. + +Lemma label_pos_preserved_blocks: + forall l f tf, + transf_function f = OK tf -> + label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf). +Proof. + intros. monadInv H. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned _); try discriminate. + monadInv EQ0. simpl. eapply label_pos_preserved; eauto. +Qed. + +Lemma transf_exec_control: + forall f tf ex rs m, + transf_function f = OK tf -> + exec_control ge f ex rs m = exec_control tge tf ex rs m. +Proof. + intros. destruct ex; simpl; auto. + assert (ge = Genv.globalenv prog). auto. + assert (tge = Genv.globalenv tprog). auto. + pose symbol_address_preserved. + exploreInst; simpl; auto; try congruence. + - unfold goto_label. erewrite label_pos_preserved_blocks; eauto. +Admitted. + + Lemma transf_exec_bblock: forall f tf bb rs m, transf_function f = OK tf -> exec_bblock ge f bb rs m = exec_bblock tge tf bb rs m. Proof. -Admitted. + intros. unfold exec_bblock. rewrite transf_exec_body. destruct (exec_body _ _ _ _); auto. + eapply transf_exec_control; eauto. +Qed. Lemma transf_step_simu: forall tf b lbb ofs c tbb rs m rs' m', -- cgit