{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Lang.Crucible.Simulator.GlobalState
  ( SymGlobalState
  , emptyGlobals
  , GlobalEntry(..)
  , insertGlobal
  , lookupGlobal
  , insertRef
  , lookupRef
  , dropRef
  , updateRef
  , globalPushBranch
  , globalAbortBranch
  , globalMuxFn
  ) where

import           Control.Applicative ((<|>))
import           Control.Monad.Trans.Class (lift)
import           Data.Functor.Identity
import           Data.Kind

import qualified Data.Parameterized.Map as MapF
import           Data.Parameterized.TraversableF

import           What4.Interface
import           What4.Partial
import           What4.ProgramLoc

import           Lang.Crucible.CFG.Core
import           Lang.Crucible.FunctionHandle
import           Lang.Crucible.Simulator.Intrinsics
import           Lang.Crucible.Simulator.RegMap
import           Lang.Crucible.Backend
import           Lang.Crucible.Panic(panic)

-- | As a map element, type @GlobalEntry sym tp@ models the contents
-- of a 'GlobalVar', which is always defined.
newtype GlobalEntry (sym :: Type) (tp :: CrucibleType) =
  GlobalEntry { forall sym (tp :: CrucibleType).
GlobalEntry sym tp -> RegValue sym tp
globalEntryValue :: RegValue sym tp }

-- | Type @RefCellContents sym tp@ models the contents of a @RefCell@,
-- which holds a partial value. A @RefCell@ not found in the map is
-- considered to represent the 'Unassigned' value.
data RefCellContents (sym :: Type) (tp :: CrucibleType)
  = RefCellContents !(Pred sym) !(RegValue sym tp)

-- | Type @RefCellUpdate sym tp@ models an update to the contents of a
-- @RefCell@. The value @RefCellUpdate Unassigned@ represents the
-- deletion of a @RefCell@.
newtype RefCellUpdate (sym :: Type) (tp :: CrucibleType) =
  RefCellUpdate (PartExpr (Pred sym) (RegValue sym tp))

------------------------------------------------------------------------
-- GlobalTable

data GlobalTable f g =
  GlobalTable
  { forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF GlobalVar f
globalVars :: !(MapF.MapF GlobalVar f)
  , forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF RefCell g
globalRefs :: !(MapF.MapF RefCell g)
  }

updateGlobalVars ::
  (MapF.MapF GlobalVar v -> MapF.MapF GlobalVar v) ->
  GlobalTable v r -> GlobalTable v r
updateGlobalVars :: forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
(MapF GlobalVar v -> MapF GlobalVar v)
-> GlobalTable v r -> GlobalTable v r
updateGlobalVars MapF GlobalVar v -> MapF GlobalVar v
f (GlobalTable MapF GlobalVar v
vs MapF RefCell r
rs) = MapF GlobalVar v -> MapF RefCell r -> GlobalTable v r
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable (MapF GlobalVar v -> MapF GlobalVar v
f MapF GlobalVar v
vs) MapF RefCell r
rs

updateGlobalRefs ::
  (MapF.MapF RefCell r -> MapF.MapF RefCell r) ->
  GlobalTable v r -> GlobalTable v r
updateGlobalRefs :: forall (r :: CrucibleType -> Type) (v :: CrucibleType -> Type).
(MapF RefCell r -> MapF RefCell r)
-> GlobalTable v r -> GlobalTable v r
updateGlobalRefs MapF RefCell r -> MapF RefCell r
f (GlobalTable MapF GlobalVar v
vs MapF RefCell r
rs) = MapF GlobalVar v -> MapF RefCell r -> GlobalTable v r
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar v
vs (MapF RefCell r -> MapF RefCell r
f MapF RefCell r
rs)

-- | The empty set of global variable updates.
emptyGlobalTable :: GlobalTable v r
emptyGlobalTable :: forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r
emptyGlobalTable = MapF GlobalVar v -> MapF RefCell r -> GlobalTable v r
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar v
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty MapF RefCell r
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty

-- | Take the union of two sets of updates, preferring elements from
-- the first set when duplicate keys are encountered.
mergeGlobalTable :: GlobalTable v r -> GlobalTable v r -> GlobalTable v r
mergeGlobalTable :: forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r -> GlobalTable v r -> GlobalTable v r
mergeGlobalTable (GlobalTable MapF GlobalVar v
vs1 MapF RefCell r
rs1) (GlobalTable MapF GlobalVar v
vs2 MapF RefCell r
rs2) =
  MapF GlobalVar v -> MapF RefCell r -> GlobalTable v r
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable (MapF GlobalVar v -> MapF GlobalVar v -> MapF GlobalVar v
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union MapF GlobalVar v
vs1 MapF GlobalVar v
vs2) (MapF RefCell r -> MapF RefCell r -> MapF RefCell r
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union MapF RefCell r
rs1 MapF RefCell r
rs2)

-- | Maps from global variables and global references to their values.
type GlobalContents sym = GlobalTable (GlobalEntry sym) (RefCellContents sym)

-- | A collection of updates to the global variables and global
-- references that have happened since a branch push.
type GlobalUpdates sym = GlobalTable (GlobalEntry sym) (RefCellUpdate sym)

-- | Apply a set of updates to the contents of global memory.
-- @GlobalVar@s cannot be deleted, so we just merge the @GlobalVar@
-- maps, preferring entries from the first argument. When merging the
-- @RefCell@ maps, a @RefCellUpdate Unassigned@ entry causes the
-- corresponding entry in the old map to be deleted.
applyGlobalUpdates :: forall sym . GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
applyGlobalUpdates :: forall sym.
GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
applyGlobalUpdates (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs1 MapF RefCell (RefCellUpdate sym)
rs1) (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs2 MapF RefCell (RefCellContents sym)
rs2) =
  MapF GlobalVar (GlobalEntry sym)
-> MapF RefCell (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable (MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type).
OrdF k =>
MapF k a -> MapF k a -> MapF k a
MapF.union MapF GlobalVar (GlobalEntry sym)
vs1 MapF GlobalVar (GlobalEntry sym)
vs2) (Identity (MapF RefCell (RefCellContents sym))
-> MapF RefCell (RefCellContents sym)
forall a. Identity a -> a
runIdentity ((forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellUpdate sym tp
 -> RefCellContents sym tp
 -> Identity (Maybe (RefCellContents sym tp)))
-> (MapF RefCell (RefCellUpdate sym)
    -> Identity (MapF RefCell (RefCellContents sym)))
-> (MapF RefCell (RefCellContents sym)
    -> Identity (MapF RefCell (RefCellContents sym)))
-> MapF RefCell (RefCellUpdate sym)
-> MapF RefCell (RefCellContents sym)
-> Identity (MapF RefCell (RefCellContents sym))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM RefCell tp
-> RefCellUpdate sym tp
-> RefCellContents sym tp
-> Identity (Maybe (RefCellContents sym tp))
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellContents sym tp
-> Identity (Maybe (RefCellContents sym tp))
both MapF RefCell (RefCellUpdate sym)
-> Identity (MapF RefCell (RefCellContents sym))
left MapF RefCell (RefCellContents sym)
-> Identity (MapF RefCell (RefCellContents sym))
forall a. a -> Identity a
Identity MapF RefCell (RefCellUpdate sym)
rs1 MapF RefCell (RefCellContents sym)
rs2))
  where
    upd :: forall tp. RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
    upd :: forall (tp :: CrucibleType).
RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
upd (RefCellUpdate PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
Unassigned) = Maybe (RefCellContents sym tp)
forall a. Maybe a
Nothing
    upd (RefCellUpdate (PE SymExpr sym BaseBoolType
p RegValue sym tp
e)) = RefCellContents sym tp -> Maybe (RefCellContents sym tp)
forall a. a -> Maybe a
Just (SymExpr sym BaseBoolType
-> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents SymExpr sym BaseBoolType
p RegValue sym tp
e)

    both :: forall tp. RefCell tp -> RefCellUpdate sym tp -> RefCellContents sym tp -> Identity (Maybe (RefCellContents sym tp))
    both :: forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellContents sym tp
-> Identity (Maybe (RefCellContents sym tp))
both RefCell tp
_ RefCellUpdate sym tp
u RefCellContents sym tp
_ = Maybe (RefCellContents sym tp)
-> Identity (Maybe (RefCellContents sym tp))
forall a. a -> Identity a
Identity (RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
forall (tp :: CrucibleType).
RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
upd RefCellUpdate sym tp
u)

    left :: MapF.MapF RefCell (RefCellUpdate sym) -> Identity (MapF.MapF RefCell (RefCellContents sym))
    left :: MapF RefCell (RefCellUpdate sym)
-> Identity (MapF RefCell (RefCellContents sym))
left MapF RefCell (RefCellUpdate sym)
m = MapF RefCell (RefCellContents sym)
-> Identity (MapF RefCell (RefCellContents sym))
forall a. a -> Identity a
Identity ((forall (tp :: CrucibleType).
 RefCellUpdate sym tp -> Maybe (RefCellContents sym tp))
-> MapF RefCell (RefCellUpdate sym)
-> MapF RefCell (RefCellContents sym)
forall {v} (f :: v -> Type) (g :: v -> Type) (ktp :: v -> Type).
(forall (tp :: v). f tp -> Maybe (g tp))
-> MapF ktp f -> MapF ktp g
MapF.mapMaybe RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
forall (tp :: CrucibleType).
RefCellUpdate sym tp -> Maybe (RefCellContents sym tp)
upd MapF RefCell (RefCellUpdate sym)
m)

------------------------------------------------------------------------
-- GlobalFrames

-- | The state of global memory as a stack of changes separated by
-- branch pushes. The second parameter of 'BranchFrame' caches
-- the combined view of memory as of the previous branch push.
data GlobalFrames (sym :: Type) =
    InitialFrame !(GlobalContents sym)
  | BranchFrame !(GlobalUpdates sym) (GlobalContents sym) !(GlobalFrames sym)

-- | The depth of this value represents the number of symbolic
-- branches currently pending. We use this primarily as a sanity check
-- to help find bugs where we fail to match up calls to
-- 'globalPushBranch' with 'globalAbortBranch'/'globalMuxFn'.
globalPendingBranches :: GlobalFrames sym -> Int
globalPendingBranches :: forall sym. GlobalFrames sym -> Int
globalPendingBranches (InitialFrame GlobalContents sym
_) = Int
0
globalPendingBranches (BranchFrame GlobalUpdates sym
_ GlobalContents sym
_ GlobalFrames sym
gf) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ GlobalFrames sym -> Int
forall sym. GlobalFrames sym -> Int
globalPendingBranches GlobalFrames sym
gf

-- | The empty set of global variable bindings.
emptyGlobalFrames :: GlobalFrames sym
emptyGlobalFrames :: forall sym. GlobalFrames sym
emptyGlobalFrames = GlobalContents sym -> GlobalFrames sym
forall sym. GlobalContents sym -> GlobalFrames sym
InitialFrame GlobalContents sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r
emptyGlobalTable

------------------------------------------------------------------------
-- GlobalTable

-- | A map from global variables to their value.
data SymGlobalState (sym :: Type) =
  GlobalState
  { forall sym. SymGlobalState sym -> GlobalFrames sym
globalFrames :: !(GlobalFrames sym)
    -- ^ The stack of updates to global memory, separated by branch
    -- pushes. This field only contains values with ordinary crucible
    -- types (i.e. not intrinsic), which do not have mux operations
    -- that require branch push notifications.
  , forall sym. SymGlobalState sym -> GlobalContents sym
globalIntrinsics :: !(GlobalContents sym)
    -- ^ The set of updates since initialization to vars and refs that
    -- have intrinsic or "any" types, which must be notified of
    -- branch pushes.
  }

-- | The empty set of global variable bindings.
emptyGlobals :: SymGlobalState sym
emptyGlobals :: forall sym. SymGlobalState sym
emptyGlobals = GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
forall sym.
GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
GlobalState GlobalFrames sym
forall sym. GlobalFrames sym
emptyGlobalFrames GlobalContents sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r
emptyGlobalTable

-- | Test whether this type could be an intrinsic type, which must be
-- notified of branch pushes and aborts.
needsNotification :: TypeRepr tp -> Bool
needsNotification :: forall (tp :: CrucibleType). TypeRepr tp -> Bool
needsNotification TypeRepr tp
tr =
  case TypeRepr tp
tr of
    IntrinsicRepr{} -> Bool
True
    TypeRepr tp
AnyRepr -> Bool
True
    TypeRepr tp
_ -> Bool
False

-- | Lookup a global variable in the state.
lookupGlobal :: GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal :: forall (tp :: CrucibleType) sym.
GlobalVar tp -> SymGlobalState sym -> Maybe (RegValue sym tp)
lookupGlobal GlobalVar tp
g SymGlobalState sym
gst
  | TypeRepr tp -> Bool
forall (tp :: CrucibleType). TypeRepr tp -> Bool
needsNotification (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
g) =
      GlobalEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
GlobalEntry sym tp -> RegValue sym tp
globalEntryValue (GlobalEntry sym tp -> RegValue sym tp)
-> Maybe (GlobalEntry sym tp) -> Maybe (RegValue sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalVar tp
-> MapF GlobalVar (GlobalEntry sym) -> Maybe (GlobalEntry sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup GlobalVar tp
g (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF GlobalVar (GlobalEntry sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF GlobalVar f
globalVars (SymGlobalState sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall sym. SymGlobalState sym -> GlobalContents sym
globalIntrinsics SymGlobalState sym
gst))
  | Bool
otherwise =
      GlobalEntry sym tp -> RegValue sym tp
forall sym (tp :: CrucibleType).
GlobalEntry sym tp -> RegValue sym tp
globalEntryValue (GlobalEntry sym tp -> RegValue sym tp)
-> Maybe (GlobalEntry sym tp) -> Maybe (RegValue sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalFrames sym -> Maybe (GlobalEntry sym tp)
go (SymGlobalState sym -> GlobalFrames sym
forall sym. SymGlobalState sym -> GlobalFrames sym
globalFrames SymGlobalState sym
gst)
  where
    -- We never have to search more than one level deep, because the
    -- 'BranchFrame' constructor caches the combined contents of the
    -- rest of the 'GlobalFrames'.
    go :: GlobalFrames sym -> Maybe (GlobalEntry sym tp)
go (InitialFrame GlobalTable (GlobalEntry sym) (RefCellContents sym)
c) = GlobalVar tp
-> MapF GlobalVar (GlobalEntry sym) -> Maybe (GlobalEntry sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup GlobalVar tp
g (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF GlobalVar (GlobalEntry sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF GlobalVar f
globalVars GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)
    go (BranchFrame GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
_) = GlobalVar tp
-> MapF GlobalVar (GlobalEntry sym) -> Maybe (GlobalEntry sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup GlobalVar tp
g (GlobalUpdates sym -> MapF GlobalVar (GlobalEntry sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF GlobalVar f
globalVars GlobalUpdates sym
u) Maybe (GlobalEntry sym tp)
-> Maybe (GlobalEntry sym tp) -> Maybe (GlobalEntry sym tp)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> GlobalVar tp
-> MapF GlobalVar (GlobalEntry sym) -> Maybe (GlobalEntry sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup GlobalVar tp
g (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF GlobalVar (GlobalEntry sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF GlobalVar f
globalVars GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)

-- | Set the value of a global in the state, or create a new global variable.
insertGlobal ::
  GlobalVar tp ->
  RegValue sym tp ->
  SymGlobalState sym ->
  SymGlobalState sym
insertGlobal :: forall (tp :: CrucibleType) sym.
GlobalVar tp
-> RegValue sym tp -> SymGlobalState sym -> SymGlobalState sym
insertGlobal GlobalVar tp
g RegValue sym tp
v SymGlobalState sym
gst
  | TypeRepr tp -> Bool
forall (tp :: CrucibleType). TypeRepr tp -> Bool
needsNotification (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
g) =
      SymGlobalState sym
gst{ globalIntrinsics = updateGlobalVars (MapF.insert g x) (globalIntrinsics gst) }
  | Bool
otherwise =
      SymGlobalState sym
gst{ globalFrames = upd (globalFrames gst) }
  where
    x :: GlobalEntry sym tp
x = RegValue sym tp -> GlobalEntry sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> GlobalEntry sym tp
GlobalEntry RegValue sym tp
v
    upd :: GlobalFrames sym -> GlobalFrames sym
upd (InitialFrame GlobalTable (GlobalEntry sym) (RefCellContents sym)
c) = GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalFrames sym
forall sym. GlobalContents sym -> GlobalFrames sym
InitialFrame ((MapF GlobalVar (GlobalEntry sym)
 -> MapF GlobalVar (GlobalEntry sym))
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
(MapF GlobalVar v -> MapF GlobalVar v)
-> GlobalTable v r -> GlobalTable v r
updateGlobalVars (GlobalVar tp
-> GlobalEntry sym tp
-> MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert GlobalVar tp
g GlobalEntry sym tp
x) GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)
    upd (BranchFrame GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
gf) = GlobalUpdates sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalFrames sym
-> GlobalFrames sym
forall sym.
GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
BranchFrame ((MapF GlobalVar (GlobalEntry sym)
 -> MapF GlobalVar (GlobalEntry sym))
-> GlobalUpdates sym -> GlobalUpdates sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
(MapF GlobalVar v -> MapF GlobalVar v)
-> GlobalTable v r -> GlobalTable v r
updateGlobalVars (GlobalVar tp
-> GlobalEntry sym tp
-> MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert GlobalVar tp
g GlobalEntry sym tp
x) GlobalUpdates sym
u) GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
gf
    -- NOTE: While global variables can be updated within branches, it
    -- should probably be forbidden to create a new global variable in
    -- a branch. However, we don't check for this currently. (An error
    -- will happen later when merging the branches if the set of
    -- global variables does not match.)

-- | Look up the value of a reference cell in the state.
lookupRef :: RefCell tp -> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
lookupRef :: forall (tp :: CrucibleType) sym.
RefCell tp
-> SymGlobalState sym -> PartExpr (Pred sym) (RegValue sym tp)
lookupRef RefCell tp
r SymGlobalState sym
gst
  | TypeRepr tp -> Bool
forall (tp :: CrucibleType). TypeRepr tp -> Bool
needsNotification (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) = Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall {sym} {tp :: CrucibleType}.
Maybe (RefCellContents sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
post (Maybe (RefCellContents sym tp)
 -> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp))
-> Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ RefCell tp
-> MapF RefCell (RefCellContents sym)
-> Maybe (RefCellContents sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup RefCell tp
r (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF RefCell g
globalRefs (SymGlobalState sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall sym. SymGlobalState sym -> GlobalContents sym
globalIntrinsics SymGlobalState sym
gst))
  | Bool
otherwise = GlobalFrames sym
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
go (SymGlobalState sym -> GlobalFrames sym
forall sym. SymGlobalState sym -> GlobalFrames sym
globalFrames SymGlobalState sym
gst)
  where
    -- We never have to search more than one level deep, because the
    -- 'BranchFrame' constructor caches the combined contents of the
    -- rest of the 'GlobalFrames'.
    post :: Maybe (RefCellContents sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
post = PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
-> (RefCellContents sym tp
    -> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp))
-> Maybe (RefCellContents sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
forall p v. PartExpr p v
Unassigned (\(RefCellContents SymExpr sym BaseBoolType
p RegValue sym tp
e) -> SymExpr sym BaseBoolType
-> RegValue sym tp
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
forall p v. p -> v -> PartExpr p v
PE SymExpr sym BaseBoolType
p RegValue sym tp
e)
    go :: GlobalFrames sym
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
go (InitialFrame GlobalTable (GlobalEntry sym) (RefCellContents sym)
c) = Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall {sym} {tp :: CrucibleType}.
Maybe (RefCellContents sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
post (Maybe (RefCellContents sym tp)
 -> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp))
-> Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ RefCell tp
-> MapF RefCell (RefCellContents sym)
-> Maybe (RefCellContents sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup RefCell tp
r (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF RefCell g
globalRefs GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)
    go (BranchFrame GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
_) =
      case RefCell tp
-> MapF RefCell (RefCellUpdate sym) -> Maybe (RefCellUpdate sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup RefCell tp
r (GlobalUpdates sym -> MapF RefCell (RefCellUpdate sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF RefCell g
globalRefs GlobalUpdates sym
u) of
        Just (RefCellUpdate PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
pe) -> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
pe
        Maybe (RefCellUpdate sym tp)
Nothing -> Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall {sym} {tp :: CrucibleType}.
Maybe (RefCellContents sym tp)
-> PartExpr (SymExpr sym BaseBoolType) (RegValue sym tp)
post (Maybe (RefCellContents sym tp)
 -> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp))
-> Maybe (RefCellContents sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
forall a b. (a -> b) -> a -> b
$ RefCell tp
-> MapF RefCell (RefCellContents sym)
-> Maybe (RefCellContents sym tp)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> Maybe (a tp)
MapF.lookup RefCell tp
r (GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
GlobalTable f g -> MapF RefCell g
globalRefs GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)

-- | Set the value of a reference cell in the state.
insertRef ::
  IsExprBuilder sym =>
  sym ->
  RefCell tp ->
  RegValue sym tp ->
  SymGlobalState sym ->
  SymGlobalState sym
insertRef :: forall sym (tp :: CrucibleType).
IsExprBuilder sym =>
sym
-> RefCell tp
-> RegValue sym tp
-> SymGlobalState sym
-> SymGlobalState sym
insertRef sym
sym RefCell tp
r RegValue sym tp
v = RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
updateRef RefCell tp
r (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
v)

-- | Write a partial value to a reference cell in the state.
updateRef ::
  -- IsExprBuilder sym =>
  RefCell tp ->
  PartExpr (Pred sym) (RegValue sym tp) ->
  SymGlobalState sym ->
  SymGlobalState sym
updateRef :: forall (tp :: CrucibleType) sym.
RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
updateRef RefCell tp
r PartExpr (Pred sym) (RegValue sym tp)
pe SymGlobalState sym
gst
  | TypeRepr tp -> Bool
forall (tp :: CrucibleType). TypeRepr tp -> Bool
needsNotification (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) =
      SymGlobalState sym
gst{ globalIntrinsics = updateGlobalRefs ins (globalIntrinsics gst) }
  | Bool
otherwise =
      SymGlobalState sym
gst{ globalFrames = upd (globalFrames gst) }
  where
    ins :: MapF RefCell (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
ins =
      case PartExpr (Pred sym) (RegValue sym tp)
pe of
        PartExpr (Pred sym) (RegValue sym tp)
Unassigned -> RefCell tp
-> MapF RefCell (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> MapF k a -> MapF k a
MapF.delete RefCell tp
r
        PE Pred sym
p RegValue sym tp
e -> RefCell tp
-> RefCellContents sym tp
-> MapF RefCell (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert RefCell tp
r (Pred sym -> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents Pred sym
p RegValue sym tp
e)
    upd :: GlobalFrames sym -> GlobalFrames sym
upd (InitialFrame GlobalTable (GlobalEntry sym) (RefCellContents sym)
c) = GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalFrames sym
forall sym. GlobalContents sym -> GlobalFrames sym
InitialFrame ((MapF RefCell (RefCellContents sym)
 -> MapF RefCell (RefCellContents sym))
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall (r :: CrucibleType -> Type) (v :: CrucibleType -> Type).
(MapF RefCell r -> MapF RefCell r)
-> GlobalTable v r -> GlobalTable v r
updateGlobalRefs MapF RefCell (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
ins GlobalTable (GlobalEntry sym) (RefCellContents sym)
c)
    upd (BranchFrame GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
gf) =
      GlobalUpdates sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalFrames sym
-> GlobalFrames sym
forall sym.
GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
BranchFrame ((MapF RefCell (RefCellUpdate sym)
 -> MapF RefCell (RefCellUpdate sym))
-> GlobalUpdates sym -> GlobalUpdates sym
forall (r :: CrucibleType -> Type) (v :: CrucibleType -> Type).
(MapF RefCell r -> MapF RefCell r)
-> GlobalTable v r -> GlobalTable v r
updateGlobalRefs (RefCell tp
-> RefCellUpdate sym tp
-> MapF RefCell (RefCellUpdate sym)
-> MapF RefCell (RefCellUpdate sym)
forall {v} (k :: v -> Type) (tp :: v) (a :: v -> Type).
OrdF k =>
k tp -> a tp -> MapF k a -> MapF k a
MapF.insert RefCell tp
r (PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
RefCellUpdate PartExpr (Pred sym) (RegValue sym tp)
pe)) GlobalUpdates sym
u) GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
gf

-- | Reset a reference cell to the uninitialized state. @'dropRef' r@ is
-- equivalent to @'updateRef' r 'Unassigned'@.
dropRef :: RefCell tp -> SymGlobalState sym -> SymGlobalState sym
dropRef :: forall (tp :: CrucibleType) sym.
RefCell tp -> SymGlobalState sym -> SymGlobalState sym
dropRef RefCell tp
r = RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
forall (tp :: CrucibleType) sym.
RefCell tp
-> PartExpr (Pred sym) (RegValue sym tp)
-> SymGlobalState sym
-> SymGlobalState sym
updateRef RefCell tp
r PartExpr (Pred sym) (RegValue sym tp)
forall p v. PartExpr p v
Unassigned

-- | Mark a branch point in the global state. Later calls to
-- 'globalMuxFn' will assume that the input states are identical up
-- until the most recent branch point.
globalPushBranch ::
  forall sym .
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  SymGlobalState sym ->
  IO (SymGlobalState sym)
globalPushBranch :: forall sym.
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> SymGlobalState sym
-> IO (SymGlobalState sym)
globalPushBranch sym
sym IntrinsicTypes sym
iTypes (GlobalState GlobalFrames sym
gf (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs MapF RefCell (RefCellContents sym)
rs)) =
  do -- Notify intrinsic-typed vars and refs of the branch push.
     MapF GlobalVar (GlobalEntry sym)
vs' <- (forall (tp :: CrucibleType).
 GlobalVar tp -> GlobalEntry sym tp -> IO (GlobalEntry sym tp))
-> MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey
            (\GlobalVar tp
v (GlobalEntry RegValue sym tp
e) ->
              RegValue sym tp -> GlobalEntry sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> GlobalEntry sym tp
GlobalEntry (RegValue sym tp -> GlobalEntry sym tp)
-> IO (RegValue sym tp) -> IO (GlobalEntry 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 (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
v) RegValue sym tp
e)
            MapF GlobalVar (GlobalEntry sym)
vs
     MapF RefCell (RefCellContents sym)
rs' <- (forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellContents sym tp -> IO (RefCellContents sym tp))
-> MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey
            (\RefCell tp
r (RefCellContents Pred sym
p RegValue sym tp
e) ->
              Pred sym -> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents Pred sym
p (RegValue sym tp -> RefCellContents sym tp)
-> IO (RegValue sym tp) -> IO (RefCellContents 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 (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) RegValue sym tp
e)
            MapF RefCell (RefCellContents sym)
rs
     --loc <- getCurrentProgramLoc sym
     --putStrLn $ unwords ["PUSH BRANCH:", show d, show $ plSourceLoc loc]
     let gf' :: GlobalFrames sym
gf' = GlobalUpdates sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalFrames sym
-> GlobalFrames sym
forall sym.
GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
BranchFrame GlobalUpdates sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r
emptyGlobalTable GlobalTable (GlobalEntry sym) (RefCellContents sym)
cache GlobalFrames sym
gf
     SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GlobalFrames sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> SymGlobalState sym
forall sym.
GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
GlobalState GlobalFrames sym
gf' (MapF GlobalVar (GlobalEntry sym)
-> MapF RefCell (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar (GlobalEntry sym)
vs' MapF RefCell (RefCellContents sym)
rs'))
  where
    cache :: GlobalTable (GlobalEntry sym) (RefCellContents sym)
cache =
      case GlobalFrames sym
gf of
        InitialFrame GlobalTable (GlobalEntry sym) (RefCellContents sym)
c -> GlobalTable (GlobalEntry sym) (RefCellContents sym)
c
        BranchFrame GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c GlobalFrames sym
_ -> GlobalUpdates sym
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall sym.
GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
applyGlobalUpdates GlobalUpdates sym
u GlobalTable (GlobalEntry sym) (RefCellContents sym)
c

-- | Merge a set of updates into the outermost frame of a stack of global frames.
abortBranchFrame :: GlobalUpdates sym -> GlobalFrames sym -> GlobalFrames sym
abortBranchFrame :: forall sym.
GlobalUpdates sym -> GlobalFrames sym -> GlobalFrames sym
abortBranchFrame GlobalUpdates sym
u (InitialFrame GlobalContents sym
c) = GlobalContents sym -> GlobalFrames sym
forall sym. GlobalContents sym -> GlobalFrames sym
InitialFrame (GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
forall sym.
GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
applyGlobalUpdates GlobalUpdates sym
u GlobalContents sym
c)
abortBranchFrame GlobalUpdates sym
u (BranchFrame GlobalUpdates sym
u' GlobalContents sym
c GlobalFrames sym
gf) = GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
forall sym.
GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
BranchFrame (GlobalUpdates sym -> GlobalUpdates sym -> GlobalUpdates sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r -> GlobalTable v r -> GlobalTable v r
mergeGlobalTable GlobalUpdates sym
u GlobalUpdates sym
u') GlobalContents sym
c GlobalFrames sym
gf

-- | Remove the most recent branch point marker, and thus cancel the
-- effect of the most recent 'globalPushBranch'.
globalAbortBranch ::
  forall sym .
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  SymGlobalState sym ->
  IO (SymGlobalState sym)

globalAbortBranch :: forall sym.
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> SymGlobalState sym
-> IO (SymGlobalState sym)
globalAbortBranch sym
sym IntrinsicTypes sym
iTypes (GlobalState (BranchFrame GlobalUpdates sym
u GlobalContents sym
_ GlobalFrames sym
gf) (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs MapF RefCell (RefCellContents sym)
rs)) =
  do -- Notify intrinsic-typed vars and refs of the branch abort.
     MapF GlobalVar (GlobalEntry sym)
vs' <- (forall (tp :: CrucibleType).
 GlobalVar tp -> GlobalEntry sym tp -> IO (GlobalEntry sym tp))
-> MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey
            (\GlobalVar tp
v (GlobalEntry RegValue sym tp
e) ->
              RegValue sym tp -> GlobalEntry sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> GlobalEntry sym tp
GlobalEntry (RegValue sym tp -> GlobalEntry sym tp)
-> IO (RegValue sym tp) -> IO (GlobalEntry 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 (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
v) RegValue sym tp
e)
            MapF GlobalVar (GlobalEntry sym)
vs
     MapF RefCell (RefCellContents sym)
rs' <- (forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellContents sym tp -> IO (RefCellContents sym tp))
-> MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey
            (\RefCell tp
r (RefCellContents Pred sym
p RegValue sym tp
e) ->
              Pred sym -> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents Pred sym
p (RegValue sym tp -> RefCellContents sym tp)
-> IO (RegValue sym tp) -> IO (RefCellContents 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 (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) RegValue sym tp
e)
            MapF RefCell (RefCellContents sym)
rs
     --loc <- getCurrentProgramLoc sym
     --putStrLn $ unwords ["ABORT BRANCH:", show (d-1), show $ plSourceLoc loc]
     let gf' :: GlobalFrames sym
gf' = GlobalUpdates sym -> GlobalFrames sym -> GlobalFrames sym
forall sym.
GlobalUpdates sym -> GlobalFrames sym -> GlobalFrames sym
abortBranchFrame GlobalUpdates sym
u GlobalFrames sym
gf
     SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
forall sym.
GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
GlobalState GlobalFrames sym
gf' (MapF GlobalVar (GlobalEntry sym)
-> MapF RefCell (RefCellContents sym) -> GlobalContents sym
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar (GlobalEntry sym)
vs' MapF RefCell (RefCellContents sym)
rs'))

globalAbortBranch sym
sym IntrinsicTypes sym
_ (GlobalState (InitialFrame GlobalContents sym
_) GlobalContents sym
_) =
  do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     String -> [String] -> IO (SymGlobalState sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"GlobalState.globalAbortBranch"
       [ String
"Attempting to commit global changes at branch depth 0"
       , String
"*** Location: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc)
       ]

muxPartialRegForType ::
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  TypeRepr tp ->
  MuxFn (Pred sym) (PartExpr (Pred sym) (RegValue sym tp))
muxPartialRegForType :: forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxFn (Pred sym) (PartExpr (Pred sym) (RegValue sym tp))
muxPartialRegForType sym
sym IntrinsicTypes sym
iteFns TypeRepr tp
tp =
  sym
-> (SymExpr sym BaseBoolType
    -> RegValue sym tp
    -> RegValue sym tp
    -> PartialT sym IO (RegValue sym tp))
-> SymExpr sym BaseBoolType
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
-> PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp)
-> IO
     (PartialWithErr () (SymExpr sym BaseBoolType) (RegValue sym tp))
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 (\SymExpr sym BaseBoolType
c RegValue sym tp
u RegValue sym tp
v -> IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
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 (IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp))
-> IO (RegValue sym tp) -> PartialT sym IO (RegValue sym tp)
forall a b. (a -> b) -> a -> 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
tp SymExpr sym BaseBoolType
c RegValue sym tp
u RegValue sym tp
v)

-- | A symbolic mux function for @GlobalContents@.
muxGlobalContents ::
  forall sym .
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  MuxFn (Pred sym) (GlobalContents sym)
muxGlobalContents :: forall sym.
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (GlobalContents sym)
muxGlobalContents sym
sym IntrinsicTypes sym
iteFns Pred sym
c (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs1 MapF RefCell (RefCellContents sym)
rs1) (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs2 MapF RefCell (RefCellContents sym)
rs2) =
  do MapF GlobalVar (GlobalEntry sym)
vs' <- (forall (tp :: CrucibleType).
 GlobalVar tp
 -> GlobalEntry sym tp
 -> GlobalEntry sym tp
 -> IO (Maybe (GlobalEntry sym tp)))
-> (MapF GlobalVar (GlobalEntry sym)
    -> IO (MapF GlobalVar (GlobalEntry sym)))
-> (MapF GlobalVar (GlobalEntry sym)
    -> IO (MapF GlobalVar (GlobalEntry sym)))
-> MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (Maybe (GlobalEntry sym tp))
forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (Maybe (GlobalEntry sym tp))
muxEntry MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
checkNullMap MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
checkNullMap MapF GlobalVar (GlobalEntry sym)
vs1 MapF GlobalVar (GlobalEntry sym)
vs2
     MapF RefCell (RefCellContents sym)
rs' <- (forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellContents sym tp
 -> RefCellContents sym tp
 -> IO (Maybe (RefCellContents sym tp)))
-> (MapF RefCell (RefCellContents sym)
    -> IO (MapF RefCell (RefCellContents sym)))
-> (MapF RefCell (RefCellContents sym)
    -> IO (MapF RefCell (RefCellContents sym)))
-> MapF RefCell (RefCellContents sym)
-> MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM RefCell tp
-> RefCellContents sym tp
-> RefCellContents sym tp
-> IO (Maybe (RefCellContents sym tp))
forall (tp :: CrucibleType).
RefCell tp
-> RefCellContents sym tp
-> RefCellContents sym tp
-> IO (Maybe (RefCellContents sym tp))
muxRef MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
refLeft MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
refRight MapF RefCell (RefCellContents sym)
rs1 MapF RefCell (RefCellContents sym)
rs2
     GlobalTable (GlobalEntry sym) (RefCellContents sym)
-> IO (GlobalTable (GlobalEntry sym) (RefCellContents sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MapF GlobalVar (GlobalEntry sym)
-> MapF RefCell (RefCellContents sym)
-> GlobalTable (GlobalEntry sym) (RefCellContents sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar (GlobalEntry sym)
vs' MapF RefCell (RefCellContents sym)
rs')
  where
    muxEntry :: GlobalVar tp
             -> GlobalEntry sym tp
             -> GlobalEntry sym tp
             -> IO (Maybe (GlobalEntry sym tp))
    muxEntry :: forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (Maybe (GlobalEntry sym tp))
muxEntry GlobalVar tp
g (GlobalEntry RegValue sym tp
u) (GlobalEntry RegValue sym tp
v) =
      GlobalEntry sym tp -> Maybe (GlobalEntry sym tp)
forall a. a -> Maybe a
Just (GlobalEntry sym tp -> Maybe (GlobalEntry sym tp))
-> (RegValue sym tp -> GlobalEntry sym tp)
-> RegValue sym tp
-> Maybe (GlobalEntry sym tp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegValue sym tp -> GlobalEntry sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> GlobalEntry sym tp
GlobalEntry (RegValue sym tp -> Maybe (GlobalEntry sym tp))
-> IO (RegValue sym tp) -> IO (Maybe (GlobalEntry 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 (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
g) Pred sym
c RegValue sym tp
u RegValue sym tp
v

    muxRef :: RefCell tp
           -> RefCellContents sym tp
           -> RefCellContents sym tp
           -> IO (Maybe (RefCellContents sym tp))
    muxRef :: forall (tp :: CrucibleType).
RefCell tp
-> RefCellContents sym tp
-> RefCellContents sym tp
-> IO (Maybe (RefCellContents sym tp))
muxRef RefCell tp
r (RefCellContents Pred sym
pu RegValue sym tp
u) (RefCellContents Pred sym
pv RegValue sym tp
v) =
      do RegValue sym tp
uv <- 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 (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) Pred sym
c RegValue sym tp
u RegValue sym tp
v
         Pred sym
p <- 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
sym Pred sym
c Pred sym
pu Pred sym
pv
         Maybe (RefCellContents sym tp)
-> IO (Maybe (RefCellContents sym tp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe (RefCellContents sym tp)
 -> IO (Maybe (RefCellContents sym tp)))
-> (RefCellContents sym tp -> Maybe (RefCellContents sym tp))
-> RefCellContents sym tp
-> IO (Maybe (RefCellContents sym tp))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCellContents sym tp -> Maybe (RefCellContents sym tp)
forall a. a -> Maybe a
Just (RefCellContents sym tp -> IO (Maybe (RefCellContents sym tp)))
-> RefCellContents sym tp -> IO (Maybe (RefCellContents sym tp))
forall a b. (a -> b) -> a -> b
$ Pred sym -> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents Pred sym
p RegValue sym tp
uv

    -- Make a partial value undefined unless the given predicate holds.
    restrictRefCellContents :: Pred sym -> RefCellContents sym tp -> IO (RefCellContents sym tp)
    restrictRefCellContents :: forall (tp :: CrucibleType).
Pred sym -> RefCellContents sym tp -> IO (RefCellContents sym tp)
restrictRefCellContents Pred sym
p1 (RefCellContents Pred sym
p2 RegValue sym tp
x) =
      do Pred sym
p' <- sym -> Pred sym -> Pred sym -> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
andPred sym
sym Pred sym
p1 Pred sym
p2
         RefCellContents sym tp -> IO (RefCellContents sym tp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Pred sym -> RegValue sym tp -> RefCellContents sym tp
forall sym (tp :: CrucibleType).
Pred sym -> RegValue sym tp -> RefCellContents sym tp
RefCellContents Pred sym
p' RegValue sym tp
x)

    refLeft :: MapF.MapF RefCell (RefCellContents sym) -> IO (MapF.MapF RefCell (RefCellContents sym))
    refLeft :: MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
refLeft MapF RefCell (RefCellContents sym)
m = (forall (s :: CrucibleType).
 RefCellContents sym s -> IO (RefCellContents sym s))
-> MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF RefCell e -> m (MapF RefCell f)
traverseF (Pred sym -> RefCellContents sym s -> IO (RefCellContents sym s)
forall (tp :: CrucibleType).
Pred sym -> RefCellContents sym tp -> IO (RefCellContents sym tp)
restrictRefCellContents Pred sym
c) MapF RefCell (RefCellContents sym)
m

    refRight :: MapF.MapF RefCell (RefCellContents sym) -> IO (MapF.MapF RefCell (RefCellContents sym))
    refRight :: MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
refRight MapF RefCell (RefCellContents sym)
m =
      do Pred sym
cnot <- sym -> Pred sym -> IO (Pred sym)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
notPred sym
sym Pred sym
c
         (forall (s :: CrucibleType).
 RefCellContents sym s -> IO (RefCellContents sym s))
-> MapF RefCell (RefCellContents sym)
-> IO (MapF RefCell (RefCellContents sym))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF RefCell e -> m (MapF RefCell f)
traverseF (Pred sym -> RefCellContents sym s -> IO (RefCellContents sym s)
forall (tp :: CrucibleType).
Pred sym -> RefCellContents sym tp -> IO (RefCellContents sym tp)
restrictRefCellContents Pred sym
cnot) MapF RefCell (RefCellContents sym)
m

    -- Sets of global variables are required to be the same in both branches.
    checkNullMap :: MapF.MapF GlobalVar (GlobalEntry sym)
                 -> IO (MapF.MapF GlobalVar (GlobalEntry sym))
    checkNullMap :: MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
checkNullMap MapF GlobalVar (GlobalEntry sym)
m
      | MapF GlobalVar (GlobalEntry sym) -> Bool
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a -> Bool
MapF.null MapF GlobalVar (GlobalEntry sym)
m = MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MapF GlobalVar (GlobalEntry sym)
m
      | Bool
otherwise =
        String -> [String] -> IO (MapF GlobalVar (GlobalEntry sym))
forall a. HasCallStack => String -> [String] -> a
panic String
"GlobalState.globalMuxFn"
                [ String
"Different global variables in each branch." ]

data EitherOrBoth f g (tp :: k) =
  JustLeft (f tp) | Both (f tp) (g tp) | JustRight (g tp)

-- | A symbolic mux function for @GlobalUpdates@. For cases where a
-- pre-existing value is updated only on one side, we require a
-- @GlobalContents@ to look up the previous value to use in place of
-- the missing update.
muxGlobalUpdates ::
  forall sym .
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  GlobalContents sym ->
  MuxFn (Pred sym) (GlobalUpdates sym)
muxGlobalUpdates :: forall sym.
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> GlobalContents sym
-> MuxFn (Pred sym) (GlobalUpdates sym)
muxGlobalUpdates sym
sym IntrinsicTypes sym
iteFns (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs0 MapF RefCell (RefCellContents sym)
rs0) Pred sym
c (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs1 MapF RefCell (RefCellUpdate sym)
rs1) (GlobalTable MapF GlobalVar (GlobalEntry sym)
vs2 MapF RefCell (RefCellUpdate sym)
rs2) =
  do -- Zip together the two maps of globals.
     MapF GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
vs3 <- (forall (tp :: CrucibleType).
 GlobalVar tp
 -> GlobalEntry sym tp
 -> GlobalEntry sym tp
 -> IO
      (Maybe (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp)))
-> (MapF GlobalVar (GlobalEntry sym)
    -> IO
         (MapF
            GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))))
-> (MapF GlobalVar (GlobalEntry sym)
    -> IO
         (MapF
            GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))))
-> MapF GlobalVar (GlobalEntry sym)
-> MapF GlobalVar (GlobalEntry sym)
-> IO
     (MapF GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym)))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM
            (\GlobalVar tp
_ GlobalEntry sym tp
x GlobalEntry sym tp
y -> Maybe (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp)
-> IO (Maybe (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
-> Maybe (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp)
forall a. a -> Maybe a
Just (GlobalEntry sym tp
-> GlobalEntry sym tp
-> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
f tp -> g tp -> EitherOrBoth f g tp
Both GlobalEntry sym tp
x GlobalEntry sym tp
y)))
            ((forall (s :: CrucibleType).
 GlobalEntry sym s
 -> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s))
-> MapF GlobalVar (GlobalEntry sym)
-> IO
     (MapF GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym)))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF GlobalVar e -> m (MapF GlobalVar f)
traverseF (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
-> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
 -> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s))
-> (GlobalEntry sym s
    -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
-> GlobalEntry sym s
-> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalEntry sym s
-> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
f tp -> EitherOrBoth f g tp
JustLeft))
            ((forall (s :: CrucibleType).
 GlobalEntry sym s
 -> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s))
-> MapF GlobalVar (GlobalEntry sym)
-> IO
     (MapF GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym)))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF GlobalVar e -> m (MapF GlobalVar f)
traverseF (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
-> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
 -> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s))
-> (GlobalEntry sym s
    -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
-> GlobalEntry sym s
-> IO (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalEntry sym s
-> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) s
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
g tp -> EitherOrBoth f g tp
JustRight))
            MapF GlobalVar (GlobalEntry sym)
vs1 MapF GlobalVar (GlobalEntry sym)
vs2
     MapF GlobalVar (GlobalEntry sym)
vs' <- (forall (tp :: CrucibleType).
 GlobalVar tp
 -> GlobalEntry sym tp
 -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
 -> IO (Maybe (GlobalEntry sym tp)))
-> (MapF GlobalVar (GlobalEntry sym)
    -> IO (MapF GlobalVar (GlobalEntry sym)))
-> (MapF
      GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
    -> IO (MapF GlobalVar (GlobalEntry sym)))
-> MapF GlobalVar (GlobalEntry sym)
-> MapF
     GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
-> IO (MapF GlobalVar (GlobalEntry sym))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM
            (\GlobalVar tp
k GlobalEntry sym tp
x0 EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
e ->
              GlobalEntry sym tp -> Maybe (GlobalEntry sym tp)
forall a. a -> Maybe a
Just (GlobalEntry sym tp -> Maybe (GlobalEntry sym tp))
-> IO (GlobalEntry sym tp) -> IO (Maybe (GlobalEntry sym tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              case EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
e of
                JustLeft GlobalEntry sym tp
x1 -> GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
muxEntry GlobalVar tp
k GlobalEntry sym tp
x1 GlobalEntry sym tp
x0 -- use old value x0 for right side
                JustRight GlobalEntry sym tp
x2 -> GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
muxEntry GlobalVar tp
k GlobalEntry sym tp
x0 GlobalEntry sym tp
x2 -- use old value x0 for left side
                Both GlobalEntry sym tp
x1 GlobalEntry sym tp
x2 -> GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
muxEntry GlobalVar tp
k GlobalEntry sym tp
x1 GlobalEntry sym tp
x2)
            (\MapF GlobalVar (GlobalEntry sym)
_ -> MapF GlobalVar (GlobalEntry sym)
-> IO (MapF GlobalVar (GlobalEntry sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MapF GlobalVar (GlobalEntry sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty) -- old values updated on neither side are excluded from merged updates
            ((forall (tp :: CrucibleType).
 GlobalVar tp
 -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
 -> IO (GlobalEntry sym tp))
-> MapF
     GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
-> IO (MapF GlobalVar (GlobalEntry sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey ((forall (tp :: CrucibleType).
  GlobalVar tp
  -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
  -> IO (GlobalEntry sym tp))
 -> MapF
      GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
 -> IO (MapF GlobalVar (GlobalEntry sym)))
-> (forall (tp :: CrucibleType).
    GlobalVar tp
    -> EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
    -> IO (GlobalEntry sym tp))
-> MapF
     GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
-> IO (MapF GlobalVar (GlobalEntry sym))
forall a b. (a -> b) -> a -> b
$ \GlobalVar tp
k EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
e ->
              case EitherOrBoth (GlobalEntry sym) (GlobalEntry sym) tp
e of
                JustLeft GlobalEntry sym tp
_ -> IO (GlobalEntry sym tp)
forall {a}. a
panicNull -- panic if there is no old value
                JustRight GlobalEntry sym tp
_ -> IO (GlobalEntry sym tp)
forall {a}. a
panicNull -- panic if there is no old value
                Both GlobalEntry sym tp
x1 GlobalEntry sym tp
x2 -> GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
muxEntry GlobalVar tp
k GlobalEntry sym tp
x1 GlobalEntry sym tp
x2)
            MapF GlobalVar (GlobalEntry sym)
vs0
            MapF GlobalVar (EitherOrBoth (GlobalEntry sym) (GlobalEntry sym))
vs3

     -- Zip together the two maps of references.
     MapF RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
rs3 <- (forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellUpdate sym tp
 -> RefCellUpdate sym tp
 -> IO
      (Maybe (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp)))
-> (MapF RefCell (RefCellUpdate sym)
    -> IO
         (MapF
            RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))))
-> (MapF RefCell (RefCellUpdate sym)
    -> IO
         (MapF
            RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))))
-> MapF RefCell (RefCellUpdate sym)
-> MapF RefCell (RefCellUpdate sym)
-> IO
     (MapF
        RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym)))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM
            (\RefCell tp
_ RefCellUpdate sym tp
x RefCellUpdate sym tp
y -> Maybe (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp)
-> IO
     (Maybe (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
-> Maybe (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp)
forall a. a -> Maybe a
Just (RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
f tp -> g tp -> EitherOrBoth f g tp
Both RefCellUpdate sym tp
x RefCellUpdate sym tp
y)))
            ((forall (s :: CrucibleType).
 RefCellUpdate sym s
 -> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s))
-> MapF RefCell (RefCellUpdate sym)
-> IO
     (MapF
        RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym)))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF RefCell e -> m (MapF RefCell f)
traverseF (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
-> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
 -> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s))
-> (RefCellUpdate sym s
    -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
-> RefCellUpdate sym s
-> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCellUpdate sym s
-> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
f tp -> EitherOrBoth f g tp
JustLeft))
            ((forall (s :: CrucibleType).
 RefCellUpdate sym s
 -> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s))
-> MapF RefCell (RefCellUpdate sym)
-> IO
     (MapF
        RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym)))
forall {k} (t :: (k -> Type) -> Type) (m :: Type -> Type)
       (e :: k -> Type) (f :: k -> Type).
(TraversableF t, Applicative m) =>
(forall (s :: k). e s -> m (f s)) -> t e -> m (t f)
forall (m :: Type -> Type) (e :: CrucibleType -> Type)
       (f :: CrucibleType -> Type).
Applicative m =>
(forall (s :: CrucibleType). e s -> m (f s))
-> MapF RefCell e -> m (MapF RefCell f)
traverseF (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
-> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
 -> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s))
-> (RefCellUpdate sym s
    -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
-> RefCellUpdate sym s
-> IO (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RefCellUpdate sym s
-> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) s
forall k (f :: k -> Type) (g :: k -> Type) (tp :: k).
g tp -> EitherOrBoth f g tp
JustRight))
            MapF RefCell (RefCellUpdate sym)
rs1 MapF RefCell (RefCellUpdate sym)
rs2
     MapF RefCell (RefCellUpdate sym)
rs' <- (forall (tp :: CrucibleType).
 RefCell tp
 -> RefCellContents sym tp
 -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
 -> IO (Maybe (RefCellUpdate sym tp)))
-> (MapF RefCell (RefCellContents sym)
    -> IO (MapF RefCell (RefCellUpdate sym)))
-> (MapF
      RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
    -> IO (MapF RefCell (RefCellUpdate sym)))
-> MapF RefCell (RefCellContents sym)
-> MapF
     RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
-> IO (MapF RefCell (RefCellUpdate sym))
forall {v} (k :: v -> Type) (a :: v -> Type) (b :: v -> Type)
       (c :: v -> Type) (m :: Type -> Type).
(Applicative m, OrdF k) =>
(forall (tp :: v). k tp -> a tp -> b tp -> m (Maybe (c tp)))
-> (MapF k a -> m (MapF k c))
-> (MapF k b -> m (MapF k c))
-> MapF k a
-> MapF k b
-> m (MapF k c)
MapF.mergeWithKeyM
            (\RefCell tp
k (RefCellContents Pred sym
p RegValue sym tp
e) EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
eb ->
              let x0 :: RefCellUpdate sym tp
x0 = PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
RefCellUpdate (Pred sym
-> RegValue sym tp -> PartExpr (Pred sym) (RegValue sym tp)
forall p v. p -> v -> PartExpr p v
PE Pred sym
p RegValue sym tp
e) in
              RefCellUpdate sym tp -> Maybe (RefCellUpdate sym tp)
forall a. a -> Maybe a
Just (RefCellUpdate sym tp -> Maybe (RefCellUpdate sym tp))
-> IO (RefCellUpdate sym tp) -> IO (Maybe (RefCellUpdate sym tp))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              case EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
eb of
                JustLeft RefCellUpdate sym tp
x1 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
x1 RefCellUpdate sym tp
x0 -- use old value x0 for right side
                JustRight RefCellUpdate sym tp
x2 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
x0 RefCellUpdate sym tp
x2 -- use old value x0 for left side
                Both RefCellUpdate sym tp
x1 RefCellUpdate sym tp
x2 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
x1 RefCellUpdate sym tp
x2)
            (\MapF RefCell (RefCellContents sym)
_ -> MapF RefCell (RefCellUpdate sym)
-> IO (MapF RefCell (RefCellUpdate sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return MapF RefCell (RefCellUpdate sym)
forall {v} (k :: v -> Type) (a :: v -> Type). MapF k a
MapF.empty) -- old values updated on neither side are excluded from merged updates
            ((forall (tp :: CrucibleType).
 RefCell tp
 -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
 -> IO (RefCellUpdate sym tp))
-> MapF
     RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
-> IO (MapF RefCell (RefCellUpdate sym))
forall {v} (m :: Type -> Type) (ktp :: v -> Type) (f :: v -> Type)
       (g :: v -> Type).
Applicative m =>
(forall (tp :: v). ktp tp -> f tp -> m (g tp))
-> MapF ktp f -> m (MapF ktp g)
MapF.traverseWithKey ((forall (tp :: CrucibleType).
  RefCell tp
  -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
  -> IO (RefCellUpdate sym tp))
 -> MapF
      RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
 -> IO (MapF RefCell (RefCellUpdate sym)))
-> (forall (tp :: CrucibleType).
    RefCell tp
    -> EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
    -> IO (RefCellUpdate sym tp))
-> MapF
     RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
-> IO (MapF RefCell (RefCellUpdate sym))
forall a b. (a -> b) -> a -> b
$ \RefCell tp
k EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
e ->
              case EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym) tp
e of
                JustLeft RefCellUpdate sym tp
x1 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
x1 RefCellUpdate sym tp
forall (tp :: CrucibleType). RefCellUpdate sym tp
undef -- x1 was newly-created on left side, undefined on right
                JustRight RefCellUpdate sym tp
x2 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
forall (tp :: CrucibleType). RefCellUpdate sym tp
undef RefCellUpdate sym tp
x2 -- x2 was newly-created on right side, undefined on left
                Both RefCellUpdate sym tp
x1 RefCellUpdate sym tp
x2 -> RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
k RefCellUpdate sym tp
x1 RefCellUpdate sym tp
x2)
            MapF RefCell (RefCellContents sym)
rs0
            MapF RefCell (EitherOrBoth (RefCellUpdate sym) (RefCellUpdate sym))
rs3
     GlobalTable (GlobalEntry sym) (RefCellUpdate sym)
-> IO (GlobalTable (GlobalEntry sym) (RefCellUpdate sym))
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (MapF GlobalVar (GlobalEntry sym)
-> MapF RefCell (RefCellUpdate sym)
-> GlobalTable (GlobalEntry sym) (RefCellUpdate sym)
forall (f :: CrucibleType -> Type) (g :: CrucibleType -> Type).
MapF GlobalVar f -> MapF RefCell g -> GlobalTable f g
GlobalTable MapF GlobalVar (GlobalEntry sym)
vs' MapF RefCell (RefCellUpdate sym)
rs')
  where
    undef :: forall tp. RefCellUpdate sym tp
    undef :: forall (tp :: CrucibleType). RefCellUpdate sym tp
undef = PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
RefCellUpdate PartExpr (Pred sym) (RegValue sym tp)
forall p v. PartExpr p v
Unassigned

    muxEntry :: GlobalVar tp
             -> GlobalEntry sym tp
             -> GlobalEntry sym tp
             -> IO (GlobalEntry sym tp)
    muxEntry :: forall (tp :: CrucibleType).
GlobalVar tp
-> GlobalEntry sym tp
-> GlobalEntry sym tp
-> IO (GlobalEntry sym tp)
muxEntry GlobalVar tp
g (GlobalEntry RegValue sym tp
u) (GlobalEntry RegValue sym tp
v) =
      RegValue sym tp -> GlobalEntry sym tp
forall sym (tp :: CrucibleType).
RegValue sym tp -> GlobalEntry sym tp
GlobalEntry (RegValue sym tp -> GlobalEntry sym tp)
-> IO (RegValue sym tp) -> IO (GlobalEntry 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 (GlobalVar tp -> TypeRepr tp
forall (tp :: CrucibleType). GlobalVar tp -> TypeRepr tp
globalType GlobalVar tp
g) Pred sym
c RegValue sym tp
u RegValue sym tp
v

    muxRef :: RefCell tp
           -> RefCellUpdate sym tp
           -> RefCellUpdate sym tp
           -> IO (RefCellUpdate sym tp)
    muxRef :: forall (tp :: CrucibleType).
RefCell tp
-> RefCellUpdate sym tp
-> RefCellUpdate sym tp
-> IO (RefCellUpdate sym tp)
muxRef RefCell tp
r (RefCellUpdate PartExpr (Pred sym) (RegValue sym tp)
pe1) (RefCellUpdate PartExpr (Pred sym) (RegValue sym tp)
pe2) =
      PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
forall sym (tp :: CrucibleType).
PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp
RefCellUpdate (PartExpr (Pred sym) (RegValue sym tp) -> RefCellUpdate sym tp)
-> IO (PartExpr (Pred sym) (RegValue sym tp))
-> IO (RefCellUpdate sym tp)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxFn (Pred sym) (PartExpr (Pred sym) (RegValue sym tp))
forall sym (tp :: CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> TypeRepr tp
-> MuxFn (Pred sym) (PartExpr (Pred sym) (RegValue sym tp))
muxPartialRegForType sym
sym IntrinsicTypes sym
iteFns (RefCell tp -> TypeRepr tp
forall (tp :: CrucibleType). RefCell tp -> TypeRepr tp
refType RefCell tp
r) Pred sym
c PartExpr (Pred sym) (RegValue sym tp)
pe1 PartExpr (Pred sym) (RegValue sym tp)
pe2

    panicNull :: a
panicNull =
      String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"GlobalState.globalMuxFn"
            [ String
"Different global variables in each branch." ]

-- | Compute a symbolic if-then-else on two global states. The
-- function assumes that the two states were identical up until the
-- most recent branch point marked by 'globalPushBranch'. This most
-- recent branch point marker is also popped from the stack.
globalMuxFn ::
  forall sym .
  IsSymInterface sym =>
  sym ->
  IntrinsicTypes sym ->
  MuxFn (Pred sym) (SymGlobalState sym)

globalMuxFn :: forall sym.
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (SymGlobalState sym)
globalMuxFn sym
sym IntrinsicTypes sym
iteFns Pred sym
cond
  (GlobalState (BranchFrame GlobalUpdates sym
u1 GlobalContents sym
cache1 GlobalFrames sym
gf1) GlobalContents sym
s1)
  (GlobalState (BranchFrame GlobalUpdates sym
u2 GlobalContents sym
_cache2 GlobalFrames sym
gf2) GlobalContents sym
s2)
  | GlobalFrames sym -> Int
forall sym. GlobalFrames sym -> Int
globalPendingBranches GlobalFrames sym
gf1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== GlobalFrames sym -> Int
forall sym. GlobalFrames sym -> Int
globalPendingBranches GlobalFrames sym
gf2 =
    -- We assume gf1 is in fact equal to gf2, which should be the case
    -- if we've followed the appropriate branching discipline.
    do GlobalUpdates sym
u3 <- sym
-> IntrinsicTypes sym
-> GlobalContents sym
-> MuxFn (Pred sym) (GlobalUpdates sym)
forall sym.
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> GlobalContents sym
-> MuxFn (Pred sym) (GlobalUpdates sym)
muxGlobalUpdates sym
sym IntrinsicTypes sym
iteFns GlobalContents sym
cache1 Pred sym
cond GlobalUpdates sym
u1 GlobalUpdates sym
u2
       GlobalContents sym
s3 <- sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (GlobalContents sym)
forall sym.
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (GlobalContents sym)
muxGlobalContents sym
sym IntrinsicTypes sym
iteFns Pred sym
cond GlobalContents sym
s1 GlobalContents sym
s2
       --let gf' = updateFrame (mergeGlobalUpdates x') gf1
       let gf3 :: GlobalFrames sym
gf3 =
             case GlobalFrames sym
gf1 of
               InitialFrame GlobalContents sym
c' -> GlobalContents sym -> GlobalFrames sym
forall sym. GlobalContents sym -> GlobalFrames sym
InitialFrame (GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
forall sym.
GlobalUpdates sym -> GlobalContents sym -> GlobalContents sym
applyGlobalUpdates GlobalUpdates sym
u3 GlobalContents sym
c')
               BranchFrame GlobalUpdates sym
u' GlobalContents sym
c' GlobalFrames sym
gf' -> GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
forall sym.
GlobalUpdates sym
-> GlobalContents sym -> GlobalFrames sym -> GlobalFrames sym
BranchFrame (GlobalUpdates sym -> GlobalUpdates sym -> GlobalUpdates sym
forall (v :: CrucibleType -> Type) (r :: CrucibleType -> Type).
GlobalTable v r -> GlobalTable v r -> GlobalTable v r
mergeGlobalTable GlobalUpdates sym
u3 GlobalUpdates sym
u') GlobalContents sym
c' GlobalFrames sym
gf'
       SymGlobalState sym -> IO (SymGlobalState sym)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
forall sym.
GlobalFrames sym -> GlobalContents sym -> SymGlobalState sym
GlobalState GlobalFrames sym
gf3 GlobalContents sym
s3)

globalMuxFn sym
sym IntrinsicTypes sym
_ Pred sym
_ (GlobalState GlobalFrames sym
gf1 GlobalContents sym
_) (GlobalState GlobalFrames sym
gf2 GlobalContents sym
_) =
  do ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
getCurrentProgramLoc sym
sym
     String -> [String] -> IO (SymGlobalState sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"GlobalState.globalMuxFn"
           [ String
"Attempting to merge global states of incorrect branch depths:"
           , String
" *** Depth 1:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (GlobalFrames sym -> Int
forall sym. GlobalFrames sym -> Int
globalPendingBranches GlobalFrames sym
gf1)
           , String
" *** Depth 2:  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (GlobalFrames sym -> Int
forall sym. GlobalFrames sym -> Int
globalPendingBranches GlobalFrames sym
gf2)
           , String
" *** Location: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Position -> String
forall a. Show a => a -> String
show (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc)
           ]