From e9f8fa5f0635f3c1af489bcf084d38f89ea58b13 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 5 May 2021 14:03:04 +0200 Subject: advance in cfg checker --- scheduling/BTL.v | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 138 insertions(+), 1 deletion(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 28941e01..82a54061 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -513,11 +513,148 @@ Proof. Qed. (* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *) -Parameter verify_block: PTree.t node -> RTL.code -> bool -> node -> iblock -> res (option node). +Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := + match ib with + | BF fi => + match fi with + | Bgoto pc => + match dupmap!pc with + | Some _ => OK None + | None => Error (msg "verify_block: incorrect dupmap Bgoto") + end + | _ => + match cfg!pc with + | Some i => Error (msg "TODO") (* TODO *) + | None => Error (msg "verify_block: incorrect cfg BF") + end + end + | Bnop => + match cfg!pc with + | Some (Inop pc') => OK (Some pc') + | _ => Error (msg "verify_block: incorrect cfg Bnop") + end + | Bop op lr r => + match cfg!pc with + | Some (Iop op' lr' r' pc') => + if (eq_operation op op') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bop") + else Error (msg "verify_block: different lr in Bop") + else Error (msg "verify_block: different operations in Bop") + | _ => Error (msg "verify_block: incorrect cfg Bop") + end + | Bload tm m a lr r => + match cfg!pc with + | Some (Iload tm' m' a' lr' r' pc') => + if (trapping_mode_eq tm tm') then + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then + OK (Some pc') + else Error (msg "verify_block: different r in Bload") + else Error (msg "verify_block: different lr in Bload") + else Error (msg "verify_block: different addressing in Bload") + else Error (msg "verify_block: different mchunk in Bload") + else Error (msg "verify_block: different trapping_mode in Bload") + | _ => Error (msg "verify_block: incorrect cfg Bload") + end + | Bstore m a lr r => + match cfg!pc with + | Some (Istore m' a' lr' r' pc') => + if (chunk_eq m m') then + if (eq_addressing a a') then + if (list_eq_dec Pos.eq_dec lr lr') then + if (Pos.eq_dec r r') then OK (Some pc') + else Error (msg "verify_block: different r in Bstore") + else Error (msg "verify_block: different lr in Bstore") + else Error (msg "verify_block: different addressing in Bstore") + else Error (msg "verify_block: different mchunk in Bstore") + | _ => Error (msg "verify_block: incorrect cfg Bstore") + end + | Bseq b1 b2 => + do opc <- verify_block dupmap cfg isfst pc b1; + match opc with + | Some pc' => + verify_block dupmap cfg false pc' b2 + | None => Error (msg "verify_block: None next pc in Bseq (deadcode)") + end + | Bcond c lr bso bnot i => + match cfg!pc with + | Some (Icond c' lr' pcso pcnot i') => + if (list_eq_dec Pos.eq_dec lr lr') then + if (eq_condition c c') then + do opc1 <- verify_block dupmap cfg false pcso bso; + do opc2 <- verify_block dupmap cfg false pcnot bnot; + match opc1, opc2 with + | None, o => OK o + | o, None => OK o + | Some x, Some x' => + if Pos.eq_dec x x' then OK (Some x) + else Error (msg "verify_block: is_join_opt incorrect for Bcond") + end + else Error (msg "verify_block: incompatible conditions in Bcond") + else Error (msg "verify_block: different lr in Bcond") + | _ => Error (msg "verify_block: incorrect cfg Bcond") + end + end. (* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *) Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin, verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin. +Proof. + induction ib; intros; + try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]). + - admit. + - (* Bnop *) + destruct i; inv H. + constructor; assumption. + - (* Bop *) + destruct i; try discriminate. + destruct (eq_operation _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bload *) + destruct i; try discriminate. + destruct (trapping_mode_eq _ _); try discriminate. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bstore *) + destruct i; try discriminate. + destruct (chunk_eq _ _); try discriminate. + destruct (eq_addressing _ _); try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (Pos.eq_dec _ _); try discriminate. inv H. + constructor; assumption. + - (* Bseq *) + monadInv H. + destruct x; try discriminate. + eapply mib_seq_Some. + eapply IHib1; eauto. admit. + (*eapply IHib2; eauto.*) + (*destruct (cfg!pc) eqn:ECFG; try discriminate.*) + (*destruct i; try discriminate.*) + - (* Bcond *) + destruct i; try discriminate. + destruct (list_eq_dec _ _ _); try discriminate. + destruct (eq_condition _ _); try discriminate. + fold (verify_block dupmap cfg false n ib1) in H. + fold (verify_block dupmap cfg false n0 ib2) in H. + monadInv H. + destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate. + + inv EQ2. eapply mib_cond; eauto. + admit. + admit. + admit. + + admit. + + admit. + + admit. Admitted. Local Hint Resolve verify_block_correct: core. -- cgit