starting to experiment SE of fsem

1 files changed, 158 insertions, 55 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 5125ea3c..fb7c650f 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -28,6 +28,7 @@ Record iblock_exec_context := Bctx {
 
 (* symbolic value *)
 Inductive sval :=
+  | Sundef
   | Sinput (r: reg)
   | Sop (op:operation) (lsv: list_sval)  (sm: smem)
   | Sload (sm: smem) (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) (lsv:list_sval) 
@@ -53,6 +54,7 @@ Local Open Scope option_monad_scope.
 
 Fixpoint eval_sval ctx (sv: sval): option val :=
   match sv with
+  | Sundef => Some Vundef
   | Sinput r => Some ((crs0 ctx)#r)
   | Sop op l sm =>
      SOME args <- eval_list_sval ctx l IN
@@ -383,7 +385,6 @@ Qed.
 Inductive sfval :=
   | Sgoto (pc: exit)
   | Scall (sig:signature) (svos: sval + ident) (lsv:list_sval) (res:reg) (pc:exit)
-    (* NB: [res] the return register is hard-wired ! Is it restrictive ? *)
   | Stailcall: signature -> sval + ident -> list_sval -> sfval
   | Sbuiltin (ef:external_function) (sargs: list (builtin_arg sval)) (res: builtin_res reg) (pc:exit)
   | Sjumptable (sv: sval) (tbl: list exit)
@@ -397,39 +398,60 @@ Definition sfind_function ctx (svos : sval + ident): option fundef :=
   end
 .
 
-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 rs m)
+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)
   | 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 ->
-      sem_sfval ctx (Sreturn osv) rs m 
+      (forall r, rsx r = Some Vundef) ->
+      sem_sfval ctx rsx (Sreturn osv) rs m
          E0 (Returnstate (cstk ctx) v m')
-  | exec_Scall rs m sig svos lsv args res pc fd:
+  | exec_Scall rs m sig svos lsv args res pc fd rs':
       sfind_function ctx svos = Some fd ->
       funsig fd = sig ->
       eval_list_sval ctx lsv = Some args ->
-      sem_sfval ctx (Scall sig svos lsv res pc) rs m
-        E0 (Callstate (Stackframe res (cf ctx) (csp ctx) pc rs :: (cstk ctx)) fd args m)
+      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)
   | 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 ->
-      sem_sfval ctx (Stailcall sig svos lsv) rs m
+      (forall r, rsx r = Some Vundef) ->
+      sem_sfval ctx rsx (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:
+  | exec_Sbuiltin m' rs m vres res pc t sargs ef vargs rs':
       seval_builtin_args ctx m sargs vargs ->
       external_call ef (cge ctx) vargs m t vres m' ->
-      sem_sfval ctx (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' = tr_inputs ctx.(cf) [pc] None (regmap_setres res vres 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 rs' m')
+  | exec_Sjumptable sv tbl pc' n rs m rs':
       eval_sval ctx sv = Some (Vint n) ->
       list_nth_z tbl (Int.unsigned n) = Some pc' ->
-      sem_sfval ctx (Sjumptable sv tbl) rs m
-        E0 (State (cstk ctx) (cf ctx) (csp ctx) pc' rs m)
+      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)
 .
 
 (** * Preservation properties *)
@@ -536,18 +558,18 @@ End SymbValPreserved.
 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 (st: sistate) (rs: regset) (m: mem): Prop :=
-  st.(si_pre) ctx
-  /\ eval_smem ctx st.(si_smem) = Some m
-  /\ forall (r:reg), eval_sval ctx (st.(si_sreg) r) = Some (rs#r).
+Definition sem_sistate ctx (sis: sistate) (rs: regset) (m: mem): Prop :=
+  sis.(si_pre) ctx
+  /\ 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 st rs1 m1 rs2 m2:
-  sem_sistate ctx st rs1 m1 ->
-  sem_sistate ctx st rs2 m2 ->
+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).
@@ -556,6 +578,82 @@ Proof.
 Qed.
 
 (** * 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)).
+
+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:
+  (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.
+Admitted.
+
+Local Hint Resolve transfer_sis_correct: core.
+
+(* TODO: move the 3 below functions in [BTL] ?
+   Could be reused for liveness checking ?
+*)
+Definition reg_builtin_res (res: builtin_res reg): option reg :=
+  match res with
+  | BR r => Some r
+  | _ => None
+  end.
+
+Definition poly_tr {A} (tr: function -> list exit -> option reg -> A) f (i: final): A := 
+  match i with
+  | Bgoto pc => tr f [pc] None
+  | Bcall sig ros args res pc => tr f [pc] (Some res)
+  | Btailcall sig ros args => tr f [] None
+  | Bbuiltin ef args res pc => tr f [pc] (reg_builtin_res res)
+  | Breturn or => tr f [] None
+  | Bjumptable reg tbl => tr f tbl None
+  end.
+
+Definition tr_regs: function -> final -> regset -> regset :=
+  poly_tr tr_inputs.
+
+Definition tr_sis: function -> final -> sistate -> sistate := 
+  poly_tr transfer_sis.
+
+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).
+  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).
+  destruct fin; simpl; econstructor; simpl; intuition eauto.
+Qed.
+
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
@@ -582,10 +680,10 @@ 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 tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i 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 -> 
+  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). 
+  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.
@@ -597,21 +695,20 @@ Proof.
     - erewrite eval_list_sval_inj; simpl; auto.
   + (* Bbuiltin *) intros. eapply exec_Sbuiltin; eauto.
     eapply seval_builtin_args_correct; eauto.
