{-# LANGUAGE QuasiQuotes #-}

-- | C code generator.  This module can convert a correct ImpCode
-- program to an equivalent ISPC program.
module Futhark.CodeGen.Backends.MulticoreISPC
  ( compileProg,
    GC.CParts (..),
    GC.asLibrary,
    GC.asExecutable,
    GC.asServer,
    operations,
    ISPCState,
  )
where

import Control.Lens (each, over)
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State
import Data.Bifunctor
import Data.DList qualified as DL
import Data.List (unzip4)
import Data.Loc (noLoc)
import Data.Map qualified as M
import Data.Maybe
import Data.Text qualified as T
import Futhark.CodeGen.Backends.GenericC qualified as GC
import Futhark.CodeGen.Backends.GenericC.Pretty
import Futhark.CodeGen.Backends.MulticoreC qualified as MC
import Futhark.CodeGen.Backends.MulticoreC.Boilerplate (generateBoilerplate)
import Futhark.CodeGen.Backends.SimpleRep
import Futhark.CodeGen.ImpCode.Multicore
import Futhark.CodeGen.ImpGen.Multicore qualified as ImpGen
import Futhark.CodeGen.RTS.C (errorsH, ispcUtilH, uniformH)
import Futhark.IR.MCMem (MCMem, Prog)
import Futhark.IR.Prop (isBuiltInFunction)
import Futhark.MonadFreshNames
import Language.C.Quote.OpenCL qualified as C
import Language.C.Syntax qualified as C
import NeatInterpolation (untrimming)

type ISPCCompilerM a = GC.CompilerM Multicore ISPCState a

-- | Transient state tracked by the ISPC backend.
data ISPCState = ISPCState
  { ISPCState -> DList Definition
sDefs :: DL.DList C.Definition,
    ISPCState -> Names
sUniform :: Names
  }

uniform :: C.TypeQual
uniform :: TypeQual
uniform = String -> SrcLoc -> TypeQual
C.EscTypeQual String
"uniform" forall a. IsLocation a => a
noLoc

unmasked :: C.TypeQual
unmasked :: TypeQual
unmasked = String -> SrcLoc -> TypeQual
C.EscTypeQual String
"unmasked" forall a. IsLocation a => a
noLoc

export :: C.TypeQual
export :: TypeQual
export = String -> SrcLoc -> TypeQual
C.EscTypeQual String
"export" forall a. IsLocation a => a
noLoc

varying :: C.TypeQual
varying :: TypeQual
varying = String -> SrcLoc -> TypeQual
C.EscTypeQual String
"varying" forall a. IsLocation a => a
noLoc

-- | Compile the program to C and ISPC code using multicore operations.
compileProg ::
  MonadFreshNames m => T.Text -> Prog MCMem -> m (ImpGen.Warnings, (GC.CParts, T.Text))
compileProg :: forall (m :: * -> *).
MonadFreshNames m =>
Text -> Prog MCMem -> m (Warnings, (CParts, Text))
compileProg Text
version Prog MCMem
prog = do
  -- Dynamic scheduling seems completely broken currently, so we disable it.
  (Warnings
ws, Definitions Multicore
defs) <- forall (m :: * -> *).
MonadFreshNames m =>
Prog MCMem -> m (Warnings, Definitions Multicore)
ImpGen.compileProg Prog MCMem
prog
  let Functions [(Name, Function Multicore)]
funs = forall a. Definitions a -> Functions a
defFuns Definitions Multicore
defs

  (Warnings
ws', (CParts
cparts, CompilerState ISPCState
endstate)) <-
    forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse
      ( forall (m :: * -> *) op s.
MonadFreshNames m =>
Text
-> Text
-> ParamMap
-> Operations op s
-> s
-> CompilerM op s ()
-> Text
-> (Space, [Space])
-> [Option]
-> Definitions op
-> m (CParts, CompilerState s)
GC.compileProg'
          Text
"ispc"
          Text
version
          forall a. Monoid a => a
mempty
          Operations Multicore ISPCState
operations
          (DList Definition -> Names -> ISPCState
ISPCState forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty)
          ( do
              forall op s. CompilerM op s ()
generateBoilerplate
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op. (Name, Function op) -> CompilerM Multicore ISPCState ()
compileBuiltinFun [(Name, Function Multicore)]
funs
          )
          forall a. Monoid a => a
mempty
          (Space
DefaultSpace, [Space
DefaultSpace])
          [Option]
MC.cliOptions
      )
      (Warnings
ws, Definitions Multicore
defs)

  let ispc_decls :: Text
ispc_decls = [Definition] -> Text
definitionsText forall a b. (a -> b) -> a -> b
$ forall a. DList a -> [a]
DL.toList forall a b. (a -> b) -> a -> b
$ ISPCState -> DList Definition
sDefs forall a b. (a -> b) -> a -> b
$ forall s. CompilerState s -> s
GC.compUserState CompilerState ISPCState
endstate

  -- The bool #define is a workaround around an ISPC bug, stdbool doesn't get included.
  let ispcdefs :: Text
ispcdefs =
        [untrimming|
#define bool uint8
typedef int64 int64_t;
typedef int32 int32_t;
typedef int16 int16_t;
typedef int8 int8_t;
typedef int8 char;
typedef unsigned int64 uint64_t;
typedef unsigned int32 uint32_t;
typedef unsigned int16 uint16_t;
typedef unsigned int8 uint8_t;
#define volatile

$errorsH

#define INFINITY (floatbits((uniform int)0x7f800000))
#define NAN (floatbits((uniform int)0x7fc00000))
#define fabs(x) abs(x)
#define FUTHARK_F64_ENABLED
$cScalarDefs

$uniformH

$ispcUtilH

$ispc_decls|]

  forall (f :: * -> *) a. Applicative f => a -> f a
pure (Warnings
ws', (CParts
cparts, Text
ispcdefs))

-- | Compiler operations specific to the ISPC multicore backend.
operations :: GC.Operations Multicore ISPCState
operations :: Operations Multicore ISPCState
operations =
  forall s. Operations Multicore s
MC.operations
    { opsCompiler :: OpCompiler Multicore ISPCState
GC.opsCompiler = OpCompiler Multicore ISPCState
compileOp
    }

ispcDecl :: C.Definition -> ISPCCompilerM ()
ispcDecl :: Definition -> CompilerM Multicore ISPCState ()
ispcDecl Definition
def =
  forall s op. (s -> s) -> CompilerM op s ()
GC.modifyUserState (\ISPCState
s -> ISPCState
s {sDefs :: DList Definition
sDefs = ISPCState -> DList Definition
sDefs ISPCState
s forall a. Semigroup a => a -> a -> a
<> forall a. a -> DList a
DL.singleton Definition
def})

ispcEarlyDecl :: C.Definition -> ISPCCompilerM ()
ispcEarlyDecl :: Definition -> CompilerM Multicore ISPCState ()
ispcEarlyDecl Definition
def =
  forall s op. (s -> s) -> CompilerM op s ()
GC.modifyUserState (\ISPCState
s -> ISPCState
s {sDefs :: DList Definition
sDefs = forall a. a -> DList a
DL.singleton Definition
def forall a. Semigroup a => a -> a -> a
<> ISPCState -> DList Definition
sDefs ISPCState
s})

ispcDef :: MC.DefSpecifier ISPCState
ispcDef :: DefSpecifier ISPCState
ispcDef String
s Name -> CompilerM Multicore ISPCState Definition
f = do
  Name
s' <- forall op s. String -> CompilerM op s Name
MC.multicoreName String
s
  Definition -> CompilerM Multicore ISPCState ()
ispcDecl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> CompilerM Multicore ISPCState Definition
f Name
s'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
s'

-- | Expose a struct to both ISPC and C.
sharedDef :: MC.DefSpecifier ISPCState
sharedDef :: DefSpecifier ISPCState
sharedDef String
s Name -> CompilerM Multicore ISPCState Definition
f = do
  Name
s' <- forall op s. String -> CompilerM op s Name
MC.multicoreName String
s
  Definition -> CompilerM Multicore ISPCState ()
ispcDecl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> CompilerM Multicore ISPCState Definition
f Name
s'
  forall op s. Definition -> CompilerM op s ()
GC.earlyDecl forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> CompilerM Multicore ISPCState Definition
f Name
s'
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
s'

-- | Copy memory where one of the operands is using an AoS layout.
copyMemoryAOS ::
  PrimType ->
  C.Exp ->
  C.Exp ->
  C.Exp ->
  C.Exp ->
  C.Exp ->
  GC.CompilerM op s ()
copyMemoryAOS :: forall op s.
PrimType -> Exp -> Exp -> Exp -> Exp -> Exp -> CompilerM op s ()
copyMemoryAOS PrimType
pt Exp
destmem Exp
destidx Exp
srcmem Exp
srcidx Exp
nbytes =
  forall op s. Stm -> CompilerM op s ()
GC.stm
    [C.cstm|if ($exp:nbytes > 0) {
              $id:overload($exp:destmem + $exp:destidx,
                      $exp:srcmem + $exp:srcidx,
                      extract($exp:nbytes, 0));
            }|]
  where
    size :: String
size = forall a. Show a => a -> String
show (Integer
8 forall a. Num a => a -> a -> a
* forall a. Num a => PrimType -> a
primByteSize PrimType
pt :: Integer)
    overload :: String
overload = String
"memmove_" forall a. Semigroup a => a -> a -> a
<> String
size

-- | ISPC has no string literals, so this makes one in C and exposes it via an
-- external function, returning the name.
makeStringLiteral :: String -> ISPCCompilerM Name
makeStringLiteral :: String -> CompilerM Multicore ISPCState Name
makeStringLiteral String
str = do
  Name
name <- forall s. DefSpecifier s
MC.multicoreDef String
"strlit_shim" forall a b. (a -> b) -> a -> b
$ \Name
s ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cedecl|char* $id:s() { return $string:str; }|]
  Definition -> CompilerM Multicore ISPCState ()
ispcDecl
    [C.cedecl|extern "C" $tyqual:unmasked $tyqual:uniform char* $tyqual:uniform $id:name();|]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
name

-- | Set memory in ISPC
setMem :: (C.ToExp a, C.ToExp b) => a -> b -> Space -> ISPCCompilerM ()
setMem :: forall a b.
(ToExp a, ToExp b) =>
a -> b -> Space -> CompilerM Multicore ISPCState ()
setMem a
dest b
src Space
space = do
  let src_s :: String
src_s = Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Exp -> Text
expText forall a b. (a -> b) -> a -> b
$ forall a. ToExp a => a -> SrcLoc -> Exp
C.toExp b
src forall a. IsLocation a => a
noLoc
  Name
strlit <- String -> CompilerM Multicore ISPCState Name
makeStringLiteral String
src_s
  forall op s. Stm -> CompilerM op s ()
GC.stm
    [C.cstm|if ($id:(GC.fatMemSet space)(ctx, &$exp:dest, &$exp:src,
                                            $id:strlit()) != 0) {
                    $escstm:("unmasked { return 1; }")
                  }|]

