From b0452edc5e911d8585a691ad4e530d4f1427f463 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 22 Feb 2021 16:09:53 +0100 Subject: a bit more cleaning --- scheduling/RTLpathLivegen.v | 17 +++++++++++++++-- scheduling/RTLpathSE_impl.v | 2 +- scheduling/RTLpathSE_theory.v | 22 ++-------------------- scheduling/RTLpathSchedulerproof.v | 21 ++------------------- scheduling/RTLpathWFcheck.v | 3 +-- 5 files changed, 21 insertions(+), 44 deletions(-) diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 7855d375..9f646ad0 100644 --- a/scheduling/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v @@ -46,7 +46,6 @@ Proof. inversion_ASSERT; try_simplify_someHyps. Qed. -(* FIXME - what about trap? *) Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) := match i with | Inop pc' => Some (alive, pc') @@ -63,7 +62,7 @@ Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): opti | Icond cond args ifso ifnot _ => ASSERT list_mem args alive IN exit_checker pm alive ifso (alive, ifnot) - | _ => None (* TODO jumptable ? *) + | _ => None end. @@ -109,6 +108,20 @@ Proof. * intros; eapply iinst_checker_path_entry; eauto. Qed. + +Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res, + ipath_checker path f (fn_path f) alive pc = Some res + -> nth_default_succ (fn_code f) path pc = Some (snd res). +Proof. + induction path; simpl. + + try_simplify_someHyps. + + intros alive pc res. + inversion_SOME i; intros INST. + inversion_SOME res0; intros ICHK IPCHK. + rewrite INST. + erewrite iinst_checker_default_succ; eauto. +Qed. + Definition reg_option_mem (or: option reg) (alive: Regset.t) := match or with None => true | Some r => Regset.mem r alive end. diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v index bd26171d..bdd4bda8 100644 --- a/scheduling/RTLpathSE_impl.v +++ b/scheduling/RTLpathSE_impl.v @@ -764,7 +764,7 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) : DO vargs <~ hlist_args prev args ;; let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |}) - | _ => RET None (* TODO jumptable ? *) + | _ => RET None end. diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index eec0bc51..aa8db342 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -345,31 +345,13 @@ Qed. Lemma ssem_local_exclude_sabort_local ge sp loc rs m rs' m': ssem_local ge sp loc rs m rs' m' -> -(* all_fallthrough ge sp (si_exits st) rs m -> *) sabort_local ge sp loc rs m -> False. Proof. - intros SIML (* ALLF *) ABORT. inv SIML. destruct H0 as (H0 & H0'). + intros SIML ABORT. inv SIML. destruct H0 as (H0 & H0'). inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. Qed. -(* TODO: remove this JUNK ? -Lemma ssem_local_exclude_sabort_exit ge sp st ext lx rs m rs' m': - ssem_local ge sp (si_local st) rs m rs' m' -> - all_fallthrough ge sp (si_exits st) rs m -> - is_tail (ext :: lx) (si_exits st) -> - sabort_exit ge sp ext rs m -> - False. -Proof. - intros SSEML ALLF TAIL ABORT. - inv ABORT. - - exploit ALLF; eauto. congruence. - - (* FIXME Problem : if we have a ssem_local, this means we ONLY evaluated the conditions, - but we NEVER actually evaluated the si_elocal from the sistate_exit ! So we cannot prove - a lack of abort on the si_elocal.. We must change the definitions *) -Abort. -*) - Lemma ssem_local_exclude_sabort ge sp st rs m rs' m': ssem_local ge sp (si_local st) rs m rs' m' -> all_fallthrough ge sp (si_exits st) rs m -> @@ -497,7 +479,7 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := let vargs := list_sval_inj (List.map prev.(si_sreg) args) in let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := prev; si_ifso := ifso |} in Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := prev |} - | _ => None (* TODO jumptable ? *) + | _ => None end. Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v index 72a4ee01..a9c2fa76 100644 --- a/scheduling/RTLpathSchedulerproof.v +++ b/scheduling/RTLpathSchedulerproof.v @@ -260,19 +260,6 @@ Proof. + rewrite <- H. erewrite <- seval_preserved; eauto. Qed. -Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res, - ipath_checker path f (fn_path f) alive pc = Some res - -> nth_default_succ (fn_code f) path pc = Some (snd res). -Proof. - induction path; simpl. - + try_simplify_someHyps. - + intros alive pc res. - inversion_SOME i; intros INST. - inversion_SOME res0; intros ICHK IPCHK. - rewrite INST. - erewrite iinst_checker_default_succ; eauto. -Qed. - Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone (irs is) (imem is) t s) @@ -331,17 +318,14 @@ Qed. Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs': (liveness_ok_function f) -> (fn_path f) ! pc0 = Some path0 -> - (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *) (* NB: should be useless *) sexec f pc0 = Some st -> - (* icontinue is = true -> *) list_forall2 match_stackframes stk stk' -> - (* ssem_internal ge sp st rs0 m0 is -> *) ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s -> eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' -> exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'. Proof. Local Hint Resolve eqlive_stacks_refl: core. - intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE. + intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE. (* start decomposing path_checker *) generalize (LIVE pc0 path0 PATH0). unfold path_checker. @@ -413,7 +397,6 @@ Qed. (* The main theorem on simulation of symbolic states ! *) Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: (fn_path f) ! pc0 = Some path0 -> - (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *) sexec f pc0 = Some st -> match_function dm f f' -> liveness_ok_function f -> @@ -422,7 +405,7 @@ Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) -> exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'. Proof. - intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU. + intros PATH0 SEXEC MFUNC LIVE STACKS SEM SIMU. destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU. destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *. - (* sem_early *) diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v index 0ddc3142..63b914ec 100644 --- a/scheduling/RTLpathWFcheck.v +++ b/scheduling/RTLpathWFcheck.v @@ -31,14 +31,13 @@ Proof. inversion_SOME path; try_simplify_someHyps. Qed. -(* FIXME - what about trap? *) Definition iinst_checker (pm: path_map) (i: instruction): option (node) := match i with | Inop pc' | Iop _ _ _ pc' | Iload _ _ _ _ _ pc' | Istore _ _ _ _ pc' => Some (pc') | Icond cond args ifso ifnot _ => exit_checker pm ifso ifnot - | _ => None (* TODO jumptable ? *) + | _ => None end. Local Hint Resolve exit_checker_path_entry: core. -- cgit