chore: refuse to compile if FLT_EVAL_METHOD != 0 (#13872)

This PR is the first of several aiming to harden our runtime against
floating point nondeterminism.

Author: TwoFX

script/prepare-llvm-linux.sh

@@ -35,7 +35,7 @@ $CP $GCC_LIB/lib/libatomic.so* stage1/lib/
 
 find stage1 -type f -exec strip --strip-unneeded '{}' \; 2> /dev/null
 # lean.h dependencies
-$CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
+$CP llvm/lib/clang/*/include/{std*,__std*,limits,float,__float*}.h stage1/include/clang
 # ELF dependencies, must be put there for `--sysroot`
 $CP $GLIBC/lib/*crt* llvm/lib/
 $CP $GLIBC/lib/*crt* stage1/lib/

script/prepare-llvm-macos.sh

@@ -30,7 +30,7 @@ gcp -L llvm/bin/llvm-ar stage1/bin/
 $CP llvm/lib/lib{clang-cpp,LLVM}.dylib stage1/lib/
 #find stage1 -type f -exec strip --strip-unneeded '{}' \; 2> /dev/null
 # lean.h dependencies
-$CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
+$CP llvm/lib/clang/*/include/{std*,__std*,limits,float,__float*}.h stage1/include/clang
 # runtime
 (cd llvm; $CP --parents lib/clang/*/lib/*/libclang_rt.osx.a ../stage1)
 # libSystem stub, includes libc

script/prepare-llvm-mingw.sh

@@ -20,7 +20,7 @@ cp llvm/bin/llvm-ar stage1/bin/
 # dependencies of the above
 cp $(ldd llvm/bin/{clang,lld,llvm-ar}.exe | cut -f3 -d' ' --only-delimited | grep -E 'llvm|clang64') stage1/bin
 # lean.h dependencies
-cp llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang
+cp llvm/lib/clang/*/include/{std*,__std*,limits,float,__float*}.h stage1/include/clang
 # single Windows dependency
 echo '
 // https://docs.microsoft.com/en-us/windows/win32/api/errhandlingapi/nf-errhandlingapi-seterrormode

src/include/lean/lean.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <stdbool.h>
 #include <stdint.h>
 #include <limits.h>
+#include <float.h>
 
 #include <lean/config.h>
 
@@ -78,6 +79,14 @@ void lean_notify_assert(const char * fileName, int line, const char * condition)
 #define LEAN_EXPORT
 #endif
 
+// `FLT_EVAL_METHOD` is mandated to exist by the standard since C++11 and C99, but if we're in danger of triggering this
+// error, all bets are probably off and we should check whether it exists to avoid falling back to `0`.
+// We also perform this check in `lean.h` rather than in one of the runtime files because it is only valid per translation
+// unit, so we try to be safe and check it in all translation units.
+#if !defined(FLT_EVAL_METHOD) || (FLT_EVAL_METHOD != 0)
+#error Lean requires `FLT_EVAL_METHOD = 0` to ensure predictable semantics for floating-point operations.
+#endif
+
 #define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index)
 
 #define LeanMaxCtorTag  243