----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.RegMap
-- Description      : Runtime representation of CFG registers
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- Register maps hold the values of registers at simulation/run time.
------------------------------------------------------------------------
{-# LANGUAGE AllowAmbiguousTypes #-} -- for @reg@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Lang.Crucible.Simulator.RegMap
  ( RegEntry(..)
  , muxRegEntry
  , RegMap(..)
  , regMapSize
  , emptyRegMap
  , reg
  , regVal
  , regVal'
  , assignReg
  , assignReg'
  , appendRegs
  , takeRegs
  , unconsReg
  , muxRegForType
  , muxReference
  , eqReference
  , pushBranchForType
  , abortBranchForType
  , pushBranchRegs
  , abortBranchRegs
  , pushBranchRegEntry
  , abortBranchRegEntry
  , mergeRegs
  , asSymExpr
  , module Lang.Crucible.Simulator.RegValue
  ) where


import qualified Data.Parameterized.Context as Ctx
import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.TraversableFC

import           What4.Interface
import           What4.WordMap

import           Lang.Crucible.CFG.Core (Reg(..))
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.RegValue
import           Lang.Crucible.Types
import           Lang.Crucible.Utils.MuxTree
import           Lang.Crucible.Backend
import           Lang.Crucible.Panic

------------------------------------------------------------------------
-- RegMap

-- | The value of a register.
data RegEntry sym tp = RegEntry { forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
regType :: !(TypeRepr tp)
                                , forall sym (tp :: CrucibleType). RegEntry sym tp -> RegValue sym tp
regValue :: !(RegValue sym tp)
                                }

-- | A set of registers in an execution frame.
newtype RegMap sym (ctx :: Ctx CrucibleType)
      = RegMap { forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
regMap :: Ctx.Assignment (RegEntry sym) ctx }

regMapSize :: RegMap sym ctx -> Ctx.Size ctx
regMapSize :: forall sym (ctx :: Ctx CrucibleType). RegMap sym ctx -> Size ctx
regMapSize (RegMap Assignment (RegEntry sym) ctx
s) = Assignment (RegEntry sym) ctx -> Size ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (RegEntry sym) ctx
s

-- | Create a new set of registers.
emptyRegMap :: RegMap sym EmptyCtx
emptyRegMap :: forall sym. RegMap sym EmptyCtx
emptyRegMap = Assignment (RegEntry sym) EmptyCtx -> RegMap sym EmptyCtx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap Assignment (RegEntry sym) EmptyCtx
forall {k} (f :: k -> Type). Assignment f EmptyCtx
Ctx.empty

assignReg :: TypeRepr tp
          -> RegValue sym tp
          -> RegMap sym ctx
          -> RegMap sym (ctx ::> tp)
assignReg :: forall (tp :: CrucibleType) sym (ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg TypeRepr tp
tp RegValue sym tp
v (RegMap Assignment (RegEntry sym) ctx
m) =  Assignment (RegEntry sym) (ctx ::> tp) -> RegMap sym (ctx ::> tp)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx
m Assignment (RegEntry sym) ctx
-> RegEntry sym tp -> Assignment (RegEntry sym) (ctx ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp RegValue sym tp
v)
{-# INLINE assignReg #-}

assignReg' :: RegEntry sym tp
           -> RegMap sym ctx
           -> RegMap sym (ctx ::> tp)
assignReg' :: forall sym (tp :: CrucibleType) (ctx :: Ctx CrucibleType).
RegEntry sym tp -> RegMap sym ctx -> RegMap sym (ctx ::> tp)
assignReg' RegEntry sym tp
v (RegMap Assignment (RegEntry sym) ctx
m) =  Assignment (RegEntry sym) (ctx ::> tp) -> RegMap sym (ctx ::> tp)
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx
m Assignment (RegEntry sym) ctx
-> RegEntry sym tp -> Assignment (RegEntry sym) (ctx ::> tp)
forall {k} (ctx' :: Ctx k) (f :: k -> Type) (ctx :: Ctx k)
       (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
Ctx.:> RegEntry sym tp
v)
{-# INLINE assignReg' #-}


appendRegs ::
  RegMap sym ctx ->
  RegMap sym ctx' ->
  RegMap sym (ctx <+> ctx')
appendRegs :: forall sym (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType).
RegMap sym ctx -> RegMap sym ctx' -> RegMap sym (ctx <+> ctx')
appendRegs (RegMap Assignment (RegEntry sym) ctx
m1) (RegMap Assignment (RegEntry sym) ctx'
m2) = Assignment (RegEntry sym) (ctx <+> ctx')
-> RegMap sym (ctx <+> ctx')
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx
m1 Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx'
-> Assignment (RegEntry sym) (ctx <+> ctx')
forall {k} (f :: k -> Type) (x :: Ctx k) (y :: Ctx k).
Assignment f x -> Assignment f y -> Assignment f (x <+> y)
Ctx.<++> Assignment (RegEntry sym) ctx'
m2)

unconsReg ::
  RegMap sym (ctx ::> tp) ->
  (RegMap sym ctx, RegEntry sym tp)
unconsReg :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym (ctx ::> tp) -> (RegMap sym ctx, RegEntry sym tp)
unconsReg (RegMap (Assignment (RegEntry sym) ctx
hd Ctx.:> RegEntry sym tp
tl)) = (Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap Assignment (RegEntry sym) ctx
Assignment (RegEntry sym) ctx
hd, RegEntry sym tp
RegEntry sym tp
tl)

takeRegs ::
  Ctx.Size ctx ->
  Ctx.Size ctx' ->
  RegMap sym (ctx <+> ctx') ->
  RegMap sym ctx
takeRegs :: forall (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType) sym.
Size ctx
-> Size ctx' -> RegMap sym (ctx <+> ctx') -> RegMap sym ctx
takeRegs Size ctx
sz Size ctx'
sz' (RegMap Assignment (RegEntry sym) (ctx <+> ctx')
m) = Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Size ctx
-> Size ctx'
-> Assignment (RegEntry sym) (ctx <+> ctx')
-> Assignment (RegEntry sym) ctx
forall {k} (f :: k -> Type) (ctx :: Ctx k) (ctx' :: Ctx k).
Size ctx
-> Size ctx' -> Assignment f (ctx <+> ctx') -> Assignment f ctx
Ctx.take Size ctx
sz Size ctx'
sz' Assignment (RegEntry sym) (ctx <+> ctx')
m)

reg :: forall n sym ctx tp. Ctx.Idx n ctx tp => RegMap sym ctx -> RegValue sym tp
reg :: forall (n :: Nat) sym (ctx :: Ctx CrucibleType)
       (tp :: CrucibleType).
Idx n ctx tp =>
RegMap sym ctx -> RegValue sym tp
reg RegMap sym ctx
m = RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
regVal RegMap sym ctx
m (Index ctx tp -> Reg ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Index ctx tp -> Reg ctx tp
Reg (forall (n :: Nat) (ctx :: Ctx CrucibleType) (r :: CrucibleType).
Idx n ctx r =>
Index ctx r
forall {k} (n :: Nat) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
Ctx.natIndex @n))

regVal :: RegMap sym ctx
       -> Reg ctx tp
       -> RegValue sym tp
regVal :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegValue sym tp
regVal (RegMap Assignment (RegEntry sym) ctx
a) Reg ctx tp
r = RegValue sym tp
v
  where RegEntry TypeRepr tp
_ RegValue sym tp
v = Assignment (RegEntry sym) ctx
a Assignment (RegEntry sym) ctx -> Index ctx tp -> RegEntry sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx tp
r

regVal' :: RegMap sym ctx
       -> Reg ctx tp
       -> RegEntry sym tp
regVal' :: forall sym (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
RegMap sym ctx -> Reg ctx tp -> RegEntry sym tp
regVal' (RegMap Assignment (RegEntry sym) ctx
a) Reg ctx tp
r = Assignment (RegEntry sym) ctx
a Assignment (RegEntry sym) ctx -> Index ctx tp -> RegEntry sym tp
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Reg ctx tp -> Index ctx tp
forall (ctx :: Ctx CrucibleType) (tp :: CrucibleType).
Reg ctx tp -> Index ctx tp
regIndex Reg ctx tp
r


muxAny :: IsSymInterface sym
       => sym
       -> IntrinsicTypes sym
       -> ValMuxFn sym AnyType
muxAny :: forall sym.
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> ValMuxFn sym AnyType
muxAny sym
s IntrinsicTypes sym
itefns Pred sym
p (AnyValue TypeRepr tp
tpx RegValue sym tp
x) (AnyValue TypeRepr tp
tpy RegValue sym tp
y)
  | Just tp :~: tp
Refl <- TypeRepr tp -> TypeRepr 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).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp
tpx TypeRepr tp
tpy =
       TypeRepr tp -> RegValue sym tp -> AnyValue sym
forall (tp :: CrucibleType) sym.
TypeRepr tp -> RegValue sym tp -> AnyValue sym
AnyValue TypeRepr tp
tpx (RegValue sym tp -> AnyValue sym)
-> IO (RegValue sym tp) -> IO (AnyValue sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns TypeRepr tp
tpx Pred sym
p RegValue sym tp
x RegValue sym tp
RegValue sym tp
y
  | Bool
otherwise = sym -> String -> IO (RegValue sym AnyType)
forall sym (m :: Type -> Type) a.
(IsExprBuilder sym, MonadIO m, HasCallStack) =>
sym -> String -> m a
throwUnsupported sym
s (String -> IO (RegValue sym AnyType))
-> String -> IO (RegValue sym AnyType)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
                      [String
"Attempted to mux ANY values of different runtime type"
                      , TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpx, TypeRepr tp -> String
forall a. Show a => a -> String
show TypeRepr tp
tpy
                      ]

muxReference ::
  IsSymInterface sym => sym -> ValMuxFn sym (ReferenceType tp)
muxReference :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> ValMuxFn sym (ReferenceType tp)
muxReference sym
s = sym
-> SymExpr sym BaseBoolType
-> MuxTree sym (RefCell tp)
-> MuxTree sym (RefCell tp)
-> IO (MuxTree sym (RefCell tp))
forall a sym.
(Ord a, IsExprBuilder sym) =>
sym
-> Pred sym -> MuxTree sym a -> MuxTree sym a -> IO (MuxTree sym a)
mergeMuxTree sym
s

eqReference ::
  IsSymInterface sym =>
  sym ->
  RegValue sym (ReferenceType tp) ->
  RegValue sym (ReferenceType tp) ->
  IO (Pred sym)
eqReference :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> RegValue sym (ReferenceType tp)
-> RegValue sym (ReferenceType tp)
-> IO (Pred sym)
eqReference sym
sym = sym
-> MuxTree sym (RefCell tp)
-> MuxTree sym (RefCell tp)
-> IO (SymExpr sym BaseBoolType)
forall a sym.
(Eq a, IsExprBuilder sym) =>
sym -> MuxTree sym a -> MuxTree sym a -> IO (Pred sym)
muxTreeEq sym
sym


{-# INLINABLE pushBranchForType #-}
pushBranchForType :: forall sym tp
               . IsSymInterface sym
              => sym
              -> IntrinsicTypes sym
              -> TypeRepr tp
              -> RegValue sym tp
              -> IO (RegValue sym tp)
pushBranchForType :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
pushBranchForType sym
s IntrinsicTypes sym
iTypes TypeRepr tp
p =
  case TypeRepr tp
p of
    IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx ->
       case SymbolRepr nm
-> IntrinsicTypes sym -> Maybe (IntrinsicMuxFn sym nm)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymbolRepr nm
nm IntrinsicTypes sym
iTypes of
         Just IntrinsicMuxFn sym nm
IntrinsicMuxFn -> sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
IntrinsicClass sym nm =>
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
pushBranchIntrinsic sym
s IntrinsicTypes sym
iTypes SymbolRepr nm
nm CtxRepr ctx
ctx
         Maybe (IntrinsicMuxFn sym nm)
Nothing -> \RegValue sym tp
_ ->
           String -> [String] -> IO (Intrinsic sym nm ctx)
forall a. HasCallStack => String -> [String] -> a
panic String
"RegMap.pushBranchForType"
              [ String
"Unknown intrinsic type:"
              , String
"*** Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymbolRepr nm -> String
forall a. Show a => a -> String
show SymbolRepr nm
nm
              ]

    TypeRepr tp
AnyRepr -> \(AnyValue TypeRepr tp
tpr RegValue sym tp
x) -> TypeRepr tp -> RegValue sym tp -> AnyValue sym
forall (tp :: CrucibleType) sym.
TypeRepr tp -> RegValue sym tp -> AnyValue sym
AnyValue TypeRepr tp
tpr (RegValue sym tp -> AnyValue sym)
-> IO (RegValue sym tp) -> IO (AnyValue sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
pushBranchForType sym
s IntrinsicTypes sym
iTypes TypeRepr tp
tpr RegValue sym tp
x

    -- All remaining types do no push branch bookkeeping
    TypeRepr tp
_ -> RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return

{-# INLINABLE abortBranchForType #-}
abortBranchForType :: forall sym tp
               . IsSymInterface sym
              => sym
              -> IntrinsicTypes sym
              -> TypeRepr tp
              -> RegValue sym tp
              -> IO (RegValue sym tp)
abortBranchForType :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
abortBranchForType sym
s IntrinsicTypes sym
iTypes TypeRepr tp
p =
  case TypeRepr tp
p of
    IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx ->
       case SymbolRepr nm
-> IntrinsicTypes sym -> Maybe (IntrinsicMuxFn sym nm)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymbolRepr nm
nm IntrinsicTypes sym
iTypes of
         Just IntrinsicMuxFn sym nm
IntrinsicMuxFn -> sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
IntrinsicClass sym nm =>
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
abortBranchIntrinsic sym
s IntrinsicTypes sym
iTypes SymbolRepr nm
nm CtxRepr ctx
ctx
         Maybe (IntrinsicMuxFn sym nm)
Nothing ->
           String
-> [String] -> Intrinsic sym nm ctx -> IO (Intrinsic sym nm ctx)
forall a. HasCallStack => String -> [String] -> a
panic String
"RegMap.abortBranchForType"
              [ String
"Unknown intrinsic type:"
              , String
"*** Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymbolRepr nm -> String
forall a. Show a => a -> String
show SymbolRepr nm
nm
              ]
    TypeRepr tp
AnyRepr -> \(AnyValue TypeRepr tp
tpr RegValue sym tp
x) ->
      TypeRepr tp -> RegValue sym tp -> AnyValue sym
forall (tp :: CrucibleType) sym.
TypeRepr tp -> RegValue sym tp -> AnyValue sym
AnyValue TypeRepr tp
tpr (RegValue sym tp -> AnyValue sym)
-> IO (RegValue sym tp) -> IO (AnyValue sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
abortBranchForType sym
s IntrinsicTypes sym
iTypes TypeRepr tp
tpr RegValue sym tp
x

    -- All remaining types do no abort branch bookkeeping
    TypeRepr tp
_ -> RegValue sym tp -> IO (RegValue sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return

{-# INLINABLE muxRegForType #-}
muxRegForType :: forall sym tp
               . IsSymInterface sym
              => sym
              -> IntrinsicTypes sym
              -> TypeRepr tp
              -> ValMuxFn sym tp
muxRegForType :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns TypeRepr tp
p =
  case TypeRepr tp
p of
     TypeRepr tp
UnitRepr          -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
NatRepr           -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
IntegerRepr       -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
RealValRepr       -> sym -> TypeRepr 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 TypeRepr tp
p
     FloatRepr FloatInfoRepr flt
_       -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
ComplexRealRepr   -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
CharRepr          -> sym -> TypeRepr 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 TypeRepr tp
p
     TypeRepr tp
BoolRepr          -> sym -> TypeRepr 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 TypeRepr tp
p
     StringRepr StringInfoRepr si
_      -> sym -> TypeRepr 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 TypeRepr tp
p
     IEEEFloatRepr FloatPrecisionRepr ps
_p  -> sym -> TypeRepr 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 TypeRepr tp
p

     TypeRepr tp
AnyRepr -> sym -> IntrinsicTypes sym -> ValMuxFn sym AnyType
forall sym.
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> ValMuxFn sym AnyType
muxAny sym
s IntrinsicTypes sym
itefns
     StructRepr  CtxRepr ctx
ctx -> (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx -> ValMuxFn sym ('StructType ctx)
forall sym (ctx :: Ctx CrucibleType).
(forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx -> ValMuxFn sym (StructType ctx)
muxStruct    (sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns) CtxRepr ctx
ctx
     VariantRepr CtxRepr ctx
ctx -> sym
-> (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx
-> ValMuxFn sym ('VariantType ctx)
forall sym (ctx :: Ctx CrucibleType).
IsExprBuilder sym =>
sym
-> (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> CtxRepr ctx
-> ValMuxFn sym (VariantType ctx)
muxVariant sym
s (sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns) CtxRepr ctx
ctx
     ReferenceRepr TypeRepr a
_x -> sym -> ValMuxFn sym ('ReferenceType a)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> ValMuxFn sym (ReferenceType tp)
muxReference sym
s
     WordMapRepr NatRepr n
w BaseTypeRepr tp1
tp -> sym
-> NatRepr n
-> BaseTypeRepr tp1
-> SymExpr sym BaseBoolType
-> WordMap sym n tp1
-> WordMap sym n tp1
-> IO (WordMap sym n tp1)
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 n
w BaseTypeRepr tp1
tp
     BVRepr NatRepr n
w ->
       case NatRepr n -> Maybe (LeqProof 1 n)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr n
w of
         Maybe (LeqProof 1 n)
Nothing -> \SymExpr sym BaseBoolType
_ RegValue sym tp
x RegValue sym tp
_ -> SymExpr sym (BaseBVType n) -> IO (SymExpr sym (BaseBVType n))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return SymExpr sym (BaseBVType n)
RegValue sym tp
x
         Just LeqProof 1 n
LeqProof -> sym
-> SymExpr sym BaseBoolType
-> SymExpr sym (BaseBVType n)
-> SymExpr sym (BaseBVType n)
-> IO (SymExpr sym (BaseBVType n))
forall (w :: Nat).
(1 <= w) =>
sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte sym
s
     FunctionHandleRepr CtxRepr ctx
_ TypeRepr ret
_ -> sym -> TypeRepr 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 TypeRepr tp
p

     MaybeRepr TypeRepr tp1
r          -> sym
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp1 -> RegValue sym tp1 -> IO (RegValue sym tp1))
-> SymExpr sym BaseBoolType
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> IO (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1))
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 (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> SymExpr sym BaseBoolType
-> RegValue sym tp1
-> RegValue sym tp1
-> IO (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns TypeRepr tp1
r)
     VectorRepr TypeRepr tp1
r         -> sym
-> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> MuxFn (SymExpr sym BaseBoolType) (Vector (RegValue sym tp1))
forall sym p e.
IsExprBuilder sym =>
sym -> MuxFn p e -> MuxFn p (Vector e)
muxVector sym
s (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns TypeRepr tp1
r)
     SequenceRepr TypeRepr tp1
_r      -> sym
-> SymExpr sym BaseBoolType
-> SymSequence sym (RegValue sym tp1)
-> SymSequence sym (RegValue sym tp1)
-> IO (SymSequence sym (RegValue sym tp1))
forall sym a.
sym
-> Pred sym
-> SymSequence sym a
-> SymSequence sym a
-> IO (SymSequence sym a)
muxSymSequence sym
s
     StringMapRepr TypeRepr tp1
r      -> sym
-> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp1)
-> MuxFn
     (SymExpr sym BaseBoolType)
     (Map Text (PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp1)))
forall sym e.
IsExprBuilder sym =>
sym
-> MuxFn (Pred sym) e
-> MuxFn (Pred sym) (Map Text (PartExpr (Pred sym) e))
muxStringMap sym
s (sym
-> IntrinsicTypes sym
-> TypeRepr tp1
-> MuxFn (SymExpr sym BaseBoolType) (RegValue sym tp1)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns TypeRepr tp1
r)
     SymbolicArrayRepr{}         -> sym
-> SymExpr sym BaseBoolType
-> SymArray sym (idx ::> tp1) t
-> SymArray sym (idx ::> tp1) t
-> IO (SymArray sym (idx ::> tp1) t)
forall sym (idx :: Ctx BaseType) (b :: BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
forall (idx :: Ctx BaseType) (b :: BaseType).
sym
-> SymExpr sym BaseBoolType
-> SymArray sym idx b
-> SymArray sym idx b
-> IO (SymArray sym idx b)
arrayIte sym
s
     SymbolicStructRepr{}        -> sym
-> SymExpr sym BaseBoolType
-> SymStruct sym ctx
-> SymStruct sym ctx
-> IO (SymStruct sym ctx)
forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym
-> Pred sym
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
forall (flds :: Ctx BaseType).
sym
-> SymExpr sym BaseBoolType
-> SymStruct sym flds
-> SymStruct sym flds
-> IO (SymStruct sym flds)
structIte sym
s
     RecursiveRepr SymbolRepr nm
nm CtxRepr ctx
ctx -> (forall (tp :: CrucibleType). TypeRepr tp -> ValMuxFn sym tp)
-> SymbolRepr nm
-> CtxRepr ctx
-> ValMuxFn sym ('RecursiveType nm ctx)
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 (sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> SymExpr sym BaseBoolType
-> RegValue sym tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
s IntrinsicTypes sym
itefns) SymbolRepr nm
nm CtxRepr ctx
ctx
     IntrinsicRepr SymbolRepr nm
nm CtxRepr ctx
ctx ->
       case SymbolRepr nm
-> IntrinsicTypes sym -> Maybe (IntrinsicMuxFn sym nm)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup SymbolRepr nm
nm IntrinsicTypes sym
itefns of
         Just IntrinsicMuxFn sym nm
IntrinsicMuxFn -> sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> SymExpr sym BaseBoolType
-> Intrinsic sym nm ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall sym (nm :: Symbol) (ctx :: Ctx CrucibleType).
IntrinsicClass sym nm =>
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> Pred sym
-> Intrinsic sym nm ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
forall (ctx :: Ctx CrucibleType).
sym
-> IntrinsicTypes sym
-> SymbolRepr nm
-> CtxRepr ctx
-> SymExpr sym BaseBoolType
-> Intrinsic sym nm ctx
-> Intrinsic sym nm ctx
-> IO (Intrinsic sym nm ctx)
muxIntrinsic sym
s IntrinsicTypes sym
itefns SymbolRepr nm
nm CtxRepr ctx
ctx
         Maybe (IntrinsicMuxFn sym nm)
Nothing -> \SymExpr sym BaseBoolType
_ RegValue sym tp
_ RegValue sym tp
_ ->
           String -> [String] -> IO (Intrinsic sym nm ctx)
forall a. HasCallStack => String -> [String] -> a
panic String
"RegMap.muxRegForType"
              [ String
"Unknown intrinsic type:"
              , String
"*** Name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymbolRepr nm -> String
forall a. Show a => a -> String
show SymbolRepr nm
nm
              ]

-- | Mux two register entries.
{-# INLINE muxRegEntry #-}
muxRegEntry :: IsSymInterface sym
             => sym
             -> IntrinsicTypes sym
             -> MuxFn (Pred sym) (RegEntry sym tp)
muxRegEntry :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym tp)
muxRegEntry sym
sym IntrinsicTypes sym
iteFns Pred sym
pp (RegEntry TypeRepr tp
rtp RegValue sym tp
x) (RegEntry TypeRepr tp
_ RegValue sym tp
y) = do
  TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
rtp (RegValue sym tp -> RegEntry sym tp)
-> IO (RegValue sym tp) -> IO (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> TypeRepr tp -> ValMuxFn sym tp
muxRegForType sym
sym IntrinsicTypes sym
iteFns TypeRepr tp
rtp Pred sym
pp RegValue sym tp
x RegValue sym tp
y

pushBranchRegEntry
             :: (IsSymInterface sym)
             => sym
             -> IntrinsicTypes sym
             -> RegEntry sym tp
             -> IO (RegEntry sym tp)
pushBranchRegEntry :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
pushBranchRegEntry sym
sym IntrinsicTypes sym
iTypes (RegEntry TypeRepr tp
tp RegValue sym tp
x) =
  TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp (RegValue sym tp -> RegEntry sym tp)
-> IO (RegValue sym tp) -> IO (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
pushBranchForType sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tp RegValue sym tp
x

abortBranchRegEntry
             :: (IsSymInterface sym)
             => sym
             -> IntrinsicTypes sym
             -> RegEntry sym tp
             -> IO (RegEntry sym tp)
abortBranchRegEntry :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
abortBranchRegEntry sym
sym IntrinsicTypes sym
iTypes (RegEntry TypeRepr tp
tp RegValue sym tp
x) =
  TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
forall sym (tp :: CrucibleType).
TypeRepr tp -> RegValue sym tp -> RegEntry sym tp
RegEntry TypeRepr tp
tp (RegValue sym tp -> RegEntry sym tp)
-> IO (RegValue sym tp) -> IO (RegEntry sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> RegValue sym tp
-> IO (RegValue sym tp)
abortBranchForType sym
sym IntrinsicTypes sym
iTypes TypeRepr tp
tp RegValue sym tp
x


{-# INLINE mergeRegs #-}
mergeRegs :: (IsSymInterface sym)
          => sym
          -> IntrinsicTypes sym
          -> MuxFn (Pred sym) (RegMap sym ctx)
mergeRegs :: forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegMap sym ctx)
mergeRegs sym
sym IntrinsicTypes sym
iTypes Pred sym
pp (RegMap Assignment (RegEntry sym) ctx
rx) (RegMap Assignment (RegEntry sym) ctx
ry) = do
  Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx -> RegMap sym ctx)
-> IO (Assignment (RegEntry sym) ctx) -> IO (RegMap sym ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType).
 RegEntry sym x -> RegEntry sym x -> IO (RegEntry sym x))
-> Assignment (RegEntry sym) ctx
-> Assignment (RegEntry sym) ctx
-> IO (Assignment (RegEntry sym) ctx)
forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (h :: k -> Type) (a :: Ctx k).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Assignment f a -> Assignment g a -> m (Assignment h a)
Ctx.zipWithM (sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym x)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegEntry sym tp)
muxRegEntry sym
sym IntrinsicTypes sym
iTypes Pred sym
pp) Assignment (RegEntry sym) ctx
rx Assignment (RegEntry sym) ctx
ry

{-# INLINE pushBranchRegs #-}
pushBranchRegs :: forall sym ctx
           . (IsSymInterface sym)
          => sym
          -> IntrinsicTypes sym
          -> RegMap sym ctx
          -> IO (RegMap sym ctx)
pushBranchRegs :: forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)
pushBranchRegs sym
sym IntrinsicTypes sym
iTypes (RegMap Assignment (RegEntry sym) ctx
rx) =
  Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx -> RegMap sym ctx)
-> IO (Assignment (RegEntry sym) ctx) -> IO (RegMap sym ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). RegEntry sym x -> IO (RegEntry sym x))
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> IO (Assignment (RegEntry sym) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC (sym -> IntrinsicTypes sym -> RegEntry sym x -> IO (RegEntry sym x)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
pushBranchRegEntry sym
sym IntrinsicTypes sym
iTypes) Assignment (RegEntry sym) ctx
rx

{-# INLINE abortBranchRegs #-}
abortBranchRegs :: forall sym ctx
           . (IsSymInterface sym)
          => sym
          -> IntrinsicTypes sym
          -> RegMap sym ctx
          -> IO (RegMap sym ctx)
abortBranchRegs :: forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> RegMap sym ctx -> IO (RegMap sym ctx)
abortBranchRegs sym
sym IntrinsicTypes sym
iTypes (RegMap Assignment (RegEntry sym) ctx
rx) =
  Assignment (RegEntry sym) ctx -> RegMap sym ctx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
RegMap (Assignment (RegEntry sym) ctx -> RegMap sym ctx)
-> IO (Assignment (RegEntry sym) ctx) -> IO (RegMap sym ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (x :: CrucibleType). RegEntry sym x -> IO (RegEntry sym x))
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> IO (Assignment (RegEntry sym) x)
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type)
       (m :: Type -> Type).
Applicative m =>
(forall (x :: CrucibleType). f x -> m (g x))
-> forall (x :: Ctx CrucibleType).
   Assignment f x -> m (Assignment g x)
traverseFC (sym -> IntrinsicTypes sym -> RegEntry sym x -> IO (RegEntry sym x)
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym -> RegEntry sym tp -> IO (RegEntry sym tp)
abortBranchRegEntry sym
sym IntrinsicTypes sym
iTypes) Assignment (RegEntry sym) ctx
rx

------------------------------------------------------------------------
-- Coerce a RegEntry to a SymExpr

asSymExpr :: RegEntry sym tp -- ^ RegEntry to examine
          -> (forall bt. tp ~ BaseToType bt => SymExpr sym bt -> a)
               -- ^ calculate final value when the register is a SymExpr
          -> a -- ^ final value to use if the register entry is not a SymExpr
          -> a
asSymExpr :: forall sym (tp :: CrucibleType) a.
RegEntry sym tp
-> (forall (bt :: BaseType).
    (tp ~ BaseToType bt) =>
    SymExpr sym bt -> a)
-> a
-> a
asSymExpr (RegEntry TypeRepr tp
tp RegValue sym tp
v) forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just a
nothing =
  case TypeRepr tp
tp of
     TypeRepr tp
IntegerRepr       -> SymExpr sym BaseIntegerType -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym BaseIntegerType
RegValue sym tp
v
     TypeRepr tp
RealValRepr       -> SymExpr sym BaseRealType -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym BaseRealType
RegValue sym tp
v
     TypeRepr tp
ComplexRealRepr   -> SymExpr sym BaseComplexType -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym BaseComplexType
RegValue sym tp
v
     TypeRepr tp
BoolRepr          -> SymExpr sym BaseBoolType -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym BaseBoolType
RegValue sym tp
v
     BVRepr NatRepr n
_w         -> SymExpr sym (BaseBVType n) -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym (BaseBVType n)
RegValue sym tp
v
     IEEEFloatRepr FloatPrecisionRepr ps
_p  -> SymExpr sym (BaseFloatType ps) -> a
forall (bt :: BaseType).
(tp ~ BaseToType bt) =>
SymExpr sym bt -> a
just SymExpr sym (BaseFloatType ps)
RegValue sym tp
v
     TypeRepr tp
_ -> a
nothing