From 25595a7b34b70011dcb77aae277ee1cdb8920c60 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 28 May 2021 14:28:56 +0200 Subject: splitting BTL by introducing BTLmatchRTL reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL --- scheduling/BTL.v | 565 +------------------------------------------------------ 1 file changed, 6 insertions(+), 559 deletions(-) (limited to 'scheduling/BTL.v') diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 2c1dda5b..6536addb 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -90,8 +90,6 @@ Coercion BF: final >-> Funclass. - the same trick appears for all "basic" instructions and [Icond]. *) - - Record iblock_info := { entry: iblock; input_regs: Regset.t; (* extra liveness information for BTL functional semantics *) @@ -187,6 +185,8 @@ Section RELSEM. Here, [or] is an optional register that will be assigned after exiting the iblock, but before entering in [pc]: e.g. the register set by a function call before entering in return address. + See [tr_inputs] implementation below. + *) Variable tr_exit: function -> list exit -> option reg -> regset -> regset. @@ -390,14 +390,6 @@ Inductive final_state: state -> int -> Prop := | final_state_intro: forall r m, final_state (Returnstate nil (Vint r) m) r. -(** The "raw" CFG small-step semantics for a BTL program (e.g. close to RTL semantics) *) - -(* tid = transfer_identity *) -Definition tid (_:function) (_:list exit) (_: option reg) (rs:regset) := rs. - -Definition cfgsem (p: program) := - Semantics (step tid) (initial_state p) final_state (Genv.globalenv p). - (** The full "functional" small-step semantics for a BTL program. at each exit, we only transfer register in "input_regs" (i.e. "alive" registers). *) @@ -633,9 +625,9 @@ Proof. - repeat (rewrite Regmap.gso); auto. Qed. -(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. +(* * Comparing BTL semantics modulo [regs_lessdef]. -We start by extending the previous [equiv_*] stuff for [Val.lessdef]: we need to also compare memories +This extends the previous [equiv_*] stuff for [Val.lessdef]. Here, we need to also compare memories for Mem.extends, because Vundef values are propagated in memory through stores, allocation, etc. *) @@ -721,16 +713,6 @@ Proof. eapply set_reg_lessdef; eauto. intros r2; eauto. Qed. -Local Hint Resolve init_regs_lessdef_preserv: core. - -Lemma tr_inputs_lessdef f rs1 rs2 tbl or r - (REGS: forall r, Val.lessdef rs1#r rs2#r) - :Val.lessdef (tr_inputs f tbl or rs1)#r (tid f tbl or rs2)#r. -Proof. - unfold tid; rewrite tr_inputs_get. - autodestruct. -Qed. -Local Hint Resolve tr_inputs_lessdef: core. Lemma find_function_lessdef ge ros rs1 rs2 fd (FIND: find_function ge ros rs1 = Some fd) @@ -742,547 +724,12 @@ Proof. intros (b & EQ). destruct (REGS r); try congruence. Qed. -Local Hint Resolve find_function_lessdef regs_lessdef_regs: core. - - -Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of - (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of) - rs2 m2 - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS: Mem.extends m1 m2) - : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) - /\ (forall r, Val.lessdef rs1'#r rs2'#r) - /\ (Mem.extends m1' m2'). -Proof. - induction ISTEP; simpl; try_simplify_someHyps. -Admitted. - -Local Hint Constructors final_step list_forall2: core. -Local Hint Unfold regs_lessdef: core. - -Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 - (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1) - (STACKS: list_forall2 lessdef_stackframe stk1 stk2) - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS: Mem.extends m1 m2) - : exists s2, final_step tid ge stk2 f sp rs2 m2 fin t s2 - /\ lessdef_state s1 s2. -Proof. - destruct FSTEP; try (eexists; split; simpl; econstructor; eauto; fail). - - (* return *) - exploit Mem.free_parallel_extends; eauto. - intros (m2' & FREE & MEMS2). - eexists; split; simpl; econstructor; eauto. - destruct or; simpl; auto. - - (* tailcall *) - exploit Mem.free_parallel_extends; eauto. - intros (m2' & FREE & MEMS2). - eexists; split; simpl; econstructor; eauto. - - (* builtin *) - exploit (eval_builtin_args_lessdef (ge:=ge) (e1:=(fun r => rs1 # r)) (fun r => rs2 # r)); eauto. - intros (vl2' & BARGS & VARGS). - exploit external_call_mem_extends; eauto. - intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). - eexists; split; simpl; econstructor; eauto. - intros; apply set_res_lessdef; eauto. - - (* jumptable *) - eexists; split; simpl; econstructor; eauto. - destruct (REGS arg); try congruence. -Qed. - -Lemma fsem2cfgsem_ibstep_simu ge stk1 stk2 f sp rs1 m1 ib t s1 rs2 m2 - (STEP: iblock_step tr_inputs ge stk1 f sp rs1 m1 ib t s1) - (STACKS : list_forall2 lessdef_stackframe stk1 stk2) - (REGS: forall r, Val.lessdef rs1#r rs2#r) - (MEMS : Mem.extends m1 m2) - : exists s2, iblock_step tid ge stk2 f sp rs2 m2 ib t s2 - /\ lessdef_state s1 s2. -Proof. - destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP). - exploit fsem2cfgsem_ibistep_simu; eauto. - intros (rs2' & m2' & ISTEP2 & REGS2 & MEMS2). - rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP REGS MEMS. - exploit fsem2cfgsem_finalstep_simu; eauto. - intros (s2 & FSTEP2 & LESSDEF). clear FSTEP. - unfold iblock_step; eexists; split; eauto. -Qed. - -Local Hint Constructors step: core. - -Lemma fsem2cfgsem_step_simu ge s1 t s1' s2 - (STEP: step tr_inputs ge s1 t s1') - (REGS: lessdef_state s1 s2) - :exists s2' : state, - step tid ge s2 t s2' /\ - lessdef_state s1' s2'. -Proof. - destruct STEP; inv REGS. - - (* iblock *) - intros; exploit fsem2cfgsem_ibstep_simu; eauto. clear STEP. - intros (s2 & STEP2 & REGS2). - eexists; split; eauto. - - (* internal call *) - exploit (Mem.alloc_extends m m2 0 (fn_stacksize f) stk m' 0 (fn_stacksize f)); eauto. - 1-2: lia. - intros (m2' & ALLOC2 & MEMS2). clear ALLOC MEMS. - eexists; split; econstructor; eauto. - - (* external call *) - exploit external_call_mem_extends; eauto. - intros (vres' & m2' & CALL2 & REGS2 & MEMS2 & UNCHANGED). clear EXTCALL MEMS. - eexists; split; econstructor; eauto. - - (* return *) - inversion STACKS as [|d1 d2 d3 d4 STF2 STK2]. subst. - inv STF2. - eexists; split; econstructor; eauto. - intros; eapply set_reg_lessdef; eauto. -Qed. - -Theorem fsem2cfgsem prog: - forward_simulation (fsem prog) (cfgsem prog). -Proof. - eapply forward_simulation_step with lessdef_state; simpl; auto. - - destruct 1; intros; eexists; intuition eauto. econstructor; eauto. - - intros s1 s2 r REGS FINAL; destruct FINAL. - inv REGS; inv STACKS; inv REGS0. - econstructor; eauto. - - intros; eapply fsem2cfgsem_step_simu; eauto. -Qed. - -(** TODO: est-ce qu'il faudrait déplacer ceci dans une librairie du genre "BTLlib" ? *) - -(** Matching BTL and RTL code - -We should be able to define a single verifier able to prove a bisimulation between BTL and RTL code. - -NB 1: the proof of BTL -> RTL (plus simulation) should be much easier than RTL -> BTL (star simulation). - -NB 2: our scheme allows the BTL to duplicate some RTL code. -- in other words: RTL -> BTL allows tail duplication, loop unrolling, etc. Exactly like "Duplicate" on RTL. -- BTL -> RTL allows to "undo" some duplications (e.g. remove duplications that have not enabled interesting optimizations) ! - -Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. - -The [match_*] definitions gives a "relational" specification of the verifier... -*) - -Require Import Errors. - -Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := -(* TODO: it may be simplify the oracle for BTL -> RTL, but may makes the verifier more complex ? - | mfi_goto pc pc': - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bgoto pc) (Inop pc') -*) - | mfi_return or: match_final_inst dupmap (Breturn or) (Ireturn or) - | mfi_call pc pc' s ri lr r: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bcall s ri lr r pc) (Icall s ri lr r pc') - | mfi_tailcall s ri lr: - match_final_inst dupmap (Btailcall s ri lr) (Itailcall s ri lr) - | mfi_builtin pc pc' ef la br: - dupmap!pc = (Some pc') -> match_final_inst dupmap (Bbuiltin ef la br pc) (Ibuiltin ef la br pc') - | mfi_jumptable ln ln' r: - list_forall2 (fun pc pc' => (dupmap!pc = (Some pc'))) ln ln' -> - match_final_inst dupmap (Bjumptable r ln) (Ijumptable r ln') -. - -Inductive is_join_opt {A}: (option A) -> (option A) -> (option A) -> Prop := - | ijo_None_left o: is_join_opt None o o - | ijo_None_right o: is_join_opt o None o - | ijo_Some x: is_join_opt (Some x) (Some x) (Some x) - . - -(* [match_iblock dupmap cfg isfst pc ib opc] means that [ib] match a block in a RTL code starting at [pc], with: - - [isfst] (in "input") indicates that no step in the surrounding block has been executed before entering [pc] - - if [opc] (in "ouput") is [None], this means that all branches of the block ends on a final instruction - - if [opc] is [Some pc'], this means that all branches of the block that do not exit, join on [pc']. -*) -Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> iblock -> (option node) -> Prop := - | mib_BF isfst fi pc i iinfo: - cfg!pc = Some i -> - match_final_inst dupmap fi i -> - match_iblock dupmap cfg isfst pc (BF fi iinfo) None - | mib_nop_on_rtl isfst pc pc' iinfo: - cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc') - | mib_nop_skip pc: - match_iblock dupmap cfg false pc (Bnop None) (Some pc) - | mib_op isfst pc pc' op lr r iinfo: - cfg!pc = Some (Iop op lr r pc') -> - match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') - | mib_load isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') - | mib_store isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Istore m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') - | mib_exit pc pc' iinfo: - dupmap!pc = (Some pc') -> - match_iblock dupmap cfg false pc' (BF (Bgoto pc) iinfo) None - (* NB: on RTL side, we exit the block by a "basic" instruction (or Icond). - Thus some step should have been executed before [pc'] in the RTL code *) - | mib_seq_Some isfst b1 b2 pc1 pc2 opc: - match_iblock dupmap cfg isfst pc1 b1 (Some pc2) -> - match_iblock dupmap cfg false pc2 b2 opc -> - match_iblock dupmap cfg isfst pc1 (Bseq b1 b2) opc -(* | mib_seq_None isfst b1 b2 pc: - match_iblock dupmap cfg isfst pc b1 None -> - match_iblock dupmap cfg isfst (Bseq b1 b2) pc None - (* TODO: here [b2] is dead code ! Is this case really useful ? - The oracle could remove this dead code. - And the verifier could fail if there is such dead code! - *) -*) - | mib_cond isfst c lr bso bnot pcso pcnot pc opc1 opc2 opc i iinfo: - cfg!pc = Some (Icond c lr pcso pcnot i) -> - match_iblock dupmap cfg false pcso bso opc1 -> - match_iblock dupmap cfg false pcnot bnot opc2 -> - is_join_opt opc1 opc2 opc -> - match_iblock dupmap cfg isfst pc (Bcond c lr bso bnot iinfo) opc - . - -Definition match_cfg dupmap (cfg: code) (cfg':RTL.code): Prop := - forall pc pc', dupmap!pc = Some pc' -> - exists ib, cfg!pc = Some ib /\ match_iblock dupmap cfg' true pc' ib.(entry) None. - -(** Shared verifier between RTL -> BTL and BTL -> RTL *) - -Local Open Scope error_monad_scope. - -Definition verify_is_copy dupmap n n' := - match dupmap!n with - | None => Error(msg "BTL.verify_is_copy None") - | Some revn => match (Pos.compare n' revn) with Eq => OK tt | _ => Error(msg "BTL.verify_is_copy invalid map") end - end. - -Fixpoint verify_is_copy_list dupmap ln ln' := - match ln with - | n::ln => match ln' with - | n'::ln' => do _ <- verify_is_copy dupmap n n'; - verify_is_copy_list dupmap ln ln' - | nil => Error (msg "BTL.verify_is_copy_list: ln' bigger than ln") end - | nil => match ln' with - | n :: ln' => Error (msg "BTL.verify_is_copy_list: ln bigger than ln'") - | nil => OK tt end - end. - -Lemma verify_is_copy_correct dupmap n n' tt: - verify_is_copy dupmap n n' = OK tt -> - dupmap ! n = Some n'. -Proof. - unfold verify_is_copy; repeat autodestruct. - intros NP H; destruct (_ ! n) eqn:REVM; [|inversion H]. - eapply Pos.compare_eq in NP. congruence. -Qed. -Local Hint Resolve verify_is_copy_correct: core. - -Lemma verify_is_copy_list_correct dupmap ln: forall ln' tt, - verify_is_copy_list dupmap ln ln' = OK tt -> - list_forall2 (fun n n' => dupmap ! n = Some n') ln ln'. -Proof. - induction ln. - - intros. destruct ln'; monadInv H. constructor. - - intros. destruct ln'; monadInv H. constructor; eauto. -Qed. - -(* TODO Copied from duplicate, should we import ? *) -Lemma product_eq {A B: Type} : - (forall (a b: A), {a=b} + {a<>b}) -> - (forall (c d: B), {c=d} + {c<>d}) -> - forall (x y: A+B), {x=y} + {x<>y}. -Proof. - intros H H'. intros. decide equality. -Qed. - -(* TODO Copied from duplicate, should we import ? *) -(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application" - * error when doing so *) -Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}. -Proof. - intros. - apply (builtin_arg_eq Pos.eq_dec). -Defined. -Global Opaque builtin_arg_eq_pos. - -(* TODO Copied from duplicate, should we import ? *) -Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}. -Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed. -Global Opaque builtin_res_eq_pos. - -Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) := - match ib with - | BF fi _ => - match fi with - | Bgoto pc1 => - do u <- verify_is_copy dupmap pc1 pc; - if negb isfst then - OK None - else Error (msg "BTL.verify_block: isfst is true Bgoto") - | Breturn or => - match cfg!pc with - | Some (Ireturn or') => - if option_eq Pos.eq_dec or or' then OK None - else Error (msg "BTL.verify_block: different opt reg in Breturn") - | _ => Error (msg "BTL.verify_block: incorrect cfg Breturn") - end - | Bcall s ri lr r pc1 => - match cfg!pc with - | Some (Icall s' ri' lr' r' pc2) => - do u <- verify_is_copy dupmap pc1 pc2; - if (signature_eq s s') then - if (product_eq Pos.eq_dec ident_eq ri ri') then - if (list_eq_dec Pos.eq_dec lr lr') then - if (Pos.eq_dec r r') then OK None - else Error (msg "BTL.verify_block: different r r' in Bcall") - else Error (msg "BTL.verify_block: different lr in Bcall") - else Error (msg "BTL.verify_block: different ri in Bcall") - else Error (msg "BTL.verify_block: different signatures in Bcall") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bcall") - end - | Btailcall s ri lr => - match cfg!pc with - | Some (Itailcall s' ri' lr') => - if (signature_eq s s') then - if (product_eq Pos.eq_dec ident_eq ri ri') then - if (list_eq_dec Pos.eq_dec lr lr') then OK None - else Error (msg "BTL.verify_block: different lr in Btailcall") - else Error (msg "BTL.verify_block: different ri in Btailcall") - else Error (msg "BTL.verify_block: different signatures in Btailcall") - | _ => Error (msg "BTL.verify_block: incorrect cfg Btailcall") - end - | Bbuiltin ef la br pc1 => - match cfg!pc with - | Some (Ibuiltin ef' la' br' pc2) => - do u <- verify_is_copy dupmap pc1 pc2; - if (external_function_eq ef ef') then - if (list_eq_dec builtin_arg_eq_pos la la') then - if (builtin_res_eq_pos br br') then OK None - else Error (msg "BTL.verify_block: different brr in Bbuiltin") - else Error (msg "BTL.verify_block: different lbar in Bbuiltin") - else Error (msg "BTL.verify_block: different ef in Bbuiltin") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bbuiltin") - end - | Bjumptable r ln => - match cfg!pc with - | Some (Ijumptable r' ln') => - do u <- verify_is_copy_list dupmap ln ln'; - if (Pos.eq_dec r r') then OK None - else Error (msg "BTL.verify_block: different r in Bjumptable") - | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") - end - end - | Bnop oiinfo => - match oiinfo with - | Some _ => - match cfg!pc with - | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") - end - | None => - if negb isfst then OK (Some pc) - else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)") - 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 "BTL.verify_block: different r in Bop") - else Error (msg "BTL.verify_block: different lr in Bop") - else Error (msg "BTL.verify_block: different operations in Bop") - | _ => Error (msg "BTL.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 TRAP && trapping_mode_eq tm' TRAP) 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 "BTL.verify_block: different r in Bload") - else Error (msg "BTL.verify_block: different lr in Bload") - else Error (msg "BTL.verify_block: different addressing in Bload") - else Error (msg "BTL.verify_block: different mchunk in Bload") - else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") - | _ => Error (msg "BTL.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 "BTL.verify_block: different r in Bstore") - else Error (msg "BTL.verify_block: different lr in Bstore") - else Error (msg "BTL.verify_block: different addressing in Bstore") - else Error (msg "BTL.verify_block: different mchunk in Bstore") - | _ => Error (msg "BTL.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 "BTL.verify_block: None next pc in Bseq (deadcode)") - end - | Bcond c lr bso bnot _ => - 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 "BTL.verify_block: is_join_opt incorrect for Bcond") - end - else Error (msg "BTL.verify_block: incompatible conditions in Bcond") - else Error (msg "BTL.verify_block: different lr in Bcond") - | _ => Error (msg "BTL.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 dupmap cfg ib: forall pc isfst 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 ]). - - (* BF *) - destruct fi; unfold verify_block in H. - + (* Bgoto *) - monadInv H. - destruct (isfst); simpl in EQ0; inv EQ0. - eapply verify_is_copy_correct in EQ. - constructor; assumption. - + (* Breturn *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - destruct (option_eq _ _ _); try discriminate. inv H. - eapply mib_BF; eauto. constructor. - + (* Bcall *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_correct in EQ. - destruct (signature_eq _ _); try discriminate. - destruct (product_eq _ _ _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (Pos.eq_dec _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - + (* Btailcall *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - destruct (signature_eq _ _); try discriminate. - destruct (product_eq _ _ _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. subst. - inv H. eapply mib_BF; eauto. constructor. - + (* Bbuiltin *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_correct in EQ. - destruct (external_function_eq _ _); try discriminate. - destruct (list_eq_dec _ _ _); try discriminate. - destruct (builtin_res_eq_pos _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - + (* Bjumptable *) - destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate. - monadInv H. - eapply verify_is_copy_list_correct in EQ. - destruct (Pos.eq_dec _ _); try discriminate. subst. - inv EQ0. eapply mib_BF; eauto. constructor; assumption. - - (* Bnop *) - destruct oiinfo; simpl in *. - + destruct (cfg!pc) eqn:EQCFG; try discriminate. - destruct i0; inv H. constructor; assumption. - + destruct isfst; try discriminate. 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. - do 2 (destruct (trapping_mode_eq _ _); try discriminate). - simpl in H. - 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. - eapply IHib2; eauto. - - (* 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. - all: inv EQ2; eapply mib_cond; eauto; econstructor. -Qed. -Local Hint Resolve verify_block_correct: core. - -Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit := - match l with - | nil => OK tt - | (pc, pc')::l => - match cfg!pc with - | Some ib => do o <- verify_block dupmap cfg' true pc' ib.(entry); - match o with - | None => verify_blocks dupmap cfg cfg' l - | _ => Error(msg "BTL.verify_blocks.end") - end - | _ => Error(msg "BTL.verify_blocks.entry") - end - end. -Definition verify_cfg dupmap (cfg: code) (cfg':RTL.code): res unit := - verify_blocks dupmap cfg cfg' (PTree.elements dupmap). - -Lemma verify_cfg_correct dupmap cfg cfg' tt: - verify_cfg dupmap cfg cfg' = OK tt -> - match_cfg dupmap cfg cfg'. -Proof. - unfold verify_cfg. - intros X pc pc' H; generalize X; clear X. - exploit PTree.elements_correct; eauto. - generalize tt pc pc' H; clear tt pc pc' H. - generalize (PTree.elements dupmap). - induction l as [|[pc1 pc1']l]; simpl. - - tauto. - - intros pc pc' DUP u H. - unfold bind. - repeat autodestruct. - intros; subst. - destruct H as [H|H]; eauto. - inversion H; subst. - eexists; split; eauto. -Qed. - -Definition verify_function dupmap f f' : res unit := - do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f'); - verify_cfg dupmap (fn_code f) (RTL.fn_code f'). +(** * Auxiliary general purpose functions on BTL *) Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false end. + -- cgit