{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.RegValue
( RegValue
, CanMux(..)
, RegValue'(..)
, MuxFn
, AnyValue(..)
, FnVal(..)
, fnValType
, RolledType(..)
, SymSequence(..)
, VariantBranch(..)
, injectVariant
, ValMuxFn
, eqMergeFn
, mergePartExpr
, muxRecursive
, muxStringMap
, muxStruct
, muxVariant
, muxVector
, muxSymSequence
, muxHandle
) where
import Control.Monad
import Control.Monad.Trans.Class
import Data.Kind
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Proxy
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Vector as V
import Data.Word
import GHC.TypeNats (KnownNat)
import qualified Data.Parameterized.Context as Ctx
import What4.FunctionName
import What4.Interface
import What4.InterpretedFloatingPoint
import What4.Partial
import What4.WordMap
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Simulator.Intrinsics
import Lang.Crucible.Simulator.SymSequence
import Lang.Crucible.Types
import Lang.Crucible.Utils.MuxTree
import Lang.Crucible.Backend
type MuxFn p v = p -> v -> v -> IO v
type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where
RegValue sym (BaseToType bt) = SymExpr sym bt
RegValue sym (FloatType fi) = SymInterpretedFloat sym fi
RegValue sym AnyType = AnyValue sym
RegValue sym UnitType = ()
RegValue sym NatType = SymNat sym
RegValue sym CharType = Word16
RegValue sym (FunctionHandleType a r) = FnVal sym a r
RegValue sym (MaybeType tp) = PartExpr (Pred sym) (RegValue sym tp)
RegValue sym (VectorType tp) = V.Vector (RegValue sym tp)
RegValue sym (SequenceType tp) = SymSequence sym (RegValue sym tp)
RegValue sym (StructType ctx) = Ctx.Assignment (RegValue' sym) ctx
RegValue sym (VariantType ctx) = Ctx.Assignment (VariantBranch sym) ctx
RegValue sym (ReferenceType tp) = MuxTree sym (RefCell tp)
RegValue sym (WordMapType w tp) = WordMap sym w tp
RegValue sym (RecursiveType nm ctx) = RolledType sym nm ctx
RegValue sym (IntrinsicType nm ctx) = Intrinsic sym nm ctx
RegValue sym (StringMapType tp) = Map Text (PartExpr (Pred sym) (RegValue sym tp))
newtype RegValue' sym tp = RV { forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV :: RegValue sym tp }
data FnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where
ClosureFnVal ::
!(FnVal sym (args ::> tp) ret) ->
!(TypeRepr tp) ->
!(RegValue sym tp) ->
FnVal sym args ret
VarargsFnVal ::
!(FnHandle (args ::> VectorType AnyType) ret) ->
!(CtxRepr addlArgs) ->
FnVal sym (args <+> addlArgs) ret
HandleFnVal ::
!(FnHandle a r) ->
FnVal sym a r
closureFunctionName :: FnVal sym args res -> FunctionName
closureFunctionName :: forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> FunctionName
closureFunctionName (ClosureFnVal FnVal sym (args ::> tp) res
c TypeRepr tp
_ RegValue sym tp
_) = FnVal sym (args ::> tp) res -> FunctionName
forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> FunctionName
closureFunctionName FnVal sym (args ::> tp) res
c
closureFunctionName (HandleFnVal FnHandle args res
h) = FnHandle args res -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args res
h
closureFunctionName (VarargsFnVal FnHandle (args ::> VectorType AnyType) res
h CtxRepr addlArgs
_) = FnHandle (args ::> VectorType AnyType) res -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle (args ::> VectorType AnyType) res
h
fnValType :: FnVal sym args res -> TypeRepr (FunctionHandleType args res)
fnValType :: forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> TypeRepr (FunctionHandleType args res)
fnValType (HandleFnVal FnHandle args res
h) = CtxRepr args
-> TypeRepr res -> TypeRepr ('FunctionHandleType args res)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr (FnHandle args res -> CtxRepr args
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle args res
h) (FnHandle args res -> TypeRepr res
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle args res
h)
fnValType (VarargsFnVal FnHandle (args ::> VectorType AnyType) res
h CtxRepr addlArgs
addlArgs) =
case FnHandle (args ::> VectorType AnyType) res
-> CtxRepr (args ::> VectorType AnyType)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> CtxRepr args
handleArgTypes FnHandle (args ::> VectorType AnyType) res
h of
Assignment TypeRepr ctx
args Ctx.:> TypeRepr tp
_ -> CtxRepr args
-> TypeRepr res -> TypeRepr ('FunctionHandleType args res)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr (Assignment TypeRepr ctx
args Assignment TypeRepr ctx
-> CtxRepr addlArgs -> Assignment TypeRepr (ctx <+> addlArgs)
forall {k} (f :: k -> Type) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
Ctx.<++> CtxRepr addlArgs
addlArgs) (FnHandle (args ::> VectorType AnyType) res -> TypeRepr res
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> TypeRepr ret
handleReturnType FnHandle (args ::> VectorType AnyType) res
h)
fnValType (ClosureFnVal FnVal sym (args ::> tp) res
fn TypeRepr tp
_ RegValue sym tp
_) =
case FnVal sym (args ::> tp) res
-> TypeRepr (FunctionHandleType (args ::> tp) res)
forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> TypeRepr (FunctionHandleType args res)
fnValType FnVal sym (args ::> tp) res
fn of
FunctionHandleRepr CtxRepr ctx
allArgs TypeRepr ret
r ->
case CtxRepr ctx
allArgs of
Assignment TypeRepr ctx
args Ctx.:> TypeRepr tp
_ -> CtxRepr args
-> TypeRepr res -> TypeRepr ('FunctionHandleType args res)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
FunctionHandleRepr CtxRepr args
Assignment TypeRepr ctx
args TypeRepr res
TypeRepr ret
r
instance Show (FnVal sym a r) where
show :: FnVal sym a r -> String
show = FunctionName -> String
forall a. Show a => a -> String
show (FunctionName -> String)
-> (FnVal sym a r -> FunctionName) -> FnVal sym a r -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FnVal sym a r -> FunctionName
forall sym (args :: Ctx CrucibleType) (res :: CrucibleType).
FnVal sym args res -> FunctionName
closureFunctionName
type ValMuxFn sym tp = MuxFn (Pred sym) (RegValue sym tp)
class CanMux sym (tp :: CrucibleType) where
muxReg :: sym
-> p tp
-> ValMuxFn sym tp
{-# INLINE eqMergeFn #-}
eqMergeFn :: (IsExprBuilder sym, Eq v) => sym -> String -> MuxFn p v
eqMergeFn :: forall sym v p.
(IsExprBuilder sym, Eq v) =>
sym -> String -> MuxFn p v
eqMergeFn sym
sym String
nm = \p
_ v
x v
y ->
if v
x v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
y then
v -> IO v
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return v
x
else
sym -> String -> IO v
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m, HasCallStack) =>
sym -> String -> m a
throwUnsupported sym
sym (String -> IO v) -> String -> IO v
forall a b. (a -> b) -> a -> b
$ String
"Cannot merge dissimilar " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
data AnyValue sym where
AnyValue :: TypeRepr tp -> RegValue sym tp -> AnyValue sym
instance CanMux sym UnitType where
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p UnitType -> ValMuxFn sym UnitType
muxReg sym
_ = \p UnitType
_ Pred sym
_ RegValue sym UnitType
x RegValue sym UnitType
_y -> () -> IO ()
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
RegValue sym UnitType
x
instance IsExprBuilder sym => CanMux sym BoolType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p BoolType -> ValMuxFn sym BoolType
muxReg sym
s = ValMuxFn sym BoolType -> p BoolType -> ValMuxFn sym BoolType
forall a b. a -> b -> a
const (ValMuxFn sym BoolType -> p BoolType -> ValMuxFn sym BoolType)
-> ValMuxFn sym BoolType -> p BoolType -> ValMuxFn sym BoolType
forall a b. (a -> b) -> a -> b
$ sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred sym
s
instance IsExprBuilder sym => CanMux sym NatType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p NatType -> ValMuxFn sym NatType
muxReg sym
s = \p NatType
_ -> sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymNat sym -> SymNat sym -> IO (SymNat sym)
natIte sym
s
instance IsExprBuilder sym => CanMux sym IntegerType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p IntegerType -> ValMuxFn sym IntegerType
muxReg sym
s = \p IntegerType
_ -> sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym
-> Pred sym
-> SymInteger sym
-> SymInteger sym
-> IO (SymInteger sym)
intIte sym
s
instance IsExprBuilder sym => CanMux sym RealValType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p RealValType -> ValMuxFn sym RealValType
muxReg sym
s = \p RealValType
_ -> sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymReal sym -> SymReal sym -> IO (SymReal sym)
realIte sym
s
instance IsInterpretedFloatExprBuilder sym => CanMux sym (FloatType fi) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (FloatType fi) -> ValMuxFn sym (FloatType fi)
muxReg sym
s = \p (FloatType fi)
_ -> forall sym (fi :: FloatInfo).
IsInterpretedFloatExprBuilder sym =>
sym
-> Pred sym
-> SymInterpretedFloat sym fi
-> SymInterpretedFloat sym fi
-> IO (SymInterpretedFloat sym fi)
iFloatIte @sym @fi sym
s
instance IsExprBuilder sym => CanMux sym ComplexRealType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p ComplexRealType -> ValMuxFn sym ComplexRealType
muxReg sym
s = \p ComplexRealType
_ -> sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SymCplx sym -> SymCplx sym -> IO (SymCplx sym)
cplxIte sym
s
instance IsExprBuilder sym => CanMux sym (StringType si) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (StringType si) -> ValMuxFn sym (StringType si)
muxReg sym
s = \p (StringType si)
_ -> sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
forall sym (si :: StringInfo).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
forall (si :: StringInfo).
sym
-> Pred sym
-> SymString sym si
-> SymString sym si
-> IO (SymString sym si)
stringIte sym
s
instance IsExprBuilder sym => CanMux sym (IEEEFloatType fpp) where
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (IEEEFloatType fpp) -> ValMuxFn sym (IEEEFloatType fpp)
muxReg sym
s = \p (IEEEFloatType fpp)
_ -> sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
forall sym (fpp :: FloatPrecision).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
forall (fpp :: FloatPrecision).
sym
-> Pred sym
-> SymFloat sym fpp
-> SymFloat sym fpp
-> IO (SymFloat sym fpp)
floatIte sym
s
{-# INLINE muxVector #-}
muxVector :: IsExprBuilder sym =>
sym -> MuxFn p e -> MuxFn p (V.Vector e)
muxVector :: forall sym p e.
IsExprBuilder sym =>
sym -> MuxFn p e -> MuxFn p (Vector e)
muxVector sym
sym MuxFn p e
f p
p Vector e
x Vector e
y
| Vector e -> Int
forall a. Vector a -> Int
V.length Vector e
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector e -> Int
forall a. Vector a -> Int
V.length Vector e
y = (e -> e -> IO e) -> Vector e -> Vector e -> IO (Vector e)
forall (m :: Type -> Type) a b c.
Monad m =>
(a -> b -> m c) -> Vector a -> Vector b -> m (Vector c)
V.zipWithM (MuxFn p e
f p
p) Vector e
x Vector e
y
| Bool
otherwise =
sym -> String -> IO (Vector e)
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m, HasCallStack) =>
sym -> String -> m a
throwUnsupported sym
sym String
"Cannot merge vectors with different dimensions."
instance (IsSymInterface sym, CanMux sym tp) => CanMux sym (VectorType tp) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (VectorType tp) -> ValMuxFn sym (VectorType tp)
muxReg sym
s p (VectorType tp)
_ = sym
-> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp)
-> MuxFn (SymExpr sym BaseBoolType) (Vector (RegValue sym tp))
forall sym p e.
IsExprBuilder sym =>
sym -> MuxFn p e -> MuxFn p (Vector e)
muxVector sym
s (sym
-> Proxy tp -> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp)
forall sym (tp :: CrucibleType) (p :: CrucibleType -> Type).
CanMux sym tp =>
sym -> p tp -> ValMuxFn sym tp
forall (p :: CrucibleType -> Type).
sym -> p tp -> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp)
muxReg sym
s (Proxy tp
forall {k} (t :: k). Proxy t
Proxy :: Proxy tp))
instance (IsExprBuilder sym, KnownNat w, KnownRepr BaseTypeRepr tp)
=> CanMux sym (WordMapType w tp) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (WordMapType w tp) -> ValMuxFn sym (WordMapType w tp)
muxReg sym
s p (WordMapType w tp)
_ Pred sym
p = sym
-> NatRepr w
-> BaseTypeRepr tp
-> Pred sym
-> WordMap sym w tp
-> WordMap sym w tp
-> IO (WordMap sym w tp)
forall sym (w :: Nat) (a :: BaseType).
IsExprBuilder sym =>
sym
-> NatRepr w
-> BaseTypeRepr a
-> Pred sym
-> WordMap sym w a
-> WordMap sym w a
-> IO (WordMap sym w a)
muxWordMap sym
s NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat BaseTypeRepr tp
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr Pred sym
p
instance IsSymInterface sym => CanMux sym CharType where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p CharType -> ValMuxFn sym CharType
muxReg sym
s = \p CharType
_ -> sym -> String -> MuxFn (SymExpr sym BaseBoolType) Word16
forall sym v p.
(IsExprBuilder sym, Eq v) =>
sym -> String -> MuxFn p v
eqMergeFn sym
s String
"characters"
mergePartExpr :: IsExprBuilder sym
=> sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr :: forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
sym Pred sym -> v -> v -> IO v
fn = sym
-> (Pred sym -> v -> v -> PartialT sym IO v)
-> Pred sym
-> PartialWithErr () (Pred sym) v
-> PartialWithErr () (Pred sym) v
-> IO (PartialWithErr () (Pred sym) v)
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m) =>
sym
-> (Pred sym -> a -> a -> PartialT sym m a)
-> Pred sym
-> PartExpr (Pred sym) a
-> PartExpr (Pred sym) a
-> m (PartExpr (Pred sym) a)
mergePartial sym
sym (\Pred sym
c v
a v
b -> IO v -> PartialT sym IO v
forall (m :: Type -> Type) a. Monad m => m a -> PartialT sym m a
forall (t :: (Type -> Type) -> Type -> Type) (m :: Type -> Type) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Pred sym -> v -> v -> IO v
fn Pred sym
c v
a v
b))
instance (IsExprBuilder sym, CanMux sym tp) => CanMux sym (MaybeType tp) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym -> p (MaybeType tp) -> ValMuxFn sym (MaybeType tp)
muxReg sym
s = \p (MaybeType tp)
_ -> do
let f :: ValMuxFn sym tp
f = sym -> Proxy tp -> ValMuxFn sym tp
forall sym (tp :: CrucibleType) (p :: CrucibleType -> Type).
CanMux sym tp =>
sym -> p tp -> ValMuxFn sym tp
forall (p :: CrucibleType -> Type). sym -> p tp -> ValMuxFn sym tp
muxReg sym
s (Proxy tp
forall {k} (t :: k). Proxy t
Proxy :: Proxy tp)
in sym
-> ValMuxFn sym tp
-> Pred sym
-> PartExpr (Pred sym) (RegValue sym tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> IO (PartExpr (Pred sym) (RegValue sym tp))
forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
s ValMuxFn sym tp
f
{-# INLINE muxHandle #-}
muxHandle :: IsExpr (SymExpr sym)
=> sym
-> Pred sym
-> FnVal sym a r
-> FnVal sym a r
-> IO (FnVal sym a r)
muxHandle :: forall sym (a :: Ctx CrucibleType) (r :: CrucibleType).
IsExpr (SymExpr sym) =>
sym
-> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)
muxHandle sym
_ Pred sym
c FnVal sym a r
x FnVal sym a r
y
| Just Bool
b <- Pred sym -> Maybe Bool
forall (e :: BaseType -> Type).
IsExpr e =>
e BaseBoolType -> Maybe Bool
asConstantPred Pred sym
c = FnVal sym a r -> IO (FnVal sym a r)
forall a. a -> IO a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (FnVal sym a r -> IO (FnVal sym a r))
-> FnVal sym a r -> IO (FnVal sym a r)
forall a b. (a -> b) -> a -> b
$! if Bool
b then FnVal sym a r
x else FnVal sym a r
y
| Bool
otherwise = FnVal sym a r -> IO (FnVal sym a r)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return FnVal sym a r
x
instance IsExprBuilder sym => CanMux sym (FunctionHandleType a r) where
{-# INLINE muxReg #-}
muxReg :: forall (p :: CrucibleType -> Type).
sym
-> p (FunctionHandleType a r)
-> ValMuxFn sym (FunctionHandleType a r)
muxReg sym
s = \p (FunctionHandleType a r)
_ Pred sym
c RegValue sym (FunctionHandleType a r)
x RegValue sym (FunctionHandleType a r)
y -> do
sym
-> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)
forall sym (a :: Ctx CrucibleType) (r :: CrucibleType).
IsExpr (SymExpr sym) =>
sym
-> Pred sym -> FnVal sym a r -> FnVal sym a r -> IO (FnVal sym a r)
muxHandle sym
s Pred sym
c FnVal sym a r
RegValue sym (FunctionHandleType a r)
x FnVal sym a r
RegValue sym (FunctionHandleType a r)
y
{-# INLINE muxStringMap #-}
muxStringMap :: IsExprBuilder sym
=> sym
-> MuxFn (Pred sym) e
-> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e))
muxStringMap :: forall sym e.
IsExprBuilder sym =>
sym
-> MuxFn (Pred sym) e
-> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e))
muxStringMap sym
sym = \MuxFn (Pred sym) e
f Pred sym
c Map Text (PartExpr (Pred sym) e)
x Map Text (PartExpr (Pred sym) e)
y -> do
let keys :: [Text]
keys = Set Text -> [Text]
forall a. Set a -> [a]
Set.toList (Set Text -> [Text]) -> Set Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Set Text -> Set Text -> Set Text
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map Text (PartExpr (Pred sym) e) -> Set Text
forall k a. Map k a -> Set k
Map.keysSet Map Text (PartExpr (Pred sym) e)
x) (Map Text (PartExpr (Pred sym) e) -> Set Text
forall k a. Map k a -> Set k
Map.keysSet Map Text (PartExpr (Pred sym) e)
y)
([(Text, PartExpr (Pred sym) e)]
-> Map Text (PartExpr (Pred sym) e))
-> IO [(Text, PartExpr (Pred sym) e)]
-> IO (Map Text (PartExpr (Pred sym) e))
forall a b. (a -> b) -> IO a -> IO b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Text, PartExpr (Pred sym) e)] -> Map Text (PartExpr (Pred sym) e)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (IO [(Text, PartExpr (Pred sym) e)]
-> IO (Map Text (PartExpr (Pred sym) e)))
-> IO [(Text, PartExpr (Pred sym) e)]
-> IO (Map Text (PartExpr (Pred sym) e))
forall a b. (a -> b) -> a -> b
$ [Text]
-> (Text -> IO (Text, PartExpr (Pred sym) e))
-> IO [(Text, PartExpr (Pred sym) e)]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Text]
keys ((Text -> IO (Text, PartExpr (Pred sym) e))
-> IO [(Text, PartExpr (Pred sym) e)])
-> (Text -> IO (Text, PartExpr (Pred sym) e))
-> IO [(Text, PartExpr (Pred sym) e)]
forall a b. (a -> b) -> a -> b
$ \Text
k -> do
let vx :: PartExpr (Pred sym) e
vx = Maybe (PartExpr (Pred sym) e) -> PartExpr (Pred sym) e
forall p v. Maybe (PartExpr p v) -> PartExpr p v
joinMaybePE (Text
-> Map Text (PartExpr (Pred sym) e)
-> Maybe (PartExpr (Pred sym) e)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
k Map Text (PartExpr (Pred sym) e)
x)
let vy :: PartExpr (Pred sym) e
vy = Maybe (PartExpr (Pred sym) e) -> PartExpr (Pred sym) e
forall p v. Maybe (PartExpr p v) -> PartExpr p v
joinMaybePE (Text
-> Map Text (PartExpr (Pred sym) e)
-> Maybe (PartExpr (Pred sym) e)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
k Map Text (PartExpr (Pred sym) e)
y)
PartExpr (Pred sym) e
r <- sym
-> MuxFn (Pred sym) e
-> Pred sym
-> PartExpr (Pred sym) e
-> PartExpr (Pred sym) e
-> IO (PartExpr (Pred sym) e)
forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
sym MuxFn (Pred sym) e
f Pred sym
c PartExpr (Pred sym) e
vx PartExpr (Pred sym) e
vy
(Text, PartExpr (Pred sym) e) -> IO (Text, PartExpr (Pred sym) e)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text
k,PartExpr (Pred sym) e
r)
newtype RolledType sym nm ctx = RolledType { forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
unroll :: RegValue sym (UnrollType nm ctx) }
{-# INLINE muxRecursive #-}
muxRecursive
:: IsRecursiveType nm
=> (forall tp. TypeRepr tp -> ValMuxFn sym tp)
-> SymbolRepr nm
-> CtxRepr ctx
-> ValMuxFn sym (RecursiveType nm ctx)
muxRecursive :: forall (nm :: Symbol) sym (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
(forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> SymbolRepr nm
-> CtxRepr ctx
-> ValMuxFn sym (RecursiveType nm ctx)
muxRecursive forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf = \SymbolRepr nm
nm CtxRepr ctx
ctx Pred sym
p RegValue sym (RecursiveType nm ctx)
x RegValue sym (RecursiveType nm ctx)
y -> do
RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx
RolledType (RegValue sym (UnrollType nm ctx) -> RolledType sym nm ctx)
-> IO (RegValue sym (UnrollType nm ctx))
-> IO (RolledType sym nm ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRepr (UnrollType nm ctx) -> ValMuxFn sym (UnrollType nm ctx)
forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf (SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (nm :: Symbol) (ctx :: Ctx CrucibleType).
IsRecursiveType nm =>
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
forall (ctx :: Ctx CrucibleType).
SymbolRepr nm -> CtxRepr ctx -> TypeRepr (UnrollType nm ctx)
unrollType SymbolRepr nm
nm CtxRepr ctx
ctx) Pred sym
p (RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
unroll RolledType sym nm ctx
RegValue sym (RecursiveType nm ctx)
x) (RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
RolledType sym nm ctx -> RegValue sym (UnrollType nm ctx)
unroll RolledType sym nm ctx
RegValue sym (RecursiveType nm ctx)
y)
{-# INLINE muxStruct #-}
muxStruct
:: (forall tp. TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx
-> ValMuxFn sym (StructType ctx)
muxStruct :: forall sym (ctx :: Ctx CrucibleType).
(forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx -> ValMuxFn sym (StructType ctx)
muxStruct forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf CtxRepr ctx
ctx = \Pred sym
p RegValue sym (StructType ctx)
x RegValue sym (StructType ctx)
y ->
Size ctx
-> (forall {tp :: CrucibleType}.
Index ctx tp -> IO (RegValue' sym tp))
-> IO (Assignment (RegValue' sym) ctx)
forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
Ctx.generateM (CtxRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr ctx
ctx) ((forall {tp :: CrucibleType}.
Index ctx tp -> IO (RegValue' sym tp))
-> IO (Assignment (RegValue' sym) ctx))
-> (forall {tp :: CrucibleType}.
Index ctx tp -> IO (RegValue' sym tp))
-> IO (Assignment (RegValue' sym) ctx)
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i -> do
RegValue sym tp -> RegValue' sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
RV (RegValue sym tp -> RegValue' sym tp)
-> IO (RegValue sym tp) -> IO (RegValue' sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeRepr tp -> ValMuxFn sym tp
forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf (CtxRepr ctx
ctx CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) Pred sym
p (RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ Assignment (RegValue' sym) ctx
RegValue sym (StructType ctx)
x Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i) (RegValue' sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV (RegValue' sym tp -> RegValue sym tp)
-> RegValue' sym tp -> RegValue sym tp
forall a b. (a -> b) -> a -> b
$ Assignment (RegValue' sym) ctx
RegValue sym (StructType ctx)
y Assignment (RegValue' sym) ctx -> Index ctx tp -> RegValue' sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i)
newtype VariantBranch sym tp = VB { forall sym (tp :: CrucibleType).
VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
unVB :: PartExpr (Pred sym) (RegValue sym tp) }
injectVariant ::
IsExprBuilder sym =>
sym ->
CtxRepr ctx ->
Ctx.Index ctx tp ->
RegValue sym tp ->
RegValue sym (VariantType ctx)
injectVariant :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> CtxRepr ctx
-> Index ctx tp
-> RegValue sym tp
-> RegValue sym (VariantType ctx)
injectVariant sym
sym CtxRepr ctx
ctxRepr Index ctx tp
idx RegValue sym tp
val =
Size ctx
-> (forall (tp :: CrucibleType).
Index ctx tp -> VariantBranch sym tp)
-> Assignment (VariantBranch sym) ctx
forall {k} (ctx :: Ctx k) (f :: k -> Type).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate (CtxRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr ctx
ctxRepr) ((forall (tp :: CrucibleType).
Index ctx tp -> VariantBranch sym tp)
-> Assignment (VariantBranch sym) ctx)
-> (forall (tp :: CrucibleType).
Index ctx tp -> VariantBranch sym tp)
-> Assignment (VariantBranch sym) ctx
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
j ->
case Index ctx tp -> Index ctx tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
Index ctx a -> Index ctx b -> Maybe (a :~: b)
testEquality Index ctx tp
j Index ctx tp
idx of
Just tp :~: tp
Refl -> PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
VB (Pred sym
-> RegValue sym tp -> PartExpr (Pred sym) (RegValue sym tp)
forall p v. p -> v -> PartExpr p v
PE (sym -> Pred sym
forall sym. IsExprBuilder sym => sym -> Pred sym
truePred sym
sym) RegValue sym tp
val)
Maybe (tp :~: tp)
Nothing -> PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
VB PartExpr (Pred sym) (RegValue sym tp)
forall p v. PartExpr p v
Unassigned
{-# INLINE muxVariant #-}
muxVariant
:: IsExprBuilder sym
=> sym
-> (forall tp. TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx
-> ValMuxFn sym (VariantType ctx)
muxVariant :: forall sym (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx
-> ValMuxFn sym (VariantType ctx)
muxVariant sym
sym forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf CtxRepr ctx
ctx = \Pred sym
p RegValue sym (VariantType ctx)
x RegValue sym (VariantType ctx)
y ->
Size ctx
-> (forall {tp :: CrucibleType}.
Index ctx tp -> IO (VariantBranch sym tp))
-> IO (Assignment (VariantBranch sym) ctx)
forall {k} (m :: Type -> Type) (ctx :: Ctx k) (f :: k -> Type).
Applicative m =>
Size ctx
-> (forall (tp :: k). Index ctx tp -> m (f tp))
-> m (Assignment f ctx)
Ctx.generateM (CtxRepr ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size CtxRepr ctx
ctx) ((forall {tp :: CrucibleType}.
Index ctx tp -> IO (VariantBranch sym tp))
-> IO (Assignment (VariantBranch sym) ctx))
-> (forall {tp :: CrucibleType}.
Index ctx tp -> IO (VariantBranch sym tp))
-> IO (Assignment (VariantBranch sym) ctx)
forall a b. (a -> b) -> a -> b
$ \Index ctx tp
i ->
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp
VB (PartExpr (Pred sym) (RegValue sym tp) -> VariantBranch sym tp)
-> IO (PartExpr (Pred sym) (RegValue sym tp))
-> IO (VariantBranch sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> (Pred sym
-> RegValue sym tp -> RegValue sym tp -> IO (RegValue sym tp))
-> Pred sym
-> PartExpr (Pred sym) (RegValue sym tp)
-> PartExpr (Pred sym) (RegValue sym tp)
-> IO (PartExpr (Pred sym) (RegValue sym tp))
forall sym v.
IsExprBuilder sym =>
sym
-> (Pred sym -> v -> v -> IO v)
-> Pred sym
-> PartExpr (Pred sym) v
-> PartExpr (Pred sym) v
-> IO (PartExpr (Pred sym) v)
mergePartExpr sym
sym
(TypeRepr tp
-> Pred sym
-> RegValue sym tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp
recf (CtxRepr ctx
ctx CtxRepr ctx -> Index ctx tp -> TypeRepr tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i))
Pred sym
p
(VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
forall sym (tp :: CrucibleType).
VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
unVB (Assignment (VariantBranch sym) ctx
RegValue sym (VariantType ctx)
x Assignment (VariantBranch sym) ctx
-> Index ctx tp -> VariantBranch sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i))
(VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
forall sym (tp :: CrucibleType).
VariantBranch sym tp -> PartExpr (Pred sym) (RegValue sym tp)
unVB (Assignment (VariantBranch sym) ctx
RegValue sym (VariantType ctx)
y Assignment (VariantBranch sym) ctx
-> Index ctx tp -> VariantBranch sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index ctx tp
i))