diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-02 08:20:58 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-02 08:20:58 +0200 |
commit | abfc8509ec4686924095c1328179fa06766dc496 (patch) | |
tree | a3052548018a306b91eeb03d2b339209fd130138 /scheduling | |
parent | f6a3483c7dcac5ed56a349361a19dc1f4c985de3 (diff) | |
download | compcert-kvx-abfc8509ec4686924095c1328179fa06766dc496.tar.gz compcert-kvx-abfc8509ec4686924095c1328179fa06766dc496.zip |
the current "high-level" specification of the simulation test will not work !
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL_SEsimuref.v | 94 | ||||
-rw-r--r-- | scheduling/BTL_SEtheory.v | 58 | ||||
-rw-r--r-- | scheduling/BTL_Scheduler.v | 9 |
3 files changed, 124 insertions, 37 deletions
diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v index af2159cb..65052310 100644 --- a/scheduling/BTL_SEsimuref.v +++ b/scheduling/BTL_SEsimuref.v @@ -182,8 +182,8 @@ Local Hint Resolve SIMU_FAILS SIMU_MEM SIMU_REG: core. Local Hint Constructors ris_simu: core. Local Hint Resolve sge_match: core. -Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context): - ris_simu ris1 ris2 -> ris_ok (bctx1 f1 ctx) ris1 -> ris_ok (bctx2 f2 ctx) ris2. +Lemma ris_simu_ok_preserv f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2): + ris_simu ris1 ris2 -> ris_ok (bctx1 ctx) ris1 -> ris_ok (bctx2 ctx) ris2. Proof. intros SIMU OK; econstructor; eauto. - erewrite <- SIMU_MEM; eauto. @@ -191,12 +191,12 @@ Proof. - unfold bctx2; intros; erewrite eval_sval_preserved; eauto. Qed. -Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context) sis1 sis2 rs m: +Lemma ris_simu_correct f1 f2 ris1 ris2 (ctx:simu_proof_context f1 f2) sis1 sis2 rs m: ris_simu ris1 ris2 -> - ris_refines (bctx1 f1 ctx) ris1 sis1 -> - ris_refines (bctx2 f2 ctx) ris2 sis2 -> - sem_sistate (bctx1 f1 ctx) sis1 rs m -> - sem_sistate (bctx2 f2 ctx) sis2 rs m. + ris_refines (bctx1 ctx) ris1 sis1 -> + ris_refines (bctx2 ctx) ris2 sis2 -> + sem_sistate (bctx1 ctx) sis1 rs m -> + sem_sistate (bctx2 ctx) sis2 rs m. Proof. intros RIS REF1 REF2 SEM. (* destruct REF1. destruct REF2. *) @@ -216,21 +216,59 @@ Proof. erewrite REG_EQ; eauto. Qed. -Definition rfv_refines ctx (rfv sfv: sfval): Prop := - forall rs m t s, sem_sfval ctx rfv rs m t s <-> sem_sfval ctx sfv rs m t s. +Definition option_refines ctx (orsv: option sval) (osv: option sval) := + match orsv, osv with + | Some rsv, Some sv => eval_sval ctx rsv = eval_sval ctx sv + | None, None => True + | _, _ => False + end. + +Definition sum_refines ctx (rsi: sval + ident) (si: sval + ident) := + match rsi, si with + | inl rsv, inl sv => eval_sval ctx rsv = eval_sval ctx sv + | inr id, inr id' => id = id' + | _, _ => False + end. + +Definition bargs_refines ctx (rargs: list (builtin_arg sval)) (args: list (builtin_arg sval)): Prop := + eval_list_builtin_sval ctx rargs = eval_list_builtin_sval ctx args. + +Inductive rfv_refines ctx: sfval -> sfval -> Prop := + | refines_Sgoto pc: rfv_refines ctx (Sgoto pc) (Sgoto pc) + | refines_Scall: forall sig rvos ros rargs args r pc + (SUM:sum_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + ,rfv_refines ctx (Scall sig rvos rargs r pc) (Scall sig ros args r pc) + | refines_Stailcall: forall sig rvos ros rargs args + (SUM:sum_refines ctx rvos ros) + (LIST:eval_list_sval ctx rargs = eval_list_sval ctx args) + ,rfv_refines ctx (Stailcall sig rvos rargs) (Stailcall sig ros args) + | refines_Sbuiltin: forall ef lbra lba br pc + (BARGS: bargs_refines ctx lbra lba) + ,rfv_refines ctx (Sbuiltin ef lbra br pc) (Sbuiltin ef lba br pc) + | refines_Sjumptable: forall rsv sv lpc + (VAL: eval_sval ctx rsv = eval_sval ctx sv) + ,rfv_refines ctx (Sjumptable rsv lpc) (Sjumptable sv lpc) + | refines_Sreturn: forall orsv osv + (OPT:option_refines ctx orsv osv) + ,rfv_refines ctx (Sreturn orsv) (Sreturn osv) +. Definition rfv_simu (rfv1 rfv2: sfval): Prop := rfv1 = rfv2. -Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context) sfv1 sfv2 rs m t s: +Local Hint Constructors sem_sfval equiv_state: core. + +Lemma rvf_simu_correct f1 f2 rfv1 rfv2 (ctx: simu_proof_context f1 f2) sfv1 sfv2 rs m t s: rfv_simu rfv1 rfv2 -> - rfv_refines (bctx1 f1 ctx) rfv1 sfv1 -> - rfv_refines (bctx2 f2 ctx) rfv2 sfv2 -> - sem_sfval (bctx1 f1 ctx) sfv1 rs m t s -> - sem_sfval (bctx2 f2 ctx) sfv2 rs m t s. + rfv_refines (bctx1 ctx) rfv1 sfv1 -> + rfv_refines (bctx2 ctx) rfv2 sfv2 -> + sem_sfval (bctx1 ctx) sfv1 rs m t s -> + exists s', sem_sfval (bctx2 ctx) sfv2 rs m t s' /\ equiv_state s s'. Proof. - unfold rfv_simu, rfv_refines; intros X REF1 REF2 SEM. subst. - rewrite <- REF2. - assert (sem_sfval (bctx1 f1 ctx) rfv2 rs m t s). { rewrite REF1; auto. } + unfold rfv_simu; intros X REF1 REF2 SEM. subst. + unfold bctx2; destruct REF1; inv REF2; inv SEM; simpl. + - eexists; split; eauto; simpl. + (* eapply State_equiv; eauto. NE MARCHE PAS ! *) Admitted. (* refinement of (symbolic) state *) @@ -277,11 +315,11 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop := Lemma rst_simu_correct rst1 rst2: rst_simu rst1 rst2 -> - forall f1 f2 ctx st1 st2 (*ok1 ok2*), - rst_refines (*ok1*) (bctx1 f1 ctx) rst1 st1 -> - rst_refines (*ok2*) (bctx2 f2 ctx) rst2 st2 -> + forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*), + rst_refines (*ok1*) (bctx1 ctx) rst1 st1 -> + rst_refines (*ok2*) (bctx2 ctx) rst2 st2 -> (* ok1 -> ok2 -> *) - sstate_simu f1 f2 ctx st1 st2. + sstate_simu ctx st1 st2. Proof. induction 1; simpl; auto. - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. @@ -293,25 +331,29 @@ Proof. intros RIS_OK2. intuition. exploit ris_simu_correct; eauto. exploit rvf_simu_correct; eauto. - simpl. + simpl. (* eexists; split. + econstructor; eauto. simpl. - admit. (* TODO: condition sur les tr_inputs: à ajouter plutôt dans le simu_proof_context ! *) + clear SIS. + admit. (* TODO: condition sur les tr_inputs du simu_proof_context ! *) + (* TODO: le rfv_refines est trop sémantique ! *) + admit. - (* cond *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. inv REF1. inv REF2. inv SEM1. destruct b; simpl. - + assert (TODO1: rst_refines (bctx1 f1 ctx) rifso1 ifso). admit. - assert (TODO2: rst_refines (bctx2 f2 ctx) rifso2 ifso0). admit. + + assert (TODO1: rst_refines (bctx1 ctx) rifso1 ifso). admit. + assert (TODO2: rst_refines (bctx2 ctx) rifso2 ifso0). admit. exploit IHrst_simu1; eauto. intros (s2 & X1 & X2). exists s2; split; eauto. econstructor; eauto. - * assert (TODO3: seval_condition (bctx2 f2 ctx) cond args0 sm0 = Some true). admit. + * assert (TODO3: seval_condition (bctx2 ctx) cond args0 sm0 = Some true). admit. eauto. * simpl; eauto. + admit. - (* abort *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1. inv REF1. inv SEM1. +*) + Admitted. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index c7a44153..72789121 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -1022,38 +1022,76 @@ Qed. (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *) -Record simu_proof_context := Sctx { +(* +Definition equiv_input_regs (f1 f2: BTL.function): Prop := + (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) + /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). + +Lemma equiv_input_regs_union f1 f2: + equiv_input_regs f1 f2 -> forall tbl, union_inputs f1 tbl = union_inputs f2 tbl. +Proof. + intros (EQNone & EQSome). induction tbl as [|pc l']; simpl; auto. + generalize (EQNone pc) (EQSome pc); clear EQNone EQSome; intros EQN EQS. + do 2 autodestruct; intuition; try_simplify_someHyps. + intros; exploit EQS; eauto; clear EQS. congruence. +Qed. + +Lemma equiv_input_regs_pre f1 f2 tbl or: + equiv_input_regs f1 f2 -> pre_inputs f1 tbl or = pre_inputs f2 tbl or. +Proof. + intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. +Qed. +*) + +Record simu_proof_context {f1 f2: BTL.function} := Sctx { sge1: BTL.genv; sge2: BTL.genv; sge_match: forall s, Genv.find_symbol sge1 s = Genv.find_symbol sge2 s; sstk1: list BTL.stackframe; sstk2: list BTL.stackframe; sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2; + (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *) ssp: val; srs0: regset; sm0: mem }. +Arguments simu_proof_context: clear implicits. -Definition bctx1 f1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition bctx2 f2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx1 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge1) ctx.(sstk1) f1 ctx.(ssp) ctx.(srs0) ctx.(sm0). +Definition bctx2 {f1 f2} (ctx: simu_proof_context f1 f2):= Bctx ctx.(sge2) ctx.(sstk2) f2 ctx.(ssp) ctx.(srs0) ctx.(sm0). -Definition sstate_simu f1 f2 (ctx: simu_proof_context) (st1 st2: sstate) := - forall t s1, sem_sstate (bctx1 f1 ctx) t s1 st1 -> - exists s2, sem_sstate (bctx2 f2 ctx) t s2 st2 /\ equiv_state s1 s2. -Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2). +(* TODO: A REVOIR. L'approche suivie ne marche pas !!! + +le [equiv_state] ci-dessous n'est pas assez général + => il faut un [match_state] qui va dépendre de [BTL_Scheduler.match_function] (dans le [match_stackframe]). + +Or, le [sstate_simu] qu'on cherche à définir ici, c'était pour définir ce [match_function]: circularité ! + +Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ? + +Pas sûr que ça marche, on aura aussi la dépendance circulaire entre [simu_proof_context] et [match_function] ! + +Autre solution: définir [sfval_simu] syntaxiquement comme dans [RTLpath_SEtheory] pour éviter le problème de circularité ! + +*) +Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2: sstate) := + forall t s1, sem_sstate (bctx1 ctx) t s1 st1 -> + exists s2, sem_sstate (bctx2 ctx) t s2 st2 /\ equiv_state s1 s2. + +Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2). Theorem symbolic_simu_correct f1 f2 ib1 ib2: symbolic_simu f1 f2 ib1 ib2 -> - forall ctx t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> + forall (ctx: simu_proof_context f1 f2) t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 -> exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2. Proof. unfold symbolic_simu, sstate_simu. intros SIMU ctx t s1 STEP1. - exploit (sexec_correct (bctx1 f1 ctx)); simpl; eauto. + exploit (sexec_correct (bctx1 ctx)); simpl; eauto. intros; exploit SIMU; eauto. intros (s2 & SEM1 & EQ1). - exploit (sexec_exact (bctx2 f2 ctx)); simpl; eauto. + exploit (sexec_exact (bctx2 ctx)); simpl; eauto. intros (s3 & STEP2 & EQ2). clear STEP1; eexists; split; eauto. eapply equiv_state_trans; eauto. diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index b479204c..bcddcf5d 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -15,7 +15,8 @@ Record match_function (f1 f2: BTL.function): Prop := { preserv_fnparams: fn_params f1 = fn_params f2; preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; - symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> + (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *) + symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); }. @@ -23,6 +24,12 @@ Local Open Scope error_monad_scope. Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *) +(* TODO: a-t-on besoin de ça ? +Lemma check_symbolic_simu_input_equiv x f1 f2: + check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Admitted. +*) + Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> forall pc ib1, (fn_code f1)!pc = Some ib1 -> |