From 3bdb983e0b21c8d45e85aff08278475396038f4f Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 20 Feb 2020 19:17:57 +0100 Subject: 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. --- aarch64/Conventions1.v | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'aarch64/Conventions1.v') 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. -- cgit