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

2 files changed, 115 insertions, 12 deletions

diff --git a/scheduling/BTL_SEsimuref.v b/scheduling/BTL_SEsimuref.v
index a4da4291..6d74ccf9 100644
--- a/scheduling/BTL_SEsimuref.v
+++ b/scheduling/BTL_SEsimuref.v
@@ -1,13 +1,18 @@
 (** Refinement of BTL_SEtheory data-structures
     in order to introduce (and prove correct) a lower-level specification of the simulation test.
 
-    Ceci est un "bac à sable". TODO: A REVOIR COMPLETEMENT. Introduire "fake" hash-consing
+    Ceci est un "bac à sable". 
 
     - On introduit une représentation plus concrète pour les types d'état symbolique [sistate] et [sstate].
     - Etant donné une spécification intuitive "*_simu" pour tester la simulation sur cette représentation des états symboliques,
       on essaye déjà de trouver les bonnes notions de raffinement "*_refines" qui permette de prouver les lemmes "*_simu_correct".
     - Il faudra ensuite vérifier que l'exécution symbolique préserve ces relations de raffinement !
 
+    TODO: A REVOIR COMPLETEMENT.
+    - essayer de découper chaque relation de raffinement en une fonction "projection/abstraction" (à la "hsval_proj" à renommer en "hsval_abstract") 
+      et une équivalence sur la représentation abstraite.
+    - introduire "fake" hash-consed values (à renommer en "refined" plutôt que "fake").
+
 *)
 
 Require Import Coqlib Maps Floats.
@@ -15,7 +20,7 @@ Require Import AST Integers Values Events Memory Globalenvs Smallstep.
 Require Import Op Registers.
 Require Import RTL BTL OptionMonad BTL_SEtheory.
 
