archi pour la verif du scheduler

3 files changed, 82 insertions, 11 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 5b15fe9b..ea7082a9 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1020,7 +1020,10 @@ Proof.
     inversion SEXEC.
 Qed.
 
-(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
+(** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] 
+
+TODO: à revoir complètement. Il faut passer le dupmap en paramètre et match les états symboliques modulo le dupmap.
+*)
 
 Record simu_proof_context := Sctx {
    sge1: BTL.genv;
@@ -1028,24 +1031,23 @@ Record simu_proof_context := Sctx {
    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;
-   sf1: BTL.function;
-   sf2: BTL.function;
+   sstk_equiv: list_forall2 equiv_stackframe sstk1 sstk2;  (* REM: equiv_stackframe n'est pas suffisant, il faut le dupmap dedans ! *)
    ssp: val;
    srs0: regset; 
    sm0: mem
 }.
 
-Definition bctx1 (ctx: simu_proof_context):= Bctx ctx.(sge1) ctx.(sstk1) ctx.(sf1) ctx.(ssp) ctx.(srs0) ctx.(sm0).
-Definition bctx2 (ctx: simu_proof_context):= Bctx ctx.(sge2) ctx.(sstk2) ctx.(sf2) ctx.(ssp) ctx.(srs0) ctx.(sm0).
+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 sstate_simu (ctx: simu_proof_context) (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.
+(* TODO: A REVOIR ! *)
+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 ctx ib1 ib2: Prop := sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) ib2).
+Definition symbolic_simu f1 f2 ctx ib1 ib2: sstate_simu f1 f2 ctx (sexec (f1 ctx) ib1) (sexec (f2 ctx) ib2).
 
-Theorem symbolic_simu_correct ctx ib1 ib2:
+Theorem symbolic_simu_correct f1 f2 ctx ib1 ib2:
   symbolic_simu ctx ib1 ib2 ->
   forall t s1, iblock_step tr_inputs (sge1 ctx) (sstk1 ctx) (sf1 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s1 ->
   exists s2, iblock_step tr_inputs (sge2 ctx) (sstk2 ctx) (sf2 ctx) (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s2 /\ equiv_state s1 s2.
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index e69de29b..8cf9635c 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -0,0 +1,40 @@
+Require Import Coqlib Maps.
+Require Import AST Integers Values Events Memory Globalenvs Smallstep.
+Require Import RTL Op Registers OptionMonad BTL.
+
+Require Import Errors Linking BTL_SEtheory.
+
+(** External oracle *)
+Axiom scheduler: BTL.function -> BTL.code * node * (PTree.t node).
+
+(* FAKE: A REVOIR avec BTL_SEtheory... *)
+Definition symbolic_simu (dupmap: PTree.t node) (f1 f2: BTL.function) (pc1 pc2: node): Prop := True.
+
+Record match_function (dupmap: PTree.t node) (f1 f2: BTL.function): Prop := {
+  preserv_fnsig: fn_sig f1 = fn_sig f2;
+  preserv_fnparams: fn_params f1 = fn_params f2;
+  preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2;
+  preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint);
+  dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> symbolic_simu dupmap f1 f2 pc1 pc2;
+}.
+
+Definition verified_scheduler (f: BTL.function) :=
+  let (tcte, dupmap) := scheduler f in
+  let (tc, te) := tcte in
+  let f' := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
+  OK (f', dupmap).  (* TODO: fixme *)
+
+Program Definition transf_function (f: BTL.function):
+  { r : res BTL.function | forall f', r = OK f' -> exists dm, match_function dm f f'} :=
+  match (verified_scheduler f) with
+  | Error e => Error e
+  | OK (tf, dm) => OK tf
+  end.
+Next Obligation.
+Admitted.
+
+Definition transf_fundef (f: fundef) : res fundef :=
+  transf_partial_fundef (fun f => proj1_sig (transf_function f)) f.
+
+Definition transf_program (p: program) : res program :=
+  transform_partial_program transf_fundef p.
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v
index e69de29b..049dc6b1 100644
--- a/scheduling/BTL_Schedulerproof.v
+++ b/scheduling/BTL_Schedulerproof.v
@@ -0,0 +1,29 @@
+Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
+Require Import Coqlib Maps Events Errors Op.
+Require Import RTL BTL BTL_SEtheory.
+Require Import BTL_Scheduler.
+
+Definition match_prog (p tp: program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
+Proof.
+  intros. eapply match_transform_partial_program_contextual; eauto.
+Qed.
+
+Section PRESERVATION.
+
+Variable prog: program.
+Variable tprog: program.
+
+Hypothesis TRANSL: match_prog prog tprog.
+
+Let pge := Genv.globalenv prog.
+Let tpge := Genv.globalenv tprog.
+
+Theorem transf_program_correct:
+  forward_simulation (fsem prog) (fsem tprog).
+Admitted.
+
+End PRESERVATION.