Add support for FloatArray

granule-compiler.cabal

@@ -29,7 +29,10 @@ library
       Language.Granule.Codegen.Compile
       Language.Granule.Codegen.MarkGlobals
   other-modules:
-      Language.Granule.Codegen.Builtins
+      Language.Granule.Codegen.Builtins.Builtins
+      Language.Granule.Codegen.Builtins.Extras
+      Language.Granule.Codegen.Builtins.FloatArray
+      Language.Granule.Codegen.Builtins.Shared
       Language.Granule.Codegen.Emit.EmitableDef
       Language.Granule.Codegen.Emit.EmitBuiltins
       Language.Granule.Codegen.Emit.EmitterState
@@ -44,6 +47,7 @@ library
       Language.Granule.Codegen.Emit.Names
       Language.Granule.Codegen.Emit.Primitives
       Language.Granule.Codegen.Emit.Types
+      Language.Granule.Codegen.RewriteAST
       Paths_granule_compiler
   hs-source-dirs:
       src

src/Language/Granule/Codegen/Builtins/Builtins.hs

@@ -0,0 +1,24 @@
+module Language.Granule.Codegen.Builtins.Builtins where
+
+import Language.Granule.Codegen.Builtins.Extras
+import Language.Granule.Codegen.Builtins.FloatArray
+import Language.Granule.Codegen.Builtins.Shared
+import Language.Granule.Syntax.Identifiers (Id, mkId)
+
+builtins :: [Builtin]
+builtins =
+  [ charToIntDef,
+    divDef,
+    newFloatArrayIDef,
+    readFloatArrayIDef,
+    writeFloatArrayIDef,
+    lengthFloatArrayIDef,
+    newFloatArrayDef,
+    readFloatArrayDef,
+    writeFloatArrayDef,
+    lengthFloatArrayDef,
+    deleteFloatArrayDef
+  ]
+
+builtinIds :: [Id]
+builtinIds = map (mkId . builtinId) builtins

src/Language/Granule/Codegen/Builtins/Extras.hs

@@ -0,0 +1,27 @@
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+module Language.Granule.Codegen.Builtins.Extras where
+
+import LLVM.AST.Type as IR
+import LLVM.IRBuilder.Instruction
+import Language.Granule.Codegen.Builtins.Shared
+import Language.Granule.Syntax.Identifiers
+import Language.Granule.Syntax.Type as Gr
+
+-- charToInt :: Char -> Int
+charToIntDef :: Builtin
+charToIntDef =
+    Builtin "charToInt" args ret impl
+    where
+        args = [TyCon (Id "Char" "Char")]
+        ret = TyCon (Id "Int" "Int")
+        impl [x] = zext x i32
+
+-- div :: Int -> Int -> Int
+divDef :: Builtin
+divDef =
+    Builtin "div" args ret impl
+    where
+        args = [TyCon (Id "Int" "Int"), TyCon (Id "Int" "Int")]
+        ret = TyCon (Id "Int" "Int")
+        impl [x, y] = sdiv x y

src/Language/Granule/Codegen/Builtins/FloatArray.hs

