diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-19 12:50:55 +0100 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-21 13:29:39 +0100 |
commit | 28f235806aa0918499b2ef162110f513ebe4db30 (patch) | |
tree | 24a22f126f1e65b35eeddc557bb924e4bb76f06e /x86 | |
parent | be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b (diff) | |
download | compcert-kvx-28f235806aa0918499b2ef162110f513ebe4db30.tar.gz compcert-kvx-28f235806aa0918499b2ef162110f513ebe4db30.zip |
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.
Diffstat (limited to 'x86')
-rw-r--r-- | x86/Conventions1.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 595cb721..01b15e98 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -471,3 +471,17 @@ Lemma loc_arguments_main: Proof. unfold loc_arguments; destruct Archi.ptr64; reflexivity. Qed. + +(** ** Normalization of function results *) + +(** In the x86 ABI, a return value of type "char" is returned in + register AL, leaving the top 24 bits of EAX unspecified. + Likewise, a return value of type "short" is returned in register + AH, leaving the top 16 bits of EAX unspecified. Hence, return + values of small integer types need re-normalization after calls. *) + +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end. |