From 457bc7206fe57fedfa69678597d0ec030beb3915 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 1 Jul 2022 21:56:10 +0100 Subject: Finish DeadBlocksproof --- src/hls/DeadBlocksproof.v | 204 ++++++++++++++++++++++++---------------------- src/hls/GibleSeq.v | 49 +++++++++++ src/hls/IfConversion.v | 6 +- 3 files changed, 158 insertions(+), 101 deletions(-) (limited to 'src') diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v index eda9b5e..7f1da9c 100644 --- a/src/hls/DeadBlocksproof.v +++ b/src/hls/DeadBlocksproof.v @@ -26,6 +26,7 @@ Require Import Events. Require Import Gible. Require Import GibleSeq. Require Import Relation_Operators. +Require Import Vericertlib. Unset Allow StrictProp. @@ -878,149 +879,156 @@ Hint Resolve sig_fundef_translated : valagree. Hint Resolve senv_preserved : valagree. Hint Resolve stacksize_preserved: valagree. +Lemma step_instr : + forall sp s1 s2 a, + step_instr ge sp s1 a s2 -> + step_instr tge sp s1 a s2. +Proof. + inversion 1; subst; econstructor; eauto with valagree. + - erewrite eval_operation_preserved; eauto with valagree. + - erewrite eval_addressing_preserved; eauto with valagree. + - erewrite eval_addressing_preserved; eauto with valagree. +Qed. + +Lemma seqbb_eq : + forall bb sp i1 i2 cf, + SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) -> + SeqBB.step tge sp (Iexec i1) bb (Iterm i2 cf). +Proof. + induction bb; crush; inv H. + - econstructor; eauto. apply step_instr; eassumption. + destruct state'. eapply IHbb; eauto. + - constructor; apply step_instr; auto. +Qed. + Ltac try_succ f pc pc' := try (eapply Rstar_trans ; eauto) ; constructor ; (eapply (CFG (fn_code f) pc pc'); eauto; simpl; auto). -Lemma transl_step_correct: - forall s1 t s2, - step ge s1 t s2 -> - forall s1' (MS: match_states s1 s1'), - exists s2', step tge s1' t s2' /\ match_states s2 s2'. +Lemma step_cf_eq : + forall stk stk' f tf sp pc rs pr m cf s t bb p, + step_cf_instr ge (State stk f sp pc rs pr m) cf t s -> + match_stackframes stk stk' -> + transf_function f = OK tf -> + (cfg (fn_code f) ** ) (fn_entrypoint f) pc -> + (fn_code f)!pc = Some bb -> + In (RBexit p cf) bb -> + exists s', step_cf_instr tge (State stk' tf sp pc rs pr m) cf t s' + /\ match_states s s'. Proof. - induction 1; intros; inv MS; auto. - - (* inop *) - exploit instr_at; eauto; intros. - destruct state0. - exists (State stack f0 sp0 pc0 rs0 pr0 m0); split ; eauto. - econstructor; auto. eauto. admit. admit. - constructor; auto. admit. - try_succ f pc pc'. - - (* iop *) - exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp pc' (rs#res<- v) m); split ; eauto. - eapply RTLdfs.exec_Iop ; eauto. - rewrite <- H0 ; eauto with valagree. - constructor; auto. - try_succ f pc pc'. - - (* iload *) - exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp pc' (rs#dst <- v) m); split ; eauto. - eapply RTLdfs.exec_Iload ; eauto. - try solve [rewrite <- H0 ; eauto with valagree]. - econstructor ; eauto. - try_succ f pc pc'. + inversion 1; subst; simplify. - (* istore *) - exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp pc' rs m'); split ; eauto. - eapply RTLdfs.exec_Istore ; eauto. - try solve [rewrite <- H0 ; eauto with valagree]. - constructor ; eauto. - try_succ f pc pc'. - - (* icall *) + (*icall*) destruct ros. exploit spec_ros_r_find_function ; eauto. - intros. destruct H1 as [tf' [Hfind OKtf']]. + intros. destruct H5 as [tf' [Hfind OKtf']]. - exploit instr_at; eauto; intros. - exists (RTLdfs.Callstate (RTLdfs.Stackframe res tf sp pc' rs :: ts) tf' rs ## args m) ; split ; eauto. - eapply RTLdfs.exec_Icall ; eauto. - eauto with valagree. - constructor; auto. - constructor; auto. - try_succ f pc pc'. + eexists ; split ; eauto. constructor; eauto with valagree. + constructor; eauto. constructor; eauto. try_succ f pc pc'; eauto. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. exploit spec_ros_id_find_function ; eauto. - intros. destruct H1 as [tf' [Hfind OKtf']]. + intros. destruct H5 as [tf' [Hfind OKtf']]. - exploit instr_at; eauto; intros. - exists (RTLdfs.Callstate (RTLdfs.Stackframe res tf sp pc' rs :: ts) tf' rs ## args m) ; split ; eauto. - eapply RTLdfs.exec_Icall ; eauto. - eauto with valagree. - constructor; auto. - constructor ; eauto. - try_succ f pc pc'. + eexists ; split ; eauto. constructor; eauto with valagree. + constructor; eauto. constructor; eauto. try_succ f pc pc'; eauto. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. - (* itailcall *) + (*itailcall*) destruct ros. exploit spec_ros_r_find_function ; eauto. - intros. destruct H1 as [tf' [Hfind OKtf']]. + intros. destruct H5 as [tf' [Hfind OKtf']]. - exploit instr_at; eauto; intros. exploit find_function_preserved_same ; eauto. intros. - exists (RTLdfs.Callstate ts tf' rs##args m'); split ; eauto. - eapply RTLdfs.exec_Itailcall ; eauto with valagree. - replace (RTLdfs.fn_stacksize tf) with (fn_stacksize f); eauto with valagree. + exists (Callstate stk' tf' rs##args m'); split ; eauto. + constructor; eauto with valagree. + replace (fn_stacksize tf) with (fn_stacksize f); eauto with valagree. exploit spec_ros_id_find_function ; eauto. - intros. destruct H1 as [tf' [Hfind OKtf']]. + intros. destruct H5 as [tf' [Hfind OKtf']]. - exploit instr_at; eauto; intros. - exists (RTLdfs.Callstate ts tf' rs##args m'); split ; eauto. - eapply RTLdfs.exec_Itailcall ; eauto with valagree. - replace (RTLdfs.fn_stacksize tf) with (fn_stacksize f); eauto with valagree. + exists (Callstate stk' tf' rs##args m'); split ; eauto. + constructor ; eauto with valagree. + replace (fn_stacksize tf) with (fn_stacksize f); eauto with valagree. (* ibuiltin *) exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp pc' (regmap_setres res vres rs) m') ; split ; eauto. - eapply RTLdfs.exec_Ibuiltin with (vargs:= vargs) ; eauto. - eapply eval_builtin_args_preserved with (2:= H0); eauto with valagree. + exists (State stk' tf sp pc' (regmap_setres res vres rs) pr m') ; split ; eauto. + econstructor ; eauto. + eapply eval_builtin_args_preserved with (2:= H10); eauto with valagree. eapply external_call_symbols_preserved; eauto with valagree. constructor; auto. try_succ f pc pc'. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. (* ifso *) - - exploit instr_at; eauto; intros. destruct b. - exists (RTLdfs.State ts tf sp ifso rs m); split ; eauto. - eapply RTLdfs.exec_Icond ; eauto. + exists (State stk' tf sp ifso rs pr m); split ; eauto. + eapply exec_RBcond ; eauto. constructor; auto. try_succ f pc ifso. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. - (* ifnot *) - exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp ifnot rs m); split ; eauto. - eapply RTLdfs.exec_Icond ; eauto. + (*ifnot*) + exists (State stk' tf sp ifnot rs pr m); split ; eauto. + eapply exec_RBcond ; eauto. constructor; auto. try_succ f pc ifnot. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. (* ijump *) - exploit instr_at; eauto; intros. - exists (RTLdfs.State ts tf sp pc' rs m); split ; eauto. - eapply RTLdfs.exec_Ijumptable ; eauto. + exists (State stk' tf sp pc' rs pr m); split ; eauto. + eapply exec_RBjumptable ; eauto. constructor; auto. try_succ f pc pc'. - eapply list_nth_z_in; eauto. + eapply in_cf_all_successors; eauto. eapply list_nth_z_in; eauto. (* ireturn *) - exploit instr_at; eauto; intros. - exists (RTLdfs.Returnstate ts (regmap_optget or Vundef rs) m'); split ; eauto. - eapply RTLdfs.exec_Ireturn ; eauto. - rewrite <- H0 ; eauto with valagree. + exists (Returnstate stk' (regmap_optget or Vundef rs) m'); split ; eauto. + eapply exec_RBreturn ; eauto. + rewrite <- H10 ; eauto with valagree. rewrite stacksize_preserved with f tf ; eauto. + (*igoto*) + exists (State stk' tf sp pc' rs pr m); split; eauto. + eapply exec_RBgoto; eauto. + constructor; auto. + try_succ f pc pc'. + eapply in_cf_all_successors; eauto; cbn [successors_instr]; intuition. +Qed. + +Lemma transl_step_correct: + forall s1 t s2, + step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + exists s2', step tge s1' t s2' /\ match_states s2 s2'. +Proof. + induction 1; intros; inv MS; auto. + + exploit instr_at; eauto; intros. + exploit step_cf_in; eauto; simplify. + exploit step_cf_eq; eauto; simplify. + exists x0. + split. econstructor; eauto. + apply seqbb_eq; auto. auto. + (* internal *) simpl in SPEC. monadInv SPEC. simpl in STACK. - exists (RTLdfs.State ts x - (Vptr stk Ptrofs.zero) - x.(RTLdfs.fn_entrypoint) - (init_regs args x.(RTLdfs.fn_params)) - m'). + exists (State ts x + (Vptr stk Ptrofs.zero) + x.(fn_entrypoint) + (init_regs args x.(fn_params)) + (PMap.init false) + m'). split. - eapply RTLdfs.exec_function_internal; eauto. + eapply exec_function_internal; eauto. rewrite stacksize_preserved with f x in H ; auto. - replace (RTL.fn_entrypoint f) with (RTLdfs.fn_entrypoint x). - replace (RTL.fn_params f) with (RTLdfs.fn_params x). + replace (fn_entrypoint f) with (fn_entrypoint x). + replace (fn_params f) with (fn_params x). econstructor ; eauto. - replace (RTLdfs.fn_entrypoint x) with (fn_entrypoint f). + replace (fn_entrypoint x) with (fn_entrypoint f). eapply Rstar_refl ; eauto. monadInv EQ. auto. monadInv EQ. auto. @@ -1028,19 +1036,19 @@ Proof. (* external *) inv SPEC. - exists (RTLdfs.Returnstate ts res m'). split. - eapply RTLdfs.exec_function_external; eauto. + exists (Returnstate ts res m'). split. + eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto with valagree. econstructor ; eauto. (* return state *) inv STACK. - exists (RTLdfs.State ts0 tf sp pc (rs# res <- vres) m); + exists (State ts0 tf sp pc (rs# res <- vres) pr m); split; ( try constructor ; eauto). Qed. Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTLdfs.semantics tprog). + forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_step. eapply senv_preserved. diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 2a04a55..45095f3 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -198,3 +198,52 @@ Proof. inv H. assert (i1 = (Iterm state' cf)) by (eapply exec_determ; eauto). subst. exfalso; eapply step_list2_false; eauto. Qed. + +Lemma step_cf_in : + forall A B (ge: Genv.t A B) sp bb i1 i2 cf, + SeqBB.step ge sp (Iexec i1) bb (Iterm i2 cf) -> + exists p, In (RBexit p cf) bb. +Proof. + induction bb; crush; inv H; eauto. + exploit IHbb; eauto; simplify; eauto. + inv H3; eauto. +Qed. + +Lemma SeqBB_foldl_In : + forall bb l pc, + In pc l -> + In pc (fold_left (fun (ns : list node) (i : instr) => match i with + | RBexit _ cf0 => successors_instr cf0 ++ ns + | _ => ns + end) bb l). +Proof. + induction bb; crush. eapply IHbb; eauto. + destruct a; auto. + apply in_or_app; auto. +Qed. + +Lemma in_cf_all_successors' : + forall bb pc cf p l, + In pc (successors_instr cf) -> + In (RBexit p cf) bb -> + In pc (fold_left (fun (ns : list node) (i : instr) => match i with + | RBexit _ cf0 => successors_instr cf0 ++ ns + | _ => ns + end) bb l). +Proof. + induction bb; crush. + inv H0. simplify. + eapply SeqBB_foldl_In. + apply in_or_app; auto. + eapply IHbb; eauto. +Qed. + +Lemma in_cf_all_successors : + forall bb pc cf p, + In pc (successors_instr cf) -> + In (RBexit p cf) bb -> + In pc (all_successors bb). +Proof. + unfold all_successors, SeqBB.foldl; intros. + eapply in_cf_all_successors'; eauto. +Qed. diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index ce6149b..d29eeeb 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -235,15 +235,15 @@ Section TRANSF_PROGRAM. Variable A B V: Type. Variable transf: ident -> A -> B. -Definition transform_program_globdef (idg: ident * globdef A V) : ident * globdef B V := +Definition transform_program_globdef' (idg: ident * globdef A V) : ident * globdef B V := match idg with | (id, Gfun f) => (id, Gfun (transf id f)) | (id, Gvar v) => (id, Gvar v) end. -Definition transform_program (p: AST.program A V) : AST.program B V := +Definition transform_program' (p: AST.program A V) : AST.program B V := mkprogram - (List.map transform_program_globdef p.(prog_defs)) + (List.map transform_program_globdef' p.(prog_defs)) p.(prog_public) p.(prog_main). -- cgit