some advance, new section to simplify context from symbolic exec

1 files changed, 143 insertions, 60 deletions

diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index c7ecb0dc..85b185c5 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -33,6 +33,18 @@ Proof.
   eapply (Genv.senv_match TRANSL).
 Qed.
 
+Lemma functions_preserved:
+  forall (v: val) (f: fundef),
+  Genv.find_funct pge v = Some f ->
+  exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog.
+Proof.
+  intros. exploit (Genv.find_funct_match TRANSL); eauto.
+  intros (cu & tf & A & B & C).
+  repeat eexists; intuition eauto.
+  + unfold incl; auto.
+  + eapply linkorder_refl.
+Qed.
+
 (* TODO gourdinl move this to BTL_Scheduler.v? *)
 Inductive match_fundef: fundef -> fundef -> Prop :=
   | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f')
@@ -85,7 +97,9 @@ Lemma transf_function_correct f f':
   transf_function f = OK f' -> match_function f f'.
 Proof.
   unfold transf_function. intros H. monadInv H.
-  econstructor; eauto. eapply check_symbolic_simu_correct; eauto.
+  econstructor; eauto.
+  eapply check_symbolic_simu_input_equiv; eauto.
+  eapply check_symbolic_simu_correct; eauto.
 Qed.
 
 Lemma transf_fundef_correct f f':
