{-# Language GADTs, DataKinds, TypeOperators #-}
{-# Language ScopedTypeVariables #-}
{-# Language Rank2Types #-}
module Lang.Crucible.Vector
( module Data.Parameterized.Vector
, fromBV
, toBV
, joinVecBV
, splitVecBV
) where
import Prelude hiding (length,zipWith)
import Data.Coerce
import Data.Proxy
import Data.Parameterized.NatRepr
import Data.Parameterized.Vector
import Data.Parameterized.Utils.Endian
import Lang.Crucible.Types
import Lang.Crucible.Syntax (IsExpr(..))
import Lang.Crucible.CFG.Expr ( App( BVConcat, BVSelect ) )
toBV :: forall f n w. (1 <= w, IsExpr f) =>
Endian ->
NatRepr w ->
Vector n (f (BVType w)) -> f (BVType (n * w))
toBV :: forall (f :: CrucibleType -> Type) (n :: Natural) (w :: Natural).
(1 <= w, IsExpr f) =>
Endian
-> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
toBV Endian
endian NatRepr w
w Vector n (f (BVType w))
xs = f (BVType (n * w))
ys
where
xs' :: Vector n (Bits f w)
xs' = Vector n (f (BVType w)) -> Vector n (Bits f w)
forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec Vector n (f (BVType w))
xs
jn :: (1 <= b) => NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
jn :: forall (b :: Natural).
(1 <= b) =>
NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
jn = case Endian
endian of
Endian
LittleEndian -> NatRepr w -> NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnLittle NatRepr w
w
Endian
BigEndian -> NatRepr w -> NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnBig NatRepr w
w
Bits f (BVType (n * w))
ys = (forall (b :: Natural).
(1 <= b) =>
NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b))
-> NatRepr w -> Vector n (Bits f w) -> Bits f (n * w)
forall (f :: Natural -> Type) (n :: Natural) (w :: Natural).
(1 <= w) =>
(forall (l :: Natural).
(1 <= l) =>
NatRepr l -> f w -> f l -> f (w + l))
-> NatRepr w -> Vector n (f w) -> f (n * w)
joinWith NatRepr l -> Bits f w -> Bits f l -> Bits f (w + l)
forall (b :: Natural).
(1 <= b) =>
NatRepr b -> Bits f w -> Bits f b -> Bits f (w + b)
jn NatRepr w
w Vector n (Bits f w)
xs'
{-# Inline toBV #-}
coerceVec :: Coercible a b => Vector n a -> Vector n b
coerceVec :: forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec = Vector n a -> Vector n b
forall a b. Coercible a b => a -> b
coerce
newtype Bits f n = Bits (f (BVType n))
jnBig :: (IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b ->
Bits f a -> Bits f b -> Bits f (a + b)
jnBig :: forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnBig NatRepr a
la NatRepr b
lb (Bits f (BVType a)
a) (Bits f (BVType b)
b) =
case LeqProof 1 a -> NatRepr b -> LeqProof 1 (a + b)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
(p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (Proxy 1 -> NatRepr a -> LeqProof 1 a
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
(g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) NatRepr a
la) NatRepr b
lb of { LeqProof 1 (a + b)
LeqProof ->
f (BVType (a + b)) -> Bits f (a + b)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType (a + b)) -> f (BVType (a + b))
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr a
-> NatRepr b
-> f (BVType a)
-> f (BVType b)
-> App (ExprExt f) f (BVType (a + b))
forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type)
ext.
(1 <= u, 1 <= v, 1 <= (u + v)) =>
NatRepr u
-> NatRepr v
-> f (BVType u)
-> f (BVType v)
-> App ext f ('BaseToType (BaseBVType (u + v)))
BVConcat NatRepr a
la NatRepr b
lb f (BVType a)
a f (BVType b)
b)) }
{-# Inline jnBig #-}
jnLittle :: (IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b ->
Bits f a -> Bits f b -> Bits f (a + b)
jnLittle :: forall (f :: CrucibleType -> Type) (a :: Natural) (b :: Natural).
(IsExpr f, 1 <= a, 1 <= b) =>
NatRepr a -> NatRepr b -> Bits f a -> Bits f b -> Bits f (a + b)
jnLittle NatRepr a
la NatRepr b
lb (Bits f (BVType a)
a) (Bits f (BVType b)
b) =
case LeqProof 1 b -> NatRepr a -> LeqProof 1 (b + a)
forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
(p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd (Proxy 1 -> NatRepr b -> LeqProof 1 b
forall (m :: Natural) (n :: Natural) (f :: Natural -> Type)
(g :: Natural -> Type).
(m <= n) =>
f m -> g n -> LeqProof m n
leqProof (Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1) NatRepr b
lb) NatRepr a
la of { LeqProof 1 (b + a)
LeqProof ->
case NatRepr b -> NatRepr a -> (b + a) :~: (a + b)
forall (f :: Natural -> Type) (m :: Natural) (g :: Natural -> Type)
(n :: Natural).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr b
lb NatRepr a
la of { (b + a) :~: (a + b)
Refl ->
f (BVType (b + a)) -> Bits f (b + a)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType (b + a)) -> f (BVType (b + a))
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr b
-> NatRepr a
-> f (BVType b)
-> f (BVType a)
-> App (ExprExt f) f (BVType (b + a))
forall (u :: Natural) (v :: Natural) (f :: CrucibleType -> Type)
ext.
(1 <= u, 1 <= v, 1 <= (u + v)) =>
NatRepr u
-> NatRepr v
-> f (BVType u)
-> f (BVType v)
-> App ext f ('BaseToType (BaseBVType (u + v)))
BVConcat NatRepr b
lb NatRepr a
la f (BVType b)
b f (BVType a)
a)) }}
{-# Inline jnLittle #-}
fromBV :: forall f w n.
(1 <= w, 1 <= n, IsExpr f) =>
Endian ->
NatRepr n -> NatRepr w -> f (BVType (n * w)) -> Vector n (f (BVType w))
fromBV :: forall (f :: CrucibleType -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n, IsExpr f) =>
Endian
-> NatRepr n
-> NatRepr w
-> f (BVType (n * w))
-> Vector n (f (BVType w))
fromBV Endian
e NatRepr n
n NatRepr w
w f (BVType (n * w))
xs = Vector n (Bits f w) -> Vector n (f (BVType w))
forall a b (n :: Natural).
Coercible a b =>
Vector n a -> Vector n b
coerceVec (Endian
-> (forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w)
-> NatRepr n
-> NatRepr w
-> Bits f (n * w)
-> Vector n (Bits f w)
forall (f :: Natural -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n) =>
Endian
-> (forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> f (n * w) -> f w)
-> NatRepr n
-> NatRepr w
-> f (n * w)
-> Vector n (f w)
splitWith Endian
e NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
sel NatRepr n
n NatRepr w
w (f (BVType (n * w)) -> Bits f (n * w)
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits f (BVType (n * w))
xs))
where
sel :: (i + w <= n * w) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
sel :: forall (i :: Natural).
((i + w) <= (n * w)) =>
NatRepr (n * w) -> NatRepr i -> Bits f (n * w) -> Bits f w
sel NatRepr (n * w)
totL NatRepr i
i (Bits f (BVType (n * w))
val) =
case NatRepr n -> NatRepr w -> LeqProof 1 (n * w)
forall (p :: Natural -> Type) (q :: Natural -> Type) (x :: Natural)
(y :: Natural).
(1 <= x, 1 <= y) =>
p x -> q y -> LeqProof 1 (x * y)
leqMulPos NatRepr n
n NatRepr w
w of { LeqProof 1 (n * w)
LeqProof ->
f (BVType w) -> Bits f w
forall (f :: CrucibleType -> Type) (n :: Natural).
f (BVType n) -> Bits f n
Bits (App (ExprExt f) f (BVType w) -> f (BVType w)
forall (tp :: CrucibleType). App (ExprExt f) f tp -> f tp
forall (e :: CrucibleType -> Type) (tp :: CrucibleType).
IsExpr e =>
App (ExprExt e) e tp -> e tp
app (NatRepr i
-> NatRepr w
-> NatRepr (n * w)
-> f (BVType (n * w))
-> App (ExprExt f) f (BVType w)
forall (w :: Natural) (len :: Natural) (idx :: Natural)
(f :: CrucibleType -> Type) ext.
(1 <= w, 1 <= len, (idx + len) <= w) =>
NatRepr idx
-> NatRepr len
-> NatRepr w
-> f (BVType w)
-> App ext f ('BaseToType (BaseBVType len))
BVSelect NatRepr i
i NatRepr w
w NatRepr (n * w)
totL f (BVType (n * w))
val)) }
{-# Inline fromBV #-}
joinVecBV :: (IsExpr f, 1 <= i, 1 <= w, 1 <= n) =>
Endian ->
NatRepr w ->
NatRepr i ->
Vector (n * i) (f (BVType w)) ->
Vector n (f (BVType (i * w)))
joinVecBV :: forall (f :: CrucibleType -> Type) (i :: Natural) (w :: Natural)
(n :: Natural).
(IsExpr f, 1 <= i, 1 <= w, 1 <= n) =>
Endian
-> NatRepr w
-> NatRepr i
-> Vector (n * i) (f (BVType w))
-> Vector n (f (BVType (i * w)))
joinVecBV Endian
e NatRepr w
w NatRepr i
i Vector (n * i) (f (BVType w))
xs = Endian
-> NatRepr w -> Vector i (f (BVType w)) -> f (BVType (i * w))
forall (f :: CrucibleType -> Type) (n :: Natural) (w :: Natural).
(1 <= w, IsExpr f) =>
Endian
-> NatRepr w -> Vector n (f (BVType w)) -> f (BVType (n * w))
toBV Endian
e NatRepr w
w (Vector i (f (BVType w)) -> f (BVType (i * w)))
-> Vector n (Vector i (f (BVType w)))
-> Vector n (f (BVType (i * w)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> NatRepr n
-> NatRepr i
-> Vector (n * i) (f (BVType w))
-> Vector n (Vector i (f (BVType w)))
forall (w :: Natural) (n :: Natural) a.
(1 <= w, 1 <= n) =>
NatRepr n -> NatRepr w -> Vector (n * w) a -> Vector n (Vector w a)
split (NatRepr (n * i) -> NatRepr i -> NatRepr n
forall (n :: Natural) (m :: Natural).
(1 <= n) =>
NatRepr (m * n) -> NatRepr n -> NatRepr m
divNat (Vector (n * i) (f (BVType w)) -> NatRepr (n * i)
forall (n :: Natural) a. Vector n a -> NatRepr n
length Vector (n * i) (f (BVType w))
xs) NatRepr i
i) NatRepr i
i Vector (n * i) (f (BVType w))
xs
{-# Inline joinVecBV #-}
splitVecBV :: (IsExpr f, 1 <= i, 1 <= w) =>
Endian ->
NatRepr i ->
NatRepr w ->
Vector n (f (BVType (i * w))) -> Vector (n*i) (f (BVType w))
splitVecBV :: forall (f :: CrucibleType -> Type) (i :: Natural) (w :: Natural)
(n :: Natural).
(IsExpr f, 1 <= i, 1 <= w) =>
Endian
-> NatRepr i
-> NatRepr w
-> Vector n (f (BVType (i * w)))
-> Vector (n * i) (f (BVType w))
splitVecBV Endian
e NatRepr i
i NatRepr w
w Vector n (f (BVType (i * w)))
xs = NatRepr i
-> Vector n (Vector i (f (BVType w)))
-> Vector (n * i) (f (BVType w))
forall (w :: Natural) (n :: Natural) a.
(1 <= w) =>
NatRepr w -> Vector n (Vector w a) -> Vector (n * w) a
join NatRepr i
i (Endian
-> NatRepr i
-> NatRepr w
-> f (BVType (i * w))
-> Vector i (f (BVType w))
forall (f :: CrucibleType -> Type) (w :: Natural) (n :: Natural).
(1 <= w, 1 <= n, IsExpr f) =>
Endian
-> NatRepr n
-> NatRepr w
-> f (BVType (n * w))
-> Vector n (f (BVType w))
fromBV Endian
e NatRepr i
i NatRepr w
w (f (BVType (i * w)) -> Vector i (f (BVType w)))
-> Vector n (f (BVType (i * w)))
-> Vector n (Vector i (f (BVType w)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector n (f (BVType (i * w)))
xs)
{-# Inline splitVecBV #-}