{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

module Crux.LLVM.Compile where

import           Control.Applicative
import           Control.Exception ( SomeException(..), try )
import           Control.Monad ( guard, unless, when, forM_ )
import           Control.Monad.Logic ( observeAll )
import qualified Data.Foldable as Fold
import           Data.List ( intercalate, isSuffixOf )
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.Some
import qualified Data.Text as T
import qualified Data.Text.IO as TIO
import           System.Directory ( doesFileExist, findExecutable, removeFile
                                  , createDirectoryIfMissing, copyFile )
import           System.Exit ( ExitCode(..) )
import           System.FilePath ( takeExtension, (</>), (-<.>)
                                 , takeDirectory, takeFileName )
import           System.Process ( readProcessWithExitCode )

import           What4.Interface
import           What4.ProgramLoc

import           Lang.Crucible.Simulator.SimError

import           Crux
import qualified Crux.Config.Common as CC
import           Crux.Model ( toDouble, showBVLiteral, showFloatLiteral
                            , showDoubleLiteral )
import           Crux.Types

import           Crux.LLVM.Config
import qualified Crux.LLVM.Log as Log


isCPlusPlus :: FilePath -> Bool
isCPlusPlus :: String -> Bool
isCPlusPlus String
file =
  case String -> String
takeExtension String
file of
    String
".cpp" -> Bool
True
    String
".cxx" -> Bool
True
    String
".C" -> Bool
True
    String
".bc" -> Bool
False
    String
_ -> Bool
False

anyCPPFiles :: [FilePath] -> Bool
anyCPPFiles :: [String] -> Bool
anyCPPFiles = (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any String -> Bool
isCPlusPlus

-- | attempt to find Clang executable by searching the file system
-- throw an error if it cannot be found this way.
-- (NOTE: do not look for environment var "CLANG". That is assumed
--  to be tried already.)
getClang :: IO FilePath
getClang :: IO String
getClang = [IO (Maybe String)] -> IO String
attempt ((String -> IO (Maybe String)) -> [String] -> [IO (Maybe String)]
forall a b. (a -> b) -> [a] -> [b]
map String -> IO (Maybe String)
findExecutable [String]
clangs)
  where
  clangs :: [String]
clangs = String
"clang"
         String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [ String
"clang-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ver
           | String
ver <- [String
"3.6", String
"3.7", String
"3.8", String
"3.9", String
"4.0", String
"5.0", String
"6.0"]
                    -- Starting with LLVM 7, the version numbers used in binaries only display the major version. See
                    -- https://releases.llvm.org/7.0.0/tools/clang/docs/ReleaseNotes.html#non-comprehensive-list-of-changes-in-this-release
                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"7", String
"8", String
"9", String
"10", String
"11"] ]

  attempt :: [IO (Maybe FilePath)] -> IO FilePath
  attempt :: [IO (Maybe String)] -> IO String
attempt [IO (Maybe String)]
ms =
    case [IO (Maybe String)]
ms of
      [] -> CError -> IO String
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (CError -> IO String) -> CError -> IO String
forall a b. (a -> b) -> a -> b
$ String -> CError
EnvError (String -> CError) -> String -> CError
forall a b. (a -> b) -> a -> b
$
              [String] -> String
unlines [ String
"Failed to find `clang`."
                      , String
"You may use CLANG to provide path to executable."
                      ]
      IO (Maybe String)
m : [IO (Maybe String)]
more -> do Maybe String
x <- IO (Maybe String)
m
                     case Maybe String
x of
                       Maybe String
Nothing -> [IO (Maybe String)] -> IO String
attempt [IO (Maybe String)]
more
                       Just String
a  -> String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
a

runClang ::
  Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  LLVMOptions -> [String] -> IO ()
runClang :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions -> [String] -> IO ()
runClang LLVMOptions
llvmOpts [String]
params =
  do let clang :: String
clang = LLVMOptions -> String
clangBin LLVMOptions
llvmOpts
         allParams :: [String]
allParams = LLVMOptions -> [String]
clangOpts LLVMOptions
llvmOpts [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
params
     CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM ([Text] -> CruxLLVMLogMessage
Log.ClangInvocation (String -> Text
T.pack (String -> Text) -> [String] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String
clang String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
forall a. Show a => a -> String
show [String]
allParams)))
     (ExitCode
res,String
sout,String
serr) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
clang [String]
allParams String
""
     case ExitCode
res of
       ExitCode
ExitSuccess   -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       ExitFailure Int
n -> CError -> IO ()
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (Int -> String -> String -> CError
ClangError Int
n String
sout String
serr)

llvmLink :: LLVMOptions -> [FilePath] -> FilePath -> IO ()
llvmLink :: LLVMOptions -> [String] -> String -> IO ()
llvmLink LLVMOptions
llvmOpts [String]
ins String
out =
  do let params :: [String]
params = [String]
ins [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"-o", String
out ]
     (ExitCode
res, String
sout, String
serr) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode (LLVMOptions -> String
linkBin LLVMOptions
llvmOpts) [String]
params String
""
     case ExitCode
res of
       ExitCode
ExitSuccess   -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       ExitFailure Int
n -> CError -> IO ()
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (Int -> String -> String -> CError
ClangError Int
n String
sout String
serr)

parseLLVMLinkVersion :: String -> String
parseLLVMLinkVersion :: String -> String
parseLLVMLinkVersion = [[String]] -> String
forall {a}. (Eq a, IsString a) => [[a]] -> a
go ([[String]] -> String)
-> (String -> [[String]]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [String]) -> [String] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map String -> [String]
words ([String] -> [[String]])
-> (String -> [String]) -> String -> [[String]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines
  where
    go :: [[a]] -> a
go ((a
"LLVM" : a
"version" : a
version : [a]
_) : [[a]]
_) = a
version
    go ([a]
_ : [[a]]
rest) = [[a]] -> a
go [[a]]
rest
    go [] = a
""

llvmLinkVersion :: LLVMOptions -> IO String
llvmLinkVersion :: LLVMOptions -> IO String
llvmLinkVersion LLVMOptions
llvmOpts =
  do (ExitCode
res, String
sout, String
serr) <- String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode (LLVMOptions -> String
linkBin LLVMOptions
llvmOpts) [String
"--version"] String
""
     case ExitCode
res of
       ExitCode
ExitSuccess   -> String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> String
parseLLVMLinkVersion String
sout)
       ExitFailure Int
n -> CError -> IO String
forall (m :: * -> *) b. MonadIO m => CError -> m b
throwCError (Int -> String -> String -> CError
ClangError Int
n String
sout String
serr)

-- | Generates compiled LLVM bitcode for the set of input files
-- specified in the 'CruxOptions' argument, writing the output to a
-- pre-determined filename in the build directory specified in
-- 'CruxOptions'.
genBitCode ::
  Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  CruxOptions -> LLVMOptions -> IO FilePath
genBitCode :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions -> LLVMOptions -> IO String
genBitCode CruxOptions
cruxOpts LLVMOptions
llvmOpts =
  -- n.b. use of head here is OK because inputFiles should not be
  -- empty (and was previously verified as such in CruxLLVMMain).
  if LLVMOptions -> Bool
noCompile LLVMOptions
llvmOpts
  then String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> String
forall a. HasCallStack => [a] -> a
head (CruxOptions -> [String]
Crux.inputFiles CruxOptions
cruxOpts))
  else do
    let ofn :: String