-- | Unref memory in ISPC
unRefMem :: C.ToExp a => a -> Space -> ISPCCompilerM ()
unRefMem :: forall a. ToExp a => a -> Space -> CompilerM Multicore ISPCState ()
unRefMem a
mem Space
space = do
  Bool
cached <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem a
mem
  let mem_s :: String
mem_s = Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Exp -> Text
expText forall a b. (a -> b) -> a -> b
$ forall a. ToExp a => a -> SrcLoc -> Exp
C.toExp a
mem forall a. IsLocation a => a
noLoc
  Name
strlit <- String -> CompilerM Multicore ISPCState Name
makeStringLiteral String
mem_s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
cached forall a b. (a -> b) -> a -> b
$
    forall op s. Stm -> CompilerM op s ()
GC.stm
      [C.cstm|if ($id:(GC.fatMemUnRef space)(ctx, &$exp:mem, $id:strlit()) != 0) {
                  $escstm:("unmasked { return 1; }")
                }|]

-- | Allocate memory in ISPC
allocMem ::
  (C.ToExp a, C.ToExp b) =>
  a ->
  b ->
  Space ->
  C.Stm ->
  ISPCCompilerM ()
allocMem :: forall a b.
(ToExp a, ToExp b) =>
a -> b -> Space -> Stm -> CompilerM Multicore ISPCState ()
allocMem a
mem b
size Space
space Stm
on_failure = do
  let mem_s :: String
mem_s = Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Exp -> Text
expText forall a b. (a -> b) -> a -> b
$ forall a. ToExp a => a -> SrcLoc -> Exp
C.toExp a
mem forall a. IsLocation a => a
noLoc
  Name
strlit <- String -> CompilerM Multicore ISPCState Name
makeStringLiteral String
mem_s
  forall op s. Stm -> CompilerM op s ()
GC.stm
    [C.cstm|if ($id:(GC.fatMemAlloc space)(ctx, &$exp:mem, $exp:size, $id:strlit())) {
                    $stm:on_failure
            }|]

-- | Free memory in ISPC
freeAllocatedMem :: ISPCCompilerM [C.BlockItem]
freeAllocatedMem :: ISPCCompilerM [BlockItem]
freeAllocatedMem = forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. ToExp a => a -> Space -> CompilerM Multicore ISPCState ()
unRefMem) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall s. CompilerState s -> [(VName, Space)]
GC.compDeclaredMem

-- | Given a ImpCode function, generate all the required machinery for calling
-- it in ISPC, both in a varying or uniform context. This involves handling
-- for the fact that ISPC cannot pass structs by value to external functions.
compileBuiltinFun :: (Name, Function op) -> ISPCCompilerM ()
compileBuiltinFun :: forall op. (Name, Function op) -> CompilerM Multicore ISPCState ()
compileBuiltinFun (Name
fname, func :: Function op
func@(Function Maybe EntryPoint
_ [Param]
outputs [Param]
inputs Code op
_))
  | forall a. Maybe a -> Bool
isNothing forall a b. (a -> b) -> a -> b
$ forall a. FunctionT a -> Maybe EntryPoint
functionEntry Function op
func = do
      let extra :: [Param]
extra = [[C.cparam|$tyqual:uniform struct futhark_context * $tyqual:uniform ctx|]]
          extra_c :: [Param]
extra_c = [[C.cparam|struct futhark_context * ctx|]]
          extra_exp :: [Exp]
extra_exp = [[C.cexp|$id:p|] | C.Param (Just Id
p) DeclSpec
_ Decl
_ SrcLoc
_ <- [Param]
extra]

      ([Param]
inparams_c, [Exp]
in_args_c) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (forall {op} {s}. [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileInputsExtern []) [Param]
inputs
      ([Param]
outparams_c, [Exp]
out_args_c) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (forall {op} {s}. [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileOutputsExtern []) [Param]
outputs

      ([Param]
inparams_extern, [Exp]
_) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (forall {op} {s}. [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileInputsExtern [C.ctyquals|$tyqual:uniform|]) [Param]
inputs
      ([Param]
outparams_extern, [Exp]
_) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (forall {op} {s}. [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileOutputsExtern [C.ctyquals|$tyqual:uniform|]) [Param]
outputs

      ([Param]
inparams_uni, [Exp]
in_args_noderef) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM forall {op} {s}. Param -> CompilerM op s (Param, Exp)
compileInputsUniform [Param]
inputs
      ([Param]
outparams_uni, [Exp]
out_args_noderef) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM forall {op} {s}. Param -> CompilerM op s (Param, Exp)
compileOutputsUniform [Param]
outputs

      ([Param]
inparams_varying, [Exp]
in_args_vary, [[BlockItem]]
prebody_in') <- forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {op} {s}. Param -> CompilerM op s (Param, Exp, [BlockItem])
compileInputsVarying [Param]
inputs
      ([Param]
outparams_varying, [Exp]
out_args_vary, [[BlockItem]]
prebody_out', [[BlockItem]]
postbody_out') <- forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {op} {s}.
Param -> CompilerM op s (Param, Exp, [BlockItem], [BlockItem])
compileOutputsVarying [Param]
outputs
      let ([BlockItem]
prebody_in, [BlockItem]
prebody_out, [BlockItem]
postbody_out) = forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over forall s t a b. Each s t a b => Traversal s t a b
each forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[BlockItem]]
prebody_in', [[BlockItem]]
prebody_out', [[BlockItem]]
postbody_out')

      forall op s. Definition -> CompilerM op s ()
GC.libDecl
        [C.cedecl|int $id:(funName fname <> "_extern")($params:extra_c, $params:outparams_c, $params:inparams_c) {
                  return $id:(funName fname)($args:extra_exp, $args:out_args_c, $args:in_args_c);
                }|]

      let ispc_extern :: Definition
ispc_extern =
            [C.cedecl|extern "C" $tyqual:unmasked $tyqual:uniform int $id:((funName fname) <> "_extern")
                      ($params:extra, $params:outparams_extern, $params:inparams_extern);|]

          ispc_uniform :: Definition
ispc_uniform =
            [C.cedecl|$tyqual:uniform int $id:(funName fname)
                    ($params:extra, $params:outparams_uni, $params:inparams_uni) {
                      return $id:(funName (fname<>"_extern"))(
                        $args:extra_exp,
                        $args:out_args_noderef,
                        $args:in_args_noderef);
                    }|]

          ispc_varying :: Definition
ispc_varying =
            [C.cedecl|$tyqual:uniform int $id:(funName fname)
                    ($params:extra, $params:outparams_varying, $params:inparams_varying) {
                        $tyqual:uniform int err = 0;
                        $items:prebody_in
                        $items:prebody_out
                        $escstm:("foreach_active (i)")
                        {
                          err |= $id:(funName $ fname<>"_extern")(
                            $args:extra_exp,
                            $args:out_args_vary,
                            $args:in_args_vary);
                        }
                        $items:postbody_out
                        return err;
                    }|]

      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Definition -> CompilerM Multicore ISPCState ()
ispcEarlyDecl [Definition
ispc_varying, Definition
ispc_uniform, Definition
ispc_extern]
  | Bool
otherwise = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    compileInputsExtern :: [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileInputsExtern [TypeQual]
vari (ScalarParam VName
name PrimType
bt) = do
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([C.cparam|$tyquals:vari $ty:ctp $id:name|], [C.cexp|$id:name|])
    compileInputsExtern [TypeQual]
vari (MemParam VName
name Space
space) = do
      Type
ty <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([C.cparam|$tyquals:vari $ty:ty * $tyquals:vari $id:name|], [C.cexp|*$id:name|])

    compileOutputsExtern :: [TypeQual] -> Param -> CompilerM op s (Param, Exp)
compileOutputsExtern [TypeQual]
vari (ScalarParam VName
name PrimType
bt) = do
      VName
p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"out_" forall a. [a] -> [a] -> [a]
++ VName -> String
baseString VName
name
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([C.cparam|$tyquals:vari $ty:ctp * $tyquals:vari $id:p_name|], [C.cexp|$id:p_name|])
    compileOutputsExtern [TypeQual]
vari (MemParam VName
name Space
space) = do
      Type
ty <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      VName
p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ VName -> String
baseString VName
name forall a. [a] -> [a] -> [a]
++ String
"_p"
      forall (f :: * -> *) a. Applicative f => a -> f a
pure ([C.cparam|$tyquals:vari $ty:ty * $tyquals:vari $id:p_name|], [C.cexp|$id:p_name|])

    compileInputsUniform :: Param -> CompilerM op s (Param, Exp)
compileInputsUniform (ScalarParam VName
name PrimType
bt) = do
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
          params :: Param
params = [C.cparam|$tyqual:uniform $ty:ctp $id:name|]
          args :: Exp
args = [C.cexp|$id:name|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args)
    compileInputsUniform (MemParam VName
name Space
space) = do
      Type
ty <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      let params :: Param
params = [C.cparam|$tyqual:uniform $ty:ty $id:name|]
          args :: Exp
args = [C.cexp|&$id:name|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args)

    compileOutputsUniform :: Param -> CompilerM op s (Param, Exp)
compileOutputsUniform (ScalarParam VName
name PrimType
bt) = do
      VName
p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"out_" forall a. [a] -> [a] -> [a]
++ VName -> String
baseString VName
name
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
          params :: Param
params = [C.cparam|$tyqual:uniform $ty:ctp *$tyqual:uniform $id:p_name|]
          args :: Exp
args = [C.cexp|$id:p_name|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args)
    compileOutputsUniform (MemParam VName
name Space
space) = do
      Type
ty <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      VName
p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ VName -> String
baseString VName
name forall a. [a] -> [a] -> [a]
++ String
"_p"
      let params :: Param
params = [C.cparam|$tyqual:uniform $ty:ty $id:p_name|]
          args :: Exp
args = [C.cexp|&$id:p_name|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args)

    compileInputsVarying :: Param -> CompilerM op s (Param, Exp, [BlockItem])
compileInputsVarying (ScalarParam VName
name PrimType
bt) = do
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
          params :: Param
params = [C.cparam|$ty:ctp $id:name|]
          args :: Exp
args = [C.cexp|extract($id:name,i)|]
          pre_body :: [a]
pre_body = []
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args, forall a. [a]
pre_body)
    compileInputsVarying (MemParam VName
name Space
space) = do
      Type
typ <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      VName
newvn <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"aos_" forall a. Semigroup a => a -> a -> a
<> VName -> String
baseString VName
name
      let params :: Param
params = [C.cparam|$ty:typ $id:name|]
          args :: Exp
args = [C.cexp|&$id:(newvn)[i]|]
          pre_body :: [BlockItem]
pre_body =
            [C.citems|$tyqual:uniform $ty:typ $id:(newvn)[programCount];
                               $id:(newvn)[programIndex] = $id:name;|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args, [BlockItem]
pre_body)

    compileOutputsVarying :: Param -> CompilerM op s (Param, Exp, [BlockItem], [BlockItem])
compileOutputsVarying (ScalarParam VName
name PrimType
bt) = do
      VName
p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"out_" forall a. [a] -> [a] -> [a]
++ VName -> String
baseString VName
name
      VName
deref_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"aos_" forall a. [a] -> [a] -> [a]
++ VName -> String
baseString VName
name
      VName
vari_p_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"convert_" forall a. [a] -> [a] -> [a]
++ VName -> String
baseString VName
name
      let ctp :: Type
ctp = PrimType -> Type
GC.primTypeToCType PrimType
bt
          pre_body :: [BlockItem]
pre_body =
            [C.citems|$tyqual:varying $ty:ctp $id:vari_p_name = *$id:p_name;
                                $tyqual:uniform $ty:ctp $id:deref_name[programCount];
                                $id:deref_name[programIndex] = $id:vari_p_name;|]
          post_body :: [BlockItem]
post_body = [C.citems|*$id:p_name = $id:(deref_name)[programIndex];|]
          params :: Param
params = [C.cparam|$tyqual:varying $ty:ctp * $tyqual:uniform $id:p_name|]
          args :: Exp
args = [C.cexp|&$id:(deref_name)[i]|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args, [BlockItem]
pre_body, [BlockItem]
post_body)
    compileOutputsVarying (MemParam VName
name Space
space) = do
      Type
typ <- forall op s. VName -> Space -> CompilerM op s Type
GC.memToCType VName
name Space
space
      VName
newvn <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ String
"aos_" forall a. Semigroup a => a -> a -> a
<> VName -> String
baseString VName
name
      let params :: Param
params = [C.cparam|$ty:typ $id:name|]
          args :: Exp
args = [C.cexp|&$id:(newvn)[i]|]
          pre_body :: [BlockItem]
pre_body =
            [C.citems|$tyqual:uniform $ty:typ $id:(newvn)[programCount];
                       $id:(newvn)[programIndex] = $id:name;|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Param
params, Exp
args, [BlockItem]
pre_body, [])

-- | Handle logging an error message in ISPC.
handleError :: ErrorMsg Exp -> String -> ISPCCompilerM ()
handleError :: ErrorMsg Exp -> String -> CompilerM Multicore ISPCState ()
handleError ErrorMsg Exp
msg String
stacktrace = do
  -- Get format sting
  (String
formatstr, [Exp]
formatargs) <- forall op s. ErrorMsg Exp -> CompilerM op s (String, [Exp])
GC.errorMsgString ErrorMsg Exp
msg
  let formatstr' :: String
formatstr' = String
"Error: " forall a. Semigroup a => a -> a -> a
<> String
formatstr forall a. Semigroup a => a -> a -> a
<> String
"\n\nBacktrace:\n%s"
  -- Get args types and names for shim
  let arg_types :: [PrimType]
arg_types = forall a. ErrorMsg a -> [PrimType]
errorMsgArgTypes ErrorMsg Exp
msg
  [VName]
arg_names <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const String
"arg") [PrimType]
arg_types
  let params :: [Param]
params = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\PrimType
ty VName
name -> [C.cparam|$ty:(GC.primTypeToCType ty) $id:name|]) [PrimType]
arg_types [VName]
arg_names
  let params_uni :: [Param]
params_uni = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\PrimType
ty VName
name -> [C.cparam|$tyqual:uniform $ty:(GC.primTypeToCType ty) $id:name|]) [PrimType]
arg_types [VName]
arg_names
  -- Make shim
  let formatargs' :: [Exp]
formatargs' = forall {a} {a}. ToIdent a => ErrorMsg a -> [Exp] -> [a] -> [Exp]
mapArgNames ErrorMsg Exp
msg [Exp]
formatargs [VName]
arg_names
  Name
shim <- forall s. DefSpecifier s
MC.multicoreDef String
"assert_shim" forall a b. (a -> b) -> a -> b
$ \Name
s -> do
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      [C.cedecl|void $id:s(struct futhark_context* ctx, $params:params) {
          set_error(ctx, msgprintf($string:formatstr', $args:formatargs', $string:stacktrace));
      }|]
  Definition -> CompilerM Multicore ISPCState ()
ispcDecl
    [C.cedecl|extern "C" $tyqual:unmasked void $id:shim($tyqual:uniform struct futhark_context* $tyqual:uniform, $params:params_uni);|]
  -- Call the shim
  [Exp]
args <- ErrorMsg Exp -> CompilerM Multicore ISPCState [Exp]
getErrorValExps ErrorMsg Exp
msg
  VName
uni <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName String
"uni"
  let args' :: [Exp]
args' = forall a b. (a -> b) -> [a] -> [b]
map (\Exp
x -> [C.cexp|extract($exp:x, $id:uni)|]) [Exp]
args
  forall op s. [BlockItem] -> CompilerM op s ()
GC.items
    [C.citems|
      $escstm:("foreach_active(" <> prettyString uni <> ")")
      {
        $id:shim(ctx, $args:args');
        err = FUTHARK_PROGRAM_ERROR;
      }
      $escstm:("unmasked { return err; }")|]
  where
    getErrorVal :: ErrorMsgPart a -> Maybe a
getErrorVal (ErrorString Text
_) = forall a. Maybe a
Nothing
    getErrorVal (ErrorVal PrimType
_ a
v) = forall a. a -> Maybe a
Just a
v

    getErrorValExps :: ErrorMsg Exp -> CompilerM Multicore ISPCState [Exp]
getErrorValExps (ErrorMsg [ErrorMsgPart Exp]
m) = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Exp -> ISPCCompilerM Exp
compileExp forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {a}. ErrorMsgPart a -> Maybe a
getErrorVal [ErrorMsgPart Exp]
m

    mapArgNames' :: [ErrorMsgPart a] -> [Exp] -> [a] -> [Exp]
mapArgNames' (ErrorMsgPart a
x : [ErrorMsgPart a]
xs) (Exp
y : [Exp]
ys) (a
t : [a]
ts)
      | forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ forall {a}. ErrorMsgPart a -> Maybe a
getErrorVal ErrorMsgPart a
x = [C.cexp|$id:t|] forall a. a -> [a] -> [a]
: [ErrorMsgPart a] -> [Exp] -> [a] -> [Exp]
mapArgNames' [ErrorMsgPart a]
xs [Exp]
ys [a]
ts
      | Bool
otherwise = Exp
y forall a. a -> [a] -> [a]
: [ErrorMsgPart a] -> [Exp] -> [a] -> [Exp]
mapArgNames' [ErrorMsgPart a]
xs [Exp]
ys (a
t forall a. a -> [a] -> [a]
: [a]
ts)
    mapArgNames' [ErrorMsgPart a]
_ [Exp]
ys [] = [Exp]
ys
    mapArgNames' [ErrorMsgPart a]
_ [Exp]
_ [a]
_ = []

    mapArgNames :: ErrorMsg a -> [Exp] -> [a] -> [Exp]
mapArgNames (ErrorMsg [ErrorMsgPart a]
parts) = forall {a} {a}.
ToIdent a =>
[ErrorMsgPart a] -> [Exp] -> [a] -> [Exp]
mapArgNames' [ErrorMsgPart a]
parts

-- | Given the name and type of a parameter, return the C type used to
-- represent it. We use uniform pointers to varying values for lexical
-- memory blocks, as this generally results in less gathers/scatters.
getMemType :: VName -> PrimType -> ISPCCompilerM C.Type
getMemType :: VName -> PrimType -> ISPCCompilerM Type
getMemType VName
dest PrimType
elemtype = do
  Bool
cached <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
dest
  if Bool
cached
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cty|$tyqual:varying $ty:(primStorageType elemtype)* uniform|]
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cty|$ty:(primStorageType elemtype)*|]

