diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 3 | ||||
| -rw-r--r-- | backend/Asmgenproof0.v | 17 | ||||
| -rw-r--r-- | backend/LTL.v | 13 | ||||
| -rw-r--r-- | backend/Linear.v | 2 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 11 | ||||
| -rw-r--r-- | backend/Mach.v | 5 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 26 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 10 |
8 files changed, 79 insertions, 8 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 585fb0da..068e0de0 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2476,7 +2476,8 @@ Proof. rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss. rewrite val_longofwords_eq_1 by auto. auto. red; intros. rewrite (AG l H0). - symmetry; apply Locmap.gpo. + rewrite Locmap.gpo. + unfold undef_caller_save_regs. destruct l; auto. simpl in H0; rewrite H0; auto. assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). { intros. destruct l; simpl in *. congruence. auto. } generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index f6f03868..70c4323c 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -316,6 +316,23 @@ Proof. intros. rewrite Pregmap.gso; auto. Qed. +Lemma agree_undef_caller_save_regs: + forall ms sp rs, + agree ms sp rs -> + agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs). +Proof. + intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split. +- unfold proj_sumbool; rewrite dec_eq_true. auto. +- auto. +- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. ++ apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. ++ destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. +Qed. + Lemma agree_change_sp: forall ms sp rs sp', agree ms sp rs -> sp' <> Vundef -> diff --git a/backend/LTL.v b/backend/LTL.v index 8567a891..6dd1abd6 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -106,6 +106,17 @@ Definition return_regs (caller callee: locset) : locset := | S sl ofs ty => caller (S sl ofs ty) end. +(** [undef_caller_save_regs ls] models the effect of calling + an external function: caller-save registers can change unpredictably, + hence we set them to [Vundef]. *) + +Definition undef_caller_save_regs (ls: locset) : locset := + fun (l: loc) => + match l with + | R r => if is_callee_save r then ls (R r) else Vundef + | S sl ofs ty => ls (S sl ofs ty) + end. + (** LTL execution states. *) Inductive stackframe : Type := @@ -259,7 +270,7 @@ Inductive step: state -> trace -> state -> Prop := | exec_function_external: forall s ef t args res rs m rs' m', args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs -> + rs' = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> step (Callstate s (External ef) rs m) t (Returnstate s rs' m') | exec_return: forall f sp rs1 bb s rs m, diff --git a/backend/Linear.v b/backend/Linear.v index 55f92d16..447c6ba6 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -239,7 +239,7 @@ Inductive step: state -> trace -> state -> Prop := forall s ef args res rs1 rs2 m t m', args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) -> external_call ef ge args m t res m' -> - rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 -> + rs2 = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs1) -> step (Callstate s (External ef) rs1 m) t (Returnstate s rs2 m') | exec_return: diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 30cc0d91..fd252dc6 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -149,6 +149,14 @@ Proof. unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto. Qed. +Lemma wt_undef_caller_save_regs: + forall ls, wt_locset ls -> wt_locset (undef_caller_save_regs ls). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. + destruct (is_callee_save r); auto; simpl; auto. +Qed. + Lemma wt_init: wt_locset (Locmap.init Vundef). Proof. @@ -339,8 +347,9 @@ Local Opaque mreg_type. econstructor. eauto. eauto. eauto. apply wt_undef_regs. apply wt_call_regs. auto. - (* external function *) - econstructor. auto. apply wt_setpair; auto. + econstructor. auto. apply wt_setpair. eapply external_call_well_typed; eauto. + apply wt_undef_caller_save_regs; auto. - (* return *) inv WTSTK. econstructor; eauto. Qed. diff --git a/backend/Mach.v b/backend/Mach.v index 839a25bd..9fdee9eb 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -156,6 +156,9 @@ Proof. unfold Regmap.set. destruct (RegEq.eq r a); auto. Qed. +Definition undef_caller_save_regs (rs: regset) : regset := + fun r => if is_callee_save r then rs r else Vundef. + Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset := match p with | One r => rs#r <- v @@ -407,7 +410,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge fb = Some (External ef) -> extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> external_call ef ge args m t res m' -> - rs' = set_pair (loc_result (ef_sig ef)) res rs -> + rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> step (Callstate s fb rs m) t (Returnstate s rs' m') | exec_return: diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index f7570f57..5dbc4532 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -666,6 +666,16 @@ Proof. apply agree_regs_set_reg; auto. Qed. +Lemma agree_regs_undef_caller_save_regs: + forall j ls rs, + agree_regs j ls rs -> + agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs). +Proof. + intros; red; intros. + unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. + destruct (is_callee_save r); auto. +Qed. + (** Preservation under assignment of stack slot *) Lemma agree_regs_set_slot: @@ -826,6 +836,16 @@ Proof. unfold return_regs. destruct l; auto. rewrite H; auto. Qed. +Lemma agree_callee_save_undef_caller_save_regs: + forall ls1 ls2, + agree_callee_save ls1 ls2 -> + agree_callee_save (LTL.undef_caller_save_regs ls1) ls2. +Proof. + intros; red; intros. unfold LTL.undef_caller_save_regs. + destruct l; auto. + rewrite H0; auto. +Qed. + Lemma agree_callee_save_set_result: forall sg v ls1 ls2, agree_callee_save ls1 ls2 -> @@ -2113,8 +2133,10 @@ Proof. eapply external_call_symbols_preserved; eauto. apply senv_preserved. eapply match_states_return with (j := j'). eapply match_stacks_change_meminj; eauto. - apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto. - apply agree_callee_save_set_result; auto. + apply agree_regs_set_pair. apply agree_regs_undef_caller_save_regs. + apply agree_regs_inject_incr with j; auto. + auto. + apply agree_callee_save_set_result. apply agree_callee_save_undef_caller_save_regs. auto. apply stack_contents_change_meminj with j; auto. rewrite sep_comm, sep_assoc; auto. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c6644ceb..fd97ce33 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -334,6 +334,14 @@ Proof. induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef. Qed. +Lemma locmap_undef_caller_save_regs_lessdef: + forall ls1 ls2, + locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l; auto. destruct (Conventions1.is_callee_save r); auto. +Qed. + Lemma find_function_translated: forall ros ls tls fd, locmap_lessdef ls tls -> @@ -516,7 +524,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - simpl. econstructor; eauto using locmap_setpair_lessdef. + simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef. - (* return *) inv STK. inv H1. left; econstructor; split. |