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, 19 insertions, 69 deletions

diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 5dbc4532..ffd9b227 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -294,12 +294,13 @@ Qed.
 
 Lemma contains_locations_exten:
   forall ls ls' j sp pos bound sl,
-  (forall ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) ->
+  (forall ofs ty, Val.lessdef (ls' (S sl ofs ty)) (ls (S sl ofs ty))) ->
   massert_imp (contains_locations j sp pos bound sl ls)
               (contains_locations j sp pos bound sl ls').
 Proof.
   intros; split; simpl; intros; auto.
-  intuition auto. rewrite H. eauto.
+  intuition auto. exploit H5; eauto. intros (v & A & B). exists v; split; auto. 
+  specialize (H ofs ty). inv H. congruence. auto. 
 Qed.
 
 Lemma contains_locations_incr:
@@ -481,7 +482,8 @@ Qed.
 
 Lemma frame_contents_exten:
   forall ls ls0 ls' ls0' j sp parent retaddr P m,
-  (forall sl ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) ->
+  (forall ofs ty, Val.lessdef (ls' (S Local ofs ty)) (ls (S Local ofs ty))) ->
+  (forall ofs ty, Val.lessdef (ls' (S Outgoing ofs ty)) (ls (S Outgoing ofs ty))) ->
   (forall r, In r b.(used_callee_save) -> ls0' (R r) = ls0 (R r)) ->
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
   m |= frame_contents j sp ls' ls0' parent retaddr ** P.
@@ -573,16 +575,6 @@ Record agree_locs (ls ls0: locset) : Prop :=
        ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty)
 }.
 
-(** Auxiliary predicate used at call points *)
-
-Definition agree_callee_save (ls ls0: locset) : Prop :=
-  forall l,
-  match l with
-  | R r => is_callee_save r = true
-  | S _ _ _ => True
-  end ->
-  ls l = ls0 l.
-
 (** ** Properties of [agree_regs]. *)
 
 (** Values of registers *)
@@ -810,51 +802,7 @@ Lemma agree_locs_return:
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
 - rewrite H0; auto. unfold mreg_within_bounds in H. tauto.
-- rewrite H0; auto.
-Qed.
-
-(** Preservation at tailcalls (when [ls0] is changed but not [ls]). *)
-
-Lemma agree_locs_tailcall:
-  forall ls ls0 ls0',
-  agree_locs ls ls0 ->
-  agree_callee_save ls0 ls0' ->
-  agree_locs ls ls0'.
-Proof.
-  intros. red in H0. inv H; constructor; auto; intros.
-- rewrite <- H0; auto. unfold mreg_within_bounds in H. tauto.
-- rewrite <- H0; auto.
-Qed.
-
-(** ** Properties of [agree_callee_save]. *)
-
-Lemma agree_callee_save_return_regs:
-  forall ls1 ls2,
-  agree_callee_save (return_regs ls1 ls2) ls1.
-Proof.
-  intros; red; intros.
-  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 ->
-  agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2.
-Proof.
-  intros; red; intros. rewrite Locmap.gpo. apply H; auto.
-  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
-  { intros. destruct l; auto. simpl; congruence. }
-  generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto.
+- rewrite <- agree_incoming0 by auto. apply H0. congruence.
 Qed.
 
 (** ** Properties of destroyed registers. *)
@@ -1091,6 +1039,7 @@ Lemma function_prologue_correct:
   forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k P,
   agree_regs j ls rs ->
   agree_callee_save ls ls0 ->
+  agree_outgoing_arguments (Linear.fn_sig f) ls ls0 ->
   (forall r, Val.has_type (ls (R r)) (mreg_type r)) ->
   ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
   rs1 = undef_regs destroyed_at_function_entry rs ->
@@ -1110,7 +1059,7 @@ Lemma function_prologue_correct:
   /\ j' sp = Some(sp', fe.(fe_stack_data))
   /\ inject_incr j j'.
 Proof.
-  intros until P; intros AGREGS AGCS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP.
+  intros until P; intros AGREGS AGCS AGARGS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP.
   rewrite unfold_transf_function.
   unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs.
   (* Stack layout info *)
@@ -1194,7 +1143,7 @@ Local Opaque b fe.
   split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity].
     constructor; intros. unfold call_regs. apply AGCS.
     unfold mreg_within_bounds in H; tauto.
-    unfold call_regs. apply AGCS. auto.
+    unfold call_regs. apply AGARGS. apply incoming_slot_in_parameters; auto.
   split. exact SEPFINAL.
   split. exact SAME. exact INCR.
 Qed.
@@ -1345,7 +1294,7 @@ Proof.
     apply CS; auto.
     rewrite NCS by auto. apply AGR.
   split. red; unfold return_regs; intros.
-    destruct l; auto. rewrite H; auto.
+    destruct l. rewrite H; auto. destruct sl; auto; contradiction. 
   assumption.
 Qed.
 
@@ -1639,6 +1588,7 @@ Variable ls: locset.
 Variable rs: regset.
 Hypothesis AGR: agree_regs j ls rs.
 Hypothesis AGCS: agree_callee_save ls (parent_locset cs).
+Hypothesis AGARGS: agree_outgoing_arguments sg ls (parent_locset cs).
 Variable m': mem.
 Hypothesis SEP: m' |= stack_contents j cs cs'.
 
@@ -1661,7 +1611,7 @@ Proof.
   assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto.
   exploit frame_get_outgoing; eauto. intros (v & A & B).
   exists v; split.
-  constructor. exact A. red in AGCS. rewrite AGCS; auto.
+  constructor. exact A. rewrite AGARGS by auto. exact B. 
 Qed.
 
 Lemma transl_external_argument_2:
@@ -1836,7 +1786,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (TRANSL: transf_fundef f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some tf)
         (AGREGS: agree_regs j ls rs)
-        (AGLOCS: agree_callee_save ls (parent_locset cs))
         (SEP: m' |= stack_contents j cs cs'
                  ** minjection j m
                  ** globalenv_inject ge j),
@@ -1846,7 +1795,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
       forall cs ls m cs' rs m' j sg
         (STACKS: match_stacks j cs cs' sg)
         (AGREGS: agree_regs j ls rs)
-        (AGLOCS: agree_callee_save ls (parent_locset cs))
         (SEP: m' |= stack_contents j cs cs'
                  ** minjection j m
                  ** globalenv_inject ge j),
@@ -2004,9 +1952,8 @@ Proof.
   econstructor; eauto with coqlib.
   apply Val.Vptr_has_type.
   intros; red.
-    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto.
+    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. 
     apply loc_arguments_bounded; auto.
-  simpl; red; auto.
   simpl. rewrite sep_assoc. exact SEP.
 
 - (* Ltailcall *)
@@ -2106,6 +2053,7 @@ Proof.
   destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence.
   intros EQ; inversion EQ; clear EQ; subst tf.
   rewrite sep_comm, sep_assoc in SEP.
+  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
   exploit function_prologue_correct; eauto.
   red; intros; eapply wt_callstate_wt_regs; eauto.
   eapply match_stacks_type_sp; eauto.
@@ -2124,6 +2072,7 @@ Proof.
 
 - (* external function *)
   simpl in TRANSL. inversion TRANSL; subst tf.
+  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
   exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]].
   rewrite sep_comm, sep_assoc in SEP.
   exploit external_call_parallel_rule; eauto.
@@ -2136,17 +2085,19 @@ Proof.
   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.
 
 - (* return *)
-  inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP.
+  inv STACKS. exploit wt_returnstate_agree; eauto. intros [AGCS OUTU].
+  simpl in AGCS. simpl in SEP. rewrite sep_assoc in SEP.
   econstructor; split.
   apply plus_one. apply exec_return.
   econstructor; eauto.
   apply agree_locs_return with rs0; auto.
   apply frame_contents_exten with rs0 (parent_locset s); auto.
+  intros; apply Val.lessdef_same; apply AGCS; red; congruence.
+  intros; rewrite (OUTU ty ofs); auto. 
 Qed.
 
 Lemma transf_initial_states:
@@ -2164,7 +2115,6 @@ Proof.
   eapply match_states_call with (j := j); eauto.
   constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction.
   red; simpl; auto.
-  red; simpl; auto.
   simpl. rewrite sep_pure. split; auto. split;[|split].
   eapply Genv.initmem_inject; eauto.
   simpl. exists (Mem.nextblock m0); split. apply Ple_refl.