diff options
-rwxr-xr-x | configure | 2 | ||||
-rw-r--r-- | kvx/lib/RTLpathSE_impl.v | 113 |
2 files changed, 67 insertions, 48 deletions
@@ -845,7 +845,7 @@ EXECUTE=kvx-cluster --syscall=libstd_scalls.so -- CFLAGS= -D __KVX_COS__ SIMU=kvx-cluster -- BACKENDLIB=Machblock.v Machblockgen.v Machblockgenproof.v\\ - RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ + RTLpath.v RTLpathproof.v RTLpathLivegen.v RTLpathLivegenproof.v RTLpathSE_theory.v RTLpathSE_impl.v RTLpathScheduler.v RTLpathSchedulerproof.v\\ Asmblock.v Asmblockgen.v Asmblockgenproof0.v Asmblockgenproof1.v Asmblockgenproof.v Asmvliw.v Asmblockprops.v\\ ForwardSimulationBlock.v PostpassScheduling.v PostpassSchedulingproof.v\\ Asmblockdeps.v DecBoolOps.v Chunks.v Peephole.v ExtValues.v ExtFloats.v\\ diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index 1c62825a..e4ae1af8 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -78,32 +78,32 @@ Definition hsok_local ge sp (hst: hsistate_local) rs0 m0: Prop := /\ forall sm, List.In sm (hsi_lsmem hst) -> seval_smem ge sp sm rs0 m0 <> None. (* refinement link between a (st: sistate_local) and (hst: hsistate_local) *) -Definition hsistate_local_refines (hst: hsistate_local) (st: sistate_local) := forall ge sp, - (forall rs0 m0, sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0) - /\ (forall rs0 m0, hsok_local ge sp hst rs0 m0 -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0) - /\ (forall rs0 m0 r, hsok_local ge sp hst rs0 m0 -> hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0). +Definition hsistate_local_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) := + (sok_local ge sp st rs0 m0 <-> hsok_local ge sp hst rs0 m0) + /\ (hsok_local ge sp hst rs0 m0 -> hsi_smem_eval ge sp hst rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0) + /\ (hsok_local ge sp hst rs0 m0 -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0). (* Syntax and semantics of symbolic exit states *) (* TODO: add hash-consing *) Record hsistate_exit := mk_hsistate_exit { hsi_cond: condition; hsi_scondargs: list_sval; hsi_elocal: hsistate_local; hsi_ifso: node }. -Definition hsistate_exit_refines (hext: hsistate_exit) (ext: sistate_exit): Prop := +Definition hsistate_exit_refines ge sp rs0 m0 (hext: hsistate_exit) (ext: sistate_exit): Prop := hsi_cond hext = si_cond ext /\ hsi_scondargs hext = si_scondargs ext - /\ hsistate_local_refines (hsi_elocal hext) (si_elocal ext) + /\ hsistate_local_refines ge sp rs0 m0 (hsi_elocal hext) (si_elocal ext) /\ hsi_ifso hext = si_ifso ext. (** * Syntax and Semantics of symbolic internal state *) Record hsistate := { hsi_pc: node; hsi_exits: list hsistate_exit; hsi_local: hsistate_local }. -Definition hsistate_refines (hst: hsistate) (st:sistate): Prop := +Definition hsistate_refines ge sp rs0 m0 (hst: hsistate) (st:sistate): Prop := hsi_pc hst = si_pc st - /\ list_forall2 hsistate_exit_refines (hsi_exits hst) (si_exits st) - /\ hsistate_local_refines (hsi_local hst) (si_local st). + /\ list_forall2 (hsistate_exit_refines ge sp rs0 m0) (hsi_exits hst) (si_exits st) + /\ hsistate_local_refines ge sp rs0 m0 (hsi_local hst) (si_local st). -Lemma hsistate_refines_pceq st hst: - hsistate_refines hst st -> +Lemma hsistate_refines_pceq ge sp rs0 m0 st hst: + hsistate_refines ge sp rs0 m0 hst st -> (hsi_pc hst) = (si_pc st). Proof. Admitted. @@ -175,13 +175,16 @@ Definition hsiexec_inst (i: instruction) (hst: hsistate): option hsistate := | _ => None (* TODO jumptable ? *) end. -Lemma hsiexec_inst_none i st hst: +(* SB: est-ce utile ? +Lemma hsiexec_inst_none ge sp rs0 m0 i st hst: siexec_inst i st = None -> - hsistate_refines hst st -> + hsistate_refines ge sp rs0 m0 hst st -> hsiexec_inst i hst = None. Proof. Admitted. +*) +(* SB: inutile en principe Lemma hsiexec_inst_complete i st st' hst: siexec_inst i st = Some st' -> hsistate_refines hst st -> @@ -190,13 +193,14 @@ Lemma hsiexec_inst_complete i st st' hst: /\ hsistate_refines hst' st'. Proof. Admitted. +*) -Lemma hsiexec_inst_correct i hst hst' st: +Lemma hsiexec_inst_correct ge sp rs0 m0 i hst hst' st: hsiexec_inst i hst = Some hst' -> - hsistate_refines hst st -> + hsistate_refines ge sp rs0 m0 hst st -> exists st', siexec_inst i st = Some st' - /\ hsistate_refines hst' st'. + /\ hsistate_refines ge sp rs0 m0 hst' st'. Proof. Admitted. @@ -209,6 +213,7 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate hsiexec_path p f hst1 end. +(* On ne devrait pas avoir besoin de ça ! Lemma hsiexec_path_complete ps f st st' hst: siexec_path ps f st = Some st' -> hsistate_refines hst st -> @@ -217,20 +222,21 @@ Lemma hsiexec_path_complete ps f st st' hst: /\ hsistate_refines hst' st'. Proof. Admitted. +*) Lemma hsiexec_path_correct ps f hst hst' st: hsiexec_path ps f hst = Some hst' -> - hsistate_refines hst st -> + forall ge sp rs0 m0, hsistate_refines ge sp rs0 m0 hst st -> exists st', siexec_path ps f st = Some st' - /\ hsistate_refines hst' st'. + /\ hsistate_refines ge sp rs0 m0 hst' st'. Proof. Admitted. Record hsstate := { hinternal:> hsistate; hfinal: sfval }. -Definition hsstate_refines (hst: hsstate) (st:sstate): Prop := - hsistate_refines (hinternal hst) (internal st) +Definition hsstate_refines ge sp rs0 m0 (hst: hsstate) (st:sstate): Prop := + hsistate_refines ge sp rs0 m0 (hinternal hst) (internal st) /\ hfinal hst = final st. (* TODO *) Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := @@ -255,8 +261,8 @@ Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := | _ => Snone end. -Lemma hsexec_final_correct hsl sl i: - hsistate_local_refines hsl sl -> +Lemma hsexec_final_correct ge sp rs0 m0 hsl sl i: + hsistate_local_refines ge sp rs0 m0 hsl sl -> hsexec_final i hsl = sexec_final i sl. Proof. Admitted. @@ -265,8 +271,8 @@ Definition init_hsistate_local := {| hsi_lsmem := Sinit::nil; hsi_ok_lsval := ni Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}. -Remark init_hsistate_correct pc: - hsistate_refines (init_hsistate pc) (init_sistate pc). +Remark init_hsistate_correct ge sp rs0 m0 pc: + hsistate_refines ge sp rs0 m0 (init_hsistate pc) (init_sistate pc). Proof. Admitted. @@ -279,18 +285,21 @@ Definition hsexec (f: function) (pc:node): option hsstate := | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |} end). -(* FIXME - this lemma might be unprovable ? *) +(* FIXME - this lemma might be unprovable ? SB: inutile en principe Lemma hsistate_refines_determ hst st st': hsistate_refines hst st -> hsistate_refines hst st' -> st = st'. Proof. Admitted. +*) -Lemma hsexec_correct f pc st hst: +Lemma hsexec_correct f pc hst: hsexec f pc = Some hst -> - hsstate_refines hst st -> - sexec f pc = Some st. + exists st, sexec f pc = Some st /\ + forall ge sp rs0 m0, hsstate_refines ge sp rs0 m0 hst st. +Admitted. +(* Proof. unfold hsexec. intros H HREF. explore. unfold sexec. rewrite EQ. @@ -304,7 +313,10 @@ Proof. eapply hsistate_refines_determ in HIREF; eauto. congruence. - admit. Admitted. +*) + +(* NB: inutile en principe. Lemma hsexec_complete f pc st: sexec f pc = Some st -> exists hst, hsexec f pc = Some hst /\ hsstate_refines hst st. @@ -322,13 +334,12 @@ Proof. constructor; auto. simpl. destruct HREF as (_ & _ & HLREF). apply hsexec_final_correct. assumption. Qed. +*) Definition hsstate_simu dm f (hst1 hst2: hsstate): Prop := - forall st1, - hsstate_refines hst1 st1 -> - exists st2, - hsstate_refines hst2 st2 - /\ sstate_simu dm f st1 st2. + forall ge sp rs0 m0 st1 st2, + hsstate_refines ge sp rs0 m0 hst1 st1 -> + hsstate_refines ge sp rs0 m0 hst2 st2 -> sstate_simu dm f st1 st2. Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *) @@ -338,21 +349,23 @@ Lemma hsstate_simub_correct dm f hst1 hst2: Proof. Admitted. +(* SB: Hum, le "exists st2" ne me plaît pas du tout ici... Definition hsexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop := forall hst1, hsexec f1 pc1 = Some hst1 -> exists hst2, hsexec f2 pc2 = Some hst2 /\ hsstate_simu dm f1 hst1 hst2. -Lemma hsexec_sexec_simu dm f1 f2 pc1 pc2: - hsexec_simu dm f1 f2 pc1 pc2 -> sexec_simu dm f1 f2 pc1 pc2. + +Lemma hsexec_sexec_simu dm f1 f2 pc1 pc2 hst1 hst2: + hsexec f1 pc1 = Some hst1 -> + hsexec f2 pc2 = Some hst2 -> + hsstate_simu dm f1 hst1 hst2 -> sexec_simu dm f1 f2 pc1 pc2. Proof. - intro HESIMU. - intros st1 SEXEC. - eapply hsexec_complete in SEXEC. - destruct SEXEC as (hst & HSEXEC & HREF). + intros HSEXEC1 HSEXEC2 HESIMU. eapply HESIMU in HSEXEC. destruct HSEXEC as (hst' & HSEXEC' & HSSIMU). eapply HSSIMU in HREF. destruct HREF as (st' & HREF' & SSIMU). eapply hsexec_correct in HSEXEC'; eauto. Qed. +*) Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) := let (pc2, pc1) := m in @@ -369,14 +382,20 @@ Lemma simu_check_single_correct dm tf f pc1 pc2: simu_check_single dm f tf (pc2, pc1) = OK tt -> sexec_simu dm f tf pc1 pc2. Proof. - unfold simu_check_single. intro. explore. - assert (hsexec_simu dm f tf pc1 pc2). { - unfold hsexec_simu. intros st1 STEQ. assert (h = st1) by congruence. subst. - exists h0. constructor; auto. - apply hsstate_simub_correct. assumption. - } - apply hsexec_sexec_simu. assumption. -Qed. + unfold simu_check_single. intro. + unfold sexec_simu. + intros st1 SEXEC. + explore. + exploit hsexec_correct; eauto. + intros (st2 & SEXEC2 & REF2). + clear EQ0. (* now, useless in principle and harmful for the next [exploit] *) + exploit hsexec_correct; eauto. + intros (st0 & SEXEC1 & REF1). + rewrite SEXEC1 in SEXEC; inversion SEXEC; subst. + eexists; split; eauto. + eapply hsstate_simub_correct; eauto. + (* SB: issue: remaining goals are on the shelf... *) +Admitted. Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm := match lm with |