-(** * ... *)
+(** * Refinement of data-structures and of the specification of the simulation test *)
 
 Record sis_ok ctx (sis: sistate): Prop := {
   OK_PRE: (sis.(si_pre) ctx);
@@ -254,6 +259,103 @@ Proof.
     * exploit IHrst_simu2; eauto.
 Qed.
 
+(** * Refinement of the symbolic execution *)
+
+Local Hint Constructors rfv_refines optrsv_refines rsvident_refines rsvident_refines: core.
+
+Lemma eval_list_sval_refpreserv ctx args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  eval_list_sval ctx (list_sval_inj (map ris args)) =
+  eval_list_sval ctx (list_sval_inj (map sis args)).
+Proof.
+  intros REF OK.
+  induction args; simpl; eauto.
+  intros; erewrite REG_EQ, IHargs; eauto.
+Qed.
+
+Local Hint Resolve eval_list_sval_refpreserv: core.
+
+Lemma eval_builtin_sval_refpreserv ctx arg ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  eval_builtin_sval ctx (builtin_arg_map ris arg) = eval_builtin_sval ctx (builtin_arg_map sis arg).
+Proof.
+  intros REF OK; induction arg; simpl; eauto.
+  + erewrite REG_EQ; eauto.
+  + erewrite IHarg1, IHarg2; eauto.
+  + erewrite IHarg1, IHarg2; eauto.
+Qed.
+
+Lemma bargs_refpreserv ctx args ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  bargs_refines ctx (map (builtin_arg_map ris) args) (map (builtin_arg_map sis) args).
+Proof.
+  unfold bargs_refines. intros REF OK.
+  induction args; simpl; eauto.
+  erewrite eval_builtin_sval_refpreserv, IHargs; eauto.
+Qed.
+
+Local Hint Resolve bargs_refpreserv: core.
+
+Lemma exec_final_refpreserv ctx i ris sis:
+  ris_refines ctx ris sis ->
+  ris_ok ctx ris ->
+  rfv_refines ctx (sexec_final_sfv i ris) (sexec_final_sfv i sis).
+Proof.
+  destruct i; simpl; unfold sum_left_map; try autodestruct; eauto.
+Qed.
+
+Definition ris_init: ristate := {| ris_smem:= Sinit; ris_input_init:=true; ris_ok_sval := nil; ris_sreg := PTree.empty _ |}.
+
+Lemma ris_init_correct ctx:
+  ris_refines ctx ris_init sis_init.
+Proof.
+  unfold ris_init, sis_init; econstructor; simpl in *; eauto.
+  + split; destruct 1; econstructor; simpl in *; eauto.
+    congruence.
+  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
+    intros; rewrite PTree.gempty; eauto.
+  + try_simplify_someHyps.
+Qed.
+
+Definition rset_smem rm (ris:ristate): ristate :=
+  {| ris_smem := rm;
+     ris_input_init := ris.(ris_input_init);
+     ris_ok_sval := ris.(ris_ok_sval);
+     ris_sreg:= ris.(ris_sreg)
+  |}.
+
+Lemma sis_ok_set_mem ctx sm sis:
+  sis_ok ctx (set_smem sm sis)
+  <-> (sis_ok ctx sis /\ eval_smem ctx sm <> None).
+Proof.
+  split; destruct 1; econstructor; simpl in *; eauto.
+  intuition eauto.
+Qed.
+
+Lemma ris_ok_set_mem ctx rm (ris: ristate):
+  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
+  ris_ok ctx (rset_smem rm ris)
+  <-> (ris_ok ctx ris /\ eval_smem ctx rm <> None).
+Proof.
+   split; destruct 1; econstructor; simpl in *; eauto.
+Qed.
+
+Lemma rset_mem_refpreserv ctx rm sm ris sis:
+  (eval_smem ctx ris.(ris_smem) = None -> eval_smem ctx rm = None) ->
+  (forall m b ofs, eval_smem ctx sm = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer (cm0 ctx) b ofs) ->
+  ris_refines ctx ris sis ->
+  (ris_ok ctx ris -> eval_smem ctx rm = eval_smem ctx sm) ->
+  ris_refines ctx (rset_smem rm ris) (set_smem sm sis).
+Proof.
+  destruct 3; intros.
+  econstructor; eauto.
+  + rewrite sis_ok_set_mem, ris_ok_set_mem; intuition congruence.
+  + rewrite ris_ok_set_mem; intuition eauto.
+  + rewrite ris_ok_set_mem; intuition eauto.
+Qed.
 
 (** TODO: could be useful ?
 Lemma seval_condition_valid_preserv ctx cond args sm b
@@ -268,4 +370,5 @@ Proof.
   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 9ab64d7d..4b4571e4 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -437,7 +437,7 @@ Inductive sem_sfval ctx stk: sfval -> regset -> mem -> trace -> state -> Prop :=
 
 (* Syntax and Semantics of symbolic internal states *)
 (* [si_pre] is a precondition on initial context *)
-Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg: reg -> sval; si_smem: smem }.
+Record sistate := { si_pre: iblock_exec_context -> Prop; si_sreg:> reg -> sval; si_smem: smem }.
 
 (* Predicate on which (rs, m) is a possible final state after evaluating [st] on ((crs0 ctx), (cm0 ctx)) *)
 Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
@@ -446,25 +446,25 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
   /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r).
 
 (** * Symbolic execution of final step *)
-Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
+Definition sexec_final_sfv (i: final) (sreg: reg -> sval): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
   | Bcall sig ros args res pc => 
-    let svos := sum_left_map sis.(si_sreg) ros in
-    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    let svos := sum_left_map sreg ros in
+    let sargs := list_sval_inj (List.map sreg args) in
     Scall sig svos sargs res pc
   | Btailcall sig ros args =>
-    let svos := sum_left_map sis.(si_sreg) ros in
-    let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
+    let svos := sum_left_map sreg ros in
+    let sargs := list_sval_inj (List.map sreg args) in
     Stailcall sig svos sargs
   | Bbuiltin ef args res pc =>
-    let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
+    let sargs := List.map (builtin_arg_map sreg) args in
     Sbuiltin ef sargs res pc
   | Breturn or => 
-    let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
+    let sor := SOME r <- or IN Some (sreg r) in
     Sreturn sor
   | Bjumptable reg tbl =>
-    let sv := sis.(si_sreg) reg in
+    let sv := sreg reg in
     Sjumptable sv tbl
   end.