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 /lib/BoolEqual.v | |
parent | be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b (diff) | |
download | compcert-28f235806aa0918499b2ef162110f513ebe4db30.tar.gz compcert-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 'lib/BoolEqual.v')
0 files changed, 0 insertions, 0 deletions