Complete RTLTunnelingproof

There is still some refactoring to do, though

1 files changed, 66 insertions, 16 deletions

diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index 53f8bbf7..7f6696ad 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -344,7 +344,7 @@ Proof.
   apply H. apply IHargs.
 Qed.
 
-Lemma instruction_type_preserved: 
+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)
@@ -362,7 +362,7 @@ Proof.
 Qed.
 
 (* rq: utilisée pour `tunnel_step_correct` mais je ne comprends pas tout *)
-(**) Lemma find_function_translated: 
+(**) Lemma find_function_translated:
   forall ros rs trs fd,
   regs_lessdef rs trs ->
   find_function ge ros rs = Some fd ->
@@ -375,7 +375,7 @@ Proof.
       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. 
+    rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0.
     exploit function_ptr_translated; eauto.
     intros (tf & X1 & X2). exists tf; intuition.
 Qed.
@@ -386,7 +386,7 @@ Lemma list_forall2_lessdef_rs:
   list_forall2 Val.lessdef rs ## args trs ## args.
 Proof.
   intros rs trs args LD.
-  exploit (reglist_lessdef rs trs args). apply 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.
@@ -418,15 +418,25 @@ Proof.
 Qed.
 
 Lemma tunnel_fundef_Internal:
-  forall (f:function) (tf:fundef)
+  forall (f: function) (tf: fundef)
   (TF: tunnel_fundef (Internal f) = OK tf),
-  exists (tf':function), tf = (Internal tf') /\ tunnel_function 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 tunnel_fundef_External:
+  forall (ef: external_function) (tf: fundef)
+  (TF: tunnel_fundef (External ef) = OK tf),
+  tf = (External ef).
+Proof.
+  intros f tf.
+  unfold tunnel_fundef. simpl. intro H. monadInv H. reflexivity.
+Qed.
+
+
 Lemma fn_entrypoint_preserved:
   forall f tf
   (TF: tunnel_function f = OK tf),
@@ -449,12 +459,26 @@ Proof.
   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.
+  intro TF. monadInv TF. simpl. 
+  (* 
+  induction ARGS.
+  - induction (fn_params f) eqn:EQP; apply Hundef.
+  - induction (fn_params f) eqn:EQP.
+    * simpl. apply Hundef.
+    * simpl. apply set_reg_lessdef. apply H. 
+    *)
+    
+  generalize (fn_params f) as l. induction ARGS; induction l; try (simpl; apply Hundef).
+    simpl. apply set_reg_lessdef; try assumption. apply IHARGS.
+Qed.
+
+Lemma lessdef_forall2_list:
+  forall args ta,
+  list_forall2 Val.lessdef args ta -> Val.lessdef_list args ta.
+Proof.
+  intros args ta H. induction H. apply Val.lessdef_list_nil. apply Val.lessdef_list_cons. apply H. apply IHlist_forall2.
+Qed.
+
 
 (* `Lemma tunnel_step_correct` correspond au diagramme "option simulation" *)
 Lemma tunnel_step_correct:
@@ -570,7 +594,22 @@ Proof.
       * eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXT.
     + apply match_states_intro; try assumption. apply regs_setres_lessdef; try assumption.
   - (* Icond *)
-    admit.
+    simpl. exploit branch_target_bounds. apply TF. rewrite H. intro. inv H1.
+    + (* TB_default *)
+      rewrite TB.
+      destruct (fn_code tf)!pc as [[]|] eqn:EQ;
+      assert (tunnel_function f = OK tf) as TF'; auto;
+      unfold tunnel_function in TF; destruct (check_included _ _) in TF; monadInv TF;
+      simpl in EQ; rewrite PTree.gmap1 in EQ; rewrite H in EQ; simpl in EQ; destruct (peq _ _) eqn: EQpeq in EQ; try congruence.
+      * left. eexists. split. 
+        -- eapply exec_Inop. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity.
+        -- destruct b. apply match_states_intro; eauto. rewrite e. apply match_states_intro; eauto.
+      * left. eexists. split.
+        -- eapply exec_Icond; auto. simpl. rewrite PTree.gmap1. rewrite H. simpl. rewrite EQpeq. reflexivity. eapply eval_condition_lessdef; try eassumption. apply reglist_lessdef. apply RS.
+        -- destruct b; apply match_states_intro; auto.
+    + (* TB_cond *) right; repeat split; destruct b; try assumption.
+      * rewrite EQSO. apply match_states_intro; try assumption.
+      * rewrite EQNOT. apply match_states_intro; try assumption.
   - (* Ijumptable *)
     left. eexists. split.
     + eapply exec_Ijumptable.
@@ -596,9 +635,20 @@ Proof.
     + 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.
-    
-
+      apply init_regs_lessdef. apply ARGS. apply TF'.
+  - (* external function *)
+    exploit external_call_mem_extends. eapply H. eapply MEM.  eapply lessdef_forall2_list. eapply ARGS.
+    intros (tvres & tm' & EXTCALL & LD & EXT & MEMUNCHGD).
+    left. eexists. split.
+    + erewrite (tunnel_fundef_External ef tf); try eassumption.
+      eapply exec_function_external. eapply external_call_symbols_preserved. eapply senv_preserved. eapply EXTCALL.
+    + eapply match_states_return; try assumption.
+  - (* return *)
+    inv STK. inv H1.
+    left. eexists. split.
+    + eapply exec_return.
+    + eapply match_states_intro; try assumption.
+      apply set_reg_lessdef; try assumption.
 Qed.