compileExp :: Exp -> ISPCCompilerM C.Exp
compileExp :: Exp -> ISPCCompilerM Exp
compileExp e :: Exp
e@(ValueExp (FloatValue (Float64Value Double
v))) =
  if forall a. RealFloat a => a -> Bool
isInfinite Double
v Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isNaN Double
v
    then forall op s. Exp -> CompilerM op s Exp
GC.compileExp Exp
e
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$esc:(prettyString v <> "d")|]
compileExp e :: Exp
e@(ValueExp (FloatValue (Float16Value Half
v))) =
  if forall a. RealFloat a => a -> Bool
isInfinite Half
v Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isNaN Half
v
    then forall op s. Exp -> CompilerM op s Exp
GC.compileExp Exp
e
    else forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$esc:(prettyString v <> "f16")|]
compileExp (ValueExp PrimValue
val) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. ToExp a => a -> SrcLoc -> Exp
C.toExp PrimValue
val forall a. Monoid a => a
mempty
compileExp (LeafExp VName
v PrimType
_) =
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$id:v|]
compileExp (UnOpExp Complement {} Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|~$exp:x'|]
compileExp (UnOpExp Not {} Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|!$exp:x'|]
compileExp (UnOpExp (FAbs FloatType
Float32) Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|(float)fabs($exp:x')|]
compileExp (UnOpExp (FAbs FloatType
Float64) Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|fabs($exp:x')|]
compileExp (UnOpExp SSignum {} Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|($exp:x' > 0 ? 1 : 0) - ($exp:x' < 0 ? 1 : 0)|]
compileExp (UnOpExp USignum {} Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|($exp:x' > 0 ? 1 : 0) - ($exp:x' < 0 ? 1 : 0) != 0|]
compileExp (UnOpExp UnOp
op Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$id:(prettyString op)($exp:x')|]
compileExp (CmpOpExp CmpOp
cmp Exp
x Exp
y) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  Exp
y' <- Exp -> ISPCCompilerM Exp
compileExp Exp
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case CmpOp
cmp of
    CmpEq {} -> [C.cexp|$exp:x' == $exp:y'|]
    FCmpLt {} -> [C.cexp|$exp:x' < $exp:y'|]
    FCmpLe {} -> [C.cexp|$exp:x' <= $exp:y'|]
    CmpLlt {} -> [C.cexp|$exp:x' < $exp:y'|]
    CmpLle {} -> [C.cexp|$exp:x' <= $exp:y'|]
    CmpOp
_ -> [C.cexp|$id:(prettyString cmp)($exp:x', $exp:y')|]
compileExp (ConvOpExp ConvOp
conv Exp
x) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$id:(prettyString conv)($exp:x')|]
compileExp (BinOpExp BinOp
bop Exp
x Exp
y) = do
  Exp
x' <- Exp -> ISPCCompilerM Exp
compileExp Exp
x
  Exp
y' <- Exp -> ISPCCompilerM Exp
compileExp Exp
y
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ case BinOp
bop of
    Add IntType
_ Overflow
OverflowUndef -> [C.cexp|$exp:x' + $exp:y'|]
    Sub IntType
_ Overflow
OverflowUndef -> [C.cexp|$exp:x' - $exp:y'|]
    Mul IntType
_ Overflow
OverflowUndef -> [C.cexp|$exp:x' * $exp:y'|]
    FAdd {} -> [C.cexp|$exp:x' + $exp:y'|]
    FSub {} -> [C.cexp|$exp:x' - $exp:y'|]
    FMul {} -> [C.cexp|$exp:x' * $exp:y'|]
    FDiv {} -> [C.cexp|$exp:x' / $exp:y'|]
    Xor {} -> [C.cexp|$exp:x' ^ $exp:y'|]
    And {} -> [C.cexp|$exp:x' & $exp:y'|]
    Or {} -> [C.cexp|$exp:x' | $exp:y'|]
    LogAnd {} -> [C.cexp|$exp:x' && $exp:y'|]
    LogOr {} -> [C.cexp|$exp:x' || $exp:y'|]
    BinOp
_ -> [C.cexp|$id:(prettyString bop)($exp:x', $exp:y')|]
compileExp (FunExp String
h [Exp]
args PrimType
_) = do
  [Exp]
args' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Exp -> ISPCCompilerM Exp
compileExp [Exp]
args
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cexp|$id:(funName (nameFromString h))($args:args')|]

-- | Compile a block of code with ISPC specific semantics, falling back
-- to generic C when this semantics is not needed.
-- All recursive constructors are duplicated here, since not doing so
-- would cause use to enter regular generic C codegen with no escape.
compileCode :: MCCode -> ISPCCompilerM ()
compileCode :: MCCode -> CompilerM Multicore ISPCState ()
compileCode (Comment Text
s MCCode
code) = do
  [BlockItem]
xs <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
code
  let comment :: String
comment = String
"// " forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
s
  forall op s. Stm -> CompilerM op s ()
GC.stm
    [C.cstm|$comment:comment
              { $items:xs }
             |]
compileCode (DeclareScalar VName
name Volatility
_ PrimType
t) = do
  let ct :: Type
ct = PrimType -> Type
GC.primTypeToCType PrimType
t
  [TypeQual]
quals <- VName -> ISPCCompilerM [TypeQual]
getVariabilityQuals VName
name
  forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyquals:quals $ty:ct $id:name;|]
compileCode (DeclareArray VName
name PrimType
t ArrayContents
vs) = do
  VName
name_realtype <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ VName -> String
baseString VName
name forall a. [a] -> [a] -> [a]
++ String
"_realtype"
  let ct :: Type
ct = PrimType -> Type
GC.primTypeToCType PrimType
t
  case ArrayContents
vs of
    ArrayValues [PrimValue]
vs' -> do
      let vs'' :: [Initializer]
vs'' = [[C.cinit|$exp:v|] | PrimValue
v <- [PrimValue]
vs']
      forall op s. Definition -> CompilerM op s ()
GC.earlyDecl [C.cedecl|static $ty:ct $id:name_realtype[$int:(length vs')] = {$inits:vs''};|]
    ArrayZeros Int
n ->
      forall op s. Definition -> CompilerM op s ()
GC.earlyDecl [C.cedecl|static $ty:ct $id:name_realtype[$int:n];|]
  -- Make an exported C shim to access a faked memory block.
  Name
shim <- forall s. DefSpecifier s
MC.multicoreDef String
"get_static_array_shim" forall a b. (a -> b) -> a -> b
$ \Name
f ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      [C.cedecl|struct memblock $id:f(struct futhark_context* ctx) {
                  return (struct memblock){NULL,(unsigned char*)$id:name_realtype,0};
                }|]
  Definition -> CompilerM Multicore ISPCState ()
ispcDecl
    [C.cedecl|extern "C" $tyqual:unmasked $tyqual:uniform struct memblock $tyqual:uniform
                        $id:shim($tyqual:uniform struct futhark_context* $tyqual:uniform ctx);|]
  -- Call it
  forall op s. BlockItem -> CompilerM op s ()
GC.item [C.citem|$tyqual:uniform struct memblock $id:name = $id:shim(ctx);|]
compileCode (MCCode
c1 :>>: MCCode
c2) = [MCCode] -> CompilerM Multicore ISPCState ()
go (forall op. Code op -> [Code op]
GC.linearCode (MCCode
c1 forall a. Code a -> Code a -> Code a
:>>: MCCode
c2))
  where
    go :: [MCCode] -> CompilerM Multicore ISPCState ()
go (DeclareScalar VName
name Volatility
_ PrimType
t : SetScalar VName
dest Exp
e : [MCCode]
code)
      | VName
name forall a. Eq a => a -> a -> Bool
== VName
dest = do
          let ct :: Type
ct = PrimType -> Type
GC.primTypeToCType PrimType
t
          Exp
e' <- Exp -> ISPCCompilerM Exp
compileExp Exp
e
          [TypeQual]
quals <- VName -> ISPCCompilerM [TypeQual]
getVariabilityQuals VName
name
          forall op s. BlockItem -> CompilerM op s ()
GC.item [C.citem|$tyquals:quals $ty:ct $id:name = $exp:e';|]
          [MCCode] -> CompilerM Multicore ISPCState ()
go [MCCode]
code
    go (MCCode
x : [MCCode]
xs) = MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [MCCode] -> CompilerM Multicore ISPCState ()
go [MCCode]
xs
    go [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
compileCode (Allocate VName
name (Count (TPrimExp Exp
e)) Space
space) = do
  Exp
size <- Exp -> ISPCCompilerM Exp
compileExp Exp
e
  Maybe VName
cached <- forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
name
  case Maybe VName
cached of
    Just VName
cur_size ->
      forall op s. Stm -> CompilerM op s ()
GC.stm
        [C.cstm|if ($exp:cur_size < $exp:size) {
                  err = lexical_realloc(ctx, &$exp:name, &$exp:cur_size, $exp:size);
                  if (err != FUTHARK_SUCCESS) {
                    $escstm:("unmasked { return err; }")
                  }
                }|]
    Maybe VName
_ ->
      forall a b.
(ToExp a, ToExp b) =>
a -> b -> Space -> Stm -> CompilerM Multicore ISPCState ()
allocMem VName
name Exp
size Space
space [C.cstm|$escstm:("unmasked { return 1; }")|]
compileCode (SetMem VName
dest VName
src Space
space) =
  forall a b.
(ToExp a, ToExp b) =>
a -> b -> Space -> CompilerM Multicore ISPCState ()
setMem VName
dest VName
src Space
space
compileCode (Write VName
dest (Count TExp Int64
idx) PrimType
elemtype Space
DefaultSpace Volatility
_ Exp
elemexp)
  | forall {v}. PrimExp v -> Bool
isConstExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
idx) = do
      Exp
dest' <- forall op s. VName -> CompilerM op s Exp
GC.rawMem VName
dest
      Exp
idxexp <- Exp -> ISPCCompilerM Exp
compileExp forall a b. (a -> b) -> a -> b
$ forall v. PrimExp v -> PrimExp v
constFoldPrimExp forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
idx
      Exp
deref <-
        Exp -> Exp -> Type -> Exp
GC.derefPointer Exp
dest' [C.cexp|($tyquals:([varying]) typename int64_t)$exp:idxexp|]
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> PrimType -> ISPCCompilerM Type
getMemType VName
dest PrimType
elemtype
      Exp
elemexp' <- PrimType -> Exp -> Exp
toStorage PrimType
elemtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ISPCCompilerM Exp
compileExp Exp
elemexp
      forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$exp:deref = $exp:elemexp';|]
  | Bool
otherwise = do
      Exp
dest' <- forall op s. VName -> CompilerM op s Exp
GC.rawMem VName
dest
      Exp
deref <-
        Exp -> Exp -> Type -> Exp
GC.derefPointer Exp
dest'
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ISPCCompilerM Exp
compileExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
idx)
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VName -> PrimType -> ISPCCompilerM Type
getMemType VName
dest PrimType
elemtype
      Exp
elemexp' <- PrimType -> Exp -> Exp
toStorage PrimType
elemtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ISPCCompilerM Exp
compileExp Exp
elemexp
      forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$exp:deref = $exp:elemexp';|]
  where
    isConstExp :: PrimExp v -> Bool
isConstExp = forall {v}. PrimExp v -> Bool
isSimple forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall v. PrimExp v -> PrimExp v
constFoldPrimExp
    isSimple :: PrimExp v -> Bool
isSimple (ValueExp PrimValue
_) = Bool
True
    isSimple PrimExp v
_ = Bool
False
compileCode (Read VName
x VName
src (Count TExp Int64
iexp) PrimType
restype Space
DefaultSpace Volatility
_) = do
  Exp
src' <- forall op s. VName -> CompilerM op s Exp
GC.rawMem VName
src
  Exp
e <-
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PrimType -> Exp -> Exp
fromStorage PrimType
restype) forall a b. (a -> b) -> a -> b
$
      Exp -> Exp -> Type -> Exp
GC.derefPointer Exp
src'
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> ISPCCompilerM Exp
compileExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
iexp)
        forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> VName -> PrimType -> ISPCCompilerM Type
getMemType VName
src PrimType
restype
  forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:x = $exp:e;|]
compileCode code :: MCCode
code@(Copy PrimType
pt VName
dest (Count TExp Int64
destoffset) Space
DefaultSpace VName
src (Count TExp Int64
srcoffset) Space
DefaultSpace (Count TExp Int64
size)) = do
  Bool
dm <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
dest
  Bool
sm <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
src
  if Bool
dm Bool -> Bool -> Bool
|| Bool
sm
    then
      forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$
        forall op s.
PrimType -> Exp -> Exp -> Exp -> Exp -> Exp -> CompilerM op s ()
copyMemoryAOS PrimType
pt
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall op s. VName -> CompilerM op s Exp
GC.rawMem VName
dest
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> ISPCCompilerM Exp
compileExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
destoffset)
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall op s. VName -> CompilerM op s Exp
GC.rawMem VName
src
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> ISPCCompilerM Exp
compileExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
srcoffset)
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Exp -> ISPCCompilerM Exp
compileExp (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
size)
    else forall op s. Code op -> CompilerM op s ()
GC.compileCode MCCode
code
compileCode (Free VName
name Space
space) = do
  Bool
cached <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
name
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
cached forall a b. (a -> b) -> a -> b
$ forall a. ToExp a => a -> Space -> CompilerM Multicore ISPCState ()
unRefMem VName
name Space
space
compileCode (For VName
i Exp
bound MCCode
body)
  -- The special-case here is to avoid certain pathological/contrived
  -- programs that construct statically known zero-element arrays.
  -- Due to the way we do constant-fold index functions, this produces
  -- code that looks like it has uniform/varying mismatches (i.e. race
  -- conditions) to ISPC, even though that code is never actually run.
  | forall {v}. PrimExp v -> Bool
isZero Exp
bound = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise = do
      let i' :: SrcLoc -> Id
i' = forall a. ToIdent a => a -> SrcLoc -> Id
C.toIdent VName
i
          t :: Type
t = PrimType -> Type
GC.primTypeToCType forall a b. (a -> b) -> a -> b
$ forall v. PrimExp v -> PrimType
primExpType Exp
bound
      Exp
bound' <- Exp -> ISPCCompilerM Exp
compileExp Exp
bound
      [BlockItem]
body' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
body
      [TypeQual]
quals <- VName -> ISPCCompilerM [TypeQual]
getVariabilityQuals VName
i
      forall op s. Stm -> CompilerM op s ()
GC.stm
        [C.cstm|for ($tyquals:quals $ty:t $id:i' = 0; $id:i' < $exp:bound'; $id:i'++) {
            $items:body'
          }|]
  where
    isZero :: PrimExp v -> Bool
isZero (ValueExp PrimValue
v) = PrimValue -> Bool
zeroIsh PrimValue
v
    isZero PrimExp v
_ = Bool
False
compileCode (While TExp Bool
cond MCCode
body) = do
  Exp
cond' <- Exp -> ISPCCompilerM Exp
compileExp forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Bool
cond
  [BlockItem]
body' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
body
  forall op s. Stm -> CompilerM op s ()
GC.stm
    [C.cstm|while ($exp:cond') {
            $items:body'
          }|]
compileCode (If TExp Bool
cond MCCode
tbranch MCCode
fbranch) = do
  Exp
cond' <- Exp -> ISPCCompilerM Exp
compileExp forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Bool
cond
  [BlockItem]
tbranch' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
tbranch
  [BlockItem]
fbranch' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
fbranch
  forall op s. Stm -> CompilerM op s ()
GC.stm forall a b. (a -> b) -> a -> b
$ case ([BlockItem]
tbranch', [BlockItem]
fbranch') of
    ([BlockItem]
_, []) ->
      [C.cstm|if ($exp:cond') { $items:tbranch' }|]
    ([], [BlockItem]
_) ->
      [C.cstm|if (!($exp:cond')) { $items:fbranch' }|]
    ([BlockItem], [BlockItem])
_ ->
      [C.cstm|if ($exp:cond') { $items:tbranch' } else { $items:fbranch' }|]
compileCode (Call [VName]
dests Name
fname [Arg]
args) = do
  ([VName]
dests', [[Stm]]
unpack_dest) <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM forall op s. VName -> CompilerM op s (VName, [Stm])
GC.compileDest [VName]
dests
  forall {a} {op} {s}.
ToIdent a =>
[a] -> Name -> [Exp] -> CompilerM op s ()
defCallIspc [VName]
dests' Name
fname forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall op s. Arg -> CompilerM op s Exp
GC.compileArg [Arg]
args
  forall op s. [Stm] -> CompilerM op s ()
GC.stms forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [[Stm]]
unpack_dest
  where
    defCallIspc :: [a] -> Name -> [Exp] -> CompilerM op s ()
defCallIspc [a]
dests' Name
fname' [Exp]
args' = do
      let out_args :: [Exp]
out_args = [[C.cexp|&$id:d|] | a
d <- [a]
dests']
          args'' :: [Exp]
args''
            | Name -> Bool
isBuiltInFunction Name
fname' = [Exp]
args'
            | Bool
otherwise = [C.cexp|ctx|] forall a. a -> [a] -> [a]
: [Exp]
out_args forall a. [a] -> [a] -> [a]
++ [Exp]
args'
      case [a]
dests' of
        [a
d]
          | Name -> Bool
isBuiltInFunction Name
fname' ->
              forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:d = $id:(funName fname')($args:args'');|]
        [a]
_ ->
          forall op s. BlockItem -> CompilerM op s ()
GC.item
            [C.citem|
            if ($id:(funName fname')($args:args'') != 0) {
              $escstm:("unmasked { return 1; }")
            }|]
compileCode (Assert Exp
e ErrorMsg Exp
msg (SrcLoc
loc, [SrcLoc]
locs)) = do
  Exp
e' <- Exp -> ISPCCompilerM Exp
compileExp Exp
e
  [BlockItem]
err <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ ErrorMsg Exp -> String -> CompilerM Multicore ISPCState ()
handleError ErrorMsg Exp
msg String
stacktrace
  forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|if (!$exp:e') { $items:err }|]
  where
    stacktrace :: String
stacktrace = Text -> String
T.unpack forall a b. (a -> b) -> a -> b
$ Int -> [Text] -> Text
prettyStacktrace Int
0 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a => a -> Text
locText forall a b. (a -> b) -> a -> b
$ SrcLoc
loc forall a. a -> [a] -> [a]
: [SrcLoc]
locs
compileCode MCCode
code =
  forall op s. Code op -> CompilerM op s ()
GC.compileCode MCCode
code

-- | Prepare a struct with memory allocted in the scope and populate
-- its fields with values
prepareMemStruct :: [(VName, VName)] -> [VName] -> ISPCCompilerM Name
prepareMemStruct :: [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState Name
prepareMemStruct [(VName, VName)]
lexmems [VName]
fatmems = do
  let lex_defs :: [FieldGroup]
lex_defs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {a}. (ToIdent a, ToIdent a) => (a, a) -> [FieldGroup]
lexMemDef [(VName, VName)]
lexmems
  let fat_defs :: [FieldGroup]
fat_defs = forall a b. (a -> b) -> [a] -> [b]
map forall {a}. ToIdent a => a -> FieldGroup
fatMemDef [VName]
fatmems
  Name
name <- DefSpecifier ISPCState
ispcDef String
"mem_struct" forall a b. (a -> b) -> a -> b
$ \Name
s -> do
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      [C.cedecl|struct $id:s {
        $sdecls:lex_defs
        $sdecls:fat_defs
      };|]
  let name' :: Name
name' = Name
name forall a. Semigroup a => a -> a -> a
<> Name
"_"
  forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform struct $id:name $id:name';|]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(VName
a, VName
b) -> [VName
a, VName
b]) [(VName, VName)]
lexmems) forall a b. (a -> b) -> a -> b
$ \VName
m ->
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:name'.$id:m = $id:m;|]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [VName]
fatmems forall a b. (a -> b) -> a -> b
$ \VName
m ->
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:name'.$id:m = &$id:m;|]
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
name
  where
    lexMemDef :: (a, a) -> [FieldGroup]
lexMemDef (a
name, a
size) =
      [ [C.csdecl|$tyqual:varying unsigned char * $tyqual:uniform $id:name;|],
        [C.csdecl|$tyqual:varying size_t $id:size;|]
      ]
    fatMemDef :: a -> FieldGroup
fatMemDef a
name =
      [C.csdecl|$tyqual:varying struct memblock * $tyqual:uniform $id:name;|]

-- | Get memory from the memory struct into local variables
compileGetMemStructVals :: Name -> [(VName, VName)] -> [VName] -> ISPCCompilerM ()
compileGetMemStructVals :: Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileGetMemStructVals Name
struct [(VName, VName)]
lexmems [VName]
fatmems = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [VName]
fatmems forall a b. (a -> b) -> a -> b
$ \VName
m ->
    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|struct memblock $id:m = *$id:struct->$id:m;|]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(VName, VName)]
lexmems forall a b. (a -> b) -> a -> b
$ \(VName
m, VName
s) -> do
    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:varying unsigned char * $tyqual:uniform $id:m = $id:struct->$id:m;|]
    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|size_t $id:s = $id:struct->$id:s;|]

-- | Write back potentially changed memory addresses and sizes to the memory struct
compileWritebackMemStructVals :: Name -> [(VName, VName)] -> [VName] -> ISPCCompilerM ()
compileWritebackMemStructVals :: Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileWritebackMemStructVals Name
struct [(VName, VName)]
lexmems [VName]
fatmems = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [VName]
fatmems forall a b. (a -> b) -> a -> b
$ \VName
m ->
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|*$id:struct->$id:m = $id:m;|]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(VName, VName)]
lexmems forall a b. (a -> b) -> a -> b
$ \(VName
m, VName
s) -> do
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:struct->$id:m = $id:m;|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:struct->$id:s = $id:s;|]

-- | Read back potentially changed memory addresses and sizes to the memory struct into local variables
compileReadbackMemStructVals :: Name -> [(VName, VName)] -> [VName] -> ISPCCompilerM ()
compileReadbackMemStructVals :: Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileReadbackMemStructVals Name
struct [(VName, VName)]
lexmems [VName]
fatmems = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [VName]
fatmems forall a b. (a -> b) -> a -> b
$ \VName
m ->
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:m = *$id:struct.$id:m;|]
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(VName, VName)]
lexmems forall a b. (a -> b) -> a -> b
$ \(VName
m, VName
s) -> do
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:m = $id:struct.$id:m;|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:s = $id:struct.$id:s;|]

compileGetStructVals ::
  Name ->
  [VName] ->
  [(C.Type, MC.ValueType)] ->
  ISPCCompilerM [C.BlockItem]
compileGetStructVals :: Name -> [VName] -> [(Type, ValueType)] -> ISPCCompilerM [BlockItem]
compileGetStructVals Name
struct [VName]
a [(Type, ValueType)]
b = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM VName -> (Type, ValueType) -> ISPCCompilerM [BlockItem]
field [VName]
a [(Type, ValueType)]
b
  where
    struct' :: Name
struct' = Name
struct forall a. Semigroup a => a -> a -> a
<> Name
"_"
    field :: VName -> (Type, ValueType) -> ISPCCompilerM [BlockItem]
field VName
name (Type
ty, MC.Prim PrimType
pt) = do
      let inner :: Exp
inner = [C.cexp|$id:struct'->$id:(MC.closureFreeStructField name)|]
      forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.citems|$tyqual:uniform $ty:ty $id:name = $exp:(fromStorage pt inner);|]
    field VName
name (Type
_, ValueType
_) = do
      Name
strlit <- String -> CompilerM Multicore ISPCState Name
makeStringLiteral forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyString VName
name
      forall (f :: * -> *) a. Applicative f => a -> f a
pure
        [C.citems|$tyqual:uniform struct memblock $id:name;
                     $id:name.desc = $id:strlit();
                     $id:name.mem = $id:struct'->$id:(MC.closureFreeStructField name);
                     $id:name.size = 0;
                     $id:name.references = NULL;|]

-- | Can the given code produce an error? If so, we can't use foreach
-- loops, since they don't allow for early-outs in error handling.
mayProduceError :: MCCode -> Bool
mayProduceError :: MCCode -> Bool
mayProduceError (MCCode
x :>>: MCCode
y) = MCCode -> Bool
mayProduceError MCCode
x Bool -> Bool -> Bool
|| MCCode -> Bool
mayProduceError MCCode
y
mayProduceError (If TExp Bool
_ MCCode
x MCCode
y) = MCCode -> Bool
mayProduceError MCCode
x Bool -> Bool -> Bool
|| MCCode -> Bool
mayProduceError MCCode
y
mayProduceError (For VName
_ Exp
_ MCCode
x) = MCCode -> Bool
mayProduceError MCCode
x
mayProduceError (While TExp Bool
_ MCCode
x) = MCCode -> Bool
mayProduceError MCCode
x
mayProduceError (Comment Text
_ MCCode
x) = MCCode -> Bool
mayProduceError MCCode
x
mayProduceError (Op (ForEachActive VName
_ MCCode
body)) = MCCode -> Bool
mayProduceError MCCode
body
mayProduceError (Op (ForEach VName
_ Exp
_ Exp
_ MCCode
body)) = MCCode -> Bool
mayProduceError MCCode
body
mayProduceError (Op SegOp {}) = Bool
True
mayProduceError Allocate {} = Bool
True
mayProduceError Assert {} = Bool
True
mayProduceError SetMem {} = Bool
True
mayProduceError Free {} = Bool
True
mayProduceError Call {} = Bool
True
mayProduceError MCCode
_ = Bool
False

-- Generate a segop function for top_level and potentially nested SegOp code
compileOp :: GC.OpCompiler Multicore ISPCState
compileOp :: OpCompiler Multicore ISPCState
compileOp (SegOp String
name [Param]
params ParallelTask
seq_task Maybe ParallelTask
par_task [Param]
retvals (SchedulerInfo Exp
e Scheduling
sched)) = do
  let (ParallelTask MCCode
seq_code) = ParallelTask
seq_task
  [(Type, ValueType)]
free_ctypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall op s. Param -> CompilerM op s (Type, ValueType)
MC.paramToCType [Param]
params
  [(Type, ValueType)]
retval_ctypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall op s. Param -> CompilerM op s (Type, ValueType)
MC.paramToCType [Param]
retvals
  let free_args :: [VName]
free_args = forall a b. (a -> b) -> [a] -> [b]
map Param -> VName
paramName [Param]
params
      retval_args :: [VName]
retval_args = forall a b. (a -> b) -> [a] -> [b]
map Param -> VName
paramName [Param]
retvals
      free :: [(VName, (Type, ValueType))]
free = forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
free_args [(Type, ValueType)]
free_ctypes
      retval :: [(VName, (Type, ValueType))]
retval = forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
retval_args [(Type, ValueType)]
retval_ctypes

  Exp
e' <- Exp -> ISPCCompilerM Exp
compileExp Exp
e

  let lexical :: Map VName Space
lexical = KernelHandling -> Function Multicore -> Map VName Space
lexicalMemoryUsageMC KernelHandling
OpaqueKernels forall a b. (a -> b) -> a -> b
$ forall a.
Maybe EntryPoint -> [Param] -> [Param] -> Code a -> FunctionT a
Function forall a. Maybe a
Nothing [] [Param]
params MCCode
seq_code

  Name
fstruct <-
    forall s.
DefSpecifier s
-> String
-> [VName]
-> [(Type, ValueType)]
-> [VName]
-> [(Type, ValueType)]
-> CompilerM Multicore s Name
MC.prepareTaskStruct DefSpecifier ISPCState
sharedDef String
"task" [VName]
free_args [(Type, ValueType)]
free_ctypes [VName]
retval_args [(Type, ValueType)]
retval_ctypes

  Name
fpar_task <- forall a s.
ToIdent a =>
Map VName Space
-> String
-> MCCode
-> a
-> [(VName, (Type, ValueType))]
-> [(VName, (Type, ValueType))]
-> CompilerM Multicore s Name
MC.generateParLoopFn Map VName Space
lexical (String
name forall a. [a] -> [a] -> [a]
++ String
"_task") MCCode
seq_code Name
fstruct [(VName, (Type, ValueType))]
free [(VName, (Type, ValueType))]
retval
  forall op s. Name -> CompilerM op s ()
MC.addTimingFields Name
fpar_task

  let ftask_name :: Name
ftask_name = Name
fstruct forall a. Semigroup a => a -> a -> a
<> Name
"_task"

  [BlockItem]
to_c <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ do
    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|struct scheduler_segop $id:ftask_name;|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.args = args;|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.top_level_fn = $id:fpar_task;|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.name = $string:(nameToString fpar_task);|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.iterations = iterations;|]
    -- Create the timing fields for the task
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.task_time = &ctx->program->$id:(MC.functionTiming fpar_task);|]
    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.task_iter = &ctx->program->$id:(MC.functionIterations fpar_task);|]

    case Scheduling
sched of
      Scheduling
Dynamic -> forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.sched = DYNAMIC;|]
      Scheduling
