crucible-llvm-0.9: src/Lang/Crucible/LLVM/MemModel/Common.hs
-----------------------------------------------------------------------
-- |
-- Module : Lang.Crucible.LLVM.MemModel.Common
-- Description : Core definitions of the symbolic C memory model
-- Copyright : (c) Galois, Inc 2011-2016
-- License : BSD3
-- Maintainer : Rob Dockins <rdockins@galois.com>
-- Stability : provisional
------------------------------------------------------------------------
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
module Lang.Crucible.LLVM.MemModel.Common
( -- * Range declarations.
Range(..)
-- * Pointer declarations
, OffsetExpr(..)
, IntExpr(..)
, Cond(..)
, Mux(..)
, ValueCtor(..)
, BasePreference(..)
, RangeLoad(..)
, rangeLoad
, fixedOffsetRangeLoad
, fixedSizeRangeLoad
, symbolicRangeLoad
, symbolicUnboundedRangeLoad
, ValueView(..)
, ValueLoad(..)
, valueLoad
, LinearLoadStoreOffsetDiff(..)
, symbolicValueLoad
, loadBitvector
, memsetValue
, loadTypedValueFromBytes
) where
import Control.Exception (assert)
import Control.Lens
import Control.Monad (guard)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Vector (Vector)
import qualified Data.Vector as V
import Numeric.Natural
import Lang.Crucible.Panic ( panic )
import Lang.Crucible.LLVM.Bytes
import Lang.Crucible.LLVM.MemModel.Type
-- | @R i j@ denotes that the write should store in range [i..j).
data Range = R { rStart :: Addr, _rEnd :: Addr }
deriving (Eq, Show)
-- Value
data OffsetExpr
= OffsetAdd OffsetExpr IntExpr
| Load
| Store
deriving (Show)
data IntExpr
= OffsetDiff OffsetExpr OffsetExpr
| IntAdd IntExpr IntExpr
| CValue Bytes
| StoreSize
deriving (Show)
data Cond
= OffsetEq OffsetExpr OffsetExpr
| OffsetLe OffsetExpr OffsetExpr
| IntEq IntExpr IntExpr
| IntLe IntExpr IntExpr
| And Cond Cond
| Or Cond Cond
deriving (Show)
(.==) :: OffsetExpr -> OffsetExpr -> Cond
infix 4 .==
x .== y = OffsetEq x y
(.<=) :: OffsetExpr -> OffsetExpr -> Cond
infix 4 .<=
x .<= y = OffsetLe x y
infixl 6 .+
(.+) :: OffsetExpr -> IntExpr -> OffsetExpr
x .+ CValue 0 = x
x .+ y = OffsetAdd x y
infixl 6 .-
(.-) :: OffsetExpr -> OffsetExpr -> IntExpr
x .- y = OffsetDiff x y
-- Muxs
data Mux a
= Mux Cond (Mux a) (Mux a)
| MuxTable OffsetExpr OffsetExpr (Map Bytes (Mux a)) (Mux a)
-- ^ 'MuxTable' encodes a lookup table: @'MuxTable' p1 p2
-- 'Map.empty' z@ is equivalent to @z@, and @'MuxTable' p1 p2
-- ('Map.insert' (i, x) m) z@ is equivalent to @'Mux' (p1 '.+'
-- 'CValue' i '.==' p2) x ('MuxTable' p1 p2 m z)@.
| MuxVar a
deriving Show
-- Variable for mem model.
loadOffset :: Bytes -> OffsetExpr
loadOffset n = Load .+ CValue n
storeOffset :: Bytes -> OffsetExpr
storeOffset n = Store .+ CValue n
storeEnd :: OffsetExpr
storeEnd = Store .+ StoreSize
-- | @loadInStoreRange n@ returns predicate if Store <= Load && Load <= Store + n
loadInStoreRange :: Bytes -> Cond
loadInStoreRange (Bytes 0) = Load .== Store
loadInStoreRange n = And (Store .<= Load)
(Load .<= Store .+ CValue n)
-- Value constructor
-- | Describes how to construct a larger LLVM value as a combination
-- of smaller components.
data ValueCtor a
= ValueCtorVar a
-- | Concatenates two bitvectors.
-- The first bitvector contains values stored at the low-address bytes
-- while the second contains values at the high-address bytes. Thus, the
-- meaning of this depends on the endianness of the target architecture.
| ConcatBV (ValueCtor a) (ValueCtor a)
| BVToFloat (ValueCtor a)
| BVToDouble (ValueCtor a)
| BVToX86_FP80 (ValueCtor a)
-- | Cons one value to beginning of array.
| ConsArray (ValueCtor a) (ValueCtor a)
| AppendArray (ValueCtor a) (ValueCtor a)
| MkArray StorageType (Vector (ValueCtor a))
| MkStruct (Vector (Field StorageType, ValueCtor a))
deriving (Functor, Foldable, Traversable, Show)
concatBV :: Bytes -> ValueCtor a -> Bytes -> ValueCtor a -> ValueCtor a
concatBV _xw x _yw y = ConcatBV x y
singletonArray :: StorageType -> ValueCtor a -> ValueCtor a
singletonArray tp e = MkArray tp (V.singleton e)
-- | Create value of type that splits at a particular byte offset.
splitTypeValue :: StorageType -- ^ Type of value to create
-> Offset -- ^ Bytes offset to slice type at.
-> (Offset -> StorageType -> ValueCtor a) -- ^ Function for subtypes.
-> ValueCtor a
splitTypeValue tp d subFn = assert (d > 0) $
case storageTypeF tp of
Bitvector sz -> assert (d < sz) $
concatBV d (subFn 0 (bitvectorType d))
(sz - d) (subFn d (bitvectorType (sz - d)))
Float -> BVToFloat (subFn 0 (bitvectorType 4))
Double -> BVToDouble (subFn 0 (bitvectorType 8))
X86_FP80 -> BVToX86_FP80 (subFn 0 (bitvectorType 10))
Array n0 etp -> assert (n0 > 0) $ do
let esz = storageTypeSize etp
let (c,part) = assert (esz > 0) $ toInteger d `divMod` toInteger esz
let n = toInteger n0 - toInteger c
let o = d - toBytes part -- (Bytes c) * esz
let consPartial
| n < 0 = panic "splitTypeValue" ["Unexpected array size: " ++ show n, show tp, show d]
| part == 0 = subFn o (arrayType (fromInteger n) etp)
| n > 1 =
ConsArray (subFn o etp)
(subFn (o+esz) (arrayType (fromInteger (n-1)) etp))
| otherwise = assert (n == 1) $
singletonArray etp (subFn o etp)
let result
| c > 0 = assert (c < toInteger n0) $
AppendArray (subFn 0 (arrayType (fromInteger c) etp))
consPartial
| otherwise = consPartial
result
Struct flds -> MkStruct (fldFn <$> flds)
where fldFn fld = (fld, subFn (fieldOffset fld) (fld^.fieldVal))
-- | This is used so that when we are comparing symbolic loads against
-- previous stores, we can represent the difference as relative to
-- a fixed address whenever possible.
data BasePreference
= FixedLoad
| FixedStore
| NeitherFixed
deriving (Eq, Show)
-- RangeLoad
-- | A 'RangeLoad' describes different kinds of memory loads in the
-- context of a byte range copied into an old memory.
data RangeLoad a b
= OutOfRange a StorageType
-- ^ Load from an address range disjoint from the copied bytes.
-- The arguments represent the address and type of the load.
| InRange b StorageType
-- ^ Load consists of bytes within the copied range. The first
-- argument represents the offset relative to the start of the
-- copied bytes.
deriving (Show)
adjustOffset :: (b -> d)
-> (a -> c)
-> RangeLoad a b -> RangeLoad c d
adjustOffset _ outFn (OutOfRange a tp) = OutOfRange (outFn a) tp
adjustOffset inFn _ (InRange b tp) = InRange (inFn b) tp
-- | Decomposes a single load after a memcopy into a combination of
-- simple value loads.
rangeLoad ::
Addr {- ^ load offset -} ->
StorageType {- ^ load type -} ->
Range {- ^ copied range -} ->
ValueCtor (RangeLoad Addr Addr)
rangeLoad lo ltp s@(R so se)
| so == se = loadFail
| le <= so = loadFail
| se <= lo = loadFail
| lo < so = splitTypeValue ltp (so - lo) (\o tp -> rangeLoad (lo+o) tp s)
| se < le = splitTypeValue ltp (se - lo) (\o tp -> rangeLoad (lo+o) tp s)
| otherwise = assert (so <= lo && le <= se) $ ValueCtorVar (InRange (lo - so) ltp)
where le = typeEnd lo ltp
loadFail = ValueCtorVar (OutOfRange lo ltp)
-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store offsets are concrete and the store size is bounded
fixedOffsetRangeLoad :: Addr
-- ^ Address of load
-> StorageType
-- ^ Type to load
-> Addr
-- ^ Address of store
-> Mux (ValueCtor (RangeLoad Addr Addr))
fixedOffsetRangeLoad l tp s
| s < l = do -- Store is before load.
let sd = l - s -- Number of bytes load comes after store
Mux (IntLe StoreSize (CValue sd)) loadFail (loadCase (sd+1))
| le <= s = loadFail -- No load if load ends before write.
| otherwise = loadCase 0
where
le = typeEnd l tp
loadCase i
| i < le-s = Mux (IntEq StoreSize (CValue i)) (loadVal i) (loadCase (i+1))
| otherwise = loadVal i
loadVal ssz = MuxVar (rangeLoad l tp (R s (s+ssz)))
loadFail = MuxVar (ValueCtorVar (OutOfRange l tp))
-- | @fixLoadBeforeStoreOffset pref i k@ adjusts a pointer value that is relative
-- the load address into a global pointer. The code assumes that @load + i == store@.
fixLoadBeforeStoreOffset :: BasePreference -> Offset -> Offset -> OffsetExpr
fixLoadBeforeStoreOffset pref i k
| pref == FixedStore = Store .+ CValue (k - i)
| otherwise = Load .+ CValue k
-- | @fixLoadAfterStoreOffset pref i k@ adjusts a pointer value that is relative
-- the load address into a global pointer. The code assumes that @load == store + i@.
fixLoadAfterStoreOffset :: BasePreference -> Offset -> Offset -> OffsetExpr
fixLoadAfterStoreOffset pref i k = assert (k >= i) $
case pref of
FixedStore -> Store .+ CValue k
_ -> Load .+ CValue (k - i)
-- | @loadFromStoreStart pref tp i j@ loads a value of type @tp@ from a range under the
-- assumptions that @load + i == store@ and @j = i + min(StoreSize, typeEnd(tp)@.
loadFromStoreStart :: BasePreference
-> StorageType
-> Offset
-> Offset
-> ValueCtor (RangeLoad OffsetExpr IntExpr)
loadFromStoreStart pref tp i j = adjustOffset inFn outFn <$> rangeLoad 0 tp (R i j)
where inFn = CValue
outFn = fixLoadBeforeStoreOffset pref i
-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store values are concrete
fixedSizeRangeLoad :: BasePreference -- ^ Whether addresses are based on store or load.
-> StorageType
-> Bytes
-> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
fixedSizeRangeLoad _ tp 0 = MuxVar (ValueCtorVar (OutOfRange Load tp))
fixedSizeRangeLoad pref tp ssz =
Mux (loadOffset lsz .<= Store) loadFail (prefixL lsz)
where
lsz = typeEnd 0 tp
prefixL i
| i > 0 = Mux (loadOffset i .== Store) (loadVal i) (prefixL (i-1))
-- Special case where we skip some offsets, it it won't
-- make more splitting
| lsz <= ssz && pref == NeitherFixed =
-- Load is contained in storage.
Mux (loadInStoreRange (ssz-lsz)) loadSucc $
-- Load extends past end of storage
suffixS (ssz-lsz)
| otherwise = suffixS 0
suffixS i
| i < ssz = Mux (Load .== storeOffset i) (storeVal i) (suffixS (i+1))
| otherwise = loadFail
loadVal i = MuxVar (loadFromStoreStart pref tp i (i+ssz))
storeVal i = MuxVar (adjustOffset inFn outFn <$> rangeLoad i tp (R 0 ssz))
where inFn = CValue
outFn = fixLoadAfterStoreOffset pref i
loadSucc = MuxVar (ValueCtorVar (InRange (Load .- Store) tp))
loadFail = MuxVar (ValueCtorVar (OutOfRange Load tp))
-- | Produces a @Mux ValueCtor@ expression representing the range load conditions
-- when the load and store values are symbolic and the @StoreSize@ is bounded.
symbolicRangeLoad :: BasePreference -> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicRangeLoad pref tp =
Mux (Store .<= Load)
(Mux (loadOffset sz .<= storeEnd) (loadVal0 sz) (loadIter0 (sz-1)))
(storeAfterLoad 1)
where
sz = typeEnd 0 tp
loadIter0 j
| j > 0 = Mux (loadOffset j .== storeEnd) (loadVal0 j) (loadIter0 (j-1))
| otherwise = loadFail
loadVal0 j = MuxVar $ adjustOffset inFn outFn <$> rangeLoad 0 tp (R 0 j)
where inFn k = IntAdd (OffsetDiff Load Store) (CValue k)
outFn k = OffsetAdd Load (CValue k)
storeAfterLoad i
| i < sz = Mux (loadOffset i .== Store) (loadFromOffset i) (storeAfterLoad (i+1))
| otherwise = loadFail
loadFromOffset i =
assert (0 < i && i < sz) $
Mux (IntLe (CValue (sz - i)) StoreSize) (loadVal i (i+sz)) (f (sz-1))
where f j | j > i = Mux (IntEq (CValue (j-i)) StoreSize) (loadVal i j) (f (j-1))
| otherwise = loadFail
loadVal i j = MuxVar (loadFromStoreStart pref tp i j)
loadFail = MuxVar (ValueCtorVar (OutOfRange Load tp))
-- | Produces a @Mux ValueCtor@ expression representing the RangeLoad conditions
-- when the load and store values are symbolic and the @StoreSize@ is unbounded.
symbolicUnboundedRangeLoad :: BasePreference -> StorageType -> Mux (ValueCtor (RangeLoad OffsetExpr IntExpr))
symbolicUnboundedRangeLoad pref tp =
Mux (Store .<= Load)
(loadVal0 sz)
(storeAfterLoad 1)
where
sz = typeEnd 0 tp
loadVal0 j = MuxVar $ adjustOffset inFn outFn <$> rangeLoad 0 tp (R 0 j)
where inFn k = IntAdd (OffsetDiff Load Store) (CValue k)
outFn k = OffsetAdd Load (CValue k)
storeAfterLoad i
| i < sz = Mux (loadOffset i .== Store) (loadFromOffset i) (storeAfterLoad (i+1))
| otherwise = loadFail
loadFromOffset i =
assert (0 < i && i < sz) $
Mux (IntLe (CValue (sz - i)) StoreSize) (loadVal i (i+sz)) (f (sz-1))
where f j | j > i = Mux (IntEq (CValue (j-i)) StoreSize) (loadVal i j) (f (j-1))
| otherwise = loadFail
loadVal i j = MuxVar (loadFromStoreStart pref tp i j)
loadFail = MuxVar (ValueCtorVar (OutOfRange Load tp))
-- ValueView
-- | Represents a projection of a sub-component out of a larger LLVM value.
data ValueView
= ValueViewVar StorageType
-- | Select low-address bytes in the bitvector.
-- The sizes include the number of low bytes, and the number of high bytes.
| SelectPrefixBV Bytes Bytes ValueView
-- | Select the given number of high-address bytes in the bitvector.
-- The sizes include the number of low bytes, and the number of high bytes.
| SelectSuffixBV Bytes Bytes ValueView
| FloatToBV ValueView
| DoubleToBV ValueView
| X86_FP80ToBV ValueView
| ArrayElt Natural StorageType Natural ValueView
| FieldVal (Vector (Field StorageType)) Int ValueView
deriving (Show, Eq, Ord)
viewType :: ValueView -> Maybe StorageType
viewType (ValueViewVar tp) = Just tp
viewType (SelectPrefixBV u v vv) =
do tp <- storageTypeF <$> viewType vv
guard (Bitvector (u + v) == tp)
pure $ bitvectorType u
viewType (SelectSuffixBV u v vv) =
do tp <- storageTypeF <$> viewType vv
guard (Bitvector (u + v) == tp)
pure $ bitvectorType v
viewType (FloatToBV vv) =
do tp <- storageTypeF <$> viewType vv
guard (Float == tp)
pure $ bitvectorType 4
viewType (DoubleToBV vv) =
do tp <- storageTypeF <$> viewType vv
guard (Double == tp)
pure $ bitvectorType 8
viewType (X86_FP80ToBV vv) =
do tp <- storageTypeF <$> viewType vv
guard (X86_FP80 == tp)
pure $ bitvectorType 10
viewType (ArrayElt n etp i vv) =
do tp <- storageTypeF <$> viewType vv
guard (i < n && Array n etp == tp)
pure $ etp
viewType (FieldVal v i vv) =
do tp <- storageTypeF <$> viewType vv
guard (Struct v == tp)
view fieldVal <$> (v V.!? i)
-- | A 'ValueLoad' describes different kinds of memory loads in the
-- context of a new value stored into an old memory.
data ValueLoad v
= OldMemory v StorageType
-- ^ Load from an address range disjoint from the stored value.
-- The arguments represent the address and type of the load.
| LastStore ValueView
-- ^ Load consists of valid bytes within the stored value.
| InvalidMemory StorageType
-- ^ Load touches invalid memory. Currently, this can only arise when
-- trying to read struct padding bytes as a bitvector.
deriving (Functor,Show)
loadBitvector :: Addr -> Bytes -> Addr -> ValueView -> ValueCtor (ValueLoad Addr)
loadBitvector lo lw so v = do
let le = lo + lw
let ltp = bitvectorType lw
let stp = fromMaybe (error ("loadBitvector given bad view " ++ show v)) (viewType v)
let retValue eo v' = (sz', valueLoad lo' (bitvectorType sz') eo v')
where etp = fromMaybe (error ("Bad view " ++ show v')) (viewType v')
esz = storageTypeSize etp
lo' = max lo eo
sz' = min le (eo+esz) - lo'
case storageTypeF stp of
Bitvector sw
| so < lo -> do
-- Number of bytes to drop.
let d = lo - so
-- Store is before load.
valueLoad lo ltp lo (SelectSuffixBV d (sw - d) v)
| otherwise ->
-- TODO(#1560): This assertion can fail.
-- Load ends before store ends.
-- assert (lo == so && lw < sw) $
valueLoad lo ltp so (SelectPrefixBV lw (sw - lw) v)
Float -> valueLoad lo ltp so (FloatToBV v)
Double -> valueLoad lo ltp so (DoubleToBV v)
X86_FP80 -> valueLoad lo ltp so (X86_FP80ToBV v)
Array n tp -> snd $ foldl1 cv (val <$> r)
where cv (wx,x) (wy,y) = (wx + wy, concatBV wx x wy y)
esz = storageTypeSize tp
c0 = assert (esz > 0) $ toInteger (lo - so) `div` toInteger esz
(c1, p1) = toInteger (le - so) `divMod` toInteger esz
-- Get range of indices to read.
r | p1 == 0 = assert (c1 > c0) [c0..c1-1]
| otherwise = assert (c1 >= c0) [c0..c1]
val i
| i >= 0 = retValue (so + natBytesMul (fromInteger i) esz) (ArrayElt n tp (fromInteger i) v)
| otherwise = panic "loadBitvector" ["Bad array index", show i, show (lo, lw, so, v)]
Struct sflds -> assert (not (null r)) $ snd $ foldl1 cv r
where cv (wx,x) (wy,y) = (wx+wy, concatBV wx x wy y)
r = concat (zipWith val [0..] (V.toList sflds))
val i f = v1
where eo = so + fieldOffset f
ee = eo + storageTypeSize (f^.fieldVal)
v1 | le <= eo = v2
| ee <= lo = v2
| otherwise = retValue eo (FieldVal sflds i v) : v2
v2 | fieldPad f == 0 = [] -- Return no padding.
| le <= ee = [] -- Nothing of load ends before padding.
-- Nothing if padding ends before load begins.
| ee+fieldPad f <= lo = []
| otherwise = [(p, ValueCtorVar badMem)]
where p = min (ee+fieldPad f) le - (max lo ee)
tpPad = bitvectorType p
badMem = InvalidMemory tpPad
-- | Decomposes a single load after a store into a combination of
-- simple value loads.
valueLoad ::
Addr {- ^ load address -} ->
StorageType {- ^ load type -} ->
Addr {- ^ store address -} ->
ValueView {- ^ view of stored value -} ->
ValueCtor (ValueLoad Addr)
valueLoad lo ltp so v
-- The non-zero test ensures that 0-byte loads are always overlapping
-- with the most recent store so that they're not spuriously rejected.
| le <= so && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Load ends before store
| se <= lo && nonZeroLoad = ValueCtorVar (OldMemory lo ltp) -- Store ends before load
-- Load is before store.
| lo < so = splitTypeValue ltp (so - lo) (\o tp -> valueLoad (lo+o) tp so v)
-- Load ends after store ends.
| se < le = splitTypeValue ltp (le - se) (\o tp -> valueLoad (lo+o) tp so v)
| (lo,ltp) == (so,stp) = ValueCtorVar (LastStore v)
| otherwise =
case storageTypeF ltp of
Bitvector lw -> loadBitvector lo lw so v
Float -> BVToFloat $ valueLoad lo (bitvectorType 4) so v
Double -> BVToDouble $ valueLoad lo (bitvectorType 8) so v
X86_FP80 -> BVToX86_FP80 $ valueLoad lo (bitvectorType 10) so v
Array ln tp ->
let leSize = storageTypeSize tp
val i = valueLoad (lo+leSize*fromIntegral i) tp so v
in MkArray tp (V.generate (fromIntegral ln) val)
Struct lflds ->
let val f = (f, valueLoad (lo+fieldOffset f) (f^.fieldVal) so v)
in MkStruct (val <$> lflds)
where stp = fromMaybe (error ("Coerce value given bad view " ++ show v)) (viewType v)
le = typeEnd lo ltp
se = so + storageTypeSize stp
nonZeroLoad = le - lo > 0
-- | @LinearLoadStoreOffsetDiff stride delta@ represents the fact that
-- the difference between the load offset and the store offset is
-- of the form @stride * n + delta@ for some integer @n@, where
-- @stride@ and @delta@ are non-negative integers, and @n@ can be
-- positive, negative, or zero. If no form if known, then @stride@ is @1@
-- and @delta@ is @0@.
data LinearLoadStoreOffsetDiff = LinearLoadStoreOffsetDiff Bytes Bytes
-- | This function computes a mux tree value for loading a chunk from inside
-- a previously-written value. The @StorageType@ of the load indicates
-- the size of the loaded value and how we intend to view it. The bounds,
-- if provided, are bounds on the difference between the load pointer and the
-- store pointer. Postive values indicate the Load offset is larger than the
-- store offset. These bounds, if provided, are used to shrink the size of
-- the computed mux tree, and can lead to significantly smaller results.
-- The @ValueView@ is the syntactic representation of the value being
-- loaded from. The @LinearLoadStoreOffsetDiff@ form further reduces the size
-- of the mux tree by only considering (load offset - store offset) values of
-- the given form.
symbolicValueLoad ::
BasePreference {- ^ whether addresses are based on store or load -} ->
StorageType {- ^ load type -} ->
Maybe (Integer, Integer) {- ^ optional bounds on the offset between load and store -} ->
ValueView {- ^ view of stored value -} ->
LinearLoadStoreOffsetDiff {- ^ linear (load offset - store offset) form -} ->
Mux (ValueCtor (ValueLoad OffsetExpr))
symbolicValueLoad pref tp bnd v (LinearLoadStoreOffsetDiff stride delta) =
Mux (Or (loadOffset lsz .<= Store) (storeOffset (storageTypeSize stp) .<= Load)) loadFail $
MuxTable Load Store prefixTable $
MuxTable Store Load suffixTable loadFail
where
lsz = typeEnd 0 tp
stp = case viewType v of
Just x -> x
Nothing -> panic "crucible-llvm:symbolicValueLoad"
[ "Unable obtain type of stored value ValueView" ]
-- The prefix table represents cases where the load pointer occurs strictly before the
-- write pointer, so that the end of the load may be partially satisfied by this write.
prefixTable = mkPrefixTable prefixLoBound
-- The suffix table represents cases where the load pointer occurs at or after the write
-- pointer so that the load is fully satisfied or the beginning is partially satisfied
-- by this write.
suffixTable = mkSuffixTable suffixLoBound
-- The smallest (non-negative) offset value that can occur in the suffix table.
-- This is either 0 (load = store) or is given by the difference bound when
-- the low value is positive.
suffixLoBound =
case bnd of
Just (lo, _hi)
| lo > 0 -> adjustLoBound delta (toBytes lo)
_ -> delta
-- One past the largest offset value that can occur in the suffix table.
-- This is either the length of the written value, or is given by the
-- difference bound. Note, in the case @hi@ is negative, the suffix table
-- will be empty.
suffixHiBound =
case bnd of
Just (_lo, hi)
| hi >= 0 -> min (storageTypeSize stp) (toBytes hi + 1)
| otherwise -> 0
_ -> storageTypeSize stp
-- The smallest magnitude of offset that the load may occur
-- behind the write pointer. This is at least the stride of the alignment,
-- but may also be given by the high bound value of the difference, if it is negative.
prefixLoBound =
case bnd of
Just (_lo, hi)
| hi < 0 -> adjustLoBound (stride - delta) (toBytes (-hi))
_ -> stride - delta
-- The largest magnitude of offset, plus one, that the load may occur
-- behind the write pointer. This is at most the length of the read,
-- but may also be given by the low bound value of the offset difference,
-- if it is negative. Note, in the case that @lo@ is positive, the
-- prefix table will be empty.
prefixHiBound =
case bnd of
Just (lo, _hi)
| lo < 0 -> min lsz (toBytes (-lo) + 1)
| otherwise -> 0
_ -> lsz
-- Walk through prefix offset values, computing a mux tree of the values
-- for those prefix loads.
mkPrefixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkPrefixTable i
| i < prefixHiBound = Map.insert i
(MuxVar (fmap adjustFn <$> valueLoad 0 tp i v))
(mkPrefixTable (i + stride))
| otherwise = Map.empty
where adjustFn = fixLoadBeforeStoreOffset pref i
-- Walk through suffix offset values, computing a mux tree of the values
-- for those suffix loads.
mkSuffixTable :: Bytes -> Map Bytes (Mux (ValueCtor (ValueLoad OffsetExpr)))
mkSuffixTable i
| i < suffixHiBound =
Map.insert i
(MuxVar (fmap adjustFn <$> valueLoad i tp 0 v))
(mkSuffixTable (i + stride))
| otherwise = Map.empty
where adjustFn = fixLoadAfterStoreOffset pref i
loadFail = MuxVar (ValueCtorVar (OldMemory Load tp))
adjustLoBound :: Bytes -> Bytes -> Bytes
adjustLoBound i bound = if i >= bound
then i
else adjustLoBound (i + stride) bound
-- | Create a value of the given type made up of copies of the given byte.
memsetValue :: a -> StorageType -> ValueCtor a
memsetValue byte = go
where
val = ValueCtorVar byte
go tp =
case storageTypeF tp of
Bitvector sz
| sz <= 1 -> val
| otherwise -> concatBV 1 val (sz - 1) (go (bitvectorType (sz - 1)))
Float -> BVToFloat (go (bitvectorType 4))
Double -> BVToDouble (go (bitvectorType 8))
X86_FP80 -> BVToX86_FP80 (go (bitvectorType 10))
Array n etp -> MkArray etp (V.replicate (fromIntegral n) (go etp))
Struct flds -> MkStruct (fldFn <$> flds)
where fldFn fld = (fld, go (fld^.fieldVal))
-- | Create value of type that splits at a particular byte offset.
--
-- This function uses the given 'StorageType' to determine how many bytes to
-- read (including accounting for padding in struct types). The function to
-- load each byte is provided as an argument.
--
-- NOTE: The 'Offset' argument is not necessarily the offset into the
-- allocation; it *could* be zero if the load function captures the offset into
-- the allocation.
loadTypedValueFromBytes
:: Offset -- ^ The initial offset to pass to the byte loading function
-> StorageType -- ^ The type used to compute how many bytes to read
-> (Offset -> IO a) -- ^ A function to read individual bytes (at the given offset)
-> IO (ValueCtor a)
loadTypedValueFromBytes off tp subFn = case storageTypeF tp of
Bitvector size
| size <= 1 -> ValueCtorVar <$> subFn off
| otherwise -> do
head_byte <- ValueCtorVar <$> subFn off
tail_bytes <- loadTypedValueFromBytes
(off + 1)
(bitvectorType (size - 1))
subFn
return $ concatBV 1 head_byte (size - 1) tail_bytes
Float ->
BVToFloat <$> loadTypedValueFromBytes off (bitvectorType 4) subFn
Double ->
BVToDouble <$> loadTypedValueFromBytes off (bitvectorType 8) subFn
X86_FP80 ->
BVToX86_FP80 <$> loadTypedValueFromBytes off (bitvectorType 10) subFn
Array len elem_type -> MkArray elem_type <$> V.generateM
(fromIntegral len)
(\idx -> loadTypedValueFromBytes
(off + (fromIntegral idx) * (storageTypeSize elem_type))
elem_type
subFn)
Struct fields -> MkStruct <$> V.mapM
(\field -> do
field_val <- loadTypedValueFromBytes
(off + (fieldOffset field))
(field^.fieldVal)
subFn
return (field, field_val))
fields