content: ---
  layout: post
  title: "Text Bug"
  date: 2014-03-01
  comments: true
  external-url:
  author: Eric Seidel
  published: false
  categories: benchmarks, text
  demo: TextBug.hs
  ---
  
  For our last post on `text`, we return to the topic of building a new `Text`
  value, i.e. proving the safety of write operations.
  
  <!-- more -->
  
  <div class="hidden">
  
  \begin{code}
  {-# LANGUAGE BangPatterns, CPP, MagicHash, Rank2Types,
      RecordWildCards, UnboxedTuples, ExistentialQuantification #-}
  {-@ LIQUID "--no-termination" @-}
  module TextBug where
  
  import Control.Monad.ST.Unsafe (unsafeIOToST)
  import Foreign.C.Types (CSize)
  import GHC.Base hiding (unsafeChr)
  import GHC.ST
  import GHC.Word (Word16(..))
  import Data.Bits hiding (shiftL)
  import Data.Word
  
  import Language.Haskell.Liquid.Prelude
  
  --------------------------------------------------------------------------------
  --- From TextInternal
  --------------------------------------------------------------------------------
  
  {-@ 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#)
  
  {-@ measure isUnknown :: Size -> Prop
      isUnknown (Exact n) = false
      isUnknown (Max   n) = false
      isUnknown (Unknown) = true
    @-}
  {-@ measure getSize :: Size -> Int
      getSize (Exact n) = n
      getSize (Max   n) = n
    @-}
  
  {-@ invariant {v:Size | (getSize v) >= 0} @-}
  
  data Size = Exact {-# UNPACK #-} !Int -- ^ Exact size.
            | Max   {-# UNPACK #-} !Int -- ^ Upper bound on size.
            | Unknown                   -- ^ Unknown size.
              deriving (Eq, Show)
  
  {-@ upperBound :: k:Nat -> s:Size -> {v:Nat | v = ((isUnknown s) ? k : (getSize s))} @-}
  upperBound :: Int -> Size -> Int
  upperBound _ (Exact n) = n
  upperBound _ (Max   n) = n
  upperBound k _         = k
  
  data Step s a = Done
                | Skip !s
                | Yield !a !s
  
  data Stream a =
      forall s. Stream
      (s -> Step s a)             -- stepper function
      !s                          -- current state
      !Size                       -- size hint
  
  {-@ data Array = Array { aBA  :: ByteArray#
                         , aLen :: Nat 
                         } 
    @-}
  
  data Array = Array {
      aBA  :: ByteArray#
    , aLen :: !Int
    }
  
  {-@ measure alen     :: Array -> Int
      alen (Array a n) = n
    @-}
  
  {-@ aLen :: a:Array -> {v:Nat | v = (alen a)}  @-}
  
  {-@ type ArrayN  N   = {v:Array | (alen v) = N} @-}
  
  {-@ type AValidI A   = {v:Nat | v     <  (alen A)} @-}
  {-@ type AValidO A   = {v:Nat | v     <= (alen A)} @-}
  {-@ type AValidL O A = {v:Nat | (v+O) <= (alen A)} @-}
  
  {-@ data MArray s = MArray { maBA  :: MutableByteArray# s
                             , maLen :: Nat } @-}
  
  data MArray s = MArray {
      maBA  :: MutableByteArray# s
    , maLen :: !Int
    }
  
  {-@ measure malen :: MArray s -> Int
      malen (MArray a n) = n
    @-}
  
  {-@ maLen :: a:MArray s -> {v:Nat | v = (malen a)}  @-}
  
  {-@ type MArrayN s N = {v:MArray s | (malen v) = N} @-}
  
  {-@ type MAValidI MA = {v:Nat | v <  (malen MA)} @-}
  {-@ type MAValidO MA = {v:Nat | v <= (malen MA)} @-}
  
  {-@ new :: forall s. n:Nat -> ST s (MArrayN s n) @-}
  new          :: forall s. Int -> ST s (MArray s)
  new n
    | n < 0 || n .&. highBit /= 0 = error $ "Data.Text.Array.new: 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
  
  {-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-}
  unsafeWrite  :: MArray s -> Int -> Word16 -> ST s ()
  unsafeWrite MArray{..} i@(I# i#) (W16# e#)
    | i < 0 || i >= maLen = liquidError "out of bounds"
    | otherwise = ST $ \s1# ->
        case writeWord16Array# maBA i# e# s1# of
          s2# -> (# s2#, () #)
  
  {-@ 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        :: MArray s               -- ^ Destination
               -> Int                    -- ^ Destination offset
               -> MArray s               -- ^ Source
               -> Int                    -- ^ Source offset
               -> Int                    -- ^ Count
               -> ST s ()
  copyM dest didx src sidx count
      | count <= 0 = return ()
      | otherwise =
      liquidAssert (sidx + count <= maLen src) .
      liquidAssert (didx + count <= maLen dest) .
      unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                             (maBA src) (fromIntegral sidx)
                             (fromIntegral count)
  
  {-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-}
  memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO ()
  memcpyM = undefined
  
  {-@ unsafeFreeze :: ma:MArray s -> ST s (ArrayN (malen ma)) @-}
  unsafeFreeze :: MArray s -> ST s Array
  unsafeFreeze MArray{..} = ST $ \s# ->
                            (# s#, Array (unsafeCoerce# maBA) maLen #)
  
  {-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-}
  unsafeIndex  :: Array -> Int -> Word16
  unsafeIndex Array{..} i@(I# i#)
    | i < 0 || i >= aLen = liquidError "out of bounds"
    | otherwise = case indexWord16Array# aBA i# of
                    r# -> (W16# r#)
  
  data Text = Text Array Int Int
  {-@ data Text [tlen] = Text (tarr :: Array)
                              (toff :: TValidO tarr)
                              (tlen :: TValidL toff tarr)
    @-}
  
  {-@ type TValidI T   = {v:Nat | v     <  (tlen T)} @-}
  {-@ type TValidO A   = {v:Nat | v     <= (alen A)} @-}
  {-@ type TValidL O A = {v:Nat | (v+O) <= (alen A)} @-}
  
  
  --------------------------------------------------------------------------------
  --- From TextRead
  --------------------------------------------------------------------------------
  
  {-@ measure numchars :: Array -> Int -> Int -> Int @-}
  {-@ measure tlength :: Text -> Int @-}
  {-@ invariant {v:Text | (tlength v) = (numchars (tarr v) (toff v) (tlen v))} @-}
  
  --------------------------------------------------------------------------------
  --- From TextWrite
  --------------------------------------------------------------------------------
  
  {-@ qualif Ord(v:int, i:int, x:Char)
          : ((((ord x) <  65536) => (v = i))
          && (((ord x) >= 65536) => (v = (i + 1))))
    @-}
  
  {-@ predicate Room C MA I = (((One C) => (RoomN 1 MA I))
                            && ((Two C) => (RoomN 2 MA I)))
    @-}
  {-@ predicate RoomN N MA I = (I+N <= (malen MA)) @-}
  
  {-@ measure ord :: Char -> Int @-}
  {-@ ord :: c:Char -> {v:Int | v = (ord c)} @-}
  {-@ predicate One C = ((ord C) <  65536) @-}
  {-@ predicate Two C = ((ord C) >= 65536) @-}
  
  {-@ writeChar :: ma:MArray s -> i:Nat -> {v:Char | (Room v ma i)}
                -> ST s {v:Nat | (RoomN v ma i)}
    @-}
  writeChar :: MArray s -> Int -> Char -> ST s Int
  writeChar marr i c
      | n < 0x10000 = do
          unsafeWrite marr i (fromIntegral n)
          return 1
      | otherwise = do
          unsafeWrite marr i lo
          unsafeWrite marr (i+1) hi
          return 2
      where n = ord c
            m = n - 0x10000
            lo = fromIntegral $ (m `shiftR` 10) + 0xD800
            hi = fromIntegral $ (m .&. 0x3FF) + 0xDC00
  
  --------------------------------------------------------------------------------
  --- Helpers
  --------------------------------------------------------------------------------
  
  {-@ qualif MALenLE(v:int, a:MArray s): v <= (malen a) @-}
  {-@ qualif ALenLE(v:int, a:Array): v <= (alen a) @-}
  
  \end{code}
  
  </div>
  
  Let's take a look at `mapAccumL`, which combines a map and a fold
  over a `Stream` and bundles the result of the map into a new `Text`.
  Again, we'll want to focus our attention on the `Yield` case of the
  inner loop.
  
  \begin{code}
  mapAccumL f z0 (Stream next0 s0 len) =
    (nz, Text na 0 nl)
   where
    mlen = upperBound 4 len
    (na,(nz,nl)) = runST $ do
         (marr,x) <- (new mlen >>= \arr ->
                      outer arr mlen z0 s0 0)
         arr      <- unsafeFreeze marr
         return (arr,x)
    outer arr top = loop
     where
      loop !z !s !i =
        case next0 s of
          Done          -> return (arr, (z,i))
          Skip s'       -> loop z s' i
          Yield x s'
            | j >= top  -> do
              let top' = (top + 1) `shiftL` 1
              arr' <- new top'
              copyM arr' 0 arr 0 top
              outer arr' top' z s i
            | otherwise -> do
              let (z',c) = f z x
              d <- writeChar arr i c
              loop z' s' (i+d)
            where j | ord x < 0x10000 = i
                    | otherwise       = i + 1
  \end{code}
  
  If you recall `unstream` from last time, you'll notice that this loop body
  looks almost identical to the one found in `unstream`, but LiquidHaskell has
  flagged the `writeChar` call as unsafe! What's going on here?
  
  Let's take a look at `j`, recalling that it carried a crucial part of the safety
  \begin{code} proof last time, and see what LiquidHaskell was able to infer.
  {v:Int | ((ord x >= 65536) => (v == i+1))
        && ((ord x <  65536) => (v == i))}
  \end{code}
  
  Well that's not very useful at all! LiquidHaskell can prove that it's safe to
  write `x` but here we are trying to write `c` into the array. This is actually
  a *good* thing though, because `c` is the result of calling an arbitrary
  function `f` on `x`! We haven't constrained `f` in any way, so it could easily
  return a character above `U+10000` given any input.
  
  So `mapAccumL` is actually *unsafe*, and our first wild bug caught by
  LiquidHaskell! The fix is luckily easy, we simply have to lift the
  `let (z',c) = f z x` binder into the `where` clause, and change `j` to
  depend on `ord c` instead.
  
  \begin{code}
  mapAccumL' f z0 (Stream next0 s0 len) =
    (nz, Text na 0 nl)
   where
    mlen = upperBound 4 len
    (na,(nz,nl)) = runST $ do
         (marr,x) <- (new mlen >>= \arr ->
                      outer arr mlen z0 s0 0)
         arr      <- unsafeFreeze marr
         return (arr,x)
    outer arr top = loop
     where
      loop !z !s !i =
        case next0 s of
          Done          -> return (arr, (z,i))
          Skip s'       -> loop z s' i
          Yield x s'
            | j >= top  -> do
              let top' = (top + 1) `shiftL` 1
              arr' <- new top'
              copyM arr' 0 arr 0 top
              outer arr' top' z s i
            | otherwise -> do
              d <- writeChar arr i c
              loop z' s' (i+d)
            where (z',c) = f z x
                  j | ord c < 0x10000 = i
                    | otherwise       = i + 1
  \end{code}
  
  LiquidHaskell happily accepts our revised `mapAccumL`, as did the `text`
  maintainers.
  
  We hope you've enjoyed this whirlwind tour of using LiquidHaskell to verify
  production code, we have many more examples in the `benchmarks` folder of
  our GitHub repository for the intrepid reader.
  