bvlongdouble is not a proper name and probably not correctly implemented

[shaobo-he]

We name SMT floating-point sort (_ FloatingPoint 15 65) as bvlongdouble which implements LLVM's x86_fp80 type. I think it's very problematic for two reasons.

1. The type long double in C does not necessarily mean x86_fp80 type (see https://en.wikipedia.org/wiki/Long_double).
2. Even if it maps to x86_fp80, the type x86_fp80 is not equivalent to the floating-point type. For example, the assertion in the following program should hold while SMACK reports an error,

#include "smack.h"
int main() {
  long double a = 1.0;
  assert((double)a == 1.0);
  return 0;
}

This is probably due to the fact that x86_fp80 uses an explicit integer part in the significand bits.

[zvonimir]

Why does it matter to SMACK what long double is in C? LLVM has x86_fp80 type, and hopefully that is what we use in our source code to recognize it. In the LLVM language manual, this type is specified as "80-bit floating-point value (X87)". So I don't understand your point (1).

[zvonimir]

I agree with your point (2) above. My follow-up question is - do we have any regressions or are there any SVCOMP benchmarks that use x86_fp80?

[shaobo-he]

Why does it matter to SMACK what long double is in C? LLVM has x86_fp80 type, and hopefully that is what we use in our source code to recognize it. In the LLVM language manual, this type is specified as "80-bit floating-point value (X87)". So I don't understand your point (1).

My point is that long double is not a type synonym for x86_fp80 even though long double is often compiled to to x86_fp80. The language specification doesn't require this behavior. Therefore I think the Boogie type corresponding to the LLVM x86_fp80 type should not be named as bvlongdouble.

[shaobo-he]

I agree with your point (2) above. My follow-up question is - do we have any regressions or are there any SVCOMP benchmarks that use x86_fp80?

No, I think I've never seen any of those.

[zvonimir]

Ah, I see. You were mainly referring to the naming convention in your point (1). Yes, I agree with that. The way I see it, we should: (1) Rename this type into something else, maybe x86fp80 to roughly match LLVM's type. (2) I would guess that we should also leave this type unintepreted since my understanding is that it would be hard to model is using the available SMT theories.