diff options
Diffstat (limited to 'scheduling/RTLpathSE_theory.v')
-rw-r--r-- | scheduling/RTLpathSE_theory.v | 168 |
1 files changed, 117 insertions, 51 deletions
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v index 2a791feb..74f90b0e 100644 --- a/scheduling/RTLpathSE_theory.v +++ b/scheduling/RTLpathSE_theory.v @@ -126,6 +126,11 @@ 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 @@ -135,10 +140,7 @@ 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 -> @@ -457,6 +459,11 @@ 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' => @@ -474,11 +481,15 @@ 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 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 |} + 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 |} | _ => None end. @@ -510,6 +521,13 @@ 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. @@ -549,35 +567,46 @@ Proof. - left. constructor; eauto. eapply slocal_set_smem_preserves_sabort_local; eauto. - right. exists ext0, lx0. constructor; eauto. (* COND *) - * 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) + * 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) (si_smem (si_elocal ext)) rs m) eqn:SEVAL; [destruct b|]. - (* 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. + (* 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. } } Qed. Lemma siexec_inst_WF i st: siexec_inst i st = None -> default_succ i = None. Proof. - destruct i; simpl; unfold sist_set_local; simpl; congruence. + destruct i; simpl; try destruct Pos.eq_dec; 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; unfold sist_set_local; simpl; try congruence; + destruct i; simpl; try destruct Pos.eq_dec; unfold sist_set_local; simpl; try congruence; intro H; inversion_clear H; simpl; auto. Qed. @@ -594,7 +623,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: @@ -603,7 +632,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; simpl; auto. + destruct i eqn:INST; simpl; auto. + (* Nop *) constructor; [|constructor]; simpl; auto. constructor; auto. @@ -685,25 +714,55 @@ Proof. + (* COND *) Local Hint Resolve is_tail_refl: core. Local Hint Unfold ssem_local: core. - 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. + 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. erewrite seval_list_sval_inj; simpl; auto. - try_simplify_someHyps. - - intuition. unfold all_fallthrough in * |- *. simpl. - intuition. subst. simpl. + 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. unfold seval_condition. erewrite seval_list_sval_inj; simpl; auto. - 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. } + try_simplify_someHyps. } } Qed. @@ -713,7 +772,8 @@ 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_simplify_someHyps. + destruct i; simpl; unfold sist_set_local, ssem_internal, ssem_local; simpl; + try destruct Pos.eq_dec; try_simplify_someHyps. Qed. (** * Symbolic execution of the internal steps of a path *) @@ -730,7 +790,8 @@ 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_clear SISTEP; unfold siexec_inst; simpl; (discriminate || eauto). + destruct i; simpl; intro SISTEP; inversion SISTEP; unfold siexec_inst; simpl; + try destruct Pos.eq_dec; try_simplify_someHyps. Qed. Lemma siexec_inst_preserves_allfu ge sp ext lx rs0 m0 st st' i: @@ -740,7 +801,8 @@ 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_clear SISTEP; simpl; (discriminate || eauto). + destruct i; simpl in SISTEP; inversion SISTEP; simpl; + try destruct Pos.eq_dec; try_simplify_someHyps. Qed. Lemma siexec_path_correct_false ge sp f rs0 m0 st' is: @@ -819,6 +881,9 @@ 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. @@ -1079,7 +1144,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 |- *; unfold sist_set_local in Hi; try congruence. + + (* Snone *) intro Hi; destruct i; simpl in Hi |- *; try destruct Pos.eq_dec in *; unfold sist_set_local in Hi; try congruence. + (* Icall *) intros; eapply exec_Scall; auto. - destruct ros; simpl in * |- *; auto. rewrite REG; auto. @@ -1126,11 +1191,13 @@ 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. @@ -1464,7 +1531,6 @@ 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'). |