advance for tr_input proof

1 files changed, 171 insertions, 24 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 8d613ef8..3882639c 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -276,23 +276,50 @@ Let ge := Genv.globalenv prog.
 Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f.
 
 Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.
-(*
-Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
-  forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
-  :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2).
-REGS' : forall v : val,
-        eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v
-forall v : val,
-eqlive_reg (ext (input_regs ibf))
-  (tid f tbl or rs1) # res <- v
-  (tr_inputs f tbl or rs2) # res <- v
- 
 
+Lemma tr_inputs_eqlive_None f pc ibf rs1 rs2:
+  (fn_code f) ! pc = Some ibf ->
+  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
+  eqlive_reg (ext (input_regs ibf)) (tid f (pc :: nil) None rs1)
+    (tr_inputs f (pc :: nil) None rs2).
+Proof.
+  intros PC REGS.
+  unfold eqlive_reg. intros r INR.
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC.
+  exploit Regset.union_3. eapply INR.
+  intros INRU. eapply Regset.mem_1 in INRU.
+  erewrite INRU; eauto.
+Qed.
+
+Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val,
+  eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v ->
+  res <> r -> Regset.In r alive ->
+  rs1 # r = rs2 # r.
+Proof.
+  intros v REGS NRES INR. unfold eqlive_reg in REGS.
+  specialize REGS with r. apply REGS in INR.
+  rewrite !Regmap.gso in INR; auto.
+Qed.
+
+Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res:
+  (fn_code f) ! pc = Some ibf ->
+  forall v : val,
+    eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v ->
+  eqlive_reg (ext (input_regs ibf))
+    (tid f (pc :: nil) (Some res) rs1) # res <- v
+    (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v.
 Proof.
-  unfold tid; rewrite tr_inputs_get.
-  autodestruct.
+  intros PC v REGS. apply eqlive_reg_update.
+  unfold eqlive_reg. intros r (NRES & INR).
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC. assert (NRES': res <> r) by auto.
+  clear NRES. exploit Regset.union_3. eapply INR.
+  intros INRU. exploit Regset.remove_2; eauto.
+  intros INRU_RES. eapply Regset.mem_1 in INRU_RES.
+  erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto.
 Qed.
- *)
+
 Lemma find_funct_liveness_ok v fd:
   Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd.
 Proof.
@@ -321,7 +348,34 @@ Proof.
   intros H; erewrite (EQLIVE r); eauto.
 Qed.
 
-Lemma exit_checker_eqlive_ext1 (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2:
+Lemma exit_checker_eqlive (btl: code) (alive: Regset.t) (pc: node) rs1 rs2:
+  exit_checker btl alive pc = Some tt ->
+  eqlive_reg (ext alive) rs1 rs2 -> 
+  exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2.
+Proof.
+  unfold exit_checker.
+  inversion_SOME next.
+  inversion_ASSERT. try_simplify_someHyps.
+  repeat (econstructor; eauto).
+  intros; eapply eqlive_reg_monotonic; eauto.
+  intros; exploit Regset.subset_2; eauto.
+Qed.
+
+Lemma exit_list_checker_eqlive (btl: code) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n,
+  exit_list_checker btl alive tbl = true ->  
+  eqlive_reg (ext alive) rs1 rs2 -> 
+  list_nth_z tbl n = Some pc ->
+  exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2.
+Proof.
+  induction tbl; simpl.
+  - intros; try congruence.
+  - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn.
+    * try_simplify_someHyps; intuition.
+      exploit exit_checker_eqlive; eauto.
+    * intuition. eapply IHtbl; eauto.
+Qed.
+
+Lemma exit_checker_eqlive_update (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2:
   exit_checker btl (Regset.add r alive) pc = Some tt ->  
   eqlive_reg (ext alive) rs1 rs2 ->
   exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)).
@@ -336,6 +390,56 @@ Proof.
   rewrite regset_add_spec. intuition subst.
 Qed.
 
+Lemma exit_checker_eqlive_builtin_res (btl: code) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg):
+  exit_checker btl (reg_builtin_res res alive) pc = Some tt ->
+  eqlive_reg (ext alive) rs1 rs2 ->
+  exists ibf, btl!pc = Some ibf /\ (forall vres, eqlive_reg (ext ibf.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)).
+Proof.
+  destruct res; simpl.
+  - intros; exploit exit_checker_eqlive_update; eauto.
+  - intros; exploit exit_checker_eqlive; eauto.
+    intros (ibf & PC & REGS).
+    eexists; intuition eauto.
+  - intros; exploit exit_checker_eqlive; eauto.
+    intros (ibf & PC & REGS).
+    eexists; intuition eauto.
+Qed.
+
+Local Hint Resolve in_or_app: local.
+Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs:
+  eqlive_reg alive rs1 rs2 ->
+  Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs ->
+  (forall r, List.In r (params_of_builtin_args args) -> alive r) ->
+  Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs.
+Proof.
+  unfold Events.eval_builtin_args.
+  intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl.
+  { econstructor; eauto. }
+  intro X. 
+  assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2).
+  { eapply eqlive_reg_monotonic; eauto with local. }
+  lapply IHEVALL; eauto with local.
+  clear X IHEVALL; intro X. econstructor; eauto.
+  generalize X1; clear EVALL X1 X.
+  induction EVAL1; simpl; try (econstructor; eauto; fail).
+  - intros X1; erewrite X1; [ econstructor; eauto | eauto ].
+  - intros; econstructor.
+    + eapply IHEVAL1_1; eauto.
+      eapply eqlive_reg_monotonic; eauto.
+      simpl; intros; eauto with local.
+    + eapply IHEVAL1_2; eauto.
+      eapply eqlive_reg_monotonic; eauto.
+      simpl; intros; eauto with local.
+  - intros; econstructor.
+    + eapply IHEVAL1_1; eauto.
+      eapply eqlive_reg_monotonic; eauto.
+      simpl; intros; eauto with local.
+    + eapply IHEVAL1_2; eauto.
+      eapply eqlive_reg_monotonic; eauto.
+      simpl; intros; eauto with local.
+Qed.
+
+Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core.
 Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2
   (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s)
   (LIVE: liveness_ok_function f)
