diff options
author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 16:25:58 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 16:25:58 +0100 |
commit | 17b1ec4333af8120ab6867baf9c5c9139541c6b7 (patch) | |
tree | 71bd521b6603820c81217ebc10a24fcd940f110a /backend/ForwardMovesproof.v | |
parent | e9dc339d5e5ec129dcf6b541d6c70f9ca7fe134c (diff) | |
parent | 98ec44d9d96e7e94896eea9ac054a0188be7b6dd (diff) | |
download | compcert-kvx-17b1ec4333af8120ab6867baf9c5c9139541c6b7.tar.gz compcert-kvx-17b1ec4333af8120ab6867baf9c5c9139541c6b7.zip |
Merge branch 'RTL_has_loaded' into kvx-work
Diffstat (limited to 'backend/ForwardMovesproof.v')
-rw-r--r-- | backend/ForwardMovesproof.v | 160 |
1 files changed, 80 insertions, 80 deletions
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. |