From 33958cecc396be3d7ba8bf369b2039c633d39849 Mon Sep 17 00:00:00 2001 From: Pierre Goutagny Date: Fri, 11 Jun 2021 13:30:20 +0200 Subject: Complete RTLTunnelingproof There is still some refactoring to do, though --- backend/RTLTunnelingproof.v | 82 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 66 insertions(+), 16 deletions(-) (limited to 'backend') 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. -- cgit