-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Common
-- Description      : Core definitions of the symbolic C 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.Common
  ( -- * Range declarations.
    Range(..)

    -- * Pointer declarations
  , OffsetExpr(..)
  , IntExpr(..)
  , Cond(..)

  , Mux(..)

  , ValueCtor(..)

  , BasePreference(..)

  , RangeLoad(..)
  , rangeLoad
  , fixedOffsetRangeLoad
  , fixedSizeRangeLoad
  , symbolicRangeLoad
  , symbolicUnboundedRangeLoad

  , ValueView(..)

  , ValueLoad(..)
  , valueLoad
  , LinearLoadStoreOffsetDiff(..)
  , symbolicValueLoad
  , loadBitvector

  , memsetValue
  , loadTypedValueFromBytes
  ) where

import Control.Exception (assert)
import Control.Lens
import Control.Monad (guard)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Vector (Vector)
import qualified Data.Vector as V
import Numeric.Natural

import Lang.Crucible.Panic ( panic )
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.LLVM.MemModel.Type

-- | @R i j@ denotes that the write should store in range [i..j).
data Range = R { Range -> Bytes
rStart :: Addr, Range -> Bytes
_rEnd :: Addr }
  deriving (Range -> Range -> Bool
(Range -> Range -> Bool) -> (Range -> Range -> Bool) -> Eq Range
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Range -> Range -> Bool
== :: Range -> Range -> Bool
$c/= :: Range -> Range -> Bool
/= :: Range -> Range -> Bool
Eq, Int -> Range -> ShowS
[Range] -> ShowS
Range -> String
(Int -> Range -> ShowS)
-> (Range -> String) -> ([Range] -> ShowS) -> Show Range
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Range -> ShowS
showsPrec :: Int -> Range -> ShowS
$cshow :: Range -> String
show :: Range -> String
$cshowList :: [Range] -> ShowS
showList :: [Range] -> ShowS
Show)

-- Value

data OffsetExpr
  = OffsetAdd OffsetExpr IntExpr
  | Load
  | Store
  deriving (Int -> OffsetExpr -> ShowS
[OffsetExpr] -> ShowS
OffsetExpr -> String
(Int -> OffsetExpr -> ShowS)
-> (OffsetExpr -> String)
-> ([OffsetExpr] -> ShowS)
-> Show OffsetExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OffsetExpr -> ShowS
showsPrec :: Int -> OffsetExpr -> ShowS
$cshow :: OffsetExpr -> String
show :: OffsetExpr -> String
$cshowList :: [OffsetExpr] -> ShowS
showList :: [OffsetExpr] -> ShowS
Show)

data IntExpr
  = OffsetDiff OffsetExpr OffsetExpr
  | IntAdd IntExpr IntExpr
  | CValue Bytes
  | StoreSize
  deriving (Int -> IntExpr -> ShowS
[IntExpr] -> ShowS
IntExpr -> String
(Int -> IntExpr -> ShowS)
-> (IntExpr -> String) -> ([IntExpr] -> ShowS) -> Show IntExpr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntExpr -> ShowS
showsPrec :: Int -> IntExpr -> ShowS
$cshow :: IntExpr -> String
show :: IntExpr -> String
$cshowList :: [IntExpr] -> ShowS
showList :: [IntExpr] -> ShowS
Show)

data Cond
  = OffsetEq OffsetExpr OffsetExpr
  | OffsetLe OffsetExpr OffsetExpr
  | IntEq IntExpr IntExpr
  | IntLe IntExpr IntExpr
  | And Cond Cond
  | Or Cond Cond
  deriving (Int -> Cond -> ShowS
[Cond] -> ShowS
Cond -> String
(Int -> Cond -> ShowS)
-> (Cond -> String) -> ([Cond] -> ShowS) -> Show Cond
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cond -> ShowS
showsPrec :: Int -> Cond -> ShowS
$cshow :: Cond -> String
show :: Cond -> String
$cshowList :: [Cond] -> ShowS
showList :: [Cond] -> ShowS
Show)

(.==) :: OffsetExpr -> OffsetExpr -> Cond
infix 4 .==
OffsetExpr
x .== :: OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
y = OffsetExpr -> OffsetExpr -> Cond
OffsetEq OffsetExpr
x OffsetExpr
y

(.<=) :: OffsetExpr -> OffsetExpr -> Cond
infix 4 .<=
OffsetExpr
x .<= :: OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
y = OffsetExpr -> OffsetExpr -> Cond
OffsetLe OffsetExpr
x OffsetExpr
y

infixl 6 .+
(.+) :: OffsetExpr -> IntExpr -> OffsetExpr
OffsetExpr
x .+ :: OffsetExpr -> IntExpr -> OffsetExpr
.+ CValue Bytes
0 = OffsetExpr
x
OffsetExpr
x .+ IntExpr
y = OffsetExpr -> IntExpr -> OffsetExpr
OffsetAdd OffsetExpr
x IntExpr
y

infixl 6 .-
(.-) :: OffsetExpr -> OffsetExpr -> IntExpr
OffsetExpr
x .- :: OffsetExpr -> OffsetExpr -> IntExpr
.- OffsetExpr
y = OffsetExpr -> OffsetExpr -> IntExpr
OffsetDiff OffsetExpr
x OffsetExpr
y

-- Muxs

data Mux a
  = Mux Cond (Mux a) (Mux a)
  | MuxTable OffsetExpr OffsetExpr (Map Bytes (Mux a)) (Mux a)
    -- ^ 'MuxTable' encodes a lookup table: @'MuxTable' p1 p2
    -- 'Map.empty' z@ is equivalent to @z@, and @'MuxTable' p1 p2
    -- ('Map.insert' (i, x) m) z@ is equivalent to @'Mux' (p1 '.+'
    -- 'CValue' i '.==' p2) x ('MuxTable' p1 p2 m z)@.
  | MuxVar a
  deriving Int -> Mux a -> ShowS
[Mux a] -> ShowS
Mux a -> String
(Int -> Mux a -> ShowS)
-> (Mux a -> String) -> ([Mux a] -> ShowS) -> Show (Mux a)
forall a. Show a => Int -> Mux a -> ShowS
forall a. Show a => [Mux a] -> ShowS
forall a. Show a => Mux a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Mux a -> ShowS
showsPrec :: Int -> Mux a -> ShowS
$cshow :: forall a. Show a => Mux a -> String
show :: Mux a -> String
$cshowList :: forall a. Show a => [Mux a] -> ShowS
showList :: [Mux a] -> ShowS
Show

-- Variable for mem model.

loadOffset :: Bytes -> OffsetExpr
loadOffset :: Bytes -> OffsetExpr
loadOffset Bytes
n = OffsetExpr
Load OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue Bytes
n

storeOffset :: Bytes -> OffsetExpr
storeOffset :: Bytes -> OffsetExpr
storeOffset Bytes
n = OffsetExpr
Store OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue Bytes
n

storeEnd :: OffsetExpr
storeEnd :: OffsetExpr
storeEnd = OffsetExpr
Store OffsetExpr -> IntExpr -> OffsetExpr
.+ IntExpr
StoreSize

-- | @loadInStoreRange n@ returns predicate if Store <= Load && Load <= Store + n
loadInStoreRange :: Bytes -> Cond
loadInStoreRange :: Bytes -> Cond
loadInStoreRange (Bytes Integer
0) = OffsetExpr
Load OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
Store
loadInStoreRange Bytes
n = Cond -> Cond -> Cond
And (OffsetExpr
Store OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Load)
                         (OffsetExpr
Load OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Store OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue Bytes
n)

-- Value constructor

