diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
commit | 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a (patch) | |
tree | abbb54fca752a15a190e66dcb902a42b0be97cd9 | |
parent | 65247b67cbd469b9cd3bea22410bd11af450696c (diff) | |
download | compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.tar.gz compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.zip |
Now supporting Bnop insertion in conditions
-rw-r--r-- | scheduling/BTL.v | 66 | ||||
-rw-r--r-- | scheduling/BTLtoRTLaux.ml | 17 | ||||
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 29 | ||||
-rw-r--r-- | scheduling/RTLtoBTLaux.ml | 11 | ||||
-rw-r--r-- | scheduling/RTLtoBTLproof.v | 151 |
5 files changed, 135 insertions, 139 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index ca727f82..05391c58 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -58,7 +58,7 @@ Inductive iblock: Type := (* final instructions that stops block execution *) | BF (fi: final) (iinfo: inst_info) (* basic instructions that continues block execution, except when aborting *) - | Bnop (iinfo: inst_info) (* nop instruction *) + | Bnop (oiinfo: option inst_info) (* nop instruction *) | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info) (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *) | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info) @@ -204,7 +204,7 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop := (** internal big-step execution of one iblock *) Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop := | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin) - | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None +| exec_nop rs m oiinfo: iblock_istep sp rs m (Bnop oiinfo) rs m None | exec_op rs m op args res v iinfo (EVAL: eval_operation ge sp op rs##args m = Some v) : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None @@ -425,9 +425,11 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i cfg!pc = Some i -> match_final_inst dupmap fi i -> match_iblock dupmap cfg isfst pc (BF fi iinfo) None - | mib_nop isfst pc pc' iinfo: + | mib_nop_on_rtl isfst pc pc' iinfo: cfg!pc = Some (Inop pc') -> - match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some 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') @@ -592,10 +594,16 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable") end end - | Bnop _ => - match cfg!pc with - | Some (Inop pc') => OK (Some pc') - | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop") + | 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 @@ -712,8 +720,11 @@ Proof. destruct (Pos.eq_dec _ _); try discriminate. subst. inv EQ0. eapply mib_BF; eauto. constructor; assumption. - (* Bnop *) - destruct i; inv H. - constructor; assumption. + 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. @@ -803,10 +814,16 @@ Definition is_goto (ib: iblock): bool := Definition is_atom (ib: iblock): bool := match ib with - | Bseq _ _ | Bcond _ _ _ _ _ => false + | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false | _ => true end. +Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }. +Proof. + destruct k; simpl; try destruct oiinfo; + intuition congruence. +Defined. + (** Is expand property to only support atomic instructions on the left part of a Bseq *) Inductive is_expand: iblock -> Prop := | exp_Bseq ib1 ib2: @@ -814,8 +831,8 @@ Inductive is_expand: iblock -> Prop := is_expand ib2 -> is_expand (Bseq ib1 ib2) | exp_Bcond cond args ib1 ib2 iinfo: - is_expand ib1 -> - is_expand ib2 -> + is_expand ib1 \/ ib1 = Bnop None -> + is_expand ib2 \/ ib2 = Bnop None -> is_expand (Bcond cond args ib1 ib2 iinfo) | exp_others ib: is_atom ib = true -> @@ -823,22 +840,27 @@ Inductive is_expand: iblock -> Prop := . Local Hint Constructors is_expand: core. -Fixpoint expand (ib: iblock) (k: option iblock): iblock := +Fixpoint expand (ib: iblock) (k: iblock): iblock := match ib with - | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k)) + | Bseq ib1 ib2 => expand ib1 (expand ib2 k) | Bcond cond args ib1 ib2 iinfo => Bcond cond args (expand ib1 k) (expand ib2 k) iinfo | BF fin iinfo => BF fin iinfo - | ib => - match k with - | None => ib - | Some rem => Bseq ib rem - end + | Bnop None => k + | ib => + if Bnop_dec k then ib else Bseq ib k end. Lemma expand_correct ib: forall k, - (match k with Some rem => is_expand rem | None => True end) + (k <> (Bnop None) -> is_expand k) + -> (expand ib k) <> (Bnop None) -> is_expand (expand ib k). Proof. - induction ib; simpl; intros; try autodestruct; auto. + induction ib; simpl; intros; auto. + 1-4: + try destruct oiinfo; + destruct (Bnop_dec k); auto. + constructor. + - destruct (Bnop_dec (expand ib1 k)); auto. + - destruct (Bnop_dec (expand ib2 k)); auto. Qed. diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index b4833b2c..36d3e6a4 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -6,15 +6,11 @@ open AuxTools open DebugPrint open BTLaux -let is_atom = function - | Bseq (_, _) | Bcond (_, _, _, _, _) -> false - | _ -> true - let get_inumb iinfo = P.of_int iinfo.inumb let rec get_ib_num = function | BF (Bgoto s, _) -> s - | Bnop iinfo + | Bnop Some iinfo | Bop (_, _, _, iinfo) | Bload (_, _, _, _, _, iinfo) | Bstore (_, _, _, _, iinfo) @@ -22,6 +18,7 @@ let rec get_ib_num = function | BF (_, iinfo) -> get_inumb iinfo | Bseq (ib1, _) -> get_ib_num ib1 + | Bnop None -> failwith "get_ib_num: Bnop None found" let translate_function code entry = let rtl_code = ref PTree.empty in @@ -45,23 +42,21 @@ let translate_function code entry = | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) -> next_nodes := s1 :: s2 :: !next_nodes; Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo) - | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) -> + | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) -> assert (iinfo.pcond = Some false); next_nodes := s1 :: !next_nodes; - translate_btl_block ib2 None; Some - ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond), + ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond), get_inumb iinfo ) (* TODO gourdinl remove dynamic check *) | Bcond (_, _, _, _, _) -> failwith "translate_function: invalid Bcond" | Bseq (ib1, ib2) -> - (* TODO gourdinl remove dynamic check *) - assert (is_atom ib1); translate_btl_block ib1 (Some ib2); translate_btl_block ib2 None; None - | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop Some iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop None -> failwith "translate_function: invalid Bnop" | Bop (op, lr, rd, iinfo) -> Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo) | Bload (trap, chk, addr, lr, rd, iinfo) -> diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b37d8fa..2e8d960c 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -202,6 +202,17 @@ Proof. eapply plus_trans; eauto. Qed. +Lemma css_E0_trans isfst isfst' s0 s1 s2: + cond_star_step (isfst=false) s0 E0 s1 -> + cond_star_step (false=isfst') s1 E0 s2 -> + cond_star_step (isfst=isfst') s0 E0 s2. +Proof. + intros S1 S2. + inversion S1; subst; eauto. + inversion S2; subst; eauto. + eapply css_plus_trans; eauto. +Qed. + Lemma css_star P s0 s1 t: cond_star_step P s0 t s1 -> star RTL.step tge s0 t s1. @@ -219,7 +230,7 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin forall pc0 opc isfst (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc), match ofin with - | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) + | None => exists pc1,(opc = Some pc1) /\ cond_star_step (isfst = false) (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) | Some fin => exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) @@ -231,19 +242,19 @@ Proof. subst. repeat eexists; eauto. - (* exec_nop *) - inv MIB. exists pc'; split; eauto. + inv MIB; eexists; split; econstructor; eauto. - (* exec_op *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Iop; eauto. erewrite <- eval_operation_preserved; eauto. intros; rewrite symbols_preserved; trivial. - (* exec_load *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Iload; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. - (* exec_store *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Istore; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. @@ -257,10 +268,10 @@ Proof. destruct ofin; simpl. + intros (ifst2 & pc2 & iinfo & M2 & STEP2). repeat eexists; eauto. - eapply css_plus_trans; eauto. + eapply css_E0_trans; eauto. + intros (pc2 & EQpc2 & STEP2); inv EQpc2. eexists; split; auto. - eapply plus_trans; eauto. + eapply css_E0_trans; eauto. - (* exec_cond *) inv MIB. rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) @@ -275,7 +286,7 @@ Proof. intros (pc1 & OPC & PLUS). inv OPC. inv JOIN; eexists; split; eauto. all: - eapply plus_trans; eauto. + eapply css_plus_trans; eauto. + (* taking ifnot *) destruct ofin; simpl. * (* ofin is Some final *) @@ -286,7 +297,7 @@ Proof. intros (pc1 & OPC & PLUS). subst. inv JOIN; eexists; split; eauto. all: - eapply plus_trans; eauto. + eapply css_plus_trans; eauto. Qed. Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 43556150..4be2b180 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -2,9 +2,9 @@ open Maps open RTL open BTL open Registers -open DebugPrint open PrintBTL open AuxTools +open DebugPrint open BTLaux let undef_node = -1 @@ -20,13 +20,13 @@ let encaps_final inst osucc = | BF _ | Bcond _ -> inst | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo)) -let translate_inst iinfo inst is_final = +let translate_inst (iinfo: BTL.inst_info) inst is_final = let osucc = ref None in let btli = match inst with | Inop s -> osucc := Some s; - Bnop iinfo + Bnop (Some iinfo) | Iop (op, lr, rd, s) -> osucc := Some s; Bop (op, lr, rd, iinfo) @@ -80,12 +80,13 @@ let translate_function code entry join_points = assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; iinfo.pcond <- info; + Bseq ( Bcond ( cond, lr, BF (Bgoto ifso, def_iinfo), - build_btl_block s, - iinfo ) + Bnop None, + iinfo ), build_btl_block s) | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) | None -> debug "BLOCK END.\n"; diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 7ad1472b..f3e258ae 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -242,11 +242,20 @@ Proof. Qed. Lemma expand_entry_isnt_goto dupmap f pc ib: - match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> - is_goto (expand (entry ib) None) = false. + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None -> + is_goto (expand (entry ib) (Bnop None)) = false. Proof. - destruct (is_goto (expand (entry ib) None))eqn:EQG; - destruct (expand (entry ib) None); + destruct (is_goto (expand (entry ib) (Bnop None))) eqn:EQG; + destruct (expand (entry ib) (Bnop None)); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H5. +Qed. + +Lemma expand_entry_isnt_bnop dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None -> + expand (entry ib) (Bnop None) <> Bnop None. +Proof. + destruct (expand (entry ib) (Bnop None)) eqn:EQG; try destruct fi; try discriminate; trivial. intros; inv H; inv H5. Qed. @@ -268,38 +277,23 @@ Proof. intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. Qed. +Local Hint Constructors iblock_istep: core. Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1: forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1) k ofin2 rs2 m2 (CONT: match ofin1 with - | None => - (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) - \/ (exists rem, k = Some rem - /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2) + | None => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2 | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 end), iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2. Proof. - induction 1; simpl. - { (* BF *) - intros ? ? ? ? (HRS & HM & HOF); subst. - constructor. } - (*destruct k; intros. try inv CONT.*) - 1-4: (* Bnop, Bop, Bload, Bstore *) - destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; - subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail); - inversion HR; subst; clear HR; - eapply exec_seq_continue; [ econstructor; eauto | assumption]. - - (* Bseq_stop *) - destruct k; intros; apply IHISTEP; eauto. - - (* Bseq_continue *) - destruct ofin; intros. - + destruct CONT as [HRS [HM HOF]]; subst. - eapply IHISTEP1; right. eexists; repeat split; eauto. - + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst. - * eapply IHISTEP1; right. eexists; repeat split; eauto. - eapply IHISTEP2; left; simpl; auto. - * eapply IHISTEP1; right. eexists; repeat split; eauto. + induction 1; simpl; intros; intuition subst; eauto. + { (* Bnop *) + autodestruct; intros OI; inv OI; destruct (Bnop_dec k); subst; + try (inv CONT; constructor; fail); repeat econstructor; eauto. } + 1-3: (* Bop, Bload, Bstore *) + intros; destruct (Bnop_dec k); subst; repeat econstructor; eauto; + inv CONT; econstructor; eauto. - (* Bcond *) destruct ofin; intros; econstructor; eauto; @@ -308,47 +302,19 @@ Qed. Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin -> - iblock_istep tge sp rs0 m0 (expand ib None) rs1 m1 ofin. + iblock_istep tge sp rs0 m0 (expand ib (Bnop None)) rs1 m1 ofin. Proof. intros; eapply expand_iblock_istep_rec_correct; eauto. destruct ofin; simpl; auto. Qed. -(* TODO gourdinl useless? *) -Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1: - forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 = - Some {| _rs := rs1; _m := m1; _fin := ofin1 |}) - k ofin2 rs2 m2 - (CONT: match ofin1 with - | None => - (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None) - \/ (exists rem, k = Some rem - /\ iblock_istep_run tge sp rem rs1 m1 = - Some {| _rs := rs2; _m := m2; _fin := ofin2 |}) - | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1 - end), - iblock_istep_run tge sp (expand ib k) rs0 m0 = - Some {| _rs := rs2; _m := m2; _fin := ofin2 |}. -Proof. - intros. destruct ofin1; - rewrite <- iblock_istep_run_equiv in *. - - destruct CONT as [HRS [HM HO]]; subst. - eapply expand_iblock_istep_rec_correct; eauto. - simpl; auto. - - eapply expand_iblock_istep_rec_correct; eauto. - simpl. destruct CONT as [HL | [rem [HR ISTEP']]]. - left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'. - right; eexists; split; eauto. -Qed. - Lemma expand_iblock_istep_run_None_rec sp ib: forall rs0 m0 o k (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o) (CONT: match o with | Some (out rs1 m1 ofin) => - exists rem, - k = Some rem /\ ofin = None /\ - iblock_istep_run tge sp rem rs1 m1 = None + ofin = None /\ + iblock_istep_run tge sp k rs1 m1 = None | _ => True end), iblock_istep_run tge sp (expand ib k) rs0 m0 = None. @@ -357,35 +323,34 @@ Proof. try discriminate. - (* BF *) intros; destruct o; try discriminate; simpl in *. - inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO. + inv ISTEP. destruct CONT as [HO ISTEP]; inv HO. - (* Bnop *) - intros; destruct o; inv ISTEP; destruct k; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto. + destruct (Bnop_dec k); subst; repeat econstructor; eauto. - (* Bop *) - intros; destruct o; - destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k; - simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]]; - inv HR; inv HO; trivial. + intros; destruct o; destruct (Bnop_dec k); + destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; + simpl; rewrite EVAL; auto; destruct CONT as [HO ISTEP]; + trivial. - (* Bload *) - intros; destruct o; + intros; destruct o; destruct (Bnop_dec k); destruct (trap) eqn:TRAP; try destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k; + try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + destruct CONT as [HO ISTEP]; trivial. - (* Bstore *) - intros; destruct o; + intros; destruct o; destruct (Bnop_dec k); destruct (eval_addressing _ _ _ _) eqn:EVAL; - try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k; + try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; simpl; try rewrite EVAL; try rewrite MEM; simpl; auto; - destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial. + destruct CONT as [HO ISTEP]; inv HO; trivial. - (* Bseq *) intros. eapply IHib1; eauto. destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto. - destruct o0. eexists; split; eauto. simpl in *. - destruct _fin; inv ISTEP. - + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA. + destruct o0; simpl in *. destruct _fin; inv ISTEP. + + destruct CONT as [CONTRA _]; inv CONTRA. + split; auto. eapply IHib2; eauto. - (* Bcond *) intros; destruct (eval_condition _ _ _); trivial. @@ -396,7 +361,7 @@ Qed. Lemma expand_preserves_iblock_istep_run_None sp ib: forall rs m, iblock_istep_run tge sp ib rs m = None - -> iblock_istep_run tge sp (expand ib None) rs m = None. + -> iblock_istep_run tge sp (expand ib (Bnop None)) rs m = None. Proof. intros; eapply expand_iblock_istep_run_None_rec; eauto. simpl; auto. @@ -404,7 +369,7 @@ Qed. Lemma expand_preserves_iblock_istep_run sp ib: forall rs m, iblock_istep_run tge sp ib rs m = - iblock_istep_run tge sp (expand ib None) rs m. + iblock_istep_run tge sp (expand ib (Bnop None)) rs m. Proof. intros. destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP. @@ -415,28 +380,24 @@ Proof. apply expand_preserves_iblock_istep_run_None; auto. Qed. +Local Hint Constructors match_iblock: core. Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst: forall opc1 (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2 (CONT: match opc1 with | Some pc' => - k = None /\ opc2 = opc1 \/ - (exists rem, k = Some rem - /\ match_iblock dupmap cfg false pc' rem opc2) + match_iblock dupmap cfg false pc' k opc2 | None => opc2=opc1 end), match_iblock dupmap cfg isfst pc (expand ib k) opc2. Proof. - induction 1; simpl. + induction 1; simpl; intros; eauto. { (* BF *) - intros; inv CONT; econstructor; eauto. } - 1-4: (* Bnop *) - destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]]; - try inv HK; try inv HO; try inv HR; repeat econstructor; eauto. + inv CONT; econstructor; eauto. } + 1-4: (* Bnop, Bop, Bload, Bstore *) + destruct (Bnop_dec k); subst; eauto; inv CONT; econstructor; eauto. { (* Bgoto *) intros; inv CONT; apply mib_exit; auto. } - { (* Bseq *) - intros. eapply IHMIB1. right. eexists; split; eauto. } { (* Bcond *) intros. inv H0; econstructor; eauto; try econstructor. @@ -445,7 +406,7 @@ Qed. Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc: match_iblock dupmap cfg isfst pc ib opc -> - match_iblock dupmap cfg isfst pc (expand ib None) opc. + match_iblock dupmap cfg isfst pc (expand ib (Bnop None)) opc. Proof. intros. eapply expand_matchiblock_rec_correct; eauto. @@ -508,6 +469,7 @@ Proof. apply iblock_istep_run_equiv in BTL_RUN; eauto. + econstructor; apply expand_matchiblock_correct in MI. econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. econstructor. apply expand_preserves_iblock_istep_run. eapply expand_entry_isnt_goto; eauto. - (* Others *) @@ -575,7 +537,8 @@ Proof. eapply eval_builtin_args_preserved; eauto. eapply external_call_symbols_preserved; eauto. eapply senv_preserved. * econstructor; eauto; apply expand_matchiblock_correct in MI. - { econstructor; eauto. apply expand_correct; trivial. + { econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. apply star_refl. apply expand_preserves_iblock_istep_run. } eapply expand_entry_isnt_goto; eauto. + (* Bjumptable *) @@ -591,6 +554,7 @@ Proof. eapply BTL_RUN. econstructor; eauto. * econstructor; eauto; apply expand_matchiblock_correct in MI. { econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. apply star_refl. apply expand_preserves_iblock_istep_run. } eapply expand_entry_isnt_goto; eauto. - (* mib_exit *) @@ -599,7 +563,7 @@ Proof. inversion H; subst; try (inv IS_EXPD; try inv H5; discriminate; fail); inversion STEP; subst; try_simplify_someHyps; intros. - + (* Bnop *) + + (* Bnop is_rtl *) eapply match_strong_state_simu. 1,2: do 2 (econstructor; eauto). econstructor; eauto. @@ -637,7 +601,8 @@ Proof. intros; rewrite H12 in BTL_RUN. destruct b; eapply match_strong_state_simu; eauto. 1,3: inv H2; econstructor; eauto. - 1,3,5,7: inv IS_EXPD; auto; discriminate. + 1,3: inv IS_EXPD; [ inv H3; auto; inv H0 | inv H ]. + 3,5: inv IS_EXPD; [ inv H7; auto; inv H1 | inv H ]. 1-4: eapply star_right; eauto. assert (measure bnot > 0) by apply measure_pos; lia. assert (measure bso > 0) by apply measure_pos; lia. @@ -698,6 +663,7 @@ Proof. * apply expand_matchiblock_correct in MI. econstructor. econstructor; eauto. apply expand_correct; trivial. + intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto. 3: eapply expand_entry_isnt_goto; eauto. all: erewrite preserv_fnparams; eauto. constructor. @@ -719,7 +685,8 @@ Proof. + apply expand_matchiblock_correct in MI. econstructor. econstructor; eauto. apply expand_correct; trivial. - constructor. apply expand_preserves_iblock_istep_run. + constructor. congruence. eapply expand_entry_isnt_bnop; eauto. + econstructor. apply expand_preserves_iblock_istep_run. eapply expand_entry_isnt_goto; eauto. Qed. |