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.

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.