diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 18:20:31 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 18:20:31 +0200 |
| commit | 6fa6e763ba241da7eeb8bd309344a118c6b1ec4a (patch) | |
| tree | f85f36cf5688ceee1315dd918a55514f921e5314 | |
| parent | 7df2b7d824f3187f1936685629c06d1028fdc243 (diff) | |
| download | compcert-kvx-6fa6e763ba241da7eeb8bd309344a118c6b1ec4a.tar.gz compcert-kvx-6fa6e763ba241da7eeb8bd309344a118c6b1ec4a.zip | |
finished the proofs for non-trapping loads
| -rw-r--r-- | backend/Allocproof.v | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index ab6f87b0..3d8fb451 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2260,25 +2260,36 @@ Proof. eapply wt_exec_Iload_notrap; eauto. (* load regular notrap2 *) -- (* exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. +- 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]]. - - econstructor; split. + 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. eapply exec_Lload_notrap2 with (a := a'). rewrite <- F. + 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. - - generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS). intro WTRS'. - *) + } + { 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. + } - admit. - - (* load notrap2 dead *) exploit exec_moves; eauto. intros [ls1 [X Y]]. econstructor; split. @@ -2542,7 +2553,7 @@ Proof. eapply plus_left. constructor. eexact A. traceEq. econstructor; eauto. apply wt_regset_assign; auto. rewrite WTRES0; auto. -Admitted. +Qed. Lemma initial_states_simulation: forall st1, RTL.initial_state prog st1 -> |