From 601998970909bd4343452472e9803f720c422b88 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 9 May 2022 11:32:04 +0100 Subject: Change the specification of the RTLBlockgenproof --- src/hls/RTLBlockgenproof.v | 76 +++++++++++++++++++++++++++------------------- 1 file changed, 45 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 6e4138b..7b80b68 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -134,45 +134,49 @@ finding is actually done at that higher level already. tc ! pc' = Some (mk_bblock bb cf) -> match_bblock tc pc pc' (list_drop (offset pc pc') bb).*) - Definition imm_succ (pc pc': node) : Prop := pc' = Pos.succ pc. + Definition imm_succ (pc pc': node) : Prop := pc' = Pos.pred pc. Inductive match_block (c: RTL.code) (pc: node): bb -> cf_instr -> Prop := (* * Basic Block Instructions *) - | match_block_nop b cf: - c ! pc = Some (RTL.Inop (Pos.pred pc)) -> - match_block c (Pos.pred pc) b cf -> + | match_block_nop b cf pc': + imm_succ pc pc' -> + c ! pc = Some (RTL.Inop pc') -> + match_block c pc' b cf -> match_block c pc (RBnop :: b) cf - | match_block_op cf b op args dst: - c ! pc = Some (RTL.Iop op args dst (Pos.pred pc)) -> - match_block c (Pos.pred pc) 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 pc' b cf -> match_block c pc (RBop None op args dst :: b) cf - | match_block_load cf b chunk addr args dst: - c ! pc = Some (RTL.Iload chunk addr args dst (Pos.pred pc)) -> - match_block c (Pos.pred pc) 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 pc' b cf -> match_block c pc (RBload None chunk addr args dst :: b) cf - | match_block_store cf b chunk addr args src: - c ! pc = Some (RTL.Istore chunk addr args src (Pos.pred pc)) -> - match_block c (Pos.pred pc) 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 pc' b cf -> match_block c pc (RBstore None chunk addr args src :: b) cf (* * Control flow instructions using goto *) | match_block_goto pc': - pc' <> Pos.pred pc -> + ~ imm_succ pc pc' -> c ! pc = Some (RTL.Inop pc') -> match_block c pc (RBnop :: nil) (RBgoto pc') | match_block_op_cf pc' op args dst: - pc' <> Pos.pred pc -> + ~ imm_succ pc pc' -> c ! pc = Some (RTL.Iop op args dst pc') -> match_block c pc (RBop None op args dst :: nil) (RBgoto pc') | match_block_load_cf pc' chunk addr args dst: - pc' <> Pos.pred pc -> + ~ imm_succ pc pc' -> c ! pc = Some (RTL.Iload chunk addr args dst pc') -> match_block c pc (RBload None chunk addr args dst :: nil) (RBgoto pc') | match_block_store_cf pc' chunk addr args src: - pc' <> Pos.pred pc -> + ~ imm_succ pc pc' -> c ! pc = Some (RTL.Istore chunk addr args src pc') -> match_block c pc (RBstore None chunk addr args src :: nil) (RBgoto pc') (* @@ -225,7 +229,11 @@ the basic block. c ! pc = Some i -> In pc' (RTL.successors_instr i) -> imm_succ pc pc' -> - exists b, tc ! pc' = Some b /\ match_block c pc b.(bb_body) b.(bb_exit). + exists b, tc ! pc' = Some b. + + Definition match_code3 (c: RTL.code) (tc: code) : Prop := + (forall pc b, tc ! pc = Some b -> match_block c pc b.(bb_body) b.(bb_exit)) + /\ match_code' c tc. Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := | match_stackframe_init : @@ -257,7 +265,7 @@ whole execution (in one big step) of the basic block. | match_state : forall stk stk' f tf sp pc rs m pc0 b rs0 m0 (TF: transl_function f = OK tf) - (CODE: match_code' f.(RTL.fn_code) tf.(fn_code)) + (CODE: match_code3 f.(RTL.fn_code) tf.(fn_code)) (BLOCK: exists b', tf.(fn_code) ! pc0 = Some b' /\ match_block f.(RTL.fn_code) pc b b'.(bb_exit)) (STK: Forall2 match_stackframe stk stk') @@ -345,15 +353,16 @@ whole execution (in one big step) of the basic block. Proof. induction l; crush. Qed. Lemma transl_Inop_correct_nj: - forall s f sp pc rs m stk' tf pc1 rs1 m1 b x, - (RTL.fn_code f) ! pc = Some (RTL.Inop (Pos.pred pc)) -> + forall s f sp pc rs m stk' tf pc1 rs1 m1 b x pc', + 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) -> - (RTL.fn_code f) ! pc = Some (RTL.Inop (Pos.pred pc)) -> - match_block (RTL.fn_code f) (Pos.pred pc) b x -> + (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> + match_block (RTL.fn_code f) pc' b x -> exists b' s2', Smallstep.star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' /\ - match_states b' (RTL.State s f sp (Pos.pred pc) rs m) s2'. + match_states b' (RTL.State s f sp pc' rs m) s2'. Proof. intros s f sp pc rs m H stk' tf pc1 rs1 m1 b H0 x H1 H3. Admitted. @@ -366,7 +375,7 @@ whole execution (in one big step) of the basic block. match_block (RTL.fn_code f) pc1 (bb_body x) (bb_exit x) -> RBgoto pc' = bb_exit x -> (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> - pc' <> Pos.pred pc -> + ~ imm_succ pc pc' -> exists b' s2', Smallstep.star 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'. @@ -387,6 +396,12 @@ whole execution (in one big step) of the basic block. decide equality. Defined. + Lemma imm_succ_refl pc : imm_succ pc (Pos.pred pc). + Proof. unfold imm_succ; auto. Qed. + + Lemma imm_succ_refl2 pc : imm_succ (Pos.succ pc) pc. + Proof. unfold imm_succ; auto using Pos.pred_succ. Qed. + Lemma transl_Inop_correct: forall s f sp pc rs m pc', (RTL.fn_code f) ! pc = Some (RTL.Inop pc') -> @@ -396,14 +411,13 @@ whole execution (in one big step) of the basic block. Proof. intros s f sp pc rs m pc' H. inversion 1; subst; simplify. - unfold match_code' in *. + unfold match_code3 in *. assert (X1: In pc' (RTL.successors_instr (RTL.Inop pc'))) by (crush). destruct (imm_succ_dec pc pc'). - { admit. } - { pose proof (CODE _ _ pc' H X1 n) as X. simplify. - inv H3; crush. admit. - eapply transl_Inop_correct_j; eauto. - eauto using transl_Inop_correct_nj, transl_Inop_correct_j. } + { inv H3; crush. eapply transl_Inop_correct_nj; eauto. } + { pose proof (CODE _ _ H2) as X. + inv H3; crush. + eapply transl_Inop_correct_j; eauto. } Qed. Lemma transl_Iop_correct: -- cgit