-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Bytes
-- Description      : A type representing numbers of bytes.
-- Copyright        : (c) Galois, Inc 2011-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

module Lang.Crucible.LLVM.Bytes
  ( -- * Bytes
    Bytes(..)
  , Addr
  , Offset
  , bytesToBits
  , bytesToNatural
  , bytesToInteger
  , bytesToBV
  , toBytes
  , bitsToBytes
  , natBytesMul
  )  where

import qualified Data.BitVector.Sized as BV
import Data.Parameterized.NatRepr
import Numeric.Natural

-- | A newtype for expressing numbers of bytes.
--   This newtype is explicitly introduced to avoid confusion
--   between widths expressed as numbers of bits vs numbers of bytes.
newtype Bytes = Bytes { Bytes -> Integer
unBytes :: Integer }
  deriving (Bytes -> Bytes -> Bool
(Bytes -> Bytes -> Bool) -> (Bytes -> Bytes -> Bool) -> Eq Bytes
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bytes -> Bytes -> Bool
== :: Bytes -> Bytes -> Bool
$c/= :: Bytes -> Bytes -> Bool
/= :: Bytes -> Bytes -> Bool
Eq, Eq Bytes
Eq Bytes =>
(Bytes -> Bytes -> Ordering)
-> (Bytes -> Bytes -> Bool)
-> (Bytes -> Bytes -> Bool)
-> (Bytes -> Bytes -> Bool)
-> (Bytes -> Bytes -> Bool)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> Ord Bytes
Bytes -> Bytes -> Bool
Bytes -> Bytes -> Ordering
Bytes -> Bytes -> Bytes
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Bytes -> Bytes -> Ordering
compare :: Bytes -> Bytes -> Ordering
$c< :: Bytes -> Bytes -> Bool
< :: Bytes -> Bytes -> Bool
$c<= :: Bytes -> Bytes -> Bool
<= :: Bytes -> Bytes -> Bool
$c> :: Bytes -> Bytes -> Bool
> :: Bytes -> Bytes -> Bool
$c>= :: Bytes -> Bytes -> Bool
>= :: Bytes -> Bytes -> Bool
$cmax :: Bytes -> Bytes -> Bytes
max :: Bytes -> Bytes -> Bytes
$cmin :: Bytes -> Bytes -> Bytes
min :: Bytes -> Bytes -> Bytes
Ord, Integer -> Bytes
Bytes -> Bytes
Bytes -> Bytes -> Bytes
(Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes)
-> (Bytes -> Bytes)
-> (Bytes -> Bytes)
-> (Integer -> Bytes)
-> Num Bytes
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Bytes -> Bytes -> Bytes
+ :: Bytes -> Bytes -> Bytes
$c- :: Bytes -> Bytes -> Bytes
- :: Bytes -> Bytes -> Bytes
$c* :: Bytes -> Bytes -> Bytes
* :: Bytes -> Bytes -> Bytes
$cnegate :: Bytes -> Bytes
negate :: Bytes -> Bytes
$cabs :: Bytes -> Bytes
abs :: Bytes -> Bytes
$csignum :: Bytes -> Bytes
signum :: Bytes -> Bytes
$cfromInteger :: Integer -> Bytes
fromInteger :: Integer -> Bytes
Num, Int -> Bytes
Bytes -> Int
Bytes -> [Bytes]
Bytes -> Bytes
Bytes -> Bytes -> [Bytes]
Bytes -> Bytes -> Bytes -> [Bytes]
(Bytes -> Bytes)
-> (Bytes -> Bytes)
-> (Int -> Bytes)
-> (Bytes -> Int)
-> (Bytes -> [Bytes])
-> (Bytes -> Bytes -> [Bytes])
-> (Bytes -> Bytes -> [Bytes])
-> (Bytes -> Bytes -> Bytes -> [Bytes])
-> Enum Bytes
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Bytes -> Bytes
succ :: Bytes -> Bytes
$cpred :: Bytes -> Bytes
pred :: Bytes -> Bytes
$ctoEnum :: Int -> Bytes
toEnum :: Int -> Bytes
$cfromEnum :: Bytes -> Int
fromEnum :: Bytes -> Int
$cenumFrom :: Bytes -> [Bytes]
enumFrom :: Bytes -> [Bytes]
$cenumFromThen :: Bytes -> Bytes -> [Bytes]
enumFromThen :: Bytes -> Bytes -> [Bytes]
$cenumFromTo :: Bytes -> Bytes -> [Bytes]
enumFromTo :: Bytes -> Bytes -> [Bytes]
$cenumFromThenTo :: Bytes -> Bytes -> Bytes -> [Bytes]
enumFromThenTo :: Bytes -> Bytes -> Bytes -> [Bytes]
Enum, Num Bytes
Ord Bytes
(Num Bytes, Ord Bytes) => (Bytes -> Rational) -> Real Bytes
Bytes -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
$ctoRational :: Bytes -> Rational
toRational :: Bytes -> Rational
Real, Enum Bytes
Real Bytes
(Real Bytes, Enum Bytes) =>
(Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> Bytes)
-> (Bytes -> Bytes -> (Bytes, Bytes))
-> (Bytes -> Bytes -> (Bytes, Bytes))
-> (Bytes -> Integer)
-> Integral Bytes
Bytes -> Integer
Bytes -> Bytes -> (Bytes, Bytes)
Bytes -> Bytes -> Bytes
forall a.
(Real a, Enum a) =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: Bytes -> Bytes -> Bytes
quot :: Bytes -> Bytes -> Bytes
$crem :: Bytes -> Bytes -> Bytes
rem :: Bytes -> Bytes -> Bytes
$cdiv :: Bytes -> Bytes -> Bytes
div :: Bytes -> Bytes -> Bytes
$cmod :: Bytes -> Bytes -> Bytes
mod :: Bytes -> Bytes -> Bytes
$cquotRem :: Bytes -> Bytes -> (Bytes, Bytes)
quotRem :: Bytes -> Bytes -> (Bytes, Bytes)
$cdivMod :: Bytes -> Bytes -> (Bytes, Bytes)
divMod :: Bytes -> Bytes -> (Bytes, Bytes)
$ctoInteger :: Bytes -> Integer
toInteger :: Bytes -> Integer
Integral)

instance Show Bytes where
  show :: Bytes -> String
show (Bytes Integer
n) = Integer -> String
forall a. Show a => a -> String
show Integer
n

bytesToBits :: Bytes -> Natural
bytesToBits :: Bytes -> Natural
bytesToBits (Bytes Integer
n) = Natural
8 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
* Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n

bytesToNatural :: Bytes -> Natural
bytesToNatural :: Bytes -> Natural
bytesToNatural (Bytes Integer
n) = Integer -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n

bytesToInteger :: Bytes -> Integer
bytesToInteger :: Bytes -> Integer
bytesToInteger (Bytes Integer
n) = Integer
n

bytesToBV :: NatRepr w -> Bytes -> BV.BV w
bytesToBV :: forall (w :: Natural). NatRepr w -> Bytes -> BV w
bytesToBV NatRepr w
w = NatRepr w -> Integer -> BV w
forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w (Integer -> BV w) -> (Bytes -> Integer) -> Bytes -> BV w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bytes -> Integer
bytesToInteger

toBytes :: Integral a => a -> Bytes
toBytes :: forall a. Integral a => a -> Bytes
toBytes = Integer -> Bytes
Bytes (Integer -> Bytes) -> (a -> Integer) -> a -> Bytes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral

bitsToBytes :: Integral a => a -> Bytes
bitsToBytes :: forall a. Integral a => a -> Bytes
bitsToBytes a
n = Integer -> Bytes
Bytes ( (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
7) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
8 )

-- | Multiply a number of bytes by a natural number
natBytesMul :: Natural -> Bytes -> Bytes
natBytesMul :: Natural -> Bytes -> Bytes
natBytesMul Natural
n (Bytes Integer
x) = Integer -> Bytes
Bytes (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
x)

type Addr = Bytes
type Offset = Bytes