+    admit.
   + (* Bjumptable *) intros. eapply exec_Sjumptable; eauto. congruence.
-Qed.
+Admitted.
 
 Local Hint Constructors final_step: core.
 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 (sexec_final_sfv i sis) rs m t s
-  -> final_step tid (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
+  -> final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs m i t s.
 Proof.
   intros (PRE&MEM&REG).
   destruct i; simpl; intros LAST; inv LAST; eauto.
-  + (* Bgoto *)
-    econstructor.
   + (* Breturn *)
     enough (v=regmap_optget res Vundef rs) as ->; eauto.
     destruct res; simpl in *; congruence.
@@ -625,8 +722,6 @@ Proof.
     intros; eapply exec_Btailcall; eauto.
     destruct fn; simpl in * |- *; auto.
     rewrite REG in * |- ; auto.
-  + (* Bbuiltin *)
-    eapply (exec_Bbuiltin tid); eauto.
   + (* Bjumptable *)
     eapply exec_Bjumptable; eauto.
     congruence.
@@ -752,9 +847,10 @@ 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 m
-     (SIS: sem_sistate ctx sis rs m)
-     (SFV: sem_sfval ctx sfv rs m t s)
+  | 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_sstate ctx t s (Sfinal sis sfv)
   | sem_Scond b cond args sm ifso ifnot
      (SEVAL: seval_condition ctx cond args sm = Some b)
@@ -774,9 +870,9 @@ pour représenter l'ensemble des chemins.
 
 *)
 
-Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := 
+Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := 
   match ib with
-  | BF fin => Sfinal sis (sexec_final_sfv fin sis)
+  | BF fin => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis)
   (* basic instructions *)
   | Bnop => k sis
   | Bop op args res => k (sexec_op op args res sis)
@@ -785,19 +881,19 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
-      sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
+      sexec_rec f ib1 sis (fun sis2 => sexec_rec f ib2 sis2 k) 
   | Bcond cond args ifso ifnot _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
-      let ifso := sexec_rec ifso sis k in
-      let ifnot := sexec_rec ifnot sis k in
+      let ifso := sexec_rec f ifso sis k in
+      let ifnot := sexec_rec f ifnot sis k in
       Scond cond args sis.(si_smem) ifso ifnot
   end
   .
 
-Definition sexec ib := sexec_rec ib sis_init (fun _ => Sabort).
+Definition sexec f ib := sexec_rec f ib sis_init (fun _ => Sabort).
 
 Local Hint Constructors sem_sstate: core.
-Local Hint Resolve sexec_op_correct sexec_final_svf_correct 
+Local Hint Resolve sexec_op_correct sexec_final_svf_correct tr_sis_regs_correct_aux tr_sis_regs_correct
                    sexec_load_TRAP_correct sexec_store_correct sis_init_correct: core.
 
 Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
@@ -805,16 +901,16 @@ Lemma sexec_rec_correct ctx t s ib rs m rs1 m1 ofin
   (SIS: sem_sistate ctx sis rs m)
   (CONT: match ofin with
          | None => forall sis', sem_sistate ctx sis' rs1 m1 -> sem_sstate ctx t s (k sis')
-         | Some fin => final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
+         | Some fin => final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs1 m1 fin t s
          end),
-  sem_sstate ctx t s (sexec_rec ib sis k).
+  sem_sstate ctx t s (sexec_rec (cf ctx) ib sis k).
 Proof.
   induction ISTEP; simpl; try autodestruct; eauto.
   (* condition *)
   all: intros;
     eapply sem_Scond; eauto; [
       erewrite seval_condition_eq; eauto |
-      replace (if b then sexec_rec ifso sis k else sexec_rec ifnot sis k) with (sexec_rec (if b then ifso else ifnot) sis k); 
+      replace (if b then sexec_rec (cf ctx) ifso sis k else sexec_rec (cf ctx) ifnot sis k) with (sexec_rec (cf ctx) (if b then ifso else ifnot) sis k); 
       try autodestruct; eauto ].
 Qed.
 
@@ -822,8 +918,8 @@ Qed.
   (sexec is a correct over-approximation)
 *)
 Theorem sexec_correct ctx ib t s: 
