missed alarm?

[regehr]

Alive with Z3 4.12.6 verifies this pair:

define i64 @src(float %0) {
if.end27:
  %1 = fptosi float %0 to i32
  %2 = sext i32 %1 to i64
  ret i64 %2

sink:                                             ; No predecessors!
  unreachable
}

define i64 @tgt(float %0) {
if.end27:
  %1 = fptosi float %0 to i64
  ret i64 %1

sink:                                             ; No predecessors!
  unreachable
}

but I don't think it's right

Johns-MacBook-Pro:~ regehr$ cat test.c
#include <stdio.h>

unsigned long src(float);
unsigned long tgt(float);

int main(void) {
  float f = 1.1e12;
  printf("%ld\n", src(f));
  printf("%ld\n", tgt(f));
}
Johns-MacBook-Pro:~ regehr$ llc foo.ll
Johns-MacBook-Pro:~ regehr$ clang test.c foo.s
Johns-MacBook-Pro:~ regehr$ ./a.out 
2147483647
1100000002048
Johns-MacBook-Pro:~ regehr$ 

I looked at the SMT queries and they seem plausible but I don't understand all of what's going on there. cc @zhengyang92

[nunoplopes]

It's correct because fptosi gives poison if the value doesn't fit. Doing fptosi in 64 bits will have the same behavior as the 32 bit version in src when the value fits.

If you flip src/tgt, then you get a counterexample.

[regehr]

argh thanks Nuno.