Skip to content
  • Xavier Leroy's avatar
    Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions · ef5477a4
    Xavier Leroy authored
    Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat
    PowerPC operations.
    
    The pseudoinstructions were used to implement these operations,
    as follows:
    
    Pfcfi  : Ofloatofint   i.e. the conversion signed int32 -> float64
    Pfcfiu : Ofloatofintu  i.e. the conversion unsigned int32 -> float64
    Pfctiu : Ointuoffloat  i.e. the conversion float64 -> unsigned int32
    
    These pseudoinstructions were expanded (in Asmexpand.ml) in terms of
    
    Pfcfid  : signed int64 -> float64
    Pfctidz : float64 -> signed int64
    
    and int32/int64 conversions.
    
    This commit performs this expansion during instruction selection
    (SelectOp.vp):
    
    floatofint(n)  becomes floatoflong(longofint(n))
    floatofintu(n) becomes floatoflong(longuofint(n))
    intuoffloat(n) becomes cast32unsigned(longoffloat(n))
    
    Then there is no need for the 3 removed operations and the 3 removed
    pseudoinstructions.
    
    More importantly, the correctness of these expansions is now proved as
    part of instruction selection, using the corresponding results from
    Floats.v.
    ef5477a4