GaloisInc / crucible

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

Add overrides for `fma` and friends #1154

Closed RyanGlScott closed 9 months ago

RyanGlScott commented 9 months ago

Clang 14 and later enable -ffp-contract=on by default, which which cause combinations of multiplications/additions to be optimized into the llvm.fmuladd.* intrinsic, even with -O0. Here is an example of a simple program that works when run with crux-llvm and Clang 13 and earlier, but fails with Clang 14+ because of this issue:

double fmuladd(double a, double b, double c) {
  return a * b + c;
}

int main(void) {
  double d = fmuladd(1.0, 2.0, 3.0);
  return 0;
}
``` # With Clang 13.0.0 $ cabal run exe:crux-llvm -- test.c -O0 [Crux] Using pointer width: 64 for file crux-build/crux~test.bc [Crux] Simulating function main [Crux] All goals discharged through internal simplification. [Crux] Overall status: Valid. # With Clang 14.0.0 $ cabal run exe:crux-llvm -- test.c -O0 [Crux] Using pointer width: 64 for file crux-build/crux~test.bc [Crux] Simulating function main [Crux] Attempting to prove verification conditions. [Crux] *** debug executable: results/test/debug-2 [Crux] *** break on line: 2 [Crux] Found counterexample for verification goal [Crux] test.c:2:16: error: in fmuladd [Crux] Failed to load function handle [Crux] Details: [Crux] No implementation or override found for pointer [Crux] The given pointer could not be resolved to a callable function [Crux] No implementation or override found for pointer [Crux] Attempting to load callable function with type: double(double, double, double) [Crux] Via pointer: Global symbol "llvm.fmuladd.f64" (2, 0x0:[64]) [Crux] In memory state: [Crux] Stack frame fmuladd [Crux] Allocations: [Crux] StackAlloc 9 0x8:[64] Mutable 8-byte-aligned test.c:1:43 [Crux] StackAlloc 8 0x8:[64] Mutable 8-byte-aligned test.c:1:33 [Crux] StackAlloc 7 0x8:[64] Mutable 8-byte-aligned test.c:1:23 [Crux] Writes: [Crux] Indexed chunk: [Crux] 7 |-> *(7, 0x0:[64]) := 1 [Crux] 8 |-> *(8, 0x0:[64]) := 2 [Crux] 9 |-> *(9, 0x0:[64]) := 3 [Crux] Stack frame main [Crux] Allocations: [Crux] StackAlloc 6 0x8:[64] Mutable 8-byte-aligned test.c:6:10 [Crux] StackAlloc 5 0x4:[64] Mutable 4-byte-aligned internal [Crux] Writes: [Crux] Indexed chunk: [Crux] 5 |-> memset (5, 0x0:[64]) 0x0:[8] 0x4:[64] [Crux] Base memory [Crux] Allocations: [Crux] GlobalAlloc 4 0x0:[64] Immutable 1-byte-aligned [defined function ] main [Crux] GlobalAlloc 3 0x0:[64] Immutable 1-byte-aligned [defined function ] fmuladd [Crux] GlobalAlloc 2 0x0:[64] Immutable 1-byte-aligned [external function] llvm.fmuladd.f64 [Crux] GlobalAlloc 1 0x0:[64] Immutable 1-byte-aligned [external function] llvm.dbg.declare [Crux] in context: [Crux] fmuladd [Crux] main [Crux] Goal status: [Crux] Total: 1 [Crux] Proved: 0 [Crux] Disproved: 1 [Crux] Incomplete: 0 [Crux] Unknown: 0 [Crux] Overall status: Invalid. ```

We should add overrides for llvm.fmuladd.*, the related intrinsic llvm.fma.*, and the fma/fmaf functions from libc.