From f6bf6fcb22cc2b4e9e71e5229ed2adbb8cc277c0 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 23 Apr 2020 17:57:58 +0200 Subject: [BROKEN] Added wf predicate sistate - simatch_exclude_abort proven, need to modify some functions --- mppa_k1c/lib/RTLpathSE_theory.v | 198 ++++++++++++++++++++++++---------------- 1 file changed, 121 insertions(+), 77 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index e38e66dd..c503936b 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -110,24 +110,32 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop := exists ext, List.In ext lx /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None. - -Inductive simatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop := - simatch_exits_intro ext lx': - is_tail (ext::lx') lx -> - all_fallthrough ge sp lx' rs0 m0 -> - seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = Some true -> - simatch_local ge sp ext.(si_elocal) rs0 m0 rs m -> - ext.(si_ifso) = pc -> - simatch_exits ge sp lx rs0 m0 rs m pc. - +Inductive simatch_exits (ge: RTL.genv) (sp: val) (lx: list sistate_exit) (rs: regset) (m: mem) rs' m' (pc': node) : Prop := + simatch_exits_intro: forall ext lx', + lx = ext::lx' -> + all_fallthrough ge sp lx' rs m -> + seval_condition ge sp (si_cond ext) (si_scondargs ext) ext.(si_elocal).(si_smem) rs m = Some true -> + simatch_local ge sp (si_elocal ext) rs m rs' m' -> + (si_ifso ext) = pc' -> + simatch_exits ge sp lx rs m rs' m' pc'. + +(* Ensuring there isn't more sistate_local after taking a branch *) +Inductive simatch_exits_bind (ext: sistate_exit) (loc: sistate_local) : Prop := + simatch_exits_bind_intro: + (forall ge sp lx rs m rs' m' pc', simatch_exits ge sp (ext::lx) rs m rs' m' pc' -> si_elocal ext = loc) -> + simatch_exits_bind ext loc. + +Definition sistate_wf exits loc := + exists ext lx, exits = ext::lx /\ simatch_exits_bind ext loc. (** * Syntax and Semantics of symbolic internal state *) -Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. +Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local; + si_wf: sistate_wf si_exits si_local }. Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop := if (is.(icontinue)) then - simatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) + simatch_local ge sp st.(si_local) rs0 m0 is.(irs) is.(imem) /\ st.(si_pc) = is.(ipc) /\ all_fallthrough ge sp st.(si_exits) rs0 m0 else simatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc). @@ -162,7 +170,7 @@ Definition istate_eq ist1 ist2 := (* TODO: is it useful Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0: - all_fallthrough ge sp (ext::lx) rs0 m0 <-> + all_fallthrough ge sp (ext::lx) rs0 m0 <-> (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(si_smem) rs0 m0 = Some false /\ all_fallthrough ge sp lx rs0 m0). Proof. unfold all_fallthrough; simpl; intuition (subst; auto). @@ -177,7 +185,7 @@ Proof. Local Hint Resolve is_tail_in: core. destruct 1 as [ext lx' lc NYE' EVAL SEM PC]. subst. unfold all_fallthrough; intros NYE; rewrite NYE in EVAL; eauto. - try congruence. + try congruence. rewrite lc. econstructor; eauto. Qed. Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2: @@ -249,9 +257,9 @@ Proof. Local Hint Resolve exit_cond_determ eq_sym: core. destruct 1 as [ext1 lx1 TAIL1 NYE1 EVAL1 SEM1 PC1]; subst. destruct 1 as [ext2 lx2 TAIL2 NYE2 EVAL2 SEM2 PC2]; subst. - assert (X:ext1=ext2). - - destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. - - subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. + assert (X:ext1=ext2) by congruence. +(*{ destruct (is_tail_bounded_total (ext1 :: lx1) (ext2::lx2) lx) as [TAIL|TAIL]; eauto. } *) + subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. Qed. Lemma simatch_determ ge sp st rs m is1 is2: @@ -270,58 +278,94 @@ Proof. intuition. Qed. -Lemma simatch_exclude_sabort_local_continue ge sp st rs m is: - icontinue is = true -> +Lemma simatch_local_exclude_sabort_local ge sp st rs m rs' m': + simatch_local ge sp (si_local st) rs m rs' m' -> + all_fallthrough ge sp (si_exits st) rs m -> sabort_local ge sp (si_local st) rs m -> - simatch ge sp st rs m is -> False. + False. Proof. - intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM. - destruct SEM as (SEML & _ & _). inversion SEML as (SEML1 & SEML2 & SEML3); clear SEML. - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT. - - contradiction. - - rewrite SEML2 in ABORT2. discriminate. - - inv ABORT3. rewrite SEML3 in H. discriminate. + intros SIML ALLF ABORT. inv SIML. destruct H0 as (H0 & H0'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. Qed. -Lemma simatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is: - icontinue is = false -> - sabort_local ge sp (si_local st) rs0 m0 -> - simatch ge sp st rs0 m0 is -> False. +Lemma simatch_local_exclude_sabort_exits ge sp st rs m rs' m': + simatch_local ge sp (si_local st) rs m rs' m' -> + all_fallthrough ge sp (si_exits st) rs m -> + sabort_exits ge sp (si_exits st) rs m -> + False. Proof. -(* intros CONT ABORT SEM. unfold simatch in SEM. rewrite CONT in SEM. - destruct st as [pc si_exits iis]. simpl in *. - destruct is as [cont pc' rs' m']. simpl in *. - inv SEM. inversion H2 as (SEML1 & SEML2 & SEML3); clear H2. - inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; clear ABORT. - - Search iis. - - rewrite SEML2 in ABORT2. discriminate. - - inv ABORT3. rewrite SEML3 in H. discriminate. *) -Admitted. + intros SIML ALLF ABORT. inv ABORT. inv H. + unfold all_fallthrough in ALLF. apply ALLF in H0. congruence. +Qed. +Lemma simatch_local_exclude_sabort ge sp st rs m rs' m': + simatch_local ge sp (si_local st) rs m rs' m' -> + all_fallthrough ge sp (si_exits st) rs m -> + sabort ge sp st rs m -> + False. +Proof. + intros SIML ALLF ABORT. + inv ABORT. + - eapply simatch_local_exclude_sabort_local; eauto. + - eapply simatch_local_exclude_sabort_exits; eauto. +Qed. -Lemma simatch_exclude_sabort_local ge sp st rs m is: +Lemma simatch_exits_exclude_sabort_local ge sp st rs m rs' m' pc': + simatch_exits ge sp (si_exits st) rs m rs' m' pc' -> sabort_local ge sp (si_local st) rs m -> - simatch ge sp st rs m is -> False. + False. Proof. - intros. destruct (icontinue is) eqn:CONT. - - eapply simatch_exclude_sabort_local_continue; eauto. - - eapply simatch_exclude_sabort_local_nocontinue; eauto. + destruct st as [spc exits loc SISTWF]. simpl. + intros SIMEX ABORT. inv SISTWF. inv H. inv H0. + inversion SIMEX. subst. inv H. + inv H1. eapply H in SIMEX. subst. clear H. + inv H3. destruct H1 as (H1 & H1'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. Qed. -Lemma simatch_exclude_sabort_exits ge sp st rs m is: - sabort_exits ge sp (si_exits st) rs m -> - simatch ge sp st rs m is -> False. +(* Weaker version if we don't have the simatch_exits_bind - not used anymore, couldn't get any use from it *) +Remark simatch_exits_exclude_sabort_local' ge sp rs m rs' m' pc' exits ext: + simatch_exits ge sp (ext::exits) rs m rs' m' pc' -> + sabort_local ge sp (si_elocal ext) rs m -> + False. Proof. -Admitted. + intros SIMEX ABORT. + inv SIMEX. inv H. inv H2. destruct H3 as (H3 & H3'). + inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence. +Qed. + +Lemma simatch_exits_exclude_sabort_exits ge sp exits rs m rs' m' pc': + simatch_exits ge sp exits rs m rs' m' pc' -> + sabort_exits ge sp exits rs m -> + False. +Proof. + intros SIMEX ABORT. + inv ABORT. inv H. inv SIMEX. unfold all_fallthrough in H2. + inv H0. + - congruence. + - apply H2 in H. congruence. +Qed. + +Lemma simatch_exits_exclude_sabort ge sp st rs m rs' m' pc': + simatch_exits ge sp (si_exits st) rs m rs' m' pc' -> + sabort ge sp st rs m -> + False. +Proof. + intros SIME ABORT. + inv ABORT. + - eapply simatch_exits_exclude_sabort_local; eauto. + - eapply simatch_exits_exclude_sabort_exits; eauto. +Qed. Lemma simatch_exclude_sabort ge sp st rs m is: sabort ge sp st rs m -> simatch ge sp st rs m is -> False. Proof. intros ABORT SEM. - inv ABORT. - - eapply simatch_exclude_sabort_local; eauto. - - eapply simatch_exclude_sabort_exits; eauto. + unfold simatch in SEM. destruct icontinue. + - destruct SEM as (SEM1 & SEM2 & SEM3). + eapply simatch_local_exclude_sabort; eauto. + - eapply simatch_exits_exclude_sabort; eauto. Qed. Definition istate_eq_opt ist1 oist := @@ -353,7 +397,7 @@ Definition sist_set_local (st: sistate) (pc: node) (nxt: sistate_local): option Some {| si_pc := pc; si_exits := st.(si_exits); si_local:= nxt |}. (* FIXME - add notrap *) -Definition sistep (i: instruction) (st: sistate): option sistate := +Definition sistep (i: instruction) (st: sistate): option sistate := match i with | Inop pc' => sist_set_local st pc' st.(si_local) @@ -420,7 +464,7 @@ Proof. unfold sabort_local. simpl; intuition. Qed. -Lemma sistep_preserves_sabort i ge sp rs0 m0 st st': +Lemma sistep_preserves_sabort i ge sp rs0 m0 st st': sistep i st = Some st' -> sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0. Proof. @@ -463,7 +507,7 @@ Proof. subst; rewrite Regmap.gss; simpl; auto. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. - - unfold sabort, sabort_local; simpl. + - unfold sabort, sabort_local; simpl. left. right. right. exists r. destruct (Pos.eq_dec r r); try congruence. simpl. erewrite seval_list_sval_inj; simpl; auto. @@ -482,7 +526,7 @@ Proof. exists r. destruct (Pos.eq_dec r r); try congruence. simpl. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. } - { unfold sabort, sabort_local; simpl. + { unfold sabort, sabort_local; simpl. left. right. right. exists r. destruct (Pos.eq_dec r r); try congruence. simpl. erewrite seval_list_sval_inj; simpl; auto. @@ -527,7 +571,7 @@ Admitted. Lemma sistep_correct_None ge sp i st rs0 m0 rs m: simatch_local ge sp (st.(si_local)) rs0 m0 rs m -> - sistep i st = None -> + sistep i st = None -> istep ge i sp rs m = None. Proof. intros (PRE & MEM & REG). @@ -544,9 +588,9 @@ Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate := sisteps p f st1 end. -Lemma sisteps_correct_false ge sp path f rs0 m0 st' is: +Lemma sisteps_correct_false ge sp path f rs0 m0 st' is: is.(icontinue)=false -> - forall st, simatch ge sp st rs0 m0 is -> + forall st, simatch ge sp st rs0 m0 is -> sisteps path f st = Some st' -> simatch ge sp st' rs0 m0 is. Proof. @@ -558,7 +602,7 @@ Proof. inversion_SOME st1; eauto. Qed. -Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st, +Lemma sisteps_preserves_sabort ge sp path f rs0 m0 st': forall st, sisteps path f st = Some st' -> sabort ge sp st rs0 m0 -> sabort ge sp st' rs0 m0. Proof. @@ -592,7 +636,7 @@ Qed. Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is, is.(icontinue)=true -> - simatch ge sp st rs0 m0 is -> + simatch ge sp st rs0 m0 is -> nth_default_succ (fn_code f) path st.(si_pc) <> None -> simatch_opt2 ge sp (sisteps path f st) rs0 m0 (isteps ge path f sp is.(irs) is.(imem) is.(ipc)) @@ -608,7 +652,7 @@ Proof. intros (LOCAL & PC & NYE) WF. rewrite <- PC. inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto. - exploit sistep_correct; eauto. + exploit sistep_correct; eauto. inversion_SOME st1; intros Hst1; erewrite Hst1; simpl. - inversion_SOME is1; intros His1;rewrite His1; simpl. * destruct (icontinue is1) eqn:CONT1. @@ -707,7 +751,7 @@ Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stac sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> match osv with Some sv => seval_sval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> - sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m + sfmatch pge ge sp st stack f rs0 m0 (Sreturn osv) rs m E0 (Returnstate stack v m') . @@ -716,17 +760,17 @@ Record sstate := { internal:> sistate; final: sfval }. Inductive smatch pge (ge: RTL.genv) (sp:val) (st: sstate) stack f (rs0: regset) (m0: mem): trace -> state -> Prop := | smatch_early is: is.(icontinue) = false -> - simatch ge sp st rs0 m0 is -> + simatch ge sp st rs0 m0 is -> smatch pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(ipc) is.(irs) is.(imem)) | smatch_normal is t s: is.(icontinue) = true -> - simatch ge sp st rs0 m0 is -> + simatch ge sp st rs0 m0 is -> sfmatch pge ge sp st stack f rs0 m0 st.(final) is.(irs) is.(imem) t s -> - smatch pge ge sp st stack f rs0 m0 t s + smatch pge ge sp st stack f rs0 m0 t s . (** * Symbolic execution of final step *) -Definition sfstep (i: instruction) (prev: sistate_local): sfval := +Definition sfstep (i: instruction) (prev: sistate_local): sfval := match i with | Icall sig ros args res pc => let svos := sum_left_map prev.(si_sreg) ros in @@ -743,7 +787,7 @@ Lemma sfstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s: pc = st.(si_pc) -> simatch_local ge sp (si_local st) rs0 m0 rs m -> path_last_step ge pge stack f sp pc rs m t s -> - sistep i st = None -> + sistep i st = None -> sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s. Proof. intros PC1 PC2 (PRE&MEM®) LAST Hi. destruct LAST; subst; try_simplify_someHyps; simpl. @@ -818,9 +862,9 @@ Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: pc = st.(si_pc) -> sistep i st = Some st' -> path_last_step ge pge stack f sp pc rs m t s -> - exists mk_istate, - istep ge i sp rs m = Some mk_istate - /\ t = E0 + exists mk_istate, + istep ge i sp rs m = Some mk_istate + /\ t = E0 /\ s = (State stack f sp mk_istate.(ipc) mk_istate.(RTLpath.irs) mk_istate.(imem)). Proof. intros PC1 PC2 Hst' LAST; destruct LAST; subst; try_simplify_someHyps; simpl. @@ -829,7 +873,7 @@ Qed. (* NB: each concrete execution can be executed on the symbolic state (produced from [sstep]) (sstep is a correct over-approximation) *) -Theorem sstep_correct f pc pge ge sp path stack rs m t s: +Theorem sstep_correct f pc pge ge sp path stack rs m t s: (fn_path f)!pc = Some path -> path_step ge pge path.(psize) stack f sp rs m pc t s -> exists st, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s. @@ -846,7 +890,7 @@ Proof. (* intro SEM *) (simpl; unfold simatch; simpl; rewrite CONT; intro SEM); (* intro Hi' *) - ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); + ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); [ unfold nth_default_succ_inst in Hi; exploit sisteps_default_succ; eauto; simpl; intros DEF; rewrite DEF in Hi; auto @@ -963,9 +1007,9 @@ Qed. (* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution (sstep is exact). *) -Theorem sstep_exact f pc pge ge sp path stack st rs m t s1: +Theorem sstep_exact f pc pge ge sp path stack st rs m t s1: (fn_path f)!pc = Some path -> - sstep f pc = Some st -> + sstep f pc = Some st -> smatch pge ge sp st stack f rs m t s1 -> exists s2, path_step ge pge path.(psize) stack f sp rs m pc t s2 /\ equiv_state s1 s2. @@ -1087,7 +1131,7 @@ Definition istate_simu f (srce: PTree.t node) is1 is2: Prop := sur la dernière instruction du superblock. *) istate_simulive (fun _ => True) srce is1 is2 else - exists path, f.(fn_path)!(is1.(ipc)) = Some path + exists path, f.(fn_path)!(is1.(ipc)) = Some path /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2 /\ srce!(is2.(ipc)) = Some is1.(ipc). @@ -1096,7 +1140,7 @@ Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sis forall sp ge1 ge2, (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) -> liveness_ok_function f -> - forall rs m is1, simatch ge1 sp st1 rs m is1 -> + forall rs m is1, simatch ge1 sp st1 rs m is1 -> exists is2, simatch ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2. (* NOTE: a syntactic definition on [sfval] in order to abstract the [match_states] *) @@ -1115,7 +1159,7 @@ Definition sstate_simu f srce (s1 s2: sstate): Prop := /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final). Definition sstep_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop := - forall st1, sstep f1 pc1 = Some st1 -> + forall st1, sstep f1 pc1 = Some st1 -> exists st2, sstep f2 pc2 = Some st2 /\ sstate_simu f1 srce st1 st2. (* IDEA: we will provide an efficient test for checking "sstep_simu" property, by hash-consing. -- cgit