diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | scheduling/BTL.v | 565 | ||||
| -rw-r--r-- | scheduling/BTLmatchRTL.v | 587 | ||||
| -rw-r--r-- | scheduling/BTLtoRTL.v | 7 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 42 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 3 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 44 |
7 files changed, 615 insertions, 635 deletions
@@ -143,7 +143,7 @@ SCHEDULING= \ RTLpathproof.v RTLpathSE_theory.v \ RTLpathSchedulerproof.v RTLpath.v \ RTLpathScheduler.v RTLpathWFcheck.v \ - BTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ + BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ BTL_SEtheory.v # C front-end modules (in cfrontend/) 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. + diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v new file mode 100644 index 00000000..23ff6681 --- /dev/null +++ b/scheduling/BTLmatchRTL.v @@ -0,0 +1,587 @@ +(** General notions about the bisimulation BTL <-> RTL. + +This bisimulation is proved on the "CFG semantics" of BTL called [cfgsem] defined below, +such that the full state of registers is preserved when exiting blocks. + +*) + +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep. +Require Import RTL Op Registers OptionMonad Lia. +Require Export BTL. + +(* 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). + +(* * Simulation of BTL fsem by BTL cfgsem: a lock-step less-def simulation. +*) + + +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 init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs + lessdef_state_refl: 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 lessdef_stackframe lessdef_state final_step list_forall2 step: 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. + +(** * Matching BTL (for cfgsem) and RTL code + +We define a single verifier able to prove a bisimulation between BTL and RTL code. + +Hence, in a sense, our verifier imitates the approach of Duplicate, where [dupmap] maps the BTL nodes to the RTL nodes. + +The [match_function] definition gives a "relational" specification of the verifier... +*) + +Require Import Errors. + +Inductive match_final_inst (dupmap: PTree.t node): final -> instruction -> Prop := + | 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 + (* here [b2] is dead code ! Our verifier rejects 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: BTL.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. + +Record match_function dupmap f f': Prop := { + dupmap_correct: match_cfg dupmap (BTL.fn_code f) (RTL.fn_code f'); + dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); + preserv_fnsig: fn_sig f = RTL.fn_sig f'; + preserv_fnparams: fn_params f = RTL.fn_params f'; + preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' +}. + +Inductive match_fundef: BTL.fundef -> RTL.fundef -> Prop := + | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := + | match_stackframe_intro + dupmap res f sp pc rs f' pc' + (TRANSF: match_function dupmap f f') + (DUPLIC: dupmap!pc = Some pc') + : match_stackframes (BTL.Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). + + +(** * 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'). + +Lemma verify_function_correct dupmap f f' tt: + verify_function dupmap f f' = OK tt -> + fn_sig f = RTL.fn_sig f' -> + fn_params f = RTL.fn_params f' -> + fn_stacksize f = RTL.fn_stacksize f' -> + match_function dupmap f f'. +Proof. + unfold verify_function; intro VERIF. monadInv VERIF. + constructor; eauto. + eapply verify_cfg_correct; eauto. +Qed. + diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v index 1333b406..fc58533d 100644 --- a/scheduling/BTLtoRTL.v +++ b/scheduling/BTLtoRTL.v @@ -1,21 +1,22 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. +Require Export BTLmatchRTL. Require Import Errors Linking. (** External oracle *) -Axiom btl2rtl: function -> RTL.code * node * (PTree.t node). +Axiom btl2rtl: BTL.function -> RTL.code * node * (PTree.t node). Extract Constant btl2rtl => "BTLtoRTLaux.btl2rtl". Local Open Scope error_monad_scope. -Definition transf_function (f: function) : res RTL.function := +Definition transf_function (f: BTL.function) : res RTL.function := let (tcte, dupmap) := btl2rtl f in let (tc, te) := tcte in let f' := RTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in - (*do u <- verify_function dupmap f f';*) + do u <- verify_function dupmap f f'; OK f'. Definition transf_fundef (f: fundef) : res RTL.fundef := diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 46f360c5..765f9cad 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -1,31 +1,12 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. -Require Import RTL Op Registers OptionMonad BTL. +Require Import RTL Op Registers OptionMonad. Require Import Errors Linking BTLtoRTL. Require Import Linking. -Record match_function dupmap f f': Prop := { - dupmap_correct: match_cfg dupmap (fn_code f) (RTL.fn_code f'); - dupmap_entrypoint: dupmap!(fn_entrypoint f) = Some (RTL.fn_entrypoint f'); - preserv_fnsig: fn_sig f = RTL.fn_sig f'; - preserv_fnparams: fn_params f = RTL.fn_params f'; - preserv_fnstacksize: fn_stacksize f = RTL.fn_stacksize f' -}. - -Inductive match_fundef: fundef -> RTL.fundef -> Prop := - | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f') - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc = Some pc') - : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). - -Inductive match_states: state -> RTL.state -> Prop := +Inductive match_states: BTL.state -> RTL.state -> Prop := | match_states_intro dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') @@ -43,26 +24,13 @@ Inductive match_states: state -> RTL.state -> Prop := : match_states (Returnstate st v m) (RTL.Returnstate st' v m) . -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f f' = OK tt -> - fn_sig f = RTL.fn_sig f' -> - fn_params f = RTL.fn_params f' -> - fn_stacksize f = RTL.fn_stacksize f' -> - match_function dupmap f f'. -Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - - eapply verify_cfg_correct; eauto. - - eapply verify_is_copy_correct; eauto. -Qed. - Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. Admitted. (* +Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. - Qed.*) +Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -402,7 +370,7 @@ Proof. Qed. Theorem transf_program_correct_cfg: - forward_simulation (BTL.cfgsem prog) (RTL.semantics tprog). + forward_simulation (BTLmatchRTL.cfgsem prog) (RTL.semantics tprog). Proof. eapply forward_simulation_plus with match_states. - eapply senv_preserved. diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v index 2ac02597..507fc9d9 100644 --- a/scheduling/RTLtoBTL.v +++ b/scheduling/RTLtoBTL.v @@ -1,6 +1,7 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. +Require Export BTLmatchRTL. Require Import Errors Linking. @@ -15,7 +16,7 @@ Definition transf_function (f: RTL.function) : res BTL.function := let (tcte, dupmap) := rtl2btl f in let (tc, te) := tcte in let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in - (*do u <- verify_function dupmap f' f;*) + do u <- verify_function dupmap f' f; OK f'. Definition transf_fundef (f: RTL.fundef) : res fundef := diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f2f99ef5..ef336de5 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -229,45 +229,21 @@ Qed. (** * Matching relation on functions *) -Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { - dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); - dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); - preserv_fnsig: fn_sig tf = RTL.fn_sig f; - preserv_fnparams: fn_params tf = RTL.fn_params f; - preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f -}. - -Inductive match_fundef: RTL.fundef -> fundef -> Prop := - | match_Internal dupmap f tf: match_function dupmap f tf -> match_fundef (Internal f) (Internal tf) - | match_External ef: match_fundef (External ef) (External ef). - -Inductive match_stackframes: RTL.stackframe -> stackframe -> Prop := - | match_stackframe_intro - dupmap res f sp pc rs f' pc' - (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) - : match_stackframes (RTL.Stackframe res f sp pc rs) (Stackframe res f' sp pc' rs). +(* we simply switch [f] and [tf] in the usual way *) +Definition match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := + BTLmatchRTL.match_function dupmap tf f. -Lemma verify_function_correct dupmap f f' tt: - verify_function dupmap f' f = OK tt -> - fn_sig f' = RTL.fn_sig f -> - fn_params f' = RTL.fn_params f -> - fn_stacksize f' = RTL.fn_stacksize f -> - match_function dupmap f f'. -Proof. - unfold verify_function; intro VERIF. monadInv VERIF. - constructor; eauto. - - eapply verify_cfg_correct; eauto. - - eapply verify_is_copy_correct; eauto. -Qed. +Definition match_fundef f tf := BTLmatchRTL.match_fundef tf f. + +Definition match_stackframes stk stk' := BTLmatchRTL.match_stackframes stk' stk. Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. Admitted. (* +Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. - Qed.*) +Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -711,7 +687,7 @@ Proof. inv H. + (* Internal function *) inv TRANSF. - rename H0 into TRANSF. + rename H1 into TRANSF. eapply dupmap_entrypoint in TRANSF as ENTRY. eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. apply DMC in ENTRY as DMC'. @@ -739,7 +715,7 @@ Qed. Local Hint Resolve plus_one star_refl: core. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (BTL.cfgsem tprog). + forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog). Proof. eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states). constructor 1; simpl. |