From 7a5aef7aa4b669a722ecce3da6e7f7c646a392cc Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 17 Jun 2018 17:48:01 +0200 Subject: Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237) * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof. --- backend/Allocproof.v | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 068e0de0..1804f46b 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1317,15 +1317,6 @@ Proof. eauto. Qed. -Definition callee_save_loc (l: loc) := - match l with - | R r => is_callee_save r = true - | S sl ofs ty => sl <> Outgoing - end. - -Definition agree_callee_save (ls1 ls2: locset) : Prop := - forall l, callee_save_loc l -> ls1 l = ls2 l. - Lemma return_regs_agree_callee_save: forall caller callee, agree_callee_save caller (return_regs caller callee). @@ -2476,11 +2467,10 @@ 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). - 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. + rewrite locmap_get_set_loc_result_callee_save by auto. + unfold undef_caller_save_regs. destruct l; simpl in H0. + rewrite H0; auto. + destruct sl; auto; congruence. eapply external_call_well_typed; eauto. (* return *) -- cgit