Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-work

10 files changed, 406 insertions, 228 deletions

diff --git a/scheduling/RTLpath.v b/scheduling/RTLpath.v
index cccc8147..5b34dc16 100644
--- a/scheduling/RTLpath.v
+++ b/scheduling/RTLpath.v
@@ -85,6 +85,7 @@ Record path_info := {
     psize: nat; (* number minus 1 of instructions in the path *)
     input_regs: Regset.t;
     (** Registers that are used (as input_regs) by the "fallthrough successors" of the path *)
+    pre_output_regs: Regset.t;
     (** This field is not used by the verificator, but is helpful for the superblock scheduler *)
     output_regs: Regset.t 
 }.
diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v
index 1f0ebe3c..7855d375 100644
--- a/scheduling/RTLpathLivegen.v
+++ b/scheduling/RTLpathLivegen.v
@@ -152,47 +152,69 @@ Qed.
 
 Local Hint Resolve exit_list_checker_correct: core.
 
-Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit :=
+Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
    match i with
    | Icall sig ros args res pc' =>
       ASSERT list_mem args alive IN
       ASSERT reg_sum_mem ros alive IN
-      exit_checker pm (Regset.add res alive) pc' tt
+      exit_checker pm (Regset.add res por) pc' tt
    | Itailcall sig ros args =>
       ASSERT list_mem args alive IN
       ASSERT reg_sum_mem ros alive IN
       Some tt
    | Ibuiltin ef args res pc' =>
-      ASSERT list_mem (params_of_builtin_args args) alive IN 
-      exit_checker pm (reg_builtin_res res alive) pc' tt
+      ASSERT list_mem (params_of_builtin_args args) alive IN
+      exit_checker pm (reg_builtin_res res por) pc' tt
    | Ijumptable arg tbl =>
       ASSERT Regset.mem arg alive IN
-      ASSERT exit_list_checker pm alive tbl IN
+      ASSERT exit_list_checker pm por tbl IN
       Some tt
    | Ireturn optarg =>
-      ASSERT (reg_option_mem optarg) alive IN 
+      ASSERT (reg_option_mem optarg) alive IN
       Some tt
-   | _ => 
-      SOME res <- iinst_checker pm alive i IN
-      exit_checker pm (fst res) (snd res) tt
+   | _ => None
    end.
 
-Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
-  inst_checker pm alive i = Some tt ->
+Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
+  final_inst_checker pm alive por i = Some tt ->
   c!pc = Some i -> wellformed_path c pm 0 pc.
 Proof.
   intros CHECK PC. eapply wf_last_node; eauto.
   clear c pc PC. intros pc PC.
   destruct i; simpl in * |- *; intuition (subst; eauto);
   try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
-  intros X; exploit exit_checker_res; eauto.
-  clear X. intros; subst; eauto.
+Qed.
+
+Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
+   match iinst_checker pm alive i with
+   | Some res =>
+      ASSERT Regset.subset por (fst res) IN
+      exit_checker pm por (snd res) tt
+   | _ => 
+      ASSERT Regset.subset por alive IN
+      final_inst_checker pm alive por i
+   end.
+
+Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
+  inst_checker pm alive por i = Some tt ->
+  c!pc = Some i -> wellformed_path c pm 0 pc.
+Proof.
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
+  - simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
+    destruct i; simpl in * |- *; intuition (subst; eauto);
+    try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
+    intros PC CHECK1 CHECK2. 
+    intros; exploit exit_checker_res; eauto.
+    intros X; inversion X. intros; subst; eauto.
+  - simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto.
+    generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps.
 Qed.
 
 Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
    SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc  IN
    SOME i <- f.(fn_code)!(snd res) IN
-   inst_checker pm (fst res) i.
+   inst_checker pm (fst res) (path.(pre_output_regs)) i.
 
 Lemma path_checker_wellformed f pm pc path:
    path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.
diff --git a/scheduling/RTLpathLivegenaux.ml b/scheduling/RTLpathLivegenaux.ml
index ab921954..db3fc9d4 100644
--- a/scheduling/RTLpathLivegenaux.ml
+++ b/scheduling/RTLpathLivegenaux.ml
@@ -99,7 +99,7 @@ let get_path_map code entry join_points =
                 dig_path_rec n'
               end
           | None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
-                            input_regs = Regset.empty; output_regs = Regset.empty },
+                            input_regs = Regset.empty; pre_output_regs = Regset.empty; output_regs = Regset.empty },
                         !path_successors @ successors_inst inst)
         end
       else None
@@ -217,41 +217,50 @@ let analyze f =
 
 let rec traverse code n size =
   let inst = get_some @@ PTree.get n code in
-  if (size == 0) then inst
+  if (size == 0) then (inst, n)
   else 
     let n' = get_some @@ predicted_successor inst in
     traverse code n' (size-1)
 
-let get_outputs liveness code n pi =
-  let last_instruction = traverse code n (Camlcoq.Nat.to_int pi.psize) in
+let get_outputs liveness f n pi =
+  let (last_instruction, pc_last) = traverse f.fn_code n (Camlcoq.Nat.to_int pi.psize) in
   let path_last_successors = successors_inst last_instruction in
   let list_input_regs = List.map (
       fun n -> get_some @@ PTree.get n liveness
     ) path_last_successors in
-  List.fold_left Regset.union Regset.empty list_input_regs
+  let outputs = List.fold_left Regset.union Regset.empty list_input_regs in
+
+  match last_instruction with
+  | Icall (_, _, _, _, _) | Itailcall (_, _, _)
+  | Ibuiltin (_, _, _, _) | Ijumptable (_, _)
+  | Ireturn _ -> ((transfer f pc_last outputs), outputs)
+  | _ -> (outputs, outputs)
 
 let set_pathmap_liveness f pm =
   let liveness = analyze f in
   let new_pm = ref PTree.empty in
-  let code = f.fn_code in
   begin
     debug "Liveness: "; print_ptree_regset liveness; debug "\n";
     List.iter (fun (n, pi) ->
       let inputs = get_some @@ PTree.get n liveness in
-      let outputs = get_outputs liveness code n pi in
+      let (por, outputs) = get_outputs liveness f n pi in
       new_pm := PTree.set n
-        {psize=pi.psize; input_regs=inputs; output_regs=outputs} !new_pm
+                  {psize=pi.psize; input_regs=inputs; pre_output_regs=por; output_regs=outputs} !new_pm (* FIXME: STUB *)
     ) (PTree.elements pm);
     !new_pm
   end
 
 let print_path_info pi = begin
+  (*debug_flag := true;*)
   debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
-  debug "input_regs=";
+  debug "\ninput_regs=";
   print_regset pi.input_regs;
-  debug "; output_regs=";
+  debug "\n; pre_output_regs=";
+  print_regset pi.pre_output_regs;
+  debug "\n; output_regs=";
   print_regset pi.output_regs;
-  debug ")"
+  debug ")\n"
+  (*debug_flag := false*)
 end
 
 let print_path_map path_map = begin
diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v
index c6125985..b02400bf 100644
--- a/scheduling/RTLpathLivegenproof.v
+++ b/scheduling/RTLpathLivegenproof.v
@@ -280,34 +280,22 @@ Proof.
     intuition.
   - (* Iload *)
     inversion_ASSERT; try_simplify_someHyps.
-    destruct t. (* TODO - simplify that proof ? *)
-    + inversion_SOME a0. intros EVAL.
-      erewrite <- eqlive_reg_listmem; eauto.
-      try_simplify_someHyps.
-      inversion_SOME v; try_simplify_someHyps.
-      repeat (econstructor; simpl; eauto).
-      eapply eqlive_reg_update.
-      eapply eqlive_reg_monotonic; eauto.
-      intros r0; rewrite regset_add_spec.
+    destruct t.
+    inversion_SOME a0. intros EVAL.
+    erewrite <- eqlive_reg_listmem; eauto.
+    try_simplify_someHyps.
+    inversion_SOME v; try_simplify_someHyps.
+    repeat (econstructor; simpl; eauto).
+    2:
+      erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto;
+      destruct (eval_addressing _ _ _ _);
+      try destruct (Memory.Mem.loadv _ _ _);
+      try (intros; inv H1; repeat (econstructor; simpl; eauto)).
+    all:
+      eapply eqlive_reg_update;
+      eapply eqlive_reg_monotonic; eauto;
+      intros r0; rewrite regset_add_spec;
       intuition.
-    + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
-      destruct (eval_addressing _ _ _ _).
-      * destruct (Memory.Mem.loadv _ _ _).
-        ** intros. inv H1. repeat (econstructor; simpl; eauto).
-           eapply eqlive_reg_update.
-           eapply eqlive_reg_monotonic; eauto.
-           intros r0; rewrite regset_add_spec.
-           intuition.
-        ** intros. inv H1. repeat (econstructor; simpl; eauto).
-           eapply eqlive_reg_update.
-           eapply eqlive_reg_monotonic; eauto.
-           intros r0; rewrite regset_add_spec.
-           intuition.
-      * intros. inv H1. repeat (econstructor; simpl; eauto).
-        eapply eqlive_reg_update.
-        eapply eqlive_reg_monotonic; eauto.
-        intros r0; rewrite regset_add_spec.
-        intuition.
   - (* Istore *)
     (repeat inversion_ASSERT); try_simplify_someHyps.
     inversion_SOME a0. intros EVAL.
@@ -501,12 +489,23 @@ Proof.
   intros H; erewrite (EQLIVE r); eauto.
 Qed.
 
+Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por:
+  istep ge i sp rs m = Some st -> 
+  final_inst_checker pm alive por i = None.
+Proof.
+  destruct i; simpl; try congruence.
+Qed.
+
+(* is it useful ?
 Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
   istep ge i sp rs m = Some st -> 
   inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
 Proof.
-  destruct i; simpl; try congruence. 
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i); simpl; auto.
+  destruct i; simpl; try congruence.
 Qed.
+*)
 
 Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
   exit_checker pm (Regset.add r alive) pc tt = Some tt ->  
@@ -586,16 +585,17 @@ Proof.
     * intuition. eapply IHtbl; eauto.
 Qed.
 
-Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
+  Regset.Subset por alive ->
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
-  inst_checker (fn_path f) alive i = Some tt -> 
+  final_inst_checker (fn_path f) alive por i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
 Proof.
