content: ---
  layout: post
  title: "Pointers Gone Wild"
  date: 2014-05-28
  comments: true
  external-url:
  author: Eric Seidel
  published: true
  categories: benchmarks, text
  demo: TextInternal.hs
  ---
  
  A large part of the allure of Haskell is its elegant, high-level ADTs
  that ensure[^compilercorrectness] that programs won't be plagued by problems
  like the infamous [SSL heartbleed bug](http://en.wikipedia.org/wiki/Heartbleed).
  
  [^compilercorrectness]: Assuming the absence of errors in the compiler and run-time...
  
  However, another part of Haskell's charm is that when you really really 
  need to, you can drop down to low-level pointer twiddling to squeeze the 
  most performance out of your machine. But of course, that opens the door 
  to the #heartbleeds.
  
  Can we have have our cake and eat it too? 
  
  Can we twiddle pointers and still get the nice safety assurances of high-level types?
  
  <!-- more -->
  
  To understand the potential for potential bleeding,
  let's study the popular `text` library for efficient 
  text processing. The library provides the high-level 
  API Haskellers have come to expect while using stream 
  fusion and byte arrays under the hood to guarantee 
  high performance.
  
  Suppose we wanted to get the *i*th `Char` of a `Text`,
  \begin{code} we could write a function[^bad]
  charAt (Text a o l) i = word2char $ unsafeIndex a (o+i)
    where 
      word2char         = chr . fromIntegral
  \end{code}
  which extracts the underlying array `a`, indexes into it starting
  at the offset `o` and casts the `Word16` to a `Char`, using 
  functions exported by `text`.
  
  [^bad]: This function is bad for numerous reasons, least of which is that `Data.Text.index` is already provided, but stay with us...
  
  \begin{code}Let's try this out in GHCi.
  ghci> let t = pack ['d','o','g']
  ghci> charAt t 0
  'd'
  ghci> charAt t 2
  'g'
  \end{code}
  
  \begin{code}Looks good so far, what happens if we keep going?
  ghci> charAt t 3
  '\NUL'
  ghci> charAt t 100
  '\8745'
  \end{code}
  
  Oh dear, not only did we not get any sort of exception from Haskell, 
  we weren't even stopped by the OS with a segfault. This is quite 
  dangerous since we have no idea what sort of data we just read! 
  To be fair to the library's authors, we did use a function that 
  was clearly branded `unsafe`, but these functions, while not 
  intended for *clients*, pervade the implementation of the *library*.
  
  Wouldn't it be nice to have these last two calls *rejected at compile time*?
  
  In this post we'll see exactly how prevent invalid memory accesses 
  like this with LiquidHaskell.
  
  
  <div class="hidden">
  
  \begin{code}
  {-# LANGUAGE BangPatterns, MagicHash, Rank2Types,
      RecordWildCards, UnboxedTuples, ExistentialQuantification #-}
  {-@ LIQUID "--no-termination" @-}
  module TextInternal (test, goodMain, badMain, charAt, charAt') where
  
  import qualified Control.Exception as Ex
  import Control.Applicative     ((<$>))
  import Control.Monad           (when)
  import Control.Monad.ST.Unsafe (unsafeIOToST)
  import Data.Bits (shiftR, xor, (.&.))
  import Data.Char
  import Foreign.C.Types (CSize)
  import GHC.Base (Int(..), ByteArray#, MutableByteArray#, newByteArray#,
                   writeWord16Array#, indexWord16Array#, unsafeCoerce#, ord,
                   iShiftL#)
  import GHC.ST (ST(..), runST)
  import GHC.Word (Word16(..))
  
  import qualified Data.Text.Lazy.IO as TIO
  import qualified Data.Text as T
  import qualified Data.Text.Internal as T
  
  import Language.Haskell.Liquid.Prelude
  
  {-@ aLen :: a:Array -> {v:Nat | v = (aLen a)}  @-}
  
  {-@ maLen :: a:MArray s -> {v:Nat | v = (maLen a)}  @-}
  
  new          :: forall s. Int -> ST s (MArray s)
  unsafeWrite  :: MArray s -> Int -> Word16 -> ST s ()
  unsafeFreeze :: MArray s -> ST s Array
  unsafeIndex  :: Array -> Int -> Word16
  copyM        :: MArray s               -- ^ Destination
               -> Int                    -- ^ Destination offset
               -> MArray s               -- ^ Source
               -> Int                    -- ^ Source offset
               -> Int                    -- ^ Count
               -> ST s ()
  
  {-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-}
  memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO ()
  memcpyM = undefined
  
  --------------------------------------------------------------------------------
  --- Helper Code
  --------------------------------------------------------------------------------
  {-@ shiftL :: i:Nat -> n:Nat -> {v:Nat | ((n = 1) => (v = (i * 2)))} @-}
  shiftL :: Int -> Int -> Int
  shiftL = undefined -- (I# x#) (I# i#) = I# (x# `iShiftL#` i#)
  
  pack :: String -> Text
  pack = undefined -- not "actually" using
  
  assert b a = Ex.assert b a
  
  
  data Text = Text Array Int Int
  
  {-@ tLength :: t:Text -> {v:_ | v = (tLen t)} @-}
  tLength (Text _ _ n)  =  n
  \end{code}
  
  </div>
  
  The `Text` Lifecycle
  --------------------
  `text` splits the reading and writing array operations between two
  types of arrays, immutable `Array`s and mutable `MArray`s. This leads to
  the following general lifecycle:
  
  ![The lifecycle of a `Text`](/images/text-lifecycle.png)
  
  The main four array operations we care about are:
  
  1. **creating** an `MArray`,
  2. **writing** into an `MArray`,
  3. **freezing** an `MArray` into an `Array`, and
  4. **reading** from an `Array`.
  
  Creating an `MArray`
  --------------------
  
  The (mutable) `MArray` is a thin wrapper around GHC's primitive
  `MutableByteArray#`, additionally carrying the number of `Word16`s it
  can store.
  
  \begin{code}
  data MArray s = MArray { maBA  :: MutableByteArray# s
                         , maLen :: !Int
                         }
  \end{code}
  
  It doesn't make any sense to have a negative length, so we *refine*
  the data definition to require that `maLen` be non-negative. 
  
  \begin{code}
  {-@ data MArray s = MArray { maBA  :: MutableByteArray# s
                             , maLen :: Nat
                             }
    @-}
  \end{code}
  
  
  \begin{code} As an added bonus, the above specification generates **field-accessor measures** that we will use inside the refined types:
  {-@ measure maLen :: MArray s -> Int
      maLen (MArray a l) = l
    @-}
  \end{code}
  
  We can use these accessor measures to define `MArray`s of size `N`:
  
  \begin{code}
  {-@ type MArrayN a N = {v:MArray a | (maLen v) = N} @-}
  \end{code}
  
  and we can use the above alias, to write a type that tracks the size
  of an `MArray` at the point where it is created:
  
  \begin{code}
  {-@ new :: forall s. n:Nat -> ST s (MArrayN s n) @-}
  new n
    | n < 0 || n .&. highBit /= 0 = error "size overflow"
    | otherwise = ST $ \s1# ->
         case newByteArray# len# s1# of
           (# s2#, marr# #) -> (# s2#, MArray marr# n #)
    where !(I# len#) = bytesInArray n
          highBit    = maxBound `xor` (maxBound `shiftR` 1)
          bytesInArray n = n `shiftL` 1
  \end{code}
  
  `new n` is an `ST` action that produces an `MArray s` with `n` slots each 
  of which is 2 bytes (as internally `text` manipulates `Word16`s).
  
  The verification process here is quite simple; LH recognizes that 
  the `n` used to construct the returned array (`MArray marr# n`) 
  the same `n` passed to `new`. 
  
  Writing into an `MArray`
  ------------------------
  
  Once we have *created* an `MArray`, we'll want to write our data into it. 
  
  A `Nat` is a valid index into an `MArray` if it is *strictly less than* 
  the size of the array.
  
  \begin{code}
  {-@ type MAValidI MA = {v:Nat | v < (maLen MA)} @-}
  \end{code}
  
  We use this valid index alias to refine the type of `unsafeWrite`
  
  \begin{code}
  {-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-}
  unsafeWrite MArray{..} i@(I# i#) (W16# e#)
    | i < 0 || i >= maLen = assert False $ error "out of bounds"
    | otherwise = ST $ \s1# ->
        case writeWord16Array# maBA i# e# s1# of
          s2# -> (# s2#, () #)
  \end{code}
  
  Note that, when compiled with appropriate options, the implementation of
  `text` checks the bounds at run-time. However, LiquidHaskell can statically
  prove that the error branch is unreachable, i.e. the `assert` **cannot fail**
  (as long as the inputs adhere to the given specification) by giving `assert`
  the type:
  
  \begin{code}
  {-@ assert assert :: {v:Bool | (Prop v)} -> a -> a @-}
  \end{code}
  
  Bulk Writing into an `MArray`
  -----------------------------
  
  So now we can write individual `Word16`s into an array, but maybe we
  have a whole bunch of text we want to dump into the array. Remember,
  `text` is supposed to be fast! C has `memcpy` for cases like this but 
  it's notoriously unsafe; with the right type however, we can regain safety. 
  `text` provides a wrapper around `memcpy` to copy `n` elements from 
  one `MArray` to another.
  
  `copyM` requires two `MArray`s and valid offsets into each -- note
  that a valid offset is **not** necessarily a valid *index*, it may
  be one element out-of-bounds
  
  \begin{code}
  {-@ type MAValidO MA = {v:Nat | v <= (maLen MA)} @-}
  \end{code}
  
  -- and a `count` of elements to copy.
  The `count` must represent a valid region in each `MArray`, in
  other words `offset + count <= length` must hold for each array.
  
  \begin{code}
  {-@ copyM :: dest:MArray s
            -> didx:MAValidO dest
            -> src:MArray s
            -> sidx:MAValidO src
            -> {v:Nat | (((didx + v) <= (maLen dest))
                      && ((sidx + v) <= (maLen src)))}
            -> ST s ()
    @-}
  copyM dest didx src sidx count
      | count <= 0 = return ()
      | otherwise =
      assert (sidx + count <= maLen src) .
      assert (didx + count <= maLen dest) .
      unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                             (maBA src) (fromIntegral sidx)
                             (fromIntegral count)
  \end{code}
  
  Again, the two `assert`s in the function were in the original code as 
  (optionally compiled out) run-time checks of the precondition, but with 
  LiquidHaskell we can actually *prove* that the `assert`s **always succeed**.
  
  Freezing an `MArray` into an `Array`
  ------------------------------------
  
  Before we can package up our `MArray` into a `Text`, we need to
  *freeze* it, preventing any further mutation. The key property 
  here is of course that the frozen `Array` should have the same 
  length as the `MArray`.
  
  Just as `MArray` wraps a mutable array, `Array` wraps an *immutable*
  `ByteArray#` and carries its length in `Word16`s.
  
  \begin{code}
  data Array = Array { aBA  :: ByteArray#
                     , aLen :: !Int
                     }
  \end{code}
  
  As before, we get free accessor measures `aBA` and `aLen` just by
  refining the data definition
  
  \begin{code}
  {-@ data Array = Array { aBA  :: ByteArray#
                         , aLen :: Nat
                         }
    @-}
  \end{code}
  
  so we can refer to the components of an `Array` in our refinements.
  Using these measures, we can define
  
  \begin{code}
  {-@ type ArrayN N = {v:Array | (aLen v) = N} @-}
  {-@ unsafeFreeze :: ma:MArray s -> ST s (ArrayN (maLen ma)) @-}
  unsafeFreeze MArray{..} = ST $ \s# ->
                            (# s#, Array (unsafeCoerce# maBA) maLen #)
  \end{code}
  
  Again, LiquidHaskell is happy to prove our specification as we simply
  copy the length parameter `maLen` over into the `Array`.
  
  Reading from an `Array`
  ------------------------
  Finally, we will eventually want to read a value out of the
  `Array`. As with `unsafeWrite` we require a valid index into the
  `Array`, which we denote using the `AValidI` alias.
  
  \begin{code}
  {-@ type AValidI A = {v:Nat | v < (aLen A)} @-}
  {-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-}
  unsafeIndex Array{..} i@(I# i#)
    | i < 0 || i >= aLen = assert False $ error "out of bounds"
    | otherwise = case indexWord16Array# aBA i# of
                    r# -> (W16# r#)
  \end{code}
  
  As before, LiquidHaskell can easily prove that the error branch
  is unreachable, i.e. is *never* executed at run-time.
  
  Wrapping it all up
  ------------------
  
  Now we can finally define the core datatype of the `text` package!
  A `Text` value consists of three fields:
  
  A. an `Array`,
  
  B. an `Int` offset into the *middle* of the array, and
  
  C. an `Int` length denoting the number of valid indices *after* the offset.
  
  We can specify the invariants for fields (b) and (c) with the refined type:
  
  \begin{code}
  {-@ data Text
        = Text { tArr :: Array
               , tOff :: {v:Nat | v      <= (aLen tArr)}
               , tLen :: {v:Nat | v+tOff <= (aLen tArr)}
               }
    @-}
  \end{code}
  
  These invariants ensure that any *index* we pick between `tOff` and
  `tOff + tLen` will be a valid index into `tArr`. 
  
  As shown above with `new`, `unsafeWrite`, and `unsafeFreeze`, we can type the
  top-level function that creates a `Text` from a `[Char]` as:
  
  \begin{code}
  {-@ pack :: s:String -> {v:Text | (tLen v) = (len s)} @-}
  \end{code}
  
  Preventing Bleeds
  -----------------
  
  Now, let us close the circle and return to potentially *bleeding* function:
  
  \begin{code}
  charAt' (Text a o l) i = word2char $ unsafeIndex a (o+i)
    where 
      word2char          = chr . fromIntegral
  \end{code}
  
  Aha! LiquidHaskell flags the call to `unsafeIndex` because of course, `i` may fall
  outside the bounds of the given array `a`! We can remedy that by specifying
  a bound for the index:
  
  \begin{code}
  {-@ charAt :: t:Text -> {v:Nat | v < (tLen t)} -> Char @-}
  charAt (Text a o l) i = word2char $ unsafeIndex a (o+i)
    where 
      word2char         = chr . fromIntegral
  \end{code}
  
  That is, we can access the `i`th `Char` as long as `i` is a `Nat` less
  than the the size of the text, namely `tLen t`. Now LiquidHaskell is convinced
  that the call to `unsafeIndex` is safe, but of course, we have passed
  the burden of proof onto users of `charAt`.
  
  Now, if we try calling `charAt` as we did at the beginning
  
  \begin{code}
  test = [good,bad]
    where
      dog  = ['d','o','g']
      good = charAt (pack dog) 2
      bad  = charAt (pack dog) 3
  \end{code}
  
  we see that LiquidHaskell verifies the `good` call, but flags `bad` as
  **unsafe**.
  
  Enforcing Sanitization
  ----------------------
  
  EDIT: As several folks have pointed out, the #heartbleed error was
  due to inputs not being properly sanitized. The above approach 
  **ensures, at compile time**, that proper sanitization has been 
  performed. 
  
  To see this in action, lets write a little function that just shows the 
  character at a given position:
  
  \begin{code}
  {-@ showCharAt :: t:_ -> {v:Nat | v < (tLen t)} -> _ @-}
  showCharAt t i = putStrLn $ show $ charAt t i
  \end{code}
  
  Now, the following function, that correctly sanitizes is **accepted**
  
  \begin{code}
  goodMain :: IO ()
  goodMain 
    = do txt <- pack <$> getLine
         i   <- readLn
         if 0 <= i && i < tLength txt 
           then showCharAt txt i 
           else putStrLn "Bad Input!"
  \end{code}
  
  but this function, which has insufficient sanitization, is **rejected**
  
  \begin{code}
  badMain :: IO ()
  badMain 
    = do txt <- pack <$> getLine 
         i   <- readLn
         if 0 <= i 
           then showCharAt txt i 
           else putStrLn "Bad Input!"
  \end{code}
  
  Thus, we can use LiquidHaskell to block, at compile time, any serious bleeding
  from pointers gone wild.
  