From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:10:34 +0100 Subject: Porting the BTL non-trap loads approach to RTL --- backend/RTLtyping.v | 83 ++++++++++++++++++++++++++--------------------------- 1 file changed, 41 insertions(+), 42 deletions(-) (limited to 'backend/RTLtyping.v') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index 6048f895..85d3c439 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -938,60 +938,59 @@ Proof. induction 1; intros; inv WT; try (generalize (wt_instrs _ _ WT_FN pc _ H); intros WTI). (* Inop *) - econstructor; eauto. + - econstructor; eauto. (* Iop *) - econstructor; eauto. eapply wt_exec_Iop; eauto. + - econstructor; eauto. eapply wt_exec_Iop; eauto. (* Iload *) - econstructor; eauto. eapply wt_exec_Iload; eauto. - (* Iload notrap1*) - econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. - (* Iload notrap2*) - econstructor; eauto. eapply wt_exec_Iload_notrap; eauto. + - econstructor; eauto. inv H0. + + eapply wt_exec_Iload; eauto. + + destruct (eval_addressing) eqn:EVAL in LOAD; + eapply wt_exec_Iload_notrap; eauto. (* Istore *) - econstructor; eauto. + - econstructor; eauto. (* Icall *) - assert (wt_fundef fd). - destruct ros; simpl in H0. - pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). - exact wt_p. exact H0. - caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. - pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. - exact wt_p. exact H0. - discriminate. - econstructor; eauto. - econstructor; eauto. inv WTI; auto. - inv WTI. rewrite <- H8. apply wt_regset_list. auto. + - assert (wt_fundef fd). + destruct ros; simpl in H0. + pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). + exact wt_p. exact H0. + caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. + pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. + exact wt_p. exact H0. + discriminate. + econstructor; eauto. + econstructor; eauto. inv WTI; auto. + inv WTI. rewrite <- H8. apply wt_regset_list. auto. (* Itailcall *) - assert (wt_fundef fd). - destruct ros; simpl in H0. - pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). - exact wt_p. exact H0. - caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. - pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. - exact wt_p. exact H0. - discriminate. - econstructor; eauto. - inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto. - inv WTI. rewrite <- H7. apply wt_regset_list. auto. + - assert (wt_fundef fd). + destruct ros; simpl in H0. + pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). + exact wt_p. exact H0. + caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. + pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. + exact wt_p. exact H0. + discriminate. + econstructor; eauto. + inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto. + inv WTI. rewrite <- H7. apply wt_regset_list. auto. (* Ibuiltin *) - econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. + - econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. (* Icond *) - econstructor; eauto. + - econstructor; eauto. (* Ijumptable *) - econstructor; eauto. + - econstructor; eauto. (* Ireturn *) - econstructor; eauto. - inv WTI; simpl. auto. rewrite <- H3. auto. + - econstructor; eauto. + inv WTI; simpl. auto. rewrite <- H3. auto. (* internal function *) - simpl in *. inv H5. - econstructor; eauto. - inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. + - simpl in *. inv H5. + econstructor; eauto. + inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. (* external function *) - econstructor; eauto. - eapply external_call_well_typed; eauto. + - econstructor; eauto. + eapply external_call_well_typed; eauto. (* return *) - inv H1. econstructor; eauto. - apply wt_regset_assign; auto. rewrite H10; auto. + - inv H1. econstructor; eauto. + apply wt_regset_assign; auto. rewrite H10; auto. Qed. Lemma wt_initial_state: -- cgit