Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL

1 files changed, 49 insertions, 109 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 3083ca71..72789121 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1022,137 +1022,77 @@ 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 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).
+
+
+(* 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]).
 
-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).
+Or, le [sstate_simu] qu'on cherche à définir ici, c'était pour définir ce [match_function]: circularité !
 
-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.
+Une solution: définir le match_function à l'aide d'un [iblock_step_simu] ?
 
-Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall ctx, sstate_simu f1 f2 ctx (sexec f1 ib1) (sexec f2 ib2).
+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.
-Qed.
-
-(** * Preservation properties *)
-
-Section SymbValPreserved.
-
-Variable ge ge': BTL.genv.
-
-Hypothesis symbols_preserved_BTL: forall s, Genv.find_symbol ge' s = Genv.find_symbol ge s.
-
-Hypothesis senv_preserved_BTL: Senv.equiv ge ge'.
-
-Lemma senv_find_symbol_preserved id:
-  Senv.find_symbol ge id = Senv.find_symbol ge' id.
-Proof.
-  destruct senv_preserved_BTL as (A & B & C). congruence.
-Qed.
-
-Lemma senv_symbol_address_preserved id ofs:
-  Senv.symbol_address ge id ofs = Senv.symbol_address ge' id ofs.
-Proof.
-  unfold Senv.symbol_address. rewrite senv_find_symbol_preserved.
-  reflexivity.
-Qed.
-
-Variable stk stk': list stackframe.
-Variable f f': function.
-Variable sp: val.
-Variable rs0: regset.
-Variable m0: mem.
-
-Lemma eval_sval_preserved sv:
-  eval_sval (Bctx ge stk f sp rs0 m0) sv = eval_sval (Bctx ge' stk' f' sp rs0 m0) sv.
-Proof.
-  induction sv using sval_mut with (P0 := fun lsv => eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv)
-                                   (P1 := fun sm => eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm); simpl; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_list_sval _ _); auto.
-    rewrite IHsv0; clear IHsv0. destruct (eval_smem _ _); auto.
-    erewrite eval_operation_preserved; eauto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; auto.
-  + rewrite IHsv; clear IHsv. destruct (eval_sval _ _); auto.
-    rewrite IHsv0; auto.
-  + rewrite IHsv0; clear IHsv0. destruct (eval_list_sval _ _); auto.
-    erewrite <- eval_addressing_preserved; eauto.
-    destruct (eval_addressing _ sp _ _); auto.
-    rewrite IHsv; clear IHsv. destruct (eval_smem _ _); auto.
-    rewrite IHsv1; auto.
-Qed.
-
-Lemma seval_builtin_arg_preserved m: forall bs varg,
-  seval_builtin_arg (Bctx ge stk f sp rs0 m0) m bs varg ->
-  seval_builtin_arg (Bctx ge' stk' f' sp rs0 m0) m bs varg.
-Proof.
-  induction 1; simpl.
-  all: try (constructor; auto).
-  - rewrite <- eval_sval_preserved. assumption.
-  - rewrite <- senv_symbol_address_preserved. assumption.
-  - rewrite senv_symbol_address_preserved. eapply seval_BA_addrglobal.
-Qed.
-
-Lemma seval_builtin_args_preserved m lbs vargs:
-  seval_builtin_args (Bctx ge stk f sp rs0 m0) m lbs vargs ->
-  seval_builtin_args (Bctx ge' stk' f' sp rs0 m0) m lbs vargs.
-Proof.
-  induction 1; constructor; eauto.
-  eapply seval_builtin_arg_preserved; auto.
-Qed.
-
-Lemma list_sval_eval_preserved lsv: 
-  eval_list_sval (Bctx ge stk f sp rs0 m0) lsv = eval_list_sval (Bctx ge' stk' f' sp rs0 m0) lsv.
-Proof.
-  induction lsv; simpl; auto.
-  rewrite eval_sval_preserved. destruct (eval_sval _ _); auto.
-  rewrite IHlsv; auto.
-Qed.
-
-Lemma smem_eval_preserved sm: 
-  eval_smem (Bctx ge stk f sp rs0 m0) sm = eval_smem (Bctx ge' stk' f' sp rs0 m0) sm.
-Proof.
-  induction sm; simpl; auto.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  erewrite <- eval_addressing_preserved; eauto.
-  destruct (eval_addressing _ sp _ _); auto.
-  rewrite IHsm; clear IHsm. destruct (eval_smem _ _); auto.
-  rewrite eval_sval_preserved; auto.
-Qed.
-
-Lemma seval_condition_preserved cond lsv sm:
-  seval_condition (Bctx ge stk f sp rs0 m0) cond lsv sm = seval_condition (Bctx ge' stk' f' sp rs0 m0) cond lsv sm.
-Proof.
-  unfold seval_condition.
-  rewrite list_sval_eval_preserved. destruct (eval_list_sval _ _); auto.
-  rewrite smem_eval_preserved; auto.
-Qed.
-
-End SymbValPreserved.
+Qed.
\ No newline at end of file