diff options
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 382 |
1 files changed, 191 insertions, 191 deletions
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. |