-  intros STACKS EQLIVE LIVENESS PC; 
+  intros STACKS EQLIVE SUB LIVENESS PC; 
   destruct 1 as [i' sp pc rs1 m st1|
                  sp pc rs1 m sig ros args res pc' fd|
                  st1 pc rs1 m sig ros args fd m'|
@@ -604,28 +604,12 @@ Proof.
                  st1 pc rs1 m optr m']; 
   try_simplify_someHyps.
   + (* istate *)
-    intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
-    inversion_SOME res.
-    intros.
-    destruct (icontinue st1) eqn: CONT.
-    - (* CONT => true *)
-      exploit iinst_checker_eqlive; eauto.
-      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      exploit exit_checker_eqlive; eauto.
-      intros (path & PATH & EQLIVE2).
-      eapply eqlive_states_intro; eauto.
-      erewrite <- iinst_checker_istep_continue; eauto.
-    - (* CONT => false *)
-      intros; exploit iinst_checker_eqlive_stopped; eauto.
-      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      eapply eqlive_states_intro; eauto.
+    intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto.
+    congruence.
   + (* Icall *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_ext1; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Icall; eauto.
@@ -645,6 +629,7 @@ Proof.
   + (* Ibuiltin *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_builtin_res; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Ibuiltin; eauto.
@@ -654,6 +639,7 @@ Proof.
   + (* Ijumptable *)
     repeat inversion_ASSERT. intros.
     exploit exit_list_checker_eqlive; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Ijumptable; eauto.
@@ -669,6 +655,44 @@ Proof.
       * eapply eqlive_states_return; eauto.
 Qed.
 
+Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
+  list_forall2 eqlive_stackframes stk1 stk2 ->
+  eqlive_reg (ext alive) rs1 rs2 -> 
+  liveness_ok_function f ->
+  (fn_code f) ! pc = Some i ->
+  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
+  inst_checker (fn_path f) alive por i = Some tt -> 
+  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
+Proof.
+  unfold inst_checker;
+  intros STACKS EQLIVE LIVENESS PC.
+  destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
+  + destruct 1 as [i' sp pc rs1 m st1| | | | | ];
+    try_simplify_someHyps.
+    intros IICHECKER PC ISTEP. inversion_ASSERT.
+    intros.
+    destruct (icontinue st1) eqn: CONT.
+    - (* CONT => true *)
+      exploit iinst_checker_eqlive; eauto.
+      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      apply Regset.subset_2 in H.
+      exploit exit_checker_eqlive; eauto.
+      eapply eqlive_reg_monotonic; eauto.
+      intros (path & PATH & EQLIVE2).
+      eapply eqlive_states_intro; eauto.
+      erewrite <- iinst_checker_istep_continue; eauto.
+    - (* CONT => false *)
+      intros; exploit iinst_checker_eqlive_stopped; eauto.
+      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      eapply eqlive_states_intro; eauto.
+  + inversion_ASSERT.
+    intros; exploit final_inst_checker_eqlive; eauto.
+Qed.
+
 Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
   path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
   list_forall2 eqlive_stackframes stk1 stk2 ->
diff --git a/scheduling/RTLpathSE_impl.v b/scheduling/RTLpathSE_impl.v
index 1e36a558..ada0d308 100644
--- a/scheduling/RTLpathSE_impl.v
+++ b/scheduling/RTLpathSE_impl.v
@@ -1923,22 +1923,6 @@ Qed.
 Global Opaque PTree_frame_eq_check.
 Local Hint Resolve PTree_frame_eq_check_correct: wlp.
 
-Definition hsilocal_simu_check hst1 hst2 : ?? unit :=
-  DEBUG("? last check");;
-  phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_simu_check: hsi_smem sets aren't equiv";;
-  PTree_eq_check (hsi_sreg hst1) (hsi_sreg hst2);;
-  Sets.assert_list_incl mk_hash_params (hsi_ok_lsval hst2) (hsi_ok_lsval hst1);;
-  DEBUG("=> last check: OK").
-
-Lemma hsilocal_simu_check_correct hst1 hst2:
-  WHEN hsilocal_simu_check hst1 hst2 ~> _ THEN
-  hsilocal_simu_spec None hst1 hst2.
-Proof.
-  unfold hsilocal_simu_spec; wlp_simplify. 
-Qed.
-Hint Resolve hsilocal_simu_check_correct: wlp.
-Global Opaque hsilocal_simu_check.
-
 Definition hsilocal_frame_simu_check frame hst1 hst2 : ?? unit :=
   DEBUG("? frame check");;
   phys_check (hsi_smem hst2) (hsi_smem hst1) "hsilocal_frame_simu_check: hsi_smem sets aren't equiv";;
@@ -1966,7 +1950,7 @@ Local Hint Resolve regset_elements_in: core.
 
 Lemma hsilocal_frame_simu_check_correct hst1 hst2 alive:
   WHEN hsilocal_frame_simu_check (Regset.elements alive) hst1 hst2 ~> _ THEN
-  hsilocal_simu_spec (Some alive) hst1 hst2.
+  hsilocal_simu_spec alive hst1 hst2.
 Proof.
   unfold hsilocal_simu_spec; wlp_simplify. symmetry; eauto.
 Qed.
@@ -2020,13 +2004,13 @@ Qed.
 Hint Resolve hsiexits_simu_check_correct: wlp.
 Global Opaque hsiexits_simu_check.
 
-Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
+Definition hsistate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsistate) :=
   hsiexits_simu_check dm f (hsi_exits hst1) (hsi_exits hst2);;
-  hsilocal_simu_check (hsi_local hst1) (hsi_local hst2).
+  hsilocal_frame_simu_check (Regset.elements outframe) (hsi_local hst1) (hsi_local hst2).
 
-Lemma hsistate_simu_check_correct dm f hst1 hst2:
-  WHEN hsistate_simu_check dm f hst1 hst2 ~> _ THEN
-  hsistate_simu_spec dm f hst1 hst2.
+Lemma hsistate_simu_check_correct dm f outframe hst1 hst2:
+  WHEN hsistate_simu_check dm f outframe hst1 hst2 ~> _ THEN
+  hsistate_simu_spec dm f outframe hst1 hst2.
 Proof.
   unfold hsistate_simu_spec; wlp_simplify.
 Qed.
@@ -2160,18 +2144,18 @@ Qed.
 Hint Resolve sfval_simu_check_correct: wlp.
 Global Opaque sfval_simu_check.
 
-Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
-  hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
+Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) :=
+  hsistate_simu_check dm f outframe (hinternal hst1) (hinternal hst2);;
   sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
-Lemma hsstate_simu_check_correct dm f hst1 hst2:
-  WHEN hsstate_simu_check dm f hst1 hst2 ~> _ THEN
-  hsstate_simu_spec dm f hst1 hst2.
+Lemma hsstate_simu_check_correct dm f outframe hst1 hst2:
+  WHEN hsstate_simu_check dm f outframe hst1 hst2 ~> _ THEN
+  hsstate_simu_spec dm f outframe hst1 hst2.
 Proof.
   unfold hsstate_simu_spec; wlp_simplify.
 Qed.
 Hint Resolve hsstate_simu_check_correct: wlp.
-Global Opaque hsstate_simu_check. 
+Global Opaque hsstate_simu_check.
 
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
   let (pc2, pc1) := m in
@@ -2185,8 +2169,10 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   DO hst1 <~ hsexec f pc1;;
   XDEBUG pc2 (fun pc => DO name_pc <~ string_of_Z (Zpos pc);; RET ("entry-point of output superblock: " +; name_pc)%string);;
   DO hst2 <~ hsexec tf pc2;;
+  DO path <~ some_or_fail ((fn_path f)!pc1) "simu_check_single.internal_error.1";;
+  let outframe := path.(pre_output_regs) in
   (* comparing the executions *)
-  hsstate_simu_check dm f hst1 hst2.
+  hsstate_simu_check dm f outframe hst1 hst2.
 
 Lemma simu_check_single_correct dm tf f pc1 pc2:
   WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
@@ -2197,7 +2183,7 @@ Proof.
   intros (st2 & SEXEC2 & REF2). try_simplify_someHyps.
   exploit H3; clear H3. 1-3: wlp_simplify.
   intros (st3 & SEXEC3 & REF3). try_simplify_someHyps.
-  eexists. split; eauto.
+  eexists. eexists. split; eauto. split; eauto.
   intros ctx.
   eapply hsstate_simu_spec_correct; eauto.
 Qed.
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v
index c9e272c0..589cf25f 100644
--- a/scheduling/RTLpathSE_simu_specs.v
+++ b/scheduling/RTLpathSE_simu_specs.v
@@ -18,10 +18,10 @@ Local Open Scope list_scope.
 
 (** * Auxilary notions on simulation tests *)
 
-Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
+Definition silocal_simu (dm: PTree.t node) (f: RTLpath.function) outframe (sl1 sl2: sistate_local) (ctx: simu_proof_context f): Prop :=
     forall is1, ssem_local (the_ge1 ctx) (the_sp ctx) sl1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) ->
     exists is2, ssem_local (the_ge2 ctx) (the_sp ctx) sl2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2)
-                /\ istate_simu f dm is1 is2.
+                /\ istate_simu f dm outframe is1 is2.
 
 (* a kind of negation of sabort_local *)
 Definition sok_local (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) (st: sistate_local): Prop :=
@@ -36,7 +36,7 @@ Proof.
   intuition congruence.
 Qed.
 
-Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
+Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) outframe (ctx: simu_proof_context f) (se1 se2: sistate_exit) :=
   (sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1) ->
           (seval_condition (the_ge1 ctx) (the_sp ctx) (si_cond se1) (si_scondargs se1) 
                              (si_smem (si_elocal se1)) (the_rs0 ctx) (the_m0 ctx)) =