Static -> forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.sched = STATIC;|]

    -- Generate the nested segop function if available
    [(Name, Bool)]
fnpar_task <- case Maybe ParallelTask
par_task of
      Just (ParallelTask MCCode
nested_code) -> do
        let lexical_nested :: Map VName Space
lexical_nested = KernelHandling -> Function Multicore -> Map VName Space
lexicalMemoryUsageMC KernelHandling
OpaqueKernels forall a b. (a -> b) -> a -> b
$ forall a.
Maybe EntryPoint -> [Param] -> [Param] -> Code a -> FunctionT a
Function forall a. Maybe a
Nothing [] [Param]
params MCCode
nested_code
        Name
fnpar_task <- forall a s.
ToIdent a =>
Map VName Space
-> String
-> MCCode
-> a
-> [(VName, (Type, ValueType))]
-> [(VName, (Type, ValueType))]
-> CompilerM Multicore s Name
MC.generateParLoopFn Map VName Space
lexical_nested (String
name forall a. [a] -> [a] -> [a]
++ String
"_nested_task") MCCode
nested_code Name
fstruct [(VName, (Type, ValueType))]
free [(VName, (Type, ValueType))]
retval
        forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.nested_fn = $id:fnpar_task;|]
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Name
fnpar_task] [Bool
True]
      Maybe ParallelTask
