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.

1 files changed, 10 insertions, 6 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.