@@ -47,10 +47,10 @@ Definition siexit_simu (dm: PTree.t node) (f: RTLpath.function) (ctx: simu_proof
       ssem_exit (the_ge1 ctx) (the_sp ctx) se1 (the_rs0 ctx) (the_m0 ctx) (irs is1) (imem is1) (ipc is1) ->
       exists is2,
           ssem_exit (the_ge2 ctx) (the_sp ctx) se2 (the_rs0 ctx) (the_m0 ctx) (irs is2) (imem is2) (ipc is2)
-      /\  istate_simu f dm is1 is2.
+      /\  istate_simu f dm outframe is1 is2.
 
-Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
-  list_forall2 (siexit_simu dm f ctx) lse1 lse2.
+Definition siexits_simu (dm: PTree.t node) (f: RTLpath.function) outframe (lse1 lse2: list sistate_exit) (ctx: simu_proof_context f) :=
+  list_forall2 (siexit_simu dm f outframe ctx) lse1 lse2.
 
 
 (** * Implementation of Data-structure use in Hash-consing *)
@@ -318,9 +318,9 @@ Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
 (** ** Specification of the simulation test on [hsistate_local].
        It is motivated by [hsilocal_simu_spec_correct theorem] below
 *)
-Definition hsilocal_simu_spec (oalive: option Regset.t) (hst1 hst2: hsistate_local) :=
+Definition hsilocal_simu_spec (alive: Regset.t) (hst1 hst2: hsistate_local) :=
      List.incl (hsi_ok_lsval hst2) (hsi_ok_lsval hst1)
-  /\ (forall r, (match oalive with Some alive => Regset.In r alive | _ => True end) -> PTree.get r hst2 = PTree.get r hst1)
+  /\ (forall r, Regset.In r alive -> PTree.get r hst2 = PTree.get r hst1)
   /\ hsi_smem hst1 = hsi_smem hst2.
 
 Definition seval_sval_partial ge sp rs0 m0 hsv :=
@@ -368,18 +368,14 @@ Proof.
   - erewrite MEMOK in OKM. erewrite smem_eval_preserved; eauto.
 Qed.
 
-Theorem hsilocal_simu_spec_correct hst1 hst2 of ge1 ge2 sp rs0 m0 rs m st1 st2:
-  hsilocal_simu_spec of hst1 hst2 ->
+Theorem hsilocal_simu_spec_correct hst1 hst2 alive ge1 ge2 sp rs0 m0 rs m st1 st2:
+  hsilocal_simu_spec alive hst1 hst2 ->
   hsilocal_refines ge1 sp rs0 m0 hst1 st1 ->
   hsilocal_refines ge2 sp rs0 m0 hst2 st2 ->
   (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
   ssem_local ge1 sp st1 rs0 m0 rs m ->
-  match of with
-  | None => ssem_local ge2 sp st2 rs0 m0 rs m
-  | Some alive => 
-      let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
-      in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'
-  end.
+  let rs' := seval_partial_regset ge2 sp rs0 m0 (hsi_sreg hst2)
+  in ssem_local ge2 sp st2 rs0 m0 rs' m /\ eqlive_reg (fun r => Regset.In r alive) rs rs'.
 Proof.
   intros CORE HREF1 HREF2 GFS SEML.
   refine (modusponens _ _ (ssem_local_refines_hok _ _ _ _ _ _ _ _ _ _) _); eauto.
@@ -394,9 +390,8 @@ Proof.
     rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
     erewrite smem_eval_preserved; [| eapply GFS].
     rewrite MEMEQ1; auto. }
-  destruct of as [alive |].
-  - constructor.
-    + constructor; [assumption | constructor; [assumption|]].
+   constructor.
+   + constructor; [assumption | constructor; [assumption|]].
       destruct HREF2 as (B & _ & A & _).
       (** B is used for the auto below. *)
       assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
@@ -420,17 +415,6 @@ Proof.
          unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; [|assumption]. rewrite RSEQ. reflexivity.
       ++ rewrite <- RSEQ. rewrite <- B; [|assumption]. unfold hsi_sreg_eval, hsi_sreg_proj.
          rewrite <- C; [|assumption]. rewrite HST2. reflexivity.
-  - constructor; [|constructor].
-    + destruct HREF2 as (OKEQ & _ & _). rewrite <- OKEQ in HOK2. apply HOK2.
-    + destruct HREF2 as (_ & MEMEQ2 & _). destruct HREF1 as (_ & MEMEQ1 & _).
-      destruct CORE as (_ & _ & MEMEQ3).
-      rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
-      erewrite smem_eval_preserved; [| eapply GFS].
-      rewrite MEMEQ1; auto.
-    + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
-      destruct CORE as (_ & C & _). rewrite <- A; auto. unfold hsi_sreg_eval, hsi_sreg_proj.
-      rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS].
-      unfold hsi_sreg_eval, hsi_sreg_proj in B; rewrite B; auto.
 Qed.
 
 (** ** Specification of the simulation test on [hsistate_exit].
@@ -438,17 +422,17 @@ Qed.
 *)
 Definition hsiexit_simu_spec dm f (hse1 hse2: hsistate_exit) :=
   (exists path, (fn_path f) ! (hsi_ifso hse1) = Some path
-    /\ hsilocal_simu_spec (Some path.(input_regs)) (hsi_elocal hse1) (hsi_elocal hse2))
+    /\ hsilocal_simu_spec path.(input_regs) (hsi_elocal hse1) (hsi_elocal hse2))
   /\ dm ! (hsi_ifso hse2) = Some (hsi_ifso hse1)
   /\ hsi_cond hse1 = hsi_cond hse2
   /\ hsi_scondargs hse1 = hsi_scondargs hse2.
 
-Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
+Definition hsiexit_simu dm f outframe (ctx: simu_proof_context f) hse1 hse2: Prop := forall se1 se2,
   hsiexit_refines_stat hse1 se1 ->
   hsiexit_refines_stat hse2 se2 ->
   hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
   hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
-  siexit_simu dm f ctx se1 se2.
+  siexit_simu dm f outframe ctx se1 se2.
 
 Lemma hsiexit_simu_spec_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
   hsiexit_simu_spec dm f hse1 hse2 ->
@@ -461,9 +445,9 @@ Proof.
   eapply hsilocal_simu_spec_nofail; eauto.
 Qed.
 
-Theorem hsiexit_simu_spec_correct dm f hse1 hse2 ctx:
+Theorem hsiexit_simu_spec_correct dm f outframe hse1 hse2 ctx:
   hsiexit_simu_spec dm f hse1 hse2 ->
-  hsiexit_simu dm f ctx hse1 hse2.
+  hsiexit_simu dm f outframe ctx hse1 hse2.
 Proof.
   intros SIMUC st1 st2 HREF1 HREF2 HDYN1 HDYN2.
   assert (SEVALC:
@@ -498,13 +482,13 @@ Proof.
     constructor; [|constructor]; simpl; auto.
 Qed.
 
-Remark hsiexit_simu_siexit dm f ctx hse1 hse2 se1 se2:
-  hsiexit_simu dm f ctx hse1 hse2 ->
+Remark hsiexit_simu_siexit dm f outframe ctx hse1 hse2 se1 se2:
+  hsiexit_simu dm f outframe ctx hse1 hse2 ->
   hsiexit_refines_stat hse1 se1 ->
   hsiexit_refines_stat hse2 se2 ->
   hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
   hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
-  siexit_simu dm f ctx se1 se2.
+  siexit_simu dm f outframe ctx se1 se2.
 Proof.
   auto.
 Qed.
@@ -513,15 +497,15 @@ Qed.
        It is motivated by [hsiexit_simu_spec_correct theorem] below
 *)
 