-- | Describes how to construct a larger LLVM value as a combination
-- of smaller components.
data ValueCtor a
  = ValueCtorVar a
    -- | Concatenates two bitvectors.
    -- The first bitvector contains values stored at the low-address bytes
    -- while the second contains values at the high-address bytes. Thus, the
    -- meaning of this depends on the endianness of the target architecture.
  | ConcatBV (ValueCtor a) (ValueCtor a)
  | BVToFloat (ValueCtor a)
  | BVToDouble (ValueCtor a)
  | BVToX86_FP80 (ValueCtor a)
    -- | Cons one value to beginning of array.
  | ConsArray (ValueCtor a) (ValueCtor a)
  | AppendArray (ValueCtor a) (ValueCtor a)
  | MkArray StorageType (Vector (ValueCtor a))
  | MkStruct (Vector (Field StorageType, ValueCtor a))
  deriving ((forall a b. (a -> b) -> ValueCtor a -> ValueCtor b)
-> (forall a b. a -> ValueCtor b -> ValueCtor a)
-> Functor ValueCtor
forall a b. a -> ValueCtor b -> ValueCtor a
forall a b. (a -> b) -> ValueCtor a -> ValueCtor 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) -> ValueCtor a -> ValueCtor b
fmap :: forall a b. (a -> b) -> ValueCtor a -> ValueCtor b
$c<$ :: forall a b. a -> ValueCtor b -> ValueCtor a
<$ :: forall a b. a -> ValueCtor b -> ValueCtor a
Functor, (forall m. Monoid m => ValueCtor m -> m)
-> (forall m a. Monoid m => (a -> m) -> ValueCtor a -> m)
-> (forall m a. Monoid m => (a -> m) -> ValueCtor a -> m)
-> (forall a b. (a -> b -> b) -> b -> ValueCtor a -> b)
-> (forall a b. (a -> b -> b) -> b -> ValueCtor a -> b)
-> (forall b a. (b -> a -> b) -> b -> ValueCtor a -> b)
-> (forall b a. (b -> a -> b) -> b -> ValueCtor a -> b)
-> (forall a. (a -> a -> a) -> ValueCtor a -> a)
-> (forall a. (a -> a -> a) -> ValueCtor a -> a)
-> (forall a. ValueCtor a -> [a])
-> (forall a. ValueCtor a -> Bool)
-> (forall a. ValueCtor a -> Int)
-> (forall a. Eq a => a -> ValueCtor a -> Bool)
-> (forall a. Ord a => ValueCtor a -> a)
-> (forall a. Ord a => ValueCtor a -> a)
-> (forall a. Num a => ValueCtor a -> a)
-> (forall a. Num a => ValueCtor a -> a)
-> Foldable ValueCtor
forall a. Eq a => a -> ValueCtor a -> Bool
forall a. Num a => ValueCtor a -> a
forall a. Ord a => ValueCtor a -> a
forall m. Monoid m => ValueCtor m -> m
forall a. ValueCtor a -> Bool
forall a. ValueCtor a -> Int
forall a. ValueCtor a -> [a]
forall a. (a -> a -> a) -> ValueCtor a -> a
forall m a. Monoid m => (a -> m) -> ValueCtor a -> m
forall b a. (b -> a -> b) -> b -> ValueCtor a -> b
forall a b. (a -> b -> b) -> b -> ValueCtor 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 => ValueCtor m -> m
fold :: forall m. Monoid m => ValueCtor m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ValueCtor a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ValueCtor a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ValueCtor a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> ValueCtor a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> ValueCtor a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ValueCtor a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ValueCtor a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ValueCtor a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ValueCtor a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ValueCtor a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ValueCtor a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> ValueCtor a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> ValueCtor a -> a
foldr1 :: forall a. (a -> a -> a) -> ValueCtor a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ValueCtor a -> a
foldl1 :: forall a. (a -> a -> a) -> ValueCtor a -> a
$ctoList :: forall a. ValueCtor a -> [a]
toList :: forall a. ValueCtor a -> [a]
$cnull :: forall a. ValueCtor a -> Bool
null :: forall a. ValueCtor a -> Bool
$clength :: forall a. ValueCtor a -> Int
length :: forall a. ValueCtor a -> Int
$celem :: forall a. Eq a => a -> ValueCtor a -> Bool
elem :: forall a. Eq a => a -> ValueCtor a -> Bool
$cmaximum :: forall a. Ord a => ValueCtor a -> a
maximum :: forall a. Ord a => ValueCtor a -> a
$cminimum :: forall a. Ord a => ValueCtor a -> a
minimum :: forall a. Ord a => ValueCtor a -> a
$csum :: forall a. Num a => ValueCtor a -> a
sum :: forall a. Num a => ValueCtor a -> a
$cproduct :: forall a. Num a => ValueCtor a -> a
product :: forall a. Num a => ValueCtor a -> a
Foldable, Functor ValueCtor
Foldable ValueCtor
(Functor ValueCtor, Foldable ValueCtor) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> ValueCtor a -> f (ValueCtor b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    ValueCtor (f a) -> f (ValueCtor a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> ValueCtor a -> m (ValueCtor b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    ValueCtor (m a) -> m (ValueCtor a))
-> Traversable ValueCtor
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 =>
ValueCtor (m a) -> m (ValueCtor a)
forall (f :: Type -> Type) a.
Applicative f =>
ValueCtor (f a) -> f (ValueCtor a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> ValueCtor a -> m (ValueCtor b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> ValueCtor a -> f (ValueCtor b)
$ctraverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> ValueCtor a -> f (ValueCtor b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> ValueCtor a -> f (ValueCtor b)
$csequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
ValueCtor (f a) -> f (ValueCtor a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
ValueCtor (f a) -> f (ValueCtor a)
$cmapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> ValueCtor a -> m (ValueCtor b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> ValueCtor a -> m (ValueCtor b)
$csequence :: forall (m :: Type -> Type) a.
Monad m =>
ValueCtor (m a) -> m (ValueCtor a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
ValueCtor (m a) -> m (ValueCtor a)
Traversable, Int -> ValueCtor a -> ShowS
[ValueCtor a] -> ShowS
ValueCtor a -> String
(Int -> ValueCtor a -> ShowS)
-> (ValueCtor a -> String)
-> ([ValueCtor a] -> ShowS)
-> Show (ValueCtor a)
forall a. Show a => Int -> ValueCtor a -> ShowS
forall a. Show a => [ValueCtor a] -> ShowS
forall a. Show a => ValueCtor a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> ValueCtor a -> ShowS
showsPrec :: Int -> ValueCtor a -> ShowS
$cshow :: forall a. Show a => ValueCtor a -> String
show :: ValueCtor a -> String
$cshowList :: forall a. Show a => [ValueCtor a] -> ShowS
showList :: [ValueCtor a] -> ShowS
Show)

concatBV :: Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV :: forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
_xw ValueCtor a
x Bytes
_yw ValueCtor a
y = ValueCtor a -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a -> ValueCtor a
ConcatBV ValueCtor a
x ValueCtor a
y

singletonArray :: StorageType -> ValueCtor a -> ValueCtor a
singletonArray :: forall a. StorageType -> ValueCtor a -> ValueCtor a
singletonArray StorageType
tp ValueCtor a
e = StorageType -> Vector (ValueCtor a) -> ValueCtor a
forall a. StorageType -> Vector (ValueCtor a) -> ValueCtor a
MkArray StorageType
tp (ValueCtor a -> Vector (ValueCtor a)
forall a. a -> Vector a
V.singleton ValueCtor a
e)

-- | Create value of type that splits at a particular byte offset.
splitTypeValue :: StorageType   -- ^ Type of value to create
               -> Offset -- ^ Bytes offset to slice type at.
               -> (Offset -> StorageType -> ValueCtor a) -- ^ Function for subtypes.
               -> ValueCtor a
splitTypeValue :: forall a.
StorageType
-> Bytes -> (Bytes -> StorageType -> ValueCtor a) -> ValueCtor a
splitTypeValue StorageType
tp Bytes
d Bytes -> StorageType -> ValueCtor a
subFn = Bool -> ValueCtor a -> ValueCtor a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
d Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
0) (ValueCtor a -> ValueCtor a) -> ValueCtor a -> ValueCtor a
forall a b. (a -> b) -> a -> b
$
  case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
    Bitvector Bytes
sz -> Bool -> ValueCtor a -> ValueCtor a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
d Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sz) (ValueCtor a -> ValueCtor a) -> ValueCtor a -> ValueCtor a
forall a b. (a -> b) -> a -> b
$
      Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
d (Bytes -> StorageType -> ValueCtor a
subFn Bytes
0 (Bytes -> StorageType
bitvectorType Bytes
d))
               (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
d) (Bytes -> StorageType -> ValueCtor a
subFn Bytes
d (Bytes -> StorageType
bitvectorType (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
d)))
    StorageTypeF StorageType
Float -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToFloat (Bytes -> StorageType -> ValueCtor a
subFn Bytes
0 (Bytes -> StorageType
bitvectorType Bytes
4))
    StorageTypeF StorageType
Double -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToDouble (Bytes -> StorageType -> ValueCtor a
subFn Bytes
0 (Bytes -> StorageType
bitvectorType Bytes
8))
    StorageTypeF StorageType
X86_FP80 -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToX86_FP80 (Bytes -> StorageType -> ValueCtor a
subFn Bytes
0 (Bytes -> StorageType
bitvectorType Bytes
10))
    Array Natural
n0 StorageType
etp -> Bool -> ValueCtor a -> ValueCtor a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Natural
n0 Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
> Natural
0) (ValueCtor a -> ValueCtor a) -> ValueCtor a -> ValueCtor a
forall a b. (a -> b) -> a -> b
$ do
      let esz :: Bytes
esz = StorageType -> Bytes
storageTypeSize StorageType
etp
      let (Integer
c,Integer
part) = Bool -> (Integer, Integer) -> (Integer, Integer)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
esz Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
0) ((Integer, Integer) -> (Integer, Integer))
-> (Integer, Integer) -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
d Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
esz
      let n :: Integer
n = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n0 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer -> Integer
forall a. Integral a => a -> Integer
toInteger Integer
c
      let o :: Bytes
o = Bytes
d Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes Integer
part -- (Bytes c) * esz
      let consPartial :: ValueCtor a
consPartial
            | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = String -> [String] -> ValueCtor a
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"splitTypeValue" [String
"Unexpected array size: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n, StorageType -> String
forall a. Show a => a -> String
show StorageType
tp, Bytes -> String
forall a. Show a => a -> String
show Bytes
d]
            | Integer
part Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Bytes -> StorageType -> ValueCtor a
subFn Bytes
o (Natural -> StorageType -> StorageType
arrayType (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n) StorageType
etp)
            | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 =
                ValueCtor a -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a -> ValueCtor a
ConsArray (Bytes -> StorageType -> ValueCtor a
subFn Bytes
o StorageType
etp)
                          (Bytes -> StorageType -> ValueCtor a
subFn (Bytes
oBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
esz) (Natural -> StorageType -> StorageType
arrayType (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)) StorageType
etp))
            | Bool
otherwise = Bool -> ValueCtor a -> ValueCtor a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) (ValueCtor a -> ValueCtor a) -> ValueCtor a -> ValueCtor a
forall a b. (a -> b) -> a -> b
$
                StorageType -> ValueCtor a -> ValueCtor a
forall a. StorageType -> ValueCtor a -> ValueCtor a
singletonArray StorageType
etp (Bytes -> StorageType -> ValueCtor a
subFn Bytes
o StorageType
etp)
      let result :: ValueCtor a
result
            | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Bool -> ValueCtor a -> ValueCtor a
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n0) (ValueCtor a -> ValueCtor a) -> ValueCtor a -> ValueCtor a
forall a b. (a -> b) -> a -> b
$
              ValueCtor a -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a -> ValueCtor a
AppendArray (Bytes -> StorageType -> ValueCtor a
subFn Bytes
0 (Natural -> StorageType -> StorageType
arrayType (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
c) StorageType
etp))
                          ValueCtor a
consPartial
            | Bool
otherwise = ValueCtor a
consPartial
      ValueCtor a
result
    Struct Vector (Field StorageType)
flds -> Vector (Field StorageType, ValueCtor a) -> ValueCtor a
forall a. Vector (Field StorageType, ValueCtor a) -> ValueCtor a
MkStruct (Field StorageType -> (Field StorageType, ValueCtor a)
fldFn (Field StorageType -> (Field StorageType, ValueCtor a))
-> Vector (Field StorageType)
-> Vector (Field StorageType, ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Field StorageType)
flds)
      where fldFn :: Field StorageType -> (Field StorageType, ValueCtor a)
fldFn Field StorageType
fld = (Field StorageType
fld, Bytes -> StorageType -> ValueCtor a
subFn (Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldOffset Field StorageType
fld) (Field StorageType
fldField 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))

-- | This is used so that when we are comparing symbolic loads against
-- previous stores, we can represent the difference as relative to
-- a fixed address whenever possible.
data BasePreference
   = FixedLoad
   | FixedStore
   | NeitherFixed
  deriving (BasePreference -> BasePreference -> Bool
(BasePreference -> BasePreference -> Bool)
-> (BasePreference -> BasePreference -> Bool) -> Eq BasePreference
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BasePreference -> BasePreference -> Bool
== :: BasePreference -> BasePreference -> Bool
$c/= :: BasePreference -> BasePreference -> Bool
/= :: BasePreference -> BasePreference -> Bool
Eq, Int -> BasePreference -> ShowS
[BasePreference] -> ShowS
BasePreference -> String
(Int -> BasePreference -> ShowS)
-> (BasePreference -> String)
-> ([BasePreference] -> ShowS)
-> Show BasePreference
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BasePreference -> ShowS
showsPrec :: Int -> BasePreference -> ShowS
$cshow :: BasePreference -> String
show :: BasePreference -> String
$cshowList :: [BasePreference] -> ShowS
showList :: [BasePreference] -> ShowS
Show)

