content: {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE DataKinds #-}
  
  --------------------------------------------------------------------------------
  -- (c) Galois, Inc. 2014.
  -- All rights reserved.
  
  -- | Check for undefined bitshift behavior. Bit-shifts on signed ints are
  -- already disallowed. This check is that we bit-shift by strictly less than n
  -- for an n-bit value.
  --------------------------------------------------------------------------------
  
  module Ivory.Opts.BitShift
    ( bitShiftFold
    ) where
  
  import Ivory.Opts.AssertFold
  
  import qualified Ivory.Language.Syntax.AST   as I
  import qualified Ivory.Language.Syntax.Type  as I
  import Ivory.Language
  
  --------------------------------------------------------------------------------
  
  bitShiftFold :: I.Proc -> I.Proc
  bitShiftFold = procFold "bits" (expFoldDefault bitShiftAssert)
  
  --------------------------------------------------------------------------------
  
  bitShiftAssert :: I.Type -> I.Expr -> FolderStmt ()
  bitShiftAssert ty e = case e of
    I.ExpOp op es -> go op es
    _             -> return ()
    where
    go op es = case op of
      I.ExpBitShiftL -> assrt
      I.ExpBitShiftR -> assrt
      _              -> return ()
  
      where
      assrt = case ty of
        I.TyWord w -> case w of
                        I.Word8  -> mkAsst (iBitSize (0 :: Uint8))
                        I.Word16 -> mkAsst (iBitSize (0 :: Uint16))
                        I.Word32 -> mkAsst (iBitSize (0 :: Uint32))
                        I.Word64 -> mkAsst (iBitSize (0 :: Uint64))
        _          -> return ()
  
      mkAsst sz = insert $ I.CompilerAssert $ I.ExpOp (I.ExpLt False ty)
                    [es !! 1, fromIntegral sz]
  
  --------------------------------------------------------------------------------
  