-Definition hsiexits_simu dm f (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop :=
-  list_forall2 (hsiexit_simu dm f ctx) lhse1 lhse2.
+Definition hsiexits_simu dm f outframe (ctx: simu_proof_context f) (lhse1 lhse2: list hsistate_exit): Prop :=
+  list_forall2 (hsiexit_simu dm f outframe ctx) lhse1 lhse2.
 
 Definition hsiexits_simu_spec dm f lhse1 lhse2: Prop :=
   list_forall2 (hsiexit_simu_spec dm f) lhse1 lhse2.
 
-Theorem hsiexits_simu_spec_correct dm f lhse1 lhse2 ctx:
+Theorem hsiexits_simu_spec_correct dm f outframe lhse1 lhse2 ctx:
   hsiexits_simu_spec dm f lhse1 lhse2 ->
-  hsiexits_simu dm f ctx lhse1 lhse2.
+  hsiexits_simu dm f outframe ctx lhse1 lhse2.
 Proof.
   induction 1; [constructor|].
   constructor; [|apply IHlist_forall2; assumption].
@@ -529,8 +513,8 @@ Proof.
 Qed.
 
 
-Lemma siexits_simu_all_fallthrough dm f ctx: forall lse1 lse2,
-  siexits_simu dm f lse1 lse2 ctx ->
+Lemma siexits_simu_all_fallthrough dm f outframe ctx: forall lse1 lse2,
+  siexits_simu dm f outframe lse1 lse2 ctx ->
   all_fallthrough (the_ge1 ctx) (the_sp ctx) lse1 (the_rs0 ctx) (the_m0 ctx) ->
   (forall se1, In se1 lse1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
   all_fallthrough (the_ge2 ctx) (the_sp ctx) lse2 (the_rs0 ctx) (the_m0 ctx).
@@ -545,8 +529,8 @@ Proof.
 Qed.
 
 
-Lemma siexits_simu_all_fallthrough_upto dm f ctx lse1 lse2:
-  siexits_simu dm f lse1 lse2 ctx ->
+Lemma siexits_simu_all_fallthrough_upto dm f outframe ctx lse1 lse2:
+  siexits_simu dm f outframe lse1 lse2 ctx ->
   forall ext1 lx1,
   (forall se1, In se1 lx1 -> sok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (si_elocal se1)) ->
   all_fallthrough_upto_exit (the_ge1 ctx) (the_sp ctx) ext1 lx1 lse1 (the_rs0 ctx) (the_m0 ctx) ->
@@ -570,14 +554,14 @@ Proof.
 Qed.
 
 
-Lemma hsiexits_simu_siexits dm f ctx lhse1 lhse2:
-  hsiexits_simu dm f ctx lhse1 lhse2 ->
+Lemma hsiexits_simu_siexits dm f outframe ctx lhse1 lhse2:
+  hsiexits_simu dm f outframe ctx lhse1 lhse2 ->
   forall lse1 lse2,
   hsiexits_refines_stat lhse1 lse1 ->
   hsiexits_refines_stat lhse2 lse2 ->
   hsiexits_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse1 lse1 ->
   hsiexits_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) lhse2 lse2 ->
-  siexits_simu dm f lse1 lse2 ctx.
+  siexits_simu dm f outframe lse1 lse2 ctx.
 Proof.
   induction 1.
   - intros. inv H. inv H0. constructor.
@@ -591,16 +575,16 @@ Qed.
        It is motivated by [hsistate_simu_spec_correct theorem] below
 *)
 
-Definition hsistate_simu_spec dm f (hse1 hse2: hsistate) :=
+Definition hsistate_simu_spec dm f outframe (hse1 hse2: hsistate) :=
      list_forall2 (hsiexit_simu_spec dm f) (hsi_exits hse1) (hsi_exits hse2)
-  /\ hsilocal_simu_spec None (hsi_local hse1) (hsi_local hse2).
+  /\ hsilocal_simu_spec outframe (hsi_local hse1) (hsi_local hse2).
 
-Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
+Definition hsistate_simu dm f outframe (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
   hsistate_refines_stat hst1 st1 ->
   hsistate_refines_stat hst2 st2 ->
   hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
   hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
-  sistate_simu dm f st1 st2 ctx.
+  sistate_simu dm f outframe st1 st2 ctx.
 
 Lemma list_forall2_nth_error {A} (l1 l2: list A) P:
   list_forall2 P l1 l2 ->
@@ -644,9 +628,9 @@ Proof.
       rewrite H0; auto.
 Qed.
 
-Theorem hsistate_simu_spec_correct dm f hst1 hst2 ctx:
-  hsistate_simu_spec dm f hst1 hst2 ->
-  hsistate_simu dm f hst1 hst2 ctx.
+Theorem hsistate_simu_spec_correct dm f outframe hst1 hst2 ctx:
+  hsistate_simu_spec dm f outframe hst1 hst2 ->
+  hsistate_simu dm f outframe hst1 hst2 ctx.
 Proof.
   intros (ESIMU & LSIMU) st1 st2 (PCREF1 & EREF1) (PCREF2 & EREF2) DREF1 DREF2 is1 SEMI.
   destruct DREF1 as (DEREF1 & LREF1 & NESTED). destruct DREF2 as (DEREF2 & LREF2 & _).
@@ -654,23 +638,27 @@ Proof.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
   - destruct SEMI as (SSEML & PCEQ & ALLFU).
     exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2.
-    exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor.
-    + unfold ssem_internal. simpl. rewrite ICONT. constructor; [assumption | constructor; [reflexivity |]].
+    exists (mk_istate (icontinue is1) (si_pc st2) (seval_partial_regset (the_ge2 ctx) (the_sp ctx) 
+              (the_rs0 ctx) (the_m0 ctx) (hsi_local hst2)) (imem is1)). constructor.
+    + unfold ssem_internal. simpl. rewrite ICONT.
+      destruct SSEML2 as [SSEMLP EQLIVE].
+      constructor; [assumption | constructor; [reflexivity |]].
       eapply siexits_simu_all_fallthrough; eauto.
       * eapply hsiexits_simu_siexits; eauto.
       * eapply nested_sok_prop; eauto.
         eapply ssem_local_sok; eauto.
-    + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]].
-      constructor.
+    + unfold istate_simu. rewrite ICONT.
+      destruct SSEML2 as [SSEMLP EQLIVE].
+      constructor; simpl; auto.
   - destruct SEMI as (ext & lx & SSEME & ALLFU).
