diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-20 19:17:57 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-21 13:29:39 +0100 |
| commit | 3bdb983e0b21c8d45e85aff08278475396038f4f (patch) | |
| tree | 46355ef86dfb0f8753b8047b5fc595471d6cd836 | |
| parent | 3bffda879e214345635e575a696e8f184bef0e55 (diff) | |
| download | compcert-kvx-3bdb983e0b21c8d45e85aff08278475396038f4f.tar.gz compcert-kvx-3bdb983e0b21c8d45e85aff08278475396038f4f.zip | |
AArch64: normalize function return values of small integer type
According to AAPCS64 (the AArch64 ABI specification), the
top bits of the register containing the function result have
unspecified value, so we need to sign- or zero-extend the function result
before using it, as in the x86 port.
| -rw-r--r-- | aarch64/Conventions1.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index b1b3badd..14cb199f 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -379,6 +379,14 @@ Qed. (** ** Normalization of function results *) -(** No normalization needed. *) - -Definition return_value_needs_normalization (t: rettype) := false. +(** 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. *) + +Definition return_value_needs_normalization (t: rettype) : bool := + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end. |