Complete `tunnel_step_correct` proof up to Ijumptable

Excluding Icond

1 files changed, 227 insertions, 9 deletions

diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index c54667a4..53f8bbf7 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -344,6 +344,118 @@ Proof.
   apply H. apply IHargs.
 Qed.
 
+Lemma instruction_type_preserved: 
+  forall (f tf:function) (pc:node) (i ti:instruction)
+  (TF: tunnel_function f = OK tf)
+  (FATPC: (fn_code f) ! pc = Some i)
+  (NOTINOP: forall s, i <> Inop s)
+  (NOTICOND: forall cond args ifso ifnot info, i <> Icond cond args ifso ifnot info)
+  (TI: ti = tunnel_instr (branch_target f) i),
+  (fn_code tf) ! (branch_target f pc) = Some ti.
+Proof.
+  intros.
+  assert ((fn_code tf) ! pc = Some (tunnel_instr (branch_target f) i)) as TFATPC.
+  rewrite (tunnel_function_unfold f tf pc); eauto.
+  rewrite FATPC; eauto.
+  exploit branch_target_bounds; eauto.
+  intro TB. inversion TB as [BT|s|cond args ifso ifnot info]; try (rewrite FATPC in H; congruence).
+Qed.
+
+(* rq: utilisée pour `tunnel_step_correct` mais je ne comprends pas tout *)
+(**) Lemma find_function_translated: 
+  forall ros rs trs fd,
+  regs_lessdef rs trs ->
+  find_function ge ros rs = Some fd ->
+  exists tfd, tunnel_fundef fd = OK tfd /\ find_function tge ros trs = Some tfd.
+Proof.
+  intros. destruct ros; simpl in *.
+  - (* reg *)
+    assert (E: trs # r = rs # r).
+    { exploit Genv.find_funct_inv. apply H0. intros (b & EQ).
+      generalize (H r) . rewrite EQ. intro LD. inv LD. auto. }
+    rewrite E. exploit functions_translated; eauto.
+  - (* ident *)
+    rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0. 
+    exploit function_ptr_translated; eauto.
+    intros (tf & X1 & X2). exists tf; intuition.
+Qed.
+
+Lemma list_forall2_lessdef_rs:
+  forall rs trs args,
+  regs_lessdef rs trs ->
+  list_forall2 Val.lessdef rs ## args trs ## args.
+Proof.
+  intros rs trs args LD.
+  exploit (reglist_lessdef rs trs args). apply LD. 
+  induction args; simpl; intros H; try constructor; inv H.
+  apply H3. apply IHargs. apply H5.
+Qed.
+
+Lemma fn_stacksize_preserved:
+  forall f tf
+  (TF: tunnel_function f = OK tf),
+  fn_stacksize f = fn_stacksize tf.
+Proof.
+  intros f tf. unfold tunnel_function.
+  destruct (check_included _ _); try congruence.
+  intro H. monadInv H. simpl. reflexivity.
+Qed.
+
+Lemma regs_setres_lessdef:
+  forall res vres tvres rs trs,
+  regs_lessdef rs trs -> Val.lessdef vres tvres ->
+  regs_lessdef (regmap_setres res vres rs) (regmap_setres res tvres trs).
+Proof.
+  induction res; intros; simpl; try auto using set_reg_lessdef.
+Qed.
+
+Lemma regmap_optget_lessdef:
+  forall or rs trs,
+  regs_lessdef rs trs -> Val.lessdef (regmap_optget or Vundef rs) (regmap_optget or Vundef trs).
+Proof.
+  intros or rs trs RS.
+  induction or; simpl; auto using set_reg_lessdef.
+Qed.
+
+Lemma tunnel_fundef_Internal:
+  forall (f:function) (tf:fundef)
+  (TF: tunnel_fundef (Internal f) = OK tf),
+  exists (tf':function), tf = (Internal tf') /\ tunnel_function f = OK tf'.
+Proof.
+  intros f tf.
+  unfold tunnel_fundef. simpl. intro H. monadInv H. exists x.
+  split. reflexivity. apply EQ.
+Qed.
+
+Lemma fn_entrypoint_preserved:
+  forall f tf
+  (TF: tunnel_function f = OK tf),
+  fn_entrypoint tf = branch_target f (fn_entrypoint f).
+Proof.
+  intros f tf.
+  unfold tunnel_function. destruct (check_included _ _); try congruence.
+  intro TF. monadInv TF. simpl. reflexivity.
+Qed.
+
+Lemma init_regs_lessdef:
+  forall f tf args targs
+  (ARGS: list_forall2 Val.lessdef args targs)
+  (TF: tunnel_function f = OK tf),
+  regs_lessdef (init_regs args (fn_params f)) (init_regs targs (fn_params tf)).
+Proof.
+  assert (regs_lessdef (Regmap.init Vundef) (Regmap.init Vundef)) as Hundef.
+  { unfold Regmap.init. unfold regs_lessdef. intro. unfold Regmap.get. rewrite PTree.gempty. apply Val.lessdef_undef. }
+
+  intros f tf args targs ARGS.
+
+  unfold tunnel_function. destruct (check_included _ _) eqn:EQinc; try congruence.
+  intro TF. monadInv TF. simpl. destruct (fn_params f) eqn:EQP; simpl.
+  - apply Hundef.
+  - induction ARGS.
+    + apply Hundef.
+    + apply set_reg_lessdef; try assumption. 
+Admitted.
+
 (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
 Lemma tunnel_step_correct:
   forall st1 t st2, step ge st1 t st2 ->
@@ -368,18 +480,124 @@ Proof.
     intros (tv & EVAL & LD).
     left; eexists; split.
     + eapply exec_Iop with (v:=tv).
-      assert ((fn_code tf) ! pc = Some (Iop op args res (branch_target f pc'))).
-      rewrite (tunnel_function_unfold f tf pc); eauto.
-      rewrite H. simpl. reflexivity.
-      (* TODO: refaire ça joliment *)
-      assert (target_bounds (branch_target f) (bound (branch_target f)) pc (fn_code f)! pc).
-      apply (branch_target_bounds) with tf. apply TF.
-      inv H2. rewrite TB. apply H1. rewrite H in H4. congruence.
-      rewrite H in H4. congruence.
+      apply instruction_type_preserved with (Iop op args res pc'); (simpl; auto)||congruence.
       rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved.
     + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS.
   - (* Iload *)
-
+    exploit eval_addressing_lessdef; try eassumption.
+    apply reglist_lessdef. apply RS.
+    intros (ta & EVAL & LD).
+    exploit Mem.loadv_extends; try eassumption.
+    intros (tv & LOAD & LD').
+    left. eexists. split.
+    + eapply exec_Iload.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
+      * apply LOAD.
+    + apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS.
+  - (* Iload NOTRAP1 *)
+    exploit eval_addressing_lessdef_none; try eassumption.
+    apply reglist_lessdef; apply RS.
+    left. eexists. split.
+    + eapply exec_Iload_notrap1.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved.
+    + apply match_states_intro; try assumption. apply set_reg_lessdef. unfold default_notrap_load_value. apply Val.lessdef_undef. apply RS.
+  - (* Iload NOTRAP2 *)
+    exploit eval_addressing_lessdef; try eassumption.
+    apply reglist_lessdef; apply RS.
+    intros (ta & EVAL & LD).
+    (* TODO: on peut sans doute factoriser ça *)
+    destruct (Mem.loadv chunk tm ta) eqn:Htload.
+    + left; eexists; split.
+      eapply exec_Iload.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
+      * apply Htload.
+      * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
+    + left; eexists; split.
+      eapply exec_Iload_notrap2.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
+      * apply Htload.
+      * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
+  - (* Lstore *)
+    exploit eval_addressing_lessdef; try eassumption.
+    apply reglist_lessdef; apply RS.
+    intros (ta & EVAL & LD).
+    exploit Mem.storev_extends; try eassumption. apply RS.
+    intros (tm' & STORE & MEM').
+    left. eexists. split.
+    + eapply exec_Istore.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
+      * rewrite STORE. reflexivity.
+    + apply match_states_intro; try eassumption.
+  - (* Icall *)
+    left.
+    exploit find_function_translated; try eassumption.
+    intros (tfd & TFD & FIND).
+    eexists. split.
+    + eapply exec_Icall.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * apply FIND.
+      * apply sig_preserved. apply TFD.
+    + apply match_states_call; try assumption.
+      * apply list_forall2_cons; try assumption. apply match_stackframes_intro; try assumption.
+      * apply list_forall2_lessdef_rs. apply RS.
+  - (* Itailcall *)
+    exploit find_function_translated; try eassumption.
+    intros (tfd & TFD & FIND).
+    exploit Mem.free_parallel_extends; try eassumption.
+    intros (tm' & FREE & MEM').
+    left. eexists. split.
+    + eapply exec_Itailcall.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * apply FIND.
+      * apply sig_preserved. apply TFD.
+      * erewrite <- fn_stacksize_preserved; try eassumption.
+    + apply match_states_call; try assumption.
+      apply list_forall2_lessdef_rs. apply RS.
+  - (* Ibuiltin *)
+    exploit eval_builtin_args_lessdef; try eassumption. apply RS.
+    intros (vl2 & EVAL & LD).
+    exploit external_call_mem_extends; try eassumption.
+    intros (tvres & tm' & EXT & LDRES & MEM' & UNCHGD).
+    left. eexists. split.
+    + eapply exec_Ibuiltin.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * eapply eval_builtin_args_preserved. eapply symbols_preserved. eapply EVAL.
+      * eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXT.
+    + apply match_states_intro; try assumption. apply regs_setres_lessdef; try assumption.
+  - (* Icond *)
+    admit.
+  - (* Ijumptable *)
+    left. eexists. split.
+    + eapply exec_Ijumptable.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * generalize (RS arg). rewrite H0. intro. inv H2. reflexivity.
+      * rewrite list_nth_z_map. rewrite H1. simpl. reflexivity.
+    + apply match_states_intro; try eassumption.
+  - (* Ireturn *)
+    exploit Mem.free_parallel_extends; try eassumption.
+    intros (tm' & FREE & MEM').
+    left. eexists. split.
+    + eapply exec_Ireturn.
+      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
+      * erewrite <- fn_stacksize_preserved. eapply FREE. eapply TF.
+    + apply match_states_return; try eassumption.
+      apply regmap_optget_lessdef. apply RS.
+  - (* internal function *)
+    exploit tunnel_fundef_Internal; try eassumption.
+    intros (tf' & EQ & TF'). subst.
+    exploit Mem.alloc_extends; try eassumption. reflexivity. reflexivity.
+    intros (m2' & ALLOC & EXT).
+    left. eexists. split.
+    + eapply exec_function_internal.
+      rewrite <- (fn_stacksize_preserved f tf'). eapply ALLOC. eapply TF'.
+    + rewrite (fn_entrypoint_preserved f tf'); try eassumption. apply match_states_intro; try eassumption.
+      apply init_regs_lessdef.
+    
 
 Qed.