From fc113f5e7fc1a7d4baac9ea7f0d63ec2c2bdcb90 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 23 Apr 2020 12:15:51 +0200 Subject: Finished renaming --- mppa_k1c/lib/RTLpathSE_theory.v | 606 ++++++++++++++++++++-------------------- mppa_k1c/lib/RTLpathScheduler.v | 70 ++--- 2 files changed, 339 insertions(+), 337 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/lib/RTLpathSE_theory.v b/mppa_k1c/lib/RTLpathSE_theory.v index 9c0c0c0a..e38e66dd 100644 --- a/mppa_k1c/lib/RTLpathSE_theory.v +++ b/mppa_k1c/lib/RTLpathSE_theory.v @@ -83,7 +83,7 @@ with seval_smem (ge: RTL.genv) (sp:val) (sm: smem) (rs0: regset) (m0: mem): opti (* [si_pre] is a precondition on initial ge, sp, rs0, m0 *) Record sistate_local := { si_pre: RTL.genv -> val -> regset -> mem -> Prop; si_sreg: reg -> sval; si_smem: smem }. -Definition smatch_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := +Definition simatch_local (ge: RTL.genv) (sp:val) (st: sistate_local) (rs0: regset) (m0: mem) (rs: regset) (m: mem): Prop := st.(si_pre) ge sp rs0 m0 /\ 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). @@ -111,46 +111,46 @@ Definition sabort_exits ge sp (lx: list sistate_exit) rs0 m0: Prop := /\ seval_condition ge sp ext.(si_cond) ext.(si_scondargs) ext.(si_elocal).(si_smem) rs0 m0 = None. -Inductive smatch_exits (ge: RTL.genv) (sp:val) (lx:list sistate_exit) (rs0: regset) (m0: mem) rs m pc: Prop := - smatch_exits_intro ext lx': +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 -> - smatch_local ge sp ext.(si_elocal) rs0 m0 rs m -> + simatch_local ge sp ext.(si_elocal) rs0 m0 rs m -> ext.(si_ifso) = pc -> - smatch_exits ge sp lx rs0 m0 rs m pc. + simatch_exits ge sp lx rs0 m0 rs m pc. (** * Syntax and Semantics of symbolic internal state *) Record sistate := { si_pc: node; si_exits: list sistate_exit; si_local: sistate_local }. -Definition smatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop := +Definition simatch (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem) (is: istate): Prop := if (is.(icontinue)) then - smatch_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 smatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc). + else simatch_exits ge sp st.(si_exits) rs0 m0 is.(irs) is.(imem) is.(ipc). Definition sabort (ge: RTL.genv) (sp:val) (st: sistate) (rs0: regset) (m0: mem): Prop := sabort_local ge sp st.(si_local) rs0 m0 \/ sabort_exits ge sp st.(si_exits) rs0 m0. -Definition smatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop := +Definition simatch_opt ge sp (st: sistate) rs0 m0 (ois: option istate): Prop := match ois with - | Some is => smatch ge sp st rs0 m0 is + | Some is => simatch ge sp st rs0 m0 is | None => sabort ge sp st rs0 m0 end. -Definition smatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop := +Definition simatch_opt2 ge sp (ost: option sistate) rs0 m0 (ois: option istate) : Prop := match ost with - | Some st => smatch_opt ge sp st rs0 m0 ois + | Some st => simatch_opt ge sp st rs0 m0 ois | None => ois=None end. (** * An internal state represents a parallel program ! - We prove below that the semantics [sem_option_istate] is deterministic. + We prove below that the semantics [simatch_opt] is deterministic. *) @@ -162,15 +162,15 @@ Definition istate_eq ist1 ist2 := (* TODO: is it useful Lemma has_not_yet_exit_cons_split ge sp ext lx rs0 m0: - has_not_yet_exit ge sp (ext::lx) rs0 m0 <-> - (seval_condition ge sp ext.(the_cond) ext.(cond_args) ext.(exit_ist).(the_smem) rs0 m0 = Some false /\ has_not_yet_exit ge sp 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 has_not_yet_exit; simpl; intuition (subst; auto). + unfold all_fallthrough; simpl; intuition (subst; auto). Qed. *) Lemma all_fallthrough_noexit ge sp st rs0 m0 rs m pc: - smatch_exits ge sp (si_exits st) rs0 m0 rs m pc -> + simatch_exits ge sp (si_exits st) rs0 m0 rs m pc -> all_fallthrough ge sp (si_exits st) rs0 m0 -> False. Proof. @@ -180,37 +180,37 @@ Proof. try congruence. Qed. -Lemma smatch_exclude_incompatible_continue ge sp st rs m is1 is2: +Lemma simatch_exclude_incompatible_continue ge sp st rs m is1 is2: is1.(icontinue) = true -> is2.(icontinue) = false -> - smatch ge sp st rs m is1 -> - smatch ge sp st rs m is2 -> + simatch ge sp st rs m is1 -> + simatch ge sp st rs m is2 -> False. Proof. Local Hint Resolve all_fallthrough_noexit: core. - unfold smatch. + unfold simatch. intros CONT1 CONT2. rewrite CONT1, CONT2; simpl. intuition eauto. Qed. -Lemma smatch_determ_continue ge sp st rs m is1 is2: - smatch ge sp st rs m is1 -> - smatch ge sp st rs m is2 -> +Lemma simatch_determ_continue ge sp st rs m is1 is2: + simatch ge sp st rs m is1 -> + simatch ge sp st rs m is2 -> is1.(icontinue) = is2.(icontinue). Proof. - Local Hint Resolve smatch_exclude_incompatible_continue: core. + Local Hint Resolve simatch_exclude_incompatible_continue: core. destruct (Bool.bool_dec is1.(icontinue) is2.(icontinue)) as [|H]; auto. intros H1 H2. assert (absurd: False); intuition. destruct (icontinue is1) eqn: His1, (icontinue is2) eqn: His2; eauto. Qed. -Lemma smatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2: - smatch_local ge sp st rs0 m0 rs1 m1 -> - smatch_local ge sp st rs0 m0 rs2 m2 -> +Lemma simatch_local_determ ge sp st rs0 m0 rs1 m1 rs2 m2: + simatch_local ge sp st rs0 m0 rs1 m1 -> + simatch_local ge sp st rs0 m0 rs2 m2 -> (forall r, rs1#r = rs2#r) /\ m1 = m2. Proof. - unfold smatch_local. intuition try congruence. + unfold simatch_local. intuition try congruence. generalize (H5 r); rewrite H4; congruence. Qed. @@ -241,9 +241,9 @@ Proof. try congruence. Qed. -Lemma smatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 : - smatch_exits ge sp lx rs0 m0 rs1 m1 pc1 -> - smatch_exits ge sp lx rs0 m0 rs2 m2 pc2 -> +Lemma simatch_exits_determ ge sp lx rs0 m0 rs1 m1 pc1 rs2 m2 pc2 : + simatch_exits ge sp lx rs0 m0 rs1 m1 pc1 -> + simatch_exits ge sp lx rs0 m0 rs2 m2 pc2 -> pc1 = pc2 /\ (forall r, rs1#r = rs2#r) /\ m1 = m2. Proof. Local Hint Resolve exit_cond_determ eq_sym: core. @@ -251,31 +251,31 @@ Proof. 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 (smatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. + - subst. destruct (simatch_local_determ ge sp (si_elocal ext2) rs0 m0 rs1 m1 rs2 m2); auto. Qed. -Lemma smatch_determ ge sp st rs m is1 is2: - smatch ge sp st rs m is1 -> - smatch ge sp st rs m is2 -> +Lemma simatch_determ ge sp st rs m is1 is2: + simatch ge sp st rs m is1 -> + simatch ge sp st rs m is2 -> istate_eq is1 is2. Proof. unfold istate_eq. intros SEM1 SEM2. - exploit (smatch_determ_continue ge sp st rs m is1 is2); eauto. - intros CONTEQ. unfold smatch in * |-. rewrite CONTEQ in * |- *. + exploit (simatch_determ_continue ge sp st rs m is1 is2); eauto. + intros CONTEQ. unfold simatch in * |-. rewrite CONTEQ in * |- *. destruct (icontinue is2). - - destruct (smatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); + - destruct (simatch_local_determ ge sp (si_local st) rs m (irs is1) (imem is1) (irs is2) (imem is2)); intuition (try congruence). - - destruct (smatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2)); + - destruct (simatch_exits_determ ge sp (si_exits st) rs m (irs is1) (imem is1) (ipc is1) (irs is2) (imem is2) (ipc is2)); intuition. Qed. -Lemma smatch_exclude_sabort_local_continue ge sp st rs m is: +Lemma simatch_exclude_sabort_local_continue ge sp st rs m is: icontinue is = true -> sabort_local ge sp (si_local st) rs m -> - smatch ge sp st rs m is -> False. + simatch ge sp st rs m is -> False. Proof. - intros CONT ABORT SEM. unfold smatch in SEM. rewrite CONT in SEM. + 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. @@ -283,13 +283,13 @@ Proof. - inv ABORT3. rewrite SEML3 in H. discriminate. Qed. -Lemma smatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is: +Lemma simatch_exclude_sabort_local_nocontinue ge sp st rs0 m0 is: icontinue is = false -> sabort_local ge sp (si_local st) rs0 m0 -> - smatch ge sp st rs0 m0 is -> False. + simatch ge sp st rs0 m0 is -> False. Proof. -(* intros CONT ABORT SEM. unfold sem_istate in SEM. rewrite CONT in SEM. - destruct st as [pc exits iis]. simpl in *. +(* 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. @@ -299,42 +299,42 @@ Proof. Admitted. -Lemma smatch_exclude_sabort_local ge sp st rs m is: +Lemma simatch_exclude_sabort_local ge sp st rs m is: sabort_local ge sp (si_local st) rs m -> - smatch ge sp st rs m is -> False. + simatch ge sp st rs m is -> False. Proof. intros. destruct (icontinue is) eqn:CONT. - - eapply smatch_exclude_sabort_local_continue; eauto. - - eapply smatch_exclude_sabort_local_nocontinue; eauto. + - eapply simatch_exclude_sabort_local_continue; eauto. + - eapply simatch_exclude_sabort_local_nocontinue; eauto. Qed. -Lemma smatch_exclude_sabort_exits ge sp st rs m is: +Lemma simatch_exclude_sabort_exits ge sp st rs m is: sabort_exits ge sp (si_exits st) rs m -> - smatch ge sp st rs m is -> False. + simatch ge sp st rs m is -> False. Proof. Admitted. -Lemma smatch_exclude_sabort ge sp st rs m is: +Lemma simatch_exclude_sabort ge sp st rs m is: sabort ge sp st rs m -> - smatch ge sp st rs m is -> False. + simatch ge sp st rs m is -> False. Proof. intros ABORT SEM. inv ABORT. - - eapply smatch_exclude_sabort_local; eauto. - - eapply smatch_exclude_sabort_exits; eauto. + - eapply simatch_exclude_sabort_local; eauto. + - eapply simatch_exclude_sabort_exits; eauto. Qed. Definition istate_eq_opt ist1 oist := exists ist2, oist = Some ist2 /\ istate_eq ist1 ist2. -Lemma smatch_opt_determ ge sp st rs m ois is: - smatch_opt ge sp st rs m ois -> - smatch ge sp st rs m is -> +Lemma simatch_opt_determ ge sp st rs m ois is: + simatch_opt ge sp st rs m ois -> + simatch ge sp st rs m is -> istate_eq_opt is ois. Proof. destruct ois as [is1|]; simpl; eauto. - - intros; eexists; intuition; eapply smatch_determ; eauto. - - intros; exploit smatch_exclude_sabort; eauto. destruct 1. + - intros; eexists; intuition; eapply simatch_determ; eauto. + - intros; exploit simatch_exclude_sabort; eauto. destruct 1. Qed. (** * Symbolic execution of one internal step *) @@ -353,7 +353,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 symb_istep (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) @@ -380,11 +380,10 @@ Definition symb_istep (i: instruction) (st: sistate): option sistate := | _ => None (* TODO jumptable ? *) end. -(* TODO TODO - continue renaming *) -Lemma list_sval_eval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: - (forall r : reg, seval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> - list_sval_eval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). +Lemma seval_list_sval_inj ge sp l rs0 m0 (sreg: reg -> sval) rs: + (forall r : reg, seval_sval ge sp (sreg r) rs0 m0 = Some (rs # r)) -> + seval_list_sval ge sp (list_sval_inj (map sreg l)) rs0 m0 = Some (rs ## l). Proof. intros H; induction l as [|r l]; simpl; auto. inversion_SOME v. @@ -393,242 +392,242 @@ Proof. try_simplify_someHyps. Qed. -Lemma symb_istep_preserv_early_exits i ge sp st rs0 m0 rs m pc st': - sem_early_exit ge sp st.(exits) rs0 m0 rs m pc -> - symb_istep i st = Some st' -> - sem_early_exit ge sp st'.(exits) rs0 m0 rs m pc. +Lemma sistep_preserves_simatch_exits i ge sp st rs0 m0 rs m pc st': + simatch_exits ge sp st.(si_exits) rs0 m0 rs m pc -> + sistep i st = Some st' -> + simatch_exits ge sp st'.(si_exits) rs0 m0 rs m pc. Proof. intros H. - destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps. + destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps. destruct H as [ext lx TAIL NYE COND INV PC]. econstructor; try (eapply is_tail_cons; eapply TAIL); eauto. Qed. -Lemma sreg_set_preserv_has_aborted ge sp st rs0 m0 r sv: - has_aborted_on_basic ge sp st rs0 m0 -> - has_aborted_on_basic ge sp (sreg_set st r sv) rs0 m0. +Lemma slocal_set_sreg_preserves_sabort_local ge sp st rs0 m0 r sv: + sabort_local ge sp st rs0 m0 -> + sabort_local ge sp (slocal_set_sreg st r sv) rs0 m0. Proof. - unfold has_aborted_on_basic. simpl; intuition. + unfold sabort_local. simpl; intuition. destruct H as [r1 H]. destruct (Pos.eq_dec r r1) as [TEST|TEST] eqn: HTEST. - subst; rewrite H; intuition. - right. right. exists r1. rewrite HTEST. auto. Qed. -Lemma smem_set_preserv_has_aborted ge sp st rs0 m0 m: - has_aborted_on_basic ge sp st rs0 m0 -> - has_aborted_on_basic ge sp (smem_set st m) rs0 m0. +Lemma slocal_set_smem_preserves_sabort_local ge sp st rs0 m0 m: + sabort_local ge sp st rs0 m0 -> + sabort_local ge sp (slocal_set_smem st m) rs0 m0. Proof. - unfold has_aborted_on_basic. simpl; intuition. + unfold sabort_local. simpl; intuition. Qed. -Lemma symb_istep_preserv_has_aborted i ge sp rs0 m0 st st': - symb_istep i st = Some st' -> - has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0. +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. - Local Hint Resolve sreg_set_preserv_has_aborted smem_set_preserv_has_aborted: core. - unfold has_aborted. - destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps; intuition eauto. + Local Hint Resolve slocal_set_sreg_preserves_sabort_local slocal_set_smem_preserves_sabort_local: core. + unfold sabort. + destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps; intuition eauto. (* COND *) - right. unfold has_aborted_on_test in * |- *. + right. unfold sabort_exits in * |- *. destruct H as (ext & H1 & H2). simpl; exists ext; intuition. Qed. -Lemma symb_istep_WF i st: - symb_istep i st = None -> default_succ i = None. +Lemma sistep_WF i st: + sistep i st = None -> default_succ i = None. Proof. - destruct i; simpl; unfold sist; simpl; congruence. + destruct i; simpl; unfold sist_set_local; simpl; congruence. Qed. -Lemma symb_istep_default_succ i st st': - symb_istep i st = Some st' -> default_succ i = Some (st'.(the_pc)). +Lemma sistep_default_succ i st st': + sistep i st = Some st' -> default_succ i = Some (st'.(si_pc)). Proof. - destruct i; simpl; unfold sist; simpl; try congruence; + destruct i; simpl; unfold sist_set_local; simpl; try congruence; intro H; inversion_clear H; simpl; auto. Qed. -Lemma symb_istep_correct ge sp i st rs0 m0 rs m: - sem_local_istate ge sp st.(curr) rs0 m0 rs m -> - has_not_yet_exit ge sp st.(exits) rs0 m0 -> - sem_option2_istate ge sp (symb_istep i st) rs0 m0 (istep ge i sp rs m). +Lemma sistep_correct ge sp i st rs0 m0 rs m: + simatch_local ge sp st.(si_local) rs0 m0 rs m -> + all_fallthrough ge sp st.(si_exits) rs0 m0 -> + simatch_opt2 ge sp (sistep i st) rs0 m0 (istep ge i sp rs m). Proof. intros (PRE & MEM & REG) NYE. destruct i; simpl; auto. + (* Nop *) - unfold sem_istate, sem_local_istate; simpl; try_simplify_someHyps. + unfold simatch, simatch_local; simpl; try_simplify_someHyps. + (* Op *) inversion_SOME v; intros OP; simpl. - - unfold sem_istate, sem_local_istate; simpl; intuition. + - unfold simatch, simatch_local; simpl; intuition. * exploit REG. try_simplify_someHyps. * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. subst; rewrite Regmap.gss; simpl; auto. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. - - unfold has_aborted, has_aborted_on_basic; simpl. + - unfold sabort, sabort_local; simpl. left. right. right. exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite list_sval_eval_inj; simpl; auto. + simpl. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. + (* LOAD *) admit. (* FIXME *) (* inversion_SOME a0; intros ADD. { inversion_SOME v; intros LOAD; simpl. - - explore_destruct; unfold sem_istate, sem_local_istate; simpl; intuition. + - explore_destruct; unfold simatch, simatch_local; simpl; intuition. * exploit REG. try_simplify_someHyps. * destruct (Pos.eq_dec r r0); [|rewrite Regmap.gso; auto]. subst; rewrite Regmap.gss; simpl. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. - - unfold has_aborted, has_aborted_on_basic; simpl. + - unfold sabort, sabort_local; simpl. left. right. right. exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite list_sval_eval_inj; simpl; auto. + simpl. erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. } - { unfold has_aborted, has_aborted_on_basic; simpl. + { unfold sabort, sabort_local; simpl. left. right. right. exists r. destruct (Pos.eq_dec r r); try congruence. - simpl. erewrite list_sval_eval_inj; simpl; auto. + simpl. erewrite seval_list_sval_inj; simpl; auto. rewrite ADD; simpl; auto. } *) + (* STORE *) inversion_SOME a0; intros ADD. { inversion_SOME m'; intros STORE; simpl. - - unfold sem_istate, sem_local_istate; simpl; intuition. + - unfold simatch, simatch_local; simpl; intuition. * congruence. - * erewrite list_sval_eval_inj; simpl; auto. + * erewrite seval_list_sval_inj; simpl; auto. erewrite REG. try_simplify_someHyps. - - unfold has_aborted, has_aborted_on_basic; simpl. + - unfold sabort, sabort_local; simpl. left. right. left. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. erewrite REG. try_simplify_someHyps. } - { unfold has_aborted, has_aborted_on_basic; simpl. + { unfold sabort, sabort_local; simpl. left. right. left. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. erewrite ADD; simpl; auto. } + (* COND *) Local Hint Resolve is_tail_refl: core. - Local Hint Unfold sem_local_istate: core. + Local Hint Unfold simatch_local: core. inversion_SOME b; intros COND. - { destruct b; simpl; unfold sem_istate, sem_local_istate; simpl. + { destruct b; simpl; unfold simatch, simatch_local; simpl. - intros; econstructor; eauto; simpl. unfold seval_condition. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. - - intuition. unfold has_not_yet_exit in * |- *. simpl. + - intuition. unfold all_fallthrough in * |- *. simpl. intuition. subst. simpl. unfold seval_condition. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. } - { unfold has_aborted, has_aborted_on_test; simpl. + { unfold sabort, sabort_exits; simpl. right. eexists; intuition eauto. simpl. unfold seval_condition. - erewrite list_sval_eval_inj; simpl; auto. + erewrite seval_list_sval_inj; simpl; auto. try_simplify_someHyps. } Admitted. -Lemma symb_istep_correct_None ge sp i st rs0 m0 rs m: - sem_local_istate ge sp (st.(curr)) rs0 m0 rs m -> - symb_istep i st = None -> +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 -> istep ge i sp rs m = None. Proof. intros (PRE & MEM & REG). - destruct i; simpl; unfold sist, sem_istate, sem_local_istate; simpl; try_simplify_someHyps. + destruct i; simpl; unfold sist_set_local, simatch, simatch_local; simpl; try_simplify_someHyps. Qed. (** * Symbolic execution of the internal steps of a path *) -Fixpoint symb_isteps (path:nat) (f: function) (st: s_istate): option s_istate := +Fixpoint sisteps (path:nat) (f: function) (st: sistate): option sistate := match path with | O => Some st | S p => - SOME i <- (fn_code f)!(st.(the_pc)) IN - SOME st1 <- symb_istep i st IN - symb_isteps p f st1 + SOME i <- (fn_code f)!(st.(si_pc)) IN + SOME st1 <- sistep i st IN + sisteps p f st1 end. -Lemma symb_isteps_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, sem_istate ge sp st rs0 m0 is -> - symb_isteps path f st = Some st' -> - sem_istate 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. - Local Hint Resolve symb_istep_preserv_early_exits: core. - intros CONT; unfold sem_istate; rewrite CONT. + Local Hint Resolve sistep_preserves_simatch_exits: core. + intros CONT; unfold simatch; rewrite CONT. induction path; simpl. - + unfold sist; try_simplify_someHyps. + + unfold sist_set_local; try_simplify_someHyps. + intros st; inversion_SOME i. inversion_SOME st1; eauto. Qed. -Lemma symb_isteps_preserv_has_aborted ge sp path f rs0 m0 st': forall st, - symb_isteps path f st = Some st' -> - has_aborted ge sp st rs0 m0 -> has_aborted ge sp st' rs0 m0. +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. - Local Hint Resolve symb_istep_preserv_has_aborted: core. + Local Hint Resolve sistep_preserves_sabort: core. induction path; simpl. - + unfold sist; try_simplify_someHyps. + + unfold sist_set_local; try_simplify_someHyps. + intros st; inversion_SOME i. inversion_SOME st1; eauto. Qed. -Lemma symb_isteps_WF path f: forall st, - symb_isteps path f st = None -> nth_default_succ (fn_code f) path st.(the_pc) = None. +Lemma sisteps_WF path f: forall st, + sisteps path f st = None -> nth_default_succ (fn_code f) path st.(si_pc) = None. Proof. induction path; simpl. - + unfold sist. intuition congruence. - + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try tauto. - destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl. - - intros; erewrite symb_istep_default_succ; eauto. - - intros; erewrite symb_istep_WF; eauto. + + unfold sist_set_local. intuition congruence. + + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try tauto. + destruct (sistep i st) as [st1|] eqn: Hst1; simpl. + - intros; erewrite sistep_default_succ; eauto. + - intros; erewrite sistep_WF; eauto. Qed. -Lemma symb_isteps_default_succ path f st': forall st, - symb_isteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(the_pc) = Some st'.(the_pc). +Lemma sisteps_default_succ path f st': forall st, + sisteps path f st = Some st' -> nth_default_succ (fn_code f) path st.(si_pc) = Some st'.(si_pc). Proof. induction path; simpl. - + unfold sist. intros st H. inversion_clear H; simpl; try congruence. - + intros st; destruct ((fn_code f) ! (the_pc st)); simpl; try congruence. - destruct (symb_istep i st) as [st1|] eqn: Hst1; simpl; try congruence. - intros; erewrite symb_istep_default_succ; eauto. + + unfold sist_set_local. intros st H. inversion_clear H; simpl; try congruence. + + intros st; destruct ((fn_code f) ! (si_pc st)); simpl; try congruence. + destruct (sistep i st) as [st1|] eqn: Hst1; simpl; try congruence. + intros; erewrite sistep_default_succ; eauto. Qed. -Lemma symb_isteps_correct_true ge sp path (f:function) rs0 m0: forall st is, +Lemma sisteps_correct_true ge sp path (f:function) rs0 m0: forall st is, is.(icontinue)=true -> - sem_istate ge sp st rs0 m0 is -> - nth_default_succ (fn_code f) path st.(the_pc) <> None -> - sem_option2_istate ge sp (symb_isteps path f st) rs0 m0 - (isteps ge path f sp is.(the_rs) is.(the_mem) is.(RTLpath.the_pc)) + 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)) . Proof. - Local Hint Resolve symb_isteps_correct_false symb_isteps_preserv_has_aborted symb_isteps_WF: core. + Local Hint Resolve sisteps_correct_false sisteps_preserves_sabort sisteps_WF: core. induction path; simpl. + intros st is CONT INV WF; - unfold sem_istate, sist in * |- *; + unfold simatch, sist_set_local in * |- *; try_simplify_someHyps. simpl. destruct is; simpl in * |- *; subst; intuition auto. - + intros st is CONT; unfold sem_istate at 1; rewrite CONT. + + intros st is CONT; unfold simatch at 1; rewrite CONT. intros (LOCAL & PC & NYE) WF. rewrite <- PC. inversion_SOME i; intro Hi; rewrite Hi in WF |- *; simpl; auto. - exploit symb_istep_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. - (* continue is0 = true *) + (* icontinue is0 = true *) intros; eapply IHpath; eauto. - destruct i; simpl in * |- *; unfold sist in * |- *; try_simplify_someHyps. - (* continue is0 = false -> EARLY EXIT *) - destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. - destruct WF. erewrite symb_istep_default_succ; eauto. + destruct i; simpl in * |- *; unfold sist_set_local in * |- *; try_simplify_someHyps. + (* icontinue is0 = false -> EARLY EXIT *) + destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. + destruct WF. erewrite sistep_default_succ; eauto. (* try_simplify_someHyps; eauto. *) - * destruct (symb_isteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. + * destruct (sisteps path f st1) as [st2|] eqn: Hst2; simpl; eauto. - intros His1;rewrite His1; simpl; auto. Qed. (** REM: in the following two unused lemmas *) -Lemma symb_isteps_right_assoc_decompose f path: forall st st', - symb_isteps (S path) f st = Some st' -> - exists st0, symb_isteps path f st = Some st0 /\ symb_isteps 1%nat f st0 = Some st'. +Lemma sisteps_right_assoc_decompose f path: forall st st', + sisteps (S path) f st = Some st' -> + exists st0, sisteps path f st = Some st0 /\ sisteps 1%nat f st0 = Some st'. Proof. induction path; simpl; eauto. intros st st'. @@ -637,10 +636,10 @@ Proof. try_simplify_someHyps; eauto. Qed. -Lemma symb_isteps_right_assoc_compose f path: forall st st0 st', - symb_isteps path f st = Some st0 -> - symb_isteps 1%nat f st0 = Some st' -> - symb_isteps (S path) f st = Some st'. +Lemma sisteps_right_assoc_compose f path: forall st st0 st', + sisteps path f st = Some st0 -> + sisteps 1%nat f st0 = Some st' -> + sisteps (S path) f st = Some st'. Proof. induction path. + intros st st0 st' H. simpl in H. @@ -668,20 +667,20 @@ Inductive sfval := | Sreturn: option sval -> sfval . -Definition s_find_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef := +Definition sfind_function (pge: RTLpath.genv) (ge: RTL.genv) (sp: val) (svos : sval + ident) (rs0: regset) (m0: mem): option fundef := match svos with - | inl sv => SOME v <- seval ge sp sv rs0 m0 IN Genv.find_funct pge v + | inl sv => SOME v <- seval_sval ge sp sv rs0 m0 IN Genv.find_funct pge v | inr symb => SOME b <- Genv.find_symbol pge symb IN Genv.find_funct_ptr pge b end. -Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop := +Inductive sfmatch (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: sistate) stack (f: function) (rs0: regset) (m0: mem): sfval -> regset -> mem -> trace -> state -> Prop := | exec_Snone rs m: - sfval_sem pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(the_pc) rs m) + sfmatch pge ge sp st stack f rs0 m0 Snone rs m E0 (State stack f sp st.(si_pc) rs m) | exec_Scall rs m sig svos lsv args res pc fd: - s_find_function pge ge sp svos rs0 m0 = Some fd -> + sfind_function pge ge sp svos rs0 m0 = Some fd -> funsig fd = sig -> - list_sval_eval ge sp lsv rs0 m0 = Some args -> - sfval_sem pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m + seval_list_sval ge sp lsv rs0 m0 = Some args -> + sfmatch pge ge sp st stack f rs0 m0 (Scall sig svos lsv res pc) rs m E0 (Callstate (Stackframe res f sp pc rs :: stack) fd args m) (* TODO: | exec_Itailcall stk pc rs m sig ros args fd m': @@ -707,52 +706,52 @@ Inductive sfval_sem (pge: RTLpath.genv) (ge: RTL.genv) (sp:val) (st: s_istate) s | exec_Sreturn stk osv rs m m' v: sp = (Vptr stk Ptrofs.zero) -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - match osv with Some sv => seval ge sp sv rs0 m0 | None => Some Vundef end = Some v -> - sfval_sem pge ge sp st stack f rs0 m0 (Sreturn osv) rs 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 E0 (Returnstate stack v m') . -Record s_state := { internal:> s_istate; final: sfval }. +Record sstate := { internal:> sistate; final: sfval }. -Inductive sem_state pge (ge: RTL.genv) (sp:val) (st: s_state) stack f (rs0: regset) (m0: mem): trace -> state -> Prop := - | sem_early is: +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 -> - sem_istate ge sp st rs0 m0 is -> - sem_state pge ge sp st stack f rs0 m0 E0 (State stack f sp is.(RTLpath.the_pc) is.(the_rs) is.(the_mem)) - | sem_normal is t s: + 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 -> - sem_istate ge sp st rs0 m0 is -> - sfval_sem pge ge sp st stack f rs0 m0 st.(final) is.(the_rs) is.(the_mem) t s -> - sem_state pge ge sp st stack f rs0 m0 t s + 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 . (** * Symbolic execution of final step *) -Definition symb_fstep (i: instruction) (prev: local_istate): sfval := +Definition sfstep (i: instruction) (prev: sistate_local): sfval := match i with | Icall sig ros args res pc => - let svos := sum_left_map prev.(the_sreg) ros in - let sargs := list_sval_inj (List.map prev.(the_sreg) args) in + let svos := sum_left_map prev.(si_sreg) ros in + let sargs := list_sval_inj (List.map prev.(si_sreg) args) in Scall sig svos sargs res pc | Ireturn or => - let sor := SOME r <- or IN Some (prev.(the_sreg) r) in + let sor := SOME r <- or IN Some (prev.(si_sreg) r) in Sreturn sor | _ => Snone end. -Lemma symb_fstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s: +Lemma sfstep_correct pge ge sp i (f:function) pc st stack rs0 m0 t rs m s: (fn_code f) ! pc = Some i -> - pc = st.(the_pc) -> - sem_local_istate ge sp (curr st) rs0 m0 rs m -> + 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 -> - symb_istep i st = None -> - sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s. + 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. - + (* Snone *) destruct i; simpl in Hi |- *; unfold sist in Hi; try congruence. + + (* Snone *) 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. - - erewrite list_sval_eval_inj; simpl; auto. + - erewrite seval_list_sval_inj; simpl; auto. + (* Itaillcall *) admit. + (* Ibuiltin *) admit. + (* Ijumptable *) admit. @@ -760,19 +759,19 @@ Proof. destruct or; simpl; auto. Admitted. -Lemma symb_fstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s: +Lemma sfstep_complete i (f:function) pc st ge pge sp stack rs0 m0 t rs m s: (fn_code f) ! pc = Some i -> - pc = st.(the_pc) -> - sem_local_istate ge sp (curr st) rs0 m0 rs m -> - sfval_sem pge ge sp st stack f rs0 m0 (symb_fstep i (curr st)) rs m t s -> - symb_istep i st = None -> + pc = st.(si_pc) -> + simatch_local ge sp (si_local st) rs0 m0 rs m -> + sfmatch pge ge sp st stack f rs0 m0 (sfstep i (si_local st)) rs m t s -> + sistep i st = None -> path_last_step ge pge stack f sp pc rs m t s. Proof. intros PC1 PC2 (PRE&MEM®) LAST Hi. destruct i as [ | | | |(*Icall*)sig ros args res pc'| | | | |(*Ireturn*)or]; - subst; try_simplify_someHyps; try (unfold sist in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *. + subst; try_simplify_someHyps; try (unfold sist_set_local in Hi; try congruence); inversion LAST; subst; clear LAST; simpl in * |- *. + (* Icall *) - erewrite list_sval_eval_inj in * |- ; simpl; try_simplify_someHyps; auto. + erewrite seval_list_sval_inj in * |- ; simpl; try_simplify_someHyps; auto. intros; eapply exec_Icall; eauto. destruct ros; simpl in * |- *; auto. rewrite REG in * |- ; auto. @@ -788,22 +787,22 @@ Admitted. (** * Main function of the symbolic execution *) -Definition init_local_istate := {| pre:= fun _ _ _ _ => True; the_sreg:= fun r => Sinput r; the_smem:= Sinit |}. +Definition init_sistate_local := {| si_pre:= fun _ _ _ _ => True; si_sreg:= fun r => Sinput r; si_smem:= Sinit |}. -Definition init_istate pc := {| the_pc:= pc; exits:=nil; curr:= init_local_istate |}. +Definition init_sistate pc := {| si_pc:= pc; si_exits:=nil; si_local:= init_sistate_local |}. -Lemma init_sem_istate ge sp pc rs m: sem_istate ge sp (init_istate pc) rs m (ist true pc rs m). +Lemma init_simatch ge sp pc rs m: simatch ge sp (init_sistate pc) rs m (mk_istate true pc rs m). Proof. - unfold sem_istate, sem_local_istate, has_not_yet_exit; simpl. intuition. + unfold simatch, simatch_local, all_fallthrough; simpl. intuition. Qed. -Definition symb_step (f: function) (pc:node): option s_state := +Definition sstep (f: function) (pc:node): option sstate := SOME path <- (fn_path f)!pc IN - SOME st <- symb_isteps path.(psize) f (init_istate pc) IN - SOME i <- (fn_code f)!(st.(the_pc)) IN - Some (match symb_istep i st with + SOME st <- sisteps path.(psize) f (init_sistate pc) IN + SOME i <- (fn_code f)!(st.(si_pc)) IN + Some (match sistep i st with | Some st' => {| internal := st'; final := Snone |} - | None => {| internal := st; final := symb_fstep i st.(curr) |} + | None => {| internal := st; final := sfstep i st.(si_local) |} end). Lemma final_node_path_simpl f path pc: @@ -816,67 +815,70 @@ Qed. Lemma symb_path_last_step i st st' ge pge stack (f:function) sp pc rs m t s: (fn_code f) ! pc = Some i -> - pc = st.(the_pc) -> - symb_istep i st = Some st' -> + pc = st.(si_pc) -> + sistep i st = Some st' -> path_last_step ge pge stack f sp pc rs m t s -> - exists ist, istep ge i sp rs m = Some ist /\ t = E0 /\ s = (State stack f sp ist.(RTLpath.the_pc) ist.(RTLpath.the_rs) ist.(the_mem)). + 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. Qed. -(* NB: each concrete execution can be executed on the symbolic state (produced from [symb_step]) -(symb_step is a correct over-approximation) +(* NB: each concrete execution can be executed on the symbolic state (produced from [sstep]) +(sstep is a correct over-approximation) *) -Theorem symb_step_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, symb_step f pc = Some st /\ sem_state pge ge sp st stack f rs m t s. + exists st, sstep f pc = Some st /\ smatch pge ge sp st stack f rs m t s. Proof. - Local Hint Resolve init_sem_istate symb_istep_preserv_early_exits: core. - intros PATH STEP; unfold symb_step; rewrite PATH; simpl. + Local Hint Resolve init_simatch sistep_preserves_simatch_exits: core. + intros PATH STEP; unfold sstep; rewrite PATH; simpl. lapply (final_node_path_simpl f path pc); eauto. intro WF. - exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist true pc rs m)); simpl; eauto. + exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). destruct STEP as [sti STEPS CONT|sti t s STEPS CONT LAST]; (* intro Hst *) - (rewrite STEPS; unfold sem_option2_istate; destruct (symb_isteps _ _ _) as [st|] eqn: Hst; try congruence); + (rewrite STEPS; unfold simatch_opt2; destruct (sisteps _ _ _) as [st|] eqn: Hst; try congruence); (* intro SEM *) - (simpl; unfold sem_istate; simpl; rewrite CONT; intro SEM); + (simpl; unfold simatch; simpl; rewrite CONT; intro SEM); (* intro Hi' *) - ( assert (Hi': (fn_code f) ! (the_pc st) = Some i); + ( assert (Hi': (fn_code f) ! (si_pc st) = Some i); [ unfold nth_default_succ_inst in Hi; - exploit symb_isteps_default_succ; eauto; simpl; + exploit sisteps_default_succ; eauto; simpl; intros DEF; rewrite DEF in Hi; auto | clear Hi; rewrite Hi' ]); (* eexists *) (eexists; constructor; eauto). - (* early *) - eapply sem_early; eauto. - unfold sem_istate; simpl; rewrite CONT. - destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl; eauto. + eapply smatch_early; eauto. + unfold simatch; simpl; rewrite CONT. + destruct (sistep i st) as [st'|] eqn: Hst'; simpl; eauto. - destruct SEM as (SEM & PC & HNYE). - destruct (symb_istep i st) as [st'|] eqn: Hst'; simpl. + destruct (sistep i st) as [st'|] eqn: Hst'; simpl. + (* normal on Snone *) rewrite <- PC in LAST. exploit symb_path_last_step; eauto; simpl. - intros (ist & ISTEP & Ht & Hs); subst. - exploit symb_istep_correct; eauto. simpl. + intros (mk_istate & ISTEP & Ht & Hs); subst. + exploit sistep_correct; eauto. simpl. erewrite Hst', ISTEP; simpl. clear LAST CONT STEPS PC SEM HNYE Hst Hi' Hst' ISTEP st sti i. - intro SEM; destruct (ist.(icontinue)) eqn: CONT. - { (* continue ist = true *) - eapply sem_normal; simpl; eauto. - unfold sem_istate in SEM. + intro SEM; destruct (mk_istate.(icontinue)) eqn: CONT. + { (* icontinue mk_istate = true *) + eapply smatch_normal; simpl; eauto. + unfold simatch in SEM. rewrite CONT in SEM. destruct SEM as (SEM & PC & HNYE). rewrite <- PC. eapply exec_Snone. } - { eapply sem_early; eauto. } + { eapply smatch_early; eauto. } + (* normal non-Snone instruction *) - eapply sem_normal; eauto. - * unfold sem_istate; simpl; rewrite CONT; intuition. - * simpl. eapply symb_fstep_correct; eauto. + eapply smatch_normal; eauto. + * unfold simatch; simpl; rewrite CONT; intuition. + * simpl. eapply sfstep_correct; eauto. rewrite PC; auto. Qed. @@ -939,10 +941,10 @@ Proof. Qed. *) -Lemma sfval_sem_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s: - sfval_sem pge ge sp st stack f rs0 m0 sv rs1 m t s -> +Lemma sfmatch_equiv pge ge sp (f:function) st sv stack rs0 m0 t rs1 rs2 m s: + sfmatch pge ge sp st stack f rs0 m0 sv rs1 m t s -> (forall r, rs1#r = rs2#r) -> - exists s', equiv_state s s' /\ sfval_sem pge ge sp st stack f rs0 m0 sv rs2 m t s'. + exists s', equiv_state s s' /\ sfmatch pge ge sp st stack f rs0 m0 sv rs2 m t s'. Proof. Local Hint Resolve equiv_stack_refl: core. destruct 1. @@ -958,57 +960,57 @@ Proof. + eapply exec_Sreturn; eauto. Qed. -(* NB: each execution of a symbolic state (produced from [symb_step]) represents a concrete execution - (symb_step is exact). +(* NB: each execution of a symbolic state (produced from [sstep]) represents a concrete execution + (sstep is exact). *) -Theorem symb_step_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 -> - symb_step f pc = Some st -> - sem_state pge ge sp st stack f rs m t s1 -> + 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. Proof. - Local Hint Resolve init_sem_istate: core. - unfold symb_step; intros PATH SSTEP SEM; rewrite PATH in SSTEP. + Local Hint Resolve init_simatch: core. + unfold sstep; intros PATH SSTEP SEM; rewrite PATH in SSTEP. lapply (final_node_path_simpl f path pc); eauto. intro WF. - exploit (symb_isteps_correct_true ge sp path.(psize) f rs m (init_istate pc) (ist true pc rs m)); simpl; eauto. + exploit (sisteps_correct_true ge sp path.(psize) f rs m (init_sistate pc) (mk_istate true pc rs m)); simpl; eauto. { intros ABS. apply WF; unfold nth_default_succ_inst. rewrite ABS; auto. } (destruct (nth_default_succ_inst (fn_code f) path.(psize) pc) as [i|] eqn: Hi; [clear WF|congruence]). unfold nth_default_succ_inst in Hi. - destruct (symb_isteps path.(psize) f (init_istate pc)) as [st0|] eqn: Hst0; simpl. + destruct (sisteps path.(psize) f (init_sistate pc)) as [st0|] eqn: Hst0; simpl. 2:{ (* absurd case *) - exploit symb_isteps_WF; eauto. + exploit sisteps_WF; eauto. simpl; intros NDS; rewrite NDS in Hi; congruence. } - exploit symb_isteps_default_succ; eauto; simpl. + exploit sisteps_default_succ; eauto; simpl. intros NDS; rewrite NDS in Hi. rewrite Hi in SSTEP. intros ISTEPS. try_simplify_someHyps. - destruct (symb_istep i st0) as [st'|] eqn: Hst'; simpl. + destruct (sistep i st0) as [st'|] eqn: Hst'; simpl. + (* normal exit on Snone instruction *) admit. + destruct SEM as [is CONT SEM|is t s CONT SEM1 SEM2]; simpl in * |- *. - (* early exit *) intros. - exploit sem_option_istate_determ; eauto. + exploit simatch_opt_determ; eauto. destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). eexists. econstructor 1. * eapply exec_early_exit; eauto. * rewrite EQ2, EQ4; eapply State_equiv. auto. - (* normal exit non-Snone instruction *) intros. - exploit sem_option_istate_determ; eauto. + exploit simatch_opt_determ; eauto. destruct 1 as (st & Hst & EQ1 & EQ2 & EQ3 & EQ4). - unfold sem_istate in SEM1. + unfold simatch in SEM1. rewrite CONT in SEM1. destruct SEM1 as (SEM1 & PC0 & NYE0). - exploit sfval_sem_equiv; eauto. + exploit sfmatch_equiv; eauto. clear SEM2; destruct 1 as (s' & Ms' & SEM2). rewrite ! EQ4 in * |-; clear EQ4. rewrite ! EQ2 in * |-; clear EQ2. exists s'; intuition. eapply exec_normal_exit; eauto. - eapply symb_fstep_complete; eauto. + eapply sfstep_complete; eauto. * congruence. - * unfold sem_local_istate in * |- *. intuition try congruence. + * unfold simatch_local in * |- *. intuition try congruence. Admitted. (** * Simulation of RTLpath code w.r.t symbolic execution *) @@ -1020,43 +1022,43 @@ Variable ge ge': RTL.genv. Hypothesis symbols_preserved_RTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s. Lemma seval_preserved sp sv rs0 m0: - seval ge sp sv rs0 m0 = seval ge' sp sv rs0 m0. + seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv rs0 m0. Proof. Local Hint Resolve symbols_preserved_RTL: core. - induction sv using sval_mut with (P0 := fun lsv => list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0) - (P1 := fun sm => smem_eval ge sp sm rs0 m0 = smem_eval ge' sp sm rs0 m0); simpl; auto. - + rewrite IHsv; clear IHsv. destruct (list_sval_eval _ _ _ _); auto. - rewrite IHsv0; clear IHsv0. destruct (smem_eval _ _ _ _); auto. + induction sv using sval_mut with (P0 := fun lsv => seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0) + (P1 := fun sm => seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0); simpl; auto. + + rewrite IHsv; clear IHsv. destruct (seval_list_sval _ _ _ _); auto. + rewrite IHsv0; clear IHsv0. destruct (seval_smem _ _ _ _); auto. erewrite eval_operation_preserved; eauto. - + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto. + + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto. erewrite <- eval_addressing_preserved; eauto. destruct (eval_addressing _ sp _ _); auto. rewrite IHsv; auto. - + rewrite IHsv; clear IHsv. destruct (seval _ _ _ _); auto. + + rewrite IHsv; clear IHsv. destruct (seval_sval _ _ _ _); auto. rewrite IHsv0; auto. - + rewrite IHsv0; clear IHsv0. destruct (list_sval_eval _ _ _ _); auto. + + rewrite IHsv0; clear IHsv0. destruct (seval_list_sval _ _ _ _); auto. erewrite <- eval_addressing_preserved; eauto. destruct (eval_addressing _ sp _ _); auto. - rewrite IHsv; clear IHsv. destruct (smem_eval _ _ _ _); auto. + rewrite IHsv; clear IHsv. destruct (seval_smem _ _ _ _); auto. rewrite IHsv1; auto. Qed. Lemma list_sval_eval_preserved sp lsv rs0 m0: - list_sval_eval ge sp lsv rs0 m0 = list_sval_eval ge' sp lsv rs0 m0. + seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv rs0 m0. Proof. induction lsv; simpl; auto. - rewrite seval_preserved. destruct (seval _ _ _ _); auto. + rewrite seval_preserved. destruct (seval_sval _ _ _ _); auto. rewrite IHlsv; auto. Qed. Lemma smem_eval_preserved sp sm rs0 m0: - smem_eval ge sp sm rs0 m0 = smem_eval ge' sp sm rs0 m0. + seval_smem ge sp sm rs0 m0 = seval_smem ge' sp sm rs0 m0. Proof. induction sm; simpl; auto. - rewrite list_sval_eval_preserved. destruct (list_sval_eval _ _ _ _); auto. + rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto. erewrite <- eval_addressing_preserved; eauto. destruct (eval_addressing _ sp _ _); auto. - rewrite IHsm; clear IHsm. destruct (smem_eval _ _ _ _); auto. + rewrite IHsm; clear IHsm. destruct (seval_smem _ _ _ _); auto. rewrite seval_preserved; auto. Qed. @@ -1064,7 +1066,7 @@ Lemma seval_condition_preserved sp cond lsv sm rs0 m0: seval_condition ge sp cond lsv sm rs0 m0 = seval_condition ge' sp cond lsv sm rs0 m0. Proof. unfold seval_condition. - rewrite list_sval_eval_preserved. destruct (list_sval_eval _ _ _ _); auto. + rewrite list_sval_eval_preserved. destruct (seval_list_sval _ _ _ _); auto. rewrite smem_eval_preserved; auto. Qed. @@ -1074,8 +1076,8 @@ Require Import RTLpathLivegen RTLpathLiveproofs. Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop := is1.(icontinue) = is2.(icontinue) - /\ eqlive_reg alive is1.(the_rs) is2.(the_rs) - /\ is1.(the_mem) = is2.(the_mem). + /\ eqlive_reg alive is1.(irs) is2.(irs) + /\ is1.(imem) = is2.(imem). Definition istate_simu f (srce: PTree.t node) is1 is2: Prop := if is1.(icontinue) then @@ -1085,17 +1087,17 @@ 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.(RTLpath.the_pc)) = 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.(RTLpath.the_pc)) = Some is1.(RTLpath.the_pc). + /\ srce!(is2.(ipc)) = Some is1.(ipc). -(* NOTE: a pure semantic definition on [s_istate], for a total freedom in refinements *) -Definition s_istate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: s_istate): Prop := +(* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *) +Definition sistate_simu (f: RTLpath.function) (srce: PTree.t node) (st1 st2: sistate): Prop := forall sp ge1 ge2, (forall s, Genv.find_symbol ge2 s = Genv.find_symbol ge1 s) -> liveness_ok_function f -> - forall rs m is1, sem_istate ge1 sp st1 rs m is1 -> - exists is2, sem_istate ge2 sp st2 rs m is2 /\ istate_simu f srce is1 is2. + 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] *) Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node): sfval -> sfval -> Prop := @@ -1108,14 +1110,14 @@ Inductive sfval_simu (f: RTLpath.function) (srce: PTree.t node) (opc1 opc2: node | Sreturn_simu os: sfval_simu f srce opc1 opc2 (Sreturn os) (Sreturn os). -Definition s_state_simu f srce (s1 s2: s_state): Prop := - s_istate_simu f srce s1.(internal) s2.(internal) - /\ sfval_simu f srce s1.(the_pc) s2.(the_pc) s1.(final) s2.(final). +Definition sstate_simu f srce (s1 s2: sstate): Prop := + sistate_simu f srce s1.(internal) s2.(internal) + /\ sfval_simu f srce s1.(si_pc) s2.(si_pc) s1.(final) s2.(final). -Definition symb_step_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop := - forall st1, symb_step f1 pc1 = Some st1 -> - exists st2, symb_step f2 pc2 = Some st2 /\ s_state_simu f1 srce st1 st2. +Definition sstep_simu srce (f1 f2: RTLpath.function) pc1 pc2: Prop := + 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 "symb_step_simu" property, by hash-consing. - See usage of [symb_step_simu] in [RTLpathScheduler]. -*) \ No newline at end of file +(* IDEA: we will provide an efficient test for checking "sstep_simu" property, by hash-consing. + See usage of [sstep_simu] in [RTLpathScheduler]. +*) diff --git a/mppa_k1c/lib/RTLpathScheduler.v b/mppa_k1c/lib/RTLpathScheduler.v index fb2be412..4478ee72 100644 --- a/mppa_k1c/lib/RTLpathScheduler.v +++ b/mppa_k1c/lib/RTLpathScheduler.v @@ -33,7 +33,7 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop := preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint); dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1; dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2; - dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> symb_step_simu dupmap f1 f2 pc1 pc2 + dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2 }. (* TODO: remove these two stub parameters *) @@ -110,13 +110,13 @@ Lemma match_stack_equiv stk1 stk2: forall stk3, list_forall2 equiv_stackframe stk2 stk3 -> list_forall2 match_stackframes stk1 stk3. Proof. - Local Hint Resolve match_stackframes_equiv. + Local Hint Resolve match_stackframes_equiv: core. induction 1; intros stk3 EQ; inv EQ; econstructor; eauto. Qed. Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3. Proof. - Local Hint Resolve match_stack_equiv. + Local Hint Resolve match_stack_equiv: core. destruct 1; intros EQ; inv EQ; econstructor; eauto. intros; eapply eqlive_reg_triv_trans; eauto. Qed. @@ -139,7 +139,7 @@ Qed. Lemma eqlive_match_states s1 s2 s3: eqlive_states s1 s2 -> match_states s2 s3 -> match_states s1 s3. Proof. - Local Hint Resolve eqlive_match_stack. + Local Hint Resolve eqlive_match_stack: core. destruct 1; intros MS; inv MS; try_simplify_someHyps; econstructor; eauto. eapply eqlive_reg_trans; eauto. Qed. @@ -293,15 +293,15 @@ Proof. Qed. Lemma s_find_function_preserved sp svos rs0 m0 fd: - s_find_function pge ge sp svos rs0 m0 = Some fd -> - exists fd', s_find_function tpge tge sp svos rs0 m0 = Some fd' + sfind_function pge ge sp svos rs0 m0 = Some fd -> + exists fd', sfind_function tpge tge sp svos rs0 m0 = Some fd' /\ transf_fundef fd = OK fd' /\ liveness_ok_fundef fd. Proof. - Local Hint Resolve symbols_preserved_RTL. - unfold s_find_function. destruct svos; simpl. - + rewrite (sval_eval_preserved ge tge); auto. - destruct (sval_eval _ _ _ _); try congruence. + Local Hint Resolve symbols_preserved_RTL: core. + unfold sfind_function. destruct svos; simpl. + + rewrite (seval_preserved ge tge); auto. + destruct (seval_sval _ _ _ _); try congruence. intros; exploit functions_preserved; eauto. intros (fd' & cunit & X). eexists. intuition eauto. eapply find_funct_liveness_ok; eauto. @@ -310,27 +310,27 @@ Proof. intros (fd' & X). eexists. intuition eauto. Qed. -Lemma sem_istate_simu f dupmap sp st st' rs m is: - sem_istate ge sp st rs m is -> +Lemma sistate_simu f dupmap sp st st' rs m is: + simatch ge sp st rs m is -> liveness_ok_function f -> - s_istate_simu f dupmap st st' -> + sistate_simu f dupmap st st' -> exists is', - sem_istate tge sp st' rs m is' /\ istate_simu f dupmap is is'. + simatch tge sp st' rs m is' /\ istate_simu f dupmap is is'. Proof. intros SEM LIVE X; eapply X; eauto. Qed. -Lemma sem_sfval_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s: +Lemma sfmatch_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s: match_function dupmap f f' -> liveness_ok_function f -> list_forall2 match_stackframes stk stk' -> (* s_istate_simu f dupmap st st' -> *) - sfval_simu f dupmap st.(the_pc) st'.(the_pc) sv sv' -> - sfval_sem pge ge sp st stk f rs0 m0 sv rs m t s -> - exists s', sfval_sem tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'. + sfval_simu f dupmap st.(si_pc) st'.(si_pc) sv sv' -> + sfmatch pge ge sp st stk f rs0 m0 sv rs m t s -> + exists s', sfmatch tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'. Proof. - Local Hint Resolve transf_fundef_correct. + Local Hint Resolve transf_fundef_correct: core. intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl. - (* Snone *) exploit initialize_path. { eapply dupmap_path_entry1; eauto. } @@ -350,38 +350,38 @@ Proof. eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. + destruct os; auto. - erewrite <- sval_eval_preserved; eauto. + erewrite <- seval_preserved; eauto. Qed. (* The main theorem on simulation of symbolic states ! *) -Theorem sem_symb_state_simu dupmap f f' stk stk' sp st st' rs m t s: +Theorem smatch_sstate_simu dupmap f f' stk stk' sp st st' rs m t s: match_function dupmap f f' -> liveness_ok_function f -> list_forall2 match_stackframes stk stk' -> - sem_state pge ge sp st stk f rs m t s -> - s_state_simu f dupmap st st' -> - exists s', sem_state tpge tge sp st' stk' f' rs m t s' /\ match_states s s'. + smatch pge ge sp st stk f rs m t s -> + sstate_simu f dupmap st st' -> + exists s', smatch tpge tge sp st' stk' f' rs m t s' /\ match_states s s'. Proof. intros MFUNC LIVE STACKS SEM (SIMU1 & SIMU2). destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl. - (* sem_early *) - exploit sem_istate_simu; eauto. + exploit sistate_simu; eauto. unfold istate_simu; rewrite CONT. intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')). - exists (State stk' f' sp (RTLpath.the_pc is') (the_rs is') (the_mem is')). + exists (State stk' f' sp (ipc is') (irs is') (imem is')). split. - + eapply sem_early; auto. congruence. + + eapply smatch_early; auto. congruence. + rewrite M'. econstructor; eauto. - (* sem_normal *) - exploit sem_istate_simu; eauto. + exploit sistate_simu; eauto. unfold istate_simu; rewrite CONT. intros (is' & SEM' & (CONT' & RS' & M')). rewrite <- eqlive_reg_triv in RS'. - exploit sem_sfval_simu; eauto. + exploit sfmatch_simu; eauto. clear SEM2; intros (s0 & SEM2 & MATCH0). - exploit sfval_sem_equiv; eauto. + exploit sfmatch_equiv; eauto. clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2). exists s1; split. - + eapply sem_normal; eauto. + + eapply smatch_normal; eauto. + eapply match_states_equiv; eauto. Qed. @@ -398,13 +398,13 @@ Proof. exploit initialize_path. { eapply dupmap_path_entry2; eauto. } intros (path' & PATH'). exists path'. - exploit (symb_step_correct f pc pge ge sp path stk rs m t s); eauto. + exploit (sstep_correct f pc pge ge sp path stk rs m t s); eauto. intros (st & SYMB & SEM); clear STEP. exploit dupmap_correct; eauto. clear SYMB; intros (st' & SYMB & SIMU). - exploit sem_symb_state_simu; eauto. + exploit smatch_sstate_simu; eauto. intros (s0 & SEM0 & MATCH). - exploit symb_step_exact; eauto. + exploit sstep_exact; eauto. intros (s' & STEP' & EQ). exists s'; intuition. eapply match_states_equiv; eauto. @@ -417,7 +417,7 @@ Lemma step_simulation s1 t s1' s2: step tge tpge s2 t s2' /\ match_states s1' s2'. Proof. - Local Hint Resolve eqlive_stacks_refl transf_fundef_correct. + Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core. destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS. (* exec_path *) - try_simplify_someHyps. intros. -- cgit