search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
637 stars 42 forks source link

Missing floating point operations #187

Open robdockins opened 5 years ago

robdockins commented 5 years ago

There are a number of llvm intrinsics and math.h functions for floating point operations that are exercised by the sv-benchmark suite that are not currently implemented.

The following ones should be relatively easy to hook up, because they already appear to have What4 representations and corresponding solver support (although we should check to ensure that the semantics of each operation match exactly):

The following will probably require additional work. For most, it's not obvious if they can easily be reduced to simpler operations that respect all the corner cases of their semantics. In other cases, the semantics probably cannot be exactly represented at all (because e.g., they distinguish between different NaNs):

There are a whole additional collection of llvm intrinsics and operations from math.h we could imagine implementing in addition to the ones listed here, of course. Let's edit this ticket as we encounter examples of these in the wild. Many of them will pose nontrivial design questions as we decide what to do about each of these operations in the various interpretations we have for them.

RyanGlScott commented 3 years ago

I recently tested crux-llvm out on a handful of floating-point SV-COMP benchmarks. Here is a tally of missing overrides that I encountered:

RyanGlScott commented 3 years ago

LLVM 12 in particular is much more eager to generate calls to llvm.copysign.* than in previous versions. With this code:

#include <stdio.h>

typedef union {
  float a;
  int b;
} c;

c d;
float e;

float f() {
  d.a = e;
  return d.b < 0 ? -1.5707963705e00 : 1.5707963705e00;
}

int main() {
  printf("%f\n", f());
  return 0;
}

Clang 10.0.0 will compile the d.b < 0 ? -1.5707963705e00 : 1.5707963705e00 part to an icmp followed by a select instruction, while Clang 12.0.0 will compile it to a call to llvm.copysign.f32().

robdockins commented 3 years ago

Also, CF https://github.com/GaloisInc/what4/issues/159

RyanGlScott commented 1 year ago

LLVM 17 in particular is much more eager to generate calls to llvm.is.fpclass than in previous versions. With this code:

#include <math.h>

int main(void) {
  double d = 0.0;
  return isnan(d);
}

Clang 17.0.1 will compile the isnan(x) call to call i1 @llvm.is.fpclass.f64(double x, i32 3), where the bitmask 3 means that LLVM will return true if x is either a signaling or quiet NaN. (See this table for a full description of what goes into the bitmask.) At present crucible-llvm does not implement an override for llvm.is.fpclass, but we will need to add one in order to support isnan going forward.

If we add support for llvm.is.fpclass, this will have the benefit of giving us all the machinery that we need to implement support for isfinite, isnormal, and isinf, so we could consider adding support for those as well. We could also consider adding support for fpclassify, although that would be more difficult, since the values that fpclassify can return (FP_NAN, FP_INFINITE, etc.) are likely implementation-defined.