Nothing -> do
        forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:ftask_name.nested_fn=NULL;|]
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Monoid a => a
mempty

    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|return scheduler_prepare_task(&ctx->scheduler, &$id:ftask_name);|]

    -- Add profile fields for -P option
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op s. BlockItem -> CompilerM op s ()
GC.profileReport forall a b. (a -> b) -> a -> b
$ [(Name, Bool)] -> [BlockItem]
MC.multiCoreReport forall a b. (a -> b) -> a -> b
$ (Name
fpar_task, Bool
True) forall a. a -> [a] -> [a]
: [(Name, Bool)]
fnpar_task

  Name
schedn <- forall s. DefSpecifier s
MC.multicoreDef String
"schedule_shim" forall a b. (a -> b) -> a -> b
$ \Name
s ->
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      [C.cedecl|int $id:s(struct futhark_context* ctx, void* args, typename int64_t iterations) {
        $items:to_c
    }|]

  Definition -> CompilerM Multicore ISPCState ()
ispcDecl
    [C.cedecl|extern "C" $tyqual:unmasked $tyqual:uniform int $id:schedn
                        (struct futhark_context $tyqual:uniform * $tyqual:uniform ctx,
                        struct $id:fstruct $tyqual:uniform * $tyqual:uniform args,
                        $tyqual:uniform int iterations);|]

  VName
aos_name <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName String
"aos"
  forall op s. [BlockItem] -> CompilerM op s ()
GC.items
    [C.citems|
    $escstm:("#if ISPC")
    $tyqual:uniform struct $id:fstruct $id:aos_name[programCount];
    $id:aos_name[programIndex] = $id:(fstruct <> "_");
    $escstm:("foreach_active (i)")
    {
      if (err == 0) {
        err = $id:schedn(ctx, &$id:aos_name[i], extract($exp:e', i));
      }
    }
    if (err != 0) {
      $escstm:("unmasked { return err; }")
    }
    $escstm:("#else")
    err = $id:schedn(ctx, &$id:(fstruct <> "_"), $exp:e');
    if (err != 0) {
      goto cleanup;
    }
    $escstm:("#endif")|]
compileOp (ISPCKernel MCCode
body [Param]
free) = do
  [(Type, ValueType)]
free_ctypes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall op s. Param -> CompilerM op s (Type, ValueType)
MC.paramToCType [Param]
free
  let free_args :: [VName]
free_args = forall a b. (a -> b) -> [a] -> [b]
map Param -> VName
paramName [Param]
free

  let lexical :: Map VName Space
lexical = KernelHandling -> Function Multicore -> Map VName Space
lexicalMemoryUsageMC KernelHandling
OpaqueKernels forall a b. (a -> b) -> a -> b
$ forall a.
Maybe EntryPoint -> [Param] -> [Param] -> Code a -> FunctionT a
Function forall a. Maybe a
Nothing [] [Param]
free MCCode
body
  -- Generate ISPC kernel
  Name
fstruct <- forall s.
DefSpecifier s
-> String
-> [VName]
-> [(Type, ValueType)]
-> [VName]
-> [(Type, ValueType)]
-> CompilerM Multicore s Name
MC.prepareTaskStruct DefSpecifier ISPCState
sharedDef String
"param_struct" [VName]
free_args [(Type, ValueType)]
free_ctypes [] []
  let fstruct' :: Name
fstruct' = Name
fstruct forall a. Semigroup a => a -> a -> a
<> Name
"_"

  Name
ispcShim <- DefSpecifier ISPCState
ispcDef String
"loop_ispc" forall a b. (a -> b) -> a -> b
$ \Name
s -> do
    [BlockItem]
mainBody <- forall op s a. CompilerM op s a -> CompilerM op s a
GC.inNewFunction forall a b. (a -> b) -> a -> b
$
      forall a. MCCode -> ISPCCompilerM a -> ISPCCompilerM a
analyzeVariability MCCode
body forall a b. (a -> b) -> a -> b
$
        forall op s a.
Map VName Space
-> ([BlockItem] -> [Stm] -> [(VName, VName)] -> CompilerM op s a)
-> CompilerM op s a
cachingMemory Map VName Space
lexical forall a b. (a -> b) -> a -> b
$ \[BlockItem]
decl_cached [Stm]
free_cached [(VName, VName)]
lexmems ->
          forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ do
            forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform struct futhark_context * $tyqual:uniform ctx = $id:fstruct'->ctx;|]
            forall op s. [BlockItem] -> CompilerM op s ()
GC.items forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> [VName] -> [(Type, ValueType)] -> ISPCCompilerM [BlockItem]
compileGetStructVals Name
fstruct [VName]
free_args [(Type, ValueType)]
free_ctypes
            [BlockItem]
body' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
body
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op s. BlockItem -> CompilerM op s ()
GC.item [BlockItem]
decl_cached
            forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op s. BlockItem -> CompilerM op s ()
GC.item forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall op s. CompilerM op s [BlockItem]
GC.declAllocatedMem

            -- Make inner kernel for error handling, if needed
            if MCCode -> Bool
mayProduceError MCCode
body
              then do
                [VName]
fatmems <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. CompilerState s -> [(VName, Space)]
GC.compDeclaredMem)
                Name
mstruct <- [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState Name
prepareMemStruct [(VName, VName)]
lexmems [VName]
fatmems
                let mstruct' :: Name
mstruct' = Name
mstruct forall a. Semigroup a => a -> a -> a
<> Name
"_"
                Name
innerShim <- DefSpecifier ISPCState
ispcDef String
"inner_ispc" forall a b. (a -> b) -> a -> b
$ \Name
t -> do
                  [BlockItem]
innerBody <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ do
                    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform struct futhark_context * $tyqual:uniform ctx = $id:fstruct'->ctx;|]
                    forall op s. [BlockItem] -> CompilerM op s ()
GC.items forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> [VName] -> [(Type, ValueType)] -> ISPCCompilerM [BlockItem]
compileGetStructVals Name
fstruct [VName]
free_args [(Type, ValueType)]
free_ctypes
                    Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileGetMemStructVals Name
mstruct' [(VName, VName)]
lexmems [VName]
fatmems
                    forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform int err = 0;|]
                    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op s. BlockItem -> CompilerM op s ()
GC.item [BlockItem]
body'
                    Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileWritebackMemStructVals Name
mstruct' [(VName, VName)]
lexmems [VName]
fatmems
                    forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|return err;|]
                  forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    [C.cedecl|
                static $tyqual:unmasked inline $tyqual:uniform int $id:t(
                  $tyqual:uniform typename int64_t start,
                  $tyqual:uniform typename int64_t end,
                  struct $id:fstruct $tyqual:uniform * $tyqual:uniform $id:fstruct',
                  struct $id:mstruct $tyqual:uniform * $tyqual:uniform $id:mstruct') {
                  $items:innerBody
                }|]
                -- Call the kernel and read back potentially changed memory
                forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform int err = $id:innerShim(start, end, $id:fstruct', &$id:mstruct');|]
                Name
-> [(VName, VName)] -> [VName] -> CompilerM Multicore ISPCState ()
compileReadbackMemStructVals Name
mstruct' [(VName, VName)]
lexmems [VName]
fatmems
              else do
                forall op s. InitGroup -> CompilerM op s ()
GC.decl [C.cdecl|$tyqual:uniform int err = 0;|]
                forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall op s. BlockItem -> CompilerM op s ()
GC.item [BlockItem]
body'

            [BlockItem]
free_mem <- ISPCCompilerM [BlockItem]
freeAllocatedMem
            forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|cleanup: {$stms:free_cached $items:free_mem}|]
            forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|return err;|]
    forall op s. Definition -> CompilerM op s ()
GC.earlyDecl
      [C.cedecl|int $id:s(typename int64_t start,
                                  typename int64_t end,
                                  struct $id:fstruct * $id:fstruct');|]
    forall (f :: * -> *) a. Applicative f => a -> f a
pure
      [C.cedecl|
        $tyqual:export $tyqual:uniform int $id:s($tyqual:uniform typename int64_t start,
                                                 $tyqual:uniform typename int64_t end,
                                                 struct $id:fstruct $tyqual:uniform * $tyqual:uniform $id:fstruct' ) {
          $items:mainBody
        }|]

  -- Generate C code to call into ISPC kernel
  forall op s. [BlockItem] -> CompilerM op s ()
GC.items
    [C.citems|
    err = $id:ispcShim(start, end, & $id:fstruct');
    if (err != 0) {
      goto cleanup;
    }|]
compileOp (ForEach VName
i Exp
from Exp
bound MCCode
body) = do
  Exp
from' <- Exp -> ISPCCompilerM Exp
compileExp Exp
from
  Exp
bound' <- Exp -> ISPCCompilerM Exp
compileExp Exp
bound
  [BlockItem]
body' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
body
  if MCCode -> Bool
mayProduceError MCCode
body
    then
      forall op s. [Stm] -> CompilerM op s ()
GC.stms
        [C.cstms|
      for ($tyqual:uniform typename int64_t i = 0; i < (($exp:bound' - $exp:from') / programCount); i++) {
        typename int64_t $id:i = $exp:from' + programIndex + i * programCount;
        $items:body'
      }
      if (programIndex < (($exp:bound' - $exp:from') % programCount)) {
        typename int64_t $id:i = $exp:from' + programIndex + ((($exp:bound' - $exp:from') / programCount) * programCount);
        $items:body'
      }|]
    else
      forall op s. [Stm] -> CompilerM op s ()
GC.stms
        [C.cstms|
      $escstm:(T.unpack ("foreach (" <> prettyText i <> " = " <> expText from' <> " ... " <> expText bound' <> ")")) {
        $items:body'
      }|]
compileOp (ForEachActive VName
name MCCode
body) = do
  [BlockItem]
body' <- forall op s. CompilerM op s () -> CompilerM op s [BlockItem]
GC.collect forall a b. (a -> b) -> a -> b
$ MCCode -> CompilerM Multicore ISPCState ()
compileCode MCCode
body
  forall op s. [Stm] -> CompilerM op s ()
GC.stms
    [C.cstms|
    for ($tyqual:uniform unsigned int $id:name = 0; $id:name < programCount; $id:name++) {
      if (programIndex == $id:name) {
        $items:body'
      }
    }|]
compileOp (ExtractLane VName
dest (ValueExp PrimValue
v) Exp
_) =
  -- extract() on constants is not allowed (type is uniform, not
  -- varying), so just turn them into an assignment.
  forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:dest = $exp:v;|]
compileOp (ExtractLane VName
dest Exp
tar Exp
lane) = do
  Exp
tar' <- Exp -> ISPCCompilerM Exp
compileExp Exp
tar
  Exp
lane' <- Exp -> ISPCCompilerM Exp
compileExp Exp
lane
  forall op s. Stm -> CompilerM op s ()
GC.stm [C.cstm|$id:dest = extract($exp:tar', $exp:lane');|]
compileOp (Atomic AtomicOp
aop) =
  forall op s.
AtomicOp
-> (Type -> VName -> CompilerM op s Type) -> CompilerM op s ()
MC.atomicOps AtomicOp
aop forall a b. (a -> b) -> a -> b
$ \Type
ty VName
arr -> do
    Bool
cached <- forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a op s. ToExp a => a -> CompilerM op s (Maybe VName)
GC.cacheMem VName
arr
    if Bool
cached
      then forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cty|$tyqual:varying $ty:ty* $tyqual:uniform|]
      else forall (f :: * -> *) a. Applicative f => a -> f a
pure [C.cty|$ty:ty*|]
compileOp Multicore
op = forall s. OpCompiler Multicore s
MC.compileOp Multicore
op

-- | Like @GenericC.cachingMemory@, but adapted for ISPC codegen.
cachingMemory ::
  M.Map VName Space ->
  ([C.BlockItem] -> [C.Stm] -> [(VName, VName)] -> GC.CompilerM op s a) ->
  GC.CompilerM op s a
cachingMemory :: forall op s a.
Map VName Space
-> ([BlockItem] -> [Stm] -> [(VName, VName)] -> CompilerM op s a)
-> CompilerM op s a
cachingMemory Map VName Space
lexical [BlockItem] -> [Stm] -> [(VName, VName)] -> CompilerM op s a
f = do
  let cached :: [VName]
cached = forall k a. Map k a -> [k]
M.keys forall a b. (a -> b) -> a -> b
$ forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (forall a. Eq a => a -> a -> Bool
== Space
DefaultSpace) Map VName Space
lexical

  [(VName, VName)]
cached' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VName]
cached forall a b. (a -> b) -> a -> b
$ \VName
mem -> do
    VName
size <- forall (m :: * -> *). MonadFreshNames m => String -> m VName
newVName forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyString VName
mem forall a. Semigroup a => a -> a -> a
<> String
"_cached_size"
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (VName
mem, VName
size)

  let lexMem :: CompilerEnv op s -> CompilerEnv op s
lexMem CompilerEnv op s
env =
        CompilerEnv op s
env
          { envCachedMem :: Map Exp VName
GC.envCachedMem =
              forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a. ToExp a => a -> SrcLoc -> Exp
`C.toExp` forall a. IsLocation a => a
noLoc)) [(VName, VName)]
cached')
                forall a. Semigroup a => a -> a -> a
<> forall op s. CompilerEnv op s -> Map Exp VName
GC.envCachedMem CompilerEnv op s
env
          }

      declCached :: (a, a) -> [BlockItem]
declCached (a
mem, a
size) =
        [ [C.citem|size_t $id:size = 0;|],
          [C.citem|$tyqual:varying unsigned char * $tyqual:uniform $id:mem = NULL;|]
        ]

      freeCached :: (a, b) -> Stm
freeCached (a
mem, b
_) =
        [C.cstm|free($id:mem);|]

  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local forall {op} {s}. CompilerEnv op s -> CompilerEnv op s
lexMem forall a b. (a -> b) -> a -> b
$ [BlockItem] -> [Stm] -> [(VName, VName)] -> CompilerM op s a
f (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {a}. (ToIdent a, ToIdent a) => (a, a) -> [BlockItem]
declCached [(VName, VName)]
cached') (forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b}. ToIdent a => (a, b) -> Stm
freeCached [(VName, VName)]
cached') [(VName, VName)]
cached'

-- Variability analysis
type Dependencies = M.Map VName Names

data Variability = Uniform | Varying
  deriving (Variability -> Variability -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Variability -> Variability -> Bool
$c/= :: Variability -> Variability -> Bool
== :: Variability -> Variability -> Bool
$c== :: Variability -> Variability -> Bool
Eq, Eq Variability
Variability -> Variability -> Bool
Variability -> Variability -> Ordering
Variability -> Variability -> Variability
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Variability -> Variability -> Variability
$cmin :: Variability -> Variability -> Variability
max :: Variability -> Variability -> Variability
$cmax :: Variability -> Variability -> Variability
>= :: Variability -> Variability -> Bool
$c>= :: Variability -> Variability -> Bool
> :: Variability -> Variability -> Bool
$c> :: Variability -> Variability -> Bool
<= :: Variability -> Variability -> Bool
$c<= :: Variability -> Variability -> Bool
< :: Variability -> Variability -> Bool
$c< :: Variability -> Variability -> Bool
compare :: Variability -> Variability -> Ordering
$ccompare :: Variability -> Variability -> Ordering
Ord, Int -> Variability -> ShowS
[Variability] -> ShowS
Variability -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Variability] -> ShowS
$cshowList :: [Variability] -> ShowS
show :: Variability -> String
$cshow :: Variability -> String
showsPrec :: Int -> Variability -> ShowS
$cshowsPrec :: Int -> Variability -> ShowS
Show)

newtype VariabilityM a
  = VariabilityM (ReaderT Names (State Dependencies) a)
  deriving
    ( forall a b. a -> VariabilityM b -> VariabilityM a
forall a b. (a -> b) -> VariabilityM a -> VariabilityM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> VariabilityM b -> VariabilityM a
$c<$ :: forall a b. a -> VariabilityM b -> VariabilityM a
fmap :: forall a b. (a -> b) -> VariabilityM a -> VariabilityM b
$cfmap :: forall a b. (a -> b) -> VariabilityM a -> VariabilityM b
Functor,
      Functor VariabilityM
forall a. a -> VariabilityM a
forall a b. VariabilityM a -> VariabilityM b -> VariabilityM a
forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
forall a b.
VariabilityM (a -> b) -> VariabilityM a -> VariabilityM b
forall a b c.
(a -> b -> c) -> VariabilityM a -> VariabilityM b -> VariabilityM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM a
$c<* :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM a
*> :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
$c*> :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
liftA2 :: forall a b c.
(a -> b -> c) -> VariabilityM a -> VariabilityM b -> VariabilityM c
$cliftA2 :: forall a b c.
(a -> b -> c) -> VariabilityM a -> VariabilityM b -> VariabilityM c
<*> :: forall a b.
VariabilityM (a -> b) -> VariabilityM a -> VariabilityM b
$c<*> :: forall a b.
VariabilityM (a -> b) -> VariabilityM a -> VariabilityM b
pure :: forall a. a -> VariabilityM a
$cpure :: forall a. a -> VariabilityM a
Applicative,
      Applicative VariabilityM
forall a. a -> VariabilityM a
forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
forall a b.
VariabilityM a -> (a -> VariabilityM b) -> VariabilityM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> VariabilityM a
$creturn :: forall a. a -> VariabilityM a
>> :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
$c>> :: forall a b. VariabilityM a -> VariabilityM b -> VariabilityM b
>>= :: forall a b.
VariabilityM a -> (a -> VariabilityM b) -> VariabilityM b
$c>>= :: forall a b.
VariabilityM a -> (a -> VariabilityM b) -> VariabilityM b
Monad,
      MonadState Dependencies,
      MonadReader Names
    )

execVariabilityM :: VariabilityM a -> Dependencies
execVariabilityM :: forall a. VariabilityM a -> Dependencies
execVariabilityM (VariabilityM ReaderT Names (State Dependencies) a
m) =
  forall s a. State s a -> s -> s
execState (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Names (State Dependencies) a
m forall a. Monoid a => a
mempty) forall a. Monoid a => a
mempty

-- | Extend the set of dependencies with a new one
addDeps :: VName -> Names -> VariabilityM ()
addDeps :: VName -> Names -> VariabilityM ()
addDeps VName
v Names
ns = do
  Dependencies
deps <- forall s (m :: * -> *). MonadState s m => m s
get
  Names
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup VName
v Dependencies
deps of
    Maybe Names
Nothing -> forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Names
ns forall a. Semigroup a => a -> a -> a
<> Names
env) Dependencies
deps
    Just Names
ns' -> forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert VName
v (Names
ns forall a. Semigroup a => a -> a -> a
<> Names
ns') Dependencies
deps

-- | Find all the dependencies in a body of code
findDeps :: MCCode -> VariabilityM ()
findDeps :: MCCode -> VariabilityM ()
findDeps (MCCode
x :>>: MCCode
y) = do
  MCCode -> VariabilityM ()
findDeps MCCode
x
  MCCode -> VariabilityM ()
findDeps MCCode
y
findDeps (If TExp Bool
cond MCCode
x MCCode
y) =
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn TExp Bool
cond) forall a b. (a -> b) -> a -> b
$ do
    MCCode -> VariabilityM ()
findDeps MCCode
x
    MCCode -> VariabilityM ()
findDeps MCCode
y
findDeps (For VName
idx Exp
bound MCCode
x) = do
  VName -> Names -> VariabilityM ()
addDeps VName
idx Names
free
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a. Semigroup a => a -> a -> a
<> Names
free) forall a b. (a -> b) -> a -> b
$ MCCode -> VariabilityM ()
findDeps MCCode
x
  where
    free :: Names
free = forall a. FreeIn a => a -> Names
freeIn Exp
bound
findDeps (While TExp Bool
cond MCCode
x) = do
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn TExp Bool
cond) forall a b. (a -> b) -> a -> b
$ MCCode -> VariabilityM ()
findDeps MCCode
x
findDeps (Comment Text
_ MCCode
x) =
  MCCode -> VariabilityM ()
findDeps MCCode
x
findDeps (Op (SegOp String
_ [Param]
free ParallelTask
_ Maybe ParallelTask
_ [Param]
retvals SchedulerInfo
_)) =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
    ( \Param
x ->
        VName -> Names -> VariabilityM ()
addDeps (Param -> VName
paramName Param
x) forall a b. (a -> b) -> a -> b
$
          [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$
            forall a b. (a -> b) -> [a] -> [b]
map Param -> VName
paramName [Param]
free
    )
    [Param]
retvals
findDeps (Op (ForEach VName
_ Exp
_ Exp
_ MCCode
body)) =
  MCCode -> VariabilityM ()
findDeps MCCode
body
findDeps (Op (ForEachActive VName
_ MCCode
body)) =
  MCCode -> VariabilityM ()
findDeps MCCode
body
findDeps (SetScalar VName
name Exp
e) =
  VName -> Names -> VariabilityM ()
addDeps VName
name forall a b. (a -> b) -> a -> b
$ forall a. FreeIn a => a -> Names
freeIn Exp
e
findDeps (Call [VName]
tars Name
_ [Arg]
args) =
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\VName
x -> VName -> Names -> VariabilityM ()
addDeps VName
x forall a b. (a -> b) -> a -> b
$ forall a. FreeIn a => a -> Names
freeIn [Arg]
args) [VName]
tars
findDeps (Read VName
x VName
arr (Count TExp Int64
iexp) PrimType
_ Space
DefaultSpace Volatility
_) = do
  VName -> Names -> VariabilityM ()
addDeps VName
x forall a b. (a -> b) -> a -> b
$ forall a. FreeIn a => a -> Names
freeIn (forall {k} (t :: k) v. TPrimExp t v -> PrimExp v
untyped TExp Int64
iexp)
  VName -> Names -> VariabilityM ()
addDeps VName
x forall a b. (a -> b) -> a -> b
$ VName -> Names
oneName VName
arr
findDeps (Op (GetLoopBounds VName
x VName
y)) = do
  VName -> Names -> VariabilityM ()
addDeps VName
x forall a. Monoid a => a
mempty
  VName -> Names -> VariabilityM ()
addDeps VName
y forall a. Monoid a => a
mempty
findDeps (Op (ExtractLane VName
x Exp
_ Exp
_)) = do
  VName -> Names -> VariabilityM ()
addDeps VName
x forall a. Monoid a => a
mempty
findDeps (Op (Atomic (AtomicCmpXchg PrimType
_ VName
old VName
arr Count Elements (TExp Int32)
ind VName
res Exp
val))) = do
  VName -> Names -> VariabilityM ()
addDeps VName
res forall a b. (a -> b) -> a -> b
$ forall a. FreeIn a => a -> Names
freeIn VName
arr forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn Count Elements (TExp Int32)
ind forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn Exp
val
  VName -> Names -> VariabilityM ()
addDeps VName
old forall a b. (a -> b) -> a -> b
$ forall a. FreeIn a => a -> Names
freeIn VName
arr forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn Count Elements (TExp Int32)
ind forall a. Semigroup a => a -> a -> a
<> forall a. FreeIn a => a -> Names
freeIn Exp
val
findDeps MCCode
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Take a list of dependencies and iterate them to a fixed point.
depsFixedPoint :: Dependencies -> Dependencies
depsFixedPoint :: Dependencies -> Dependencies
depsFixedPoint Dependencies
deps =
  if Dependencies
deps forall a. Eq a => a -> a -> Bool
== Dependencies
deps'
    then Dependencies
deps
    else Dependencies -> Dependencies
depsFixedPoint Dependencies
deps'
  where
    grow :: Names -> Names
grow Names
names =
      Names
names forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\VName
n -> forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault forall a. Monoid a => a
mempty VName
n Dependencies
deps) (Names -> IntMap VName
namesIntMap Names
names)
    deps' :: Dependencies
deps' = forall a b k. (a -> b) -> Map k a -> Map k b
M.map Names -> Names
grow Dependencies
deps

-- | Find roots of variance. These are memory blocks declared in
-- the current scope as well as loop indices of foreach loops.
findVarying :: MCCode -> [VName]
findVarying :: MCCode -> [VName]
findVarying (MCCode
x :>>: MCCode
y) = MCCode -> [VName]
findVarying MCCode
x forall a. [a] -> [a] -> [a]
++ MCCode -> [VName]
findVarying MCCode
y
findVarying (If TExp Bool
_ MCCode
x MCCode
y) = MCCode -> [VName]
findVarying MCCode
x forall a. [a] -> [a] -> [a]
++ MCCode -> [VName]
findVarying MCCode
y
findVarying (For VName
_ Exp
_ MCCode
x) = MCCode -> [VName]
findVarying MCCode
x
findVarying (While TExp Bool
_ MCCode
x) = MCCode -> [VName]
findVarying MCCode
x
findVarying (Comment Text
_ MCCode
x) = MCCode -> [VName]
findVarying MCCode
x
findVarying (Op (ForEachActive VName
_ MCCode
body)) = MCCode -> [VName]
findVarying MCCode
body
findVarying (Op (ForEach VName
idx Exp
_ Exp
_ MCCode
body)) = VName
idx forall a. a -> [a] -> [a]
: MCCode -> [VName]
findVarying MCCode
body
findVarying (DeclareMem VName
mem Space
_) = [VName
mem]
findVarying MCCode
_ = []

-- | Analyze variability in a body of code and run an action with
-- info about that variability in the compiler state.
analyzeVariability :: MCCode -> ISPCCompilerM a -> ISPCCompilerM a
analyzeVariability :: forall a. MCCode -> ISPCCompilerM a -> ISPCCompilerM a
analyzeVariability MCCode
code ISPCCompilerM a
m = do
  let roots :: [VName]
roots = MCCode -> [VName]
findVarying MCCode
code
  let deps :: Dependencies
deps = Dependencies -> Dependencies
depsFixedPoint forall a b. (a -> b) -> a -> b
$ forall a. VariabilityM a -> Dependencies
execVariabilityM forall a b. (a -> b) -> a -> b
$ MCCode -> VariabilityM ()
findDeps MCCode
code
  let safelist :: Dependencies
safelist = forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (\Names
b -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (VName -> Names -> Bool
`notNameIn` Names
b) [VName]
roots) Dependencies
deps
  let safe :: Names
safe = [VName] -> Names
namesFromList forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [k]
M.keys Dependencies
safelist
  ISPCState
pre_state <- forall op s. CompilerM op s s
GC.getUserState
  forall s op. (s -> s) -> CompilerM op s ()
GC.modifyUserState (\ISPCState
s -> ISPCState
s {sUniform :: Names
sUniform = Names
safe})
  a
a <- ISPCCompilerM a
m
  forall s op. (s -> s) -> CompilerM op s ()
GC.modifyUserState (\ISPCState
s -> ISPCState
s {sUniform :: Names
sUniform = ISPCState -> Names
sUniform ISPCState
pre_state})
  forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

-- | Get the variability of a variable
getVariability :: VName -> ISPCCompilerM Variability
getVariability :: VName -> ISPCCompilerM Variability
getVariability VName
name = do
  Names
uniforms <- ISPCState -> Names
sUniform forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall op s. CompilerM op s s
GC.getUserState
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
    if VName
name VName -> Names -> Bool
`nameIn` Names
uniforms
      then Variability
Uniform
      else Variability
Varying

-- | Get the variability qualifiers of a variable
getVariabilityQuals :: VName -> ISPCCompilerM [C.TypeQual]
getVariabilityQuals :: VName -> ISPCCompilerM [TypeQual]
getVariabilityQuals VName
name = Variability -> [TypeQual]
variQuals forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VName -> ISPCCompilerM Variability
getVariability VName
name
  where
    variQuals :: Variability -> [TypeQual]
variQuals Variability
Uniform = [C.ctyquals|$tyqual:uniform|]
    variQuals Variability
Varying = []