fix tr_sis definition

1 files changed, 90 insertions, 57 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index d682f776..a066626e 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -563,20 +563,6 @@ Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
   /\ eval_smem ctx sis.(si_smem) = Some m
   /\ forall (r:reg), eval_sval ctx (sis.(si_sreg) r) = Some (rs#r).
 
-(* 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.
-
 (** * Symbolic execution of final step *)
 Fixpoint transfer_sreg (inputs: list reg) (sreg: reg -> sval): reg -> sval :=
   match inputs with
@@ -598,29 +584,28 @@ Qed.
 
 Definition str_inputs (f:function) (tbl: list exit) (or:option reg) := transfer_sreg (Regset.elements (inputs_exit f tbl or)).
 
-Definition transfer_sis (f:function) (tbl: list exit) (or:option reg) (sis: sistate) :=
-  {| si_pre := sis.(si_pre); si_sreg := str_inputs f tbl or 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 transfer_sis_correct ctx sis rs tbl or r:
+Lemma str_inputs_correct ctx sis rs tbl or r:
   (forall r : reg, eval_sval ctx (si_sreg sis r) = Some rs # r) ->
-  sreg_eval ctx (transfer_sis (cf ctx) tbl or sis) r = Some (tr_inputs (cf ctx) tbl or 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 transfer_sis_correct: core.
+Local Hint Resolve str_inputs_correct: core.
 
-Definition tr_sis: function -> final -> sistate -> sistate := 
-  poly_tr transfer_sis.
+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.
-  destruct 1 as (_ & _ & REG).
+  unfold sreg_eval; simpl. destruct 1 as (_ & _ & REG).
   destruct fin; simpl; eauto.
-Qed.
+Admitted.
 
 Lemma tr_sis_regs_correct ctx fin sis rs m:
   sem_sistate ctx sis rs m ->
@@ -629,7 +614,7 @@ Proof.
   intros H.
   generalize (tr_sis_regs_correct_aux _ fin _ _ _ H).
   destruct H as (PRE & MEM & REG).
-  destruct fin; simpl; econstructor; simpl; intuition eauto.
+  econstructor; simpl; intuition eauto || congruence.
 Qed.
 
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
@@ -661,7 +646,7 @@ Lemma sexec_final_svf_correct ctx i sis t rs m s:
   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.
 Proof.
-  intros (PRE&MEM&REG).
+  unfold sreg_eval. 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.
@@ -975,18 +960,35 @@ Qed.
 
 Local Hint Resolve tr_inputs_ext: core.
 
-(* TODO
-Lemma sem_sfval_equiv rs1 rs2 ctx sfv m t s:
-  sem_sfval ctx sfv rs1 m t s ->
-  (forall r, rs1#r = rs2#r) -> 
-  exists s', equiv_state s s' /\  sem_sfval ctx sfv rs2 m t s'.
+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.
-  econstructor; eauto.
+  destruct 1; eexists; split; econstructor; eauto; try congruence.
 Qed.
-*)
+
+
 
 Local Hint Resolve sexec_final_svf_exact: core.
 
@@ -995,17 +997,6 @@ Definition abort_sistate ctx (sis: sistate): Prop :=
   \/ eval_smem ctx sis.(si_smem) = None
   \/ exists (r: reg), eval_sval ctx (sis.(si_sreg) r) = None.
 
-Lemma sem_sistate_exclude_abort ctx sis rs m:
-  sem_sistate ctx sis rs m ->
-  abort_sistate ctx sis ->
-  False.
-Proof.
-  intros SIS ABORT. inv SIS. destruct H0 as (H0 & H0').
-  inversion ABORT as [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; congruence.
-Qed.
-
-Local Hint Resolve sem_sistate_exclude_abort: core.
-
 Lemma set_sreg_preserves_abort ctx sv dst sis:
   abort_sistate ctx sis ->
   abort_sistate ctx (set_sreg dst sv sis).
@@ -1045,8 +1036,17 @@ Proof.
   intros; eapply set_smem_preserves_abort; eauto.
 Qed.
 
+Lemma sem_sistate_tr_sis_exclude_abort ctx sis fi rs m:
+  sem_sistate ctx (tr_sis (cf ctx) fi sis) rs m ->
+  abort_sistate ctx sis ->
+  False.
+Proof.
+  intros ((PRE1 & PRE2) & MEM & REG); simpl in *.
+  intros [ABORT1 | [ABORT2 | ABORT3]]; [ | | inv ABORT3]; try congruence.
+Qed.
+
 Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
-  sexec_store_preserves_abort: core.
+  sexec_store_preserves_abort sem_sistate_tr_sis_exclude_abort: core.
 
 Lemma sexec_exclude_abort ctx ib t s1: forall sis k
   (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
@@ -1056,7 +1056,6 @@ Lemma sexec_exclude_abort ctx ib t s1: forall sis k
 Proof.
   induction ib; simpl; intros; eauto.
   - (* final *) inversion SEXEC; subst; eauto.
-    admit.
   - (* load *) destruct trap; eauto.
     inversion SEXEC.
   - (* seq *)
@@ -1065,7 +1064,7 @@ Proof.
   - (* cond *)
     inversion SEXEC; subst; eauto. clear SEXEC.
     destruct b; eauto.
-Admitted.
+Qed.
 
 Lemma set_sreg_abort ctx dst sv sis rs m:
   sem_sistate ctx sis rs m -> 
@@ -1124,6 +1123,39 @@ 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
@@ -1140,13 +1172,14 @@ Proof.
   induction ib; simpl; intros; eauto.
   - (* final *)
     inv SEXEC.
-    admit.
-    (* TODO
-    exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto.
+    exploit (sem_sistate_tr_sis_determ ctx sis rs m fi rs' m0); eauto.
     intros (REG&MEM); subst.
-    exploit (sem_sfval_equiv rs0 rs); eauto.
-    intros (s2 & EQUIV & SFV').
-    eexists; split; eauto. *)
+    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.
+*)
   - (* Bop *) autodestruct; eauto.
   - destruct trap; [| inv SEXEC ].
     repeat autodestruct; eauto.