Skip to content
  • Xavier Leroy's avatar
    Support re-normalization of values returned by function calls · 28f23580
    Xavier Leroy authored
    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.
    28f23580