Support re-normalization of function parameters at function entry

This is complementary to 28f235806

Some ABIs leave more flexibility concerning function parameters than
CompCert expects.

For instance, the AArch64/ELF ABI allow the caller of a function to
leave unspecified the "padding bits" of function parameters.  As an
example, a parameter of type "unsigned char" may not have zeros in
bits 8 to 63, but may have any bits there.

When the caller is compiled by CompCert, it normalizes argument values
to the parameter types before the call, so padding bits are always
correct w.r.t. the type of the argument.  This is no longer guaranteed
in interoperability scenarios, when the caller is not compiled by CompCert.

This commit adds a general mechanism to insert "re-normalization"
conversions on the parameters of a function, at function entry.
This is controlled by the platform-dependent function
Convention1.return_value_needs_normalization.

The semantic preservation proof is still conducted against the
CompCert model, where the argument 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 pass arguments that are not normalized.

7 files changed, 58 insertions, 27 deletions

diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v
index cfcbcbf1..7edb16dd 100644
--- a/aarch64/Conventions1.v
+++ b/aarch64/Conventions1.v
@@ -343,16 +343,19 @@ Proof.
   unfold loc_arguments; reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** According to the AAPCS64 ABI specification, "padding bits" in the return
-    value of a function have unpredictable values and must be ignored.
-    Consequently, we force normalization of return values of small integer
-    types (8- and 16-bit integers), so that the top bits (the "padding bits")
-    are proper sign- or zero-extensions of the small integer value.
+    value of a function or in a function parameter have unpredictable
+    values and must be ignored.  Consequently, we force normalization
+    of return values and of function parameters when they have small
+    integer types (8- and 16-bit integers), so that the top bits (the
+    "padding bits") are proper sign- or zero-extensions of the small
+    integer value.
 
     The Apple variant of the AAPCS64 requires the callee to return a normalized
-    value, hence no normalization is needed in the caller.
+    value, and the caller to pass normalized parameters, hence no
+    normalization is needed.
  *)
 
 Definition return_value_needs_normalization (t: rettype) : bool :=
@@ -365,3 +368,4 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
       end
   end.
 
+Definition parameter_needs_normalization := return_value_needs_normalization.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 3bd2b553..b94ce9ef 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -436,8 +436,9 @@ Proof.
   destruct Archi.abi; reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** No normalization needed. *)
 
 Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index f54aa60d..0a164e29 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -18,7 +18,7 @@ Require FSetAVL.
 Require Import Coqlib Ordered Errors.
 Require Import AST Linking.
 Require Import Ctypes Cop Clight.
-Require Compopts.
+Require Compopts Conventions1.
 
 Open Scope error_monad_scope.
 Open Scope string_scope.
@@ -157,15 +157,20 @@ with simpl_lblstmt (cenv: compilenv) (ls: labeled_statements) : res labeled_stat
   end.
 
 (** Function parameters that are not lifted to temporaries must be
-  stored in the corresponding local variable at function entry. *)
+  stored in the corresponding local variable at function entry.
+  The other function parameters may need to be normalized to their types,
+  to support interoperability with code generated by other C compilers. *)
 
 Fixpoint store_params (cenv: compilenv) (params: list (ident * type))
                       (s: statement): statement :=
   match params with
   | nil => s
   | (id, ty) :: params' =>