-- RangeLoad

-- | A 'RangeLoad' describes different kinds of memory loads in the
-- context of a byte range copied into an old memory.
data RangeLoad a b
  = OutOfRange a StorageType
    -- ^ Load from an address range disjoint from the copied bytes.
    -- The arguments represent the address and type of the load.
  | InRange b StorageType
    -- ^ Load consists of bytes within the copied range. The first
    -- argument represents the offset relative to the start of the
    -- copied bytes.
  deriving (Int -> RangeLoad a b -> ShowS
[RangeLoad a b] -> ShowS
RangeLoad a b -> String
(Int -> RangeLoad a b -> ShowS)
-> (RangeLoad a b -> String)
-> ([RangeLoad a b] -> ShowS)
-> Show (RangeLoad a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> RangeLoad a b -> ShowS
forall a b. (Show a, Show b) => [RangeLoad a b] -> ShowS
forall a b. (Show a, Show b) => RangeLoad a b -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> RangeLoad a b -> ShowS
showsPrec :: Int -> RangeLoad a b -> ShowS
$cshow :: forall a b. (Show a, Show b) => RangeLoad a b -> String
show :: RangeLoad a b -> String
$cshowList :: forall a b. (Show a, Show b) => [RangeLoad a b] -> ShowS
showList :: [RangeLoad a b] -> ShowS
Show)

adjustOffset :: (b -> d)
             -> (a -> c)
             -> RangeLoad a b -> RangeLoad c d
adjustOffset :: forall b d a c.
(b -> d) -> (a -> c) -> RangeLoad a b -> RangeLoad c d
adjustOffset b -> d
_ a -> c
outFn (OutOfRange a
a StorageType
tp) = c -> StorageType -> RangeLoad c d
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange (a -> c
outFn a
a) StorageType
tp
adjustOffset b -> d
inFn a -> c
_  (InRange b
b StorageType
tp) = d -> StorageType -> RangeLoad c d
forall a b. b -> StorageType -> RangeLoad a b
InRange (b -> d
inFn b
b) StorageType
tp

-- | Decomposes a single load after a memcopy into a combination of
-- simple value loads.
rangeLoad ::
  Addr  {- ^ load offset  -} ->
  StorageType {- ^ load type    -} ->
  Range {- ^ copied range -} ->
  ValueCtor (RangeLoad Addr Addr)
rangeLoad :: Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
lo StorageType
ltp s :: Range
s@(R Bytes
so Bytes
se)
   | Bytes
so Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
se  = ValueCtor (RangeLoad Bytes Bytes)
forall {b}. ValueCtor (RangeLoad Bytes b)
loadFail
   | Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
so  = ValueCtor (RangeLoad Bytes Bytes)
forall {b}. ValueCtor (RangeLoad Bytes b)
loadFail
   | Bytes
se Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
lo  = ValueCtor (RangeLoad Bytes Bytes)
forall {b}. ValueCtor (RangeLoad Bytes b)
loadFail
   | Bytes
lo Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
so   = StorageType
-> Bytes
-> (Bytes -> StorageType -> ValueCtor (RangeLoad Bytes Bytes))
-> ValueCtor (RangeLoad Bytes Bytes)
forall a.
StorageType
-> Bytes -> (Bytes -> StorageType -> ValueCtor a) -> ValueCtor a
splitTypeValue StorageType
ltp (Bytes
so Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
lo) (\Bytes
o StorageType
tp -> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
o) StorageType
tp Range
s)
   | Bytes
se Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
le   = StorageType
-> Bytes
-> (Bytes -> StorageType -> ValueCtor (RangeLoad Bytes Bytes))
-> ValueCtor (RangeLoad Bytes Bytes)
forall a.
StorageType
-> Bytes -> (Bytes -> StorageType -> ValueCtor a) -> ValueCtor a
splitTypeValue StorageType
ltp (Bytes
se Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
lo) (\Bytes
o StorageType
tp -> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
o) StorageType
tp Range
s)
   | Bool
otherwise = Bool
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad Bytes Bytes)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
so Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
lo Bool -> Bool -> Bool
&& Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
se) (ValueCtor (RangeLoad Bytes Bytes)
 -> ValueCtor (RangeLoad Bytes Bytes))
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad Bytes Bytes)
forall a b. (a -> b) -> a -> b
$ RangeLoad Bytes Bytes -> ValueCtor (RangeLoad Bytes Bytes)
forall a. a -> ValueCtor a
ValueCtorVar (Bytes -> StorageType -> RangeLoad Bytes Bytes
forall a b. b -> StorageType -> RangeLoad a b
InRange (Bytes
lo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
so) StorageType
ltp)
 where le :: Bytes
le = Bytes -> StorageType -> Bytes
typeEnd Bytes
lo StorageType
ltp
       loadFail :: ValueCtor (RangeLoad Bytes b)
loadFail = RangeLoad Bytes b -> ValueCtor (RangeLoad Bytes b)
forall a. a -> ValueCtor a
ValueCtorVar (Bytes -> StorageType -> RangeLoad Bytes b
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange Bytes
lo StorageType
ltp)

-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store offsets are concrete and the store size is bounded
fixedOffsetRangeLoad :: Addr
                     -- ^ Address of load
                     -> StorageType
                     -- ^ Type to load
                     -> Addr
                     -- ^ Address of store
                     -> Mux (ValueCtor (RangeLoad Addr Addr))
fixedOffsetRangeLoad :: Bytes
-> StorageType -> Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
fixedOffsetRangeLoad Bytes
l StorageType
tp Bytes
s
  | Bytes
s Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
l = do -- Store is before load.
    let sd :: Bytes
sd = Bytes
l Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
s -- Number of bytes load comes after store
    Cond
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntLe IntExpr
StoreSize (Bytes -> IntExpr
CValue Bytes
sd)) Mux (ValueCtor (RangeLoad Bytes Bytes))
forall {b}. Mux (ValueCtor (RangeLoad Bytes b))
loadFail (Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadCase (Bytes
sdBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
1))
  | Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
s = Mux (ValueCtor (RangeLoad Bytes Bytes))
forall {b}. Mux (ValueCtor (RangeLoad Bytes b))
loadFail -- No load if load ends before write.
  | Bool
otherwise = Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadCase Bytes
0
  where
    le :: Bytes
le = Bytes -> StorageType -> Bytes
typeEnd Bytes
l StorageType
tp
    loadCase :: Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadCase Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
leBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
s  = Cond
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntEq IntExpr
StoreSize (Bytes -> IntExpr
CValue Bytes
i)) (Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadVal Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadCase (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
1))
      | Bool
otherwise = Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadVal Bytes
i
    loadVal :: Bytes -> Mux (ValueCtor (RangeLoad Bytes Bytes))
loadVal Bytes
ssz = ValueCtor (RangeLoad Bytes Bytes)
-> Mux (ValueCtor (RangeLoad Bytes Bytes))
forall a. a -> Mux a
MuxVar (Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
l StorageType
tp (Bytes -> Bytes -> Range
R Bytes
s (Bytes
sBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
ssz)))
    loadFail :: Mux (ValueCtor (RangeLoad Bytes b))
loadFail = ValueCtor (RangeLoad Bytes b)
-> Mux (ValueCtor (RangeLoad Bytes b))
forall a. a -> Mux a
MuxVar (RangeLoad Bytes b -> ValueCtor (RangeLoad Bytes b)
forall a. a -> ValueCtor a
ValueCtorVar (Bytes -> StorageType -> RangeLoad Bytes b
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange Bytes
l StorageType
tp))

-- | @fixLoadBeforeStoreOffset pref i k@ adjusts a pointer value that is relative
-- the load address into a global pointer.  The code assumes that @load + i == store@.
fixLoadBeforeStoreOffset :: BasePreference -> Offset -> Offset -> OffsetExpr
fixLoadBeforeStoreOffset :: BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadBeforeStoreOffset BasePreference
pref Bytes
i Bytes
k
  | BasePreference
pref BasePreference -> BasePreference -> Bool
forall a. Eq a => a -> a -> Bool
== BasePreference
FixedStore = OffsetExpr
Store OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue (Bytes
k Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
i)
  | Bool
otherwise = OffsetExpr
Load OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue Bytes
k

-- | @fixLoadAfterStoreOffset pref i k@ adjusts a pointer value that is relative
-- the load address into a global pointer.  The code assumes that @load == store + i@.
fixLoadAfterStoreOffset :: BasePreference -> Offset -> Offset -> OffsetExpr
fixLoadAfterStoreOffset :: BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadAfterStoreOffset BasePreference
pref Bytes
i Bytes
k = Bool -> OffsetExpr -> OffsetExpr
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
k Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
>= Bytes
i) (OffsetExpr -> OffsetExpr) -> OffsetExpr -> OffsetExpr
forall a b. (a -> b) -> a -> b
$
  case BasePreference
pref of
    BasePreference
FixedStore -> OffsetExpr
Store OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue Bytes
k
    BasePreference
_          -> OffsetExpr
Load  OffsetExpr -> IntExpr -> OffsetExpr
.+ Bytes -> IntExpr
CValue (Bytes
k Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
i)

-- | @loadFromStoreStart pref tp i j@ loads a value of type @tp@ from a range under the
-- assumptions that @load + i == store@ and @j = i + min(StoreSize, typeEnd(tp)@.
loadFromStoreStart :: BasePreference
                   -> StorageType
                   -> Offset
                   -> Offset
                   -> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart :: BasePreference
-> StorageType
-> Bytes
-> Bytes
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart BasePreference
pref StorageType
tp Bytes
i Bytes
j = (Bytes -> IntExpr)
-> (Bytes -> OffsetExpr)
-> RangeLoad Bytes Bytes
-> RangeLoad OffsetExpr IntExpr
forall b d a c.
(b -> d) -> (a -> c) -> RangeLoad a b -> RangeLoad c d
adjustOffset Bytes -> IntExpr
inFn Bytes -> OffsetExpr
outFn (RangeLoad Bytes Bytes -> RangeLoad OffsetExpr IntExpr)
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
0 StorageType
tp (Bytes -> Bytes -> Range
R Bytes
i Bytes
j)
  where inFn :: Bytes -> IntExpr
inFn = Bytes -> IntExpr
CValue
        outFn :: Bytes -> OffsetExpr
outFn = BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadBeforeStoreOffset BasePreference
pref Bytes
i

-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store values are concrete
fixedSizeRangeLoad :: BasePreference -- ^ Whether addresses are based on store or load.
                   -> StorageType
                   -> Bytes
                   -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
fixedSizeRangeLoad :: BasePreference
-> StorageType
-> Bytes
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
fixedSizeRangeLoad BasePreference
_ StorageType
tp Bytes
0 = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (RangeLoad OffsetExpr IntExpr
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
forall a. a -> ValueCtor a
ValueCtorVar (OffsetExpr -> StorageType -> RangeLoad OffsetExpr IntExpr
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange OffsetExpr
Load StorageType
tp))
fixedSizeRangeLoad BasePreference
pref StorageType
tp Bytes
ssz =
  Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
lsz OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Store) Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
prefixL Bytes
lsz)
  where
    lsz :: Bytes
