Implement overrides for llvm.is.fpclass and friends (#1110)

This is primarily motivated by Clang 17 being more eager to compile the `isnan`
function into `llvm.is.fpclass`, so this patch is required to make the
`isnan.c` test case pass with Clang 17 or later. The machinery used to
implement an override for `llvm.is.fpclass` can also be used to implement
overrides for the related `isinf` function, so we also do this.

Checks off some boxes in #187.

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs

@@ -283,6 +283,8 @@ declare_overrides =
   , basic_llvm_override LLVM.llvmLog2Override_F64
   , basic_llvm_override LLVM.llvmLog10Override_F32
   , basic_llvm_override LLVM.llvmLog10Override_F64
+  , basic_llvm_override LLVM.llvmIsFpclassOverride_F32
+  , basic_llvm_override LLVM.llvmIsFpclassOverride_F64
 
   -- C standard library functions
   , basic_llvm_override Libc.llvmAbortOverride
@@ -317,6 +319,9 @@ declare_overrides =
   , basic_llvm_override Libc.llvmCeilfOverride
   , basic_llvm_override Libc.llvmFloorOverride
   , basic_llvm_override Libc.llvmFloorfOverride
+  , basic_llvm_override Libc.llvmIsinfOverride
+  , basic_llvm_override Libc.llvm__isinfOverride
+  , basic_llvm_override Libc.llvm__isinffOverride
   , basic_llvm_override Libc.llvmIsnanOverride
   , basic_llvm_override Libc.llvm__isnanOverride
   , basic_llvm_override Libc.llvm__isnanfOverride

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

@@ -30,7 +30,7 @@ module Lang.Crucible.LLVM.Intrinsics.LLVM where
 
 import           GHC.TypeNats (KnownNat)
 import           Control.Lens hiding (op, (:>), Empty)
-import           Control.Monad (unless)
+import           Control.Monad (foldM, unless)
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Data.Bits ((.&.))
 import qualified Data.Vector as V
@@ -993,6 +993,26 @@ llvmLog10Override_F64 =
   [llvmOvr| double @llvm.log10.f64( double ) |]
   (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callSpecialFunction1 bak W4.Log10) args)
 
