BTL Scheduler oracle and some drafts

1 files changed, 38 insertions, 4 deletions

diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index 8994579d..8081b3a6 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -30,21 +30,55 @@ Qed.
 
 Local Hint Resolve tr_inputs_lessdef init_regs_lessdef_preserv find_function_lessdef regs_lessdef_regs
   lessdef_state_refl: core.
+Local Hint Unfold regs_lessdef: core.
 
-Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 ib rs1' m1' of
+Lemma fsem2cfgsem_ibistep_simu ge sp rs1 m1 rs1' m1' of
+  rs2 m2 ib
   (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of)
-  rs2 m2
   (REGS: forall r, Val.lessdef rs1#r rs2#r)
   (MEMS: Mem.extends m1 m2)
   : exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of) 
      /\ (forall r, Val.lessdef rs1'#r rs2'#r)
      /\ (Mem.extends m1' m2').
 Proof.
-  induction ISTEP; simpl; try_simplify_someHyps.
+  induction ISTEP; simpl; try_simplify_someHyps; intros.
+  - (* Bop *)
+    exploit (@eval_operation_lessdef _ _ ge sp op (rs ## args)); eauto.
+    intros (v1 & EVAL' & LESSDEF).
+    do 2 eexists; rewrite EVAL'. repeat (split; eauto).
+    eapply set_reg_lessdef; eauto.
+  - (* Bload *)
+    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
+    intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto.
+    intros (v3 & LOAD' & LESSDEF').
+    do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto).
+    eapply set_reg_lessdef; eauto.
+  - (* Bstore *)
+    exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto.
+    intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto.
+    intros (v3 & STORE' & LESSDEF').
+    do 2 eexists; rewrite EVAL', STORE'. repeat (split; eauto).
+  - (* Bseq stop *)
+    exploit IHISTEP; eauto. intros (rs2' & m2' & IBIS & REGS' & MEMS').
+    destruct (iblock_istep_run _ _ _ _ _); try congruence.
+    destruct o, _fin; simpl in *; try congruence. eauto.
+  - (* Bseq continue *)
+    
+    (* TODO gourdinl induction pb?
+    exploit IHISTEP1; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1).
+    rewrite IBIS1; simpl. rewrite iblock_istep_run_equiv in ISTEP2.
+    exploit IHISTEP2; eauto. intros (rs4 & m4 & IBIS2 & REGS2 & MEMS2).
+    destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.
+    intros; apply IHISTEP1 in MEMS; auto.
+    exploit IHISTEP2; eauto. intros (rs3 & m3 & IBIS1 & REGS1 & MEMS1).
+    
+
+    destruct (iblock_istep_run _ _ _ _ _) eqn:EQb1.
+    2: { rewrite iblock_istep_run_equiv in ISTEP1. destruct b1; simpl in *; try congruence.
+       destruct o, _fin; simpl in *; try congruence; try_simplify_someHyps.*)
 Admitted.
 
 Local Hint Constructors lessdef_stackframe lessdef_state final_step list_forall2 step: core.
-Local Hint Unfold regs_lessdef: core.
 
 Lemma fsem2cfgsem_finalstep_simu ge stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
   (FSTEP: final_step tr_inputs ge stk1 f sp rs1 m1 fin t s1)