refinement failure roundtripping through the AArch64 backend for an fadd with rounding=dynamic, exceptions=strict

[regehr]

this function:

define float @fadd_s(float %0, float %1) {
  %3 = call float @llvm.experimental.constrained.fadd.f32(float %0, float %1, metadata !"round.dynamic", metadata !"fpexcept.strict") #2
  ret float %3
}

; Function Attrs: nocallback nofree nosync nounwind strictfp willreturn memory(inaccessiblemem: readwrite)
declare float @llvm.experimental.constrained.fadd.f32(float, float, metadata, metadata) #1

gets compiled by the AArch64 backend to a regular fadd:

fadd_s:
        fadd    s0, s0, s1
        ret

we lift this fadd (correctly, I hope) back to a regular LLVM fadd, resulting in this failure of refinement:

define float @fadd_s(float %#0, float %#1) {
#2:
  %#3 = fadd float %#0, %#1, rounding=dynamic, exceptions=strict
  ret float %#3
}
=>
define float @fadd_s(float %#0, float %#1) nofree willreturn asm memory(none) {
arm_tv_entry:
  %a2_6 = fadd float %#0, %#1
  ret float %a2_6
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
float %#0 = #x00000000 (+0.0)
float %#1 = #x80000000 (-0.0)

Source:
float %#3 = #x80000000 (-0.0)

Target:
float %a2_6 = #x00000000 (+0.0)
Source value: #x80000000 (-0.0)
Target value: #x00000000 (+0.0)

so it looks like someone's wrong here, but I don't know if it's Alive, the AArch64 backend, or my lifter

[nunoplopes]

My reading from https://developer.arm.com/documentation/101433/0101/Register-descriptions/Advanced-SIMD-and-floating-point-registers/FPCR--Floating-point-Control-Register?lang=en is that fadd's rounding depends on the FPCR register. This is modeled with LLVM's "round.dynamic" feature.

So I think you need to have a different lifting for strict fp and non-strict fp. But you may want to check with a more knowledgeable FP person.

[regehr]

ok, yeah, I think this is something we're not yet interested in confronting in the lifter... I'll just filter out tests that make use of this feature. thanks!