+llvmIsFpclassOverride_F32 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym
+     (EmptyCtx ::> FloatType SingleFloat
+               ::> BVType 32)
+     (BVType 1)
+llvmIsFpclassOverride_F32 =
+  [llvmOvr| i1 @llvm.is.fpclass.f32( float, i32 ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (callIsFpclass bak) args)
+
+llvmIsFpclassOverride_F64 ::
+  IsSymInterface sym =>
+  LLVMOverride p sym
+     (EmptyCtx ::> FloatType DoubleFloat
+               ::> BVType 32)
+     (BVType 1)
+llvmIsFpclassOverride_F64 =
+  [llvmOvr| i1 @llvm.is.fpclass.f64( double, i32 ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (callIsFpclass bak) args)
+
 
 llvmX86_pclmulqdq
 --declare <2 x i64> @llvm.x86.pclmulqdq(<2 x i64>, <2 x i64>, i8) #1
@@ -1423,3 +1443,83 @@ callCopysign bak
     signsSame <- eqPred sym xIsNeg yIsNeg
     xNegated  <- iFloatNeg @_ @fi sym x
     iFloatIte @_ @fi sym signsSame x xNegated
+
+-- | An implementation of the @llvm.is.fpclass@ intrinsic. This essentially
+-- combines several different floating-point checks (checking for @NaN@,
+-- infinity, zero, etc.) into a single function. The second argument is a
+-- bitmask that controls which properties to check of the first argument.
+-- The different checks in the bitmask are described by the table here:
+-- <https://llvm.org/docs/LangRef.html#id1566>
+--
+-- The specification requires being able to distinguish between signaling
+-- @NaN@s (bit 0 of the bitmask) and quit @NaN@s (bit 1 of the bitmask), but
+-- @crucible-llvm@ does not have the ability to do this. As a result, both
+-- @NaN@ checks will always return true in this implementation, regardless of
+-- whether they are signaling or quiet @NaN@s.
+callIsFpclass ::
+  forall fi p sym bak ext r args ret.
+  IsSymBackend sym bak =>
+  bak ->
+  RegEntry sym (FloatType fi) ->
+  RegEntry sym (BVType 32) ->
+  OverrideSim p sym ext r args ret (RegValue sym (BVType 1))
+callIsFpclass bak regOp@(regValue -> op) (regValue -> test) = do
+  bvOne  <- liftIO $ bvLit sym w1 (BV.one w1)
+  bvZero <- liftIO $ bvLit sym w1 (BV.zero w1)
+
+  let negative bit = liftIO $ do
+        isNeg <- iFloatIsNeg @_ @fi sym op
+        liftIO $ bvIte sym isNeg bit bvZero
+
+  let positive bit = liftIO $ do
+        isPos <- iFloatIsPos @_ @fi sym op
+        liftIO $ bvIte sym isPos bit bvZero
+
+  let negAndPos doCheck = liftIO $ do
+        check <- doCheck
+        checkN <- negative check
+        checkP <- positive check
+        pure (checkN, checkP)
+
+  let callIsInf x = do
+        isInf <- iFloatIsInf @_ @fi sym x
+        bvIte sym isInf bvOne bvZero
+
+  let callIsNormal x = do
+        isNorm <- iFloatIsNorm @_ @fi sym x
+        bvIte sym isNorm bvOne bvZero
+
+  let callIsSubnormal x = do
+        isSubnorm <- iFloatIsSubnorm @_ @fi sym x
+        bvIte sym isSubnorm bvOne bvZero
+
+  let callIsZero x = do
+        is0 <- iFloatIsZero @_ @fi sym x
+        bvIte sym is0 bvOne bvZero
+
+  isNan <- Libc.callIsnan bak w1 regOp
+  (isInfN, isInfP) <- negAndPos $ callIsInf op
+  (isNormN, isNormP) <- negAndPos $ callIsNormal op
+  (isSubnormN, isSubnormP) <- negAndPos $ callIsSubnormal op
+  (isZeroN, isZeroP) <- negAndPos $ callIsZero op
+
+  foldM
+    (\bits (bitNum, check) -> liftIO $ do
+        isBitSet <- liftIO $ testBitBV sym bitNum test
+        newBit <- liftIO $ bvIte sym isBitSet check bvZero
+        liftIO $ bvOrBits sym newBit bits)
+    bvZero
+    [ (0, isNan)      -- Signaling NaN
+    , (1, isNan)      -- Quiet NaN
+    , (2, isInfN)     -- Negative infinity
+    , (3, isNormN)    -- Negative normal
+    , (4, isSubnormN) -- Negative subnormal
+    , (5, isZeroN)    -- Negative zero
+    , (6, isZeroP)    -- Positive zero
+    , (7, isSubnormP) -- Positive subnormal
+    , (8, isNormP)    -- Positive normal
+    , (9, isInfP)     -- Positive infinity
+    ]
+  where
+    sym = backendGetSym bak
+    w1 = knownNat @1

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

@@ -739,33 +739,71 @@ llvmFloorfOverride =
   (\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args)
 
 
--- math.h defines isnan() as a macro, so you might think it unusual to provide
--- a function override for it. However, if you write (isnan)(x) instead of
--- isnan(x), Clang will compile the former as a direct function call rather
--- than as a macro application. Some experimentation reveals that the isnan
--- function's argument is always a double, so we give its argument the type
--- double here to match this unstated convention.
+-- math.h defines isinf() and isnan() as macros, so you might think it unusual
+-- to provide function overrides for them. However, if you write, say,
+-- (isnan)(x) instead of isnan(x), Clang will compile the former as a direct
+-- function call rather than as a macro application. Some experimentation
+-- reveals that the isnan function's argument is always a double, so we give its
+-- argument the type double here to match this unstated convention. We follow
+-- suit similarly with isinf.
+--
+-- Clang does not yet provide direct function call versions of isfinite() or
+-- isnormal(), so we do not provide overrides for them.
+
+llvmIsinfOverride ::
+  IsSymInterface sym =>
+  LLVMOverride p sym
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (BVType 32)
+llvmIsinfOverride =
+  [llvmOvr| i32 @isinf( double ) |]
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args)
+
+-- __isinf and __isinff are like the isinf macro, except their arguments are
+-- known to be double or float, respectively. They are not mentioned in the
+-- POSIX source standard, only the binary standard. See
+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinf.html and
+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isinff.html.
+llvm__isinfOverride ::
+  IsSymInterface sym =>
+  LLVMOverride p sym
+     (EmptyCtx ::> FloatType DoubleFloat)
+     (BVType 32)
+llvm__isinfOverride =
+  [llvmOvr| i32 @__isinf( double ) |]
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args)
+
+llvm__isinffOverride ::
+  IsSymInterface sym =>
+  LLVMOverride p sym
+     (EmptyCtx ::> FloatType SingleFloat)
+     (BVType 32)
+llvm__isinffOverride =
+  [llvmOvr| i32 @__isinff( float ) |]
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsinf sym (knownNat @32)) args)
+
 llvmIsnanOverride ::
   IsSymInterface sym =>
   LLVMOverride p sym
      (EmptyCtx ::> FloatType DoubleFloat)
      (BVType 32)
 llvmIsnanOverride =
   [llvmOvr| i32 @isnan( double ) |]
-  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym) args)
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args)
 
 -- __isnan and __isnanf are like the isnan macro, except their arguments are
 -- known to be double or float, respectively. They are not mentioned in the
 -- POSIX source standard, only the binary standard. See
--- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnan.html
+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnan.html and
+-- http://refspecs.linux-foundation.org/LSB_4.0.0/LSB-Core-generic/LSB-Core-generic/baselib---isnanf.html.
 llvm__isnanOverride ::
   IsSymInterface sym =>
   LLVMOverride p sym
      (EmptyCtx ::> FloatType DoubleFloat)
      (BVType 32)
 llvm__isnanOverride =
   [llvmOvr| i32 @__isnan( double ) |]
-  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym) args)
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args)
 
 llvm__isnanfOverride ::
   IsSymInterface sym =>
@@ -774,7 +812,7 @@ llvm__isnanfOverride ::
      (BVType 32)
 llvm__isnanfOverride =
   [llvmOvr| i32 @__isnanf( float ) |]
-  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym) args)
+  (\_memOps sym args -> Ctx.uncurryAssignment (callIsnan sym (knownNat @32)) args)
 
 
 llvmSqrtOverride ::
@@ -832,16 +870,39 @@ callFloor ::
   OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
 callFloor bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTN x
 
+-- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the
+-- argument is positive infinity, @-1@ when the argument is negative infinity,
+-- and zero otherwise.
+callIsinf ::
+  forall fi w p sym bak ext r args ret.
+  (IsSymBackend sym bak, 1 <= w) =>
+  bak ->
+  NatRepr w ->
+  RegEntry sym (FloatType fi) ->
+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))
+callIsinf bak w (regValue -> x) = liftIO $ do
+  let sym = backendGetSym bak
+  isInf <- iFloatIsInf @_ @fi sym x
+  isNeg <- iFloatIsNeg @_ @fi sym x
+  isPos <- iFloatIsPos @_ @fi sym x
+  isInfN <- andPred sym isInf isNeg
+  isInfP <- andPred sym isInf isPos
+  bvOne    <- bvLit sym w (BV.one w)
+  bvNegOne <- bvNeg sym bvOne
+  bvZero   <- bvLit sym w (BV.zero w)
+  res0 <- bvIte sym isInfP bvOne bvZero
+  bvIte sym isInfN bvNegOne res0
+
 callIsnan ::
-  forall fi p sym bak ext r args ret.
-  (IsSymBackend sym bak) =>
+  forall fi w p sym bak ext r args ret.
+  (IsSymBackend sym bak, 1 <= w) =>
   bak ->
+  NatRepr w ->
   RegEntry sym (FloatType fi) ->
-  OverrideSim p sym ext r args ret (RegValue sym (BVType 32))
-callIsnan bak (regValue -> x) = liftIO $ do
+  OverrideSim p sym ext r args ret (RegValue sym (BVType w))
+callIsnan bak w (regValue -> x) = liftIO $ do
   let sym = backendGetSym bak
   isnan  <- iFloatIsNaN @_ @fi sym x
