{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module Lang.Crucible.LLVM.MemModel.Common
(
Range(..)
, 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
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)
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
data Mux a
= Mux Cond (Mux a) (Mux a)
| MuxTable OffsetExpr OffsetExpr (Map Bytes (Mux a)) (Mux a)
| 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
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 :: 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)
data ValueCtor a
= ValueCtorVar a
| ConcatBV (ValueCtor a) (ValueCtor a)
| BVToFloat (ValueCtor a)
| BVToDouble (ValueCtor a)
| BVToX86_FP80 (ValueCtor a)
| 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)
splitTypeValue :: StorageType
-> Offset
-> (Offset -> StorageType -> ValueCtor a)
-> 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
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))
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)
data RangeLoad a b
= OutOfRange a StorageType
| InRange b StorageType
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
rangeLoad ::
Addr ->
StorageType ->
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)
fixedOffsetRangeLoad :: Addr
-> StorageType
-> Addr
-> 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
let sd :: Bytes
sd = Bytes
l Bytes -> 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
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
| 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 :: 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 :: 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 :: 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
fixedSizeRangeLoad :: BasePreference
-> 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))
| 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 =
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
$
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))
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))
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))
data ValueView
= ValueViewVar StorageType
| SelectPrefixBV Bytes Bytes ValueView
| 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)
data ValueLoad v
= OldMemory v StorageType
| LastStore ValueView
| InvalidMemory StorageType
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
let d :: Bytes
d = Bytes
lo Bytes -> Bytes -> Bytes
forall a. Num a => a -> a -> a
- Bytes
so
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
$
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
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 = []
| Bytes
le Bytes -> Bytes -> Bool
forall a. Ord a => a -> a -> Bool
<= Bytes
ee = []
| 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
valueLoad ::
Addr ->
StorageType ->
Addr ->
ValueView ->
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)
| 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)
| 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)
| 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
data LinearLoadStoreOffsetDiff = LinearLoadStoreOffsetDiff Bytes Bytes
symbolicValueLoad ::
BasePreference ->
StorageType ->
Maybe (Integer, Integer) ->
ValueView ->
LinearLoadStoreOffsetDiff ->
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" ]
prefixTable :: Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
prefixTable = Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkPrefixTable Bytes
prefixLoBound
suffixTable :: Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
suffixTable = Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkSuffixTable Bytes
suffixLoBound
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
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
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
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
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
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
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))
loadTypedValueFromBytes
:: Offset
-> StorageType
-> (Offset -> IO a)
-> 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