diff options
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. |