Skip to content
  • Xavier Leroy's avatar
    Support re-normalization of function parameters at function entry · 478ece46
    Xavier Leroy authored
    This is complementary to 28f23580
    
    Some ABIs leave more flexibility concerning function parameters than
    CompCert expects.
    
    For instance, the AArch64/ELF ABI allow the caller of a function to
    leave unspecified the "padding bits" of function parameters.  As an
    example, a parameter of type "unsigned char" may not have zeros in
    bits 8 to 63, but may have any bits there.
    
    When the caller is compiled by CompCert, it normalizes argument values
    to the parameter types before the call, so padding bits are always
    correct w.r.t. the type of the argument.  This is no longer guaranteed
    in interoperability scenarios, when the caller is not compiled by CompCert.
    
    This commit adds a general mechanism to insert "re-normalization"
    conversions on the parameters of a function, at function entry.
    This is controlled by the platform-dependent function
    Convention1.return_value_needs_normalization.
    
    The semantic preservation proof is still conducted against the
    CompCert model, where the argument 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 pass arguments that are not normalized.
    478ece46