Model external calls as destroying all caller-save registers

The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.

Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.

8 files changed, 79 insertions, 8 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 585fb0da..068e0de0 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2476,7 +2476,8 @@ 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).
-  symmetry; apply Locmap.gpo.
+  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.
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index f6f03868..70c4323c 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -316,6 +316,23 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
diff --git a/backend/LTL.v b/backend/LTL.v
index 8567a891..6dd1abd6 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -106,6 +106,17 @@ Definition return_regs (caller callee: locset) : locset :=
     | 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]. *)
+
+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 sl ofs ty => ls (S sl ofs ty)
+    end.
+
 (** LTL execution states. *)
 
 Inductive stackframe : Type :=
@@ -259,7 +270,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external: forall s ef t args res rs m rs' m',
       args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) ->
       external_call ef ge args m t res m' ->
-      rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs ->
+      rs' = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
       step (Callstate s (External ef) rs m)
          t (Returnstate s rs' m')
   | exec_return: forall f sp rs1 bb s rs m,
diff --git a/backend/Linear.v b/backend/Linear.v
index 55f92d16..447c6ba6 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -239,7 +239,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s ef args res rs1 rs2 m t m',
       args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) ->
       external_call ef ge args m t res m' ->
-      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 ->
+      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs1) ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m')
   | exec_return:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 30cc0d91..fd252dc6 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -149,6 +149,14 @@ Proof.
   unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto.
 Qed.
 
+Lemma wt_undef_caller_save_regs:
+  forall ls, wt_locset ls -> wt_locset (undef_caller_save_regs ls).
+Proof.
+  intros; red; intros. unfold undef_caller_save_regs.
+  destruct l; auto.
+  destruct (is_callee_save r); auto; simpl; auto. 
+Qed.
+
 Lemma wt_init:
   wt_locset (Locmap.init Vundef).
 Proof.
@@ -339,8 +347,9 @@ Local Opaque mreg_type.
   econstructor. eauto. eauto. eauto.
   apply wt_undef_regs. apply wt_call_regs. auto.
 - (* external function *)
-  econstructor. auto. apply wt_setpair; auto.
+  econstructor. auto. apply wt_setpair. 
   eapply external_call_well_typed; eauto.
+  apply wt_undef_caller_save_regs; auto.
 - (* return *)
   inv WTSTK. econstructor; eauto.
 Qed.
diff --git a/backend/Mach.v b/backend/Mach.v
index 839a25bd..9fdee9eb 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -156,6 +156,9 @@ Proof.
   unfold Regmap.set. destruct (RegEq.eq r a); auto.
 Qed.
 
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r => if is_callee_save r then rs r else Vundef.
+
 Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset :=
   match p with
   | One r => rs#r <- v
@@ -407,7 +410,7 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge fb = Some (External ef) ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
       external_call ef ge args m t res m' ->
-      rs' = set_pair (loc_result (ef_sig ef)) res rs ->
+      rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
       step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index f7570f57..5dbc4532 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -666,6 +666,16 @@ Proof.
   apply agree_regs_set_reg; auto.
 Qed.
 
+Lemma agree_regs_undef_caller_save_regs:
+  forall j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs).
+Proof.
+  intros; red; intros. 
+  unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. 
+  destruct (is_callee_save r); auto. 
+Qed.
+
 (** Preservation under assignment of stack slot *)
 
 Lemma agree_regs_set_slot:
@@ -826,6 +836,16 @@ Proof.
   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 ->
@@ -2113,8 +2133,10 @@ Proof.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_states_return with (j := j').
   eapply match_stacks_change_meminj; eauto.
-  apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
-  apply agree_callee_save_set_result; auto.
+  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.
 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index c6644ceb..fd97ce33 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -334,6 +334,14 @@ Proof.
   induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
 Qed.
 
+Lemma locmap_undef_caller_save_regs_lessdef:
+  forall ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2).
+Proof.
+  intros; red; intros. unfold undef_caller_save_regs. 
+  destruct l; auto. destruct (Conventions1.is_callee_save r); auto.
+Qed.
+
 Lemma find_function_translated:
   forall ros ls tls fd,
   locmap_lessdef ls tls ->
@@ -516,7 +524,7 @@ Proof.
   left; simpl; econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  simpl. econstructor; eauto using locmap_setpair_lessdef.
+  simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef.
 - (* return *)
   inv STK. inv H1.
   left; econstructor; split.