-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Libc.Math
-- Description      : Override definitions for C @math.h@ functions
-- Copyright        : (c) Galois, Inc 2026
-- License          : BSD3
-- Maintainer       : Galois, Inc. <crux@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Lang.Crucible.LLVM.Intrinsics.Libc.Math
  ( -- * @math.h@ overrides
    mathOverrides
    -- * Override declarations
  , llvmCeilOverride
  , llvmCeilfOverride
  , llvmFloorOverride
  , llvmFloorfOverride
  , llvmFmaOverride
  , llvmFmafOverride
  , llvmIsinfOverride
  , llvm__isinfOverride
  , llvm__isinffOverride
  , llvmIsnanOverride
  , llvm__isnanOverride
  , llvm__isnanfOverride
  , llvm__isnandOverride
  , llvmSqrtOverride
  , llvmSqrtfOverride
  , llvmSinOverride
  , llvmSinfOverride
  , llvmCosOverride
  , llvmCosfOverride
  , llvmTanOverride
  , llvmTanfOverride
  , llvmAsinOverride
  , llvmAsinfOverride
  , llvmAcosOverride
  , llvmAcosfOverride
  , llvmAtanOverride
  , llvmAtanfOverride
  , llvmSinhOverride
  , llvmSinhfOverride
  , llvmCoshOverride
  , llvmCoshfOverride
  , llvmTanhOverride
  , llvmTanhfOverride
  , llvmAsinhOverride
  , llvmAsinhfOverride
  , llvmAcoshOverride
  , llvmAcoshfOverride
  , llvmAtanhOverride
  , llvmAtanhfOverride
  , llvmHypotOverride
  , llvmHypotfOverride
  , llvmAtan2Override
  , llvmAtan2fOverride
  , llvmPowfOverride
  , llvmPowOverride
  , llvmExpOverride
  , llvmExpfOverride
  , llvmLogOverride
  , llvmLogfOverride
  , llvmExpm1Override
  , llvmExpm1fOverride
  , llvmLog1pOverride
  , llvmLog1pfOverride
  , llvmExp2Override
  , llvmExp2fOverride
  , llvmLog2Override
  , llvmLog2fOverride
  , llvmExp10Override
  , llvmExp10fOverride
  , llvm__exp10Override
  , llvm__exp10fOverride
  , llvmLog10Override
  , llvmLog10fOverride
    -- * Implementation functions
  , callCeil
  , callFloor
  , callFMA
  , callIsinf
  , callIsnan
  , callSqrt
  , callSpecialFunction1
  , callSpecialFunction2
  , defaultRM
  ) where

import           Control.Monad.IO.Class (liftIO)

import qualified Data.Parameterized.Context as Ctx

import           What4.Interface
import qualified What4.SpecialFunctions as W4

import           Lang.Crucible.Backend
import           Lang.Crucible.Types
import           Lang.Crucible.Simulator.OverrideSim
import           Lang.Crucible.Simulator.RegMap

import           Lang.Crucible.LLVM.QQ( llvmOvr )

import           Lang.Crucible.LLVM.Intrinsics.Common

-- | All @math.h@ overrides
mathOverrides ::
  IsSymInterface sym =>
  [SomeLLVMOverride p sym ext]
mathOverrides :: forall sym p ext.
IsSymInterface sym =>
[SomeLLVMOverride p sym ext]
mathOverrides =
  [ LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCeilOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCeilfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmFloorOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmFloorfOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmFmaOverride
  , LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmFmafOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvmIsinfOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isinfOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
llvm__isinffOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvmIsnanOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isnanOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
llvm__isnanfOverride
  , LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isnandOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSqrtOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSqrtfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSinOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSinfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCosOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCosfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmTanOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmTanfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAsinOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAsinfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAcosOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAcosfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtanOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtanfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSinhOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSinhfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCoshOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCoshfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmTanhOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmTanhfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAsinhOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAsinhfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAcoshOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAcoshfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtanhOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtanhfOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmHypotOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmHypotfOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtan2Override
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtan2fOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmPowfOverride
  , LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmPowOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExpOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExpfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLogOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLogfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExpm1Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExpm1fOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog1pOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog1pfOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExp2Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExp2fOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog2Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog2fOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExp10Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExp10fOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvm__exp10Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvm__exp10fOverride
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog10Override
  , LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
-> SomeLLVMOverride p sym ext
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType).
LLVMOverride p sym ext args ret -> SomeLLVMOverride p sym ext
SomeLLVMOverride LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog10fOverride
  ]

------------------------------------------------------------------------
-- ** Declarations

llvmCeilOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmCeilOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCeilOverride =
  [llvmOvr| double @ceil( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmCeilfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmCeilfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCeilfOverride =
  [llvmOvr| float @ceilf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)


llvmFloorOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmFloorOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmFloorOverride =
  [llvmOvr| double @floor( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmFloorfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmFloorfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmFloorfOverride =
  [llvmOvr| float @floorf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

llvmFmafOverride ::
     forall sym p ext
   . IsSymInterface sym
  => LLVMOverride p sym ext
        (EmptyCtx ::> FloatType SingleFloat
                  ::> FloatType SingleFloat
                  ::> FloatType SingleFloat)
        (FloatType SingleFloat)
llvmFmafOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmFmafOverride =
  [llvmOvr| float @fmaf( float, float, float ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
args -> CurryAssignment
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
      ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
      ::> FloatType SingleFloat)
-> x
Ctx.uncurryAssignment CurryAssignment
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
RegEntry sym (FloatType SingleFloat)
-> RegEntry sym (FloatType SingleFloat)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA Assignment
  (RegEntry sym)
  (((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
   ::> FloatType SingleFloat)
args)

llvmFmaOverride ::
     forall sym p ext
   . IsSymInterface sym
  => LLVMOverride p sym ext
        (EmptyCtx ::> FloatType DoubleFloat
                  ::> FloatType DoubleFloat
                  ::> FloatType DoubleFloat)
        (FloatType DoubleFloat)
llvmFmaOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmFmaOverride =
  [llvmOvr| double @fma( double, double, double ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
args -> CurryAssignment
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment
     (RegEntry sym)
     (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
      ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  f
  x
-> Assignment
     f
     (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
      ::> FloatType DoubleFloat)
-> x
Ctx.uncurryAssignment CurryAssignment
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
RegEntry sym (FloatType DoubleFloat)
-> RegEntry sym (FloatType DoubleFloat)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA Assignment
  (RegEntry sym)
  (((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
   ::> FloatType DoubleFloat)
args)


-- 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 ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (BVType 32)
llvmIsinfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvmIsinfOverride =
  [llvmOvr| i32 @isinf( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
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 ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (BVType 32)
llvm__isinfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isinfOverride =
  [llvmOvr| i32 @__isinf( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvm__isinffOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (BVType 32)
llvm__isinffOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
llvm__isinffOverride =
  [llvmOvr| i32 @__isinff( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

llvmIsnanOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (BVType 32)
llvmIsnanOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvmIsnanOverride =
  [llvmOvr| i32 @isnan( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
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 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 ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (BVType 32)
llvm__isnanOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isnanOverride =
  [llvmOvr| i32 @__isnan( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvm__isnanfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (BVType 32)
llvm__isnanfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType SingleFloat) (BVType 32)
llvm__isnanfOverride =
  [llvmOvr| i32 @__isnanf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- macOS compiles isnan() to __isnand() when the argument is a double.
llvm__isnandOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (BVType 32)
llvm__isnandOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p sym ext (EmptyCtx ::> FloatType DoubleFloat) (BVType 32)
llvm__isnandOverride =
  [llvmOvr| i32 @__isnand( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (SymExpr sym ('BaseBVType 32))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (NatRepr 32
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim p sym ext rtp args' ret' (RegValue sym (BVType 32))
forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32)) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmSqrtOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmSqrtOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSqrtOverride =
  [llvmOvr| double @sqrt( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmSqrtfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmSqrtfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSqrtfOverride =
  [llvmOvr| float @sqrtf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Circular trigonometry functions

-- sin(f)

llvmSinOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmSinOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSinOverride =
  [llvmOvr| double @sin( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Sin) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmSinfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmSinfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSinfOverride =
  [llvmOvr| float @sinf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Sin) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- cos(f)

llvmCosOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmCosOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCosOverride =
  [llvmOvr| double @cos( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Cos) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmCosfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmCosfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCosfOverride =
  [llvmOvr| float @cosf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Cos) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- tan(f)

llvmTanOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmTanOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmTanOverride =
  [llvmOvr| double @tan( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Tan) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmTanfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmTanfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmTanfOverride =
  [llvmOvr| float @tanf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Tan) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- asin(f)

llvmAsinOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAsinOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAsinOverride =
  [llvmOvr| double @asin( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arcsin) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAsinfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAsinfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAsinfOverride =
  [llvmOvr| float @asinf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arcsin) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- acos(f)

llvmAcosOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAcosOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAcosOverride =
  [llvmOvr| double @acos( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arccos) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAcosfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAcosfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAcosfOverride =
  [llvmOvr| float @acosf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arccos) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- atan(f)

llvmAtanOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAtanOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtanOverride =
  [llvmOvr| double @atan( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arctan) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAtanfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAtanfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtanfOverride =
  [llvmOvr| float @atanf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arctan) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Hyperbolic trigonometry functions

-- sinh(f)

llvmSinhOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmSinhOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmSinhOverride =
  [llvmOvr| double @sinh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Sinh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmSinhfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmSinhfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmSinhfOverride =
  [llvmOvr| float @sinhf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Sinh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- cosh(f)

llvmCoshOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmCoshOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmCoshOverride =
  [llvmOvr| double @cosh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Cosh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmCoshfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmCoshfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmCoshfOverride =
  [llvmOvr| float @coshf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Cosh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- tanh(f)

llvmTanhOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmTanhOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmTanhOverride =
  [llvmOvr| double @tanh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Tanh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmTanhfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmTanhfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmTanhfOverride =
  [llvmOvr| float @tanhf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Tanh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- asinh(f)

llvmAsinhOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAsinhOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAsinhOverride =
  [llvmOvr| double @asinh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arcsinh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAsinhfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAsinhfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAsinhfOverride =
  [llvmOvr| float @asinhf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arcsinh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- acosh(f)

llvmAcoshOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAcoshOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAcoshOverride =
  [llvmOvr| double @acosh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arccosh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAcoshfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAcoshfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAcoshfOverride =
  [llvmOvr| float @acoshf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arccosh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- atanh(f)

llvmAtanhOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAtanhOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtanhOverride =
  [llvmOvr| double @atanh( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arctanh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmAtanhfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAtanhfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtanhfOverride =
  [llvmOvr| float @atanhf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Arctanh) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Rectangular to polar coordinate conversion

-- hypot(f)

llvmHypotOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmHypotOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmHypotOverride =
  [llvmOvr| double @hypot( double, double ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Hypot) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args)

llvmHypotfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmHypotfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmHypotfOverride =
  [llvmOvr| float @hypotf( float, float ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Hypot) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args)

-- atan2(f)

llvmAtan2Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmAtan2Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmAtan2Override =
  [llvmOvr| double @atan2( double, double ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Arctan2) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args)

llvmAtan2fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmAtan2fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmAtan2fOverride =
  [llvmOvr| float @atan2f( float, float ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Arctan2) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Exponential and logarithm functions

-- pow(f)

llvmPowfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmPowfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmPowfOverride =
  [llvmOvr| float @powf( float, float ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Pow) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType SingleFloat) ::> FloatType SingleFloat)
args)

llvmPowOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmPowOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmPowOverride =
  [llvmOvr| double @pow( double, double ) |]
  (\GlobalVar Mem
_memOps Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args -> CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment
     (RegEntry sym)
     ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
  f
  x
-> Assignment
     f ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
-> x
Ctx.uncurryAssignment (SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
W4.Pow) Assignment
  (RegEntry sym)
  ((EmptyCtx ::> FloatType DoubleFloat) ::> FloatType DoubleFloat)
args)

-- exp(f)

llvmExpOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmExpOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExpOverride =
  [llvmOvr| double @exp( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmExpfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmExpfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExpfOverride =
  [llvmOvr| float @expf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- log(f)

llvmLogOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmLogOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLogOverride =
  [llvmOvr| double @log( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmLogfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmLogfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLogfOverride =
  [llvmOvr| float @logf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- expm1(f)

llvmExpm1Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmExpm1Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExpm1Override =
  [llvmOvr| double @expm1( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Expm1) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmExpm1fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmExpm1fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExpm1fOverride =
  [llvmOvr| float @expm1f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Expm1) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- log1p(f)

llvmLog1pOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmLog1pOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog1pOverride =
  [llvmOvr| double @log1p( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log1p) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmLog1pfOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmLog1pfOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog1pfOverride =
  [llvmOvr| float @log1pf( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log1p) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Base 2 exponential and logarithm

-- exp2(f)

llvmExp2Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmExp2Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExp2Override =
  [llvmOvr| double @exp2( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp2) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmExp2fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmExp2fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExp2fOverride =
  [llvmOvr| float @exp2f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp2) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- log2(f)

llvmLog2Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmLog2Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog2Override =
  [llvmOvr| double @log2( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log2) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmLog2fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmLog2fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog2fOverride =
  [llvmOvr| float @log2f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log2) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- **** Base 10 exponential and logarithm

-- exp10(f)

llvmExp10Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmExp10Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmExp10Override =
  [llvmOvr| double @exp10( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmExp10fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmExp10fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmExp10fOverride =
  [llvmOvr| float @exp10f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- macOS uses __exp10(f) instead of exp10(f).

llvm__exp10Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvm__exp10Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvm__exp10Override =
  [llvmOvr| double @__exp10( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvm__exp10fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvm__exp10fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvm__exp10fOverride =
  [llvmOvr| float @__exp10f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Exp10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

-- log10(f)

llvmLog10Override ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType DoubleFloat)
     (FloatType DoubleFloat)
llvmLog10Override :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType DoubleFloat)
  (FloatType DoubleFloat)
llvmLog10Override =
  [llvmOvr| double @log10( double ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType DoubleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym DoubleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType DoubleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType DoubleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType DoubleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType DoubleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType DoubleFloat)
args)

llvmLog10fOverride ::
  IsSymInterface sym =>
  LLVMOverride p sym ext
     (EmptyCtx ::> FloatType SingleFloat)
     (FloatType SingleFloat)
llvmLog10fOverride :: forall sym p ext.
IsSymInterface sym =>
LLVMOverride
  p
  sym
  ext
  (EmptyCtx ::> FloatType SingleFloat)
  (FloatType SingleFloat)
llvmLog10fOverride =
  [llvmOvr| float @log10f( float ) |]
  (\GlobalVar Mem
_memOps Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args -> CurryAssignment
  (EmptyCtx ::> FloatType SingleFloat)
  (RegEntry sym)
  (OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat)))
-> Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
-> OverrideSim
     p
     sym
     ext
     rtp
     args'
     ret'
     (SymExpr sym (SymInterpretedFloatType sym SingleFloat))
forall k (ctx :: Ctx k) (f :: k -> Type) x.
CurryAssignmentClass ctx =>
CurryAssignment ctx f x -> Assignment f ctx -> x
forall (f :: CrucibleType -> Type) x.
CurryAssignment (EmptyCtx ::> FloatType SingleFloat) f x
-> Assignment f (EmptyCtx ::> FloatType SingleFloat) -> x
Ctx.uncurryAssignment (SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType SingleFloat)
-> OverrideSim
     p sym ext rtp args' ret' (RegValue sym (FloatType SingleFloat))
forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
W4.Log10) Assignment (RegEntry sym) (EmptyCtx ::> FloatType SingleFloat)
args)

------------------------------------------------------------------------
-- ** Implementations

callSpecialFunction1 ::
  forall fi p sym ext r args ret.
  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
  W4.SpecialFunction (EmptyCtx ::> W4.R) ->
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction (EmptyCtx ::> R)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction1 SpecialFunction (EmptyCtx ::> R)
fn (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymExpr sym (SymInterpretedFloatType sym fi)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SpecialFunction (EmptyCtx ::> R)
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSpecialFunction1 sym
sym (FloatInfoRepr fi
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatInfoRepr fi) SpecialFunction (EmptyCtx ::> R)
fn RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x

callSpecialFunction2 ::
  forall fi p sym ext r args ret.
  (IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
  W4.SpecialFunction (EmptyCtx ::> W4.R ::> W4.R) ->
  RegEntry sym (FloatType fi) ->
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
(IsSymInterface sym, KnownRepr FloatInfoRepr fi) =>
SpecialFunction ((EmptyCtx ::> R) ::> R)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSpecialFunction2 SpecialFunction ((EmptyCtx ::> R) ::> R)
fn (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
y) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ sym
-> FloatInfoRepr fi
-> SpecialFunction ((EmptyCtx ::> R) ::> R)
-> SymExpr sym (SymInterpretedFloatType sym fi)
-> SymExpr sym (SymInterpretedFloatType sym fi)
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> FloatInfoRepr fi
-> SpecialFunction ((EmptyCtx ::> R) ::> R)
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
forall (fi :: FloatInfo).
sym
-> FloatInfoRepr fi
-> SpecialFunction ((EmptyCtx ::> R) ::> R)
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSpecialFunction2 sym
sym (FloatInfoRepr fi
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr :: FloatInfoRepr fi) SpecialFunction ((EmptyCtx ::> R) ::> R)
fn RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
y

callCeil ::
  forall fi p sym ext r args ret.
  IsSymInterface sym =>
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callCeil (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatRound @_ @fi sym
sym RoundingMode
RTP RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x

callFloor ::
  forall fi p sym ext r args ret.
  IsSymInterface sym =>
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFloor (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatRound @_ @fi sym
sym RoundingMode
RTN RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x

-- | An implementation of @libc@'s @fma@ function.
callFMA ::
     forall fi p sym ext r args ret
   . IsSymInterface sym
  => RegEntry sym (FloatType fi)
  -> RegEntry sym (FloatType fi)
  -> RegEntry sym (FloatType fi)
  -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callFMA (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
y) (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
z) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatFMA @_ @fi sym
sym RoundingMode
defaultRM RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
y RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
z

-- | 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 ext r args ret.
  (IsSymInterface sym, 1 <= w) =>
  NatRepr w ->
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsinf NatRepr w
w (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType w))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a b. (a -> b) -> a -> b
$ do
    SymExpr sym BaseBoolType
isInf <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsInf @_ @fi sym
sym RegValue sym (FloatType fi)
SymInterpretedFloat sym fi
x
    SymExpr sym BaseBoolType
isNeg <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsNeg @_ @fi sym
sym RegValue sym (FloatType fi)
SymInterpretedFloat sym fi
x
    SymExpr sym BaseBoolType
isPos <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsPos @_ @fi sym
sym RegValue sym (FloatType fi)
SymInterpretedFloat sym fi
x
    SymExpr sym BaseBoolType
isInfN <- sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
isInf SymExpr sym BaseBoolType
isNeg
    SymExpr sym BaseBoolType
isInfP <- sym
-> SymExpr sym BaseBoolType
-> SymExpr sym BaseBoolType
-> IO (SymExpr sym BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym SymExpr sym BaseBoolType
isInf SymExpr sym BaseBoolType
isPos
    SymExpr sym ('BaseBVType w)
bv1 <- sym -> NatRepr w -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvOne sym
sym NatRepr w
w
    SymExpr sym ('BaseBVType w)
bvNeg1 <- sym
-> SymExpr sym ('BaseBVType w) -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
bvNeg sym
sym SymExpr sym ('BaseBVType w)
bv1
    SymExpr sym ('BaseBVType w)
bv0 <- sym -> NatRepr w -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr w
w
    SymExpr sym ('BaseBVType w)
res0 <- sym
-> SymExpr sym BaseBoolType
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isInfP SymExpr sym ('BaseBVType w)
bv1 SymExpr sym ('BaseBVType w)
bv0
    sym
-> SymExpr sym BaseBoolType
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isInfN SymExpr sym ('BaseBVType w)
bvNeg1 SymExpr sym ('BaseBVType w)
res0

callIsnan ::
  forall fi w p sym ext r args ret.
  (IsSymInterface sym, 1 <= w) =>
  NatRepr w ->
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan :: forall (fi :: FloatInfo) (w :: Natural) p sym ext r
       (args :: Ctx CrucibleType) (ret :: CrucibleType).
(IsSymInterface sym, 1 <= w) =>
NatRepr w
-> RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (BVType w))
callIsnan NatRepr w
w (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym ('BaseBVType w))
 -> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w)))
-> IO (SymExpr sym ('BaseBVType w))
-> OverrideSim p sym ext r args ret (SymExpr sym ('BaseBVType w))
forall a b. (a -> b) -> a -> b
$ do
    SymExpr sym BaseBoolType
isnan  <- forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym -> SymInterpretedFloat sym fi -> IO (Pred sym)
iFloatIsNaN @_ @fi sym
sym RegValue sym (FloatType fi)
SymInterpretedFloat sym fi
x
    SymExpr sym ('BaseBVType w)
bv1 <- sym -> NatRepr w -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvOne sym
sym NatRepr w
w
    SymExpr sym ('BaseBVType w)
bv0 <- sym -> NatRepr w -> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural) sym.
(1 <= w, IsExprBuilder sym) =>
sym -> NatRepr w -> IO (SymBV sym w)
bvZero sym
sym NatRepr w
w
    -- isnan() is allowed to return any nonzero value if the argument is NaN, and
    -- out of all the possible nonzero values, `1` is certainly one of them.
    sym
-> SymExpr sym BaseBoolType
-> SymExpr sym ('BaseBVType w)
-> SymExpr sym ('BaseBVType w)
-> IO (SymExpr sym ('BaseBVType w))
forall (w :: Natural).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
sym SymExpr sym BaseBoolType
isnan SymExpr sym ('BaseBVType w)
bv1 SymExpr sym ('BaseBVType w)
bv0

callSqrt ::
  forall fi p sym ext r args ret.
  IsSymInterface sym =>
  RegEntry sym (FloatType fi) ->
  OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt :: forall (fi :: FloatInfo) p sym ext r (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
IsSymInterface sym =>
RegEntry sym (FloatType fi)
-> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
callSqrt (RegEntry sym (FloatType fi) -> RegValue sym (FloatType fi)
forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue -> RegValue sym (FloatType fi)
x) = do
  sym
sym <- OverrideSim p sym ext r args ret sym
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
OverrideSim p sym ext rtp args ret sym
getSymInterface
  IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a. IO a -> OverrideSim p sym ext r args ret a
forall (m :: Type -> Type) a. MonadIO m => IO a -> m a
liftIO (IO (SymExpr sym (SymInterpretedFloatType sym fi))
 -> OverrideSim
      p
      sym
      ext
      r
      args
      ret
      (SymExpr sym (SymInterpretedFloatType sym fi)))
-> IO (SymExpr sym (SymInterpretedFloatType sym fi))
-> OverrideSim
     p sym ext r args ret (SymExpr sym (SymInterpretedFloatType sym fi))
forall a b. (a -> b) -> a -> b
$ forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> RoundingMode
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatSqrt @_ @fi sym
sym RoundingMode
defaultRM RegValue sym (FloatType fi)
SymExpr sym (SymInterpretedFloatType sym fi)
x

-- | IEEE 754 declares 'RNE' to be the default rounding mode, and most @libc@
-- implementations agree with this in practice. The only places where we do not
-- use this as the default are operations that specifically require the behavior
-- of a particular rounding mode, such as @ceil@ or @floor@.
defaultRM :: RoundingMode
defaultRM :: RoundingMode
defaultRM = RoundingMode
RNE