-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.RegValue
-- Description      : Runtime representation of CFG registers
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- RegValue is a type family that defines the runtime representation
-- of crucible types.
------------------------------------------------------------------------
{-# 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

    -- * Register values
  , AnyValue(..)
  , FnVal(..)
  , fnValType
  , RolledType(..)
  , SymSequence(..)

  , VariantBranch(..)
  , injectVariant

    -- * Value mux functions
  , 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

-- | Maps register types to the runtime representation.
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))

-- | A newtype wrapper around RegValue.  This is wrapper necessary because
--   RegValue is a type family and, as such, cannot be partially applied.
newtype RegValue' sym tp = RV { forall sym (tp :: CrucibleType).
RegValue' sym tp -> RegValue sym tp
unRV :: RegValue sym tp }

------------------------------------------------------------------------
-- FnVal

-- | Represents a function closure.
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

-- | Extract the runtime representation of the type of the given 'FnVal'
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

-- | Version of 'MuxFn' specialized to 'RegValue'
type ValMuxFn sym tp = MuxFn (Pred sym) (RegValue sym tp)

------------------------------------------------------------------------
-- CanMux

-- | A class for 'CrucibleType's that have a
--   mux function.
class CanMux sym (tp :: CrucibleType) where
   muxReg :: sym
          -> p tp          -- ^ Unused type to identify what is being merged.
          -> ValMuxFn sym tp

-- | Merge function that checks if two values are equal, and
-- fails if they are not.
{-# 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
"."

------------------------------------------------------------------------
-- RegValue AnyType instance

data AnyValue sym where
  AnyValue :: TypeRepr tp -> RegValue sym tp -> AnyValue sym

------------------------------------------------------------------------
-- RegValue () instance

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

------------------------------------------------------------------------
-- RegValue instance for base types

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

------------------------------------------------------------------------
-- RegValue Vector instance

{-# 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))

------------------------------------------------------------------------
-- RegValue WordMap instance

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

------------------------------------------------------------------------
-- RegValue MatlabChar instance

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"

------------------------------------------------------------------------
-- RegValue Maybe instance

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

------------------------------------------------------------------------
-- RegValue FunctionHandleType instance

-- TODO: Figure out how to actually compare these.
{-# 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

------------------------------------------------------------------------
-- RegValue IdentValueMap instance

-- | Merge to string maps together.
{-# 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)

------------------------------------------------------------------------
-- RegValue Recursive instance

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)

------------------------------------------------------------------------
-- RegValue Struct instance

{-# 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)

------------------------------------------------------------------------
-- RegValue Variant instance

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) }

-- | Construct a 'VariantType' value by identifying which branch of
--   the variant to construct, and providing a value of the correct type.
injectVariant ::
  IsExprBuilder sym =>
  sym {- ^ symbolic backend -} ->
  CtxRepr ctx {- ^ Types of the variant branches -} ->
  Ctx.Index ctx tp {- ^ Which branch -} ->
  RegValue sym tp  {- ^ The value to inject -} ->
  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))