diff options
Diffstat (limited to 'scheduling/RTLpathSE_theory.v')
| -rw-r--r-- | scheduling/RTLpathSE_theory.v | 168 |
1 files changed, 51 insertions, 117 deletions
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index 74f90b0e..2a791feb 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -126,11 +126,6 @@ Definition ssem_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) /\ seval_smem ge sp st.(si_smem) rs0 m0 = Some m /\ forall (r:reg), seval_sval ge sp (st.(si_sreg) r) rs0 m0 = Some (rs#r). -Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool := - SOME args <- seval_list_sval ge sp lsv rs0 m0 IN - SOME m <- seval_smem ge sp sm rs0 m0 IN - eval_condition cond args m. - Definition sabort_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem): Prop := ~(st.(si_pre) ge sp rs0 m0) \/ seval_smem ge sp st.(si_smem) rs0 m0 = None @@ -140,7 +135,10 @@ Definition sabort_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset Record sistate_exit := mk_sistate_exit { si_cond: condition; si_scondargs: list_sval; si_elocal: sistate_local; si_ifso: node }. - +Definition seval_condition ge sp (cond: condition) (lsv: list_sval) (sm: smem) rs0 m0 : option bool := + SOME args <- seval_list_sval ge sp lsv rs0 m0 IN + SOME m <- seval_smem ge sp sm rs0 m0 IN + eval_condition cond args m. Definition all_fallthrough ge sp (lx: list sistate_exit) rs0 m0: Prop := forall ext, List.In ext lx -> @@ -459,11 +457,6 @@ Definition slocal_store st chunk addr args src : sistate_local := let sm := Sstore (si_smem st) chunk addr args src in slocal_set_smem st sm. -Definition slocal_eval_cond (st:sistate_local) (cond : condition) (args : list_sval) := - {| si_pre:=(fun ge sp rs m => seval_condition ge sp cond args st.(si_smem) rs m <> None /\ (st.(si_pre) ge sp rs m)); - si_sreg:=st.(si_sreg); - si_smem:= st.(si_smem) |}. - Definition siexec_inst (i: instruction) (st: sistate): option sistate := match i with | Inop pc' => @@ -481,15 +474,11 @@ Definition siexec_inst (i: instruction) (st: sistate): option sistate := | Istore chunk addr args src pc' => let next := slocal_store st.(si_local) chunk addr args src in Some (sist_set_local st pc' next) - | Icond cond args ifso ifnot _ => + | Icond cond args ifso ifnot _ => let prev := st.(si_local) in let vargs := list_sval_inj (List.map prev.(si_sreg) args) in - let next := slocal_eval_cond prev cond vargs in - if Pos.eq_dec ifso ifnot then - Some (sist_set_local st ifnot next) - else - let ex := {| si_cond:=cond; si_scondargs:=vargs; si_elocal := next; si_ifso := ifso |} in - Some {| si_pc := ifnot; si_exits := ex::st.(si_exits); si_local := next |} + 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 end. @@ -521,13 +510,6 @@ Proof. unfold sabort_local. simpl; intuition. Qed. -Lemma slocal_eval_cond_preserves_sabort_local ge sp st rs0 m0 cond args: - sabort_local ge sp st rs0 m0 -> - sabort_local ge sp (slocal_eval_cond st cond args) rs0 m0. -Proof. - unfold sabort_local. simpl; intuition. -Qed. - Lemma all_fallthrough_upto_exit_cons ge sp ext lx ext' exits rs m: all_fallthrough_upto_exit ge sp ext lx exits rs m -> all_fallthrough_upto_exit ge sp ext lx (ext'::exits) rs m. @@ -567,46 +549,35 @@ Proof. - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto. - right. exists ext0, lx0. constructor; eauto. (* COND *) - * destruct Pos.eq_dec; simpl in *. - { (* "Useless if" (two identical successors) *) - destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - - left; constructor; try_simplify_someHyps; - apply slocal_eval_cond_preserves_sabort_local; auto. - - right; exists ext0, lx0; try_simplify_someHyps. } - { (* Normal Icond *) - remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext. - destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. - { destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext) + * remember ({| si_cond := _; si_scondargs := _; si_elocal := _; si_ifso := _ |}) as ext. + destruct ABORT as [(ALLF & ABORTL) | (ext0 & lx0 & ALLFU & ABORTE)]. + - destruct (seval_condition ge sp (si_cond ext) (si_scondargs ext) (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|]. - (* case true *) - - right. exists ext, (si_exits st). - split. - + constructor; auto; inversion H0; constructor. - + unfold sabort_exit; right; constructor; auto. - subst; simpl in *; auto. - apply slocal_eval_cond_preserves_sabort_local; assumption. - (* case false *) - - left. constructor; eauto; inversion H0; simpl. - + apply all_fallthrough_cons; auto. - + apply slocal_eval_cond_preserves_sabort_local; auto. - (* case None *) - - right. exists ext, (si_exits st). constructor. - + constructor; auto; inversion H0; constructor. - + unfold sabort_exit; intuition. } - { right. exists ext0, lx0. constructor; eauto. - inversion H0; simpl. eapply all_fallthrough_upto_exit_cons; eauto. } } + (* case true *) + + right. exists ext, (si_exits st). + constructor. + ++ constructor. econstructor; eauto. eauto. + ++ unfold sabort_exit. right. constructor; eauto. + subst. simpl. eauto. + (* case false *) + + left. constructor; eauto. eapply all_fallthrough_cons; eauto. + (* case None *) + + right. exists ext, (si_exits st). constructor. + ++ constructor. econstructor; eauto. eauto. + ++ unfold sabort_exit. left. eauto. + - right. exists ext0, lx0. constructor; eauto. eapply all_fallthrough_upto_exit_cons; eauto. Qed. Lemma siexec_inst_WF i st: siexec_inst i st = None -> default_succ i = None. Proof. - destruct i; simpl; try destruct Pos.eq_dec; unfold sist_set_local; simpl; congruence. + destruct i; simpl; unfold sist_set_local; simpl; congruence. Qed. Lemma siexec_inst_default_succ i st st': siexec_inst i st = Some st' -> default_succ i = Some (st'.(si_pc)). Proof. - destruct i; simpl; try destruct Pos.eq_dec; unfold sist_set_local; simpl; try congruence; + destruct i; simpl; unfold sist_set_local; simpl; try congruence; intro H; inversion_clear H; simpl; auto. Qed. @@ -623,7 +594,7 @@ Proof. assert (forall r : reg, In r l -> seval_sval ge sp (si_sreg st r) rs0 m0 = None -> False). { intros r INR. eapply ALLR. right. assumption. } intro SVALLIST. intro. eapply IHl; eauto. - + intros. exploit (ALLR a); simpl; eauto. + + intros. exploit (ALLR a); simpl; eauto. Qed. Lemma siexec_inst_correct ge sp i st rs0 m0 rs m: @@ -632,7 +603,7 @@ Lemma siexec_inst_correct ge sp i st rs0 m0 rs m: ssem_internal_opt2 ge sp (siexec_inst i st) rs0 m0 (istep ge i sp rs m). Proof. intros (PRE & MEM & REG) NYE. - destruct i eqn:INST; simpl; auto. + destruct i; simpl; auto. + (* Nop *) constructor; [|constructor]; simpl; auto. constructor; auto. @@ -714,55 +685,25 @@ Proof. + (* COND *) Local Hint Resolve is_tail_refl: core. Local Hint Unfold ssem_local: core. - destruct Pos.eq_dec. - { (* Useless if *) - subst; destruct eval_condition eqn:EV_COND. - - constructor; simpl; intuition. 2: { destruct b; auto. } constructor; intuition. - unfold slocal_eval_cond; try_simplify_someHyps. - unfold seval_condition; erewrite seval_list_sval_inj; simpl; auto. - inversion_SOME m'; intros; assert (m' = m) by congruence; subst. - rewrite EV_COND; intuition; discriminate. - - simpl; unfold sabort; simpl; left; intuition. - unfold sabort_local; simpl; unfold seval_condition. + inversion_SOME b; intros COND. + { destruct b; simpl; unfold ssem_internal, ssem_local; simpl. + - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). + constructor; constructor; subst; simpl; auto. + unfold seval_condition. subst; simpl. erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps; intuition. } - { (* Normal Icond *) - inversion_SOME b; intros COND. - { (* eval_condition did not fail *) - destruct b; simpl; unfold ssem_internal, ssem_local; simpl. - - (* Case true *) - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). - split. 2: { constructor; auto. } - constructor. - 2: { constructor; subst; simpl; auto. - constructor; auto. unfold slocal_eval_cond; simpl. - constructor; auto. - unfold seval_condition. - erewrite seval_list_sval_inj; auto. - rewrite MEM; congruence. } - unfold seval_condition. - subst; simpl. - erewrite seval_list_sval_inj; simpl; auto. - rewrite MEM. assumption. - - (* Case false *) - intuition. - + unfold all_fallthrough in * |- *. - try_simplify_someHyps. - unfold seval_condition; erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps; discriminate. - + unfold all_fallthrough in * |- *. simpl. - intuition. subst. simpl. - unfold seval_condition. - erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. } - { (* Case None (eval_condition failed) *) - unfold sabort. simpl. right. - remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). - constructor; [constructor; subst; simpl; auto|]. - left. subst; simpl; auto. + try_simplify_someHyps. + - intuition. unfold all_fallthrough in * |- *. simpl. + intuition. subst. simpl. unfold seval_condition. erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. } } + try_simplify_someHyps. } + { unfold sabort. simpl. right. + remember (mk_sistate_exit _ _ _ _) as ext. exists ext, (si_exits st). + constructor; [constructor; subst; simpl; auto|]. + left. subst; simpl; auto. + unfold seval_condition. + erewrite seval_list_sval_inj; simpl; auto. + try_simplify_someHyps. } Qed. @@ -772,8 +713,7 @@ Lemma siexec_inst_correct_None ge sp i st rs0 m0 rs m: istep ge i sp rs m = None. Proof. intros (PRE & MEM & REG). - destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; - try destruct Pos.eq_dec; try_simplify_someHyps. + destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; try_simplify_someHyps. Qed. (** * Symbolic execution of the internal steps of a path *) @@ -790,8 +730,7 @@ Lemma siexec_inst_add_exits i st st': siexec_inst i st = Some st' -> ( si_exits st' = si_exits st \/ exists ext, si_exits st' = ext :: si_exits st ). Proof. - destruct i; simpl; intro SISTEP; inversion SISTEP; unfold siexec_inst; simpl; - try destruct Pos.eq_dec; try_simplify_someHyps. + destruct i; simpl; intro SISTEP; inversion_clear SISTEP; unfold siexec_inst; simpl; (discriminate || eauto). Qed. Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i: @@ -801,8 +740,7 @@ Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i: Proof. intros ALLFU SISTEP. destruct ALLFU as (ISTAIL & ALLF). constructor; eauto. - destruct i; simpl in SISTEP; inversion SISTEP; simpl; - try destruct Pos.eq_dec; try_simplify_someHyps. + destruct i; simpl in SISTEP; inversion_clear SISTEP; simpl; (discriminate || eauto). Qed. Lemma siexec_path_correct_false ge sp f rs0 m0 st' is: @@ -881,9 +819,6 @@ Proof. (* icontinue is0 = true *) intros; eapply IHpath; eauto. destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps. - { destruct Pos.eq_dec; simpl. - { intros. inversion Hst1. simpl; auto. } - { intros. inversion Hst1. simpl; auto. } } (* icontinue is0 = false -> EARLY EXIT *) destruct (siexec_path path f st1) as [st2|] eqn: Hst2; simpl; eauto. destruct WF. erewrite siexec_inst_default_succ; eauto. @@ -1144,7 +1079,7 @@ Lemma sexec_final_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s: ssem_final pge ge sp pc stack f rs0 m0 (sexec_final i (si_local st)) rs m t s. Proof. intros PC1 PC2 (PRE&MEM®) LAST. destruct LAST; subst; try_simplify_someHyps; simpl. - + (* Snone *) intro Hi; destruct i; simpl in Hi |- *; try destruct Pos.eq_dec in *; unfold sist_set_local in Hi; try congruence. + + (* Snone *) intro Hi; destruct i; simpl in Hi |- *; unfold sist_set_local in Hi; try congruence. + (* Icall *) intros; eapply exec_Scall; auto. - destruct ros; simpl in * |- *; auto. rewrite REG; auto. @@ -1191,13 +1126,11 @@ Proof. + (* Ibuiltin *) intros HPC SMEM. eapply exec_Ibuiltin; eauto. eapply seval_builtin_args_complete; eauto. - + (* Icond *) intros HPC SMEM. - destruct Pos.eq_dec in HPC; try discriminate. + (* Ijumptable *) intros HPC SMEM. - eapply exec_Ijumptable; eauto; congruence. + eapply exec_Ijumptable; eauto. + congruence. + (* Ireturn *) - intros; subst. - enough (v=regmap_optget or Vundef rs) as ->. + intros; subst. enough (v=regmap_optget or Vundef rs) as ->. * eapply exec_Ireturn; eauto. * intros; destruct or; simpl; congruence. Qed. @@ -1531,6 +1464,7 @@ Proof. destruct (icontinue is) eqn:ICONT. { destruct SEM as (SEML & SIPC & ALLF). exploit siexec_inst_early_exit_absurd; eauto. contradiction. } + eexists. econstructor 1. *** eapply exec_early_exit; eauto. *** destruct ISTEPS as (ext & lx & SSEME & ALLFU). destruct SEM as (ext' & lx' & SSEME' & ALLFU'). |