@@ -348,17 +452,17 @@ Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2
 Proof.
   destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros.
   - (* Bgoto *)
-    econstructor. econstructor.
-    econstructor. econstructor.
-    eauto. eauto.
-    repeat econstructor; eauto.
-    all: admit.
+    eexists; split.
+    + econstructor; eauto.
+    + exploit exit_checker_eqlive; eauto.
+      intros (ibf & PC & REGS').
+      econstructor; eauto.
   - (* Breturn *)
     eexists; split. econstructor; eauto.
     destruct or; simpl in *;
     try erewrite (REGS r); eauto.
   - (* Bcall *)
-    exploit exit_checker_eqlive_ext1; eauto.
+    exploit exit_checker_eqlive_update; eauto.
     intros (ibf & PC & REGS').
     eexists; split.
     + econstructor; eauto.
@@ -366,8 +470,6 @@ Proof.
     + erewrite eqlive_reg_listmem; eauto.
       eapply eqlive_states_call; eauto.
       eapply find_function_liveness_ok; eauto.
-      repeat (econstructor; eauto).
-      admit.
   - (* Btailcall *)
     eexists; split.
     + econstructor; eauto.
@@ -376,7 +478,52 @@ Proof.
       eapply eqlive_states_call; eauto.
       eapply find_function_liveness_ok; eauto.
   - (* Bbuiltin *)
-    
+    exploit exit_checker_eqlive_builtin_res; eauto.
+    intros (ibf & PC & REGS').
+    eexists; split.
+    + econstructor; eauto.
+      eapply eqlive_eval_builtin_args; eauto.
+      intros; eapply list_mem_correct; eauto.
+    + repeat (econstructor; simpl; eauto).
+      unfold regmap_setres. destruct res; simpl in *; eauto.
+  - (* Bjumptable *)
+    exploit exit_list_checker_eqlive; eauto.
+    intros (ibf & PC & REGS').
+    eexists; split.
+    + econstructor; eauto.
+      erewrite <- REGS; eauto.
+    + repeat (econstructor; simpl; eauto).
+
+(*
+      generalize dependent ibf.
+      generalize dependent n.
+      generalize dependent alive.
+      generalize dependent tbl.
+      induction tbl; simpl; try congruence.
+      intros alive REGS. rewrite lazy_and_Some_tt_true.
+      intros (EXIT & EXIT_REM) INARG n ARG. autodestruct.
+      * try_simplify_someHyps; intros.
+
+  unfold eqlive_reg. intros r INR.
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC.
+  exploit Regset.union_3. eapply INR.
+  intros INRU. eapply Regset.mem_1 in INRU.
+  erewrite INRU; eauto.
+
+
+      * try_simplify_someHyps; intros.
+        exploit IHtbl. eapply REGS.
+        eauto. eauto. eauto. eauto.
+        exploit exit_checker_eqlive; eauto.
+    intros (ibf' & PC' & REGS'').
+  unfold eqlive_reg. intros r INR.
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC'.
+  exploit Regset.union_3. eapply INR.
+  intros INRU. eapply Regset.mem_1 in INRU.
+  erewrite INRU; eauto.
+   admit.*)
 Admitted.
 
 Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'