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

3 files changed, 77 insertions, 35 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index c322a9a5..a4da4291 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -191,14 +191,14 @@ Inductive rstate :=
   .
 
 Inductive rst_simu: rstate -> rstate -> Prop :=
-  | Rfinal_simu ris1 ris2 rfv1 rfv2:
-      ris_simu ris1 ris2 ->
-      rfv_simu rfv1 rfv2 ->
-      rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
-  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2:
-      rst_simu rifso1 rifso2 ->
-      rst_simu rifnot1 rifnot2 ->
-      rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
+  | Rfinal_simu ris1 ris2 rfv1 rfv2
+      (RIS: ris_simu ris1 ris2)
+      (RFV: rfv_simu rfv1 rfv2)
+      : rst_simu (Rfinal ris1 rfv1) (Rfinal ris2 rfv2)
+  | Rcond_simu cond rargs rifso1 rifnot1 rifso2 rifnot2
+      (IFSO: rst_simu rifso1 rifso2)
+      (IFNOT: rst_simu rifnot1 rifnot2)
+      : rst_simu (Rcond cond rargs rifso1 rifnot1) (Rcond cond rargs rifso2 rifnot2)
   | Rabort_simu: rst_simu Rabort Rabort
 (* TODO: extension à voir dans un second temps !
   | Rcond_skip cond rargs rifso1 rifnot1 rst:
@@ -225,6 +225,8 @@ Inductive rst_refines ctx: (* Prop -> *) rstate -> sstate -> Prop :=
       : rst_refines ctx Rabort Sabort
   .
 
+Local Hint Resolve ris_simu_correct rvf_simu_correct: core.
+
 Lemma rst_simu_correct rst1 rst2:
    rst_simu rst1 rst2 ->
    forall f1 f2 (ctx: simu_proof_context f1 f2) st1 st2 (*ok1 ok2*),
@@ -233,7 +235,37 @@ Lemma rst_simu_correct rst1 rst2:
    (* ok1 -> ok2 -> *)
    sstate_simu ctx st1 st2.
 Proof.
-  induction 1; simpl; auto.
-  - (* final *) intros f1 f2 ctx st1 st2 REF1 REF2 t s1 SEM1.
-    inv REF1. inv REF2. inv SEM1.
-Admitted.
\ No newline at end of file
+  induction 1; simpl; intros f1 f2 ctx st1 st2 REF1 REF2 sis1 svf1 SEM1;
+  inv REF1; inv REF2; simpl in *; inv SEM1; auto.
+  - (* final_simu *) 
+    do 2 eexists; intuition; eauto.
+    exploit sem_sok; eauto.
+    erewrite OK_EQUIV; eauto.
+    intros ROK1.
+    exploit ris_simu_ok_preserv; eauto.
+  - (* cond_simu *)
+    destruct (seval_condition (bctx1 ctx) cond args sm) eqn: SCOND; try congruence.
+    generalize RCOND0.
+    erewrite <- seval_condition_preserved, RCOND by eauto.
+    intros SCOND0; rewrite <- SCOND0 in RCOND0.
+    erewrite <- SCOND0.
+    destruct b; simpl.
+    * exploit IHrst_simu1; eauto.
+    * exploit IHrst_simu2; eauto.
+Qed.
+
+
+(** TODO: could be useful ?
+Lemma seval_condition_valid_preserv ctx cond args sm b
+  (VALID_PRESERV: forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs)
+  :seval_condition ctx cond args sm = Some b ->
+   seval_condition ctx cond args Sinit = Some b.
+Proof.
+  unfold seval_condition; autodestruct; simpl; try congruence.
+  intros EVAL_LIST.
+  autodestruct; try congruence.
+  intros MEM COND. rewrite <- COND.
+  eapply cond_valid_pointer_eq; intros.
+  exploit VALID_PRESERV; eauto.
+Qed.
+*)
\ No newline at end of file
diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 557541ce..9ab64d7d 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1064,32 +1064,10 @@ Qed.
 
 (** * High-Level specification of the symbolic simulation test as predicate [symbolic_simu] *)
 
-(*
-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;
-   (* inputs_equiv: equiv_input_regs f1 f2;*) (* TODO a-t-on besoin de ça ? *)
    ssp: val;
    srs0: regset; 
    sm0: mem
@@ -1156,7 +1134,7 @@ Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate):
   forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) ->
   exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
                    /\ sistate_simu ctx sis1 sis2
-                   /\ sfv_simu ctx sfv1 sfv2
+                   /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2)
   .
 
 Definition symbolic_simu f1 f2 ib1 ib2: Prop := forall (ctx: simu_proof_context f1 f2), sstate_simu ctx (sexec f1 ib1) (sexec f2 ib2).
@@ -1261,6 +1239,16 @@ Proof.
   rewrite smem_eval_preserved; auto.
 Qed.
 
+(* TODO: useless ?
+Lemma run_sem_isstate_preserved sis:
+  run_sem_isstate (bctx1 ctx) sis = run_sem_isstate (bctx2 ctx) sis.
+Proof.
+  induction sis; simpl; eauto.
+  erewrite seval_condition_preserved.
+  repeat (autodestruct; auto).
+Qed.
+*)
+
 (* additional preservation properties under this additional hypothesis *)
 Hypothesis senv_preserved_BTL: Senv.equiv (sge1 ctx) (sge2 ctx).
 
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v
index bcddcf5d..ec83b3c1 100644
--- a/scheduling/BTL_Scheduler.v
+++ b/scheduling/BTL_Scheduler.v
@@ -9,6 +9,28 @@ Axiom scheduler: BTL.function -> BTL.code.
 
 Extract Constant scheduler => "BTLScheduleraux.btl_scheduler".
 
+(* TODO: could be useful ?
+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.
+*)
+
+
 (* a specification of the verification to do on each function *)
 Record match_function (f1 f2: BTL.function): Prop := {
   preserv_fnsig: fn_sig f1 = fn_sig f2;