read file, liquid haskell'd

liquid haskelld.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# language OverloadedStrings, BangPatterns #-}
import Data.Word
import Foreign.Ptr
import Foreign.C.Types
import Foreign.Marshal.Alloc
import System.Posix.IO.ByteString
import System.Posix.Types

main :: IO ()
main = do
  fd@(Fd fd') <- openFd "/home/chris/Work/chrisdone/lh/.stack-work/stack.sqlite3" ReadOnly defaultFileFlags
  let bufsize :: CSize
      bufsize = (128*1024)
  buffer <- mallocBytes' bufsize
  let loop :: Int -> IO ()
      loop 0 = pure ()
      loop (!i) = do
        count <- c_safe_read fd' buffer bufsize
        if count == 0 || count == (-1)
           then pure ()
           else do
             loop (i-1)
  loop 10000
  free buffer
  closeFd fd

{-@ measure size :: Ptr Word8 -> CSize @-}

{-@
  assume mallocBytes' ::
    {i : CSize | i > 0} -> IO ({p : Ptr Word8 | size p == i })
  @-}
mallocBytes' :: CSize -> IO (Ptr Word8)
mallocBytes' = mallocBytes . fromIntegral

{-@
  assume c_safe_read ::
     CInt ->
     { p : Ptr Word8 | true } ->
     { s : CSize | s > 0 && s <= size p } ->
     IO { c : CSize | c >= -1 && c <= s }
  @-}
foreign import ccall safe "read"
   c_safe_read :: CInt -> Ptr Word8 -> CSize -> IO CSize

{-

[1 of 2] Compiling Main             ( /home/chris/Work/chrisdone/lh/src/Main.hs, interpreted ) [Source file changed]

**** LIQUID: SAFE (169 constraints checked) ************************************
Ok, one module loaded.
(0.00 secs, 0 bytes)
[1 of 2] Compiling Main             ( src/Main.hs, src/Main.o ) [Source file changed]

**** LIQUID: SAFE (169 constraints checked) ************************************
[2 of 2] Linking main [Objects changed]
          40,816 bytes allocated in the heap
           3,144 bytes copied during GC
          35,984 bytes maximum residency (1 sample(s))
          21,360 bytes maximum slop
               6 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0         0 colls,     0 par    0.000s   0.000s     0.0000s    0.0000s
  Gen  1         1 colls,     0 par    0.000s   0.000s     0.0001s    0.0001s

  INIT    time    0.000s  (  0.000s elapsed)
  MUT     time    0.000s  (  0.001s elapsed)
  GC      time    0.000s  (  0.000s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time    0.001s  (  0.001s elapsed)

  %GC     time       0.0%  (0.0% elapsed)

  Alloc rate    97,958,556 bytes per MUT second

  Productivity  56.3% of total user, 61.3% of total elapsed
  
  -}