-    assert (SESIMU: siexits_simu dm f (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
+    assert (SESIMU: siexits_simu dm f outframe (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
     exploit siexits_simu_all_fallthrough_upto; eauto.
     * destruct ALLFU as (ITAIL & ALLF).
       exploit nested_sok_tail; eauto. intros NESTED2.
       inv NESTED2. destruct SSEME as (_ & SSEML & _). eapply ssem_local_sok in SSEML.
       eapply nested_sok_prop; eauto.
     * intros (ext2 & lx2 & ALLFU2 & LENEQ).
-      assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
+      assert (EXTSIMU: siexit_simu dm f outframe ctx ext ext2). {
         eapply list_forall2_nth_error; eauto.
         - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
         - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
@@ -858,18 +846,18 @@ Qed.
        It is motivated by [hsstate_simu_spec_correct theorem] below
 *)
 
-Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
-     hsistate_simu_spec dm f (hinternal hst1) (hinternal hst2)
+Definition hsstate_simu_spec (dm: PTree.t node) (f: RTLpath.function) outframe (hst1 hst2: hsstate) :=
+     hsistate_simu_spec dm f outframe (hinternal hst1) (hinternal hst2)
   /\ hfinal_simu_spec dm f (hsi_pc (hinternal hst1)) (hsi_pc (hinternal hst2)) (hfinal hst1) (hfinal hst2).
 
-Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
+Definition hsstate_simu dm f outframe (hst1 hst2: hsstate) ctx: Prop :=
   forall st1 st2,
   hsstate_refines hst1 st1 ->
-  hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.
+  hsstate_refines hst2 st2 -> sstate_simu dm f outframe st1 st2 ctx.
 
-Theorem hsstate_simu_spec_correct dm f ctx hst1 hst2:
-  hsstate_simu_spec dm f hst1 hst2 ->
-  hsstate_simu dm f hst1 hst2 ctx.
+Theorem hsstate_simu_spec_correct dm f outframe ctx hst1 hst2:
+  hsstate_simu_spec dm f outframe hst1 hst2 ->
+  hsstate_simu dm f outframe hst1 hst2 ctx.
 Proof.
   intros (SCORE & FSIMU) st1 st2 (SREF1 & DREF1 & FREF1) (SREF2 & DREF2 & FREF2).
   generalize SCORE. intro SIMU; eapply hsistate_simu_spec_correct in SIMU; eauto.
diff --git a/scheduling/RTLpathSE_theory.v b/scheduling/RTLpathSE_theory.v
index 4c492ecd..eec0bc51 100644
--- a/scheduling/RTLpathSE_theory.v
+++ b/scheduling/RTLpathSE_theory.v
@@ -1627,13 +1627,9 @@ Definition istate_simulive alive (srce: PTree.t node) (is1 is2: istate): Prop :=
      /\ eqlive_reg alive is1.(irs) is2.(irs)
      /\ is1.(imem) = is2.(imem).
 
-Definition istate_simu f (srce: PTree.t node) is1 is2: Prop :=
+Definition istate_simu f (srce: PTree.t node) outframe is1 is2: Prop :=
   if is1.(icontinue) then
-     (* TODO: il faudra raffiner le (fun _ => True) si on veut autoriser l'oracle à
-        ajouter du "code mort" sur des registres non utilisés (loop invariant code motion à la David)
-        Typiquement, pour connaître la frame des registres vivants, il faudra faire une propagation en arrière
-        sur la dernière instruction du superblock. *)
-     istate_simulive (fun _ => True) srce is1 is2
+     istate_simulive (fun r => Regset.In r outframe) srce is1 is2
   else
      exists path, f.(fn_path)!(is1.(ipc)) = Some path 
      /\ istate_simulive (fun r => Regset.In r path.(input_regs)) srce is1 is2
@@ -1651,10 +1647,10 @@ Record simu_proof_context {f1: RTLpath.function} := {
 Arguments simu_proof_context: clear implicits.
 
 (* NOTE: a pure semantic definition on [sistate], for a total freedom in refinements *)
-Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
+Definition sistate_simu (dm: PTree.t node) (f: RTLpath.function) outframe (st1 st2: sistate) (ctx: simu_proof_context f): Prop :=
   forall is1, ssem_internal (the_ge1 ctx) (the_sp ctx) st1 (the_rs0 ctx) (the_m0 ctx) is1 ->
   exists is2, ssem_internal (the_ge2 ctx) (the_sp ctx) st2 (the_rs0 ctx) (the_m0 ctx) is2
-              /\ istate_simu f dm is1 is2.
+              /\ istate_simu f dm outframe is1 is2.
 
 Inductive svident_simu (f: RTLpath.function) (ctx: simu_proof_context f): (sval + ident) -> (sval + ident) -> Prop :=
   | Sleft_simu sv1 sv2:
@@ -1885,13 +1881,14 @@ Inductive sfval_simu (dm: PTree.t node) (f: RTLpath.function) (opc1 opc2: node)
       = (seval_sval (the_ge2 ctx) (the_sp ctx) sv2 (the_rs0 ctx) (the_m0 ctx)) ->
       sfval_simu dm f opc1 opc2 ctx (Sreturn (Some sv1)) (Sreturn (Some sv2)).
 
-Definition sstate_simu dm f (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
-       sistate_simu dm f s1.(internal) s2.(internal) ctx
-    /\ forall is1, 
+Definition sstate_simu dm f outframe (s1 s2: sstate) (ctx: simu_proof_context f): Prop :=
+       sistate_simu dm f outframe s1.(internal) s2.(internal) ctx
+    /\ forall is1,
            ssem_internal (the_ge1 ctx) (the_sp ctx) s1 (the_rs0 ctx) (the_m0 ctx) is1 -> 
            is1.(icontinue) = true ->
            sfval_simu dm f s1.(si_pc) s2.(si_pc) ctx s1.(final) s2.(final).
 
 Definition sexec_simu dm (f1 f2: RTLpath.function) pc1 pc2: Prop :=
     forall st1, sexec f1 pc1 = Some st1 -> 
-    exists st2, sexec f2 pc2 = Some st2 /\ forall ctx, sstate_simu dm f1 st1 st2 ctx.
+    exists path st2, (fn_path f1)!pc1 = Some path /\ sexec f2 pc2 = Some st2 
+     /\ forall ctx, sstate_simu dm f1 path.(pre_output_regs) st1 st2 ctx.
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 4ba197b0..72a4ee01 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -143,13 +143,25 @@ Obligation 2.
   erewrite symbols_preserved_RTL. eauto.
 Qed.
 
+Lemma s_find_function_fundef f sp svos rs0 m0 fd
+  (LIVE: liveness_ok_function f):
+  sfind_function pge ge sp svos rs0 m0 = Some fd ->
+  liveness_ok_fundef fd.
+Proof.
+  unfold sfind_function. destruct svos; simpl.
+  + destruct (seval_sval _ _ _ _); try congruence.
+    eapply find_funct_liveness_ok; eauto.
+  + destruct (Genv.find_symbol _ _); try congruence.
+    intros. eapply all_fundef_liveness_ok; eauto.
+Qed.
+Local Hint Resolve s_find_function_fundef: core.
+
 Lemma s_find_function_preserved f sp svos1 svos2 rs0 m0 fd
   (LIVE: liveness_ok_function f):
   (svident_simu f (mkctx sp rs0 m0 LIVE) svos1 svos2) ->
   sfind_function pge ge sp svos1 rs0 m0 = Some fd ->
   exists fd', sfind_function tpge tge sp svos2 rs0 m0 = Some fd'
-              /\ transf_fundef fd = OK fd'
-              /\ liveness_ok_fundef fd.
+              /\ transf_fundef fd = OK fd'.
 Proof.
   Local Hint Resolve symbols_preserved_RTL: core.
   unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
@@ -159,20 +171,16 @@ Proof.
     intros; exploit functions_preserved; eauto.
     intros (fd' & cunit & (X1 & X2 & X3)). eexists.
     repeat split; eauto.
-    eapply find_funct_liveness_ok; eauto.
-(*     intros. eapply all_fundef_liveness_ok; eauto. *)
   + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
     intros; exploit function_ptr_preserved; eauto.
-    intros (fd' & X). eexists. intuition eauto.
-(*     intros. eapply all_fundef_liveness_ok; eauto. *)
 Qed.
 
-Lemma sistate_simu f dupmap sp st st' rs m is 
+Lemma sistate_simu f dupmap outframe sp st st' rs m is 
   (LIVE: liveness_ok_function f):
   ssem_internal ge sp st rs m is ->
-  sistate_simu dupmap f st st' (mkctx sp rs m LIVE)->
+  sistate_simu dupmap f outframe st st' (mkctx sp rs m LIVE)->
   exists is',
-    ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap is is'.
+    ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe is is'.
 Proof.
   intros SEM X; eapply X; eauto.
 Qed.
@@ -198,13 +206,12 @@ Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s
   (LIVE: liveness_ok_function f):
   match_function dm f f' ->
   list_forall2 match_stackframes stk stk' ->
-  (* s_istate_simu f dupmap st st' -> *)
   sfval_simu dm f st.(si_pc) st'.(si_pc) (mkctx sp rs0 m0 LIVE) sv sv' ->
   ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s ->
   exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
 Proof.
   Local Hint Resolve transf_fundef_correct: core.
-  intros FUN STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
+  intros FUN STK SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
   - (* Snone *)
     exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
     intros (path & PATH).
@@ -212,7 +219,7 @@ Proof.
     eapply eqlive_reg_refl.
   - (* Scall *)
     exploit s_find_function_preserved; eauto.
-    intros (fd' & FIND & TRANSF & LIVE').
+    intros (fd' & FIND & TRANSF).
     erewrite <- function_sig_preserved; eauto.
     exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
     intros (path & PATH).
@@ -221,7 +228,7 @@ Proof.
     + simpl. repeat (econstructor; eauto).
   - (* Stailcall *)
     exploit s_find_function_preserved; eauto.
-    intros (fd' & FIND & TRANSF & LIVE').
+    intros (fd' & FIND & TRANSF).
     erewrite <- function_sig_preserved; eauto.
     eexists; split; econstructor; eauto.
     + erewrite <- preserv_fnstacksize; eauto.
@@ -253,18 +260,171 @@ Proof.
     + rewrite <- H. erewrite <- seval_preserved; eauto.
 Qed.
 
+Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
+  ipath_checker path f (fn_path f) alive pc = Some res
+  -> nth_default_succ (fn_code f) path pc = Some (snd res).
+Proof.
+  induction path; simpl.
+  + try_simplify_someHyps.
+  + intros alive pc res.
+    inversion_SOME i; intros INST.
+    inversion_SOME res0; intros ICHK IPCHK.
+    rewrite INST.
+    erewrite iinst_checker_default_succ; eauto.
+Qed.
+
+Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
+  (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
+          (irs is) (imem is) t s)
+  (SIEXEC : siexec_inst i st0 = Some s0)
+  (ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt),
+  (liveness_ok_function f) ->
+  list_forall2 match_stackframes stk stk' ->
+  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
+  exists s' : state,
+    ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\
+    eqlive_states s s'.
+Proof.
+  Local Hint Resolve eqlive_stacks_refl: core.
+  intros ? ? ? LIVE STK EQLIVE.
+  inversion SSEM2; subst; clear SSEM2.
+  eexists; split.
+  * econstructor.
+  * generalize ICHK.
+    unfold inst_checker. destruct i; simpl in *;
+    unfold exit_checker; try discriminate.
+    all:
+      try destruct (list_mem _ _); simpl;
+      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail).
+    4,5:
+      destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+    1,2,3,4: assert (NPC: n=(si_pc s0)).
+    all: try (inv SIEXEC; simpl; auto; fail).
+    1,2,3,4:
+      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence);
+      simpl; inversion_SOME p;
+      destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence;
+      intros NPATH _; econstructor; eauto;
+      try (instantiate (1:=p); rewrite <- NPC; auto; fail).
+    1,2,3,4:
+      eapply eqlive_reg_monotonic; eauto; simpl;
+      intros; apply Regset.subset_2 in SUB_PATH;
+      unfold Regset.Subset in SUB_PATH;
+      apply SUB_PATH in H; auto.
+    assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. }
+    inversion_SOME p.
+    2: { destruct (Regset.subset _ _) eqn:?; try congruence. }
+    destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+    2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. }
+    simpl.
+    destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence.
+    inversion_SOME p'.
+    destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence.
+    intros NPATH NPATH' _. econstructor; eauto.
+    instantiate (1:=p'). rewrite <- NPC; auto.
+    eapply eqlive_reg_monotonic; eauto; simpl.
+    intros. apply Regset.subset_2 in SUB_PATH.
+    unfold Regset.Subset in SUB_PATH.
+    apply SUB_PATH in H; auto.
+Qed.
+
+Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
+  (liveness_ok_function f) ->
+  (fn_path f) ! pc0 = Some path0 ->
+  (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *)  (* NB: should be useless *)
+  sexec f pc0 = Some st -> 
+  (* icontinue is = true -> *)
+  list_forall2 match_stackframes stk stk' ->
+  (* ssem_internal ge sp st rs0 m0 is -> *)
+  ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
+  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
+  exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
+Proof.
+  Local Hint Resolve eqlive_stacks_refl: core.
+  intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
+  (* start decomposing path_checker *)
+  generalize (LIVE pc0 path0 PATH0).
+  unfold path_checker.
+  inversion_SOME res; intros IPCHK.
+  inversion_SOME i; intros INST ICHK.
+  exploit ipath_checker_default_succ; eauto. intros DEFSUCC.
+  (* start decomposing SEXEC *)
+  generalize SEXEC; clear SEXEC.
+  unfold sexec; rewrite PATH0.
+  inversion_SOME st0; intros SEXEC_PATH.
+  exploit siexec_path_default_succ; eauto.
+  simpl. rewrite DEFSUCC.
+  clear DEFSUCC. destruct res as [alive pc1]. simpl in *.
+  try_simplify_someHyps.
+  destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros.
+  (* Snone *)
+  eapply siexec_snone_por_correct; eauto.
+  destruct i; try_simplify_someHyps; try congruence;
+  inversion SSEM2; subst; clear SSEM2; simpl in *.
+ + (* Scall *)
+    eexists; split.
+    * econstructor; eauto.
+    * econstructor; eauto.
+      econstructor; eauto.
+      (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (list_mem _ _); try congruence.
+      destruct (reg_sum_mem _ _); try congruence.
+      intros EXIT.
+      exploit exit_checker_eqlive_ext1; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
+      econstructor; eauto.
+ + (* Stailcall *)
+    eexists; split.
+    * econstructor; eauto.
+    * econstructor; eauto.
+ + (* Sbuiltin *)
+    eexists; split.
+    * econstructor; eauto.
+    * (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (list_mem _ _); try congruence.
+      intros EXIT.
+      exploit exit_checker_eqlive_builtin_res; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
+      econstructor; eauto.
+ + (* Sjumptable *)
+    eexists; split.
+    * econstructor; eauto.
+    * (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (Regset.mem _ _); try congruence.
+      destruct (exit_list_checker _ _ _) eqn:EQL; try congruence.
+      exploit exit_list_checker_eqlive; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
+      econstructor; eauto.
+ + (* Sreturn *)
+    eexists; split.
+    * econstructor; eauto.
+    * econstructor; eauto.
+Qed.
+
 (* The main theorem on simulation of symbolic states ! *)
-Theorem ssem_sstate_simu dm f f' stk stk' sp st st' rs m t s:
+Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
+  (fn_path f) ! pc0 = Some path0 ->
+  (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *)
+  sexec f pc0 = Some st -> 
   match_function dm f f' ->
   liveness_ok_function f ->
   list_forall2 match_stackframes stk stk' ->
   ssem pge ge sp st stk f rs m t s ->
-  (forall ctx: simu_proof_context f, sstate_simu dm f st st' ctx) ->
+  (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
   exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
 Proof.
-  intros MFUNC LIVE STACKS SEM SIMU.
+  intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
   destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
-  destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
+  destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
   - (* sem_early *)
     exploit sistate_simu; eauto.
     unfold istate_simu; rewrite CONT.
@@ -276,15 +436,17 @@ Proof.
   - (* sem_normal *)
     exploit sistate_simu; eauto.
     unfold istate_simu; rewrite CONT.
-    intros (is' & SEM' & (CONT' & RS' & M')(*  & DMEQ *)).
-    rewrite <- eqlive_reg_triv in RS'.
+    intros (is' & SEM' & (CONT' & RS' & M')).
+    exploit pre_output_regs_correct; eauto.
+    clear SEM2; intros (s0 & SEM2 & EQLIVE).
     exploit ssem_final_simu; eauto.
-    clear SEM2; intros (s0 & SEM2 & MATCH0).
+    clear SEM2; intros (s1 & SEM2 & MATCH0).
     exploit ssem_final_equiv; eauto.
-    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
-    exists s1; split.
+    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2).
+    exists s2; split.
     + eapply ssem_normal; eauto.
-    + eapply match_states_equiv; eauto.
+    + eapply eqlive_match_states; eauto.
+      eapply match_states_equiv; eauto.
 Qed.
 
 Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s:
@@ -301,12 +463,13 @@ Proof.
   intros (path' & PATH').
   exists path'.
   exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto.
-  intros (st & SYMB & SEM); clear STEP.
+  intros (st & SYMB & SEM).
   exploit dupmap_correct; eauto.
-  clear SYMB; intros (st' & SYMB & SIMU).
+  intros (path0 & st' & PATH0 & SYMB' & SIMU).
+  rewrite PATH0 in PATH; inversion PATH; subst.
   exploit ssem_sstate_simu; eauto.
   intros (s0 & SEM0 & MATCH). 
-  exploit sexec_exact; eauto.
+  exploit (sexec_exact f'); eauto.
   intros (s' & STEP' & EQ).
   exists s'; intuition.
   eapply match_states_equiv; eauto.
diff --git a/scheduling/RTLpathWFcheck.v b/scheduling/RTLpathWFcheck.v
index f5198e68..0ddc3142 100644
--- a/scheduling/RTLpathWFcheck.v
+++ b/scheduling/RTLpathWFcheck.v
@@ -88,24 +88,11 @@ Fixpoint exit_list_checker (pm: path_map) (l: list node): bool :=
    | pc::l' => exit_checker pm pc tt &&& exit_list_checker pm l'
    end.
 
-Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.
-Proof.
-  destruct o; simpl; intuition. 
-  - eauto.
-  - firstorder. try_simplify_someHyps.
-Qed.
-
-Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
-Proof.
-   intros; rewrite lazy_and_Some_true; firstorder.
-   destruct x; auto.
-Qed.
-
 Lemma exit_list_checker_correct pm l pc:
   exit_list_checker pm l = true -> List.In pc l -> exit_checker pm pc tt = Some tt.
 Proof.
   intros EXIT PC; induction l; intuition.
-  simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT.
+  simpl in * |-. rewrite RTLpathLivegen.lazy_and_Some_tt_true in EXIT.
   firstorder (subst; eauto).
 Qed.
 
@@ -167,7 +154,7 @@ Lemma list_path_checker_correct f pm l:
   list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.
 Proof.
   intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
-  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
+  simpl in * |- *. rewrite RTLpathLivegen.lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
 Qed.
 
 Definition function_checker (f: RTL.function) (pm: path_map): bool := 
@@ -178,7 +165,7 @@ Lemma function_checker_correct f pm pc path:
   pm!pc = Some path -> 
   path_checker f pm pc path = Some tt.
 Proof.
-  unfold function_checker; rewrite lazy_and_Some_true.
+  unfold function_checker; rewrite RTLpathLivegen.lazy_and_Some_true.
   intros (ENTRY & PATH) PC.
   exploit list_path_checker_correct; eauto.
   - eapply PTree.elements_correct; eauto.
diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml
index 8d4f4f0b..ddb3c21a 100644
--- a/tools/compiler_expand.ml
+++ b/tools/compiler_expand.ml
@@ -32,6 +32,7 @@ PARTIAL, Always, NoRequire, (Some "Unrolling the body of innermost loops"), "Unr
 TOTAL, Always, NoRequire, (Some "Renumbering pre constprop"), "Renumber";
 TOTAL, (Option "optim_constprop"), Require, (Some "Constant propagation"), "Constprop";
 TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber";
+PARTIAL, (Option "optim_CSE"), Require, (Some "CSE"), "CSE";
 TOTAL, (Option "optim_CSE2"), Require, (Some "CSE2"), "CSE2";
 PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3";
 TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves";