From 70f440ee13ff95f67a9886c63061c5fd28d7f613 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 12 May 2022 19:01:07 +0100 Subject: Remove imm_succ from match_block --- src/hls/RTLBlockgenproof.v | 127 ++++++++++----------------------------------- 1 file changed, 27 insertions(+), 100 deletions(-) (limited to 'src') diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 82ac96d..875c582 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -145,22 +145,18 @@ finding is actually done at that higher level already. * Basic Block Instructions *) | match_block_nop b cf pc': - imm_succ pc pc' -> c ! pc = Some (RTL.Inop pc') -> match_block c tc pc' b cf -> match_block c tc pc (RBnop :: b) cf | match_block_op cf b op args dst pc': - imm_succ pc pc' -> c ! pc = Some (RTL.Iop op args dst pc') -> match_block c tc pc' b cf -> match_block c tc pc (RBop None op args dst :: b) cf | match_block_load cf b chunk addr args dst pc': - imm_succ pc pc' -> c ! pc = Some (RTL.Iload chunk addr args dst pc') -> match_block c tc pc' b cf -> match_block c tc pc (RBload None chunk addr args dst :: b) cf | match_block_store cf b chunk addr args src pc': - imm_succ pc pc' -> c ! pc = Some (RTL.Istore chunk addr args src pc') -> match_block c tc pc' b cf -> match_block c tc pc (RBstore None chunk addr args src :: b) cf @@ -222,40 +218,14 @@ matches some sequence of instructions starting at the node that corresponds to the basic block. |*) - Definition match_code' (c: RTL.code) (tc: code) (pc: node) := - forall n1 i, - c ! n1 = Some i -> - exists b, - find_block_spec tc n1 pc /\ tc ! pc = Some b - /\ match_block c tc pc b.(bb_body) b.(bb_exit). - - Definition match_code'' (c: RTL.code) (tc: code) : Prop := - forall i pc pc0 b bb' i' pc', - c ! pc = Some i -> - tc ! pc0 = Some b -> - b.(bb_body) = bb' ++ i' :: nil -> - match_block c tc pc (i' :: nil) b.(bb_exit) -> - In pc' (RTL.successors_instr i) -> - exists b, tc ! pc' = Some b /\ match_block c tc pc' b.(bb_body) b.(bb_exit). - - Definition match_code''' (c: RTL.code) (tc: code) : Prop := - forall i pc pc', - c ! pc = Some i -> - In pc' (RTL.successors_instr i) -> - (exists pc0 b b' bb i', - tc ! pc0 = Some b /\ - tc ! pc' = Some b' /\ match_block c tc pc' b'.(bb_body) b'.(bb_exit) - /\ b.(bb_body) = bb ++ i'::nil /\ match_block c tc pc (i'::nil) b.(bb_exit)) - \/ (exists pc0 b i' bb1 bb2, tc ! pc0 = Some b /\ - imm_succ pc pc' /\ b.(bb_body) = bb1 ++ i' :: bb2 /\ bb2 <> nil - /\ match_block c tc pc (i'::bb2) b.(bb_exit)). - Definition match_code (c: RTL.code) (tc: code) : Prop := forall pc b, tc ! pc = Some b -> match_block c tc pc b.(bb_body) b.(bb_exit). Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := | match_stackframe_init : - forall res f tf sp pc rs (TF: transl_function f = OK tf), + forall res f tf sp pc rs + (TF: transl_function f = OK tf) + (VALID: valid_succ tf.(fn_code) pc), match_stackframe (RTL.Stackframe res f sp pc rs) (Stackframe res tf sp pc rs (PMap.init false)). @@ -385,65 +355,6 @@ whole execution (in one big step) of the basic block. forall A (l: list A) n, hd_error l = Some n -> l = n :: tl l. Proof. induction l; crush. Qed. - Lemma transl_Inop_correct_nj: - forall s f sp pc rs m stk' tf pc1 rs1 m1 b pc', - b <> nil -> - imm_succ pc pc' -> - (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - match_states (Some (RBnop :: b)) (RTL.State s f sp pc rs m) - (State stk' tf sp pc1 rs1 (PMap.init false) m1) -> - exists b' s2', - star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' - /\ ltof _ measure b' (Some (RBnop :: b)) - /\ match_states b' (RTL.State s f sp pc' rs m) s2'. - Proof. - intros * NIL H1 H2 H3. - inv H3. simplify. pose proof CODE as CODE'. - unfold match_code in *. - pose proof (CODE' _ _ H0). - do 3 econstructor. - eapply star_refl. - econstructor. - instantiate (1 := Some b). - unfold ltof; auto. - econstructor; try eassumption. - do 2 econstructor; try eassumption. - inv H3; crush. - eapply star_right; eauto. - eapply RTL.exec_Inop; eauto. auto. - - unfold sem_extrap in *. intros. - eapply BB. econstructor; eauto. - constructor; auto. - auto. - Qed. - - Lemma transl_Inop_correct_j: - forall s f sp pc rs m pc' stk' tf pc1 rs1 m1 x, - (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - match_states (Some (RBnop :: nil)) (RTL.State s f sp pc rs m) - (State stk' tf sp pc1 rs1 (PMap.init false) m1) -> - (fn_code tf) ! pc1 = Some x -> - match_block f.(RTL.fn_code) tf.(fn_code) pc1 (bb_body x) (bb_exit x) -> - RBgoto pc' = bb_exit x -> - (exists b' : RTLBlockInstr.bblock, - (fn_code tf) ! pc' = Some b' - /\ match_block (RTL.fn_code f) tf.(fn_code) pc' (bb_body b') (bb_exit b')) -> - exists b' s2', plus step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' - /\ match_states b' (RTL.State s f sp pc' rs m) s2'. - Proof. - intros * H H0 H1 H4 H5 H8. - inv H0. simplify. - do 3 econstructor. apply plus_one. econstructor. - eassumption. eapply BB; [econstructor; constructor | eassumption]. - setoid_rewrite <- H5. econstructor. - - econstructor. eassumption. eassumption. eauto. eassumption. - eapply star_refl. - unfold sem_extrap. intros. setoid_rewrite H8 in H3. - crush. - Qed. - Definition imm_succ_dec pc pc' : {imm_succ pc pc'} + {~ imm_succ pc pc'}. Proof. unfold imm_succ. pose proof peq. @@ -489,13 +400,30 @@ whole execution (in one big step) of the basic block. inversion 1; subst; simplify. unfold match_code in *. match goal with H: match_block _ _ _ _ _ |- _ => inv H end; simplify. - { apply sim_star. eapply transl_Inop_correct_nj; eauto. - eapply match_block_not_nil; eassumption. + { apply sim_star. + do 3 econstructor. eapply star_refl. constructor. + instantiate (1 := Some b); unfold ltof; auto. + + constructor; try eassumption. econstructor; eauto. + eapply star_right; eauto. + eapply RTL.exec_Inop; eauto. auto. + + unfold sem_extrap in *. intros. + eapply BB. econstructor; eauto. + econstructor; eauto. auto. } - { apply sim_plus. eapply transl_Inop_correct_j; eauto. - assert (X: In pc' (RTL.successors_instr (RTL.Inop pc'))) by crush. - unfold valid_succ in H6; simplify. pose proof (CODE _ _ H3). - eauto. + { apply sim_plus. + inv H0. simplify. + unfold valid_succ in *; simplify. + do 3 econstructor. apply plus_one. econstructor. + eassumption. eapply BB; [| eassumption ]. + econstructor; econstructor; eauto. + setoid_rewrite <- H1. econstructor. + + econstructor; try eassumption. eauto. + eapply star_refl. + unfold sem_extrap. intros. setoid_rewrite H7 in H0. + crush. } Qed. @@ -533,13 +461,12 @@ whole execution (in one big step) of the basic block. {| is_rs := rs1; is_ps := PMap.init false; is_mem := m1 |} (RBop None op args res :: b) -> (fn_code tf) ! pc1 = Some x -> match_block (RTL.fn_code f) (fn_code tf) pc' b (bb_exit x) -> - imm_succ pc pc' -> exists b' s2', star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' /\ ltof _ measure b' (Some (RBop None op args res :: b)) /\ match_states b' (RTL.State s f sp pc' rs # res <- v m) s2'. Proof. - intros * IOP EVAL TR MATCHB STK STAR BB INCODE MATCHB2 IMSUCC. + intros * IOP EVAL TR MATCHB STK STAR BB INCODE MATCHB2. do 3 econstructor. eapply star_refl. constructor. instantiate (1 := Some b); unfold ltof; auto. -- cgit