@@ -132,30 +146,122 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
-Theorem symbolic_simu_ssem stk1 stk2 f1 f2 ib1 ib2:
-  forall (ctx: simu_proof_context f1 f2) t s,
-  sem_sstate (bctx1 ctx) stk1 t s (sexec f1 ib1) ->
+Section SYMBOLIC_CTX.
+
+Variables f1 f2: function.
+Variable sp0: val.
+Variable rs0: regset.
+Variable m0: Memory.Mem.mem.
+
+Lemma symbols_preserved_rev s: Genv.find_symbol pge s = Genv.find_symbol tpge s.
+Proof.
+  symmetry; apply symbols_preserved.
+Qed.
+
+Let ctx := Sctx f1 f2 pge tpge symbols_preserved_rev sp0 rs0 m0.
+
+Lemma str_regs_equiv sfv1 sfv2 rs:
+  sfv_simu ctx sfv1 sfv2 ->
+  match_function f1 f2 ->
+  str_regs (cf (bctx1 ctx)) sfv1 rs = str_regs (cf (bctx2 ctx)) sfv2 rs.
+Proof.
+  intros SFV MF; inv MF.
+  inv SFV; simpl;
+  erewrite equiv_input_regs_tr_inputs; auto.
+Qed.
+
+Lemma sfind_function_preserved ros1 ros2 fd:
+  svident_simu ctx ros1 ros2 ->
+  sfind_function (bctx1 ctx) ros1 = Some fd ->
+  exists fd',
+    sfind_function (bctx2 ctx) ros2 = Some fd'
+    /\ transf_fundef fd = OK fd'.
+Proof.
+  unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
+  + rewrite !SIMU. clear SIMU.
+    destruct (eval_sval _ _); try congruence.
+    intros; exploit functions_preserved; eauto.
+    intros (fd' & cunit & (X1 & X2 & X3)). eexists; eauto.
+  + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
+    intros; exploit function_ptr_preserved; eauto.
+Qed.
+
+Theorem symbolic_simu_ssem stk1 stk2 st st' s t:
+  sstate_simu ctx st st' ->
+  sem_sstate (bctx1 ctx) stk1 t s st ->
+  list_forall2 match_stackframes stk1 stk2 ->
+  match_function f1 f2 ->
   exists s',
-    sem_sstate (bctx2 ctx) stk2 t s' (sexec f2 ib2)
+    sem_sstate (bctx2 ctx) stk2 t s' st'
     /\ match_states s s'.
+Proof.
+  intros SIMU SST1 STACKS MF. inversion MF.
+  (*destruct SST1.*)
+  (*- [> sem_Sfinal <]*)
+    (*admit.*)
+  (*- [> sem_Scond <]*)
+
+  exploit sem_sstate_run; eauto.
+  intros (sis1 & sfv1 & rs' & m' & SOUT1 & SIS1 & SF).
+  exploit sem_si_ok; eauto. intros SOK.
+  exploit SIMU; simpl; eauto. (* rewrite SEVAL; eauto. *)
+  intros (sis2 & sfv2 & SOUT2 & SSIMU & SFVSIM).
+  remember SIS1 as EQSFV. clear HeqEQSFV.
+  eapply SFVSIM in EQSFV.
+
+
+  exploit SSIMU; eauto.
+  intros SIS2.
+
+
+
+  destruct SIS1 as (PRE1 & SMEM1 & SREGS1).
+  try_simplify_someHyps; intros.
+  (*exploit sem_sfval_equiv; eauto.*)
+  (*intros (s' & SF' & EQUIV).*)
+  set (EQSFV2:=sfv2).
+  inversion EQSFV; subst.
+  - 
+  inversion SF; subst.
+  exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+  + erewrite <- str_regs_equiv; simpl; eauto.
+  + econstructor.
+  + intros SST2. eexists; split; eauto.
+    econstructor; simpl; eauto.
+    erewrite equiv_input_regs_tr_inputs; eauto.
+
+  - 
+  inversion SF; subst.
+  exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
+  exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+  + erewrite <- str_regs_equiv; eauto.
+  + econstructor; eauto.
+    * apply function_sig_translated; auto.
+    * erewrite <- ARGS; eauto.
+  + intros SST2. eexists; split; eauto.
+    econstructor; simpl; eauto.
+    * erewrite equiv_input_regs_tr_inputs; eauto.
+      repeat (econstructor; eauto).
+    * apply transf_fundef_correct; auto.
+  - 
+      
+
+admit.
 Admitted.
 
-Theorem symbolic_simu_correct stk1 stk2 f1 f2 ib1 ib2:
-  symbolic_simu f1 f2 ib1 ib2 ->
-  forall (ctx: simu_proof_context f1 f2) t s, iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s ->
+Theorem symbolic_simu_correct stk1 stk2 ibf1 ibf2 s t:
+  sstate_simu ctx (sexec f1 ibf1.(entry)) (sexec f2 ibf2.(entry)) ->
+  iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf1.(entry) t s ->
+  list_forall2 match_stackframes stk1 stk2 ->
+  match_function f1 f2 ->
   exists s',
-    iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s'
+    iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf2.(entry) t s'
     /\ match_states s s'.
 Proof.
-  unfold symbolic_simu, sstate_simu.
-  intros SIMU ctx t s1 STEP1.
+  unfold sstate_simu.
+  intros SIMU STEP1 STACKS MF.
   exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
-  intros SST1. exploit sem_sstate_run; eauto.
-  intros (sis1 & sfv1 & rs & m & OUTC1 & SIS1 & SV1).
-  exploit sem_si_ok; eauto. intros SOK.
-  intros; exploit SIMU; eauto.
-  intros (sis2 & sfv2 & OUTC2 & SSIMU & SEM).
-  exploit symbolic_simu_ssem; eauto.
+  intros SST1. exploit symbolic_simu_ssem; eauto.
   intros (s2 & SST2 & MS).
   exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
   intros (s3 & STEP & EQUIV).
@@ -163,57 +269,34 @@ Proof.
   eapply match_states_equiv; eauto.
 Qed.
 
-(*
-Lemma iblock_istep_simulation_None stk1 stk2 f f' sp pc rs1 m rs1' m' rs2 ib1 ibf2 s
-  (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' None)
-  (PC: (fn_code f') ! pc = Some ibf2)
-  (EQREGS: forall r : positive, rs1 # r = rs2 # r)
-  (STACKS: list_forall2 match_stackframes stk1 stk2)
-  (TRANSF: match_function f f')
-  :exists rs2' s',
-       iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' None)
-    /\ match_states s s'.
+Lemma iblock_step_eqregs tr ge stk f sp ib:
+  forall rs m rs' t s,
+  (forall r, rs # r = rs' # r) ->
+  iblock_step tr ge stk f sp rs m ib t s <->
+  iblock_step tr ge stk f sp rs' m ib t s.
 Proof.
-  induction ib1; inv ISTEP; eauto.
+  induction ib; try_simplify_someHyps.
 Admitted.
 
-Lemma iblock_istep_simulation_Some stk1 stk2 f f' sp ib1: forall fin ibf2 rs1 m rs1' m' rs2 pc t s
-  (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' (Some fin))
-  (FSTEP: final_step tr_inputs pge stk1 f sp rs1' m' fin t s)
-  (PC: (fn_code f') ! pc = Some ibf2)
-  (EQREGS: forall r : positive, rs1 # r = rs2 # r)
-  (STACKS: list_forall2 match_stackframes stk1 stk2)
-  (TRANSF: match_function f f'),
-  exists rs2' s',
-       iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' (Some fin))
-    /\ final_step tr_inputs tpge stk2 f' sp rs2' m' fin t s'
-    /\ match_states s s'.
-Proof.
-  induction ib1; simpl; try_simplify_someHyps; inv ISTEP; eauto; intros.
-  - (* BF *)
-    admit.
-  - (* Bseq continue *)
-    exploit iblock_istep_simulation_None; eauto.
-    intros (rs2' & s' & ISTEP & MS).
-    admit.
-  - 
-Admitted.
- *)
-Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s pc
-  (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s)
-  (PC: (fn_code f) ! pc = Some ibf)
+End SYMBOLIC_CTX.
+
+Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc
+  (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s)
+  (PC: (fn_code f1) ! pc = Some ibf)
   (EQREGS: forall r : positive, rs # r = rs' # r)
   (STACKS: list_forall2 match_stackframes stk1 stk2)
-  (TRANSF: match_function f f')
+  (TRANSF: match_function f1 f2)
   :exists ibf' s',
-       (fn_code f') ! pc = Some ibf'
-    /\ iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s'
+       (fn_code f2) ! pc = Some ibf'
+    /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s'
     /\ match_states s s'.
 Proof.
-  destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).
-  inversion TRANSF. apply symbolic_simu_ok in PC as SYMB.
-  destruct SYMB as (ibf2 & PC' & SYMBS). clear symbolic_simu_ok.
-  unfold symbolic_simu, sstate_simu in SYMBS.
+  (*destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).*)
+  exploit symbolic_simu_ok; eauto. intros (ib2 & PC' & SYMBS).
+  exploit symbolic_simu_correct; repeat (eauto; simpl).
+  intros (s' & STEP2 & MS).
+  exists ib2; exists s'; repeat split; auto.
+  erewrite iblock_step_eqregs; eauto.
 Admitted.
 
 Local Hint Constructors step: core.