-      if VSet.mem id cenv
-      then store_params cenv params' s
+      if VSet.mem id cenv then
+        if Conventions1.parameter_needs_normalization (rettype_of_type ty)
+        then Ssequence (Sset id (make_cast (Etempvar id ty) ty))
+                       (store_params cenv params' s)
+        else store_params cenv params' s
       else Ssequence (Sassign (Evar id ty) (Etempvar id ty))
                      (store_params cenv params' s)
   end.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 8246a748..988988a1 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -1108,23 +1108,37 @@ Theorem store_params_correct:
   /\ match_envs j cenv e le m' lo hi te tle tlo thi
   /\ Mem.nextblock tm' = Mem.nextblock tm.
 Proof.
+Local Opaque Conventions1.parameter_needs_normalization.
   induction 1; simpl; intros until targs; intros NOREPET CASTED VINJ MENV MINJ TLE LE.
-  (* base case *)
+- (* base case *)
   inv VINJ. exists tle2; exists tm; split. apply star_refl. split. auto. split. auto.
   split. apply match_envs_temps_exten with tle1; auto. auto.
-  (* inductive case *)
+- (* inductive case *)
   inv NOREPET. inv CASTED. inv VINJ.
   exploit me_vars; eauto. instantiate (1 := id); intros MV.
-  destruct (VSet.mem id cenv) eqn:?.
-  (* lifted to temp *)
-  eapply IHbind_parameters with (tle1 := PTree.set id v' tle1); eauto.
-  eapply match_envs_assign_lifted; eauto.
-  inv MV; try congruence. rewrite ENV in H; inv H.
-  inv H0; try congruence.
-  unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto.
-  intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto.
-  apply TLE. intuition.
-  (* still in memory *)
+  destruct (VSet.mem id cenv) eqn:LIFTED.
++ (* lifted to temp *)
+  exploit (IHbind_parameters s tm (PTree.set id v' tle1) (PTree.set id v' tle2)).
+    eauto. eauto. eauto.
+    eapply match_envs_assign_lifted; eauto.
+    inv MV; try congruence. rewrite ENV in H; inv H.
+    inv H0; try congruence.
+    unfold Mem.storev in H2. eapply Mem.store_unmapped_inject; eauto.
+    intros. repeat rewrite PTree.gsspec. destruct (peq id0 id). auto.
+    apply TLE. intuition.
+    eauto.
+  intros (tle & tm' & U & V & X & Y & Z).
+  exists tle, tm'; split; [|auto].
+  destruct (Conventions1.parameter_needs_normalization (rettype_of_type ty)); [|assumption].
+  assert (A: tle!id = Some v').
+  { erewrite bind_parameter_temps_inv by eauto. apply PTree.gss. }
+  eapply star_left. constructor.
+  eapply star_left. econstructor. eapply make_cast_correct.
+    constructor; eauto. apply cast_val_casted; auto. eapply val_casted_inject; eauto.
+  rewrite PTree.gsident by auto.
+  eapply star_left. constructor. eassumption.
+  traceEq. traceEq. traceEq.
++ (* still in memory *)
   inv MV; try congruence. rewrite ENV in H; inv H.
   exploit assign_loc_inject; eauto.
   intros [tm1 [A [B C]]].
@@ -1979,7 +1993,7 @@ Lemma find_label_store_params:
   forall s k params, find_label lbl (store_params cenv params s) k = find_label lbl s k.
 Proof.
   induction params; simpl. auto.
-  destruct a as [id ty]. destruct (VSet.mem id cenv); auto.
+  destruct a as [id ty]. destruct (VSet.mem id cenv); [destruct Conventions1.parameter_needs_normalization|]; auto.
 Qed.
 
 Lemma find_label_add_debug_vars:
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 045eb471..56beffe8 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -349,8 +349,9 @@ Proof.
   reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** No normalization needed. *)
 
 Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 6cb06c61..eeaae3c4 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -413,8 +413,9 @@ Proof.
   reflexivity.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** No normalization needed. *)
 
 Definition return_value_needs_normalization (t: rettype) := false.
+Definition parameter_needs_normalization (t: rettype) := false.
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 803d162a..e3c51f60 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -431,7 +431,7 @@ Proof.
   unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto.
 Qed.
 
-(** ** Normalization of function results *)
+(** ** Normalization of function results and parameters *)
 
 (** In the x86 ABI, a return value of type "char" is returned in
     register AL, leaving the top 24 bits of EAX unspecified.
@@ -444,3 +444,8 @@ Definition return_value_needs_normalization (t: rettype) : bool :=
   | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
   | _ => false
   end.
+
+(** Function parameters are passed in normalized form and do not need
+    to be re-normalized at function entry. *)
+
+Definition parameter_needs_normalization (t: rettype) := false.