ofn = String
"crux~" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> (String -> String
takeFileName (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall a. HasCallStack => [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ CruxOptions -> [String]
Crux.inputFiles CruxOptions
cruxOpts) String -> String -> String
-<.> String
".bc"
    String
-> [String] -> CruxOptions -> LLVMOptions -> Bool -> IO String
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
String
-> [String] -> CruxOptions -> LLVMOptions -> Bool -> IO String
genBitCodeToFile String
ofn (CruxOptions -> [String]
Crux.inputFiles CruxOptions
cruxOpts) CruxOptions
cruxOpts LLVMOptions
llvmOpts Bool
False

-- | Given the target filename and a list of input files, along with
-- the crux and llvm options, bitcode-compile each input .c file and
-- link the resulting files, along with any input .ll files into the
-- target bitcode (BC) file.  Returns the filepath of the target
-- bitcode file.
genBitCodeToFile :: Crux.Logs msgs
                 => Log.SupportsCruxLLVMLogMessage msgs
                 => String -> [FilePath] -> CruxOptions -> LLVMOptions -> Bool
                 -> IO FilePath
genBitCodeToFile :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
String
-> [String] -> CruxOptions -> LLVMOptions -> Bool -> IO String
genBitCodeToFile String
finalBCFileName [String]
files CruxOptions
cruxOpts LLVMOptions
llvmOpts Bool
copySrc = do
  let srcBCNames :: [(String, String)]
srcBCNames = [ (String
src, CruxOptions -> String
CC.bldDir CruxOptions
cruxOpts String -> String -> String
</> String -> String
takeFileName String
src String -> String -> String
-<.> String
".bc")
                   | String
src <- [String]
files ]
      finalBCFile :: String
finalBCFile = CruxOptions -> String
CC.bldDir CruxOptions
cruxOpts String -> String -> String
</> String
finalBCFileName
      incs :: String -> [String]
incs String
src = String -> String
takeDirectory String
src String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                 (LLVMOptions -> String
libDir LLVMOptions
llvmOpts String -> String -> String
</> String
"includes") String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                 LLVMOptions -> [String]
incDirs LLVMOptions
llvmOpts
      commonFlags :: [String]
commonFlags = [ String
"-c", String
"-DCRUCIBLE", String
"-emit-llvm" ] [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<>
                    case LLVMOptions -> Maybe String
targetArch LLVMOptions
llvmOpts of
                      Maybe String
Nothing -> []
                      Just String
a -> [ String
"--target=" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
a ]
      params :: (String, String) -> IO [String]
params (String
src, String
srcBC)
        | String
".ll" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
src =
            [String] -> IO [String]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ [String]
commonFlags [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String
"-O0", String
"-o", String
srcBC, String
src]

        | Bool
otherwise =
            -- Specify commonFlags after flags embedded in the src
            -- under the /assumption/ that the latter takes
            -- precedence.
            let flgs :: [String]
flgs =
                  [String]
commonFlags [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [ String
"-g" ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ String
"-I", String
dir ] | String
dir <- String -> [String]
incs String
src ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ String
"-fsanitize="String -> String -> String
forall a. [a] -> [a] -> [a]
++String
san, String
"-fsanitize-trap="String -> String -> String
forall a. [a] -> [a] -> [a]
++String
san ]
                         | String
san <- LLVMOptions -> [String]
ubSanitizers LLVMOptions
llvmOpts ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                  [ String
"-O" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (LLVMOptions -> Int
optLevel LLVMOptions
llvmOpts), String
"-o", String
srcBC, String
src ]
            in ([String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
<> [String]
flgs) ([String] -> [String]) -> IO [String] -> IO [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO [String]
crucibleFlagsFromSrc String
src

  Bool
finalBCExists <- String -> IO Bool
doesFileExist String
finalBCFile
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
finalBCExists Bool -> Bool -> Bool
&& LLVMOptions -> Bool
lazyCompile LLVMOptions
llvmOpts) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      do [(String, String)] -> ((String, String) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(String, String)]
srcBCNames (((String, String) -> IO ()) -> IO ())
-> ((String, String) -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \f :: (String, String)
f@(String
src,String
bc) -> do
           Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
copySrc) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
copyFile String
src (String -> String
takeDirectory String
bc String -> String -> String
</> String -> String
takeFileName String
src)
           Bool
bcExists <- String -> IO Bool
doesFileExist String
bc
           Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ String
".bc" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` String
src
                      , Bool
bcExists Bool -> Bool -> Bool
&& LLVMOptions -> Bool
lazyCompile LLVMOptions
llvmOpts
                      ]) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
             LLVMOptions -> [String] -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions -> [String] -> IO ()
runClang LLVMOptions
llvmOpts ([String] -> IO ()) -> IO [String] -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (String, String) -> IO [String]
params (String, String)
f
         String
ver <- LLVMOptions -> IO String
llvmLinkVersion LLVMOptions
llvmOpts
         let libcxxBitcode :: [String]
libcxxBitcode | [String] -> Bool
anyCPPFiles [String]
files = [LLVMOptions -> String
libDir LLVMOptions
llvmOpts String -> String -> String
</> String
"libcxx-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ver String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".bc"]
                           | Bool
otherwise = []
             allBCInputFiles :: [String]
allBCInputFiles = ((String, String) -> String) -> [(String, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, String) -> String
forall a b. (a, b) -> b
snd [(String, String)]
srcBCNames [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
libcxxBitcode
         case [String]
allBCInputFiles of
           [String
bcInputFile]
             -> -- If there is only one input .bc file, just copy it to the
                -- output destination instead of using llvm-link to produce it.
                -- Not only is invoking llvm-link needlessly expensive, it can
                -- sometimes rearrange the order of declarations in the bitcode,
                -- which makes certain test cases fragile (see #1011).
                String -> String -> IO ()
copyFile String
bcInputFile String
finalBCFile
           [String]
_ -> LLVMOptions -> [String] -> String -> IO ()
llvmLink LLVMOptions
llvmOpts [String]
allBCInputFiles String
finalBCFile
         ((String, String) -> IO ()) -> [(String, String)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(String
src,String
bc) -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String
src String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
bc) (String -> IO ()
removeFile String
bc)) [(String, String)]
srcBCNames
  String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
finalBCFile


-- | A C source file being compiled and evaluated by crux can contain
-- zero or more lines matching the following:
--
-- >   /* CRUCIBLE clang_flags: {FLAGS} */
-- >   // CRUCIBLE clang_flags: {FLAGS}
-- >   /* CRUX clang_flags: {FLAGS} */
-- >   // CRUX clang_flags: {FLAGS}
--
-- Note that the "clang_flags" portion is case-insensitive, although
-- the "CRUCIBLE" or "CRUX" prefix is case sensitive and must be
-- capitalized.
--
-- All {FLAGS} will be collected as a set of space-separated words.
-- Flags from multiple lines will be concatenated together (without
-- any attempt to eliminate duplicates or conflicts) and the result
-- will be passed as additional flags to the `clang` compilation of
-- the source by Crux.
--
-- The above line matching is whitespace-sensitive and case-sensitive.
-- When C-style comment syntax is used, the comment must be closed on
-- the same line as it was opened (although there is no line length
-- restriction).

crucibleFlagsFromSrc :: FilePath -> IO [String]
crucibleFlagsFromSrc :: String -> IO [String]
crucibleFlagsFromSrc String
srcFile = do
  let marker1 :: [Text]
marker1 = [ Text
"CRUCIBLE ", Text
"CRUX "]
      marker2 :: [Text]
marker2 = [ Text
"clang_flags: " ]
      flagLines :: [Text] -> LogicT Identity Text
flagLines [Text]
fileLines =
        do let eachFrom :: [a] -> LogicT Identity a
eachFrom = (a -> LogicT Identity a -> LogicT Identity a)
-> LogicT Identity a -> [a] -> LogicT Identity a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (LogicT Identity a -> LogicT Identity a -> LogicT Identity a
forall a.
LogicT Identity a -> LogicT Identity a -> LogicT Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (LogicT Identity a -> LogicT Identity a -> LogicT Identity a)
-> (a -> LogicT Identity a)
-> a
-> LogicT Identity a
-> LogicT Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> LogicT Identity a
forall a. a -> LogicT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure) LogicT Identity a
forall a. LogicT Identity a
forall (f :: * -> *) a. Alternative f => f a
empty
           Text
l <- [Text] -> LogicT Identity Text
forall {a}. [a] -> LogicT Identity a
eachFrom [Text]
fileLines
           (Text
pfx, Text
sfx) <- [(Text, Text)] -> LogicT Identity (Text, Text)
forall {a}. [a] -> LogicT Identity a
eachFrom [ (Text
"/* ", Text
" */"), (Text
"// ", Text
"") ]
           Bool -> LogicT Identity ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> LogicT Identity ()) -> Bool -> LogicT Identity ()
forall a b. (a -> b) -> a -> b
$ Text
pfx Text -> Text -> Bool
`T.isPrefixOf` Text
l
           let l1 :: Text
l1 = Int -> Text -> Text
T.drop (Text -> Int
T.length Text
pfx) Text
l
           Bool -> LogicT Identity ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> LogicT Identity ()) -> Bool -> LogicT Identity ()
forall a b. (a -> b) -> a -> b
$ Text
sfx Text -> Text -> Bool
`T.isSuffixOf` Text
l1
           let l2 :: Text
l2 = Int -> Text -> Text
T.take (Text -> Int
T.length Text
l1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Text -> Int
T.length Text
sfx) Text
l1
           Text
m1 <- [Text] -> LogicT Identity Text
forall {a}. [a] -> LogicT Identity a
eachFrom [Text]
marker1
           Bool -> LogicT Identity ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> LogicT Identity ()) -> Bool -> LogicT Identity ()
forall a b. (a -> b) -> a -> b
$ Text
m1 Text -> Text -> Bool
`T.isPrefixOf` Text
l2
           let l3 :: Text
l3 = Int -> Text -> Text
T.drop (Text -> Int
T.length Text
m1) Text
l2
           Text
m2 <- [Text] -> LogicT Identity Text
forall {a}. [a] -> LogicT Identity a
eachFrom [Text]
marker2
           let (Text
l3pfx, Text
l4) = Int -> Text -> (Text, Text)
T.splitAt (Text -> Int
T.length Text
m2) Text
l3
           Bool -> LogicT Identity ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> LogicT Identity ()) -> Bool -> LogicT Identity ()
forall a b. (a -> b) -> a -> b
$ Text -> Text
T.toLower Text
l3pfx Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
m2
           Text -> LogicT Identity Text
forall a. a -> LogicT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Text
l4
    in (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> String
T.unpack ([Text] -> [String]) -> (Text -> [Text]) -> Text -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
       (Text -> [Text]) -> [Text] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> [Text]
T.words ([Text] -> [Text]) -> (Text -> [Text]) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
       LogicT Identity Text -> [Text]
forall a. Logic a -> [a]
observeAll (LogicT Identity Text -> [Text])
-> (Text -> LogicT Identity Text) -> Text -> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> LogicT Identity Text
flagLines ([Text] -> LogicT Identity Text)
-> (Text -> [Text]) -> Text -> LogicT Identity Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
       Text -> [Text]
T.lines (Text -> [String]) -> IO Text -> IO [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
       String -> IO Text
TIO.readFile String
srcFile


makeCounterExamplesLLVM ::
  Crux.Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()
makeCounterExamplesLLVM :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions -> LLVMOptions -> CruxSimulationResult -> IO ()
makeCounterExamplesLLVM CruxOptions
cruxOpts LLVMOptions
llvmOpts CruxSimulationResult
res
  | CruxOptions -> Bool
makeCexes CruxOptions
cruxOpts = ((ProcessedGoals, ProvedGoals) -> IO ())
-> [(ProcessedGoals, ProvedGoals)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ProvedGoals -> IO ()
go (ProvedGoals -> IO ())
-> ((ProcessedGoals, ProvedGoals) -> ProvedGoals)
-> (ProcessedGoals, ProvedGoals)
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProcessedGoals, ProvedGoals) -> ProvedGoals
forall a b. (a, b) -> b
snd) ([(ProcessedGoals, ProvedGoals)] -> IO ())
-> (Seq (ProcessedGoals, ProvedGoals)
    -> [(ProcessedGoals, ProvedGoals)])
-> Seq (ProcessedGoals, ProvedGoals)
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (ProcessedGoals, ProvedGoals)
-> [(ProcessedGoals, ProvedGoals)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList (Seq (ProcessedGoals, ProvedGoals) -> IO ())
-> Seq (ProcessedGoals, ProvedGoals) -> IO ()
forall a b. (a -> b) -> a -> b
$ (CruxSimulationResult -> Seq (ProcessedGoals, ProvedGoals)
cruxSimResultGoals CruxSimulationResult
res)
  | Bool
otherwise = () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

 where
 go :: ProvedGoals -> IO ()
go ProvedGoals
gs =
  case ProvedGoals
gs of
    Branch ProvedGoals
g1 ProvedGoals
g2  -> ProvedGoals -> IO ()
go ProvedGoals
g1 IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ProvedGoals -> IO ()
go ProvedGoals
g2
    -- skip proved goals
    ProvedGoal{} -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- skip unknown goals
    NotProvedGoal [CrucibleAssumption (Const ())]
_ SimError
_ Doc Void
_ [ProgramLoc]
_ Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
Nothing [String]
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- skip resource exhausted goals
    NotProvedGoal [CrucibleAssumption (Const ())]
_ (SimError -> SimErrorReason
simErrorReason -> ResourceExhausted{}) Doc Void
_ [ProgramLoc]
_ Maybe (ModelView, [CrucibleEvent GroundValueWrapper])
_ [String]
_ -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    -- counterexample to non-resource-exhaustion goal
    NotProvedGoal [CrucibleAssumption (Const ())]
_ SimError
c Doc Void
_ [ProgramLoc]
_ (Just (ModelView
m,[CrucibleEvent GroundValueWrapper]
_evs)) [String]
_ ->
      do let suff :: String
suff = case ProgramLoc -> Position
plSourceLoc (SimError -> ProgramLoc
simErrorLoc SimError
c) of
                      SourcePos Text
_ Int
l Int
_ -> Int -> String
forall a. Show a => a -> String
show Int
l
                      Position
_               -> String
"unknown"
         IO (String, String) -> IO (Either SomeException (String, String))
forall e a. Exception e => IO a -> IO (Either e a)
try (CruxOptions
-> LLVMOptions -> String -> String -> IO (String, String)
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions
-> LLVMOptions -> String -> String -> IO (String, String)
buildModelExes CruxOptions
cruxOpts LLVMOptions
llvmOpts String
suff (ModelView -> String
ppModelC ModelView
m)) IO (Either SomeException (String, String))
-> (Either SomeException (String, String) -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
           Left (SomeException
ex :: SomeException) -> do
             ProvedGoals -> IO ()
forall msgs. Logs msgs => ProvedGoals -> IO ()
logGoal ProvedGoals
gs
             CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM CruxLLVMLogMessage
Log.FailedToBuildCounterexampleExecutable
             SomeException -> IO ()
forall msgs. Logs msgs => SomeException -> IO ()
logException SomeException
ex
           Right (String
_prt,String
dbg) -> do
             CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (Text -> CruxLLVMLogMessage
Log.Executable (String -> Text
T.pack String
dbg))
             CruxLLVMLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxLLVMLogMessage -> IO ()
Log.sayCruxLLVM (Text -> CruxLLVMLogMessage
Log.Breakpoint (String -> Text
T.pack String
suff))

buildModelExes ::
  Crux.Logs msgs =>
  Log.SupportsCruxLLVMLogMessage msgs =>
  CruxOptions -> LLVMOptions -> String -> String -> IO (FilePath,FilePath)
buildModelExes :: forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
CruxOptions
-> LLVMOptions -> String -> String -> IO (String, String)
buildModelExes CruxOptions
cruxOpts LLVMOptions
llvmOpts String
suff String
counter_src =
  do let dir :: String
dir  = CruxOptions -> String
Crux.outDir CruxOptions
cruxOpts
     Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dir

     let counterFile :: String
counterFile = String
dir String -> String -> String
</> (String
"counter-example-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suff String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".c")
     let printExe :: String
printExe    = String
dir String -> String -> String
</> (String
"print-model-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suff)
     let debugExe :: String
debugExe    = String
dir String -> String -> String
</> (String
"debug-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suff)
     String -> String -> IO ()
writeFile String
counterFile String
counter_src

     let libs :: String
libs = LLVMOptions -> String
libDir LLVMOptions
llvmOpts
         incs :: [String]
incs = (String
libs String -> String -> String
</> String
"includes") String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
takeDirectory [String]
files [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ LLVMOptions -> [String]
incDirs LLVMOptions
llvmOpts)
         files :: [String]
files = (CruxOptions -> [String]
Crux.inputFiles CruxOptions
cruxOpts)
         libcxx :: [String]
libcxx | [String] -> Bool
anyCPPFiles [String]
files = [String
"-lstdc++"]
                | Bool
otherwise = []

     LLVMOptions -> [String] -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions -> [String] -> IO ()
runClang LLVMOptions
llvmOpts
                   [ String
"-I", String
libs String -> String -> String
</> String
"includes"
                   , String
counterFile
                   , String
libs String -> String -> String
</> String
"print-model.c"
                   , String
"-o", String
printExe
                   ]

     LLVMOptions -> [String] -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLLVMLogMessage msgs) =>
LLVMOptions -> [String] -> IO ()
runClang LLVMOptions
llvmOpts ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$
              [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ String
"-I", String
idir ] | String
idir <- [String]
incs ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
                     [ String
counterFile
                     , String
libs String -> String -> String
</> String
"concrete-backend.c"
                     , String
"-O0", String
"-g"
                     , String
"-o", String
debugExe
                     ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
files [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
libcxx

     (String, String) -> IO (String, String)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
printExe, String
debugExe)


ppValsC :: BaseTypeRepr ty -> Vals ty -> [String]
ppValsC :: forall (ty :: BaseType). BaseTypeRepr ty -> Vals ty -> [String]
ppValsC BaseTypeRepr ty
ty (Vals [Entry (GroundValue ty)]
xs) =
  let (String
cty, String
cnm, GroundValue ty -> String
ppRawVal) = case BaseTypeRepr ty
ty of
        BaseBVRepr NatRepr w
n ->
          (String
"int" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_t", String
"int" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show NatRepr w
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_t", NatRepr w -> BV w -> String
forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> String
showBVLiteral NatRepr w
n)
        BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb)
          | Just eb :~: 8
Refl <- NatRepr eb -> NatRepr 8 -> Maybe (eb :~: 8)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr eb
eb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8)
          , Just sb :~: 24
Refl <- NatRepr sb -> NatRepr 24 -> Maybe (sb :~: 24)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr sb
sb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @24)
          -> (String
"float", String
"float", BigFloat -> String
showFloatLiteral)
        BaseFloatRepr (FloatingPointPrecisionRepr NatRepr eb
eb NatRepr sb
sb)
          | Just eb :~: 11
Refl <- NatRepr eb -> NatRepr 11 -> Maybe (eb :~: 11)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr eb
eb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @11)
          , Just sb :~: 53
Refl <- NatRepr sb -> NatRepr 53 -> Maybe (sb :~: 53)
forall (a :: Natural) (b :: Natural).
NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality NatRepr sb
sb (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @53)
          -> (String
"double", String
"double", BigFloat -> String
showDoubleLiteral)
        BaseTypeRepr ty
BaseRealRepr -> (String
"double", String
"real", (Double -> String
forall a. Show a => a -> String
show (Double -> String) -> (Rational -> Double) -> Rational -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Double
toDouble))

        BaseTypeRepr ty
_ -> String -> (String, String, GroundValue ty -> String)
forall a. HasCallStack => String -> a
error (String
"Type not implemented: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BaseTypeRepr ty -> String
forall a. Show a => a -> String
show BaseTypeRepr ty
ty)
  in  [ String
"size_t const crucible_values_number_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cnm String -> String -> String
forall a. [a] -> [a] -> [a]
++
                String
" = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Entry (GroundValue ty)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Entry (GroundValue ty)]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
";"

      , String
"const char* crucible_names_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"[] = { " String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Entry (GroundValue ty) -> String)
-> [Entry (GroundValue ty)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String
forall a. Show a => a -> String
show (String -> String)
-> (Entry (GroundValue ty) -> String)
-> Entry (GroundValue ty)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry (GroundValue ty) -> String
forall a. Entry a -> String
entryName) [Entry (GroundValue ty)]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" };"

      , String
cty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" const crucible_values_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"[] = { " String -> String -> String
forall a. [a] -> [a] -> [a]
++
            String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Entry (GroundValue ty) -> String)
-> [Entry (GroundValue ty)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (GroundValue ty -> String
ppRawVal (GroundValue ty -> String)
-> (Entry (GroundValue ty) -> GroundValue ty)
-> Entry (GroundValue ty)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Entry (GroundValue ty) -> GroundValue ty
forall a. Entry a -> a
entryValue) [Entry (GroundValue ty)]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" };"
      ]

ppModelC :: ModelView -> String
ppModelC :: ModelView -> String
ppModelC ModelView
m = [String] -> String
unlines
             ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"#include <stdint.h>"
             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"#include <stddef.h>"
             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"#include <math.h>"
             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
""
             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Some BaseTypeRepr -> [String]) -> [Some BaseTypeRepr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Some BaseTypeRepr -> [String]
ppModelForType [Some BaseTypeRepr]
llvmModelTypes
 where
  ppModelForType :: Some BaseTypeRepr -> [String]
ppModelForType (Some BaseTypeRepr x
tpr) =
    case BaseTypeRepr x -> MapF BaseTypeRepr Vals -> Maybe (Vals x)
forall {v} (k :: v -> *) (tp :: v) (a :: v -> *).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup BaseTypeRepr x
tpr (ModelView -> MapF BaseTypeRepr Vals
modelVals ModelView
m) of
      -- NB, produce the declarations even if there are no variables
      Maybe (Vals x)
Nothing   -> BaseTypeRepr x -> Vals x -> [String]
forall (ty :: BaseType). BaseTypeRepr ty -> Vals ty -> [String]
ppValsC BaseTypeRepr x
tpr ([Entry (GroundValue x)] -> Vals x
forall (ty :: BaseType). [Entry (GroundValue ty)] -> Vals ty
Vals [])
      Just Vals x
vals -> BaseTypeRepr x -> Vals x -> [String]
forall (ty :: BaseType). BaseTypeRepr ty -> Vals ty -> [String]
ppValsC BaseTypeRepr x
tpr Vals x
vals


llvmModelTypes :: [Some BaseTypeRepr]
llvmModelTypes :: [Some BaseTypeRepr]
llvmModelTypes =
  [ BaseTypeRepr ('BaseBVType 8) -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (NatRepr 8 -> BaseTypeRepr ('BaseBVType 8)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8))
  , BaseTypeRepr ('BaseBVType 16) -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (NatRepr 16 -> BaseTypeRepr ('BaseBVType 16)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @16))
  , BaseTypeRepr ('BaseBVType 32) -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (NatRepr 32 -> BaseTypeRepr ('BaseBVType 32)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @32))
  , BaseTypeRepr ('BaseBVType 64) -> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (NatRepr 64 -> BaseTypeRepr ('BaseBVType 64)
forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @64))
  , BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision 8 24))
-> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (FloatPrecisionRepr ('FloatingPointPrecision 8 24)
-> BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision 8 24))
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr (NatRepr 8
-> NatRepr 24 -> FloatPrecisionRepr ('FloatingPointPrecision 8 24)
forall (eb :: Natural) (sb :: Natural).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @8) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @24)))
  , BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision 11 53))
-> Some BaseTypeRepr
forall k (f :: k -> *) (x :: k). f x -> Some f
Some (FloatPrecisionRepr ('FloatingPointPrecision 11 53)
-> BaseTypeRepr ('BaseFloatType ('FloatingPointPrecision 11 53))
forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp -> BaseTypeRepr ('BaseFloatType fpp)
BaseFloatRepr (NatRepr 11
-> NatRepr 53 -> FloatPrecisionRepr ('FloatingPointPrecision 11 53)
forall (eb :: Natural) (sb :: Natural).
(2 <= eb, 2 <= sb) =>
NatRepr eb
-> NatRepr sb -> FloatPrecisionRepr ('FloatingPointPrecision eb sb)
FloatingPointPrecisionRepr (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @11) (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @53)))
  ]