lsz = Bytes -> StorageType -> Bytes
typeEnd Bytes
0 StorageType
tp

    prefixL :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
prefixL Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
0 = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
i OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
Store) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
prefixL (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
      -- Special case where we skip some offsets, it it won't
      -- make more splitting
      | Bytes
lsz Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
ssz Bool -> Bool -> Bool
&& BasePreference
pref BasePreference -> BasePreference -> Bool
forall a. Eq a => a -> a -> Bool
== BasePreference
NeitherFixed =
        -- Load is contained in storage.
        Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> Cond
loadInStoreRange (Bytes
sszBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
lsz)) Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {a}. Mux (ValueCtor (RangeLoad a IntExpr))
loadSucc (Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
 -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr)))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a b. (a -> b) -> a -> b
$
        -- Load extends past end of storage
        Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
suffixS (Bytes
sszBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
lsz)
      | Bool
otherwise = Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
suffixS Bytes
0

    suffixS :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
suffixS Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
ssz   = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (OffsetExpr
Load OffsetExpr -> OffsetExpr -> Cond
.== Bytes -> OffsetExpr
storeOffset Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeVal Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
suffixS (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
1))
      | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadVal :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (BasePreference
-> StorageType
-> Bytes
-> Bytes
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart BasePreference
pref StorageType
tp Bytes
i (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
ssz))

    storeVal :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeVal Bytes
i = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar ((Bytes -> IntExpr)
-> (Bytes -> OffsetExpr)
-> RangeLoad Bytes Bytes
-> RangeLoad OffsetExpr IntExpr
forall b d a c.
(b -> d) -> (a -> c) -> RangeLoad a b -> RangeLoad c d
adjustOffset Bytes -> IntExpr
inFn Bytes -> OffsetExpr
outFn (RangeLoad Bytes Bytes -> RangeLoad OffsetExpr IntExpr)
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
i StorageType
tp (Bytes -> Bytes -> Range
R Bytes
0 Bytes
ssz))
      where inFn :: Bytes -> IntExpr
inFn = Bytes -> IntExpr
CValue
            outFn :: Bytes -> OffsetExpr
outFn = BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadAfterStoreOffset BasePreference
pref Bytes
i

    loadSucc :: Mux (ValueCtor (RangeLoad a IntExpr))
loadSucc = ValueCtor (RangeLoad a IntExpr)
-> Mux (ValueCtor (RangeLoad a IntExpr))
forall a. a -> Mux a
MuxVar (RangeLoad a IntExpr -> ValueCtor (RangeLoad a IntExpr)
forall a. a -> ValueCtor a
ValueCtorVar (IntExpr -> StorageType -> RangeLoad a IntExpr
forall a b. b -> StorageType -> RangeLoad a b
InRange (OffsetExpr
Load OffsetExpr -> OffsetExpr -> IntExpr
.- OffsetExpr
Store) StorageType
tp))
    loadFail :: Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail = ValueCtor (RangeLoad OffsetExpr b)
-> Mux (ValueCtor (RangeLoad OffsetExpr b))
forall a. a -> Mux a
MuxVar (RangeLoad OffsetExpr b -> ValueCtor (RangeLoad OffsetExpr b)
forall a. a -> ValueCtor a
ValueCtorVar (OffsetExpr -> StorageType -> RangeLoad OffsetExpr b
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange OffsetExpr
Load StorageType
tp))

-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store values are symbolic and the @StoreSize@ is bounded.
symbolicRangeLoad :: BasePreference -> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicRangeLoad :: BasePreference
-> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicRangeLoad BasePreference
pref StorageType
tp =
  Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (OffsetExpr
Store OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Load)
  (Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
sz OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
storeEnd) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal0 Bytes
sz) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadIter0 (Bytes
szBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1)))
  (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad Bytes
1)
  where
    sz :: Bytes
sz = Bytes -> StorageType -> Bytes
typeEnd Bytes
0 StorageType
tp

    loadIter0 :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadIter0 Bytes
j
      | Bytes
j Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
0     = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
j OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
storeEnd) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal0 Bytes
j) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadIter0 (Bytes
jBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
      | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadVal0 :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal0 Bytes
j = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (ValueCtor (RangeLoad OffsetExpr IntExpr)
 -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr)))
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a b. (a -> b) -> a -> b
$ (Bytes -> IntExpr)
-> (Bytes -> OffsetExpr)
-> RangeLoad Bytes Bytes
-> RangeLoad OffsetExpr IntExpr
forall b d a c.
(b -> d) -> (a -> c) -> RangeLoad a b -> RangeLoad c d
adjustOffset Bytes -> IntExpr
inFn Bytes -> OffsetExpr
outFn (RangeLoad Bytes Bytes -> RangeLoad OffsetExpr IntExpr)
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
0 StorageType
tp (Bytes -> Bytes -> Range
R Bytes
0 Bytes
j)
      where inFn :: Bytes -> IntExpr
inFn Bytes
k  = IntExpr -> IntExpr -> IntExpr
IntAdd (OffsetExpr -> OffsetExpr -> IntExpr
OffsetDiff OffsetExpr
Load OffsetExpr
Store) (Bytes -> IntExpr
CValue Bytes
k)
            outFn :: Bytes -> OffsetExpr
outFn Bytes
k = OffsetExpr -> IntExpr -> OffsetExpr
OffsetAdd OffsetExpr
Load (Bytes -> IntExpr
CValue Bytes
k)

    storeAfterLoad :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sz = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
i OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
Store) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadFromOffset Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
1))
      | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadFromOffset :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadFromOffset Bytes
i =
      Bool
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
0 Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
i Bool -> Bool -> Bool
&& Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sz) (Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
 -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr)))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a b. (a -> b) -> a -> b
$
      Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntLe (Bytes -> IntExpr
CValue (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
i)) IntExpr
StoreSize) (Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
sz)) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f (Bytes
szBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
      where f :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f Bytes
j | Bytes
j Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
i = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntEq (Bytes -> IntExpr
CValue (Bytes
jBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
i)) IntExpr
StoreSize) (Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i Bytes
j) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f (Bytes
jBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
                | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadVal :: Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i Bytes
j = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (BasePreference
-> StorageType
-> Bytes
-> Bytes
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart BasePreference
pref StorageType
tp Bytes
i Bytes
j)
    loadFail :: Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail = ValueCtor (RangeLoad OffsetExpr b)
-> Mux (ValueCtor (RangeLoad OffsetExpr b))
forall a. a -> Mux a
MuxVar (RangeLoad OffsetExpr b -> ValueCtor (RangeLoad OffsetExpr b)
forall a. a -> ValueCtor a
ValueCtorVar (OffsetExpr -> StorageType -> RangeLoad OffsetExpr b
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange OffsetExpr
Load StorageType
tp))

-- | Produces a @Mux ValueCtor@ expression representing the RangeLoad conditions
-- when the load and store values are symbolic and the @StoreSize@ is unbounded.
symbolicUnboundedRangeLoad :: BasePreference -> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicUnboundedRangeLoad :: BasePreference
-> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicUnboundedRangeLoad BasePreference
pref StorageType
tp =
  Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (OffsetExpr
Store OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Load)
  (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal0 Bytes
sz)
  (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad Bytes
1)
  where
    sz :: Bytes
sz = Bytes -> StorageType -> Bytes
typeEnd Bytes
0 StorageType
tp

    loadVal0 :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal0 Bytes
j = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (ValueCtor (RangeLoad OffsetExpr IntExpr)
 -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr)))
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a b. (a -> b) -> a -> b
$ (Bytes -> IntExpr)
-> (Bytes -> OffsetExpr)
-> RangeLoad Bytes Bytes
-> RangeLoad OffsetExpr IntExpr
forall b d a c.
(b -> d) -> (a -> c) -> RangeLoad a b -> RangeLoad c d
adjustOffset Bytes -> IntExpr
inFn Bytes -> OffsetExpr
outFn (RangeLoad Bytes Bytes -> RangeLoad OffsetExpr IntExpr)
-> ValueCtor (RangeLoad Bytes Bytes)
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> Range -> ValueCtor (RangeLoad Bytes Bytes)
rangeLoad Bytes
0 StorageType
tp (Bytes -> Bytes -> Range
R Bytes
0 Bytes
j)
      where inFn :: Bytes -> IntExpr
inFn Bytes
k  = IntExpr -> IntExpr -> IntExpr
IntAdd (OffsetExpr -> OffsetExpr -> IntExpr
OffsetDiff OffsetExpr
Load OffsetExpr
Store) (Bytes -> IntExpr
CValue Bytes
k)
            outFn :: Bytes -> OffsetExpr
outFn Bytes
k = OffsetExpr -> IntExpr -> OffsetExpr
OffsetAdd OffsetExpr
Load (Bytes -> IntExpr
CValue Bytes
k)

    storeAfterLoad :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sz = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Bytes -> OffsetExpr
loadOffset Bytes
i OffsetExpr -> OffsetExpr -> Cond
.== OffsetExpr
Store) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadFromOffset Bytes
i) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
storeAfterLoad (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
1))
      | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadFromOffset :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadFromOffset Bytes
i =
      Bool
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
0 Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
i Bool -> Bool -> Bool
&& Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sz) (Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
 -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr)))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a b. (a -> b) -> a -> b