@@ -0,0 +1,133 @@
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+module Language.Granule.Codegen.Builtins.FloatArray where
+
+import qualified LLVM.AST.Constant as C
+import LLVM.AST.IntegerPredicate
+import LLVM.AST.Operand (Operand (ConstantOperand))
+import LLVM.AST.Type as IR
+import LLVM.IRBuilder (emitBlockStart)
+import LLVM.IRBuilder.Constant as C
+import LLVM.IRBuilder.Instruction
+import LLVM.IRBuilder.Module (MonadModuleBuilder)
+import LLVM.IRBuilder.Monad (MonadIRBuilder, freshName)
+import Language.Granule.Codegen.Builtins.Shared
+import Language.Granule.Codegen.Emit.Primitives (trap)
+import Prelude hiding (or)
+
+-- Mutable FloatArray builtins
+newFloatArrayDef, readFloatArrayDef, writeFloatArrayDef, lengthFloatArrayDef, deleteFloatArrayDef :: Builtin
+newFloatArrayDef =
+  Builtin "newFloatArray" [tyInt] tyFloatArray impl
+  where
+    impl [len] = newFloatArray len
+readFloatArrayDef =
+  Builtin "readFloatArray" [tyFloatArray, tyInt] (tyPair (tyFloat, tyFloatArray)) impl
+  where
+    impl [arrPtr, idx] = withBoundsCheck arrPtr idx $ readFloatArray arrPtr idx
+writeFloatArrayDef =
+  Builtin "writeFloatArray" [tyFloatArray, tyInt, tyFloat] tyFloatArray impl
+  where
+    impl [arrPtr, idx, val] = withBoundsCheck arrPtr idx $ do
+      dataPtr <- readStruct arrPtr 1
+      writeData dataPtr idx val
+      return arrPtr
+lengthFloatArrayDef =
+  Builtin "lengthFloatArray" [tyFloatArray] (tyPair (tyInt, tyFloatArray)) impl
+  where
+    impl [arrPtr] = lengthFloatArray arrPtr
+deleteFloatArrayDef =
+  Builtin "deleteFloatArray" [tyFloatArray] tyUnit impl
+  where
+    impl [arrPtr] = do
+      dataPtr <- readStruct arrPtr 1
+      _ <- free dataPtr
+      _ <- free arrPtr
+      -- return unit (need to check)
+      return $ ConstantOperand (C.Struct Nothing False [])
+
+-- Immutable FloatArray builtins
+newFloatArrayIDef, readFloatArrayIDef, writeFloatArrayIDef, lengthFloatArrayIDef :: Builtin
+newFloatArrayIDef =
+  Builtin "newFloatArrayI" [tyInt] tyFloatArray impl
+  where
+    impl [len] = newFloatArray len
+readFloatArrayIDef =
+  Builtin "readFloatArrayI" [tyFloatArray, tyInt] (tyPair (tyFloat, tyFloatArray)) impl
+  where
+    impl [arrPtr, idx] = withBoundsCheck arrPtr idx $ readFloatArray arrPtr idx
+writeFloatArrayIDef =
+  Builtin "writeFloatArrayI" [tyFloatArray, tyInt, tyFloat] tyFloatArray impl
+  where
+    impl [arrPtr, idx, val] = withBoundsCheck arrPtr idx $ do
+      len <- readStruct arrPtr 0
+      dataPtr <- readStruct arrPtr 1
+
+      -- len * double precision
+      size <- mul len (int32 8)
+      -- malloc wants i64
+      size' <- sext size i64
+      newDataPtr <- allocate size' IR.double
+
+      -- copy existing data to new array
+      _ <- copy newDataPtr dataPtr size
+
+      -- write value at index
+      writeData newDataPtr idx val
+
+      -- return a new array struct
+      makeArrayStruct IR.double len newDataPtr
+lengthFloatArrayIDef =
+  Builtin "lengthFloatArrayI" [tyFloatArray] (tyPair (tyInt, tyFloatArray)) impl
+  where
+    impl [arrPtr] = lengthFloatArray arrPtr
+
+-- arrayStruct specialisation
+floatArrayStruct :: IR.Type
+floatArrayStruct = arrayStruct IR.double
+
+-- creates a new float array of length
+newFloatArray :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> m Operand
+newFloatArray len = do
+  -- len * double precision
+  size <- mul len (int32 8)
+  -- malloc wants i64
+  size' <- sext size i64
+  dataPtr <- allocate size' IR.double
+  makeArrayStruct IR.double len dataPtr
+
+-- read the value at index of float array
+readFloatArray :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Operand -> m Operand
+readFloatArray arrPtr idx = do
+  dataPtr <- readStruct arrPtr 1
+  value <- readData dataPtr idx
+  makePair (IR.double, value) (ptr floatArrayStruct, arrPtr)
+
+-- read the length of float array
+lengthFloatArray :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> m Operand
+lengthFloatArray arrPtr = do
+  len <- readStruct arrPtr 0
+  makePair (i32, len) (ptr floatArrayStruct, arrPtr)
+
+withBoundsCheck ::
+  (MonadIRBuilder m, MonadModuleBuilder m) =>
+  Operand ->
+  Operand ->
+  m Operand ->
+  m Operand
+withBoundsCheck arrPtr idx continuation = do
+  len <- readStruct arrPtr 0
+  ltZero <- icmp SLT idx (int32 0)
+  gteLen <- icmp SGE idx len
+  outOfBounds <- or ltZero gteLen
+
+  abort <- freshName "out_of_bounds"
+  continue <- freshName "in_bounds"
+
+  condBr outOfBounds abort continue
+
+  emitBlockStart abort
+  trap
+
+  emitBlockStart continue
+  continuation

src/Language/Granule/Codegen/Builtins/Shared.hs

@@ -0,0 +1,106 @@
+{-# LANGUAGE RankNTypes #-}
+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
+
+module Language.Granule.Codegen.Builtins.Shared where
+
+import LLVM.AST
+import LLVM.AST.Type as IR
+import LLVM.IRBuilder.Constant (bit, int32)
+import LLVM.IRBuilder.Instruction (bitcast, call, gep, load, store, insertValue)
+import LLVM.IRBuilder.Module
+import LLVM.IRBuilder.Monad
+import Language.Granule.Codegen.Emit.LLVMHelpers (sizeOf)
+import Language.Granule.Codegen.Emit.Primitives as P
+import Language.Granule.Syntax.Identifiers
+import Language.Granule.Syntax.Type as Gr
+import qualified LLVM.AST.Constant as C
+
+data Builtin = Builtin {
+    builtinId :: String,
+    builtinArgTys :: [Gr.Type],
+    builtinRetTy :: Gr.Type,
+    builtinImpl :: forall m. (MonadModuleBuilder m, MonadIRBuilder m) => [Operand] -> m Operand}
+
+-- LLVM helpers
+
+allocate :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> IR.Type -> m Operand
+allocate len ty = do
+  pointer <- call (ConstantOperand P.malloc) [(len, [])]
+  bitcast pointer (ptr ty)
+
+allocateStruct :: (MonadIRBuilder m, MonadModuleBuilder m) => IR.Type -> m Operand
+allocateStruct ty = allocate (ConstantOperand $ sizeOf ty) ty
+
+copy :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Operand -> Operand -> m Operand
+copy dst src len = do
+  dst' <- bitcast dst (ptr i8)
+  src' <- bitcast src (ptr i8)
+  call (ConstantOperand P.memcpy) [(dst', []), (src', []), (len, []), (bit 0, [])]
+
+free :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> m Operand
+free memPtr = do
+  memPtr' <- bitcast memPtr (ptr i8)
+  call (ConstantOperand P.free) [(memPtr', [])]
+
+makePair :: (MonadIRBuilder m, MonadModuleBuilder m) => (IR.Type, Operand) -> (IR.Type, Operand) -> m Operand
+makePair (leftTy, leftVal) (rightTy, rightVal) = do
+  let pairTy = StructureType False [leftTy, rightTy]
+  let pair = ConstantOperand $ C.Undef pairTy
+  pair' <- insertValue pair leftVal [0]
+  insertValue pair' rightVal [1]
+
+writeStruct :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Int -> Operand -> m ()
+writeStruct struct index value = do
+  field <- gep struct [int32 0, int32 $ fromIntegral index]
+  store field 0 value
+
+readStruct :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Int -> m Operand
+readStruct struct index = do
+  field <- gep struct [int32 0, int32 $ fromIntegral index]
+  load field 0
+
+-- Arrays
+
+arrayStruct :: IR.Type -> IR.Type
+arrayStruct ty = StructureType False [i32, ptr ty]
+
+-- creates a struct for len and array data
+makeArrayStruct :: (MonadIRBuilder m, MonadModuleBuilder m) => IR.Type -> Operand -> Operand -> m Operand
+makeArrayStruct ty len dataPtr = do
+  arrPtr <- allocateStruct (arrayStruct ty)
+  writeStruct arrPtr 0 len
+  writeStruct arrPtr 1 dataPtr
+  return arrPtr
+
+writeData :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Operand -> Operand -> m ()
+writeData dataPtr index value = do
+  valuePtr <- gep dataPtr [index]
+  store valuePtr 0 value
+
+readData :: (MonadIRBuilder m, MonadModuleBuilder m) => Operand -> Operand -> m Operand
+readData dataPtr index = do
+  valuePtr <- gep dataPtr [index]
+  load valuePtr 0
+
+-- Granule types
+
+mkFunType :: [Gr.Type] -> Gr.Type -> Gr.Type
+mkFunType args ret = foldr (FunTy Nothing Nothing) ret args
+
+tyInt :: Gr.Type
+tyInt = TyCon (Id "Int" "Int")
+
+tyFloat :: Gr.Type
+tyFloat = TyCon (Id "Float" "Float")
+
+tyChar :: Gr.Type
+tyChar = TyCon (Id "Char" "Char")
+
+tyUnit :: Gr.Type
+tyUnit = TyCon (Id "()" "()")
+
+tyPair :: (Gr.Type, Gr.Type) -> Gr.Type
+tyPair (l, r) = TyApp (TyApp (TyCon (Id "," ",")) l) r
+
+tyFloatArray :: Gr.Type
+tyFloatArray = TyApp (TyCon (Id "FloatArray" "FloatArray")) (TyVar (Id "id" "id"))