Support re-normalization of values returned by function calls

Some ABIs leave more flexibility concerning function return values
than CompCert expects.

For example, the x86 ABI says that a function result of type "char" is
returned in register AL, leaving the top 24 bits of register EAX
unspecified, while CompCert expects EAX to contain 32 valid bits,
namely the zero- or sign-extension of the 8-bit result.

This commits adds a general mechanism to insert "re-normalization"
conversions on the results of function calls.  Currently, it only
deals with results of small integer types, and inserts zero- or
sign-extensions if so instructed by a platform-dependent function,
Convention1.return_value_needs_normalization.

The conversions in question are inserted early in the front-end, so
that they can be optimized away in the back-end.

The semantic preservation proof is still conducted against the
CompCert model, where the return values of functions are already
normalized.  What the proof shows is that the extra conversions have
no effect in this case.  In future work we could relax the CompCert model,
allowing functions to return values that are not normalized.

1 files changed, 104 insertions, 29 deletions

diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 09e31cb2..1ceb8e4d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -15,7 +15,7 @@
 Require Import Coqlib Errors Maps Integers Floats.
 Require Import AST Linking.
 Require Import Values Events Memory Globalenvs Smallstep.
-Require Import Ctypes Cop Clight Cminor Csharpminor.
+Require Import Ctypes Ctyping Cop Clight Cminor Csharpminor.
 Require Import Cshmgen.
 
 (** * Relational specification of the transformation *)
@@ -996,6 +996,26 @@ Proof.
   eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
 Qed.
 
+Lemma make_normalization_correct:
+  forall e le m a v t,
+  eval_expr ge e le m a v ->
+  wt_val v t ->
+  eval_expr ge e le m (make_normalization t a) v.
+Proof.
+  intros. destruct t; simpl; auto. inv H0.
+- destruct i; simpl in H3.
+  + destruct s; econstructor; eauto; simpl; congruence.
+  + destruct s; econstructor; eauto; simpl; congruence.
+  + auto.
+  + econstructor; eauto; simpl; congruence.
+- auto.
+- destruct i.
+  + destruct s; econstructor; eauto. 
+  + destruct s; econstructor; eauto.
+  + auto.
+  + econstructor; eauto.
+Qed.
+
 End CONSTRUCTORS.
 
 (** * Basic preservation invariants *)
@@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha
       match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
       match_cont ce tyret nbrk ncnt
                  (Clight.Kcall id f e le k)
-                 (Kcall id tf te le tk).
+                 (Kcall id tf te le tk)
+  | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu,
+      linkorder cu prog ->
+      transl_function cu.(prog_comp_env) f = OK tf ->
+      match_env e te ->
+      match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
+      (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) ->
+      match_cont ce tyret nbrk ncnt
+                 (Clight.Kcall (Some id) f e le k)
+                 (Kcall (Some id) tf te le (Kseq (Sset id a) tk)).
 
 Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
   | match_state:
@@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
       forall fd args k m tfd tk targs tres cconv cu ce
           (LINK: linkorder cu prog)
           (TR: match_fundef cu fd tfd)
-          (MK: match_cont ce Tvoid 0%nat 0%nat k tk)
+          (MK: match_cont ce tres 0%nat 0%nat k tk)
           (ISCC: Clight.is_call_cont k)
           (TY: type_of_fundef fd = Tfunction targs tres cconv),
       match_states (Clight.Callstate fd args k m)
                    (Callstate tfd args tk m)
   | match_returnstate:
-      forall res k m tk ce
-          (MK: match_cont ce Tvoid 0%nat 0%nat k tk),
+      forall res tres k m tk ce
+          (MK: match_cont ce tres 0%nat 0%nat k tk)
+          (WT: wt_val res tres),
       match_states (Clight.Returnstate res k m)
                    (Returnstate res tk m).
 
@@ -1442,7 +1472,9 @@ Proof.
 - (* set *)
   auto.
 - (* call *)
-  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto.
+  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
+  unfold make_funcall.
+  destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto.
 - (* builtin *)
   auto.
 - (* seq *)
@@ -1500,24 +1532,26 @@ End FIND_LABEL.
 (** Properties of call continuations *)
 
 Lemma match_cont_call_cont:
-  forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk,
+  forall ce' nbrk' ncnt' ce tyret nbrk ncnt k tk,
   match_cont ce tyret nbrk ncnt k tk ->
-  match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
+  match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
 Proof.
   induction 1; simpl; auto.
-  constructor.
-  econstructor; eauto.
+- apply match_Kstop.
+- eapply match_Kcall; eauto.
+- eapply match_Kcall_normalize; eauto.
 Qed.
 
 Lemma match_cont_is_call_cont:
-  forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt',
+  forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt',
   match_cont ce tyret nbrk ncnt k tk ->
   Clight.is_call_cont k ->
-  match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
+  match_cont ce' tyret nbrk' ncnt' k tk /\ is_call_cont tk.
 Proof.
   intros. inv H; simpl in H0; try contradiction; simpl.
-  split; auto; constructor.
-  split; auto; econstructor; eauto.
+  split; auto; apply match_Kstop.
+  split; auto; eapply match_Kcall; eauto.
+  split; auto; eapply match_Kcall_normalize; eauto.
 Qed.
 
 (** The simulation proof *)
@@ -1549,19 +1583,44 @@ Proof.
 
 - (* call *)
   revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
-  intros targs tres cc CF TR. monadInv TR. inv MTR.
+  intros targs tres cc CF TR. monadInv TR.
   exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
   rewrite H in CF. simpl in CF. inv CF.
-  econstructor; split.
-  apply plus_one. econstructor; eauto.
-  eapply transl_expr_correct with (cunit := cu); eauto.
-  eapply transl_arglist_correct with (cunit := cu); eauto.
-  erewrite typlist_of_arglist_eq by eauto.
-  eapply transl_fundef_sig1; eauto.
-  rewrite H3. auto.
-  econstructor; eauto.
-  eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
-  simpl. auto.
+  set (sg := {| sig_args := typlist_of_arglist al targs;
+                sig_res := rettype_of_type tres;
+                sig_cc := cc |}) in *.
+  assert (SIG: funsig tfd = sg).
+  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
+    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
+  assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0
+               \/ exists id, optid = Some id /\
+                  tk' = tk /\ ts' = Sseq (Scall optid sg x x0)
+                                         (Sset id (make_normalization tres (Evar id)))).
+  { unfold make_funcall in MTR.
+    destruct optid. destruct Conventions1.return_value_needs_normalization.
+    inv MTR. right; exists i; auto.
+    inv MTR; auto.
+    inv MTR; auto. }
+  destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES.
+  + (* without normalization of return value *)
+    econstructor; split.
+    apply plus_one. eapply step_call; eauto.
+    eapply transl_expr_correct with (cunit := cu); eauto.
+    eapply transl_arglist_correct with (cunit := cu); eauto.
+    econstructor; eauto.
+    eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
+    exact I.
+  + (* with normalization of return value *)
+    subst optid.
+    econstructor; split.
+    eapply plus_two. apply step_seq. eapply step_call; eauto. 
+    eapply transl_expr_correct with (cunit := cu); eauto.
+    eapply transl_arglist_correct with (cunit := cu); eauto.
+    traceEq.
+    econstructor; eauto.
+    eapply match_Kcall_normalize  with (ce := prog_comp_env cu') (cu := cu); eauto.
+    intros. eapply make_normalization_correct; eauto. constructor; eauto.
+    exact I.
 
 - (* builtin *)
   monadInv TR. inv MTR.
@@ -1658,6 +1717,7 @@ Proof.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
+  constructor.
 
 - (* return some *)
   monadInv TR. inv MTR.
@@ -1667,6 +1727,7 @@ Proof.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
+  apply wt_val_casted. eapply cast_val_is_casted; eauto.
 
 - (* skip call *)
   monadInv TR. inv MTR.
@@ -1675,6 +1736,7 @@ Proof.
   apply plus_one. apply step_skip_call. auto.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
+  constructor.
 
 - (* switch *)
   monadInv TR.
@@ -1738,20 +1800,33 @@ Proof.
   simpl. econstructor; eauto.
   unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
   constructor.
+  replace (fn_return f) with tres. eassumption.
+  simpl in TY. unfold type_of_function in TY. congruence. 
 
 - (* external function *)
   inv TR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
-  apply plus_one. constructor. eauto.
+  apply plus_one. constructor.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_returnstate with (ce := ce); eauto.
+  apply has_rettype_wt_val. 
+  replace (rettype_of_type tres0) with (sig_res (ef_sig ef)).
+  eapply external_call_well_typed_gen; eauto.
+  rewrite H5. simpl. simpl in TY. congruence.
 
 - (* returnstate *)
   inv MK.
-  econstructor; split.
-  apply plus_one. constructor.
-  econstructor; eauto. simpl; reflexivity. constructor.
+  + (* without normalization *)
+    econstructor; split.
+    apply plus_one. constructor.
+    econstructor; eauto. simpl; reflexivity. constructor.
+  + (* with normalization *)
+    econstructor; split.
+    eapply plus_three. econstructor. econstructor. constructor.
+    simpl. apply H13. eauto. apply PTree.gss.
+    traceEq.
+    simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor.
 Qed.
 
 Lemma transl_initial_states: