-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Type
-- Description      : Representation of storable types used by the memory model
-- Copyright        : (c) Galois, Inc 2011-2016
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}

module Lang.Crucible.LLVM.MemModel.Type
  ( -- * Storable types
    StorageType(..)
  , StorageTypeF(..)
  , bitvectorType
  , floatType
  , doubleType
  , x86_fp80Type
  , arrayType
  , structType
  , mkStructType
  , mkStorageType
  , typeEnd
  , Field
  , fieldVal
  , fieldPad
  , fieldOffset
  , mkField
  , ppType
  )  where

import Control.Lens
import Control.Monad.State
import Data.Typeable
import Data.Vector (Vector)
import qualified Data.Vector as V
import Numeric.Natural
import Prettyprinter

import Lang.Crucible.LLVM.Bytes

data Field v =
  Field
  { forall v. Field v -> Addr
fieldOffset :: !Offset
  , forall v. Field v -> v
_fieldVal   :: !v
  , forall v. Field v -> Addr
fieldPad    :: !Bytes
  }
  deriving (Field v -> Field v -> Bool
(Field v -> Field v -> Bool)
-> (Field v -> Field v -> Bool) -> Eq (Field v)
forall v. Eq v => Field v -> Field v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => Field v -> Field v -> Bool
== :: Field v -> Field v -> Bool
$c/= :: forall v. Eq v => Field v -> Field v -> Bool
/= :: Field v -> Field v -> Bool
Eq, Eq (Field v)
Eq (Field v) =>
(Field v -> Field v -> Ordering)
-> (Field v -> Field v -> Bool)
-> (Field v -> Field v -> Bool)
-> (Field v -> Field v -> Bool)
-> (Field v -> Field v -> Bool)
-> (Field v -> Field v -> Field v)
-> (Field v -> Field v -> Field v)
-> Ord (Field v)
Field v -> Field v -> Bool
Field v -> Field v -> Ordering
Field v -> Field v -> Field v
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
forall v. Ord v => Eq (Field v)
forall v. Ord v => Field v -> Field v -> Bool
forall v. Ord v => Field v -> Field v -> Ordering
forall v. Ord v => Field v -> Field v -> Field v
$ccompare :: forall v. Ord v => Field v -> Field v -> Ordering
compare :: Field v -> Field v -> Ordering
$c< :: forall v. Ord v => Field v -> Field v -> Bool
< :: Field v -> Field v -> Bool
$c<= :: forall v. Ord v => Field v -> Field v -> Bool
<= :: Field v -> Field v -> Bool
$c> :: forall v. Ord v => Field v -> Field v -> Bool
> :: Field v -> Field v -> Bool
$c>= :: forall v. Ord v => Field v -> Field v -> Bool
>= :: Field v -> Field v -> Bool
$cmax :: forall v. Ord v => Field v -> Field v -> Field v
max :: Field v -> Field v -> Field v
$cmin :: forall v. Ord v => Field v -> Field v -> Field v
min :: Field v -> Field v -> Field v
Ord, Int -> Field v -> ShowS
[Field v] -> ShowS
Field v -> String
(Int -> Field v -> ShowS)
-> (Field v -> String) -> ([Field v] -> ShowS) -> Show (Field v)
forall v. Show v => Int -> Field v -> ShowS
forall v. Show v => [Field v] -> ShowS
forall v. Show v => Field v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Field v -> ShowS
showsPrec :: Int -> Field v -> ShowS
$cshow :: forall v. Show v => Field v -> String
show :: Field v -> String
$cshowList :: forall v. Show v => [Field v] -> ShowS
showList :: [Field v] -> ShowS
Show, (forall a b. (a -> b) -> Field a -> Field b)
-> (forall a b. a -> Field b -> Field a) -> Functor Field
forall a b. a -> Field b -> Field a
forall a b. (a -> b) -> Field a -> Field b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Field a -> Field b
fmap :: forall a b. (a -> b) -> Field a -> Field b
$c<$ :: forall a b. a -> Field b -> Field a
<$ :: forall a b. a -> Field b -> Field a
Functor, (forall m. Monoid m => Field m -> m)
-> (forall m a. Monoid m => (a -> m) -> Field a -> m)
-> (forall m a. Monoid m => (a -> m) -> Field a -> m)
-> (forall a b. (a -> b -> b) -> b -> Field a -> b)
-> (forall a b. (a -> b -> b) -> b -> Field a -> b)
-> (forall b a. (b -> a -> b) -> b -> Field a -> b)
-> (forall b a. (b -> a -> b) -> b -> Field a -> b)
-> (forall a. (a -> a -> a) -> Field a -> a)
-> (forall a. (a -> a -> a) -> Field a -> a)
-> (forall a. Field a -> [a])
-> (forall a. Field a -> Bool)
-> (forall a. Field a -> Int)
-> (forall a. Eq a => a -> Field a -> Bool)
-> (forall a. Ord a => Field a -> a)
-> (forall a. Ord a => Field a -> a)
-> (forall a. Num a => Field a -> a)
-> (forall a. Num a => Field a -> a)
-> Foldable Field
forall a. Eq a => a -> Field a -> Bool
forall a. Num a => Field a -> a
forall a. Ord a => Field a -> a
forall m. Monoid m => Field m -> m
forall a. Field a -> Bool
forall a. Field a -> Int
forall a. Field a -> [a]
forall a. (a -> a -> a) -> Field a -> a
forall m a. Monoid m => (a -> m) -> Field a -> m
forall b a. (b -> a -> b) -> b -> Field a -> b
forall a b. (a -> b -> b) -> b -> Field a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Field m -> m
fold :: forall m. Monoid m => Field m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Field a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Field a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Field a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Field a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Field a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Field a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Field a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Field a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Field a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Field a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Field a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Field a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Field a -> a
foldr1 :: forall a. (a -> a -> a) -> Field a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Field a -> a
foldl1 :: forall a. (a -> a -> a) -> Field a -> a
$ctoList :: forall a. Field a -> [a]
toList :: forall a. Field a -> [a]
$cnull :: forall a. Field a -> Bool
null :: forall a. Field a -> Bool
$clength :: forall a. Field a -> Int
length :: forall a. Field a -> Int
$celem :: forall a. Eq a => a -> Field a -> Bool
elem :: forall a. Eq a => a -> Field a -> Bool
$cmaximum :: forall a. Ord a => Field a -> a
maximum :: forall a. Ord a => Field a -> a
$cminimum :: forall a. Ord a => Field a -> a
minimum :: forall a. Ord a => Field a -> a
$csum :: forall a. Num a => Field a -> a
sum :: forall a. Num a => Field a -> a
$cproduct :: forall a. Num a => Field a -> a
product :: forall a. Num a => Field a -> a
Foldable, Functor Field
Foldable Field
(Functor Field, Foldable Field) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> Field a -> f (Field b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Field (f a) -> f (Field a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Field a -> m (Field b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Field (m a) -> m (Field a))
-> Traversable Field
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a. Monad m => Field (m a) -> m (Field a)
forall (f :: Type -> Type) a.
Applicative f =>
Field (f a) -> f (Field a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Field a -> m (Field b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Field a -> f (Field b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Field a -> f (Field b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Field a -> f (Field b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Field (f a) -> f (Field a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Field (f a) -> f (Field a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Field a -> m (Field b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Field a -> m (Field b)
$csequence :: forall (m :: Type -> Type) a. Monad m => Field (m a) -> m (Field a)
sequence :: forall (m :: Type -> Type) a. Monad m => Field (m a) -> m (Field a)
Traversable, Typeable)

fieldVal :: Lens (Field a) (Field b) a b
fieldVal :: forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal = (Field a -> a)
-> (Field a -> b -> Field b) -> Lens (Field a) (Field b) a b
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens Field a -> a
forall v. Field v -> v
_fieldVal (\Field a
s b
v -> Field a
s { _fieldVal = v })

mkField :: Offset -> v -> Bytes -> Field v
mkField :: forall v. Addr -> v -> Addr -> Field v
mkField = Addr -> v -> Addr -> Field v
forall v. Addr -> v -> Addr -> Field v
Field

data StorageTypeF v
  = Bitvector !Bytes -- ^ Size of bitvector in bytes (must be > 0).
  | Float
  | Double
  | X86_FP80
  | Array !Natural !v -- ^ Number of elements and element type
  | Struct !(Vector (Field v))
  deriving (StorageTypeF v -> StorageTypeF v -> Bool
(StorageTypeF v -> StorageTypeF v -> Bool)
-> (StorageTypeF v -> StorageTypeF v -> Bool)
-> Eq (StorageTypeF v)
forall v. Eq v => StorageTypeF v -> StorageTypeF v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => StorageTypeF v -> StorageTypeF v -> Bool
== :: StorageTypeF v -> StorageTypeF v -> Bool
$c/= :: forall v. Eq v => StorageTypeF v -> StorageTypeF v -> Bool
/= :: StorageTypeF v -> StorageTypeF v -> Bool
Eq, Eq (StorageTypeF v)
Eq (StorageTypeF v) =>
(StorageTypeF v -> StorageTypeF v -> Ordering)
-> (StorageTypeF v -> StorageTypeF v -> Bool)
-> (StorageTypeF v -> StorageTypeF v -> Bool)
-> (StorageTypeF v -> StorageTypeF v -> Bool)
-> (StorageTypeF v -> StorageTypeF v -> Bool)
-> (StorageTypeF v -> StorageTypeF v -> StorageTypeF v)
-> (StorageTypeF v -> StorageTypeF v -> StorageTypeF v)
-> Ord (StorageTypeF v)
StorageTypeF v -> StorageTypeF v -> Bool
StorageTypeF v -> StorageTypeF v -> Ordering
StorageTypeF v -> StorageTypeF v -> StorageTypeF v
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
forall v. Ord v => Eq (StorageTypeF v)
forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Bool
forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Ordering
forall v.
Ord v =>
StorageTypeF v -> StorageTypeF v -> StorageTypeF v
$ccompare :: forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Ordering
compare :: StorageTypeF v -> StorageTypeF v -> Ordering
$c< :: forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Bool
< :: StorageTypeF v -> StorageTypeF v -> Bool
$c<= :: forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Bool
<= :: StorageTypeF v -> StorageTypeF v -> Bool
$c> :: forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Bool
> :: StorageTypeF v -> StorageTypeF v -> Bool
$c>= :: forall v. Ord v => StorageTypeF v -> StorageTypeF v -> Bool
>= :: StorageTypeF v -> StorageTypeF v -> Bool
$cmax :: forall v.
Ord v =>
StorageTypeF v -> StorageTypeF v -> StorageTypeF v
max :: StorageTypeF v -> StorageTypeF v -> StorageTypeF v
$cmin :: forall v.
Ord v =>
StorageTypeF v -> StorageTypeF v -> StorageTypeF v
min :: StorageTypeF v -> StorageTypeF v -> StorageTypeF v
Ord, Int -> StorageTypeF v -> ShowS
[StorageTypeF v] -> ShowS
StorageTypeF v -> String
(Int -> StorageTypeF v -> ShowS)
-> (StorageTypeF v -> String)
-> ([StorageTypeF v] -> ShowS)
-> Show (StorageTypeF v)
forall v. Show v => Int -> StorageTypeF v -> ShowS
forall v. Show v => [StorageTypeF v] -> ShowS
forall v. Show v => StorageTypeF v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> StorageTypeF v -> ShowS
showsPrec :: Int -> StorageTypeF v -> ShowS
$cshow :: forall v. Show v => StorageTypeF v -> String
show :: StorageTypeF v -> String
$cshowList :: forall v. Show v => [StorageTypeF v] -> ShowS
showList :: [StorageTypeF v] -> ShowS
Show, Typeable)

-- | Represents the storage type of an LLVM value. A 'Type' specifies
-- how a value is represented as bytes in memory.
data StorageType =
  StorageType
  { StorageType -> StorageTypeF StorageType
storageTypeF :: !(StorageTypeF StorageType)
  , StorageType -> Addr
storageTypeSize :: !Bytes
  }
  deriving (StorageType -> StorageType -> Bool
(StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool) -> Eq StorageType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StorageType -> StorageType -> Bool
== :: StorageType -> StorageType -> Bool
$c/= :: StorageType -> StorageType -> Bool
/= :: StorageType -> StorageType -> Bool
Eq, Eq StorageType
Eq StorageType =>
(StorageType -> StorageType -> Ordering)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> Bool)
-> (StorageType -> StorageType -> StorageType)
-> (StorageType -> StorageType -> StorageType)
-> Ord StorageType
StorageType -> StorageType -> Bool
StorageType -> StorageType -> Ordering
StorageType -> StorageType -> StorageType
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 :: StorageType -> StorageType -> Ordering
compare :: StorageType -> StorageType -> Ordering
$c< :: StorageType -> StorageType -> Bool
< :: StorageType -> StorageType -> Bool
$c<= :: StorageType -> StorageType -> Bool
<= :: StorageType -> StorageType -> Bool
$c> :: StorageType -> StorageType -> Bool
> :: StorageType -> StorageType -> Bool
$c>= :: StorageType -> StorageType -> Bool
>= :: StorageType -> StorageType -> Bool
$cmax :: StorageType -> StorageType -> StorageType
max :: StorageType -> StorageType -> StorageType
$cmin :: StorageType -> StorageType -> StorageType
min :: StorageType -> StorageType -> StorageType
Ord, Typeable)

instance Show StorageType where
  showsPrec :: Int -> StorageType -> ShowS
showsPrec Int
p StorageType
t = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
t of
      Bitvector Addr
w -> String -> ShowS
showString String
"bitvectorType " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Addr -> ShowS
forall a. Show a => a -> ShowS
shows Addr
w
      StorageTypeF StorageType
Float -> String -> ShowS
showString String
"float"
      StorageTypeF StorageType
Double -> String -> ShowS
showString String
"double"
      StorageTypeF StorageType
X86_FP80 -> String -> ShowS
showString String
"long double"
      Array Natural
n StorageType
tp -> String -> ShowS
showString String
"arrayType " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> ShowS
forall a. Show a => a -> ShowS
shows Natural
n ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> StorageType -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 StorageType
tp
      Struct Vector (Field StorageType)
v -> String -> ShowS
showString String
"mkStructType " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(StorageType, Addr)] -> ShowS
forall a. Show a => a -> ShowS
shows (Vector (StorageType, Addr) -> [(StorageType, Addr)]
forall a. Vector a -> [a]
V.toList (Field StorageType -> (StorageType, Addr)
forall {v}. Field v -> (v, Addr)
fldFn (Field StorageType -> (StorageType, Addr))
-> Vector (Field StorageType) -> Vector (StorageType, Addr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Field StorageType)
v))
        where fldFn :: Field v -> (v, Addr)
fldFn Field v
f = (Field v
fField v -> Getting v (Field v) v -> v
forall s a. s -> Getting a s a -> a
^.Getting v (Field v) v
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal, Field v -> Addr
forall v. Field v -> Addr
fieldPad Field v
f)

mkStorageType :: StorageTypeF StorageType -> StorageType
mkStorageType :: StorageTypeF StorageType -> StorageType
mkStorageType StorageTypeF StorageType
tf = StorageTypeF StorageType -> Addr -> StorageType
StorageType StorageTypeF StorageType
tf (Addr -> StorageType) -> Addr -> StorageType
forall a b. (a -> b) -> a -> b
$
  case StorageTypeF StorageType
tf of
    Bitvector Addr
w -> Addr
w
    StorageTypeF StorageType
Float -> Addr
4
    StorageTypeF StorageType
Double -> Addr
8
    StorageTypeF StorageType
X86_FP80 -> Addr
10
    Array Natural
n StorageType
e -> Natural -> Addr -> Addr
natBytesMul Natural
n (StorageType -> Addr
storageTypeSize StorageType
e)
    Struct Vector (Field StorageType)
flds -> Vector (Field StorageType) -> Addr
structSize Vector (Field StorageType)
flds

bitvectorType :: Bytes -> StorageType
bitvectorType :: Addr -> StorageType
bitvectorType Addr
w = StorageTypeF StorageType -> Addr -> StorageType
StorageType (Addr -> StorageTypeF StorageType
forall v. Addr -> StorageTypeF v
Bitvector Addr
w) Addr
w

floatType :: StorageType
floatType :: StorageType
floatType = StorageTypeF StorageType -> StorageType
mkStorageType StorageTypeF StorageType
forall v. StorageTypeF v
Float

doubleType :: StorageType
doubleType :: StorageType
doubleType = StorageTypeF StorageType -> StorageType
mkStorageType StorageTypeF StorageType
forall v. StorageTypeF v
Double

x86_fp80Type :: StorageType
x86_fp80Type :: StorageType
x86_fp80Type = StorageTypeF StorageType -> StorageType
mkStorageType StorageTypeF StorageType
forall v. StorageTypeF v
X86_FP80

arrayType :: Natural -> StorageType -> StorageType
arrayType :: Natural -> StorageType -> StorageType
arrayType Natural
n StorageType
e = StorageTypeF StorageType -> Addr -> StorageType
StorageType (Natural -> StorageType -> StorageTypeF StorageType
forall v. Natural -> v -> StorageTypeF v
Array Natural
n StorageType
e) (Natural -> Addr -> Addr
natBytesMul Natural
n (StorageType -> Addr
storageTypeSize StorageType
e))

structType :: V.Vector (Field StorageType) -> StorageType
structType :: Vector (Field StorageType) -> StorageType
structType Vector (Field StorageType)
flds = StorageTypeF StorageType -> Addr -> StorageType
StorageType (Vector (Field StorageType) -> StorageTypeF StorageType
forall v. Vector (Field v) -> StorageTypeF v
Struct Vector (Field StorageType)
flds) (Vector (Field StorageType) -> Addr
structSize Vector (Field StorageType)
flds)

mkStructType :: V.Vector (StorageType, Bytes) -> StorageType
mkStructType :: Vector (StorageType, Addr) -> StorageType
mkStructType Vector (StorageType, Addr)
l = Vector (Field StorageType) -> StorageType
structType (State Addr (Vector (Field StorageType))
-> Addr -> Vector (Field StorageType)
forall s a. State s a -> s -> a
evalState (((StorageType, Addr) -> StateT Addr Identity (Field StorageType))
-> Vector (StorageType, Addr)
-> State Addr (Vector (Field StorageType))
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Vector a -> f (Vector b)
traverse (StorageType, Addr) -> StateT Addr Identity (Field StorageType)
forall {m :: Type -> Type}.
MonadState Addr m =>
(StorageType, Addr) -> m (Field StorageType)
fldFn Vector (StorageType, Addr)
l) Addr
0)
  where
    fldFn :: (StorageType, Addr) -> m (Field StorageType)
fldFn (StorageType
tp,Addr
p) =
      do Addr
o <- m Addr
forall s (m :: Type -> Type). MonadState s m => m s
get
         Addr -> m ()
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put (Addr -> m ()) -> Addr -> m ()
forall a b. (a -> b) -> a -> b
$! Addr
o Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ StorageType -> Addr
storageTypeSize StorageType
tp Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
p
         Field StorageType -> m (Field StorageType)
forall a. a -> m a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Field { fieldOffset :: Addr
fieldOffset = Addr
o
                      , _fieldVal :: StorageType
_fieldVal = StorageType
tp
                      , fieldPad :: Addr
fieldPad = Addr
p
                      }

-- | Returns end of actual type bytes (excluded padding from structs).
typeEnd :: Addr -> StorageType -> Addr
typeEnd :: Addr -> StorageType -> Addr
typeEnd Addr
a StorageType
tp = Addr -> Addr -> Addr
forall a b. a -> b -> b
seq Addr
a (Addr -> Addr) -> Addr -> Addr
forall a b. (a -> b) -> a -> b
$
  case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
    Bitvector Addr
w -> Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
w
    StorageTypeF StorageType
Float -> Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
4
    StorageTypeF StorageType
Double -> Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
8
    StorageTypeF StorageType
X86_FP80 -> Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
10
    Array Natural
0 StorageType
_   -> Addr
a
    Array Natural
n StorageType
etp -> Addr -> StorageType -> Addr
typeEnd (Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Natural -> Addr -> Addr
natBytesMul (Natural
nNatural -> Natural -> Natural
forall a. Num a => a -> a -> a
-Natural
1) (StorageType -> Addr
storageTypeSize StorageType
etp)) StorageType
etp
    Struct Vector (Field StorageType)
flds ->
      case Vector (Field StorageType)
-> Maybe (Vector (Field StorageType), Field StorageType)
forall a. Vector a -> Maybe (Vector a, a)
V.unsnoc Vector (Field StorageType)
flds of
        Just (Vector (Field StorageType)
_, Field StorageType
f) -> Addr -> StorageType -> Addr
typeEnd (Addr
a Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Field StorageType -> Addr
forall v. Field v -> Addr
fieldOffset Field StorageType
f) (Field StorageType
fField StorageType
-> Getting StorageType (Field StorageType) StorageType
-> StorageType
forall s a. s -> Getting a s a -> a
^.Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal)
        Maybe (Vector (Field StorageType), Field StorageType)
Nothing -> Addr
a

-- | Returns end of field including padding bytes.
structSize :: V.Vector (Field StorageType) -> Bytes
structSize :: Vector (Field StorageType) -> Addr
structSize Vector (Field StorageType)
flds =
  case Vector (Field StorageType)
-> Maybe (Vector (Field StorageType), Field StorageType)
forall a. Vector a -> Maybe (Vector a, a)
V.unsnoc Vector (Field StorageType)
flds of
    Just (Vector (Field StorageType)
_, Field StorageType
f) -> Field StorageType -> Addr
fieldEnd Field StorageType
f
    Maybe (Vector (Field StorageType), Field StorageType)
Nothing -> Addr
0

-- | Returns end of field including padding bytes.
fieldEnd :: Field StorageType -> Bytes
fieldEnd :: Field StorageType -> Addr
fieldEnd Field StorageType
f = Field StorageType -> Addr
forall v. Field v -> Addr
fieldOffset Field StorageType
f Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ StorageType -> Addr
storageTypeSize (Field StorageType
fField StorageType
-> Getting StorageType (Field StorageType) StorageType
-> StorageType
forall s a. s -> Getting a s a -> a
^.Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal) Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Field StorageType -> Addr
forall v. Field v -> Addr
fieldPad Field StorageType
f


-- | Pretty print type.
ppType :: StorageType -> Doc ann
ppType :: forall ann. StorageType -> Doc ann
ppType StorageType
tp =
  case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
    Bitvector Addr
w -> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'i' Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Natural -> Doc ann
forall ann. Natural -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Addr -> Natural
bytesToBits Addr
w)
    StorageTypeF StorageType
Float -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"float"
    StorageTypeF StorageType
Double -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"double"
    StorageTypeF StorageType
X86_FP80 -> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"long double"
    Array Natural
n StorageType
etp -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
brackets (Natural -> Doc ann
forall ann. Natural -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Natural
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
'x' Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType StorageType
etp)
    Struct Vector (Field StorageType)
flds -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate (Char -> Doc ann
forall ann. Char -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Char
',') ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Vector (Doc ann) -> [Doc ann]
forall a. Vector a -> [a]
V.toList (Vector (Doc ann) -> [Doc ann]) -> Vector (Doc ann) -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Field StorageType -> Doc ann
forall {ann}. Field StorageType -> Doc ann
ppFld (Field StorageType -> Doc ann)
-> Vector (Field StorageType) -> Vector (Doc ann)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Field StorageType)
flds
      where ppFld :: Field StorageType -> Doc ann
ppFld Field StorageType
f = StorageType -> Doc ann
forall ann. StorageType -> Doc ann
ppType (Field StorageType
fField StorageType
-> Getting StorageType (Field StorageType) StorageType
-> StorageType
forall s a. s -> Getting a s a -> a
^.Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal)