end of BTL_SEtheory w.r.t fsem

1 files changed, 169 insertions, 162 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index a066626e..d6b4e741 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -401,57 +401,39 @@ Definition sfind_function ctx (svos : sval + ident): option fundef :=
 Import ListNotations.
 Local Open Scope list_scope.
 
-(** [sem_sfval] corresponds to [final_step tr_inputs] for symbolic final value.
-
-    A main difference comes from [rsx] which observes the registers saved in the stackframe 
-    of the returned state.
-
-    Intuitively, only liveout registers are stored in the stack 
-    (others will be associated to [Vundef] value).
-*)
-Inductive sem_sfval ctx (rsx: reg -> option val): sfval -> regset -> mem -> trace -> state -> Prop :=
-  | exec_Sgoto pc rs rs' m:
-      rs' = tr_inputs ctx.(cf) [pc] None rs ->
-      (forall r, rsx r = Some rs'#r) ->
-      sem_sfval ctx rsx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc rs' m)
+Inductive sem_sfval ctx: sfval -> regset -> mem -> trace -> state -> Prop :=
+  | exec_Sgoto pc rs m:
+      sem_sfval ctx (Sgoto pc) rs m E0 (State (cstk ctx) (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] None rs) m)
   | exec_Sreturn stk osv rs m m' v:
       (csp ctx) = (Vptr stk Ptrofs.zero) ->
       Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
       match osv with Some sv => eval_sval ctx sv | None => Some Vundef end = Some v ->
