diff options
Diffstat (limited to 'backend/Allocationproof.v')
| -rw-r--r-- | backend/Allocationproof.v | 164 |
1 files changed, 70 insertions, 94 deletions
diff --git a/backend/Allocationproof.v b/backend/Allocationproof.v index 15cbdcdc..114a9a1d 100644 --- a/backend/Allocationproof.v +++ b/backend/Allocationproof.v @@ -2082,25 +2082,73 @@ Proof. econstructor; eauto. eapply wt_exec_Iop; eauto. -(* load regular TRAP *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. - exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. +(* load regular *) +- inv H0. + + generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + exploit Mem.loadv_extends; eauto. intros [v' [P Q]]. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. + destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload. + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap2. rewrite <- F. + apply eval_addressing_preserved. exact symbols_preserved. assumption. + eauto. + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. + } + * generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). + intro WTRS'. + exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. + exploit transfer_use_def_satisf; eauto. intros [X Y]. + exploit eval_addressing_lessdef_none; eauto. intro Haddr. + exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. + econstructor; split. + eapply plus_left. econstructor; eauto. + eapply star_trans. eexact A1. + eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + + eapply star_right. eexact A2. constructor. + eauto. eauto. eauto. traceEq. + exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. + econstructor; eauto. (* load pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2155,7 +2203,7 @@ Proof. econstructor; eauto. (* load first word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2185,7 +2233,7 @@ Proof. econstructor; eauto. (* load second word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2226,82 +2274,10 @@ Proof. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. eapply reg_unconstrained_satisf; eauto. intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload; eauto. - -- (* load notrap1 *) - generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). - intro WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef_none; eauto. intro Haddr. - exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr. - apply eval_addressing_preserved. exact symbols_preserved. eauto. - - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - -(* load notrap1 dead *) -- exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload_notrap; eauto. + econstructor; eauto. inv H0. + + eapply wt_exec_Iload; eauto. + + eapply wt_exec_Iload_notrap; eauto. -(* load regular notrap2 *) -- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). - intro WTRS'. - exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. - exploit transfer_use_def_satisf; eauto. intros [X Y]. - exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. - destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload. - { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - } - { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto. intros [ls2 [A2 B2]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_trans. eexact A1. - eapply star_left. eapply exec_Lload_notrap2. rewrite <- F. - apply eval_addressing_preserved. exact symbols_preserved. assumption. - eauto. - eapply star_right. eexact A2. constructor. - eauto. eauto. eauto. traceEq. - exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]]. - econstructor; eauto. - } - -- (* load notrap2 dead *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. - econstructor; split. - eapply plus_left. econstructor; eauto. - eapply star_right. eexact X. econstructor; eauto. - eauto. traceEq. - exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. - eapply reg_unconstrained_satisf; eauto. - intros [enext [U V]]. - econstructor; eauto. - eapply wt_exec_Iload_notrap; eauto. - (* store *) - exploit exec_moves; eauto. intros [ls1 [X Y]]. exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD. |