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/LTL.v | |
| parent | 3d348f51e343ff84b8e550fbeb905e23bf2b6175 (diff) | |
| download | compcert-kvx-7a5aef7aa4b669a722ecce3da6e7f7c646a392cc.tar.gz compcert-kvx-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/LTL.v')
| -rw-r--r-- | backend/LTL.v | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/backend/LTL.v b/backend/LTL.v index 6dd1abd6..5e7eec8c 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -96,24 +96,28 @@ Definition call_regs (caller: locset) : locset := - Callee-save machine registers have the same values as in the caller before the call. - Caller-save machine registers have the same values as in the callee. -- Stack slots have the same values as in the caller. +- Local and Incoming stack slots have the same values as in the caller. +- Outgoing stack slots are set to Vundef to reflect the fact that they + may have been changed by the callee. *) Definition return_regs (caller callee: locset) : locset := fun (l: loc) => match l with | R r => if is_callee_save r then caller (R r) else callee (R r) + | S Outgoing ofs ty => Vundef | 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]. *) + an external function: caller-save registers and outgoing locations + 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 Outgoing ofs ty => Vundef | S sl ofs ty => ls (S sl ofs ty) end. |