-      (forall r, rsx r = Some Vundef) ->
-      sem_sfval ctx rsx (Sreturn osv) rs m
+      sem_sfval ctx (Sreturn osv) rs m
          E0 (Returnstate (cstk ctx) v m')
-  | exec_Scall rs m sig svos lsv args res pc fd rs':
+  | exec_Scall rs m sig svos lsv args res pc fd:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
       eval_list_sval ctx lsv = Some args ->
-      rs' = tr_inputs ctx.(cf) [pc] (Some res) rs ->
-      (forall r, rsx r = Some rs'#r) ->
-      sem_sfval ctx rsx (Scall sig svos lsv res pc) rs m
-        E0 (Callstate ((Stackframe res (cf ctx) (csp ctx) pc rs')::cstk ctx) fd args m)
+      sem_sfval ctx (Scall sig svos lsv res pc) rs m
+        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc (tr_inputs ctx.(cf) [pc] (Some res) rs)::cstk ctx) fd args m)
   | exec_Stailcall stk rs m sig svos args fd m' lsv:
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
       (csp ctx) = Vptr stk Ptrofs.zero ->
       Mem.free m stk 0 (cf ctx).(fn_stacksize) = Some m' ->
       eval_list_sval ctx lsv = Some args ->
-      (forall r, rsx r = Some Vundef) ->
-      sem_sfval ctx rsx (Stailcall sig svos lsv) rs m
+      sem_sfval ctx (Stailcall sig svos lsv) rs m
         E0 (Callstate (cstk ctx) fd args m')
-  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs':
+  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs:
       seval_builtin_args ctx m sargs vargs ->
       external_call ef (cge ctx) vargs m t vres m' ->
-      rs' = tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs ->
-      (forall r, rsx r = Some rs'#r) ->
-      sem_sfval ctx rsx (Sbuiltin ef sargs res pc) rs m
-        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres rs') m')
-  | exec_Sjumptable sv tbl pc' n rs m rs':
+      sem_sfval ctx (Sbuiltin ef sargs res pc) rs m
+        t (State (cstk ctx) (cf ctx) (csp ctx) pc (regmap_setres res vres (tr_inputs (cf ctx) [pc] (reg_builtin_res res) rs)) m')
+  | exec_Sjumptable sv tbl pc' n rs m:
       eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      rs' = tr_inputs ctx.(cf) tbl None rs ->
-      (forall r, rsx r = Some rs'#r) ->
-      sem_sfval ctx rsx (Sjumptable sv tbl) rs m
-        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs' m)
+      sem_sfval ctx (Sjumptable sv tbl) rs m
+        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' (tr_inputs ctx.(cf) tbl None rs) m)
 .
 
 (** * Preservation properties *)
@@ -564,59 +546,6 @@ 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 *)
-Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
-  match inputs with
-  | nil => fun r => Sundef 
-  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
-  end.
-
-Lemma transfer_sreg_inputs inputs sreg r:
-  List.In r inputs -> transfer_sreg inputs sreg r = sreg r.
-Proof.
-  induction inputs; simpl; try autodestruct; intuition congruence.
-Qed.
-
-Lemma transfer_sreg_dead inputs sreg r:
-  ~List.In r inputs -> transfer_sreg inputs sreg r = Sundef.
-Proof.
-  induction inputs; simpl; try autodestruct; intuition congruence.
-Qed.
-
-Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)).
-
-Lemma str_inputs_correct ctx sis rs tbl or r:
-  (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) ->
-  eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r.
-Admitted.
-
-Local Hint Resolve str_inputs_correct: core.
-
-Definition tr_sis f (fi: final) (sis: sistate) :=
-  {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
-     si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
-     si_smem := sis.(si_smem) |}.
-
-Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
-  eval_sval ctx (sis.(si_sreg) r).
-
-Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
-  sem_sistate ctx sis rs m ->
-  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
-Proof.
-  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
-  destruct fin; simpl; eauto.
-Admitted.
-
-Lemma tr_sis_regs_correct ctx fin sis rs m:
-  sem_sistate ctx sis rs m ->
-  sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m.
-Proof.
-  intros H.
-  generalize (tr_sis_regs_correct_aux _ fin _ _ _ H).
-  destruct H as (PRE & MEM & REG).
-  econstructor; simpl; intuition eauto || congruence.
-Qed.
-
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
@@ -644,9 +573,9 @@ Local Hint Constructors sem_sfval: core.
 Lemma sexec_final_svf_correct ctx i sis t rs m s:
   sem_sistate ctx sis rs m ->
   final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s -> 
-  sem_sfval ctx (sreg_eval ctx (tr_sis (cf ctx) i sis)) (sexec_final_sfv i sis) rs m t s.
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s.
 Proof.
-  unfold sreg_eval. intros (PRE&MEM&REG).
+  intros (PRE&MEM&REG).
   destruct 1; subst; try_simplify_someHyps; simpl; intros; try autodestruct; eauto.
   + (* Bcall *) intros; eapply exec_Scall; auto.
     - destruct ros; simpl in * |- *; auto.
@@ -666,7 +595,7 @@ Local Hint Resolve seval_builtin_args_exact: core.
 
 Lemma sexec_final_svf_exact ctx i sis t rs m s:
   sem_sistate ctx sis rs m ->
-  sem_sfval ctx (sreg_eval ctx (tr_sis (cf ctx) i sis)) (sexec_final_sfv i sis) rs m t s
+  sem_sfval ctx (sexec_final_sfv i sis) rs m t s
   -> final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
 Proof.
   intros (PRE&MEM&REG).
@@ -797,6 +726,76 @@ Proof.
   erewrite MEM; auto.
 Qed.
 
+(** * Compute sistate associated to final values *)
+Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
+  match inputs with
+  | nil => fun r => Sundef 
+  | r1::l => fun r => if Pos.eq_dec r r1 then sreg r1 else transfer_sreg l sreg r
+  end.
+
+Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)).
+
+Lemma str_inputs_correct ctx sis rs tbl or r:
+  (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) ->
+  eval_sval ctx (str_inputs (cf ctx) tbl or (si_sreg sis) r) = Some (tr_inputs (cf ctx) tbl or rs) # r.
+Proof.
+  intros H.
+  unfold str_inputs, tr_inputs, transfer_regs.
+  induction (Regset.elements _) as [|x l]; simpl.
+  + rewrite Regmap.gi; auto.
+  + autodestruct; intros; subst.
+    * rewrite Regmap.gss; auto.
+    * rewrite Regmap.gso; eauto.
+Qed.
+
+Local Hint Resolve str_inputs_correct: core.
+
+Definition tr_sis f (fi: final) (sis: sistate) :=
+  {| si_pre := fun ctx => (sis.(si_pre) ctx /\ forall r, eval_sval ctx (sis.(si_sreg) r) <> None);
+     si_sreg := poly_tr str_inputs f fi sis.(si_sreg); 
+     si_smem := sis.(si_smem) |}.
+
+Definition sreg_eval ctx (sis: sistate) (r: reg): option val :=
+  eval_sval ctx (sis.(si_sreg) r).
+
+Lemma tr_sis_regs_correct_aux ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  (forall r, sreg_eval ctx (tr_sis (cf ctx) fin sis) r = Some (tr_regs (cf ctx) fin rs) # r).
+Proof.
+  Local Opaque str_inputs.
+  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
+  destruct fin; simpl; eauto.
+Qed.
+
+Lemma tr_sis_regs_correct ctx fin sis rs m:
+  sem_sistate ctx sis rs m ->
+  sem_sistate ctx (tr_sis (cf ctx) fin sis) (tr_regs (cf ctx) fin rs) m.
+Proof.
+  intros H.
+  generalize (tr_sis_regs_correct_aux _ fin _ _ _ H).
+  destruct H as (PRE & MEM & REG).
+  econstructor; simpl; intuition eauto || congruence.
+Qed.
+
+Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f (svf: sfval): A := 
+  match svf with
+  | Sgoto pc => tr f [pc] None
+  | Scall _ _ _ res pc => tr f [pc] (Some res)
+  | Stailcall _ _ args => tr f [] None
+  | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
+  | Sreturn _ => tr f [] None
+  | Sjumptable _ tbl => tr f tbl None
+  end.
+
+Definition str_regs: function -> sfval -> regset -> regset :=
+  poly_str tr_inputs.
+
+Lemma str_tr_regs_equiv f fin sis:
+  str_regs f (sexec_final_sfv fin sis) = tr_regs f fin.
+Proof.
+  destruct fin; simpl; auto.
+Qed.
+
 (** * symbolic execution of blocks *)
 
 (* symbolic state *)
@@ -808,10 +807,9 @@ Inductive sstate :=
 
 (* transition (t,s) produced by a sstate in initial context ctx *)
 Inductive sem_sstate ctx t s: sstate -> Prop :=
-  | sem_Sfinal sis sfv rs rs' rsx m 
-     (SIS: sem_sistate ctx sis rs' m)
-     (EXT: forall r, rsx r = Some (rs'#r))
-     (SFV: sem_sfval ctx rsx sfv rs m t s)
+  | sem_Sfinal sis sfv rs m 
+     (SIS: sem_sistate ctx sis (str_regs (cf ctx) sfv rs) m)
+     (SFV: sem_sfval ctx sfv rs m t s)
      : sem_sstate ctx t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
      (SEVAL: seval_condition ctx cond args sm = Some b)
@@ -867,6 +865,9 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
   sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ISTEP; simpl; try autodestruct; eauto.
+  (* final value *)
+  intros; econstructor; eauto.
+  rewrite str_tr_regs_equiv; eauto.
   (* condition *)
   all: intros;
     eapply sem_Scond; eauto; [
@@ -875,6 +876,7 @@ Proof.
       try autodestruct; eauto ].
 Qed.
 
+
 (* NB: each concrete execution can be executed on the symbolic state (produced from [sexec]) 
   (sexec is a correct over-approximation)
 *)
@@ -886,6 +888,27 @@ Proof.
   eapply sexec_rec_correct; simpl; eauto.
 Qed.
 
+(* Remark that we want to reason modulo "extensionality" wrt Regmap.get about regsets.
+   And, nothing in their representation as (val * PTree.t val) enforces that
+     (forall r, rs1#r = rs2#r) -> rs1 = rs2
+*)
+Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
+  sem_sistate ctx sis rs1 m1 ->
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 ->
+     (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) 
+  /\ m1 = m2.
+Proof.
+  intros H1 H2.
+  lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
+  unfold sreg_eval; intros X.
+  destruct H1 as (_&MEM1&REG1).
+  destruct H2 as (_&MEM2&REG2); simpl in *.
+  intuition try congruence.
+  cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r).
+  { congruence. }
+  rewrite <- REG2, X. auto.
+Qed.
+
 
 (* TODO: déplacer les trucs sur equiv_stackframe -> regmap_setres_eq dans BTL! *)
 Inductive equiv_stackframe: stackframe -> stackframe -> Prop :=
@@ -958,38 +981,19 @@ Proof.
   - repeat (rewrite Regmap.gso); auto.
 Qed.
 
-Local Hint Resolve tr_inputs_ext: core.
+(* Local Hint Resolve tr_inputs_ext: core. *)
+Local Hint Resolve regmap_setres_eq: core.
 
-Definition poly_str {A} (tr: function -> list exit -> option reg -> A) f svf: A := 
-  match svf with
-  | Sgoto pc => tr f [pc] None
-  | Scall _ _ _ res pc => tr f [pc] (Some res)
-  | Stailcall _ _ args => tr f [] None
-  | Sbuiltin _ _ res pc => tr f [pc] (reg_builtin_res res)
-  | Sreturn _ => tr f [] None
-  | Sjumptable _ tbl => tr f tbl None
-  end.
-
-
-Lemma sem_sfval_inv1 rsx ctx sfv rs m t s:
-  sem_sfval ctx rsx sfv rs m t s ->
-  (forall r, rsx r = Some (poly_str tr_inputs (cf ctx) sfv rs)#r).
-Proof. 
-  destruct 1; simpl; subst; auto.
-Admitted.
-
-Lemma sem_sfval_equivx rsx1 rsx2 ctx sfv rs m t s:
-  sem_sfval ctx rsx1 sfv rs m t s ->
-  (forall r, rsx1 r = rsx2 r) ->
-  exists s', equiv_state s s' /\  sem_sfval ctx rsx2 sfv rs m t s'.
-Proof. 
-  Local Hint Resolve equiv_stack_refl equiv_state_refl regmap_setres_eq: core.
-  Local Hint Constructors sem_sfval: core.
-  destruct 1; eexists; split; econstructor; eauto; try congruence.
+Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
+  sem_sfval ctx sfv rs1 m t s ->
+  (forall r, (str_regs (cf ctx) sfv rs1)#r = (str_regs (cf ctx) sfv rs2)#r) ->
+  exists s', sem_sfval ctx sfv rs2 m t s' /\ equiv_state s s'.
+Proof.
+  unfold str_regs.
+  destruct 1; simpl in *; intros; subst; eexists; split; econstructor; eauto; try congruence.
+  constructor; eauto.
 Qed.
 
-
-
 Local Hint Resolve sexec_final_svf_exact: core.
 
 Definition abort_sistate ctx (sis: sistate): Prop :=
@@ -1123,39 +1127,6 @@ Qed.
 
 Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core.
 
-(* Remark that we need to reason modulo "extensionality" wrt Regmap.get about regsets.
-   And, nothing in their representation as (val * PTree.t val) enforces that
-     (forall r, rs1#r = rs2#r) -> rs1 = rs2
-*)
-(*
-Lemma sem_sistate_determ ctx sis rs1 m1 rs2 m2:
-  sem_sistate ctx sis rs1 m1 ->
-  sem_sistate ctx sis rs2 m2 ->
-  (forall r, rs1#r = rs2#r) /\ m1 = m2.
-Proof.
-  intros (_&MEM1&REG1) (_&MEM2&REG2).
-  intuition try congruence.
-  generalize (REG1 r); rewrite REG2; congruence.
-Qed.
-*)
-
-Lemma sem_sistate_tr_sis_determ ctx sis rs1 m1 fi rs2 m2:
-  sem_sistate ctx sis rs1 m1 ->
-  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs2 m2 ->
-     (forall r, rs2#r = (tr_regs (cf ctx) fi rs1)#r) 
-  /\ m1 = m2.
-Proof.
-  intros H1 H2.
-  lapply (tr_sis_regs_correct_aux ctx fi sis rs1 m1); eauto.
-  unfold sreg_eval; intros X.
-  destruct H1 as (_&MEM1&REG1).
-  destruct H2 as (_&MEM2&REG2); simpl in *.
-  intuition try congruence.
-  cut (Some rs2 # r = Some (tr_regs (cf ctx) fi rs1)#r).
-  { congruence. }
-  rewrite <- REG2, X. auto.
-Qed.
-
 Lemma sexec_rec_exact ctx ib t s1: forall sis k
   (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   rs m
@@ -1172,14 +1143,11 @@ Proof.
   induction ib; simpl; intros; eauto.
   - (* final *)
     inv SEXEC.
-    exploit (sem_sistate_tr_sis_determ ctx sis rs m fi rs' m0); eauto.
+    exploit (sem_sistate_tr_sis_determ ctx sis rs m fi); eauto.
     intros (REG&MEM); subst.
-    exploit (sem_sfval_equivx rsx (sreg_eval ctx (tr_sis (cf ctx) fi sis)) ctx ); eauto.
-    + intros; rewrite EXT, REG. admit.
-    + intros (s2 & EQUIV & SFV'). admit.
-(*    eexists; split.
-      eapply sexec_final_svf_exact; eauto.
-*)
+    exploit (sem_sfval_equiv rs0 rs); eauto.
+    * intros; rewrite REG, str_tr_regs_equiv; auto.
+    * intros (s2 & EQUIV & SFV'); eauto.
   - (* Bop *) autodestruct; eauto.
   - destruct trap; [| inv SEXEC ].
     repeat autodestruct; eauto.
@@ -1205,7 +1173,7 @@ Proof.
     destruct b.
     + exploit IHib1; eauto.
     + exploit IHib2; eauto.
-Admitted.
+Qed.
 
 
 (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
@@ -1227,3 +1195,42 @@ Proof.
     inversion SEXEC.
 Qed.
 
+(** * High-Level specification of the symbolic simulation test as predicate [sstate_simu] *)
+
+Record simu_proof_context := 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;
+   sf1: BTL.function;
+   sf2: BTL.function;
+   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 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.
+
+Theorem sstate_simu_correct ctx ib1 ib2:
+  sstate_simu ctx (sexec (sf1 ctx) ib1) (sexec (sf2 ctx) 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.
+Proof.
+  unfold sstate_simu.
+  intros SIMU t s1 STEP1.
+  exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
+  intros; exploit SIMU; eauto.
+  intros (s2 & SEM1 & EQ1).
+  exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
+  intros (s3 & STEP2 & EQ2).
+  clear STEP1; eexists; split; eauto.
+  eapply equiv_state_trans; eauto.
+Qed.
+