diff options
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 161 |
1 files changed, 96 insertions, 65 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 73feccf0..2b9b71dc 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -960,32 +960,95 @@ 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. + destruct trap. + { (* TRAP *) + 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. { - rewrite find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs) in H1; trivial. - rewrite MAP in H0. - assumption. + 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. + { + rewrite find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs) in H1; trivial. + rewrite MAP in H0. + assumption. + } + 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)). + { + 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_sound with (a := a); auto. } - constructor; eauto. + { + 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 apply_instr'. + rewrite H. + rewrite MPC. + simpl. + reflexivity. + } + apply load_sound with (a := a); assumption. + } + } + + { (* NOTRAP *) + 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 *. - rewrite MAP. - apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)). + 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 (kill_reg dst mpc)). { - replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_reg 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. @@ -997,55 +1060,24 @@ Proof. 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 apply_instr'. - rewrite H. - rewrite MPC. - simpl. - reflexivity. - } - apply load_sound with (a := a); assumption. + apply kill_reg_sound; assumption. } - (* NOT IN THIS VERSION - (* 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. + rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption. constructor; auto. simpl in *. - unfold fmap_sem 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 (kill dst mpc)). + apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)). { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_reg 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. @@ -1054,26 +1086,26 @@ Proof. unfold apply_instr'. rewrite H. rewrite MPC. + simpl. reflexivity. } - apply kill_ok. - assumption. + apply kill_reg_sound; 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. + rewrite subst_args_ok with (genv := ge) (sp := sp) (m := m); assumption. constructor; auto. simpl in *. - unfold fmap_sem 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 (kill dst mpc)). + apply sem_rel_b_ge with (rb2 := Some (kill_reg dst mpc)). { - replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)). + replace (Some (kill_reg 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. @@ -1082,11 +1114,10 @@ Proof. unfold apply_instr'. rewrite H. rewrite MPC. + simpl. reflexivity. } - apply kill_ok. - assumption. - *) + apply kill_reg_sound; assumption. - (* store *) econstructor. split. |