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/Allnontrapproof.v | 38 ++-- backend/Allocationproof.v | 164 +++++++-------- backend/CSE2proof.v | 382 +++++++++++++++++------------------ backend/CSE3proof.v | 435 ++++++++++++++++++++-------------------- backend/CSEproof.v | 225 ++++++++++----------- backend/Constpropproof.v | 151 +++++++------- backend/Deadcodeproof.v | 85 ++++---- backend/Duplicateproof.v | 32 ++- backend/FirstNopproof.v | 39 ++-- backend/ForwardMovesproof.v | 160 +++++++-------- backend/Injectproof.v | 254 +++++++++++------------ backend/Inliningproof.v | 99 ++++----- backend/KillUselessMovesproof.v | 54 ++--- backend/ProfilingExploitproof.v | 35 ++-- backend/Profilingproof.v | 42 ++-- backend/RTL.v | 30 ++- backend/RTLTunnelingproof.v | 78 +++---- backend/RTLgenproof.v | 4 +- backend/RTLtyping.v | 83 ++++---- backend/Renumberproof.v | 133 ++++++------ backend/Tailcallproof.v | 73 +++---- backend/Unusedglobproof.v | 88 ++++---- backend/ValueAnalysis.v | 15 +- 23 files changed, 1322 insertions(+), 1377 deletions(-) (limited to 'backend') diff --git a/backend/Allnontrapproof.v b/backend/Allnontrapproof.v index 157c5de2..f3b10600 100644 --- a/backend/Allnontrapproof.v +++ b/backend/Allnontrapproof.v @@ -111,6 +111,8 @@ Inductive match_states: RTL.state -> RTL.state -> Prop := match_states (Returnstate stk v m) (Returnstate stk' v m). +(*Lemma load_notrap_simu_correct:*) + Lemma step_simulation: forall S1 t S2, RTL.step ge S1 t S2 -> forall S1', match_states S1 S1' -> @@ -126,23 +128,25 @@ Proof. rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. constructor; auto. (* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - constructor; auto. -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - constructor; auto. -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - constructor; auto. +- inv H0. + + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + constructor; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some v). + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. apply LOAD; auto. + constructor; auto. + * econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + constructor; auto. - (* store *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). 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. diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 252240c9..08891e1d 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -1314,105 +1314,62 @@ Proof. } (* load *) -- unfold transf_instr in *. - destruct find_load_in_fmap eqn:FIND_LOAD. - { - unfold find_load_in_fmap, fmap_sem', fmap_sem in *. - destruct (forward_map f) as [map |] eqn:MAP. - 2: discriminate. - change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. - destruct (map # pc) as [mpc | ] eqn:MPC. - 2: discriminate. - econstructor; split. +- unfold transf_instr in *. inv H0. + + destruct find_load_in_fmap eqn:FIND_LOAD. { - eapply exec_Iop with (v := v); eauto. - simpl. - rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. { - f_equal. - symmetry. - rewrite MAP in H0. - eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). - all: eassumption. + eapply exec_Iop with (v := v); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL. + { + f_equal. + symmetry. + rewrite MAP in EVAL. + eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. } - unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. - } - constructor; eauto. - unfold fmap_sem', fmap_sem in *. - rewrite MAP. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). - { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - unfold sem_rel_b', sem_rel_b. - apply load_sound with (a := a); auto. - } - { - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - rewrite (subst_args_ok' sp m); assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem', fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). - { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + unfold sem_rel_b', sem_rel_b. + apply load_sound with (a := a); auto. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - apply load_sound with (a := a); assumption. - } - -- (* load notrap1 *) - unfold transf_instr in *. - destruct find_load_in_fmap eqn:FIND_LOAD. - { - unfold find_load_in_fmap, fmap_sem', fmap_sem in *. - destruct (forward_map f) as [map |] eqn:MAP. - 2: discriminate. - change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. - destruct (map # pc) as [mpc | ] eqn:MPC. - 2: discriminate. + { econstructor; split. - { - eapply exec_Iop with (v := Vundef); eauto. - simpl. - rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. - { - f_equal. - rewrite MAP in H0. - eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). - all: eassumption. - } - unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. - } - constructor; eauto. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- EVAL. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite (subst_args_ok' sp m); assumption. + constructor; auto. + + simpl in *. unfold fmap_sem', fmap_sem in *. - rewrite MAP. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). { replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). @@ -1427,111 +1384,154 @@ Proof. simpl. reflexivity. } - unfold sem_rel_b', sem_rel_b. - apply load_notrap1_sound; auto. - } - { - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - rewrite (subst_args_ok' sp m); assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem', fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). - { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + apply load_sound with (a := a); assumption. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - apply load_notrap1_sound; assumption. - } - -(* load notrap2 *) -- unfold transf_instr in *. - destruct find_load_in_fmap eqn:FIND_LOAD. - { - unfold find_load_in_fmap, fmap_sem', fmap_sem in *. - destruct (forward_map f) as [map |] eqn:MAP. - 2: discriminate. - change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. - destruct (map # pc) as [mpc | ] eqn:MPC. - 2: discriminate. - econstructor; split. - { - eapply exec_Iop with (v := Vundef); eauto. - simpl. - rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0. + + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + destruct find_load_in_fmap eqn:FIND_LOAD. + { + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := Vundef); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL. + { + f_equal. + rewrite MAP in EVAL. + eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: try eassumption. apply LOAD; auto. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_notrap2_sound with (a := v); auto. + } + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some v). + rewrite <- EVAL. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite (subst_args_ok' sp m). + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'; auto. + assumption. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_notrap2_sound with (a := v); auto. + } + + * destruct find_load_in_fmap eqn:FIND_LOAD. { - f_equal. - rewrite MAP in H0. - eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). - all: try eassumption. + unfold find_load_in_fmap, fmap_sem', fmap_sem in *. + destruct (forward_map f) as [map |] eqn:MAP. + 2: discriminate. + change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. + destruct (map # pc) as [mpc | ] eqn:MPC. + 2: discriminate. + econstructor; split. + { + eapply exec_Iop with (v := Vundef); eauto. + simpl. + rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL. + { + f_equal. + rewrite MAP in EVAL. + eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs). + all: eassumption. + } + unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. + } + constructor; eauto. + unfold fmap_sem', fmap_sem in *. + rewrite MAP. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + { + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + unfold sem_rel_b', sem_rel_b. + apply load_notrap1_sound; auto. } - unfold fmap_sem. rewrite MAP. rewrite MPC. assumption. - } - constructor; eauto. - unfold fmap_sem', fmap_sem in *. - rewrite MAP. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). - { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- EVAL. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite (subst_args_ok' sp m); eauto. congruence. + constructor; auto. + + simpl in *. + unfold fmap_sem', fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_notrap1_sound; assumption. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - unfold sem_rel_b', sem_rel_b. - apply load_notrap2_sound with (a := a); auto. - } - { - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - rewrite (subst_args_ok' sp m); assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem', fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). - { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - apply load_notrap2_sound with (a := a); assumption. - } - (* store *) econstructor. split. diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index a601d5d5..86c2c8a7 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -582,48 +582,51 @@ Proof. apply oper_sound; unfold ctx; eauto with cse3. (* END INVARIANT *) - (* Iload *) - exists (State ts tf sp pc' (rs # dst <- v) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite H1 in FIND_SOUND. (* LOAD *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + inv H0. + + exists (State ts tf sp pc' (rs # dst <- v) m). split. + * pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + -- destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite LOAD in FIND_SOUND. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_normal; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + assumption. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. TR_AT. { subst instr'. congruence. } + eapply has_loaded_normal; eauto. rewrite subst_args_ok with (sp:=sp) (m:=m). { rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. @@ -634,183 +637,187 @@ Proof. with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). rewrite INV_PC. assumption. - + econstructor; eauto. - * eapply wt_exec_Iload with (f:=f); try eassumption. + * econstructor; eauto. + -- eapply wt_exec_Iload with (f:=f); try eassumption. eauto with wt. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) - - - (* Iload notrap1 *) - exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - + econstructor; eauto. - * apply wt_undef; assumption. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) + -- (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) + + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + ++ destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite LOAD in FIND_SOUND; auto. (* LOAD *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- econstructor; eauto. + ++ apply wt_undef; assumption. + ++ (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - - (* Iload notrap2 *) - exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. - + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. - assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. - unfold param_transf_instr, find_load_in_fmap in instr'. - destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. - pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) - (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. - * destruct rhs_find eqn:FIND. - ** apply exec_Iop with (op := Omove) (args := r :: nil). - TR_AT. - subst instr'. - congruence. - simpl. - specialize FIND_SOUND with (src := r) (rs := rs) (m := m). - simpl in FIND_SOUND. - rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. - rewrite H0 in FIND_SOUND. (* ADDR *) - rewrite H1 in FIND_SOUND. (* LOAD *) - rewrite FIND_SOUND; auto. - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. - TR_AT. - { subst instr'. - congruence. } - rewrite subst_args_ok with (sp:=sp) (m:=m). - { - rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. - assumption. - } - unfold fmap_sem. - change ((fst (preanalysis tenv f)) # pc) - with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). - rewrite INV_PC. - assumption. - + econstructor; eauto. - * apply wt_undef; assumption. - * (* BEGIN INVARIANT *) - fold ctx. fold invs. - assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). - unfold check_inductiveness in IND. - rewrite andb_true_iff in IND. - destruct IND as [IND_entry IND_step]. - rewrite PTree_Properties.for_all_correct in IND_step. - pose proof (IND_step pc _ H) as IND_step_me. - clear IND_entry IND_step. - destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. - 2: contradiction. - cbn in IND_step_me. - destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. - 2: discriminate. - rewrite andb_true_iff in IND_step_me. - destruct IND_step_me. - rewrite rel_leb_correct in *. - eapply rel_ge. - eassumption. - apply oper_sound; unfold ctx; eauto with cse3. - (* END INVARIANT *) + * exists (State ts tf sp pc' (rs # dst <- Vundef) m). split. + -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'. + assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity. + unfold param_transf_instr, find_load_in_fmap in instr'. + destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC. + pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr) + (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND. + ++ destruct rhs_find eqn:FIND. + ** apply exec_Iop with (op := Omove) (args := r :: nil). + TR_AT. + subst instr'. + congruence. + simpl. + specialize FIND_SOUND with (src := r) (rs := rs) (m := m). + simpl in FIND_SOUND. + rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND. + rewrite EVAL in FIND_SOUND. (* ADDR *) + rewrite FIND_SOUND; auto. + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial. + TR_AT. + { subst instr'. + congruence. } + eapply has_loaded_default; eauto. + rewrite subst_args_ok with (sp:=sp) (m:=m). + { + rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + unfold fmap_sem. + change ((fst (preanalysis tenv f)) # pc) + with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))). + rewrite INV_PC. + assumption. + -- econstructor; eauto. + ++ apply wt_undef; assumption. + ++ (* BEGIN INVARIANT *) + fold ctx. fold invs. + assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto). + unfold check_inductiveness in IND. + rewrite andb_true_iff in IND. + destruct IND as [IND_entry IND_step]. + rewrite PTree_Properties.for_all_correct in IND_step. + pose proof (IND_step pc _ H) as IND_step_me. + clear IND_entry IND_step. + destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL. + 2: contradiction. + cbn in IND_step_me. + destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *. + 2: discriminate. + rewrite andb_true_iff in IND_step_me. + destruct IND_step_me. + rewrite rel_leb_correct in *. + eapply rel_ge. + eassumption. + apply oper_sound; unfold ctx; eauto with cse3. + (* END INVARIANT *) - (* Istore *) exists (State ts tf sp pc' rs m'). split. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 556b44b3..72b52375 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1098,135 +1098,126 @@ Proof. destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - destruct trap. - - (* TRAP *) - { - destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. -+ (* replaced by move *) - exploit find_rhs_sound; eauto. intros (v' & EV & LD). - assert (v' = v) by (inv EV; congruence). subst v'. - econstructor; split. - eapply exec_Iop; eauto. simpl; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. -+ (* load is preserved, but addressing is possibly simplified *) - destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. - assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). - { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. - intros; eapply combine_addr_sound; eauto. } - exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. - intros [a' [A B]]. - assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). - { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends; eauto. - intros [v' [X Y]]. - econstructor; split. - eapply exec_Iload; eauto. - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - eapply add_load_holds; eauto. - apply set_reg_lessdef; auto. - } - - (* NOTRAP *) - { - assert (exists a' : val, - eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') - as Haa'. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Haa' as [a' [Ha'1 Ha'2]]. - - assert ( - exists v' : val, - Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by - (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). - destruct Hload' as [v' [Hv'1 Hv'2]]. - - econstructor. split. - eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. - assumption. - apply set_reg_lessdef; assumption. - } - -- (* Iload notrap 1*) - destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - - econstructor. split. - eapply exec_Iload_notrap1; eauto. - rewrite eval_addressing_preserved with (ge1 := ge). - apply eval_addressing_lessdef_none with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - exact symbols_preserved. - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. - assumption. - apply set_reg_lessdef. - constructor. assumption. - -- (* Iload notrap 2*) - destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. - destruct SAT as [valu1 NH1]. - exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q). - - assert (exists a' : val, - eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') - as Haa'. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Haa' as [a' [Ha'1 Ha'2]]. + destruct trap; inv H0. + + + (* TRAP *) + { destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?. + * (* replaced by move *) + exploit find_rhs_sound; eauto. intros (v' & EV & LD). + assert (v' = v) by (inv EV; congruence). subst v'. + econstructor; split. + eapply exec_Iop; eauto. simpl; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto. + * (* load is preserved, but addressing is possibly simplified *) + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. } + exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR. + intros [a' [A B]]. + assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a'). + { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends; eauto. + intros [v' [X Y]]. + econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + eapply add_load_holds; eauto. + apply set_reg_lessdef; auto. } + + + (* NOTRAP1 *) + { assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Haa' as [a' [Ha'1 Ha'2]]. - destruct (Mem.loadv chunk m' a') eqn:Hload'. + assert ( + exists v' : val, + Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by + (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption). + destruct Hload' as [v' [Hv'1 Hv'2]]. - { econstructor. split. - eapply exec_Iload; eauto. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - + econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. unfold transfer. rewrite H. exists valu1. apply set_unknown_holds. assumption. - apply set_reg_lessdef; eauto. + apply set_reg_lessdef; assumption. } - { - econstructor. split. - eapply exec_Iload_notrap2; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). - - econstructor; eauto. - eapply analysis_correct_1; eauto. simpl; eauto. - unfold transfer. rewrite H. - exists valu1. - apply set_unknown_holds. + + + (* NOTRAP2 *) + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (exists a' : val, + eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef v a') + as Haa'. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. assumption. - apply set_reg_lessdef. - constructor. assumption. - } - + destruct Haa' as [a' [Ha'1 Ha'2]]. + + destruct (Mem.loadv chunk m' a') eqn:Hload'. + + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef; eauto. + } + { + econstructor. split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a EVAL'; + rewrite eval_addressing_preserved with (ge1 := ge) in EVAL'; [| exact symbols_preserved]; + inv Ha'2; rewrite Ha'1 in EVAL'; inv EVAL'; auto). + + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + } + * econstructor. split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1 := ge). + intros a EVAL'. eapply eval_addressing_lessdef_none with (vl1 := rs ## args) in EVAL. + erewrite EVAL in EVAL'. congruence. + apply regs_lessdef_regs; assumption. + exact symbols_preserved. + + -- econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; eauto. + unfold transfer. rewrite H. + exists valu1. + apply set_unknown_holds. + assumption. + apply set_reg_lessdef. + constructor. assumption. + - (* Istore *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. destruct SAT as [valu1 NH1]. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b59ee8b4..749add67 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -402,90 +402,89 @@ Proof. - (* Iload *) rename pc'0 into pc. TransfInstr. - set (aa := eval_static_addressing addr (aregs ae args)). - assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). - set (av := loadv chunk (romem_for cu) am aa). - assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). - destruct trap. - { - destruct (const_for_result av) as [cop|] eqn:?; intros. -+ (* constant-propagated *) - exploit const_for_result_correct; eauto. intros (v' & A & B). - left; econstructor; econstructor; split. - eapply exec_Iop; eauto. - eapply match_states_succ; eauto. - apply set_reg_lessdef; auto. -+ (* strength-reduced *) - assert (ADDR: - let (addr', args') := addr_strength_reduction addr args (aregs ae args) in - exists a', - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\ - Val.lessdef a a'). - { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } - destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. - destruct ADDR as (a' & P & Q). - exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. - intros (a'' & U & V). - assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a''). - { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } - exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. - intros (v' & X & Y). - left; econstructor; econstructor; split. - eapply exec_Iload; eauto. - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - } - { - assert (exists v2 : val, - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Hexist2 as [v2 [Heval2 Hlessdef2]]. - destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]]. - left; econstructor; econstructor; split. - eapply exec_Iload with (a := v2); eauto. - try (erewrite eval_addressing_preserved with (ge1:=ge); auto; - exact symbols_preserved). - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - - } - -- (* Iload notrap1 *) - rename pc'0 into pc. TransfInstr. - assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = None). - rewrite eval_addressing_preserved with (ge1 := ge); eauto. - apply eval_addressing_lessdef_none with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - exact symbols_preserved. - - left; econstructor; econstructor; split. - eapply exec_Iload_notrap1; eauto. - eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - -- (* Iload notrap2 *) - rename pc'0 into pc. TransfInstr. - assert (exists v2 : val, - eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. - apply eval_addressing_lessdef with (vl1 := rs ## args). - apply regs_lessdef_regs; assumption. - assumption. - destruct Hexist2 as [a' [Heval' Hlessdef']]. - destruct (Mem.loadv chunk m' a') eqn:Hload'. + inv H0. + + set (aa := eval_static_addressing addr (aregs ae args)). + assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va). + set (av := loadv chunk (romem_for cu) am aa). + assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto). + destruct trap. { + destruct (const_for_result av) as [cop|] eqn:?; intros. + * (* constant-propagated *) + exploit const_for_result_correct; eauto. intros (v' & A & B). + left; econstructor; econstructor; split. + eapply exec_Iop; eauto. + eapply match_states_succ; eauto. + apply set_reg_lessdef; auto. + * (* strength-reduced *) + assert (ADDR: + let (addr', args') := addr_strength_reduction addr args (aregs ae args) in + exists a', + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\ + Val.lessdef a a'). + { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. } + destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args']. + destruct ADDR as (a' & P & Q). + exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P. + intros (a'' & U & V). + assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a''). + { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. } + exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto. + intros (v' & X & Y). left; econstructor; econstructor; split. - eapply exec_Iload; eauto. - - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. eapply match_states_succ; eauto. apply set_reg_lessdef; auto. } { + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [v2 [Heval2 Hlessdef2]]. + destruct (Mem.loadv_extends chunk m m' a v2 v MEM LOAD Hlessdef2) as [vX [Hvx1 Hvx2]]. left; econstructor; econstructor; split. - eapply exec_Iload_notrap2; eauto. - - try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (erewrite eval_addressing_preserved with (ge1:=ge); auto; + exact symbols_preserved). eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (exists v2 : val, + eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef v v2) as Hexist2. + apply eval_addressing_lessdef with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + destruct Hexist2 as [a' [Heval' Hlessdef']]. + destruct (Mem.loadv chunk m' a') eqn:Hload'. + { + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. + + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply has_loaded_normal; eauto. + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + { + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a; rewrite eval_addressing_preserved with (ge1 := ge); [ intros CONTRA; try congruence | exact symbols_preserved ]). + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. + } + * assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = None). + rewrite eval_addressing_preserved with (ge1 := ge); eauto. + apply eval_addressing_lessdef_none with (vl1 := rs ## args). + apply regs_lessdef_regs; assumption. + assumption. + exact symbols_preserved. + + left; econstructor; econstructor; split. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros; congruence. + eapply match_states_succ; eauto. apply set_reg_lessdef; auto. - (* Istore *) rename pc'0 into pc. TransfInstr. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index be20af0b..305e8eeb 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -797,113 +797,108 @@ Ltac UseTransfer := apply eagree_update; eauto 2 with na. - (* load *) - TransfInstr; UseTransfer. - destruct (is_dead (nreg ne dst)) eqn:DEAD; + TransfInstr; UseTransfer. inv H0. ++ destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +* (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +* (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. destruct v; simpl; auto. apply iagree_zero. -+ (* preserved *) +* (* preserved *) exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. intros (ta & U & V). inv V; try discriminate. - destruct ta; simpl in H1; try discriminate. + destruct ta; simpl in EVAL; try discriminate. exploit magree_load; eauto. exploit aaddressing_sound; eauto. intros (bc & A & B & C). intros. apply nlive_add with bc i; assumption. intros (tv & P & Q). econstructor; split. - eapply exec_Iload with (a := Vptr b i). eauto. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - -- (* load notrap1 *) - TransfInstr; UseTransfer. ++ destruct (eval_addressing) eqn:EVAL in LOAD. +* specialize (LOAD v). destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +** (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. constructor. -+ (* preserved *) - exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption. - intro Hnone'. - assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'. +** (* preserved *) + exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. + intros (ta & U & V). + destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. + { + econstructor; split. + eapply exec_Iload. eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved with (ge1 := ge). assumption. exact symbols_preserved. - + eapply match_succ_states; eauto. simpl; auto. + apply eagree_update; eauto 2 with na. + eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. + } + { econstructor; split. - eapply exec_Iload_notrap1; eauto. + eapply exec_Iload. eauto. eapply has_loaded_default; eauto. + erewrite eval_addressing_preserved with (ge1 := ge). + intros a EVAL'; rewrite U in EVAL'; inv EVAL'. auto. + exact symbols_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - -- (* load notrap2 *) - TransfInstr; UseTransfer. - - destruct (is_dead (nreg ne dst)) eqn:DEAD; + } +* destruct (is_dead (nreg ne dst)) eqn:DEAD; [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO]; simpl in *. -+ (* dead instruction, turned into a nop *) +** (* dead instruction, turned into a nop *) econstructor; split. eapply exec_Inop; eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update_dead; auto with na. -+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) +** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *) econstructor; split. eapply exec_Iop with (v := Vint Int.zero); eauto. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; auto. rewrite is_int_zero_sound by auto. constructor. -+ (* preserved *) - exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto. - intros (ta & U & V). - destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. - { - econstructor; split. - eapply exec_Iload. eauto. +** exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption. + intro Hnone'. + assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'. erewrite eval_addressing_preserved with (ge1 := ge). - eassumption. + assumption. exact symbols_preserved. - eassumption. - eapply match_succ_states; eauto. simpl; auto. - apply eagree_update; eauto 2 with na. - eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - } - { + econstructor; split. - eapply exec_Iload_notrap2. eauto. - erewrite eval_addressing_preserved with (ge1 := ge). - eassumption. - exact symbols_preserved. - eassumption. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite Hnone2' in EVAL'; inv EVAL'. + eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. - } + - (* store *) TransfInstr; UseTransfer. destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 2f3bad2f..c4270e46 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -414,25 +414,19 @@ Proof. (* Iload *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. - pose symbols_preserved as SYMPRES. - eexists. split. - + eapply exec_Iload; eauto; (* is the follow still needed?*) erewrite eval_addressing_preserved; eauto. - + econstructor; eauto. -(* Iload notrap1 *) - - eapply dupmap_correct in DUPLIC; eauto. - destruct DUPLIC as (i' & H2 & H3). inv H3. - pose symbols_preserved as SYMPRES. - eexists. split. - + eapply exec_Iload_notrap1; eauto; erewrite eval_addressing_preserved; eauto. - + econstructor; eauto. -(* Iload notrap2 *) - - eapply dupmap_correct in DUPLIC; eauto. - destruct DUPLIC as (i' & H2 & H3). inv H3. - pose symbols_preserved as SYMPRES. - eexists. split. - + eapply exec_Iload_notrap2; eauto; erewrite eval_addressing_preserved; eauto. - + econstructor; eauto. - + pose symbols_preserved as SYMPRES. inv H0. + + eexists; split. + * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved; eauto. + * econstructor; eauto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). eexists; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. erewrite eval_addressing_preserved; eauto. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + -- econstructor; eauto. + * eexists; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. erewrite eval_addressing_preserved; eauto. + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + -- econstructor; eauto. (* Istore *) - eapply dupmap_correct in DUPLIC; eauto. destruct DUPLIC as (i' & H2 & H3). inv H3. diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v index 5a1c5acf..b0cf0879 100644 --- a/backend/FirstNopproof.v +++ b/backend/FirstNopproof.v @@ -178,23 +178,28 @@ Proof. apply eval_operation_preserved. apply symbols_preserved. + constructor; auto with firstnop. - - left. econstructor. split. - + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. - all: rewrite <- H0. - all: auto using eval_addressing_preserved, symbols_preserved. - + constructor; auto with firstnop. - - left. econstructor. split. - + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop. - all: rewrite <- H0; - apply eval_addressing_preserved; - apply symbols_preserved. - + constructor; auto with firstnop. - - left. econstructor. split. - + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop. - all: rewrite <- H0; - apply eval_addressing_preserved; - apply symbols_preserved. - + constructor; auto with firstnop. + - left. inv H0. + + econstructor. split. + * eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop. + eapply has_loaded_normal; eauto. + all: rewrite <- EVAL. + all: auto using eval_addressing_preserved, symbols_preserved. + * constructor; auto with firstnop. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + -- eapply plus_one. eapply exec_Iload; eauto with firstnop. + eapply has_loaded_default; eauto. + all: + rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved]; + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto. + -- constructor; auto with firstnop. + * econstructor; split. + -- eapply plus_one. eapply exec_Iload; eauto with firstnop. + eapply has_loaded_default; eauto. + all: + rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved]; + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto. + -- constructor; auto with firstnop. - left. econstructor. split. + eapply plus_one. eapply exec_Istore; eauto with firstnop. all: rewrite <- H0; diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index f3e572e0..27137206 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -494,89 +494,89 @@ Proof. assumption. (* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. - apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. - - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). - { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. - } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. - -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - rewrite subst_args_ok; assumption. - constructor; auto. +- inv H0. + + econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- EVAL. + apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite subst_args_ok; assumption. + constructor; auto. - simpl in *. - unfold fmap_sem in *. - destruct (forward_map _) as [map |] eqn:MAP in *; trivial. - destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. - apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). - { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). { - eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. - 2: apply apply_instr'_bot. - simpl. tauto. + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. } - unfold apply_instr'. - rewrite H. - rewrite MPC. - reflexivity. - } - apply kill_ok. - assumption. + apply kill_ok. + assumption. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some v). + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite subst_args_ok; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. apply LOAD; auto. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. + * econstructor; split. + assert (eval_addressing tge sp addr rs ## args = None). + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite subst_args_ok; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + constructor; auto. + + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction. + apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)). + { + replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + { + eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption. + 2: apply apply_instr'_bot. + simpl. tauto. + } + unfold apply_instr'. + rewrite H. + rewrite MPC. + reflexivity. + } + apply kill_ok. + assumption. - (* store *) econstructor; split. diff --git a/backend/Injectproof.v b/backend/Injectproof.v index dd5e72f8..13154850 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -785,24 +785,29 @@ Section INJECTOR. rewrite map_length. assumption. - rewrite Pos.ltb_lt in VALID. - destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:ADDR. + destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:EVAL. + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD. * exists (trs # res <- v). split. - ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_normal; eauto. all: try rewrite eval_addressing_preserved with (ge1 := ge). all: auto using symbols_preserved. ** apply assign_above; auto. * exists (trs # res <- Vundef). split. - ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_default; eauto. all: rewrite eval_addressing_preserved with (ge1 := ge). + intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'. assumption. all: auto using symbols_preserved. ** apply assign_above; auto. + exists (trs # res <- Vundef). split. - * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + * apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial. + eapply has_loaded_default; eauto. all: rewrite eval_addressing_preserved with (ge1 := ge). + intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'. all: auto using symbols_preserved. * apply assign_above; auto. Qed. @@ -1351,128 +1356,127 @@ Section INJECTOR. assumption. - (* load *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. - { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- v). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - eassumption. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- v); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** eassumption. - * constructor; trivial. - apply match_regs_write. - assumption. - - - (* load notrap1 *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. + inv H0. + + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + * exploit transf_function_redirects; eauto. { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- Vundef). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - * constructor; trivial. - apply match_regs_write. - assumption. - - - (* load notrap2 *) - destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. - + exploit transf_function_redirects; eauto. - { eapply max_pc_function_sound; eauto. } - intros [pc_inj [ALTER SKIP]]. - specialize SKIP with (ts := ts) (sp := sp) (m := m) - (trs := trs # dst <- Vundef). - destruct SKIP as [trs' [MATCH PLUS]]. - econstructor; split. - * eapply Smallstep.plus_left. - ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). - exact ALTER. - rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - eassumption. - ** apply Smallstep.plus_star. - exact PLUS. - ** reflexivity. - * constructor; trivial. - apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. - apply match_regs_write. - assumption. - + econstructor; split. - * apply Smallstep.plus_one. - apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a). - ** rewrite transf_function_preserves with (f:=f); eauto. - eapply max_pc_function_sound; eauto. - ** rewrite eval_addressing_preserved with (ge1 := ge). - { - replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. - rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. - } - exact symbols_preserved. - ** eassumption. - * constructor; trivial. - apply match_regs_write. - assumption. + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- v). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + -- eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + -- constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- v); trivial. + apply match_regs_write. + assumption. + * econstructor; split. + -- apply Smallstep.plus_one. + apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + } + exact symbols_preserved. + -- constructor; trivial. + apply match_regs_write. + assumption. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + -- exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + ++ eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + ++ constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + -- econstructor; split. + ++ apply Smallstep.plus_one. + apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + } + exact symbols_preserved. + ++ constructor; trivial. + apply match_regs_write. + assumption. + * destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. + -- exploit transf_function_redirects; eauto. + { eapply max_pc_function_sound; eauto. } + intros [pc_inj [ALTER SKIP]]. + specialize SKIP with (ts := ts) (sp := sp) (m := m) + (trs := trs # dst <- Vundef). + destruct SKIP as [trs' [MATCH PLUS]]. + econstructor; split. + ++ eapply Smallstep.plus_left. + ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + exact ALTER. + eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + exact symbols_preserved. + ** apply Smallstep.plus_star. + exact PLUS. + ** reflexivity. + ++ constructor; trivial. + apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial. + apply match_regs_write. + assumption. + -- econstructor; split. + ++ apply Smallstep.plus_one. + apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args). + ** rewrite transf_function_preserves with (f:=f); eauto. + eapply max_pc_function_sound; eauto. + ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge). + { + replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity. + rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial. + simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + } + exact symbols_preserved. + ++ constructor; trivial. + apply match_regs_write. + assumption. - (* store *) destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index eb30732b..a4bf838e 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -969,66 +969,53 @@ Proof. apply agree_set_reg; auto. - (* load *) - exploit tr_funbody_inv; eauto. intros TR; inv TR. - exploit eval_addressing_inject. - eapply match_stacks_inside_globals; eauto. - eexact SP. - instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. - eauto. - fold (saddr ctx addr). intros [a' [P Q]]. - exploit Mem.loadv_inject; eauto. intros [v' [U V]]. - assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). - rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. - left; econstructor; split. - eapply plus_one. eapply exec_Iload; eauto. - econstructor; eauto. - apply match_stacks_inside_set_reg; auto. - apply agree_set_reg; auto. - -- (* load notrap1 *) - exploit tr_funbody_inv; eauto. intros TR; inv TR. - left; econstructor; split. - eapply plus_one. eapply exec_Iload_notrap1. eassumption. - rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge). - exploit eval_addressing_inj_none. - 4: eassumption. - intros. eapply symbol_address_inject. - eapply match_stacks_inside_globals; eauto. - eauto. - instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. - rewrite Ptrofs.add_zero_l. - apply eval_addressing_none. - exact symbols_preserved. - econstructor; eauto. - apply match_stacks_inside_set_reg; auto. - apply agree_set_reg; auto. - -- (* load notrap2 *) - exploit tr_funbody_inv; eauto. intros TR; inv TR. - - exploit eval_addressing_inject. + exploit tr_funbody_inv; eauto. intros TR; inv TR. inv H0. + + exploit eval_addressing_inject. eapply match_stacks_inside_globals; eauto. eexact SP. instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. eauto. - fold (saddr ctx addr). intros [a' [P Q]]. - - destruct (Mem.loadv chunk m' a') eqn:Hload'. - + left; econstructor; split. - eapply plus_one. - eapply exec_Iload; eauto. - try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). - econstructor; eauto. - apply match_stacks_inside_set_reg; auto. - apply agree_set_reg; auto. - - + left; econstructor; split. - eapply plus_one. - eapply exec_Iload_notrap2; eauto. - try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). - econstructor; eauto. - apply match_stacks_inside_set_reg; auto. - apply agree_set_reg; auto. + fold (saddr ctx addr). intros [a' [P Q]]. + exploit Mem.loadv_inject; eauto. intros [v' [U V]]. + assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + { rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. } + left; econstructor; split. + * eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + * econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + + destruct (eval_addressing) eqn:ADDR in LOAD. + * exploit eval_addressing_inject. + eapply match_stacks_inside_globals; eauto. + eexact SP. + instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + eauto. + fold (saddr ctx addr). intros [a' [P Q]]. + destruct (Mem.loadv chunk m' a') eqn:Hload'. + -- left; econstructor; split. + ++ eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + -- left; econstructor; split. + ++ eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + try (intros a ADDR'; erewrite eval_addressing_preserved in ADDR'; [ rewrite P in ADDR' | + exact symbols_preserved ]; inv ADDR'; assumption). + ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. + * left; econstructor; split. + -- eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros. rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge) in H0. + exploit eval_addressing_inj_none. + 4: eassumption. + intros. eapply symbol_address_inject. + eapply match_stacks_inside_globals; eauto. + eauto. + instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto. + rewrite Ptrofs.add_zero_l. + intros. apply eval_addressing_none in H1. congruence. + exact symbols_preserved. + -- econstructor; eauto. apply match_stacks_inside_set_reg; auto. + apply agree_set_reg; auto. - (* store *) exploit tr_funbody_inv; eauto. intros TR; inv TR. diff --git a/backend/KillUselessMovesproof.v b/backend/KillUselessMovesproof.v index 629aa6aa..7309c28e 100644 --- a/backend/KillUselessMovesproof.v +++ b/backend/KillUselessMovesproof.v @@ -227,32 +227,34 @@ Proof. apply eval_operation_preserved. exact symbols_preserved. constructor; auto using same_rs_write. (* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs' ## args = Some a). - { rewrite <- H0. - rewrite (same_rs_subst rs rs' args SAME). - apply eval_addressing_preserved. exact symbols_preserved. - } - eapply exec_Iload; eauto. - constructor; auto using same_rs_write. -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs' ## args = None). - { rewrite <- H0. - rewrite (same_rs_subst rs rs' args SAME). - apply eval_addressing_preserved. exact symbols_preserved. - } - eapply exec_Iload_notrap1; eauto. - constructor; auto using same_rs_write. -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs' ## args = Some a). - { rewrite <- H0. - rewrite (same_rs_subst rs rs' args SAME). - apply eval_addressing_preserved. exact symbols_preserved. - } - eapply exec_Iload_notrap2; eauto. - constructor; auto using same_rs_write. +- inv H0. + + econstructor; split. + assert (eval_addressing tge sp addr rs' ## args = Some a). + { rewrite <- EVAL. + rewrite (same_rs_subst rs rs' args SAME). + apply eval_addressing_preserved. exact symbols_preserved. + } + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + constructor; auto using same_rs_write. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + assert (eval_addressing tge sp addr rs' ## args = Some v). + { rewrite <- EVAL. + rewrite (same_rs_subst rs rs' args SAME). + apply eval_addressing_preserved. exact symbols_preserved. + } + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. apply LOAD; auto. + constructor; auto using same_rs_write. + * econstructor; split. + assert (eval_addressing tge sp addr rs' ## args = None). + { rewrite <- EVAL. + rewrite (same_rs_subst rs rs' args SAME). + apply eval_addressing_preserved. exact symbols_preserved. + } + eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + constructor; auto using same_rs_write. - (* store *) econstructor; split. assert (eval_addressing tge sp addr rs' ## args = Some a). diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v index 78de09af..292acc2a 100644 --- a/backend/ProfilingExploitproof.v +++ b/backend/ProfilingExploitproof.v @@ -126,23 +126,24 @@ Proof. rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. constructor; auto. (* load *) -- econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - constructor; auto. -- (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - constructor; auto. -- (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - constructor; auto. +- inv H0. + + econstructor; split. + * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * econstructor; eauto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + exact symbols_preserved. + -- econstructor; eauto. + * econstructor; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + exact symbols_preserved. + -- econstructor; eauto. - (* store *) econstructor; split. assert (eval_addressing tge sp addr rs ## args = Some a). diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v index 0cebc601..e39e7f80 100644 --- a/backend/Profilingproof.v +++ b/backend/Profilingproof.v @@ -458,27 +458,27 @@ Proof. * rewrite eval_operation_preserved with (ge1:=ge); eauto with profiling. + constructor; auto. - - econstructor; split. - + apply plus_one. apply exec_Iload with (trap:=trap) (chunk:=chunk) - (addr:=addr) (args:=args) (a:=a). - erewrite transf_function_at; eauto. apply I. - rewrite eval_addressing_preserved with (ge1:=ge). - all: eauto with profiling. - + constructor; auto. - - econstructor; split. - + apply plus_one. apply exec_Iload_notrap1 with (chunk:=chunk) - (addr:=addr) (args:=args). - erewrite transf_function_at; eauto. apply I. - rewrite eval_addressing_preserved with (ge1:=ge). - all: eauto with profiling. - + constructor; auto. - - econstructor; split. - + apply plus_one. apply exec_Iload_notrap2 with (chunk:=chunk) - (addr:=addr) (args:=args) (a:=a). - erewrite transf_function_at; eauto. apply I. - rewrite eval_addressing_preserved with (ge1:=ge). - all: eauto with profiling. - + constructor; auto. + - inv H0. + + econstructor; split. + * apply plus_one. eapply exec_Iload; eauto. + -- erewrite transf_function_at; eauto. apply I. + -- eapply has_loaded_normal. rewrite eval_addressing_preserved with (ge1:=ge). + all: eauto with profiling. + * constructor; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * econstructor; split. + -- specialize (LOAD v). apply plus_one. eapply exec_Iload; eauto. + ++ erewrite transf_function_at; eauto. apply I. + ++ eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + eauto with profiling. + -- constructor; auto. + * econstructor; split. + -- apply plus_one. eapply exec_Iload; eauto. + ++ erewrite transf_function_at; eauto. apply I. + ++ eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. eauto with profiling. + -- constructor; auto. - econstructor; split. + apply plus_one. apply exec_Istore with (chunk:=chunk) (src := src) (addr:=addr) (args:=args) (a:=a). diff --git a/backend/RTL.v b/backend/RTL.v index fe350adf..b43fd377 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -181,6 +181,18 @@ Inductive state : Type := (m: mem), (**r memory state *) state. +Inductive has_loaded {F V: Type} (genv: Genv.t F V) sp rs m chunk addr args v: trapping_mode -> Prop := + | has_loaded_normal a trap + (EVAL: eval_addressing genv sp addr rs##args = Some a) + (LOAD: Mem.loadv chunk m a = Some v) + : has_loaded genv sp rs m chunk addr args v trap + | has_loaded_default + (LOAD: forall a, eval_addressing genv sp addr rs##args = Some a -> Mem.loadv chunk m a = None) + (DEFAULT: v = Vundef) + : has_loaded genv sp rs m chunk addr args v NOTRAP + . +Local Hint Constructors has_loaded: core. + Section RELSEM. Variable ge: genv. @@ -214,25 +226,11 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp pc rs m) E0 (State s f sp pc' (rs#res <- v) m) | exec_Iload: - forall s f sp pc rs m trap chunk addr args dst pc' a v, + forall s f sp pc rs m trap chunk addr args dst pc' v, (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> + has_loaded ge sp rs m chunk addr args v trap -> step (State s f sp pc rs m) E0 (State s f sp pc' (rs#dst <- v) m) - | exec_Iload_notrap1: - forall s f sp pc rs m chunk addr args dst pc', - (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> - eval_addressing ge sp addr rs##args = None -> - step (State s f sp pc rs m) - E0 (State s f sp pc' (rs#dst <- Vundef) m) - | exec_Iload_notrap2: - forall s f sp pc rs m chunk addr args dst pc' a, - (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') -> - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = None-> - step (State s f sp pc rs m) - E0 (State s f sp pc' (rs#dst <- Vundef) m) | exec_Istore: forall s f sp pc rs m chunk addr args src pc' a m', (fn_code f)!pc = Some(Istore chunk addr args src pc') -> diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 0861143b..2cef08e2 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -452,43 +452,47 @@ Proof. 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. 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. + inv H0. + + 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. + -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved. + * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + exploit eval_addressing_lessdef; try eassumption. + apply reglist_lessdef; apply RS. + intros (ta & ADDR & 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. + ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved. + ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + -- left; eexists; split. + eapply exec_Iload. + ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. + ++ eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite ADDR in EVAL'; inv EVAL'. auto. + apply symbols_preserved. + ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. + * exploit eval_addressing_lessdef_none; try eassumption. + apply reglist_lessdef; apply RS. + left. eexists. split. + -- eapply exec_Iload. + ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. + ++ eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + apply symbols_preserved. + -- apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS. - (* Lstore *) exploit eval_addressing_lessdef; try eassumption. apply reglist_lessdef; apply RS. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index d07dc968..59d0a451 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -586,9 +586,9 @@ Proof. exists (rs1#rd <- v'); exists tm1. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iload. eauto. - instantiate (1 := vaddr'). rewrite <- H3. + econstructor; eauto. rewrite <- H3. apply eval_addressing_preserved. exact symbols_preserved. - auto. traceEq. + auto. (* Match-env *) split. eauto with rtlg. (* Result *) 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: diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 2e161965..7c7bc7e3 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -162,84 +162,85 @@ Lemma step_simulation: Proof. induction 1; intros S1' MS; inv MS; try TR_AT. (* nop *) - econstructor; split. eapply exec_Inop; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + - econstructor; split. eapply exec_Inop; eauto. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* op *) - econstructor; split. - eapply exec_Iop; eauto. - instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + - econstructor; split. + eapply exec_Iop; eauto. + instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* load *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. - (* load notrap1 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = None). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap1; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. - (* load notrap2 *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Iload_notrap2; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + - inv H0. + + econstructor; split. + * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * econstructor; eauto. eapply reach_succ; eauto. simpl; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). econstructor; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto. + exact symbols_preserved. + -- econstructor; eauto. eapply reach_succ; eauto. simpl; auto. + * econstructor; split. + -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + rewrite eval_addressing_preserved with (ge1:=ge). + intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. + exact symbols_preserved. + -- econstructor; eauto. eapply reach_succ; eauto. simpl; auto. (* store *) - econstructor; split. - assert (eval_addressing tge sp addr rs ## args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eapply exec_Istore; eauto. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + - econstructor; split. + assert (eval_addressing tge sp addr rs ## args = Some a). + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* call *) - econstructor; split. - eapply exec_Icall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto. + - econstructor; split. + eapply exec_Icall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto. (* tailcall *) - econstructor; split. - eapply exec_Itailcall with (fd := transf_fundef fd); eauto. - eapply find_function_translated; eauto. - apply sig_preserved. - constructor. auto. + - econstructor; split. + eapply exec_Itailcall with (fd := transf_fundef fd); eauto. + eapply find_function_translated; eauto. + apply sig_preserved. + constructor. auto. (* builtin *) - econstructor; split. - eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. eapply reach_succ; eauto. simpl; auto. + - econstructor; split. + eapply exec_Ibuiltin; eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) - econstructor; split. - eapply exec_Icond; eauto. - replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot) - with (renum_pc (pnum f) (if b then ifso else ifnot)). - constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto. - destruct b; auto. + - econstructor; split. + eapply exec_Icond; eauto. + replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot) + with (renum_pc (pnum f) (if b then ifso else ifnot)). + constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto. + destruct b; auto. (* jumptbl *) - econstructor; split. - eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto. - constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto. + - econstructor; split. + eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto. + constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto. (* return *) - econstructor; split. - eapply exec_Ireturn; eauto. - constructor; auto. + - econstructor; split. + eapply exec_Ireturn; eauto. + constructor; auto. (* internal function *) - simpl. econstructor; split. - eapply exec_function_internal; eauto. - constructor; auto. unfold reach. constructor. + - simpl. econstructor; split. + eapply exec_function_internal; eauto. + constructor; auto. unfold reach. constructor. (* external function *) - econstructor; split. - eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - constructor; auto. + - econstructor; split. + eapply exec_function_external; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor; auto. (* return *) - inv STACKS. inv H1. - econstructor; split. - eapply exec_return; eauto. - constructor; auto. + - inv STACKS. inv H1. + econstructor; split. + eapply exec_return; eauto. + constructor; auto. Qed. Lemma transf_initial_states: diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 39fc10fb..c8107ad6 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -427,51 +427,34 @@ Proof. - (* load *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - exploit eval_addressing_lessdef; eauto. - intros [a' [ADDR' ALD]]. - exploit Mem.loadv_extends; eauto. - intros [v' [LOAD' VLD]]. - left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. - eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. - apply eval_addressing_preserved. exact symbols_preserved. eauto. - econstructor; eauto. apply set_reg_lessdef; auto. - -- (* load notrap1 *) - TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - left. - exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. - eapply exec_Iload_notrap1. - eassumption. - eapply eval_addressing_lessdef_none. eassumption. - erewrite eval_addressing_preserved. - eassumption. exact symbols_preserved. - - econstructor; eauto. apply set_reg_lessdef; auto. - -- (* load notrap2 *) - TransfInstr. - assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. - left. - - exploit eval_addressing_lessdef; eauto. - intros [a' [ADDR' ALD]]. - - destruct (Mem.loadv chunk m' a') eqn:Echunk2. - + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v) m'); split. - eapply exec_Iload with (a:=a'). eassumption. - erewrite eval_addressing_preserved. - eassumption. - exact symbols_preserved. - assumption. - econstructor; eauto. apply set_reg_lessdef; auto. - + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. - eapply exec_Iload_notrap2. eassumption. - erewrite eval_addressing_preserved. - eassumption. - exact symbols_preserved. - assumption. - econstructor; eauto. apply set_reg_lessdef; auto. + inv H0. + + exploit eval_addressing_lessdef; eauto. + intros [a' [EVAL' ALD]]. + exploit Mem.loadv_extends; eauto. + intros [v' [LOAD' VLD]]. + left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. + * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + rewrite <- EVAL'. apply eval_addressing_preserved. exact symbols_preserved. + * econstructor; eauto. apply set_reg_lessdef; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * left. exploit eval_addressing_lessdef; eauto. + intros [a' [EVAL' ALD]]. specialize (LOAD v). + destruct (Mem.loadv chunk m' a') eqn:Echunk2. + -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v0) m'); split. + ++ eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + erewrite eval_addressing_preserved; eauto. exact symbols_preserved. + ++ econstructor; eauto. apply set_reg_lessdef; auto. + -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. + ++ eapply exec_Iload; eauto. eapply has_loaded_default; intuition. + erewrite (eval_addressing_preserved ge tge) in H2; [ idtac | exact symbols_preserved]. + rewrite EVAL' in H2; inv H2. assumption. + ++ econstructor; eauto. apply set_reg_lessdef; auto. + * left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. + -- eapply exec_Iload; eauto. apply has_loaded_default; auto; intros. + eapply eval_addressing_lessdef_none in EVAL; eauto. + erewrite (eval_addressing_preserved ge tge) in H0; [ idtac | exact symbols_preserved]. + congruence. + -- econstructor; eauto. apply set_reg_lessdef; auto. - (* store *) TransfInstr. diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v index aaacf9d1..b9d73a42 100644 --- a/backend/Unusedglobproof.v +++ b/backend/Unusedglobproof.v @@ -910,50 +910,52 @@ Proof. econstructor; eauto. apply set_reg_inject; auto. - (* load *) - assert (A: exists ta, - eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta - /\ Val.inject j a ta). - { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). - intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. - apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto. - econstructor; eauto. - apply regs_inject; auto. - assumption. } - destruct A as (ta & B & C). - exploit Mem.loadv_inject; eauto. intros (tv & D & E). - econstructor; split. eapply exec_Iload; eauto. - econstructor; eauto. apply set_reg_inject; auto. - -- (* load notrap1 *) - assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None). - { eapply eval_addressing_inj_none. - intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. - apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. - econstructor; eauto. - rewrite Ptrofs.add_zero; reflexivity. - apply regs_inject; auto. - eassumption. - assumption. } - - econstructor; split. eapply exec_Iload_notrap1; eauto. - econstructor; eauto. apply set_reg_inject; auto. - -- (* load notrap2 *) - assert (A: exists ta, - eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta - /\ Val.inject j a ta). - { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). - intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. - apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. - econstructor; eauto. - apply regs_inject; auto. - assumption. } - destruct A as (ta & B & C). - destruct (Mem.loadv chunk tm ta) eqn:Echunk2. - + econstructor; split. eapply exec_Iload; eauto. - econstructor; eauto. apply set_reg_inject; auto. - + econstructor; split. eapply exec_Iload_notrap2; eauto. + inv H0. + + assert (A: exists ta, + eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta + /\ Val.inject j a ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + exploit Mem.loadv_inject; eauto. intros (tv & D & E). + econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. econstructor; eauto. apply set_reg_inject; auto. + + destruct (eval_addressing) eqn:EVAL in LOAD. + * specialize (LOAD v). + assert (A: exists ta, + eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta + /\ Val.inject j v ta). + { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args). + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + apply regs_inject; auto. + assumption. } + destruct A as (ta & B & C). + destruct (Mem.loadv chunk tm ta) eqn:Echunk2. + ** econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. + econstructor; eauto. apply set_reg_inject; auto. + ** econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite B in EVAL'; inv EVAL'. auto. + econstructor; eauto. apply set_reg_inject; auto. + * assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None). + { eapply eval_addressing_inj_none. + intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto. + apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto. + econstructor; eauto. + rewrite Ptrofs.add_zero; reflexivity. + apply regs_inject; auto. + eassumption. + assumption. } + + econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_default; eauto. + intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. + econstructor; eauto. apply set_reg_inject; auto. + - (* store *) assert (A: exists ta, eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index e20edff7..c112d69e 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -1272,7 +1272,7 @@ Proof. apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va. - (* load *) - destruct trap. + destruct trap; inv H0. + eapply sound_succ_state; eauto. simpl; auto. unfold transfer; rewrite H. eauto. apply ematch_update; auto. eapply loadv_sound; eauto with va. @@ -1283,16 +1283,9 @@ Proof. eapply vmatch_top. eapply loadv_sound; try eassumption. eapply eval_static_addressing_sound; eauto with va. -- (* load notrap1 *) - eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H. eauto. - apply ematch_update; auto. - constructor. -- (* load notrap2 *) - eapply sound_succ_state; eauto. simpl; auto. - unfold transfer; rewrite H. eauto. - apply ematch_update; auto. - constructor. + + eapply sound_succ_state; eauto. simpl; auto. + unfold transfer; rewrite H. eauto. + apply ematch_update; auto. econstructor. - (* store *) exploit eval_static_addressing_sound; eauto with va. intros VMADDR. eapply sound_succ_state; eauto. simpl; auto. -- cgit From 5530915001c3e8b395d731480e5a6618a08af7af Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 10:57:22 +0100 Subject: being more archi-independant --- backend/Deadcodeproof.v | 11 ++++------- backend/Duplicateproof.v | 2 +- backend/Inliningproof.v | 4 ++-- backend/ProfilingExploitproof.v | 4 ++-- backend/RTLTunnelingproof.v | 4 ++-- backend/RTLgenproof.v | 4 ++-- backend/Renumberproof.v | 4 ++-- backend/Tailcallproof.v | 8 ++++---- 8 files changed, 19 insertions(+), 22 deletions(-) (limited to 'backend') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 305e8eeb..be64a1a7 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -822,9 +822,8 @@ Ltac UseTransfer := intros. apply nlive_add with bc i; assumption. intros (tv & P & Q). econstructor; split. - eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. - eauto. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | eauto]). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -851,10 +850,8 @@ Ltac UseTransfer := destruct (Mem.loadv chunk tm ta) eqn:Hchunk2. { econstructor; split. - eapply exec_Iload. eauto. eapply has_loaded_normal; eauto. - erewrite eval_addressing_preserved with (ge1 := ge). - assumption. - exact symbols_preserved. + try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index c4270e46..5752f5d2 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -416,7 +416,7 @@ Proof. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. inv H0. + eexists; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved; eauto. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; erewrite eval_addressing_preserved; eauto). * econstructor; eauto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). eexists; split. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index a4bf838e..647938f3 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -992,8 +992,8 @@ Proof. fold (saddr ctx addr). intros [a' [P Q]]. destruct (Mem.loadv chunk m' a') eqn:Hload'. -- left; econstructor; split. - ++ eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). + ++ eapply plus_one. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved). ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. -- left; econstructor; split. diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v index 292acc2a..4308b670 100644 --- a/backend/ProfilingExploitproof.v +++ b/backend/ProfilingExploitproof.v @@ -128,8 +128,8 @@ Proof. (* load *) - inv H0. + econstructor; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved). * econstructor; eauto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). econstructor; split. diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v index 2cef08e2..aa21fc06 100644 --- a/backend/RTLTunnelingproof.v +++ b/backend/RTLTunnelingproof.v @@ -461,7 +461,7 @@ Proof. left. eexists. split. * eapply exec_Iload. -- exploit instruction_type_preserved; (simpl; eauto)||congruence. - -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved. + -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved). * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). @@ -473,7 +473,7 @@ Proof. -- left; eexists; split. eapply exec_Iload. ++ exploit instruction_type_preserved; (simpl; eauto)||congruence. - ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved. + ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved). ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto. -- left; eexists; split. eapply exec_Iload. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 59d0a451..2b1349d2 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -586,8 +586,8 @@ Proof. exists (rs1#rd <- v'); exists tm1. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iload. eauto. - econstructor; eauto. rewrite <- H3. - apply eval_addressing_preserved. exact symbols_preserved. + econstructor; eauto. try (rewrite <- H3; + apply eval_addressing_preserved; exact symbols_preserved). auto. (* Match-env *) split. eauto with rtlg. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 7c7bc7e3..cd3efe73 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -172,8 +172,8 @@ Proof. (* load *) - inv H0. + econstructor; split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved). * econstructor; eauto. eapply reach_succ; eauto. simpl; auto. + destruct (eval_addressing) eqn:EVAL in LOAD. * specialize (LOAD v). econstructor; split. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index c8107ad6..4eb0ba23 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -433,16 +433,16 @@ Proof. exploit Mem.loadv_extends; eauto. intros [v' [LOAD' VLD]]. left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. - * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - rewrite <- EVAL'. apply eval_addressing_preserved. exact symbols_preserved. + * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + rewrite <- EVAL'; apply eval_addressing_preserved; exact symbols_preserved). * econstructor; eauto. apply set_reg_lessdef; auto. + destruct (eval_addressing) eqn:EVAL in LOAD. * left. exploit eval_addressing_lessdef; eauto. intros [a' [EVAL' ALD]]. specialize (LOAD v). destruct (Mem.loadv chunk m' a') eqn:Echunk2. -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v0) m'); split. - ++ eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. - erewrite eval_addressing_preserved; eauto. exact symbols_preserved. + ++ try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; + erewrite eval_addressing_preserved; eauto; exact symbols_preserved). ++ econstructor; eauto. apply set_reg_lessdef; auto. -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. ++ eapply exec_Iload; eauto. eapply has_loaded_default; intuition. -- cgit From 98ec44d9d96e7e94896eea9ac054a0188be7b6dd Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Nov 2021 11:17:10 +0100 Subject: bugfix --- backend/Deadcodeproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index be64a1a7..52332a82 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -823,7 +823,7 @@ Ltac UseTransfer := intros (tv & P & Q). econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | eauto]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -851,7 +851,7 @@ Ltac UseTransfer := { econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. -- cgit