diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-06-17 17:48:01 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-17 17:48:01 +0200 |
commit | 7a5aef7aa4b669a722ecce3da6e7f7c646a392cc (patch) | |
tree | 5f50db9ea90cc8ca55551f364d972d134c3f9177 /backend/Conventions.v | |
parent | 3d348f51e343ff84b8e550fbeb905e23bf2b6175 (diff) | |
download | compcert-7a5aef7aa4b669a722ecce3da6e7f7c646a392cc.tar.gz compcert-7a5aef7aa4b669a722ecce3da6e7f7c646a392cc.zip |
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.
Diffstat (limited to 'backend/Conventions.v')
-rw-r--r-- | backend/Conventions.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/backend/Conventions.v b/backend/Conventions.v index bdc4c8b6..989bfa05 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -103,3 +103,56 @@ Proof. generalize (loc_arguments_bounded _ _ _ H0). generalize (typesize_pos ty). omega. Qed. + + +(** * Callee-save locations *) + +(** We classify locations as either +- callee-save, i.e. preserved across function calls: + callee-save registers, [Local] and [Incoming] stack slots; +- caller-save, i.e. possibly modified by a function call: + non-callee-save registers, [Outgoing] stack slots. + +Concerning [Outgoing] stack slots: several ABIs allow a function to modify +the stack slots used for passing parameters to this function. +The code currently generated by CompCert never does so, but the code +generated by other compilers often does so (e.g. GCC for x86-32). +Hence, CompCert-generated code must not assume that [Outgoing] stack slots +are preserved across function calls, because they might not be preserved +if the called function was compiled by another compiler. +*) + +Definition callee_save_loc (l: loc) := + match l with + | R r => is_callee_save r = true + | S sl ofs ty => sl <> Outgoing + end. + +Hint Unfold callee_save_loc. + +Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop := + forall l, callee_save_loc l -> ls1 l = ls2 l. + +(** * Assigning result locations *) + +(** Useful lemmas to reason about the result of an external call. *) + +Lemma locmap_get_set_loc_result: + forall sg v rs l, + match l with R r => is_callee_save r = true | S _ _ _ => True end -> + Locmap.setpair (loc_result sg) v rs l = rs l. +Proof. + intros. apply Locmap.gpo. + assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)). + { intros. destruct l; simpl. congruence. auto. } + generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto. +Qed. + +Lemma locmap_get_set_loc_result_callee_save: + forall sg v rs l, + callee_save_loc l -> + Locmap.setpair (loc_result sg) v rs l = rs l. +Proof. + intros. apply locmap_get_set_loc_result. + red in H; destruct l; auto. +Qed. |