-  let w = knownNat @32
   bvOne  <- bvLit sym w (BV.one w)
   bvZero <- bvLit sym w (BV.zero w)
   -- isnan() is allowed to return any nonzero value if the argument is NaN, and

crux-llvm/test-data/golden/isfinite.c

@@ -0,0 +1,37 @@
+#define _GNU_SOURCE
+#include <crucible.h>
+#include <math.h>
+
+int main(void) {
+  ////////////
+  // double //
+  ////////////
+  double d1 = 42.5;     // Finite
+  double d2 = INFINITY; // Infinite
+  double d3 = NAN;      // Not infinite (and also not finite)
+
+  check(isfinite(d1));
+  check(!(isfinite(d2)));
+  check(!(isfinite(d3)));
+
+  check(__builtin_isfinite(d1));
+  check(!(__builtin_isfinite(d2)));
+  check(!(__builtin_isfinite(d3)));
+
+  ///////////
+  // float //
+  ///////////
+  float f1 = 42.5f;    // Finite
+  float f2 = INFINITY; // Infinite
+  float f3 = NAN;      // Not infinite (and also not finite)
+
+  check(isfinite(f1));
+  check(!(isfinite(f2)));
+  check(!(isfinite(f3)));
+
+  check(__builtin_isfinite(f1));
+  check(!(__builtin_isfinite(f2)));
+  check(!(__builtin_isfinite(f3)));
+
+  return 0;
+}

crux-llvm/test-data/golden/isfinite.config

@@ -0,0 +1,2 @@
+opt-level: 0
+solver: "z3"

crux-llvm/test-data/golden/isfinite.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.

crux-llvm/test-data/golden/isinf.c

@@ -0,0 +1,65 @@
+#define _GNU_SOURCE
+#include <crucible.h>
+#include <math.h>
+
+int main(void) {
+  ////////////
+  // double //
+  ////////////
+  double d1 = 42.5;      // Finite
+  double d2 = INFINITY;  // Infinite
+  double d3 = -INFINITY; // Infinite
+  double d4 = NAN;       // Not infinite (and also not finite)
+
+  check(isinf(d1) ==  0);
+  check(isinf(d2) ==  1);
+  check(isinf(d3) == -1);
+  check(isinf(d4) ==  0);
+
+  // The parentheses around (isinf) are important here, as this instructs Clang
+  // to compile isinf as a direct function call rather than as a macro.
+  check((isinf)(d1) ==  0);
+  check((isinf)(d2) ==  1);
+  check((isinf)(d3) == -1);
+  check((isinf)(d4) ==  0);
+
+  check(__isinf(d1) ==  0);
+  check(__isinf(d2) ==  1);
+  check(__isinf(d3) == -1);
+  check(__isinf(d4) ==  0);
+
+  check(__builtin_isinf_sign(d1) ==  0);
+  check(__builtin_isinf_sign(d2) ==  1);
+  check(__builtin_isinf_sign(d3) == -1);
+  check(__builtin_isinf_sign(d4) ==  0);
+
+  ///////////
+  // float //
+  ///////////
+  float f1 = 42.5f;     // Finite
+  float f2 = INFINITY;  // Infinite
+  float f3 = -INFINITY; // Infinite
+  float f4 = NAN;       // Not infinite (and also not finite)
+
+  check(isinf(f1) ==  0);
+  check(isinf(f2) ==  1);
+  check(isinf(f3) == -1);
+  check(isinf(f4) ==  0);
+
+  check((isinf)(f1) ==  0);
+  check((isinf)(f2) ==  1);
+  check((isinf)(f3) == -1);
+  check((isinf)(f4) ==  0);
+
+  check(__isinff(f1) ==  0);
+  check(__isinff(f2) ==  1);
+  check(__isinff(f3) == -1);
+  check(__isinff(f4) ==  0);
+
+  check(__builtin_isinf_sign(f1) ==  0);
+  check(__builtin_isinf_sign(f2) ==  1);
+  check(__builtin_isinf_sign(f3) == -1);
+  check(__builtin_isinf_sign(f4) ==  0);
+
+  return 0;
+}

crux-llvm/test-data/golden/isinf.config

@@ -0,0 +1,2 @@
+opt-level: 0
+solver: "z3"

crux-llvm/test-data/golden/isinf.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.