$
      Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntLe (Bytes -> IntExpr
CValue (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
i)) IntExpr
StoreSize) (Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i (Bytes
iBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
sz)) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f (Bytes
szBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
      where f :: Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f Bytes
j | Bytes
j Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
i = Cond
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (IntExpr -> IntExpr -> Cond
IntEq (Bytes -> IntExpr
CValue (Bytes
jBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
i)) IntExpr
StoreSize) (Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i Bytes
j) (Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
f (Bytes
jBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
-Bytes
1))
                | Bool
otherwise = Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall {b}. Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail

    loadVal :: Bytes -> Bytes -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
loadVal Bytes
i Bytes
j = ValueCtor (RangeLoad OffsetExpr IntExpr)
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
forall a. a -> Mux a
MuxVar (BasePreference
-> StorageType
-> Bytes
-> Bytes
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart BasePreference
pref StorageType
tp Bytes
i Bytes
j)
    loadFail :: Mux (ValueCtor (RangeLoad OffsetExpr b))
loadFail = ValueCtor (RangeLoad OffsetExpr b)
-> Mux (ValueCtor (RangeLoad OffsetExpr b))
forall a. a -> Mux a
MuxVar (RangeLoad OffsetExpr b -> ValueCtor (RangeLoad OffsetExpr b)
forall a. a -> ValueCtor a
ValueCtorVar (OffsetExpr -> StorageType -> RangeLoad OffsetExpr b
forall a b. a -> StorageType -> RangeLoad a b
OutOfRange OffsetExpr
Load StorageType
tp))

-- ValueView

-- | Represents a projection of a sub-component out of a larger LLVM value.
data ValueView
  = ValueViewVar StorageType
    -- | Select low-address bytes in the bitvector.
    -- The sizes include the number of low bytes, and the number of high bytes.
  | SelectPrefixBV Bytes Bytes ValueView
    -- | Select the given number of high-address bytes in the bitvector.
    -- The sizes include the number of low bytes, and the number of high bytes.
  | SelectSuffixBV Bytes Bytes ValueView
  | FloatToBV ValueView
  | DoubleToBV ValueView
  | X86_FP80ToBV ValueView
  | ArrayElt Natural StorageType Natural ValueView

  | FieldVal (Vector (Field StorageType)) Int ValueView
  deriving (Int -> ValueView -> ShowS
[ValueView] -> ShowS
ValueView -> String
(Int -> ValueView -> ShowS)
-> (ValueView -> String)
-> ([ValueView] -> ShowS)
-> Show ValueView
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ValueView -> ShowS
showsPrec :: Int -> ValueView -> ShowS
$cshow :: ValueView -> String
show :: ValueView -> String
$cshowList :: [ValueView] -> ShowS
showList :: [ValueView] -> ShowS
Show, ValueView -> ValueView -> Bool
(ValueView -> ValueView -> Bool)
-> (ValueView -> ValueView -> Bool) -> Eq ValueView
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ValueView -> ValueView -> Bool
== :: ValueView -> ValueView -> Bool
$c/= :: ValueView -> ValueView -> Bool
/= :: ValueView -> ValueView -> Bool
Eq, Eq ValueView
Eq ValueView =>
(ValueView -> ValueView -> Ordering)
-> (ValueView -> ValueView -> Bool)
-> (ValueView -> ValueView -> Bool)
-> (ValueView -> ValueView -> Bool)
-> (ValueView -> ValueView -> Bool)
-> (ValueView -> ValueView -> ValueView)
-> (ValueView -> ValueView -> ValueView)
-> Ord ValueView
ValueView -> ValueView -> Bool
ValueView -> ValueView -> Ordering
ValueView -> ValueView -> ValueView
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 :: ValueView -> ValueView -> Ordering
compare :: ValueView -> ValueView -> Ordering
$c< :: ValueView -> ValueView -> Bool
< :: ValueView -> ValueView -> Bool
$c<= :: ValueView -> ValueView -> Bool
<= :: ValueView -> ValueView -> Bool
$c> :: ValueView -> ValueView -> Bool
> :: ValueView -> ValueView -> Bool
$c>= :: ValueView -> ValueView -> Bool
>= :: ValueView -> ValueView -> Bool
$cmax :: ValueView -> ValueView -> ValueView
max :: ValueView -> ValueView -> ValueView
$cmin :: ValueView -> ValueView -> ValueView
min :: ValueView -> ValueView -> ValueView
Ord)

viewType :: ValueView -> Maybe StorageType
viewType :: ValueView -> Maybe StorageType
viewType (ValueViewVar StorageType
tp) = StorageType -> Maybe StorageType
forall a. a -> Maybe a
Just StorageType
tp
viewType (SelectPrefixBV Bytes
u Bytes
v ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bytes -> StorageTypeF StorageType
forall v. Bytes -> StorageTypeF v
Bitvector (Bytes
u Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
v) StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType
bitvectorType Bytes
u
viewType (SelectSuffixBV Bytes
u Bytes
v ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Bytes -> StorageTypeF StorageType
forall v. Bytes -> StorageTypeF v
Bitvector (Bytes
u Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
v) StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType
bitvectorType Bytes
v
viewType (FloatToBV ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (StorageTypeF StorageType
forall v. StorageTypeF v
Float StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType
bitvectorType Bytes
4
viewType (DoubleToBV ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (StorageTypeF StorageType
forall v. StorageTypeF v
Double StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType
bitvectorType Bytes
8
viewType (X86_FP80ToBV ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (StorageTypeF StorageType
forall v. StorageTypeF v
X86_FP80 StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ Bytes -> StorageType
bitvectorType Bytes
10
viewType (ArrayElt Natural
n StorageType
etp Natural
i ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
n Bool -> Bool -> Bool
&& Natural -> StorageType -> StorageTypeF StorageType
forall v. Natural -> v -> StorageTypeF v
Array Natural
n StorageType
etp StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     StorageType -> Maybe StorageType
forall a. a -> Maybe a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StorageType -> Maybe StorageType)
-> StorageType -> Maybe StorageType
forall a b. (a -> b) -> a -> b
$ StorageType
etp
viewType (FieldVal Vector (Field StorageType)
v Int
i ValueView
vv) =
  do StorageTypeF StorageType
tp <- StorageType -> StorageTypeF StorageType
storageTypeF (StorageType -> StorageTypeF StorageType)
-> Maybe StorageType -> Maybe (StorageTypeF StorageType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ValueView -> Maybe StorageType
viewType ValueView
vv
     Bool -> Maybe ()
forall (f :: Type -> Type). Alternative f => Bool -> f ()
guard (Vector (Field StorageType) -> StorageTypeF StorageType
forall v. Vector (Field v) -> StorageTypeF v
Struct Vector (Field StorageType)
v StorageTypeF StorageType -> StorageTypeF StorageType -> Bool
forall a. Eq a => a -> a -> Bool
== StorageTypeF StorageType
tp)
     Getting StorageType (Field StorageType) StorageType
-> Field StorageType -> StorageType
forall s (m :: Type -> Type) a.
MonadReader s m =>
Getting a s a -> m a
view Getting StorageType (Field StorageType) StorageType
forall a b (f :: Type -> Type).
Functor f =>
(a -> f b) -> Field a -> f (Field b)
fieldVal (Field StorageType -> StorageType)
-> Maybe (Field StorageType) -> Maybe StorageType
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Vector (Field StorageType)
v Vector (Field StorageType) -> Int -> Maybe (Field StorageType)
forall a. Vector a -> Int -> Maybe a
V.!? Int
i)

-- | A 'ValueLoad' describes different kinds of memory loads in the
-- context of a new value stored into an old memory.
data ValueLoad v
  = OldMemory v StorageType
    -- ^ Load from an address range disjoint from the stored value.
    -- The arguments represent the address and type of the load.
  | LastStore ValueView
    -- ^ Load consists of valid bytes within the stored value.
  | InvalidMemory StorageType
    -- ^ Load touches invalid memory. Currently, this can only arise when
    -- trying to read struct padding bytes as a bitvector.
  deriving ((forall a b. (a -> b) -> ValueLoad a -> ValueLoad b)
-> (forall a b. a -> ValueLoad b -> ValueLoad a)
-> Functor ValueLoad
forall a b. a -> ValueLoad b -> ValueLoad a
forall a b. (a -> b) -> ValueLoad a -> ValueLoad 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) -> ValueLoad a -> ValueLoad b
fmap :: forall a b. (a -> b) -> ValueLoad a -> ValueLoad b
$c<$ :: forall a b. a -> ValueLoad b -> ValueLoad a
<$ :: forall a b. a -> ValueLoad b -> ValueLoad a
Functor,Int -> ValueLoad v -> ShowS
[ValueLoad v] -> ShowS
ValueLoad v -> String
(Int -> ValueLoad v -> ShowS)
-> (ValueLoad v -> String)
-> ([ValueLoad v] -> ShowS)
-> Show (ValueLoad v)
forall v. Show v => Int -> ValueLoad v -> ShowS
forall v. Show v => [ValueLoad v] -> ShowS
forall v. Show v => ValueLoad v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> ValueLoad v -> ShowS
showsPrec :: Int -> ValueLoad v -> ShowS
$cshow :: forall v. Show v => ValueLoad v -> String
show :: ValueLoad v -> String
$cshowList :: forall v. Show v => [ValueLoad v] -> ShowS
showList :: [ValueLoad v] -> ShowS
Show)

loadBitvector :: Addr -> Bytes -> Addr -> ValueView -> ValueCtor (ValueLoad Addr)
loadBitvector :: Bytes -> Bytes -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
loadBitvector Bytes
lo Bytes
lw Bytes
so ValueView
v = do
  let le :: Bytes
le = Bytes
lo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
lw
  let ltp :: StorageType
ltp = Bytes -> StorageType
bitvectorType Bytes
lw
  let stp :: StorageType
stp = StorageType -> Maybe StorageType -> StorageType
forall a. a -> Maybe a -> a
fromMaybe (String -> StorageType
forall a. (?callStack::CallStack) => String -> a
error (String
"loadBitvector given bad view " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueView -> String
forall a. Show a => a -> String
show ValueView
v)) (ValueView -> Maybe StorageType
viewType ValueView
v)
  let retValue :: Bytes -> ValueView -> (Bytes, ValueCtor (ValueLoad Bytes))
retValue Bytes
eo ValueView
v' = (Bytes
sz', Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo' (Bytes -> StorageType
bitvectorType Bytes
sz') Bytes
eo ValueView
v')
        where etp :: StorageType
etp = StorageType -> Maybe StorageType -> StorageType
forall a. a -> Maybe a -> a
fromMaybe (String -> StorageType
forall a. (?callStack::CallStack) => String -> a
error (String
"Bad view " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueView -> String
forall a. Show a => a -> String
show ValueView
v')) (ValueView -> Maybe StorageType
viewType ValueView
v')
              esz :: Bytes
esz = StorageType -> Bytes
storageTypeSize StorageType
etp
              lo' :: Bytes
lo' = Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
max Bytes
lo Bytes
eo
              sz' :: Bytes
sz' = Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
min Bytes
le (Bytes
eoBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
esz) Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
lo'
  case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
stp of
    Bitvector Bytes
sw
      | Bytes
so Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
lo -> do
        -- Number of bytes to drop.
        let d :: Bytes
d = Bytes
lo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
so
        -- Store is before load.
        Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
lo (Bytes -> Bytes -> ValueView -> ValueView
SelectSuffixBV Bytes
d (Bytes
sw Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
d) ValueView
v)
      | Bool
otherwise -> Bool -> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
lo Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
so Bool -> Bool -> Bool
&& Bytes
lw Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
sw) (ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$
        -- Load ends before store ends.
        Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
so (Bytes -> Bytes -> ValueView -> ValueView
SelectPrefixBV Bytes
lw (Bytes
sw Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
lw) ValueView
v)
    StorageTypeF StorageType
Float -> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
so (ValueView -> ValueView
FloatToBV ValueView
v)
    StorageTypeF StorageType
Double -> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
so (ValueView -> ValueView
DoubleToBV ValueView
v)
    StorageTypeF StorageType
X86_FP80 -> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
so (ValueView -> ValueView
X86_FP80ToBV ValueView
v)
    Array Natural
n StorageType
tp -> (Bytes, ValueCtor (ValueLoad Bytes)) -> ValueCtor (ValueLoad Bytes)
forall a b. (a, b) -> b
snd ((Bytes, ValueCtor (ValueLoad Bytes))
 -> ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ ((Bytes, ValueCtor (ValueLoad Bytes))
 -> (Bytes, ValueCtor (ValueLoad Bytes))
 -> (Bytes, ValueCtor (ValueLoad Bytes)))
-> [(Bytes, ValueCtor (ValueLoad Bytes))]
-> (Bytes, ValueCtor (ValueLoad Bytes))
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 (Bytes, ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
forall {a}.
(Bytes, ValueCtor a)
-> (Bytes, ValueCtor a) -> (Bytes, ValueCtor a)
cv (Integer -> (Bytes, ValueCtor (ValueLoad Bytes))
val (Integer -> (Bytes, ValueCtor (ValueLoad Bytes)))
-> [Integer] -> [(Bytes, ValueCtor (ValueLoad Bytes))]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer]
r)
      where cv :: (Bytes, ValueCtor a)
-> (Bytes, ValueCtor a) -> (Bytes, ValueCtor a)
cv (Bytes
wx,ValueCtor a
x) (Bytes
wy,ValueCtor a
y) = (Bytes
wx Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
wy, Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
wx ValueCtor a
x Bytes
wy ValueCtor a
y)
            esz :: Bytes
esz = StorageType -> Bytes
storageTypeSize StorageType
tp
            c0 :: Integer
c0 = Bool -> Integer -> Integer
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bytes
esz Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
> Bytes
0) (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger (Bytes
lo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
so) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
esz
            (Integer
c1, Integer
p1) = Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger (Bytes
le Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
so) Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
`divMod` Bytes -> Integer
forall a. Integral a => a -> Integer
toInteger Bytes
esz
            -- Get range of indices to read.
            r :: [Integer]
r | Integer
p1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Bool -> [Integer] -> [Integer]
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
c1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
c0) [Integer
c0..Integer
c1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1]
              | Bool
otherwise = Bool -> [Integer] -> [Integer]
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Integer
c1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
c0) [Integer
c0..Integer
c1]
            val :: Integer -> (Bytes, ValueCtor (ValueLoad Bytes))
val Integer
i
              | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Bytes -> ValueView -> (Bytes, ValueCtor (ValueLoad Bytes))
retValue (Bytes
so Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Natural -> Bytes -> Bytes
natBytesMul (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i) Bytes
esz) (Natural -> StorageType -> Natural -> ValueView -> ValueView
ArrayElt Natural
n StorageType
tp (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i) ValueView
v)
              | Bool
otherwise = String -> [String] -> (Bytes, ValueCtor (ValueLoad Bytes))
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"loadBitvector" [String
"Bad array index", Integer -> String
forall a. Show a => a -> String
show Integer
i, (Bytes, Bytes, Bytes, ValueView) -> String
forall a. Show a => a -> String
show (Bytes
lo, Bytes
lw, Bytes
so, ValueView
v)]
    Struct Vector (Field StorageType)
sflds -> Bool -> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Bool -> Bool
not ([(Bytes, ValueCtor (ValueLoad Bytes))] -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [(Bytes, ValueCtor (ValueLoad Bytes))]
r)) (ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ (Bytes, ValueCtor (ValueLoad Bytes)) -> ValueCtor (ValueLoad Bytes)
forall a b. (a, b) -> b
snd ((Bytes, ValueCtor (ValueLoad Bytes))
 -> ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ ((Bytes, ValueCtor (ValueLoad Bytes))
 -> (Bytes, ValueCtor (ValueLoad Bytes))
 -> (Bytes, ValueCtor (ValueLoad Bytes)))
-> [(Bytes, ValueCtor (ValueLoad Bytes))]
-> (Bytes, ValueCtor (ValueLoad Bytes))
forall a. (a -> a -> a) -> [a] -> a
forall (t :: Type -> Type) a.
Foldable t =>
(a -> a -> a) -> t a -> a
foldl1 (Bytes, ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
-> (Bytes, ValueCtor (ValueLoad Bytes))
forall {a}.
(Bytes, ValueCtor a)
-> (Bytes, ValueCtor a) -> (Bytes, ValueCtor a)
cv [(Bytes, ValueCtor (ValueLoad Bytes))]
r
      where cv :: (Bytes, ValueCtor a)
-> (Bytes, ValueCtor a) -> (Bytes, ValueCtor a)
cv (Bytes
wx,ValueCtor a
x) (Bytes
wy,ValueCtor a
y) = (Bytes
wxBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
wy, Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
wx ValueCtor a
x Bytes
wy ValueCtor a
y)
            r :: [(Bytes, ValueCtor (ValueLoad Bytes))]
r = [[(Bytes, ValueCtor (ValueLoad Bytes))]]
-> [(Bytes, ValueCtor (ValueLoad Bytes))]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat ((Int
 -> Field StorageType -> [(Bytes, ValueCtor (ValueLoad Bytes))])
-> [Int]
-> [Field StorageType]
-> [[(Bytes, ValueCtor (ValueLoad Bytes))]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Field StorageType -> [(Bytes, ValueCtor (ValueLoad Bytes))]
val [Int
0..] (Vector (Field StorageType) -> [Field StorageType]
forall a. Vector a -> [a]
V.toList Vector (Field StorageType)
sflds))
            val :: Int -> Field StorageType -> [(Bytes, ValueCtor (ValueLoad Bytes))]
val Int
i Field StorageType
f = [(Bytes, ValueCtor (ValueLoad Bytes))]
v1
              where eo :: Bytes
eo = Bytes
so Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldOffset Field StorageType
f
                    ee :: Bytes
ee = Bytes
eo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ StorageType -> Bytes
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)
                    v1 :: [(Bytes, ValueCtor (ValueLoad Bytes))]
v1 | Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
eo = [(Bytes, ValueCtor (ValueLoad Bytes))]
forall {v}. [(Bytes, ValueCtor (ValueLoad v))]
v2
                       | Bytes
ee Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
lo = [(Bytes, ValueCtor (ValueLoad Bytes))]
forall {v}. [(Bytes, ValueCtor (ValueLoad v))]
v2
                       | Bool
otherwise = Bytes -> ValueView -> (Bytes, ValueCtor (ValueLoad Bytes))
retValue Bytes
eo (Vector (Field StorageType) -> Int -> ValueView -> ValueView
FieldVal Vector (Field StorageType)
sflds Int
i ValueView
v) (Bytes, ValueCtor (ValueLoad Bytes))
-> [(Bytes, ValueCtor (ValueLoad Bytes))]
-> [(Bytes, ValueCtor (ValueLoad Bytes))]
forall a. a -> [a] -> [a]
: [(Bytes, ValueCtor (ValueLoad Bytes))]
forall {v}. [(Bytes, ValueCtor (ValueLoad v))]
v2
                    v2 :: [(Bytes, ValueCtor (ValueLoad v))]
v2 | Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldPad Field StorageType
f Bytes -> Bytes -> Bool
forall a. Eq a => a -> a -> Bool
== Bytes
0 = []   -- Return no padding.
                       | Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
ee = [] -- Nothing of load ends before padding.
                         -- Nothing if padding ends before load begins.
                       | Bytes
eeBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldPad Field StorageType
f Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
lo = []
                       | Bool
otherwise = [(Bytes
p, ValueLoad v -> ValueCtor (ValueLoad v)
forall a. a -> ValueCtor a
ValueCtorVar ValueLoad v
forall {v}. ValueLoad v
badMem)]
                      where p :: Bytes
p = Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
min (Bytes
eeBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldPad Field StorageType
f) Bytes
le Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- (Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
max Bytes
lo Bytes
ee)
                            tpPad :: StorageType
tpPad  = Bytes -> StorageType
bitvectorType Bytes
p
                            badMem :: ValueLoad v
badMem = StorageType -> ValueLoad v
forall v. StorageType -> ValueLoad v
InvalidMemory StorageType
tpPad

-- | Decomposes a single load after a store into a combination of
-- simple value loads.
valueLoad ::
  Addr      {- ^ load address         -} ->
  StorageType      {- ^ load type            -} ->
  Addr      {- ^ store address        -} ->
  ValueView {- ^ view of stored value -} ->
  ValueCtor (ValueLoad Addr)
valueLoad :: Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo StorageType
ltp Bytes
so ValueView
v
  | Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
so = ValueLoad Bytes -> ValueCtor (ValueLoad Bytes)
forall a. a -> ValueCtor a
ValueCtorVar (Bytes -> StorageType -> ValueLoad Bytes
forall v. v -> StorageType -> ValueLoad v
OldMemory Bytes
lo StorageType
ltp) -- Load ends before store
  | Bytes
se Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
lo = ValueLoad Bytes -> ValueCtor (ValueLoad Bytes)
forall a. a -> ValueCtor a
ValueCtorVar (Bytes -> StorageType -> ValueLoad Bytes
forall v. v -> StorageType -> ValueLoad v
OldMemory Bytes
lo StorageType
ltp) -- Store ends before load
    -- Load is before store.
  | Bytes
lo Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
so  = StorageType
-> Bytes
-> (Bytes -> StorageType -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a.
StorageType
-> Bytes -> (Bytes -> StorageType -> ValueCtor a) -> ValueCtor a
splitTypeValue StorageType
ltp (Bytes
so Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
lo) (\Bytes
o StorageType
tp -> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
o) StorageType
tp Bytes
so ValueView
v)
    -- Load ends after store ends.
  | Bytes
se Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
le  = StorageType
-> Bytes
-> (Bytes -> StorageType -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a.
StorageType
-> Bytes -> (Bytes -> StorageType -> ValueCtor a) -> ValueCtor a
splitTypeValue StorageType
ltp (Bytes
le Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
se) (\Bytes
o StorageType
tp -> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
o) StorageType
tp Bytes
so ValueView
v)
  | (Bytes
lo,StorageType
ltp) (Bytes, StorageType) -> (Bytes, StorageType) -> Bool
forall a. Eq a => a -> a -> Bool
== (Bytes
so,StorageType
stp) = ValueLoad Bytes -> ValueCtor (ValueLoad Bytes)
forall a. a -> ValueCtor a
ValueCtorVar (ValueView -> ValueLoad Bytes
forall v. ValueView -> ValueLoad v
LastStore ValueView
v)
  | Bool
otherwise =
    case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
ltp of
      Bitvector Bytes
lw -> Bytes -> Bytes -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
loadBitvector Bytes
lo Bytes
lw Bytes
so ValueView
v
      StorageTypeF StorageType
Float  -> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a. ValueCtor a -> ValueCtor a
BVToFloat  (ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo (Bytes -> StorageType
bitvectorType Bytes
4) Bytes
so ValueView
v
      StorageTypeF StorageType
Double -> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a. ValueCtor a -> ValueCtor a
BVToDouble (ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo (Bytes -> StorageType
bitvectorType Bytes
8) Bytes
so ValueView
v
      StorageTypeF StorageType
X86_FP80 -> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a. ValueCtor a -> ValueCtor a
BVToX86_FP80 (ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad Bytes)
forall a b. (a -> b) -> a -> b
$ Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
lo (Bytes -> StorageType
bitvectorType Bytes
10) Bytes
so ValueView
v
      Array Natural
ln StorageType
tp ->
        let leSize :: Bytes
leSize = StorageType -> Bytes
storageTypeSize StorageType
tp
            val :: a -> ValueCtor (ValueLoad Bytes)
val a
i = Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Bytes
leSizeBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
*a -> Bytes
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
i) StorageType
tp Bytes
so ValueView
v
         in StorageType
-> Vector (ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a. StorageType -> Vector (ValueCtor a) -> ValueCtor a
MkArray StorageType
tp (Int
-> (Int -> ValueCtor (ValueLoad Bytes))
-> Vector (ValueCtor (ValueLoad Bytes))
forall a. Int -> (Int -> a) -> Vector a
V.generate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
ln) Int -> ValueCtor (ValueLoad Bytes)
forall {a}. Integral a => a -> ValueCtor (ValueLoad Bytes)
val)
      Struct Vector (Field StorageType)
lflds ->
        let val :: Field StorageType
-> (Field StorageType, ValueCtor (ValueLoad Bytes))
val Field StorageType
f = (Field StorageType
f, Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad (Bytes
loBytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+Field StorageType -> Bytes
forall v. Field v -> Bytes
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) Bytes
so ValueView
v)
         in Vector (Field StorageType, ValueCtor (ValueLoad Bytes))
-> ValueCtor (ValueLoad Bytes)
forall a. Vector (Field StorageType, ValueCtor a) -> ValueCtor a
MkStruct (Field StorageType
-> (Field StorageType, ValueCtor (ValueLoad Bytes))
val (Field StorageType
 -> (Field StorageType, ValueCtor (ValueLoad Bytes)))
-> Vector (Field StorageType)
-> Vector (Field StorageType, ValueCtor (ValueLoad Bytes))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Field StorageType)
lflds)
 where stp :: StorageType
stp = StorageType -> Maybe StorageType -> StorageType
forall a. a -> Maybe a -> a
fromMaybe (String -> StorageType
forall a. (?callStack::CallStack) => String -> a
error (String
"Coerce value given bad view " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ValueView -> String
forall a. Show a => a -> String
show ValueView
v)) (ValueView -> Maybe StorageType
viewType ValueView
v)
       le :: Bytes
le = Bytes -> StorageType -> Bytes
typeEnd Bytes
lo StorageType
ltp
       se :: Bytes
se = Bytes
so Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ StorageType -> Bytes
storageTypeSize StorageType
stp

-- | @LinearLoadStoreOffsetDiff stride delta@ represents the fact that
--   the difference between the load offset and the store offset is
--   of the form @stride * n + delta@ for some integer @n@, where
--   @stride@ and @delta@ are non-negative integers, and @n@ can be
--   positive, negative, or zero.  If no form if known, then @stride@ is @1@
--   and @delta@ is @0@.
data LinearLoadStoreOffsetDiff = LinearLoadStoreOffsetDiff Bytes Bytes

-- | This function computes a mux tree value for loading a chunk from inside
--   a previously-written value.  The @StorageType@ of the load indicates
--   the size of the loaded value and how we intend to view it.  The bounds,
--   if provided, are bounds on the difference between the load pointer and the
--   store pointer.  Postive values indicate the Load offset is larger than the
--   store offset.  These bounds, if provided, are used to shrink the size of
--   the computed mux tree, and can lead to significantly smaller results.
--   The @ValueView@ is the syntactic representation of the value being
--   loaded from.  The @LinearLoadStoreOffsetDiff@ form further reduces the size
--   of the mux tree by only considering (load offset - store offset) values of
--   the given form.
symbolicValueLoad ::
  BasePreference {- ^ whether addresses are based on store or load -} ->
  StorageType           {- ^ load type            -} ->
  Maybe (Integer, Integer) {- ^ optional bounds on the offset between load and store -} ->
  ValueView      {- ^ view of stored value -} ->
  LinearLoadStoreOffsetDiff {- ^ linear (load offset - store offset) form -} ->
  Mux (ValueCtor (ValueLoad OffsetExpr))
symbolicValueLoad :: BasePreference
-> StorageType
-> Maybe (Integer, Integer)
-> ValueView
-> LinearLoadStoreOffsetDiff
-> Mux (ValueCtor (ValueLoad OffsetExpr))
symbolicValueLoad BasePreference
pref StorageType
tp Maybe (Integer, Integer)
bnd ValueView
v (LinearLoadStoreOffsetDiff Bytes
stride Bytes
delta) =
  Cond
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a. Cond -> Mux a -> Mux a -> Mux a
Mux (Cond -> Cond -> Cond
Or (Bytes -> OffsetExpr
loadOffset Bytes
lsz OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Store) (Bytes -> OffsetExpr
storeOffset (StorageType -> Bytes
storageTypeSize StorageType
stp) OffsetExpr -> OffsetExpr -> Cond
.<= OffsetExpr
Load)) Mux (ValueCtor (ValueLoad OffsetExpr))
loadFail (Mux (ValueCtor (ValueLoad OffsetExpr))
 -> Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a b. (a -> b) -> a -> b
$
  OffsetExpr
-> OffsetExpr
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a.
OffsetExpr -> OffsetExpr -> Map Bytes (Mux a) -> Mux a -> Mux a
MuxTable OffsetExpr
Load OffsetExpr
Store Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
prefixTable (Mux (ValueCtor (ValueLoad OffsetExpr))
 -> Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a b. (a -> b) -> a -> b
$
  OffsetExpr
-> OffsetExpr
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a.
OffsetExpr -> OffsetExpr -> Map Bytes (Mux a) -> Mux a -> Mux a
MuxTable OffsetExpr
Store OffsetExpr
Load Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
suffixTable Mux (ValueCtor (ValueLoad OffsetExpr))
loadFail
  where
    lsz :: Bytes
lsz = Bytes -> StorageType -> Bytes
typeEnd Bytes
0 StorageType
tp
    stp :: StorageType
stp = case ValueView -> Maybe StorageType
viewType ValueView
v of
            Just StorageType
x -> StorageType
x
            Maybe StorageType
Nothing -> String -> [String] -> StorageType
forall a. (?callStack::CallStack) => String -> [String] -> a
panic String
"crucible-llvm:symbolicValueLoad"
                       [ String
"Unable obtain type of stored value ValueView" ]

    -- The prefix table represents cases where the load pointer occurs strictly before the
    -- write pointer, so that the end of the load may be partially satisfied by this write.
    prefixTable :: Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
prefixTable = Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkPrefixTable Bytes
prefixLoBound

    -- The suffix table represents cases where the load pointer occurs at or after the write
    -- pointer so that the load is fully satisfied or the beginning is partially satisfied
    -- by this write.
    suffixTable :: Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
suffixTable = Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkSuffixTable Bytes
suffixLoBound

    -- The smallest (non-negative) offset value that can occur in the suffix table.
    -- This is either 0 (load = store) or is given by the difference bound when
    -- the low value is positive.
    suffixLoBound :: Bytes
suffixLoBound =
      case Maybe (Integer, Integer)
bnd of
        Just (Integer
lo, Integer
_hi)
          | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 -> Bytes -> Bytes -> Bytes
adjustLoBound Bytes
delta (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes Integer
lo)
        Maybe (Integer, Integer)
_ -> Bytes
delta

    -- One past the largest offset value that can occur in the suffix table.
    -- This is either the length of the written value, or is given by the
    -- difference bound.  Note, in the case @hi@ is negative, the suffix table
    -- will be empty.
    suffixHiBound :: Bytes
suffixHiBound =
      case Maybe (Integer, Integer)
bnd of
        Just (Integer
_lo, Integer
hi)
          | Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0   -> Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
min (StorageType -> Bytes
storageTypeSize StorageType
stp) (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes Integer
hi Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
1)
          | Bool
otherwise -> Bytes
0
        Maybe (Integer, Integer)
_ -> StorageType -> Bytes
storageTypeSize StorageType
stp

    -- The smallest magnitude of offset that the load may occur
    -- behind the write pointer.  This is at least the stride of the alignment,
    -- but may also be given by the high bound value of the difference, if it is negative.
    prefixLoBound :: Bytes
prefixLoBound =
      case Maybe (Integer, Integer)
bnd of
        Just (Integer
_lo, Integer
hi)
          | Integer
hi Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 -> Bytes -> Bytes -> Bytes
adjustLoBound (Bytes
stride Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
delta) (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes (-Integer
hi))
        Maybe (Integer, Integer)
_ -> Bytes
stride Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
delta

    -- The largest magnitude of offset, plus one, that the load may occur
    -- behind the write pointer.  This is at most the length of the read,
    -- but may also be given by the low bound value of the offset difference,
    -- if it is negative.  Note, in the case that @lo@ is positive, the
    -- prefix table will be empty.
    prefixHiBound :: Bytes
prefixHiBound =
      case Maybe (Integer, Integer)
bnd of
        Just (Integer
lo, Integer
_hi)
          | Integer
lo Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0    -> Bytes -> Bytes -> Bytes
forall a. Ord a => a -> a -> a
min Bytes
lsz (Integer -> Bytes
forall a. Integral a => a -> Bytes
toBytes (-Integer
lo) Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
1)
          | Bool
otherwise -> Bytes
0
        Maybe (Integer, Integer)
_ -> Bytes
lsz

    -- Walk through prefix offset values, computing a mux tree of the values
    -- for those prefix loads.
    mkPrefixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
    mkPrefixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkPrefixTable Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
prefixHiBound = Bytes
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Bytes
i
        (ValueCtor (ValueLoad OffsetExpr)
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a. a -> Mux a
MuxVar ((Bytes -> OffsetExpr) -> ValueLoad Bytes -> ValueLoad OffsetExpr
forall a b. (a -> b) -> ValueLoad a -> ValueLoad b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bytes -> OffsetExpr
adjustFn (ValueLoad Bytes -> ValueLoad OffsetExpr)
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad OffsetExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
0 StorageType
tp Bytes
i ValueView
v))
        (Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkPrefixTable (Bytes
i Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
stride))
      | Bool
otherwise = Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
forall k a. Map k a
Map.empty
      where adjustFn :: Bytes -> OffsetExpr
adjustFn = BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadBeforeStoreOffset BasePreference
pref Bytes
i

    -- Walk through suffix offset values, computing a mux tree of the values
    -- for those suffix loads.
    mkSuffixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
    mkSuffixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkSuffixTable Bytes
i
      | Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
< Bytes
suffixHiBound =
        Bytes
-> Mux (ValueCtor (ValueLoad OffsetExpr))
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
-> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Bytes
i
        (ValueCtor (ValueLoad OffsetExpr)
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a. a -> Mux a
MuxVar ((Bytes -> OffsetExpr) -> ValueLoad Bytes -> ValueLoad OffsetExpr
forall a b. (a -> b) -> ValueLoad a -> ValueLoad b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Bytes -> OffsetExpr
adjustFn (ValueLoad Bytes -> ValueLoad OffsetExpr)
-> ValueCtor (ValueLoad Bytes) -> ValueCtor (ValueLoad OffsetExpr)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes
-> StorageType -> Bytes -> ValueView -> ValueCtor (ValueLoad Bytes)
valueLoad Bytes
i StorageType
tp Bytes
0 ValueView
v))
        (Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkSuffixTable (Bytes
i Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
stride))
      | Bool
otherwise = Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
forall k a. Map k a
Map.empty
      where adjustFn :: Bytes -> OffsetExpr
adjustFn = BasePreference -> Bytes -> Bytes -> OffsetExpr
fixLoadAfterStoreOffset BasePreference
pref Bytes
i

    loadFail :: Mux (ValueCtor (ValueLoad OffsetExpr))
loadFail = ValueCtor (ValueLoad OffsetExpr)
-> Mux (ValueCtor (ValueLoad OffsetExpr))
forall a. a -> Mux a
MuxVar (ValueLoad OffsetExpr -> ValueCtor (ValueLoad OffsetExpr)
forall a. a -> ValueCtor a
ValueCtorVar (OffsetExpr -> StorageType -> ValueLoad OffsetExpr
forall v. v -> StorageType -> ValueLoad v
OldMemory OffsetExpr
Load StorageType
tp))

    adjustLoBound :: Bytes -> Bytes -> Bytes
    adjustLoBound :: Bytes -> Bytes -> Bytes
adjustLoBound Bytes
i Bytes
bound = if Bytes
i Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
>= Bytes
bound
      then Bytes
i
      else Bytes -> Bytes -> Bytes
adjustLoBound (Bytes
i Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
stride) Bytes
bound

-- | Create a value of the given type made up of copies of the given byte.
memsetValue :: a -> StorageType -> ValueCtor a
memsetValue :: forall a. a -> StorageType -> ValueCtor a
memsetValue a
byte = StorageType -> ValueCtor a
go
  where
    val :: ValueCtor a
val = a -> ValueCtor a
forall a. a -> ValueCtor a
ValueCtorVar a
byte
    go :: StorageType -> ValueCtor a
go StorageType
tp =
      case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
        Bitvector Bytes
sz
          | Bytes
sz Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
1 -> ValueCtor a
val
          | Bool
otherwise -> Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
1 ValueCtor a
val (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
1) (StorageType -> ValueCtor a
go (Bytes -> StorageType
bitvectorType (Bytes
sz Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
1)))
        StorageTypeF StorageType
Float -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToFloat (StorageType -> ValueCtor a
go (Bytes -> StorageType
bitvectorType Bytes
4))
        StorageTypeF StorageType
Double -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToDouble (StorageType -> ValueCtor a
go (Bytes -> StorageType
bitvectorType Bytes
8))
        StorageTypeF StorageType
X86_FP80 -> ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToX86_FP80 (StorageType -> ValueCtor a
go (Bytes -> StorageType
bitvectorType Bytes
10))
        Array Natural
n StorageType
etp -> StorageType -> Vector (ValueCtor a) -> ValueCtor a
forall a. StorageType -> Vector (ValueCtor a) -> ValueCtor a
MkArray StorageType
etp (Int -> ValueCtor a -> Vector (ValueCtor a)
forall a. Int -> a -> Vector a
V.replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (StorageType -> ValueCtor a
go StorageType
etp))
        Struct Vector (Field StorageType)
flds -> Vector (Field StorageType, ValueCtor a) -> ValueCtor a
forall a. Vector (Field StorageType, ValueCtor a) -> ValueCtor a
MkStruct (Field StorageType -> (Field StorageType, ValueCtor a)
fldFn (Field StorageType -> (Field StorageType, ValueCtor a))
-> Vector (Field StorageType)
-> Vector (Field StorageType, ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (Field StorageType)
flds)
          where fldFn :: Field StorageType -> (Field StorageType, ValueCtor a)
fldFn Field StorageType
fld = (Field StorageType
fld, StorageType -> ValueCtor a
go (Field StorageType
fldField 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))

-- | Create value of type that splits at a particular byte offset.
--
-- This function uses the given 'StorageType' to determine how many bytes to
-- read (including accounting for padding in struct types).  The function to
-- load each byte is provided as an argument.
--
-- NOTE: The 'Offset' argument is not necessarily the offset into the
-- allocation; it *could* be zero if the load function captures the offset into
-- the allocation.
loadTypedValueFromBytes
  :: Offset -- ^ The initial offset to pass to the byte loading function
  -> StorageType -- ^ The type used to compute how many bytes to read
  -> (Offset -> IO a) -- ^ A function to read individual bytes (at the given offset)
  -> IO (ValueCtor a)
loadTypedValueFromBytes :: forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes Bytes
off StorageType
tp Bytes -> IO a
subFn = case StorageType -> StorageTypeF StorageType
storageTypeF StorageType
tp of
  Bitvector Bytes
size
    | Bytes
size Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
1 -> a -> ValueCtor a
forall a. a -> ValueCtor a
ValueCtorVar (a -> ValueCtor a) -> IO a -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> IO a
subFn Bytes
off
    | Bool
otherwise -> do
      ValueCtor a
head_byte <- a -> ValueCtor a
forall a. a -> ValueCtor a
ValueCtorVar (a -> ValueCtor a) -> IO a -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> IO a
subFn Bytes
off
      ValueCtor a
tail_bytes <- Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes
        (Bytes
off Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ Bytes
1)
        (Bytes -> StorageType
bitvectorType (Bytes
size Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
1))
        Bytes -> IO a
subFn
      ValueCtor a -> IO (ValueCtor a)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ValueCtor a -> IO (ValueCtor a))
-> ValueCtor a -> IO (ValueCtor a)
forall a b. (a -> b) -> a -> b
$ Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
forall a.
Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV Bytes
1 ValueCtor a
head_byte (Bytes
size Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
1) ValueCtor a
tail_bytes
  StorageTypeF StorageType
Float ->
    ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToFloat (ValueCtor a -> ValueCtor a)
-> IO (ValueCtor a) -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes Bytes
off (Bytes -> StorageType
bitvectorType Bytes
4) Bytes -> IO a
subFn
  StorageTypeF StorageType
Double ->
    ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToDouble (ValueCtor a -> ValueCtor a)
-> IO (ValueCtor a) -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes Bytes
off (Bytes -> StorageType
bitvectorType Bytes
8) Bytes -> IO a
subFn
  StorageTypeF StorageType
X86_FP80 ->
    ValueCtor a -> ValueCtor a
forall a. ValueCtor a -> ValueCtor a
BVToX86_FP80 (ValueCtor a -> ValueCtor a)
-> IO (ValueCtor a) -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes Bytes
off (Bytes -> StorageType
bitvectorType Bytes
10) Bytes -> IO a
subFn
  Array Natural
len StorageType
elem_type -> StorageType -> Vector (ValueCtor a) -> ValueCtor a
forall a. StorageType -> Vector (ValueCtor a) -> ValueCtor a
MkArray StorageType
elem_type (Vector (ValueCtor a) -> ValueCtor a)
-> IO (Vector (ValueCtor a)) -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> (Int -> IO (ValueCtor a)) -> IO (Vector (ValueCtor a))
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM
    (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
len)
    (\Int
idx -> Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes
      (Bytes
off Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ (Int -> Bytes
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
idx) Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
* (StorageType -> Bytes
storageTypeSize StorageType
elem_type))
      StorageType
elem_type
      Bytes -> IO a
subFn)
  Struct Vector (Field StorageType)
fields -> Vector (Field StorageType, ValueCtor a) -> ValueCtor a
forall a. Vector (Field StorageType, ValueCtor a) -> ValueCtor a
MkStruct (Vector (Field StorageType, ValueCtor a) -> ValueCtor a)
-> IO (Vector (Field StorageType, ValueCtor a)) -> IO (ValueCtor a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Field StorageType -> IO (Field StorageType, ValueCtor a))
-> Vector (Field StorageType)
-> IO (Vector (Field StorageType, ValueCtor a))
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM
    (\Field StorageType
field -> do
      ValueCtor a
field_val <- Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
forall a.
Bytes -> StorageType -> (Bytes -> IO a) -> IO (ValueCtor a)
loadTypedValueFromBytes
        (Bytes
off Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
+ (Field StorageType -> Bytes
forall v. Field v -> Bytes
fieldOffset Field StorageType
field))
        (Field StorageType
fieldField 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)
        Bytes -> IO a
subFn
      (Field StorageType, ValueCtor a)
-> IO (Field StorageType, ValueCtor a)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Field StorageType
field, ValueCtor a
field_val))
    Vector (Field StorageType)
fields