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, 6 insertions, 0 deletions

diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 09cbbb44..27d09d94 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -438,3 +438,9 @@ Lemma loc_arguments_main:
 Proof.
   reflexivity.
 Qed.
+
+(** ** Normalization of function results *)
+
+(** No normalization needed. *)
+
+Definition return_value_needs_normalization (t: rettype) := false.