-  iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
-  sem_sstate ctx t s (sexec ib).
+  iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s ->
+  sem_sstate ctx t s (sexec (cf ctx) ib).
 Proof.
   destruct 1 as (rs' & m' & fin & ISTEP & FSTEP).
   eapply sexec_rec_correct; simpl; eauto.
@@ -901,6 +997,9 @@ Proof.
   - repeat (rewrite Regmap.gso); auto.
 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) -> 
@@ -911,6 +1010,7 @@ Proof.
   destruct 1; eexists; split; econstructor; eauto.
   econstructor; eauto.
 Qed.
+*)
 
 Local Hint Resolve sexec_final_svf_exact: core.
 
@@ -973,13 +1073,14 @@ Local Hint Resolve sexec_op_preserves_abort sexec_load_preserves_abort
   sexec_store_preserves_abort: core.
 
 Lemma sexec_exclude_abort ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   (ABORT: abort_sistate ctx sis),
   False.
 Proof.
   induction ib; simpl; intros; eauto.
   - (* final *) inversion SEXEC; subst; eauto.
+    admit.
   - (* load *) destruct trap; eauto.
     inversion SEXEC.
   - (* seq *)
@@ -988,7 +1089,7 @@ Proof.
   - (* cond *)
     inversion SEXEC; subst; eauto. clear SEXEC.
     destruct b; eauto.
-Qed.
+Admitted.
 
 Lemma set_sreg_abort ctx dst sv sis rs m:
   sem_sistate ctx sis rs m -> 
@@ -1048,14 +1149,14 @@ Qed.
 Local Hint Resolve sexec_op_abort sexec_load_TRAP_abort sexec_store_abort: core.
 
 Lemma sexec_rec_exact ctx ib t s1: forall sis k
-  (SEXEC: sem_sstate ctx t s1 (sexec_rec ib sis k))
+  (SEXEC: sem_sstate ctx t s1 (sexec_rec (cf ctx) ib sis k))
   rs m
   (SIS: sem_sistate ctx sis rs m)
   (CONT: forall sis', sem_sstate ctx t s1 (k sis') -> (abort_sistate ctx sis') -> False)
   ,
      match iblock_istep_run (cge ctx) (csp ctx) ib rs m with
      | Some (out rs' m' (Some fin)) =>
-        exists s2, final_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
+        exists s2, final_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) rs' m' fin t s2 /\ equiv_state s1 s2
      | Some (out rs' m' None) => exists sis', (sem_sstate ctx t s1 (k sis')) /\ (sem_sistate ctx sis' rs' m')
      | None => False
      end.
@@ -1063,11 +1164,13 @@ Proof.
   induction ib; simpl; intros; eauto.
   - (* final *)
     inv SEXEC.
+    admit.
+    (* TODO
     exploit (sem_sistate_determ ctx sis rs m rs0 m0); eauto.
     intros (REG&MEM); subst.
     exploit (sem_sfval_equiv rs0 rs); eauto.
     intros (s2 & EQUIV & SFV').
-    eexists; split; eauto.
+    eexists; split; eauto. *)
   - (* Bop *) autodestruct; eauto.
   - destruct trap; [| inv SEXEC ].
     repeat autodestruct; eauto.
@@ -1093,15 +1196,15 @@ Proof.
     destruct b.
     + exploit IHib1; eauto.
     + exploit IHib2; eauto.
-Qed.
+Admitted.
 
 
 (* NB: each execution of a symbolic state (produced from [sexec]) represents a concrete execution
   (sexec is exact).
 *)
 Theorem sexec_exact ctx ib t s1: 
-  sem_sstate ctx t s1 (sexec ib) ->
-  exists s2, iblock_step tid (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
+  sem_sstate ctx t s1 (sexec (cf ctx) ib) ->
+  exists s2, iblock_step tr_inputs (cge ctx) (cstk ctx) (cf ctx) (csp ctx) (crs0 ctx) (cm0 ctx) ib t s2
              /\ equiv_state s1 s2.
 Proof.
   intros; exploit sexec_rec_exact; eauto.